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 PUCtxtIntro.
Require Import ZArith.Zwf.
Require Import RealParams.
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 ProcGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import TacticsForTesting.
Require Import PUCtxtIntroCSource.
Require Import AbstractDataType.
Require Import CommonTactic.

Require Import ObjProc.
Require Import PUCtxtIntroDef.
Require Import GlobalOracleProp.

Module PUCTXTINTROCODE.

  Section WithPrimitives.

    Lemma Heq:
      ∀ d k ab aq u u0 u1 u2 u3 u4 u5,
        Some (d {kctxt: k} {abtcb: ab} {abq: aq}
                {uctxt: u5} {uctxt: u4}{uctxt: u3}
                {uctxt: u2} {uctxt: u1} {uctxt: u0} {uctxt: u}) =
        Some (d {kctxt: k} {abtcb: ab} {abq : aq} {uctxt: u}).
    Proof.
      symmetry.
      reflexivity.
    Qed.

    Context `{real_params: RealParams}.
    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.
    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 PROCCREATE.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem get_curid_spec
           ⊕ thread_spawn ↦ dnew_compatsem biglow_thread_spawn_spec
           ⊕ uctx_set ↦ gensem uctx_set_spec
           ⊕ uctx_set_eip ↦ uctx_set_eip_compatsem uctx_set_eip_spec
           ⊕ elf_load ↦ elf_load_compatsem.

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

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

      Section ProcCreateBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable (quota : int).

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 :
          Genv.find_funct_ptr ge bget_curid =
          Some (External (EF_external get_curid
                (signature_of_type Tnil tint cc_default))
                                   Tnil tint cc_default).

        Variable bthread_spawn: block.

        Hypothesis hthread_spawn1 : Genv.find_symbol ge thread_spawn = Some bthread_spawn.

        Hypothesis hthread_spawn2 :
          Genv.find_funct_ptr ge bthread_spawn =
          Some (External (EF_external thread_spawn
                (signature_of_type (Tcons (tptr tvoid) (Tcons tint (Tcons tint Tnil))) tint cc_default))
                                   (Tcons (tptr tvoid) (Tcons tint (Tcons tint Tnil))) tint cc_default).

        Variable buctx_set: block.

        Hypothesis huctx_set1 : Genv.find_symbol ge uctx_set = Some buctx_set.

        Hypothesis huctx_set2 : Genv.find_funct_ptr ge buctx_set = Some (External (EF_external uctx_set (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).

        Variable buctx_set_eip: block.

        Hypothesis huctx_set_eip1 : Genv.find_symbol ge uctx_set_eip = Some buctx_set_eip.

        Hypothesis huctx_set_eip2 : Genv.find_funct_ptr ge buctx_set_eip = Some (External (EF_external uctx_set_eip (signature_of_type (Tcons tint (Tcons (tptr tvoid) Tnil)) Tvoid cc_default)) (Tcons tint (Tcons (tptr tvoid) Tnil)) Tvoid cc_default).

        Variable belf_load: block.

        Hypothesis helf_load1 : Genv.find_symbol ge elf_load = Some belf_load.

        Hypothesis helf_load2 : Genv.find_funct_ptr ge belf_load = Some (External (EF_external elf_load (signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default)) (Tcons tint (Tcons tint Tnil)) tvoid cc_default).

        Lemma proc_create_body_correct:
          ∀ m d d´ env le proc_index b b´ buc ofs elf_id ofs´,
            env = PTree.empty _ →
            le ! telf_id = Some (Vint elf_id) → le ! tfun_addr = Some (Vptr buc ofs´) →
            le ! tquota = Some (Vint quota) →
            biglow_proc_create_spec d b b´ buc ofs´ (Int.unsigned quota) =
              Some (d´, Int.unsigned proc_index) →
            high_level_invariant d →
            Genv.find_symbol ge STACK_LOC = Some b →
            Int.unsigned ofs = (Int.unsigned proc_index + 1) × PgSize - 4 →
            Genv.find_symbol ge START_USER_FUN_LOC = Some b´ →
            (∃ fun_id, Genv.find_symbol ge fun_id = Some buc) →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) proc_create_body E0 le´ (m, d´)
                        (Out_return (Some (Vint proc_index, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          unfold proc_create_body.
          rename H3 into Hspec.
          unfold biglow_proc_create_spec in Hspec.
          subdestruct.
          inv Hspec.
          destruct H4, H8.

          esplit.
          rewrite <- Int.repr_unsigned with proc_index.
          d4 vcgen.
          repeat vcgen.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite Hdestruct0, Hdestruct1.
          rewrite Int.unsigned_repr; eauto; omega.
          d2 vcgen.
          repeat vcgen.
          unfold biglow_thread_spawn_spec; simpl.
          rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3.
          rewrite Hdestruct4.
          rewrite zlt_lt_true; auto.
          rewrite zle_le_true; auto.
          rewrite zlt_true; auto.
          rewrite Hdestruct8, Hdestruct9.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          erewrite <- stencil_matches_symbols; eauto.
          erewrite <- stencil_matches_symbols; eauto.
          d2 vcgen.
          repeat vcgen.
          d2 vcgen.
          repeat vcgen.
          unfold uctx_set_spec; simpl.
          rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
          rewrite zle_lt_true.
          reflexivity.
          omega.
          d2 vcgen.
          repeat vcgen.
          unfold uctx_set_spec; simpl.
          rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
          rewrite zle_lt_true.
          reflexivity.
          omega.
          d2 vcgen.
          repeat vcgen.
          unfold uctx_set_spec; simpl.
          rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
          rewrite zle_lt_true.
          reflexivity.
          omega.
          d2 vcgen.
          repeat vcgen.
          unfold uctx_set_spec; simpl.
          rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
          rewrite zle_lt_true.
          reflexivity.
          omega.
          d2 vcgen.
          repeat vcgen.
          unfold uctx_set_spec; simpl.
          rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
          rewrite zle_lt_true.
          reflexivity.
          omega.
          d2 vcgen.
          repeat vcgen.
          unfold uctx_set_spec; simpl.
          rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
          rewrite zle_lt_true.
          reflexivity.
          omega.
          d2 vcgen.
          repeat vcgen.
          repeat rewrite ZMap.set2.
          unfold uctx_set_eip_spec; simpl.
          rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
          rewrite zle_lt_true.
          reflexivity.
          omega.
          erewrite <- stencil_matches_symbols; eauto.
          repeat rewrite ZMap.set2.
          assert (tmprw: ∀ d u1 u2, d {uctxt: u1} {uctxt: u2} = d {uctxt: u2}) by reflexivity.
          assert (tmprw2: ∀ d u1 u2, (d {uctxt: u1}) {uctxt: u2} = d {uctxt: u2}) by reflexivity.
          repeat rewrite tmprw.
          repeat rewrite tmprw2.
          rewrite H9.
          rewrite Int.repr_unsigned.
          repeat rewrite ZMap.gss.
          repeat vcgen.
        Qed.


      End ProcCreateBody.

      Theorem proc_create_code_correct:
        spec_le (proc_create ↦ proc_create_spec_low) (〚proc_create ↦ f_proc_create 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        destruct H2, H3.
        generalize H; intro proccreatespec.
        unfold biglow_proc_create_spec in H.
        subdestruct.
        fbigsteptest (proc_create_body_correct s (Genv.globalenv p) makeglobalenv q
                                               b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp
                                               b4 Hb4fs Hb4fp
                                               m´0 labd labd´ (PTree.empty _)
                                               (bind_parameter_temps´ (fn_params f_proc_create)
                                                                      (Vint elf_id::Vptr buc ofs_uc::Vint q::nil)
                                                                      (create_undef_temps (fn_temps f_proc_create)))) H4.
        reflexivity.
        inv H.
        omega.
        inv H.
        omega.
        esplit; erewrite stencil_matches_symbols; eassumption.
        intro stmt.
        destruct stmt.
        repeat fbigstep_post.
      Qed.

    End PROCCREATE.

  End WithPrimitives.

End PUCTXTINTROCODE.