Library mcertikos.security.SecurityInv

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 LAsm.
Require Import XOmega.

Require Import compcert.cfrontend.Ctypes.
Require Import Conventions.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.

Require Import AbstractDataType.
Require Import Soundness.
Require Import TSysCall.
Require Import I64Layer.
Require Import LoadStoreSem2.

Require Import SecurityCommon.
Require Import ProofIrrelevance.
Require Import MakeProgram.

Require Import SecurityInv1.
Require Import SecurityInv2.


Section WITHMEM.

  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.

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

  Local Instance : ExternalCallsOps (mwd (cdata RData)) :=
    CompatExternalCalls.compatlayer_extcall_ops tsyscall_layer.
  Local Instance : LayerConfigurationOps := compatlayer_configuration_ops tsyscall_layer.

  Section WITHIMPL.

    Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
    Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.

    Variables (s : stencil) (M : module) (ge : genv) (b : block).
    Hypothesis (Hmake : make_globalenv s M tsyscall_layer = OK ge).
    Hypothesis (Hpsu : Genv.find_symbol ge proc_start_user = Some b).

    Section SECURE_INV.


      Record secure_inv id d :=
        {
          sec_high_inv: high_level_invariant d;
          sec_ihost_inv: ihost d = true;
          sec_RA_startuser_inv: RA_startuser b d;
          sec_single_mapped_inv: single_mapped (LAT d) (nps d) id;
          sec_unshared_inv: unshared (LAT d) (nps d) id
        }.

      Record secure_inv' id rs d :=
        {
          sec_used: cused (ZMap.get id (AC d)) = true;
          sec_usermode: usermode b rs d
        }.


      Lemma secure_inv_init :
        ∀ id, secure_inv id init_adt.
      Proof.
        intro id; constructor.
        - apply empty_data_high_level_invariant.
        - auto.
        - intros ? ? Hcon; simpl in Hcon; zmap_simpl; inv Hcon.
        - intros ? ? ? ? ? Hcon; simpl in Hcon; zmap_simpl; inv Hcon.
        - simpl; intros ? ? Hcon; inv Hcon.
          zmap_simpl; inv H0.
      Qed.


      Lemma secure_inv_preserved :
        ∀ id rs rs' (m m' : mem) (d d' : cdata RData) t,
          LAsm.step ge (State rs (m,d)) t (State rs' (m',d')) →
          secure_inv id d → secure_inv id d'.
      Proof.
        intros id rs rs' m m' d d' t Hstep Hinv.
        destruct Hinv; constructor.
        - eapply step_inv1; eauto.
        - eapply ihost_inv; eauto.
        - eapply RA_startuser_inv; eauto.
        - eapply step_inv1; eauto.
        - eapply step_inv1; eauto.
      Qed.

      Lemma secure_inv'_preserved :
        ∀ id rs rs' (m m' : mem) (d d' : cdata RData) t,
          LAsm.step ge (State rs (m,d)) t (State rs' (m',d')) →
          secure_inv id d → secure_inv' id rs d → secure_inv' id rs' d'.
      Proof.
        intros id rs rs' m m' d d' t Hstep Hinv Hinv'.
        destruct Hinv; destruct Hinv'; constructor.
        - eapply step_inv1; eauto.
        - eapply usermode_inv; eauto.
      Qed.

    End SECURE_INV.

  End WITHIMPL.

End WITHMEM.