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

ept_get_page_entry

        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) in ×. unfold L in ×.
        fbigstep_pre .
        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).

ept_get_page_entry

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

ept_add_mapping

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

ept_mmap

        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 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 (, Int.unsigned res)
             le´,
              exec_stmt ge env le ((m, d): mem) ept_mmap_body E0 le´ (m, ) (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:= ).
            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) in ×. unfold L in ×.
        fbigstep_pre .
        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).

ept_get_page_entry

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

ept_set_page_entry

        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 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
             le´,
              exec_stmt ge env le ((m, d): mem) ept_set_permission_body E0 le´ (m, ) 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) in ×. unfold L in ×.
        fbigstep_pre .
        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.