Library mcertikos.driver.CertiKOSproof

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
*********************************************************************** 

Require mcertikos.devdrivers.ConsoleBuffIntroGenLink.
Require mcertikos.devdrivers.AbsConsoleBuffIntroGenLink.
Require mcertikos.devdrivers.SerialIntroGenLink.
Require mcertikos.devdrivers.SerialGenLink.
Require mcertikos.devdrivers.IoApicGenLink.
Require mcertikos.devdrivers.LApicGenLink.
Require mcertikos.devdrivers.ConsoleGenLink.
Require mcertikos.devdrivers.HandlerIntroGenLink.
Require mcertikos.devdrivers.HandlerSwGenLink.
Require mcertikos.devdrivers.HandlerAsmGenLink.
Require mcertikos.devdrivers.HandlerCxtGenLink.
Require mcertikos.devdrivers.HandlerOpGenLink.
Require mcertikos.devdrivers.HandlerGenLink.
Require mcertikos.devdrivers.AbsHandlerGenLink.
Require mcertikos.mm.ContainerGenLink.
Require mcertikos.mm.ALInitGenLink.
Require mcertikos.mm.ALOpGenLink.
Require mcertikos.mm.ALGenLink.
Require mcertikos.mm.PTIntroGenLink.
Require mcertikos.mm.PTOpGenLink.
Require mcertikos.mm.PTCommGenLink.
Require mcertikos.mm.PTKernGenLink.
Require mcertikos.mm.PTInitGenLink.
Require mcertikos.mm.PTBitGenLink.
Require mcertikos.mm.PTNewGenLink.
Require mcertikos.mm.ShareIntroGenLink.
Require mcertikos.mm.ShareOpGenLink.
Require mcertikos.mm.ShareGenLink.
Require mcertikos.proc.KContextGenLink.
Require mcertikos.proc.KContextNewGenLink.
Require mcertikos.proc.ThreadIntroGenLink.
Require mcertikos.proc.ThreadInitGenLink.
Require mcertikos.proc.QueueIntroGenLink.
Require mcertikos.proc.QueueInitGenLink.
Require mcertikos.proc.AbQueueGenLink.
Require mcertikos.proc.CurIDGenLink.
Require mcertikos.proc.ThreadSchedGenLink.
Require mcertikos.proc.ThreadGenLink.
Require mcertikos.proc.IPCIntroGenLink.
Require mcertikos.proc.IPCGenLink.
Require mcertikos.proc.UCtxtIntroGenLink.
Require mcertikos.proc.ProcGenLink.
Require mcertikos.trap.TrapArgGenLink.
Require mcertikos.trap.TrapGenLink.
Require mcertikos.trap.DispatchGenLink.
Require mcertikos.trap.SysCallGenLink.
Require mcertikos.virt.intel.EPTIntroGenLink.
Require mcertikos.virt.intel.EPTOpGenLink.
Require mcertikos.virt.intel.EPTInitGenLink.
Require mcertikos.virt.intel.VMCSIntroGenLink.
Require mcertikos.virt.intel.VMCSInitGenLink.
Require mcertikos.virt.intel.VMXIntroGenLink.
Require mcertikos.virt.intel.VMXInitGenLink.
Require Import CompCertiKOSproofImpl.
Require Import RealParamsImpl.
Require Import CertiKOSAux.

Remove Hints
    MemimplX.memory_model
    MemimplX.memory_model_x
    StencilImpl.ptree_stencil_ops
    StencilImpl.ptree_stencil_prf
  : typeclass_instances.

