complete alloc

theories/lang/steps_wf.v

@@ -93,7 +93,7 @@ Lemma init_mem_lookup_empty l n :
   ∃ i, (0 ≤ i < n) ∧ l' = l +ₗ i.
 Proof. move => l' s' /init_mem_lookup_case [[//]|//]. Qed.
 
-Lemma init_stack_lookup α l n t :
+Lemma init_stacks_lookup α l n t :
   (∀ (i: nat), (i < n)%nat →
     init_stacks α l n t !! (l +ₗ i) = Some [mkItem Unique t None]) ∧
   (∀ (l': loc), (∀ (i: nat), (i < n)%nat → l' ≠ l +ₗ i) →
@@ -119,12 +119,12 @@ Proof.
     + specialize (Lt O ltac:(lia)). by rewrite shift_loc_0_nat in Lt.
 Qed.
 
-Lemma init_stack_lookup_case α l n t :
+Lemma init_stacks_lookup_case α l n t :
   ∀ l' s', init_stacks α l n t !! l' = Some s' →
   α !! l' = Some s' ∧ (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∨
   ∃ i, (0 ≤ i < n) ∧ l' = l +ₗ i.
 Proof.
-  destruct (init_stack_lookup α l n t) as [EQ1 EQ2].
+  destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
   intros l1 s1 Eq'.
   case (decide (l1.1 = l.1)) => [Eql|NEql];
     [case (decide (l.2 ≤ l1.2 < l.2 + n)) => [[Le Lt]|NIN]|].
@@ -143,13 +143,13 @@ Proof.
     rewrite EQ2 // in Eq'.
 Qed.
 
-Lemma init_stack_lookup_case_2 α l n t :
+Lemma init_stacks_lookup_case_2 α l n t :
   ∀ l' s', α !! l' = Some s' →
   init_stacks α l n t !! l' = Some s' ∧ (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∨
   ∃ i, (0 ≤ i < n) ∧ l' = l +ₗ i ∧
     init_stacks α l n t !! l' = Some [mkItem Unique t None].
 Proof.
-  destruct (init_stack_lookup α l n t) as [EQ1 EQ2].
+  destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
   intros l1 s1 Eq'.
   case (decide (l1.1 = l.1)) => [Eql|NEql];
     [case (decide (l.2 ≤ l1.2 < l.2 + n)) => [[Le Lt]|NIN]|].

theories/sim/cmra.v

@@ -38,6 +38,14 @@ Definition res := (ptrmap * cmap)%type.
 Definition resUR := prodUR ptrmapUR cmapUR.
 Definition to_resUR (r: res) : resUR := (to_ptrmapUR r.1, to_cmapUR r.2).
 
+
+Lemma local_update_discrete_valid_frame `{CmraDiscrete A} (r_f r r' : A) :
+  ✓ (r_f ⋅ r) → (r_f ⋅ r, r) ~l~> (r_f ⋅ r', r') → ✓ (r_f ⋅ r').
+Proof.
+  intros VALID UPD. apply cmra_discrete_valid.
+  apply (UPD O (Some r_f)); [by apply cmra_discrete_valid_iff|by rewrite /= comm].
+Qed.
+
 (** tag_kind properties *)
 Lemma tag_kind_incl_eq (k1 k2: tagKindR):
   ✓ k2 → k1 ≼ k2 → k1 ≡ k2.
@@ -75,6 +83,14 @@ Proof.
   destruct k as [[[]|]| |]; inversion Eq1; simplify_eq.
 Qed.
 
+Lemma tagKindR_valid (k: tagKindR) :
+  valid k → ∃ k', k ≡ to_tagKindR k'.
+Proof.
+  destruct k as [[[]|]|a |]; [|done|..|done]; intros VAL.
+  - by exists tkUnique.
+  - exists tkPub. by apply to_agree_uninj in VAL as [[] <-].
+Qed.
+
 (** cmap properties *)
 Lemma cmap_lookup_op_r (cm1 cm2: cmapUR) c T (VALID: ✓ (cm1 ⋅ cm2)):
   cm2 !! c = Some (to_callStateR (csOwned T)) →
@@ -203,13 +219,6 @@ Proof.
   - intros _. exists (∅: gmap loc _). by rewrite 2!left_id HL.
 Qed.
 
-Lemma local_update_discrete_valid_frame `{CmraDiscrete A} (r_f r r' : A) :
-  ✓ (r_f ⋅ r) → (r_f ⋅ r, r) ~l~> (r_f ⋅ r', r') → ✓ (r_f ⋅ r').
-Proof.
-  intros VALID UPD. apply cmra_discrete_valid.
-  apply (UPD O (Some r_f)); [by apply cmra_discrete_valid_iff|by rewrite /= comm].
-Qed.
-
 Lemma ptrmap_valid (r_f r: ptrmapUR) t h0 kh
   (Eqtg: r !! t = Some (to_tagKindR tkUnique, h0)) (VN: ✓ kh) :
   ✓ (r_f ⋅ r) → ✓ (r_f ⋅ (<[t:= kh]> r)).
@@ -229,12 +238,12 @@ Proof.
   destruct (h !! l) eqn:Eq; rewrite Eq //.
 Qed.
 
-Lemma tagKindR_valid (k: tagKindR) :
-  valid k → ∃ k', k ≡ to_tagKindR k'.
+Lemma to_heapletR_lookup h l s :
+  to_heapletR h !! l ≡ Some (to_agree s) → h !! l = Some s.
 Proof.
-  destruct k as [[[]|]|a |]; [|done|..|done]; intros VAL.
-  - by exists tkUnique.
-  - exists tkPub. by apply to_agree_uninj in VAL as [[] <-].
+  rewrite /to_heapletR lookup_fmap.
+  destruct (h !! l) as [s'|] eqn:Eqs; rewrite Eqs /=; [|by inversion 1].
+  intros Eq%Some_equiv_inj%to_agree_inj. by inversion Eq.
 Qed.
 
 (** The Core *)

theories/sim/one_step.v

@@ -66,24 +66,34 @@ Proof.
         intros [Eq1 Eq2]%Some_equiv_inj. simpl in Eq1, Eq2. split; [lia|].
         intros l s. rewrite -Eq2. intros Eqs stk Eqstk pm opro Instk NDIS.
         (* l is new memory *)
-        have EqPoi: s = ScPoison. { admit. }
-        split.
-        * rewrite EqPoi. (* init_mem_lookup *) admit.
-        * destruct k; [|by inversion Eq1].
-          exists []. admit.
+        apply to_heapletR_lookup in Eqs.
+        destruct (init_mem_lookup_empty _ _ _ _ Eqs) as [i [[? Lti] Eql]].
+        have Eqi: Z.of_nat (Z.to_nat i) = i by rewrite Z2Nat.id.
+        have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Eqi.
+        have ?: s = ScPoison.
+        { rewrite Eql -Eqi in Eqs.
+          rewrite (proj1 (init_mem_lookup lt (tsize T) ∅)) // in Eqs.
+          by inversion Eqs. } subst s.
+        have Eqs2 := proj1 (init_mem_lookup lt (tsize T) σt.(shp)) _ Lti'.
+        rewrite Eqi -Eql in Eqs2. split; [done|].
+        destruct k; [|by inversion Eq1].
+        have Eqstk2 := proj1 (init_stacks_lookup σt.(sst) lt (tsize T) tgt) _ Lti'.
+        rewrite Eqi -Eql Eqstk in Eqstk2.
+        exists []. move : Instk. inversion Eqstk2.
+        rewrite elem_of_list_singleton. by inversion 1.
       + rewrite lookup_insert_ne // right_id. intros Eqkh.
         specialize (PINV t k h Eqkh) as [Lt PINV].
         split. { etrans; [exact Lt|simpl; lia]. }
         intros l s Eqs stk Eqstk pm opro Instk NDIS.
         specialize (PINV l s Eqs).
-        destruct (init_stack_lookup_case _ _ _ _ _ _ Eqstk)
+        destruct (init_stacks_lookup_case _ _ _ _ _ _ Eqstk)
           as [[EqstkO Lti]|[i [[? Lti] Eql]]].
         * specialize (PINV _ EqstkO _ _ Instk NDIS) as [Eqss PINV].
           split; [|done].
           destruct (init_mem_lookup lt (tsize T) σt.(shp)) as [_ EQ].
           rewrite /= EQ //.
         * exfalso. move : Eqstk. simpl.
-          destruct (init_stack_lookup σt.(sst) lt (tsize T) tgt) as [EQ _].
+          destruct (init_stacks_lookup σt.(sst) lt (tsize T) tgt) as [EQ _].
           have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id //.
           specialize (EQ _ Lti'). rewrite Z2Nat.id // in EQ. rewrite Eql EQ.
           intros. inversion Eqstk. clear Eqstk. subst stk.
@@ -96,7 +106,7 @@ Proof.
       rewrite lookup_insert_ne // right_id.
       intros Eqh2 l Inl.
       specialize (Eqh _ _ Eqh2 l Inl) as (stk & pm & Eqsk & Instk).
-      destruct (init_stack_lookup_case_2 _ lt (tsize T) tgt _ _ Eqsk)
+      destruct (init_stacks_lookup_case_2 _ lt (tsize T) tgt _ _ Eqsk)
         as [[EqO NIn]|[i [[? Lti] [Eqi EqN]]]].
       + exists stk, pm. by rewrite EqO.
       + exfalso. apply (is_fresh_block σt.(shp) i).
@@ -123,7 +133,7 @@ Proof.
   left. (*  rewrite {1}/l {1}/t {1}EqFRESH -{1}Eqnp. *)
   apply (sim_body_result _ _ _ _ (PlaceR _ _ T) (PlaceR _ _ T)). intros.
   apply POST; eauto. by rewrite /ts Eqnp.
-Abort.
+Qed.
 
 (** Copy *)
 Lemma sim_body_copy_public fs ft r n l t Ts Tt σs σt Φ