Library mcertikos.trap.TTrapCode

Require Import TacticsForTesting.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Clight.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Ctypes.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import DispatchGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import XOmega.
Require Import TTrapCSource.
Require Import AbstractDataType.
Require Import ObjArg.
Require Import ObjTrap.
Require Import ObjSyncIPC.
Require Export TrapPrimSemantics.
Require Import CommonTactic.

Require Import TTrapCodeLemma1.
Require Import TTrapCodeLemma2.
Require Import TTrapCodeLemma3.
Require Import TTrapCodeLemma4.
Require Import TTrapCodeLemma5.
Require Import TTrapCodeLemma6.
Require Import TTrapCodeLemma7.
Require Import TTrapCodeLemma8.
Require Import TTrapCodeLemma9.
Require Import TTrapCodeLemma10.
Require Import TTrapCodeLemma11.
Require Import TTrapCodeLemma12.
Require Import TTrapCodeLemma13.
Require Import TTrapCodeLemma14.
Require Import TTrapCodeLemma15.
Require Import TTrapCodeLemma16.
Require Import TTrapCodeLemma17.
Require Import TTrapCodeLemma18.
Require Import TTrapCodeLemma19.
Require Import TTrapCodeLemma20.
Require Import TTrapCodeLemma21.
Require Import TTrapCodeLemma22.
Require Import TTrapCodeLemma23.
Require Import TTrapCodeLemma24.
Require Import TTrapCodeLemma25.
Require Import TTrapCodeLemma26.
Require Import TTrapCodeLemma27.
Require Import TTrapCodeLemma28.
Require Import TTrapCodeLemma29.

Require Import ObjTMINTELVIRT.
Require Import ObjTMIPCDEVPRIM.
Require Import ObjTMVMM.
Require Import ObjTMSCHED.
Require Import GlobalOracleProp.
Require Import SingleOracle.

