mcertikos.ipc.PIPCIntroCode

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 PIPCIntro.
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 IPCGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CalRealProcModule.
Require Import CLemmas.
Require Import TacticsForTesting.
Require Import CalRealProcModule.
Require Import AbstractDataType.
Require Import PIPCIntroCSource.
Require Import ObjProc.

Require Import CommonTactic.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import INVLemmaThreadContainer.

Module PIPCINTROCODE.

  Section WithPrimitives.

    Context `{single_oracle_prop: SingleOracleProp}.
    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 SYNCSENDTOCHAN.

      Let L: compatlayer (cdata RData) := syncsendto_chan_pre ↦ gensem thread_syncsendto_chan_pre_spec
                                        ⊕ ipc_send_body ↦ gensem thread_ipc_send_body_spec
                                        ⊕ release_lock_CHAN ↦ gensem big2_release_lock_SC_spec.

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

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

      Section SyncSendToChanBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bsyncsendto_chan_pre: block.

        Hypothesis hsyncsendto_chan_pre1 : Genv.find_symbol ge syncsendto_chan_pre = Some bsyncsendto_chan_pre.

        Hypothesis hsyncsendto_chan_pre2 : Genv.find_funct_ptr ge bsyncsendto_chan_pre
          = Some (External (EF_external syncsendto_chan_pre (signature_of_type (Tcons tint Tnil) tvoid cc_default)) (Tcons tint Tnil) tvoid cc_default).

        Variable bipc_send_body: block.

        Hypothesis hipc_send_body1 : Genv.find_symbol ge ipc_send_body = Some bipc_send_body.

        Hypothesis hipc_send_body2 : Genv.find_funct_ptr ge bipc_send_body
          = Some (External (EF_external ipc_send_body (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).

        Variable brelease_lock_CHAN: block.

        Hypothesis hrelease_lock_CHAN1 : Genv.find_symbol ge release_lock_CHAN = Some brelease_lock_CHAN.

        Hypothesis hrelease_lock_CHAN2 : Genv.find_funct_ptr ge brelease_lock_CHAN
          = Some (External (EF_external release_lock_CHAN (signature_of_type (Tcons tint Tnil) tvoid cc_default)) (Tcons tint Tnil) tvoid cc_default).

        Lemma syncsendto_chan_body_correct:
          ∀ m d d´ env le chid vaddr scount retval,
            env = PTree.empty _
            → PTree.get _chid le = Some (Vint chid)
            → PTree.get _vaddr le = Some (Vint vaddr)
            → PTree.get _scount le = Some (Vint scount)
            → high_level_invariant d
            → thread_syncsendto_chan_spec (Int.unsigned chid) (Int.unsigned vaddr) (Int.unsigned scount) d = Some (d´, Int.unsigned retval )
            → ∃ le´,
                 exec_stmt ge env le ((m , d ): mem) syncsendto_chan_body E0 le´
                                      (m , d´) (Out_return (Some (Vint retval , tint ))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syncsendto_chan_body.
          functional inversion H4; subst.
          unfold chid0 in ×.
          unfold slp_q_id in ×.
          Opaque Z.add Z.mul.
          assert(range: 0 ≤ SLEEP_Q_START + Int.unsigned chid ≤ Int.max_unsigned).
          { functional inversion H8.
            unfold ObjBigThread.big_ipc_send_body_spec in ×.
            subdestruct.
            inv H.
            Transparent Z.add Z.mul.
            omega. }
          Opaque Z.add Z.mul.
          esplit.
          repeat vcgen.
        Qed.

      End SyncSendToChanBody.

      Theorem syncsendto_chan_code_correct:
        spec_le (syncsendto_chan_post ↦ thread_syncsendto_chan_spec_low) (〚syncsendto_chan_post ↦ f_syncsendto_chan 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (syncsendto_chan_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m´0 labd labd´ (PTree.empty _)
                                        (bind_parameter_temps´ (fn_params f_syncsendto_chan)
                                                               (Vint chid :: Vint vaddr :: Vint scount :: nil)
                                                               (create_undef_temps (fn_temps f_syncsendto_chan)))) H0.
      Qed.

    End SYNCSENDTOCHAN.

    Section SYNCRECEIVECHAN.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
                                                    ⊕ tryreceive_chan ↦ gensem thread_tryreceive_chan_spec
                                                    ⊕ acquire_lock_CHAN ↦ gensem big2_acquire_lock_SC_spec
                                                    ⊕ release_lock_CHAN ↦ gensem big2_release_lock_SC_spec.

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

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

      Section SyncReceiveChanBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable btryreceive_chan: block.
        Hypothesis htryreceive_chan1 : Genv.find_symbol ge tryreceive_chan = Some btryreceive_chan.
        Hypothesis htryreceive_chan2 : Genv.find_funct_ptr ge btryreceive_chan = Some (External (EF_external tryreceive_chan (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).

        Variable bacquire_lock_CHAN: block.

        Hypothesis hacquire_lock_CHAN1 : Genv.find_symbol ge acquire_lock_CHAN = Some bacquire_lock_CHAN.

        Hypothesis hacquire_lock_CHAN2 : Genv.find_funct_ptr ge bacquire_lock_CHAN
          = Some (External (EF_external acquire_lock_CHAN (signature_of_type (Tcons tint Tnil) tvoid cc_default)) (Tcons tint Tnil) tvoid cc_default).

        Variable brelease_lock_CHAN: block.

        Hypothesis hrelease_lock_CHAN1 : Genv.find_symbol ge release_lock_CHAN = Some brelease_lock_CHAN.

        Hypothesis hrelease_lock_CHAN2 : Genv.find_funct_ptr ge brelease_lock_CHAN
          = Some (External (EF_external release_lock_CHAN (signature_of_type (Tcons tint Tnil) tvoid cc_default)) (Tcons tint Tnil) tvoid cc_default).

        Lemma syncreceive_chan_body_correct:
          ∀ m d d´ env le vaddrval rcountval val chid,
            env = PTree.empty _ →
            PTree.get _chid le = Some (Vint chid) →
            PTree.get _vaddr le = Some (Vint vaddrval) →
            PTree.get _rcount le = Some (Vint rcountval) →
            high_level_invariant d →
            thread_syncreceive_chan_spec (Int.unsigned chid) (Int.unsigned vaddrval) (Int.unsigned rcountval) d = Some (d´, Int.unsigned val ) →
            ∃ le´,
              exec_stmt ge env le ((m , d ): mem) syncreceive_chan_body E0 le´ (m , d´) (Out_return (Some (Vint val , tint ))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syncreceive_chan_body.
          functional inversion H4; subst.

          inv H3.
          unfold chid0, cpu, slp_q_id in ×.
          Opaque Z.add Z.mul.
          generalize (Int.unsigned_range chid); intro.
          esplit.
          repeat vcgen.
          functional inversion H12; subst; omega.
          functional inversion H12; subst; omega.
         Qed.

      End SyncReceiveChanBody.

      Theorem syncreceive_chan_code_correct:

        spec_le (syncreceive_chan ↦ thread_syncreceive_chan_spec_low) (〚syncreceive_chan ↦ f_syncreceive_chan 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (syncreceive_chan_body_correct s (Genv.globalenv p) makeglobalenv b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp m´0 labd labd´ (PTree.empty _)
                                        (bind_parameter_temps´ (fn_params f_syncreceive_chan)
                                                               (Vint chanid :: Vint vaddr :: Vint rcount :: nil)
                                                               (create_undef_temps (fn_temps f_syncreceive_chan)))) H1.
      Qed.

    End SYNCRECEIVECHAN.

  End WithPrimitives.

End PIPCINTROCODE.

Library mcertikos.ipc.PIPCIntroCode