Build fixed (thanks Simon!)

logsem · Feb 12, 2024 · 7b28d6e · 7b28d6e
1 parent 30ed1b3
commit 7b28d6e
Show file tree

Hide file tree

Showing 19 changed files with 1,264 additions and 163 deletions.
diff --git a/theories/app_rel_logic/primitive_laws.v b/theories/app_rel_logic/primitive_laws.v
@@ -79,7 +79,9 @@ Proof.
   iApply ("IH" with "HΨ").
 Qed.
 
+
 (** Heap *)
+
 Lemma wp_alloc E v :
   {{{ True }}} Alloc (Val v) @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
@@ -88,9 +90,68 @@ Proof.
   iIntros (σ1) "[Hh Ht] !#".
   solve_red.
   iIntros "!> /=" (e2 σ2 Hs); inv_head_step.
-  iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[$ Hl]".
+  iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[? Hl]".
   { apply not_elem_of_dom, fresh_loc_is_fresh. }
-  iIntros "!>". iFrame. by iApply "HΦ".
+  iFrame.
+  rewrite map_union_empty -insert_union_singleton_l.
+  iFrame.
+  iIntros "!>". by iApply "HΦ".
+Qed.
+
+Lemma wp_allocN (N : nat) (z : Z) E v:
+  TCEq N (Z.to_nat z) →
+  (0 < N)%Z →
+  {{{ True }}}
+    AllocN (Val $ LitV $ LitInt $ z) (Val v) @ E
+                                                    {{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 N, (l +ₗ (i : nat)) ↦ v }}}.
+Proof.
+  iIntros (-> Hn Φ) "_ HΦ".
+  iApply wp_lift_atomic_head_step; [done|].
+  iIntros (σ1) "[Hh Ht] !#".
+  iSplit.
+  { iPureIntro.
+    rewrite /head_reducible.
+    eexists.
+    apply head_step_support_equiv_rel.
+    econstructor; eauto.
+    lia.
+  }
+  iIntros "!> /=" (e2 σ2 Hs); inv_head_step.
+  iMod ((ghost_map_insert_big _ _ with "Hh")) as "[$ Hl]".
+  iIntros "!>". iFrame.
+  iApply "HΦ".
+  iInduction (H) as [ | ?] "IH" forall (σ1).
+  - simpl.
+    iSplit; auto.
+    rewrite map_union_empty.
+    rewrite loc_add_0.
+    by rewrite big_sepM_singleton.
+  - rewrite seq_S.
+    rewrite heap_array_replicate_S_end.
+    iPoseProof (big_sepM_union _ _ _ _ with "Hl") as "[H1 H2]".
+    iApply big_sepL_app.
+    iSplitL "H1".
+    + iApply "IH".
+      { iPureIntro. lia. }
+      iApply "H1".
+    + simpl. iSplit; auto.
+      by rewrite big_sepM_singleton.
+      Unshelve.
+      {
+        apply heap_array_map_disjoint.
+        intros.
+        apply not_elem_of_dom_1.
+        by apply fresh_loc_offset_is_fresh.
+      }
+      apply heap_array_map_disjoint.
+      intros.
+      apply not_elem_of_dom_1.
+      rewrite dom_singleton.
+      apply not_elem_of_singleton_2.
+      intros H2.
+      apply loc_add_inj in H2.
+      rewrite replicate_length in H1.
+      lia.
 Qed.
 
 Lemma wp_load E l dq v :
@@ -195,7 +256,7 @@ Proof.
   iFrame.
   iModIntro.
   iApply ("HΦ" with "[$Hl //]").
-Qed.  
+Qed.
 
 End lifting.
 

diff --git a/theories/app_rel_logic/spec_rules.v b/theories/app_rel_logic/spec_rules.v
@@ -54,6 +54,8 @@ Section rules.
     eapply exec_det_step_ctx; [apply _| |done].
     subst l.
     solve_step.
+    rewrite state_upd_heap_singleton.
+    solve_distr.
   Qed.
 
   Lemma step_load E K l q v:

diff --git a/theories/ctx_logic/derived_laws.v b/theories/ctx_logic/derived_laws.v
@@ -119,7 +119,7 @@ Lemma wp_allocN s E v n :
           l ↦∗ replicate (Z.to_nat n) v }}}.
   Proof.
     iIntros (? Φ) "_ HΦ".
-    iApply wp_allocN; auto; try lia.
+    iApply wp_allocN_seq; auto; try lia.
     iModIntro.
     iIntros (l) "Hlm".
     iApply "HΦ".

diff --git a/theories/ctx_logic/primitive_laws.v b/theories/ctx_logic/primitive_laws.v
@@ -94,7 +94,7 @@ Proof.
 Qed.
 
 
-Lemma wp_allocN (N : nat) (z : Z) E v s:
+Lemma wp_allocN_seq (N : nat) (z : Z) E v s:
   TCEq N (Z.to_nat z) →
   (0 < N)%Z →
   {{{ True }}}

diff --git a/theories/ctx_logic/proofmode.v b/theories/ctx_logic/proofmode.v
@@ -3,16 +3,17 @@ From clutch.prob_lang Require Export wp_tactics.
 From clutch.ctx_logic Require Import primitive_laws derived_laws.
 From iris.prelude Require Import options.
 
-#[global] Program Instance rel_logic_wptactics_base `{!clutchGS Σ} : @WpTacticsBase Σ unit wp' _ _.
+
+#[global] Program Instance rel_logic_wptactics_base `{!clutchGS Σ} : @GwpTacticsBase Σ unit _ _ wp.
 Next Obligation. intros. by apply wp_value. Qed.
 Next Obligation. intros. by apply wp_fupd. Qed.
 Next Obligation. intros. by apply wp_bind. Qed.
 
-#[global] Program Instance rel_logic_wptactics_pure `{!clutchGS Σ} : @WpTacticsPure Σ unit wp' true.
+#[global] Program Instance rel_logic_wptactics_pure `{!clutchGS Σ} : @GwpTacticsPure Σ unit true wp.
 Next Obligation. intros. by eapply lifting.wp_pure_step_later. Qed.
 
-#[global] Program Instance rel_logic_wptactics_heap `{!clutchGS Σ} : @WpTacticsHeap Σ unit wp' true :=
-  Build_WpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) (λ l q vs, (l ↦∗{q} vs)%I) _ _ _ _.
+#[global] Program Instance rel_logic_wptactics_heap `{!clutchGS Σ} : @GwpTacticsHeap Σ unit true wp :=
+  Build_GwpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) (λ l q vs, (l ↦∗{q} vs)%I) _ _ _ _.
 Next Obligation. intros. by apply wp_alloc. Qed.
 Next Obligation. intros. by apply wp_allocN. Qed.
 Next Obligation. intros. by apply wp_load. Qed.