Module TTRAPCODE.

  Section WithPrimitives.

    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.

    Context `{single_oracle_prop: SingleOracleProp}.
    Context `{real_params : RealParams}.
    Context `{multi_oracle_prop: MultiOracleProp}.

    Let mem := mwd (cdata RData).

    Context `{Hstencil: Stencil}.
    Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
    Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.

    Section SYSCALLDISPATCHC.

      Let L: compatlayer (cdata RData) := sys_proc_create ↦ trap_proccreate_compatsem trap_proc_create_spec
                                                           ⊕ sys_get_quota ↦ gensem trap_get_quota_spec
                                                           ⊕ sys_inject_event ↦ gensem trap_inject_event_spec
                                                           ⊕ sys_check_int_shadow ↦ gensem trap_check_int_shadow_spec
                                                           ⊕ sys_check_pending_event ↦ gensem trap_check_pending_event_spec
                                                           ⊕ sys_intercept_int_window ↦ gensem trap_intercept_int_window_spec
                                                           ⊕ sys_get_next_eip ↦ gensem trap_get_next_eip_spec
                                                           ⊕ sys_get_reg ↦ gensem trap_get_reg_spec
                                                           ⊕ sys_set_reg ↦ gensem trap_set_reg_spec
                                                           ⊕ sys_set_seg1 ↦ gensem trap_set_seg1_spec
                                                           ⊕ sys_set_seg2 ↦ gensem trap_set_seg2_spec
                                                           ⊕ sys_get_tsc_offset ↦ gensem trap_get_tsc_offset_spec
                                                           ⊕ sys_set_tsc_offset ↦ gensem trap_set_tsc_offset_spec
                                                           ⊕ sys_get_exitinfo ↦ gensem trap_get_exitinfo_spec
                                                           ⊕ sys_handle_rdmsr ↦ gensem trap_handle_rdmsr_spec
                                                           ⊕ sys_handle_wrmsr ↦ gensem trap_handle_wrmsr_spec
                                                           ⊕ sys_mmap ↦ gensem trap_mmap_spec
                                                           ⊕ sys_receive_chan ↦ gensem trap_receivechan_spec
                                                           ⊕ sys_sendto_chan ↦ gensem trap_sendtochan_spec
                                                           ⊕ thread_yield ↦ gensem big2_thread_yield_spec
                                                           ⊕ sys_getc ↦ gensem sys_getc_spec
                                                           ⊕ sys_putc ↦ gensem sys_putc_spec
                                                           ⊕ uctx_arg1 ↦ gensem uctx_arg1_spec
                                                           ⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec.

      Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.

      Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

      Section SyscallDispatchCBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

        Variables (ge: genv)
                  (STENCIL_MATCHES: stencil_matches sc ge).

        Variable bsys_proc_create: block.

        Hypothesis hsys_proc_create1 : Genv.find_symbol ge sys_proc_create = Some bsys_proc_create.

        Hypothesis hsys_proc_create2 : Genv.find_funct_ptr ge bsys_proc_create = Some (External (EF_external sys_proc_create (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_quota: block.

        Hypothesis hsys_get_quota1 : Genv.find_symbol ge sys_get_quota = Some bsys_get_quota.

        Hypothesis hsys_get_quota2 : Genv.find_funct_ptr ge bsys_get_quota = Some (External (EF_external sys_get_quota (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_inject_event: block.

        Hypothesis hsys_inject_event1 : Genv.find_symbol ge sys_inject_event = Some bsys_inject_event.

        Hypothesis hsys_inject_event2 : Genv.find_funct_ptr ge bsys_inject_event = Some (External (EF_external sys_inject_event (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_check_int_shadow: block.

        Hypothesis hsys_check_int_shadow1 : Genv.find_symbol ge sys_check_int_shadow = Some bsys_check_int_shadow.

        Hypothesis hsys_check_int_shadow2 : Genv.find_funct_ptr ge bsys_check_int_shadow = Some (External (EF_external sys_check_int_shadow (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_check_pending_event: block.

        Hypothesis hsys_check_pending_event1 : Genv.find_symbol ge sys_check_pending_event = Some bsys_check_pending_event.

        Hypothesis hsys_check_pending_event2 : Genv.find_funct_ptr ge bsys_check_pending_event = Some (External (EF_external sys_check_pending_event (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_intercept_int_window: block.

        Hypothesis hsys_intercept_int_window1 : Genv.find_symbol ge sys_intercept_int_window = Some bsys_intercept_int_window.

        Hypothesis hsys_intercept_int_window2 : Genv.find_funct_ptr ge bsys_intercept_int_window = Some (External (EF_external sys_intercept_int_window (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_next_eip: block.

        Hypothesis hsys_get_next_eip1 : Genv.find_symbol ge sys_get_next_eip = Some bsys_get_next_eip.

        Hypothesis hsys_get_next_eip2 : Genv.find_funct_ptr ge bsys_get_next_eip = Some (External (EF_external sys_get_next_eip (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_reg: block.

        Hypothesis hsys_get_reg1 : Genv.find_symbol ge sys_get_reg = Some bsys_get_reg.

        Hypothesis hsys_get_reg2 : Genv.find_funct_ptr ge bsys_get_reg = Some (External (EF_external sys_get_reg (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_set_reg: block.

        Hypothesis hsys_set_reg1 : Genv.find_symbol ge sys_set_reg = Some bsys_set_reg.

        Hypothesis hsys_set_reg2 : Genv.find_funct_ptr ge bsys_set_reg = Some (External (EF_external sys_set_reg (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_set_seg1: block.

        Hypothesis hsys_set_seg11 : Genv.find_symbol ge sys_set_seg1 = Some bsys_set_seg1.

        Hypothesis hsys_set_seg12 : Genv.find_funct_ptr ge bsys_set_seg1 = Some (External (EF_external sys_set_seg1 (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_set_seg2: block.

        Hypothesis hsys_set_seg21 : Genv.find_symbol ge sys_set_seg2 = Some bsys_set_seg2.

        Hypothesis hsys_set_seg22 : Genv.find_funct_ptr ge bsys_set_seg2 = Some (External (EF_external sys_set_seg2 (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_tsc_offset: block.

        Hypothesis hsys_get_tsc_offset1 : Genv.find_symbol ge sys_get_tsc_offset = Some bsys_get_tsc_offset.

        Hypothesis hsys_get_tsc_offset2 : Genv.find_funct_ptr ge bsys_get_tsc_offset = Some (External (EF_external sys_get_tsc_offset (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_set_tsc_offset: block.

        Hypothesis hsys_set_tsc_offset1 : Genv.find_symbol ge sys_set_tsc_offset = Some bsys_set_tsc_offset.

        Hypothesis hsys_set_tsc_offset2 : Genv.find_funct_ptr ge bsys_set_tsc_offset = Some (External (EF_external sys_set_tsc_offset (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_exitinfo: block.

        Hypothesis hsys_get_exitinfo1 : Genv.find_symbol ge sys_get_exitinfo = Some bsys_get_exitinfo.

        Hypothesis hsys_get_exitinfo2 : Genv.find_funct_ptr ge bsys_get_exitinfo = Some (External (EF_external sys_get_exitinfo (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_handle_rdmsr: block.

        Hypothesis hsys_handle_rdmsr1 : Genv.find_symbol ge sys_handle_rdmsr = Some bsys_handle_rdmsr.

        Hypothesis hsys_handle_rdmsr2 : Genv.find_funct_ptr ge bsys_handle_rdmsr = Some (External (EF_external sys_handle_rdmsr (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_handle_wrmsr: block.

        Hypothesis hsys_handle_wrmsr1 : Genv.find_symbol ge sys_handle_wrmsr = Some bsys_handle_wrmsr.

        Hypothesis hsys_handle_wrmsr2 : Genv.find_funct_ptr ge bsys_handle_wrmsr = Some (External (EF_external sys_handle_wrmsr (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_mmap: block.

        Hypothesis hsys_mmap1 : Genv.find_symbol ge sys_mmap = Some bsys_mmap.

        Hypothesis hsys_mmap2 : Genv.find_funct_ptr ge bsys_mmap = Some (External (EF_external sys_mmap (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_receive_chan: block.

        Hypothesis hsys_receive_chan1 : Genv.find_symbol ge sys_receive_chan = Some bsys_receive_chan.

        Hypothesis hsys_receive_chan2 : Genv.find_funct_ptr ge bsys_receive_chan = Some (External (EF_external sys_receive_chan (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_sendto_chan: block.

        Hypothesis hsys_sendto_chan1 : Genv.find_symbol ge sys_sendto_chan = Some bsys_sendto_chan.

        Hypothesis hsys_sendto_chan2 : Genv.find_funct_ptr ge bsys_sendto_chan = Some (External (EF_external sys_sendto_chan (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bthread_yield: block.

        Hypothesis hthread_yield1 : Genv.find_symbol ge thread_yield = Some bthread_yield.

        Hypothesis hthread_yield2 : Genv.find_funct_ptr ge bthread_yield = Some (External (EF_external thread_yield (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_getc: block.

        Hypothesis hsys_getc1 : Genv.find_symbol ge sys_getc = Some bsys_getc.

        Hypothesis hsys_getc2 : Genv.find_funct_ptr ge bsys_getc = Some (External (EF_external sys_getc (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_putc: block.

        Hypothesis hsys_putc1 : Genv.find_symbol ge sys_putc = Some bsys_putc.

        Hypothesis hsys_putc2 : Genv.find_funct_ptr ge bsys_putc = Some (External (EF_external sys_putc (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable buctx_arg1: block.

        Hypothesis huctx_arg11 : Genv.find_symbol ge uctx_arg1 = Some buctx_arg1.

        Hypothesis huctx_arg12 : Genv.find_funct_ptr ge buctx_arg1 = Some (External (EF_external uctx_arg1 (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_set_errno: block.

        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.

        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno = Some (External (EF_external uctx_set_errno (signature_of_type (Tcons tint Tnil) tvoid cc_default)) (Tcons tint Tnil) tvoid cc_default).

        Lemma syscall_dispatch_c_body_correct: ∀ m d d´ env le,
                                        env = PTree.empty _ →
                                        sys_dispatch_c_spec sc m d = Some d´ →
                                        high_level_invariant d →
                                        ∃ le´,
                                          exec_stmt ge env le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          subst.
          unfold sys_dispatch_c_spec in H0.
          case_eq (uctx_arg1_spec d); intros; rewrite H in H0; try discriminate H0.
          case_eq (zle_le 0 z Int.max_unsigned); intros; rewrite H2 in H0; try discriminate H0.
          case_eq (Syscall_Z2Num z); intros; rewrite H3 in H0.
          eapply TTrapCodeLemma2.TTRAPCODE.NSYS_PUTS_correct; eauto.
          eapply TTrapCodeLemma3.TTRAPCODE.NSYS_RING0_SPAWN_correct; eauto.
          eapply TTrapCodeLemma4.TTRAPCODE.NSYS_SPAWN_correct; eauto.
          eapply TTrapCodeLemma5.TTRAPCODE.NSYS_YIELD_correct; eauto.
          eapply TTrapCodeLemma6.TTRAPCODE.NSYS_DISK_OP_correct; eauto.
          eapply TTrapCodeLemma7.TTRAPCODE.NSYS_DISK_CAP_correct; eauto.
          eapply TTrapCodeLemma28.TTRAPCODE.NSYS_GET_TSC_PER_MS_correct; eauto.
          eapply TTrapCodeLemma13.TTRAPCODE.NSYS_GET_TSC_OFFSET_correct; eauto.
          eapply TTrapCodeLemma14.TTRAPCODE.NSYS_SET_TSC_OFFSET_correct; eauto.
          eapply TTrapCodeLemma15.TTRAPCODE.NSYS_RUN_VM_correct; eauto.
          eapply TTrapCodeLemma16.TTRAPCODE.NSYS_GET_EXITINFO_correct; eauto.
          eapply TTrapCodeLemma17.TTRAPCODE.NSYS_MMAP_correct; eauto.
          eapply TTrapCodeLemma18.TTRAPCODE.NSYS_SET_REG_correct; eauto.
          eapply TTrapCodeLemma19.TTRAPCODE.NSYS_GET_REG_correct; eauto.
          eapply TTrapCodeLemma20.TTRAPCODE.NSYS_SET_SEG1_correct; eauto.
          eapply TTrapCodeLemma29.TTRAPCODE.NSYS_SET_SEG2_correct; eauto.
          eapply TTrapCodeLemma21.TTRAPCODE.NSYS_GET_NEXT_EIP_correct; eauto.
          eapply TTrapCodeLemma22.TTRAPCODE.NSYS_INJECT_EVENT_correct; eauto.
          eapply TTrapCodeLemma23.TTRAPCODE.NSYS_CHECK_PENDING_EVENT_correct; eauto.
          eapply TTrapCodeLemma24.TTRAPCODE.NSYS_CHECK_INT_SHADOW_correct; eauto.
          eapply TTrapCodeLemma25.TTRAPCODE.NSYS_INTERCEPT_INT_WINDOW_correct; eauto.
          eapply TTrapCodeLemma26.TTRAPCODE.NSYS_HANDLE_RDMSR_correct; eauto.
          eapply TTrapCodeLemma27.TTRAPCODE.NSYS_HANDLE_WRMSR_correct; eauto.
          eapply TTrapCodeLemma8.TTRAPCODE.NSYS_GET_QUOTA_correct; eauto.
          eapply TTrapCodeLemma9.TTRAPCODE.NSYS_RECV_correct; eauto.
          eapply TTrapCodeLemma10.TTRAPCODE.NSYS_SENDTO_correct; eauto.
          eapply TTrapCodeLemma12.TTRAPCODE.NSYS_GETC_correct; eauto.
          eapply TTrapCodeLemma11.TTRAPCODE.NSYS_PUTC_correct; eauto.
          eapply TTrapCodeLemma1.TTRAPCODE.NSYS_NR_correct; eauto.
        Qed.

      End SyscallDispatchCBody.

      Theorem syscall_dispatch_c_code_correct:
        spec_le (syscall_dispatch_C ↦ sys_dispatch_c_spec_low) (〚syscall_dispatch_C ↦ f_syscall_dispatch_c 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (syscall_dispatch_c_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp b4 Hb4fs Hb4fp b5 Hb5fs Hb5fp b6 Hb6fs Hb6fp b7 Hb7fs Hb7fp b8 Hb8fs Hb8fp b9 Hb9fs Hb9fp b10 Hb10fs Hb10fp b11 Hb11fs Hb11fp
        b12 Hb12fs Hb12fp b13 Hb13fs Hb13fp b14 Hb14fs Hb14fp b15 Hb15fs Hb15fp
        b16 Hb16fs Hb16fp b17 Hb17fs Hb17fp b18 Hb18fs Hb18fp
        b19 Hb19fs Hb19fp b20 Hb20fs Hb20fp b21 Hb21fs Hb21fp b22 Hb22fs Hb22fp b23 Hb23fs Hb23fp m´0 labd labd0 (PTree.empty _)
                                        (bind_parameter_temps´ (fn_params f_syscall_dispatch_c)
                                                               nil
                                                               (create_undef_temps (fn_temps f_syscall_dispatch_c)))) H0.
      Qed.

    End SYSCALLDISPATCHC.


  End WithPrimitives.

End TTRAPCODE.