Library mcertikos.proc.VEPTOpCode

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 Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import VEPTInit.
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 EPTInitGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import TacticsForTesting.
Require Import AbstractDataType.
Require Import VEPTOpCSource.

Module EPTINITCODE.

  Section WithPrimitives.

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


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

    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 EPT_GPA_TO_HPA.

      Let L: compatlayer (cdata RData) := ept_get_page_entry ↦ gensem ept_get_page_entry_spec.

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

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

      Section EptGpaToHpaBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bept_get_page_entry: block.

        Hypothesis hept_get_page_entry1 : Genv.find_symbol ge ept_get_page_entry = Some bept_get_page_entry.

        Hypothesis hept_get_page_entry2 : Genv.find_funct_ptr ge bept_get_page_entry
                                          = Some (External (EF_external ept_get_page_entry
                                                                        (signature_of_type (Tcons tint Tnil) tuint cc_default))
                                                           (Tcons tint Tnil) tuint cc_default).

        Lemma ept_gpa_to_hpa_body_correct:
          ∀ m d env le gpa hpa,
            env = PTree.empty _ →
            PTree.get tgpa le = Some (Vint gpa) →
            high_level_invariant d →
            ept_gpa_to_hpa_spec (Int.unsigned gpa) d = Some (Int.unsigned hpa) →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) ept_gpa_to_hpa_body E0 le´ (m, d) (Out_return (Some (Vint hpa, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold ept_gpa_to_hpa_body.
          functional inversion H2; subst.
          {
            esplit.
            repeat vcgen.
            instantiate (1:= hpa0).
            instantiate (1:= d).
            rewrite Int.unsigned_repr.
            reflexivity.
            omega.
            repeat vcgen.
            omega.
            omega.
            repeat vcgen.
            rewrite PTree.gss.
            rewrite H3.
            rewrite Int.repr_unsigned.
            reflexivity.
          }
          {
            assert (tmp´: 0 ≤ Int.unsigned gpa ≤ Int.max_unsigned).
            apply Int.unsigned_range_2.
            esplit.
            repeat vcgen.
            instantiate (1:= hpa0).
            instantiate (1:= d).
            rewrite Int.unsigned_repr.
            reflexivity.
            omega.
            repeat vcgen.
            omega.
            omega.
            repeat vcgen.
            rewrite PTree.gss.
            repeat rewrite Int.unsigned_repr.
            rewrite H3.
            rewrite Int.repr_unsigned.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
          }
        Qed.

      End EptGpaToHpaBody.

      Theorem ept_gpa_to_hpa_code_correct:
        spec_le (ept_gpa_to_hpa ↦ ept_gpa_to_hpa_spec_low) (〚ept_gpa_to_hpa ↦ f_ept_gpa_to_hpa 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (ept_gpa_to_hpa_body_correct s (Genv.globalenv p)
                                              makeglobalenv b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
                                              (bind_parameter_temps´ (fn_params f_ept_gpa_to_hpa)
                                                                     (Vint gpa::nil)
                                                                     (create_undef_temps
                                                                        (fn_temps f_ept_gpa_to_hpa)))) H0.
      Qed.

    End EPT_GPA_TO_HPA.

    Section EPT_MMAP.

      Let L: compatlayer (cdata RData) :=
             ept_get_page_entry ↦ gensem ept_get_page_entry_spec
           ⊕ ept_add_mapping ↦ gensem ept_add_mapping_spec.

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

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

      Section EptMMapBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bept_get_page_entry: block.

        Hypothesis hept_get_page_entry1 : Genv.find_symbol ge ept_get_page_entry = Some bept_get_page_entry.

        Hypothesis hept_get_page_entry2 : Genv.find_funct_ptr ge bept_get_page_entry
                                          = Some (External (EF_external ept_get_page_entry
                                                                        (signature_of_type (Tcons tuint Tnil) tuint cc_default))
                                                           (Tcons tuint Tnil) tuint cc_default).

        Variable bept_add_mapping: block.

        Hypothesis hept_add_mapping1 : Genv.find_symbol ge ept_add_mapping = Some bept_add_mapping.

        Hypothesis hept_add_mapping2 : Genv.find_funct_ptr ge bept_add_mapping
                                       = Some (External (EF_external ept_add_mapping
                                                                     (signature_of_type
                                                                        (Tcons tuint (Tcons tuint (Tcons tuint Tnil)))
                                                                        tuint cc_default))
                                                        (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tuint cc_default).

        Variable bept_mmap: block.

        Hypothesis hept_mmap1 : Genv.find_symbol ge ept_mmap = Some bept_mmap.

        Hypothesis hept_mmap2 : Genv.find_funct_ptr ge bept_mmap
                                = Some (External (EF_external ept_mmap
                                                              (signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint Tnil)))
                                                                                 tint cc_default))
                                                 (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tint cc_default).

        Lemma ept_mmap_body_correct:
          ∀ m d d´ env le gpa hpa memtype res,
            env = PTree.empty _ →
            PTree.get tgpa le = Some (Vint gpa) →
            PTree.get thpa le = Some (Vint hpa) →
            PTree.get tmemtype le = Some (Vint memtype) →
            high_level_invariant d →
            ept_mmap_spec (Int.unsigned gpa) (Int.unsigned hpa) (Int.unsigned memtype) d = Some (d´, Int.unsigned res) →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) ept_mmap_body E0 le´ (m, d´) (Out_return (Some (Vint res, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold ept_mmap_body.
          functional inversion H4; subst.
          {
            esplit.
            repeat vcgen.
            instantiate (1:= hpa´).
            instantiate (1:= d).
            rewrite Int.unsigned_repr.
            reflexivity.
            omega.
            repeat vcgen.
            omega.
            omega.
            repeat vcgen.
            repeat vcgen.
          }
          {
            assert (tmp´: 0 ≤ Int.unsigned gpa ≤ Int.max_unsigned).
            apply Int.unsigned_range_2.
            esplit.
            repeat vcgen.
            instantiate (1:= hpa´).
            instantiate (1:= d´).
            rewrite Int.unsigned_repr.
            reflexivity.
            omega.
            repeat vcgen.
            omega.
            omega.
            repeat vcgen.
            rewrite PTree.gss.
            rewrite H6.
            rewrite Int.repr_unsigned.
            reflexivity.
          }
        Qed.

      End EptMMapBody.

      Theorem ept_mmap_code_correct:
        spec_le (ept_mmap ↦ ept_mmap_spec_low) (〚ept_mmap ↦ f_ept_mmap 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (ept_mmap_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
                                        b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
                                        (bind_parameter_temps´ (fn_params f_ept_mmap)
                                                               (Vint gpa:: Vint hpa :: Vint memtype :: nil)
                                                               (create_undef_temps (fn_temps f_ept_mmap)))) H0.
      Qed.

    End EPT_MMAP.

    Section EPT_SET_PERMISSION.

      Let L: compatlayer (cdata RData) :=
             ept_get_page_entry ↦ gensem ept_get_page_entry_spec
           ⊕ ept_set_page_entry ↦ gensem ept_set_page_entry_spec.

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

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

      Section EptSetPermissionBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bept_get_page_entry: block.

        Hypothesis hept_get_page_entry1 : Genv.find_symbol ge ept_get_page_entry = Some bept_get_page_entry.

        Hypothesis hept_get_page_entry2 : Genv.find_funct_ptr ge bept_get_page_entry
                                          = Some (External (EF_external ept_get_page_entry
                                                                        (signature_of_type (Tcons tint Tnil)
                                                                                           tuint cc_default))
                                                           (Tcons tint Tnil) tuint cc_default).

        Variable bept_set_page_entry: block.

        Hypothesis hept_set_page_entry1 : Genv.find_symbol ge ept_set_page_entry = Some bept_set_page_entry.

        Hypothesis hept_set_page_entry2 : Genv.find_funct_ptr ge bept_set_page_entry
                                          = Some (External (EF_external ept_set_page_entry
                                                                        (signature_of_type (Tcons tuint (Tcons tuint Tnil))
                                                                                           tvoid cc_default))
                                                           (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).

        Lemma ept_set_permission_body_correct:
          ∀ m d d´ env le gpa perm,
            env = PTree.empty _ →
            PTree.get tgpa le = Some (Vint gpa) →
            PTree.get tperm le = Some (Vint perm) →
            high_level_invariant d →
            ept_set_permission_spec (Int.unsigned gpa) (Int.unsigned perm) d = Some d´ →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) ept_set_permission_body E0 le´ (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold ept_set_permission_body.
          functional inversion H3; subst.
          assert (H7: 0 ≤ Int.unsigned perm ≤ Int.max_unsigned).
          apply Int.unsigned_range_2.
          unfold hpa in ×.
          esplit.
          repeat vcgen.
          instantiate (1:= hpa´).
          instantiate (1:= d).
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          unfold Int.or.
          repeat rewrite Int.unsigned_repr.
          rewrite H4.
          reflexivity.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
        Qed.

      End EptSetPermissionBody.

      Theorem ept_set_permission_code_correct:
        spec_le (ept_set_permission ↦ ept_set_permission_spec_low) (〚ept_set_permission ↦ f_ept_set_permission 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (ept_set_permission_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
                                                  b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
                                                  (bind_parameter_temps´ (fn_params f_ept_set_permission)
                                                                         (Vint gpa::Vint p0::nil)
                                                                         (create_undef_temps (fn_temps f_ept_set_permission)))) H0.
      Qed.


    End EPT_SET_PERMISSION.

  End WithPrimitives.

End EPTINITCODE.