Section CertiKOSCorrect.

  Inductive exists_program_simulation
            (s : stencil)
            (CTXT : LAsm.module)
            {CDATA}
            (HLayer : CompatLayerDef.compatlayer CDATA)
            (HSem LSem : LAsm.program → Smallstep.semantics Integers.Int.int)
            (pl : LAsm.program) : Prop :=
    exists_program_simulation_intro :
      ∀ ph : LAsm.program,
        backward_simulation (HSem ph) (LSem pl) →
        make_program s CTXT HLayer = OK ph →
        exists_program_simulation s CTXT HLayer HSem LSem pl.

  Theorem CertiKOS_correct´:
    ∀ (s: stencil) (CTXT: LAsm.module) combined_module combined
           (builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
      CertiKOS.certikos_plus_ctxt CTXT = OK combined_module →
      make_program s combined_module (MBoot.mboot ⊕ L64) = OK combined →
      exists_program_simulation
        s CTXT (TSysCall.tsyscall ⊕ L64)
        (LAsm.semantics (lcfg_ops := LC (TSysCall.tsyscall ⊕ L64)))
        (LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)))
        combined.
  Proof.
    intros s CTXT cM combined ? Hkern Hcomb.

    assert (pl_single_events :
              single_events (LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)) combined)).
    { apply LAsmModuleSemEvent.LAsm_single_events;
      [ Decision.decision | assumption ].
    }

    unfold CertiKOS.certikos_plus_ctxt in ×.
    unfold CertiKOS.add_loc in ×.
    inv_monad´ Hkern.
    unfold ret, res_monad_ops in ×.
    unfold_all_into_link_impl.

    destruct_mpe ConsoleBuffIntroGenLink.make_program_exists.
    destruct_mpe AbsConsoleBuffIntroGenLink.make_program_exists.
    destruct_mpe SerialIntroGenLink.make_program_exists.
    destruct_mpe SerialGenLink.make_program_exists.
    destruct_mpe IoApicGenLink.make_program_exists.
    destruct_mpe LApicGenLink.make_program_exists.
    destruct_mpe ConsoleGenLink.make_program_exists.
    destruct_mpe HandlerIntroGenLink.make_program_exists.
    destruct_mpe HandlerSwGenLink.make_program_exists.
    destruct_mpe HandlerAsmGenLink.make_program_exists.
    destruct_mpe HandlerCxtGenLink.make_program_exists.
    destruct_mpe HandlerOpGenLink.make_program_exists.
    destruct_mpe HandlerGenLink.make_program_exists.
    destruct_mpe AbsHandlerGenLink.make_program_exists.
    destruct_mpe ContainerGenLink.make_program_exists.
    destruct_mpe ALInitGenLink.make_program_exists.
    destruct_mpe ALOpGenLink.make_program_exists.
    destruct_mpe ALGenLink.make_program_exists.
    destruct_mpe PTIntroGenLink.make_program_exists.
    destruct_mpe PTOpGenLink.make_program_exists.
    destruct_mpe PTCommGenLink.make_program_exists.
    destruct_mpe PTKernGenLink.make_program_exists.
    destruct_mpe PTInitGenLink.make_program_exists.
    destruct_mpe PTBitGenLink.make_program_exists.
    destruct_mpe PTNewGenLink.make_program_exists.
    destruct_mpe ShareIntroGenLink.make_program_exists.
    destruct_mpe ShareOpGenLink.make_program_exists.
    destruct_mpe ShareGenLink.make_program_exists.

    destruct_mpe KContextGenLink.make_program_exists.
    destruct_mpe KContextNewGenLink.make_program_exists.
    destruct_mpe ThreadIntroGenLink.make_program_exists.
    destruct_mpe ThreadInitGenLink.make_program_exists.
    destruct_mpe QueueIntroGenLink.make_program_exists.
    destruct_mpe QueueInitGenLink.make_program_exists.
    destruct_mpe AbQueueGenLink.make_program_exists.
    destruct_mpe CurIDGenLink.make_program_exists.
    destruct_mpe ThreadSchedGenLink.make_program_exists.
    destruct_mpe ThreadGenLink.make_program_exists.
    destruct_mpe IPCIntroGenLink.make_program_exists.
    destruct_mpe IPCGenLink.make_program_exists.
    destruct_mpe UCtxtIntroGenLink.make_program_exists.
    destruct_mpe ProcGenLink.make_program_exists.

    destruct_mpe EPTIntroGenLink.make_program_exists.
    destruct_mpe EPTOpGenLink.make_program_exists.
    destruct_mpe EPTInitGenLink.make_program_exists.
    destruct_mpe VMCSIntroGenLink.make_program_exists.
    destruct_mpe VMCSInitGenLink.make_program_exists.
    destruct_mpe VMXIntroGenLink.make_program_exists.
    destruct_mpe VMXInitGenLink.make_program_exists.

    destruct_mpe TrapArgGenLink.make_program_exists.
    destruct_mpe TrapGenLink.make_program_exists.
    destruct_mpe DispatchGenLink.make_program_exists.
    destruct_mpe SysCallGenLink.make_program_exists.

    eapply exists_program_simulation_intro; [ | eassumption].

    compose_backward_simulation SysCallGenLink.cl_backward_simulation.
    compose_backward_simulation DispatchGenLink.cl_backward_simulation.
    compose_backward_simulation TrapGenLink.cl_backward_simulation.
    compose_backward_simulation TrapArgGenLink.cl_backward_simulation.

    compose_backward_simulation VMXInitGenLink.cl_backward_simulation.
    compose_backward_simulation VMXIntroGenLink.cl_backward_simulation.
    compose_backward_simulation VMCSInitGenLink.cl_backward_simulation.
    compose_backward_simulation VMCSIntroGenLink.cl_backward_simulation.
    compose_backward_simulation EPTInitGenLink.cl_backward_simulation.
    compose_backward_simulation EPTOpGenLink.cl_backward_simulation.
    compose_backward_simulation EPTIntroGenLink.cl_backward_simulation.

    compose_backward_simulation ProcGenLink.cl_backward_simulation.
    compose_backward_simulation UCtxtIntroGenLink.cl_backward_simulation.
    compose_backward_simulation IPCGenLink.cl_backward_simulation.
    compose_backward_simulation IPCIntroGenLink.cl_backward_simulation.
    compose_backward_simulation ThreadGenLink.cl_backward_simulation.
    compose_backward_simulation ThreadSchedGenLink.cl_backward_simulation.

    compose_backward_simulation CurIDGenLink.cl_backward_simulation.
    compose_backward_simulation AbQueueGenLink.cl_backward_simulation.
    compose_backward_simulation QueueInitGenLink.cl_backward_simulation.
    compose_backward_simulation QueueIntroGenLink.cl_backward_simulation.
    compose_backward_simulation ThreadInitGenLink.cl_backward_simulation.
    compose_backward_simulation ThreadIntroGenLink.cl_backward_simulation.
    compose_backward_simulation KContextNewGenLink.cl_backward_simulation.
    compose_backward_simulation KContextGenLink.cl_backward_simulation.

    compose_backward_simulation ShareGenLink.cl_backward_simulation.
    compose_backward_simulation ShareOpGenLink.cl_backward_simulation.
    compose_backward_simulation ShareIntroGenLink.cl_backward_simulation.
    compose_backward_simulation PTNewGenLink.cl_backward_simulation.
    compose_backward_simulation PTBitGenLink.cl_backward_simulation.
    compose_backward_simulation PTInitGenLink.cl_backward_simulation.
    compose_backward_simulation PTKernGenLink.cl_backward_simulation.
    compose_backward_simulation PTCommGenLink.cl_backward_simulation.
    compose_backward_simulation PTOpGenLink.cl_backward_simulation.
    compose_backward_simulation PTIntroGenLink.cl_backward_simulation.
    compose_backward_simulation ALGenLink.cl_backward_simulation.
    compose_backward_simulation ALOpGenLink.cl_backward_simulation.
    compose_backward_simulation ALInitGenLink.cl_backward_simulation.
    compose_backward_simulation ContainerGenLink.cl_backward_simulation.

    compose_backward_simulation AbsHandlerGenLink.cl_backward_simulation.
    compose_backward_simulation HandlerGenLink.cl_backward_simulation.
    compose_backward_simulation HandlerOpGenLink.cl_backward_simulation.
    compose_backward_simulation HandlerCxtGenLink.cl_backward_simulation.
    compose_backward_simulation HandlerAsmGenLink.cl_backward_simulation.
    compose_backward_simulation HandlerSwGenLink.cl_backward_simulation.
    compose_backward_simulation HandlerIntroGenLink.cl_backward_simulation.
    compose_backward_simulation ConsoleGenLink.cl_backward_simulation.
    compose_backward_simulation LApicGenLink.cl_backward_simulation.
    compose_backward_simulation IoApicGenLink.cl_backward_simulation.
    compose_backward_simulation SerialGenLink.cl_backward_simulation.
    compose_backward_simulation SerialIntroGenLink.cl_backward_simulation.
    compose_backward_simulation AbsConsoleBuffIntroGenLink.cl_backward_simulation.
    last_backward_simulation ConsoleBuffIntroGenLink.cl_backward_simulation.
  Qed.

  Theorem CertiKOS_correct:
    ∀ (s: stencil) (CTXT: LAsm.module) kernel combined_program user_program
           (builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
      CertiKOS.certikos = OK kernel →
      make_program s (CTXT ⊕ kernel) (MBoot.mboot ⊕ L64) = OK combined_program →
      make_program s CTXT (TSysCall.tsyscall ⊕ L64) = OK user_program →
      inhabited
        (backward_simulation
           (LAsm.semantics (lcfg_ops := LC (TSysCall.tsyscall ⊕ L64)) user_program)
           (LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)) combined_program)).
  Proof.
    intros s CTXT kernel combined_program user_program ? Hkernel Hcp Hup.
    edestruct (CertiKOS_plus_context CTXT) as (comb & Hcomb & Heqv); [ eassumption | ].
    eapply make_program_equiv in Hcp; [ | eassumption].
    edestruct CertiKOS_correct´; try eassumption.
    constructor.
    setoid_rewrite H in Hup.
    congruence.
  Qed.

End CertiKOSCorrect.