Library mcertikos.proc.PCVIntroCode

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 PCVIntro.
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 CVOpGenSpec.
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 PCVIntroCSource.

Module PCVINTROCODE.

  Section WithPrimitives.

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

      Let L: compatlayer (cdata RData) := set_sync_chan_count ↦ gensem set_sync_chan_count_spec
                                        
                                        ⊕ page_copy ↦ gensem page_copy_spec.

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

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

      Section IPCSendBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bset_sync_chan_count: block.

        Hypothesis hset_sync_chan_count1 : Genv.find_symbol ge set_sync_chan_count = Some bset_sync_chan_count.

        Hypothesis hset_sync_chan_count2 : Genv.find_funct_ptr ge bset_sync_chan_count
          = Some (External (EF_external set_sync_chan_count (signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
                                                                               (Tcons tint (Tcons tint Tnil)) tvoid cc_default).

        Variable bpage_copy: block.

        Hypothesis hpage_copy1 : Genv.find_symbol ge page_copy = Some bpage_copy.

        Hypothesis hpage_copy2 : Genv.find_funct_ptr ge bpage_copy
          = Some (External (EF_external page_copy (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tvoid cc_default))
                                                                               (Tcons tint (Tcons tint (Tcons tint Tnil))) tvoid cc_default).

        Lemma ipc_send_body_body_correct:
          ∀ m d d´ env le fromid vaddrval scountval retval,
            env = PTree.empty _
            → PTree.get _chid le = Some (Vint fromid)
            → PTree.get _vaddr le = Some (Vint vaddrval)
            → PTree.get _scount le = Some (Vint scountval)
            → high_level_invariant d
            → ipc_send_body_spec (Int.unsigned fromid) (Int.unsigned vaddrval) (Int.unsigned scountval) d
                 = Some (d´, Int.unsigned retval)
            → ∃ le´,
                 exec_stmt ge env le ((m, d): mem) ipc_send_body_body E0 le´
                                      (m, d´) (Out_return (Some (Vint retval, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold ipc_send_body_body.
          assert(valid_cid: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H3; auto).
          functional inversion H4; subst.
          unfold curid in ×.
          rewrite Zmin_spec in H6.
          functional inversion H13; subst.
          destruct (zlt (Int.unsigned scountval) 1024).

          apply unsigned_inj in H6.
          subst.
          esplit.
          repeat vcgen.

          {
            rewrite Zmin_spec in ×.
            repeat zdestruct.
            repeat rewrite Int.unsigned_repr; try omega.
            unfold page_copy_spec; simpl.
            Require Import CommonTactic.
            unfold index in ×.
            subrewrite´.
            rewrite zle_le_true.
            unfold cpu, l´, cpu in ×.
            rewrite H24. rewrite Int.repr_unsigned.
            reflexivity.
            repeat discharge_unsigned_range.
            omega.
          }

          subst.
          rewrite <- Int.repr_unsigned with retval.
          rewrite <- H6.
          unfold l´, cpu in ×.
          esplit.
          repeat vcgen.

          Opaque page_copy_aux.
          rewrite Zmin_spec in ×.
          repeat zdestruct.
          repeat rewrite Int.unsigned_repr; try omega.
          Opaque Z.mul Z.add Z.sub.
          unfold page_copy_spec; simpl.
          unfold index in ×.
          subrewrite´.
          change (Pos.to_nat 1024) with (Z.to_nat 1024).
          rewrite H23, H24.
          reflexivity.
        Qed.

      End IPCSendBody.

      Theorem ipc_send_body_code_correct:
        spec_le (ipc_send_body ↦ ipc_send_body_spec_low) (〚ipc_send_body ↦ f_ipc_send_body 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (ipc_send_body_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_ipc_send_body)
                                                               (Vint fromid :: Vint vaddr :: Vint rcount :: nil)
                                                               (create_undef_temps (fn_temps f_ipc_send_body)))) H1.
      Qed.

    End IPCSEND.

    Section IPCRECEIVEBODY.

      Let L: compatlayer (cdata RData) := get_sync_chan_count ↦ gensem get_sync_chan_count_spec
       
       ⊕ set_sync_chan_count ↦ gensem set_sync_chan_count_spec
       ⊕ page_copy_back ↦ gensem page_copy_back_spec.

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

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

      Section IPCReceiveBodyBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_sync_chan_count: block.
        Hypothesis hget_sync_chan_count1: Genv.find_symbol ge get_sync_chan_count = Some bget_sync_chan_count.
        Hypothesis hget_sync_chan_count2: Genv.find_funct_ptr ge bget_sync_chan_count = Some (External (EF_external get_sync_chan_count (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).

        Variable bset_sync_chan_count: block.
        Hypothesis hset_sync_chan_count1: Genv.find_symbol ge set_sync_chan_count = Some bset_sync_chan_count.
        Hypothesis hset_sync_chan_count2: Genv.find_funct_ptr ge bset_sync_chan_count = Some (External (EF_external set_sync_chan_count (signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default)) (Tcons tint (Tcons tint Tnil)) tvoid cc_default).

        Variable bpage_copy_back: block.

        Hypothesis hpage_copy_back1 : Genv.find_symbol ge page_copy_back = Some bpage_copy_back.

        Hypothesis hpage_copy_back2 : Genv.find_funct_ptr ge bpage_copy_back
          = Some (External (EF_external page_copy_back (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tvoid cc_default))
                                                                               (Tcons tint (Tcons tint (Tcons tint Tnil))) tvoid cc_default).

        Lemma ipc_receive_body_body_correct: ∀ m d d´ env le fromid vaddrval rcountval val,
                                           env = PTree.empty _ →
                                           PTree.get _chid le = Some (Vint fromid) →
                                           PTree.get _vaddr le = Some (Vint vaddrval) →
                                           PTree.get _rcount le = Some (Vint rcountval) →
                                           high_level_invariant d →
                                           ipc_receive_body_spec (Int.unsigned fromid) (Int.unsigned vaddrval) (Int.unsigned rcountval) d = Some (d´, Int.unsigned val) →
                                           0 ≤ Int.unsigned fromid < num_chan →
                                           ∃ le´,
                                             exec_stmt ge env le ((m, d): mem) ipc_receive_body_body E0 le´ (m, d´) (Out_return (Some (Vint val, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold ipc_receive_body_body.
          assert(valid_cid: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H3; auto).
          functional inversion H4; subst.
          unfold curid in ×.
          rewrite Zmin_spec in ×.
          destruct (zlt (Int.unsigned scount) (Int.unsigned rcountval)).

          apply unsigned_inj in H7.
          subst.
          functional inversion H14; subst.
          {
            esplit.
            d6 vcgen; eauto.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.

            unfold get_sync_chan_count_spec.
            rewrite H10, H11, H9, H8.
            rewrite zle_lt_true; try assumption.
            rewrite H13. reflexivity.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.

            repeat vcgen.

            unfold set_sync_chan_count_spec.
            simpl. rewrite H8, H9, H10, H11, H13.
            rewrite zle_lt_true; try omega.
            reflexivity.
          }

          subst.
          rewrite <- Int.repr_unsigned with val.
          rewrite <- H7.
          functional inversion H14; subst.
          esplit.

          d7 vcgen; eauto.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.

          unfold get_sync_chan_count_spec.
          rewrite H10, H11, H9, H8.
          rewrite zle_lt_true; try assumption.
          rewrite H13. reflexivity.

          discharge_cmp.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.

          unfold set_sync_chan_count_spec.
          simpl. rewrite H8, H9, H10, H11, H13.
          rewrite zle_lt_true; try omega.
          reflexivity.
         Qed.

      End IPCReceiveBodyBody.

      Theorem ipc_receive_body_code_correct:
        spec_le (ipc_receive_body ↦ ipc_receive_body_spec_low) (〚ipc_receive_body ↦ f_ipc_receive_body 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (ipc_receive_body_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_ipc_receive_body)
                                                               (Vint chid :: Vint vaddr :: Vint scount :: nil)
                                                               (create_undef_temps (fn_temps f_ipc_receive_body)))) H1.
      Qed.

    End IPCRECEIVEBODY.

    Section FIFOBBQ_POOL_INIT.

      Let L: compatlayer (cdata RData) :=
        tdqueue_init ↦ gensem tdqueue_init0_spec
                     ⊕ init_sync_chan ↦ gensem init_sync_chan_spec.

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

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

      Section FIFOBBQ_POOL_INIT_BODY.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable btdqueue_init: block.

        Hypothesis htdqueue_init1 : Genv.find_symbol ge tdqueue_init = Some btdqueue_init.

        Hypothesis htdqueue_init2 : Genv.find_funct_ptr ge btdqueue_init =
                                    Some (External (EF_external tdqueue_init
                                                                (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                   (Tcons tint Tnil) Tvoid cc_default).

        Variable binit_sync_chan: block.

        Hypothesis hinit_sync_chan1 : Genv.find_symbol ge init_sync_chan = Some binit_sync_chan.

        Hypothesis hinit_sync_chan2 : Genv.find_funct_ptr ge binit_sync_chan =
                                      Some (External (EF_external init_sync_chan
                                                                  (signature_of_type (Tcons tint Tnil) tvoid cc_default))
                                                     (Tcons tint Tnil) tvoid cc_default).

        Definition fifobbq_pool_init_mk_rdata (adt: RData) (index: Z) :=
          adt {syncchpool: init_zmap index (SyncChanValid (Int.repr num_chan) Int.zero Int.zero Int.zero)
                                     (syncchpool adt)}.


        Section fifobbq_pool_init_loop_proof.

          Variable minit: memb.
          Variable adt: RData.

          Hypothesis pg: pg adt = true.
          Hypothesis ipt: ipt adt = true.
          Hypothesis ihost: ihost adt = true.
          Hypothesis ikern: ikern adt = true.

          Definition fifobbq_pool_init_loop_body_P (le: temp_env) (m: mem): Prop :=
            PTree.get _i le = Some (Vint Int.zero) ∧
            m = (minit, adt).

          Definition fifobbq_pool_init_loop_body_Q (le : temp_env) (m: mem): Prop :=
            m = (minit, fifobbq_pool_init_mk_rdata adt num_chan).

          Lemma fifobbq_pool_init_loop_correct_aux :
            LoopProofSimpleWhile.t f_fifobbq_pool_init_while_condition
                                   f_fifobbq_pool_init_while_body ge
                                   (PTree.empty _) (fifobbq_pool_init_loop_body_P)
                                   (fifobbq_pool_init_loop_body_Q).
          Proof.
            generalize max_unsigned_val; intro muval.
            apply LoopProofSimpleWhile.make with
            (W := Z)
              (lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
              (I := fun le m w ⇒ ∃ i,
                        PTree.get _i le = Some (Vint i) ∧
                        0 ≤ Int.unsigned i ≤ num_chan ∧
                        (Int.unsigned i = 0 ∧
                         m = (minit, adt) ∨
                         Int.unsigned i > 0 ∧
                         m = (minit, fifobbq_pool_init_mk_rdata adt (Int.unsigned i))) ∧
                        w = num_chan + 1- Int.unsigned i
              ).
            - apply Zwf_well_founded.
            - intros.
              unfold fifobbq_pool_init_loop_body_P in H.
              destruct H as [tile msubst].
              subst.
              esplit. esplit.
              repeat vcgen.
            - intros.
              destruct H as [i tmpH].
              destruct tmpH as [tile tmpH].
              destruct tmpH as [irange tmpH].
              destruct tmpH as [icase nval].
              subst.
              unfold f_fifobbq_pool_init_while_body.
              destruct irange as [ilow ihigh].
              apply Zle_lt_or_eq in ihigh.
              destruct m.

              Caseeq ihigh.
              + Case "Int.unsigned i < num_chan".
                intro ihigh.

                Caseeq icase.
                × SCase "Int.unsigned i = 0".
                  intro tmpH; destruct tmpH as [ival mval].
                  rewrite ival in ×.
                  injection mval; intros; subst.
                  esplit. esplit.
                  repeat vcgen.
                  esplit. esplit.
                  repeat vcgen.
                  ∃ (num_chan + 1 - Int.unsigned i - 1).
                  repeat vcgen.
                  esplit.
                  repeat vcgen.
                  right.
                  split.
                  omega.
                  f_equal.
                  unfold fifobbq_pool_init_mk_rdata.
                  rewrite ival.
                  reflexivity.

                × SCase "Int.unsigned i > 0".
                  intro tmpH; destruct tmpH as [ival mval].
                  injection mval; intros; subst.
                  esplit. esplit.
                  repeat vcgen.
                  esplit. esplit.
                  repeat vcgen.
                  unfold fifobbq_pool_init_mk_rdata; simpl.
                  unfold init_sync_chan_spec; simpl.
                  rewrite ikern, ihost, pg, ipt.
                  rewrite zle_lt_true.
                  repeat zdestruct.
                  reflexivity.
                  omega.
                  ∃ (num_chan + 1 - Int.unsigned i - 1).
                  repeat vcgen.
                  esplit.
                  repeat vcgen.
                  right.
                  split.
                  omega.
                  f_equal.
                  unfold fifobbq_pool_init_mk_rdata.
                  replace (Int.unsigned i - 1 + 1) with (Int.unsigned i) by omega.
                  replace (Int.unsigned i + 1 - 1 + 1) with (Int.unsigned i + 1) by omega.
                  rewrite init_zmap_eq by omega.
                  reflexivity.

              + Case "Int.unsigned i = num_chan + 1".
                intro ival.
                rewrite ival.
                esplit. esplit.
                repeat vcgen.
                unfold fifobbq_pool_init_loop_body_Q.
                Caseeq icase; intro tmpH; destruct tmpH as [iv mval].
                exfalso; rewrite iv in ival; omega.
                rewrite ival in mval. assumption.
          Qed.

        End fifobbq_pool_init_loop_proof.

        Lemma fifo_bbq_pool_init_loop_correct: ∀ m d d´ le,
            PTree.get _i le = Some (Vint (Int.repr 0)) →
            pg d = true →
            ipt d = true →
            ihost d = true →
            ikern d = true →
            d´ = fifobbq_pool_init_mk_rdata d num_chan →
            ∃ le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem)
                        (Swhile f_fifobbq_pool_init_while_condition f_fifobbq_pool_init_while_body)
                        E0 le´ (m, d´) Out_normal.
        Proof.
          intros.
          generalize (fifobbq_pool_init_loop_correct_aux m d H0 H1 H2 H3).
          unfold fifobbq_pool_init_loop_body_P.
          unfold fifobbq_pool_init_loop_body_Q.
          intro LP.
          refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
          intro pre.
          destruct pre as [le´´ tmppre].
          destruct tmppre as [m´´ tmppre].
          destruct tmppre as [stmp m´´val].
          ∃ le´´.
          subst.
          assumption.
          auto.
        Qed.

        Require Import CalRealPT.
        Require Import CalTicketLock.
        Require Import CalRealIDPDE.
        Require Import CalRealSMSPool.
        Require Import DeviceStateDataType.

        Lemma fifobbq_pool_init_body_correct:
          ∀ m d d´ env le mbi_adr,
            env = PTree.empty _ →
            PTree.get _mbi_adr le = Some (Vint mbi_adr) →
            PTree.get _i le = Some Vundef →
            kernel_mode d →
            high_level_invariant d →
            fifobbq_pool_init_spec (Int.unsigned mbi_adr) d = Some d´ →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) f_fifobbq_pool_init_body E0 le´ (m, d´) Out_normal.
        Proof.
          intros.
          destruct H1.
          functional inversion H4; subst.
          unfold f_fifobbq_pool_init_body; subst.
          set (ds := d {ioapic/s: ioapic_init_aux d.(ioapic).(s) (Z.to_nat ((d.(ioapic).(s).(IoApicMaxIntr) + 1) - 1))}
                       {lapic: (mkLApicData
                                  (mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic d))) true
                                                (32 + 7) true true true 0 50 false 0))
                                 {l1: l1 (lapic d)}
                                 {l2: l2 (lapic d)}
                                 {l3: l3 (lapic d)}
                       } {ioapic / s / CurrentIrq: None}
                       {vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT d)} {nps: real_nps}
                       {AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool d)}
                       {multi_log: real_multi_log (multi_log d)}
                       {lock: real_lock (lock d)}
                       {idpde: real_idpde (idpde d)}
                       {smspool: real_smspool (smspool d)}
                       {abtcb: real_abtcb (abtcb d)}
                       {abq: real_abq (abq d)}).
          set (df := d {ioapic/s: ioapic_init_aux d.(ioapic).(s) (Z.to_nat ((d.(ioapic).(s).(IoApicMaxIntr) + 1) - 1))}
                       {lapic: (mkLApicData
                                  (mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic d))) true
                                                (32 + 7) true true true 0 50 false 0))
                                 {l1: l1 (lapic d)}
                                 {l2: l2 (lapic d)}
                                 {l3: l3 (lapic d)}
                       } {ioapic / s / CurrentIrq: None}
                       {vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT d)} {nps: real_nps}
                       {AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool d)}
                       {multi_log: real_multi_log (multi_log d)}
                       {lock: real_lock (lock d)}
                       {idpde: real_idpde (idpde d)}
                       {smspool: real_smspool (smspool d)}
                       {abtcb: real_abtcb (abtcb d)}
                       {abq: real_abq (abq d)}
                       {syncchpool : real_syncchpool (syncchpool d)}).
          exploit (fifo_bbq_pool_init_loop_correct m ds df (PTree.set _i (Vint (Int.repr 0)) (set_opttemp None Vundef le)));
            unfold ds in *; simpl in *; try assumption.
          - repeat vcgen.
          - reflexivity.
          - unfold fifobbq_pool_init_mk_rdata; simpl.
            unfold df.
            reflexivity.
          - intros tempH.
            destruct tempH as [le´ stmt´].
            subst.

            esplit.
            change E0 with (E0**E0).
            unfold exec_stmt.
            econstructor.
            Opaque real_multi_log real_smspool real_pt real_lock real_abtcb real_abq.
            Opaque fifobbq_pool_init_mk_rdata.
            Opaque Z.add Z.sub Z.mul Z.div.
            + econstructor.
              repeat vcgen.
              repeat vcgen.
              repeat vcgen.
              repeat vcgen.
              repeat vcgen.
              vcgen.
              vcgen.
              unfold tdqueue_init0_spec.
              rewrite H5, H6, H7, H8, H9, H10, H11, H12.
              reflexivity.
            + repeat vcgen.
        Qed.

      End FIFOBBQ_POOL_INIT_BODY.

      Theorem fifobbq_pool_init_code_correct:
        spec_le (fifobbq_pool_init ↦ fifobbq_pool_init_spec_low) (〚fifobbq_pool_init ↦ f_fifobbq_pool_init〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (fifobbq_pool_init_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_fifobbq_pool_init)
                                                                        (Vint mbi_adr :: nil)
                                                                        (create_undef_temps
                                                                           (fn_temps f_fifobbq_pool_init)))) muval.
      Qed.

    End FIFOBBQ_POOL_INIT.

  End WithPrimitives.

End PCVINTROCODE.