Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import PrimTMSemantics.
Require Import LAsm.
Require Import XOmega.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.

Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import INVLemmaProc.

Require Import AbstractDataType.

Require Import LoadStoreSem3high.
Require Export TTrapArg.
Require Export ObjTrap.
Require Export TrapPrimSemantics.

Require Import IntelPrimSemantics.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Section WITHMEM.

  Local Open Scope Z_scope.

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

  Context `{Hstencil: Stencil}.
  Context `{Hmem: Mem.MemoryModelX}.
  Context `{Hmwd: UseMemWithData mem}.

  Section Prim.

    Global Instance sys_putc_inv: PreservesInvariants sys_putc_spec.
    Proof.
      Opaque ObjInterruptManagement.serial_intr_disable_aux.
      constructor; simpl; intros; inv_generic_sem H; inversion H0.
      - functional inversion H2; subst.
        eapply uctx_set_errno_low_inv; try eassumption.
        generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_low_level_invariant _ _ d2 _ d3); eauto.
        econstructor.
        eassumption.
        generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_low_level_invariant0 _ _ d1); eauto.
        econstructor.
        econstructor.
        instantiate (1:= Int.repr c).
        rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
        eassumption.
        generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
        eapply semprops_low_level_invariant1; eauto.
        econstructor.
        eassumption.
      - functional inversion H2; subst.
        eapply uctx_set_errno_high_inv; try eassumption.
        generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_high_level_invariant _ d2 _ d3); eauto.
        econstructor.
        eassumption.
        generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_high_level_invariant0 _ d1); eauto.
        econstructor.
        econstructor.
        instantiate (1:= Int.repr c).
        rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
        eassumption.
        generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
        eapply semprops_high_level_invariant1; eauto.
        econstructor.
        eassumption.
      - functional inversion H2; subst.
        eapply uctx_set_errno_kernel_mode; try eassumption.
        generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_kernel_mode _ d2 _ d3); eauto.
        econstructor.
        eassumption.
        generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_kernel_mode0 _ d1); eauto.
        econstructor.
        econstructor.
        instantiate (1:= Int.repr c).
        rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
        eassumption.
        generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
        eapply semprops_kernel_mode1; eauto.
        econstructor.
        eassumption.
    Qed.


    Global Instance sys_getc_inv: PreservesInvariants sys_getc_spec.
    Proof.
      constructor; simpl; intros; inv_generic_sem H; inversion H0.
      - functional inversion H2; subst.
        eapply uctx_set_errno_low_inv; try eassumption.
        eapply uctx_set_retval1_low_inv; try eassumption.
        generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_low_level_invariant _ _ d2 _ d3); eauto.
        econstructor.
        eassumption.
        generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_low_level_invariant0 _ _ d1); eauto.
        econstructor.
        instantiate (1:= Int.repr x).
        rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
        eassumption.
        generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
        eapply semprops_low_level_invariant1; eauto.
        econstructor.
        eassumption.
      - functional inversion H2; subst.
        eapply uctx_set_errno_high_inv; try eassumption.
        eapply uctx_set_retval1_high_inv; try eassumption.
        generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_high_level_invariant _ d2 _ d3); eauto.
        econstructor.
        eassumption.
        generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_high_level_invariant0 _ d1); eauto.
        econstructor.
        instantiate (1:= Int.repr x).
        rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
        eassumption.
        generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
        eapply semprops_high_level_invariant1; eauto.
        econstructor.
        eassumption.
      - functional inversion H2; subst.
        eapply uctx_set_errno_kernel_mode; try eassumption.
        eapply uctx_set_retval1_kernel_mode; try eassumption.
        generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_kernel_mode _ d2 _ d3); eauto.
        econstructor.
        eassumption.
        generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
        eapply (semprops_kernel_mode0 _ d1); eauto.
        econstructor.
        instantiate (1:= Int.repr x).
        rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
        eassumption.
        generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
        eapply semprops_kernel_mode1; eauto.
        econstructor.
        eassumption.
    Qed.

    Section TRAP_GET_QUOTA.

      Lemma trap_get_quota_high_inv:
        ∀ d d´,
          trap_get_quota_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H.
        eapply uctx_set_errno_high_inv; try eassumption.
        eapply uctx_set_retval1_high_inv; eassumption.
      Qed.

      Lemma trap_get_quota_low_inv:
        ∀ d d´ n,
          trap_get_quota_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H.
        eapply uctx_set_errno_low_inv; try eassumption.
        eapply uctx_set_retval1_low_inv; eassumption.
      Qed.

      Lemma trap_get_quota_kernel_mode:
        ∀ d d´,
          trap_get_quota_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H.
        eapply uctx_set_errno_kernel_mode; try eassumption.
        eapply uctx_set_retval1_kernel_mode; eassumption.
      Qed.

      Global Instance trap_get_quota_inv: PreservesInvariants trap_get_quota_spec.
      Proof.
        preserves_invariants_simpl´;
          [ eapply trap_get_quota_low_inv
          | eapply trap_get_quota_high_inv
          | eapply trap_get_quota_kernel_mode ];
          eassumption.
      Qed.

    End TRAP_GET_QUOTA.

    Section TRAP_HANDLE_RDMSR.

      Lemma trap_handle_rdmsr_high_inv:
        ∀ d d´,
          trap_handle_rdmsr_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply thread_vmx_set_reg_high_inv; eauto.
        eapply thread_vmx_set_reg_high_inv; eauto.
        eapply thread_vmx_set_reg_high_inv; eauto.
      Qed.

      Lemma trap_handle_rdmsr_low_inv:
        ∀ d d´ n,
          trap_handle_rdmsr_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply thread_vmx_set_reg_low_inv; eauto.
        eapply thread_vmx_set_reg_low_inv; eauto.
        eapply thread_vmx_set_reg_low_inv; eauto.
      Qed.

      Lemma trap_handle_rdmsr_kernel_mode:
        ∀ d d´,
          trap_handle_rdmsr_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply thread_vmx_set_reg_kernel_mode; eauto.
        eapply thread_vmx_set_reg_kernel_mode; eauto.
        eapply thread_vmx_set_reg_kernel_mode; eauto.
      Qed.

      Global Instance trap_handle_rdmsr_inv: PreservesInvariants trap_handle_rdmsr_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_handle_rdmsr_low_inv; eauto.
        - eapply trap_handle_rdmsr_high_inv; eauto.
        - eapply trap_handle_rdmsr_kernel_mode; eauto.
      Qed.

    End TRAP_HANDLE_RDMSR.

    Section TRAP_HANDLE_WRMSR.

      Lemma trap_handle_wrmsr_high_inv:
        ∀ d d´,
          trap_handle_wrmsr_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply thread_vmx_set_reg_high_inv; eauto.
      Qed.

      Lemma trap_handle_wrmsr_low_inv:
        ∀ d d´ n,
          trap_handle_wrmsr_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply thread_vmx_set_reg_low_inv; eauto.
      Qed.

      Lemma trap_handle_wrmsr_kernel_mode:
        ∀ d d´,
          trap_handle_wrmsr_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply thread_vmx_set_reg_kernel_mode; eauto.
      Qed.

      Global Instance trap_handle_wrmsr_inv: PreservesInvariants trap_handle_wrmsr_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_handle_wrmsr_low_inv; eauto.
        - eapply trap_handle_wrmsr_high_inv; eauto.
        - eapply trap_handle_wrmsr_kernel_mode; eauto.
      Qed.

    End TRAP_HANDLE_WRMSR.


    Section TRAP_CHAN_RECEIVE.

      Lemma trap_receivechan_high_inv:
        ∀ d d´,
          trap_receivechan_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
        exploit syncreceive_chan_high_level_inv; eauto.
      Qed.

      Lemma trap_receivechan_low_inv:
        ∀ d d´ n,
          trap_receivechan_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
        exploit syncreceive_chan_low_level_inv; eauto.
      Qed.

      Lemma trap_receivechan_kernel_mode:
        ∀ d d´,
          trap_receivechan_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst.
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
        exploit syncreceive_chan_kernel_mode; eauto.
      Qed.

      Global Instance trap_receivechan_inv: PreservesInvariants trap_receivechan_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_receivechan_low_inv; eauto.
        - eapply trap_receivechan_high_inv; eauto.
        - eapply trap_receivechan_kernel_mode; eauto.
      Qed.

    End TRAP_CHAN_RECEIVE.

    Section TRAP_CHAN_SENDTO.

      Lemma trap_sendtochan_high_inv:
        ∀ d d´,
          trap_sendtochan_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
        exploit syncsendto_chan_high_level_inv; eauto.
      Qed.

      Lemma trap_sendtochan_low_inv:
        ∀ d d´ n,
          trap_sendtochan_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
        exploit syncsendto_chan_low_level_inv; eauto.
      Qed.

      Lemma trap_sendtochan_kernel_mode:
        ∀ d d´,
          trap_sendtochan_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst.
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
        exploit syncsendto_chan_kernel_mode; eauto.
      Qed.

      Global Instance trap_sendtochan_inv: PreservesInvariants trap_sendtochan_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_sendtochan_low_inv; eauto.
        - eapply trap_sendtochan_high_inv; eauto.
        - eapply trap_sendtochan_kernel_mode; eauto.
      Qed.

    End TRAP_CHAN_SENDTO.

    Section TRAP_INTERCEPT_INT_WINDOW.

      Lemma trap_intercept_int_window_high_inv:
        ∀ d d´,
          trap_intercept_int_window_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_high_inv; eauto.
        eapply thread_vmx_set_intercept_intwin_high_inv; eauto.
      Qed.

      Lemma trap_intercept_int_window_low_inv:
        ∀ d d´ n,
          trap_intercept_int_window_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_low_inv; eauto.
        eapply thread_vmx_set_intercept_intwin_low_inv; eauto.
      Qed.

      Lemma trap_intercept_int_window_kernel_mode:
        ∀ d d´,
          trap_intercept_int_window_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst.
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply thread_vmx_set_intercept_intwin_kernel_mode; eauto.
      Qed.

      Global Instance trap_intercept_int_window_inv: PreservesInvariants trap_intercept_int_window_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_intercept_int_window_low_inv; eauto.
        - eapply trap_intercept_int_window_high_inv; eauto.
        - eapply trap_intercept_int_window_kernel_mode; eauto.
      Qed.

    End TRAP_INTERCEPT_INT_WINDOW.

    Section TRAP_CHECK_PENDING_EVENT.

      Lemma trap_check_pending_event_high_inv:
        ∀ d d´,
          trap_check_pending_event_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
      Qed.

      Lemma trap_check_pending_event_low_inv:
        ∀ d d´ n,
          trap_check_pending_event_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
      Qed.

      Lemma trap_check_pending_event_kernel_mode:
        ∀ d d´,
          trap_check_pending_event_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst.
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
      Qed.

      Global Instance trap_check_pending_event_inv: PreservesInvariants trap_check_pending_event_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_check_pending_event_low_inv; eauto.
        - eapply trap_check_pending_event_high_inv; eauto.
        - eapply trap_check_pending_event_kernel_mode; eauto.
      Qed.

    End TRAP_CHECK_PENDING_EVENT.

    Section TRAP_CHECK_INT_SHADOW.

      Lemma trap_check_int_shadow_high_inv:
        ∀ d d´,
          trap_check_int_shadow_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
      Qed.

      Lemma trap_check_int_shadow_low_inv:
        ∀ d d´ n,
          trap_check_int_shadow_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
      Qed.

      Lemma trap_check_int_shadow_kernel_mode:
        ∀ d d´,
          trap_check_int_shadow_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst.
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
      Qed.

      Global Instance trap_check_int_shadow_inv: PreservesInvariants trap_check_int_shadow_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_check_int_shadow_low_inv; eauto.
        - eapply trap_check_int_shadow_high_inv; eauto.
        - eapply trap_check_int_shadow_kernel_mode; eauto.
      Qed.

    End TRAP_CHECK_INT_SHADOW.

    Section TRAP_INJECT_EVENT.

      Lemma trap_inject_event_high_inv:
        ∀ d d´,
          trap_inject_event_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply thread_vmx_inject_event_high_inv; eauto.
      Qed.

      Lemma trap_inject_event_low_inv:
        ∀ d d´ n,
          trap_inject_event_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply thread_vmx_inject_event_low_inv; eauto.
      Qed.

      Lemma trap_inject_event_kernel_mode:
        ∀ d d´,
          trap_inject_event_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply thread_vmx_inject_event_kernel_mode; eauto.
      Qed.

      Global Instance trap_inject_event_inv: PreservesInvariants trap_inject_event_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_inject_event_low_inv; eauto.
        - eapply trap_inject_event_high_inv; eauto.
        - eapply trap_inject_event_kernel_mode; eauto.
      Qed.

    End TRAP_INJECT_EVENT.

    Section TRAP_GET_NEXT_EIP.

      Lemma trap_get_next_eip_high_inv:
        ∀ d d´,
          trap_get_next_eip_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
      Qed.

      Lemma trap_get_next_eip_low_inv:
        ∀ d d´ n,
          trap_get_next_eip_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
      Qed.

      Lemma trap_get_next_eip_kernel_mode:
        ∀ d d´,
          trap_get_next_eip_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst.
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
      Qed.

      Global Instance trap_get_next_eip_inv: PreservesInvariants trap_get_next_eip_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_get_next_eip_low_inv; eauto.
        - eapply trap_get_next_eip_high_inv; eauto.
        - eapply trap_get_next_eip_kernel_mode; eauto.
      Qed.

    End TRAP_GET_NEXT_EIP.

    Section TRAP_GET_REG.

      Lemma trap_get_reg_high_inv:
        ∀ d d´,
          trap_get_reg_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
      Qed.

      Lemma trap_get_reg_low_inv:
        ∀ d d´ n,
          trap_get_reg_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
      Qed.

      Lemma trap_get_reg_kernel_mode:
        ∀ d d´,
          trap_get_reg_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
      Qed.

      Global Instance trap_get_reg_inv: PreservesInvariants trap_get_reg_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_get_reg_low_inv; eauto.
        - eapply trap_get_reg_high_inv; eauto.
        - eapply trap_get_reg_kernel_mode; eauto.
      Qed.

    End TRAP_GET_REG.

    Section TRAP_SET_REG.

      Lemma trap_set_reg_high_inv:
        ∀ d d´,
          trap_set_reg_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply thread_vmx_set_reg_high_inv; eauto.
      Qed.

      Lemma trap_set_reg_low_inv:
        ∀ d d´ n,
          trap_set_reg_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply thread_vmx_set_reg_low_inv; eauto.
      Qed.

      Lemma trap_set_reg_kernel_mode:
        ∀ d d´,
          trap_set_reg_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply thread_vmx_set_reg_kernel_mode; eauto.
      Qed.

      Global Instance trap_set_reg_inv: PreservesInvariants trap_set_reg_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_set_reg_low_inv; eauto.
        - eapply trap_set_reg_high_inv; eauto.
        - eapply trap_set_reg_kernel_mode; eauto.
      Qed.

    End TRAP_SET_REG.

    Section TRAP_SET_SEG1.

      Lemma trap_set_seg1_high_inv:
        ∀ d d´,
          trap_set_seg1_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply thread_vmx_set_desc1_high_inv; eauto.
      Qed.

      Lemma trap_set_seg1_low_inv:
        ∀ d d´ n,
          trap_set_seg1_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply thread_vmx_set_desc1_low_inv; eauto.
      Qed.

      Lemma trap_set_seg1_kernel_mode:
        ∀ d d´,
          trap_set_seg1_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply thread_vmx_set_desc1_kernel_mode; eauto.
      Qed.

      Global Instance trap_set_seg1_inv: PreservesInvariants trap_set_seg1_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_set_seg1_low_inv; eauto.
        - eapply trap_set_seg1_high_inv; eauto.
        - eapply trap_set_seg1_kernel_mode; eauto.
      Qed.

    End TRAP_SET_SEG1.

    Section TRAP_SET_SEG2.

      Lemma trap_set_seg2_high_inv:
        ∀ d d´,
          trap_set_seg2_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply thread_vmx_set_desc2_high_inv; eauto.
      Qed.

      Lemma trap_set_seg2_low_inv:
        ∀ d d´ n,
          trap_set_seg2_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply thread_vmx_set_desc2_low_inv; eauto.
      Qed.

      Lemma trap_set_seg2_kernel_mode:
        ∀ d d´,
          trap_set_seg2_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply thread_vmx_set_desc2_kernel_mode; eauto.
      Qed.

      Global Instance trap_set_seg2_inv: PreservesInvariants trap_set_seg2_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_set_seg2_low_inv; eauto.
        - eapply trap_set_seg2_high_inv; eauto.
        - eapply trap_set_seg2_kernel_mode; eauto.
      Qed.

    End TRAP_SET_SEG2.

    Section TRAP_GET_TSC_OFFSET.

      Lemma trap_get_tsc_offset_high_inv:
        ∀ d d´,
          trap_get_tsc_offset_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval2_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
      Qed.

      Lemma trap_get_tsc_offset_low_inv:
        ∀ d d´ n,
          trap_get_tsc_offset_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval2_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
      Qed.

      Lemma trap_get_tsc_offset_kernel_mode:
        ∀ d d´,
          trap_get_tsc_offset_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval2_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
      Qed.

      Global Instance trap_get_tsc_offset_inv: PreservesInvariants trap_get_tsc_offset_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_get_tsc_offset_low_inv; eauto.
        - eapply trap_get_tsc_offset_high_inv; eauto.
        - eapply trap_get_tsc_offset_kernel_mode; eauto.
      Qed.

    End TRAP_GET_TSC_OFFSET.

    Section TRAP_SET_TSC_OFFSET.

      Lemma trap_set_tsc_offset_high_inv:
        ∀ d d´,
          trap_set_tsc_offset_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        eapply thread_vmx_set_tsc_offset_high_inv; eauto.
      Qed.

      Lemma trap_set_tsc_offset_low_inv:
        ∀ d d´ n,
          trap_set_tsc_offset_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        eapply thread_vmx_set_tsc_offset_low_inv; eauto.
      Qed.

      Lemma trap_set_tsc_offset_kernel_mode:
        ∀ d d´,
          trap_set_tsc_offset_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply thread_vmx_set_tsc_offset_kernel_mode; eauto.
      Qed.

      Global Instance trap_set_tsc_offset_inv: PreservesInvariants trap_set_tsc_offset_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_set_tsc_offset_low_inv; eauto.
        - eapply trap_set_tsc_offset_high_inv; eauto.
        - eapply trap_set_tsc_offset_kernel_mode; eauto.
      Qed.

    End TRAP_SET_TSC_OFFSET.

    Section TRAP_GET_EXITINFO.

      Lemma trap_get_exitinfo_high_inv:
        ∀ d d´,
          trap_get_exitinfo_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto.
        - eapply uctx_set_retval3_high_inv; eauto.
          eapply uctx_set_retval2_high_inv; eauto.
          eapply uctx_set_retval1_high_inv; eauto.
        - eapply uctx_set_retval2_high_inv; eauto.
          eapply uctx_set_retval1_high_inv; eauto.
        - eapply uctx_set_retval2_high_inv; eauto.
          eapply uctx_set_retval1_high_inv; eauto.
        - eapply uctx_set_retval1_high_inv; eauto.
      Qed.

      Lemma trap_get_exitinfo_low_inv:
        ∀ d d´ n,
          trap_get_exitinfo_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto.
        - eapply uctx_set_retval3_low_inv; eauto.
          eapply uctx_set_retval2_low_inv; eauto.
          eapply uctx_set_retval1_low_inv; eauto.
        - eapply uctx_set_retval2_low_inv; eauto.
          eapply uctx_set_retval1_low_inv; eauto.
        - eapply uctx_set_retval2_low_inv; eauto.
          eapply uctx_set_retval1_low_inv; eauto.
        - eapply uctx_set_retval1_low_inv; eauto.
      Qed.

      Lemma trap_get_exitinfo_kernel_mode:
        ∀ d d´,
          trap_get_exitinfo_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto.
        - eapply uctx_set_retval3_kernel_mode; eauto.
          eapply uctx_set_retval2_kernel_mode; eauto.
          eapply uctx_set_retval1_kernel_mode; eauto.
        - eapply uctx_set_retval2_kernel_mode; eauto.
          eapply uctx_set_retval1_kernel_mode; eauto.
        - eapply uctx_set_retval2_kernel_mode; eauto.
          eapply uctx_set_retval1_kernel_mode; eauto.
        - eapply uctx_set_retval1_kernel_mode; eauto.
      Qed.

      Global Instance trap_get_exitinfo_inv: PreservesInvariants trap_get_exitinfo_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_get_exitinfo_low_inv; eauto.
        - eapply trap_get_exitinfo_high_inv; eauto.
        - eapply trap_get_exitinfo_kernel_mode; eauto.
      Qed.

    End TRAP_GET_EXITINFO.

    Section TRAP_MMAP.

      Lemma trap_mmap_high_inv:
        ∀ d d´,
          trap_mmap_spec d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros; functional inversion H; subst; simpl;
        eapply uctx_set_errno_high_inv; eauto;
        eapply thread_vmx_set_mmap_high_inv; eauto.
        eapply big2_ptResv_high_level_inv; eauto.
      Qed.

      Lemma trap_mmap_low_inv:
        ∀ d d´ n,
          trap_mmap_spec d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros; functional inversion H; subst; simpl;
        eapply uctx_set_errno_low_inv; eauto;
        eapply thread_vmx_set_mmap_low_inv; eauto.
        eapply big2_ptResv_low_level_inv; eauto.
      Qed.

      Lemma trap_mmap_kernel_mode:
        ∀ d d´,
          trap_mmap_spec d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros; functional inversion H; subst;
        eapply uctx_set_errno_kernel_mode; eauto;
        eapply thread_vmx_set_mmap_kernel_mode; eauto.
        eapply big2_ptResv_kernel_mode; eauto.
      Qed.

      Global Instance trap_mmap_inv: PreservesInvariants trap_mmap_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply trap_mmap_low_inv; eauto.
        - eapply trap_mmap_high_inv; eauto.
        - eapply trap_mmap_kernel_mode; eauto.
      Qed.

    End TRAP_MMAP.

    Section PTFault_RESV_INV.

      Lemma ptfault_resv_high_inv:
        ∀ d d´ i,
          ptfault_resv_spec i d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros; functional inversion H; subst; simpl.
        eapply big2_ptResv_high_level_inv; eauto.
      Qed.

      Lemma ptfault_resv_low_inv:
        ∀ d d´ i n,
          ptfault_resv_spec i d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros; functional inversion H; subst; simpl.
        eapply big2_ptResv_low_level_inv; eauto.
      Qed.

      Lemma ptfault_resv_kernel_mode:
        ∀ d d´ i,
          ptfault_resv_spec i d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros; functional inversion H; subst;
        
        eapply big2_ptResv_kernel_mode; eauto.
      Qed.

      Global Instance ptfault_resv_inv: PreservesInvariants ptfault_resv_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply ptfault_resv_low_inv; eauto.
        - eapply ptfault_resv_high_inv; eauto.
        - eapply ptfault_resv_kernel_mode; eauto.
      Qed.

    End PTFault_RESV_INV.

    Global Instance trap_proc_create_inv: TrapProcCreateINV trap_proc_create_spec.
    Proof.
      destruct big2_proc_create_inv.
      split; unfold trap_proc_create_spec; intros; subdestruct; eauto; subst.
      - eapply uctx_set_errno_high_inv; eauto.
      - eapply uctx_set_errno_high_inv; eauto.
        exploit pcreate_high_level_invariant; eauto.
        intros.
        simpl in ×.
        eapply uctx_set_retval1_high_inv; eauto.
      - eapply uctx_set_errno_high_inv; eauto.
      - eapply uctx_set_errno_high_inv; eauto.
      - eapply uctx_set_errno_high_inv; eauto.

      - eapply uctx_set_errno_low_inv; eauto.
      - eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
        exploit pcreate_low_level_invariant; eauto;
        try (eapply stencil_find_symbol_inject´; eauto;
             eapply flat_inj_inject_incr; assumption).
      - eapply uctx_set_errno_low_inv; eauto.
      - eapply uctx_set_errno_low_inv; eauto.
      - eapply uctx_set_errno_low_inv; eauto.

      - eapply uctx_set_errno_kernel_mode; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.

      - eapply Mem.load_extends in Hdestruct11; eauto.
        destruct Hdestruct11 as [v2[HLD HV]].
        inv HV. subrewrite´.

      - pose proof H1 as Hsymbol. apply H1 in Hdestruct10.
        eapply Mem.load_inject in Hdestruct11; eauto.
        destruct Hdestruct11 as [v2[HLD HV]].
        rewrite Z.add_0_r in HLD. subst.
        rewrite HLD. inv HV; eauto.
        rewrite H4 in Hdestruct10.
        inv Hdestruct10. rewrite Int.add_zero.
        subrewrite´.
    Qed.

  End Prim.

  Definition ttrap_fresh : compatlayer (cdata RData) :=
    ptfault_resv ↦ gensem ptfault_resv_spec
                  ⊕ sys_proc_create ↦ trap_proccreate_compatsem trap_proc_create_spec
                  ⊕ sys_get_quota ↦ gensem trap_get_quota_spec
                  ⊕ sys_receive_chan ↦ gensem trap_receivechan_spec
                  ⊕ sys_sendto_chan ↦ gensem trap_sendtochan_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_getc ↦ gensem sys_getc_spec
                  ⊕ sys_putc ↦ gensem sys_putc_spec.

  Definition ttrap_passthrough : compatlayer (cdata RData) :=

    vmxinfo_get ↦ gensem thread_vmxinfo_get_spec
          ⊕ palloc ↦ gensem big2_palloc_spec
          
          ⊕ pt_read ↦ gensem thread_ptRead_spec
          ⊕ pt_resv ↦ gensem big2_ptResv_spec
          ⊕ thread_yield ↦ gensem big2_thread_yield_spec

          ⊕ get_CPU_ID ↦ gensem thread_get_CPU_ID_spec
          ⊕ get_curid ↦ gensem thread_get_curid_spec

          ⊕ uctx_get ↦ gensem thread_uctx_get_spec
          ⊕ uctx_set ↦ gensem thread_uctx_set_spec

          ⊕ vmx_run_vm ↦ primcall_vmx_enter_compatsem thread_vm_run_spec vmx_run_vm
          ⊕ vmx_return_from_guest ↦ primcall_vmx_return_compatsem thread_vmx_return_from_guest_spec
          ⊕ vmx_init ↦ vmcs_set_defaults_compatsem thread_vmx_init_spec

          ⊕ uctx_arg1 ↦ gensem uctx_arg1_spec
          ⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
          ⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
          ⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
          ⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
          ⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec

          ⊕ cli ↦ gensem thread_cli_spec
          ⊕ sti ↦ gensem thread_sti_spec

          ⊕ trap_get ↦ primcall_trap_info_get_compatsem thread_trap_info_get_spec
          ⊕ trap_set ↦ primcall_trap_info_ret_compatsem thread_trap_info_ret_spec
          ⊕ proc_start_user ↦ primcall_start_user_tm_compatsem thread_proc_start_user_spec
          ⊕ proc_exit_user ↦ primcall_exit_user_tm_compatsem thread_proc_exit_user_spec
          ⊕ proc_start_user2 ↦ primcall_start_user_tm_compatsem2 thread_proc_start_user_spec
          ⊕ proc_exit_user2 ↦ primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec
          ⊕ accessors ↦ {| exec_load := (@exec_loadex _ _ _ _ _ _ _ _ Hmwd);
                           exec_store := (@exec_storeex _ _ _ _ _ _ _ _ Hmwd) |}.

  Definition ttrap : compatlayer (cdata RData) := ttrap_fresh ⊕ ttrap_passthrough.

End WITHMEM.