Commit 15062624 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris and many random changes.

- Consistent notation for ↦ of the C language: `x ↦C[lv]{q] v`, which is
  not redefined in every file.
- Many useless stylistic changes.
parent 202d84eb
......@@ -10,7 +10,6 @@ theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/c_translation/derived.v
theories/vcgen/dcexpr.v
# theories/vcgen/env.v
theories/vcgen/denv.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
......
......@@ -7,5 +7,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "branch.gen_proofmode.2018-05-31.1.27914f3f") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-06-18.3.33f0c279") | (= "dev") }
]
......@@ -8,7 +8,7 @@ Section derived.
Context `{amonadG Σ}.
Lemma a_load_ret (l: loc) (q : Qp) (w: val) R Φ:
l U{q} w (l U{q} w - Φ w) -
l C{q} w (l C{q} w - Φ w) -
awp (a_load (a_ret (#l)%E)) R Φ.
Proof.
iIntros "H". iApply a_load_spec.
......@@ -18,21 +18,21 @@ Section derived.
Lemma a_alloc_ret (e: expr) (ev: val) R Φ:
IntoVal e ev
( (l: loc), (l U ev - Φ #l)) -
( l: loc, l C ev - Φ #l) -
awp (a_alloc (a_ret e)) R Φ.
Proof.
iIntros (<-%of_to_val) "H". iApply a_alloc_spec.
iApply awp_ret. by wp_value_head.
iIntros (?) "H". iApply a_alloc_spec.
iApply awp_ret. by iApply wp_value.
Qed.
Lemma a_store_ret (l:loc) (e: expr) `{Closed [] e} R Φ :
awp e R (λ w, v, l U v (l L w - Φ w)) -
awp e R (λ w, v, l C v (l C[LLvl] w - Φ w)) -
awp (a_store (a_ret #l) e) R Φ.
Proof.
iIntros "H".
iApply ((a_store_spec _ _
(λ l1, l1 = l)%I
(λ w, v, (l U v (l L w - Φ w)))%I ) with "[] [H] []").
(λ w, v, (l C v (l C[LLvl] w - Φ w)))%I ) with "[] [H] []").
- iApply awp_ret; iApply wp_value; eauto.
- done.
- iNext. iIntros (? w) "-> H". eauto with iFrame.
......@@ -43,14 +43,14 @@ Section derived.
Ltac awp_alloc_ret r h := iApply a_alloc_ret; iIntros (r) h; awp_lam.
Lemma awp_bin_op_load_load op (l r : loc) (v1 v2: val) R Φ :
l U v1 - r U v2 -
(l U v1 - r U v2 - w : val, bin_op_eval op v1 v2 = Some w Φ w) -
l C v1 - r C v2 -
(l C v1 - r C v2 - w : val, bin_op_eval op v1 v2 = Some w Φ w) -
awp (a_bin_op op (a_load (a_ret #l)) (a_load (a_ret #r))) R Φ.
Proof.
iIntros "Hl Hr HΦ".
iApply (a_bin_op_spec _ _
(λ x, x = v1 l U v1 )%I
(λ x, x = v2 r U v2)%I with "[Hl] [Hr] [HΦ]").
(λ x, x = v1 l C v1 )%I
(λ x, x = v2 r C v2)%I with "[Hl] [Hr] [HΦ]").
- awp_load_ret l.
- awp_load_ret r.
- iNext. iIntros (??) "[-> Hl] [-> Hr]".
......@@ -58,7 +58,7 @@ Section derived.
Qed.
Lemma a_move_spec (s t :loc) (v w: val) R Φ :
s U v t U w ( t U w - s L w - Φ w) -
s C v t C w (t C w - s C[LLvl] w - Φ w) -
awp (a_store (a_ret #s) (a_load (a_ret #t))) R Φ.
Proof.
iIntros "(Hs & Ht & H)".
......@@ -72,7 +72,7 @@ Section derived.
( a, Ψ a - U (awp (ef a) R Φ)) -
awp (a_invoke ef ea) R Φ.
Proof.
iIntros (<-%of_to_val) "Ha Hfa".
iIntros (?) "Ha Hfa".
iApply (a_invoke_spec _ _ R with "Ha").
iIntros (a) "HΨ".
iSpecialize ("Hfa" with "HΨ"). iModIntro.
......@@ -84,19 +84,18 @@ Section derived.
Lemma a_invoke_full (ef ea : expr) R Ψ Φ (f : val) :
IntoVal ef f
awp ea R Ψ -
( a, Ψ a - U (R - awp (ef a) True%I (λ v, R Φ v))) -
( a, Ψ a - U (R - awp (ef a) True (λ v, R Φ v))) -
awp (a_invoke ef ea) R Φ.
Proof.
iIntros (<-%of_to_val) "Ha Hfa".
iIntros (?) "Ha Hfa".
iApply (a_invoke_spec _ _ R with "Ha").
iIntros (a) "HΨ".
iSpecialize ("Hfa" with "HΨ"). iModIntro.
iIntros "HR".
iExists True%I. rewrite bi.True_sep'.
iExists True%I. iSplit; first done.
iSpecialize ("Hfa" with "HR").
iApply (awp_wand with "Hfa"). eauto with iFrame.
Qed.
End derived.
Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
......
......@@ -57,7 +57,7 @@ Section a_wp.
set_Forall (λ v, l : loc, v = #l l preσ) X.
Definition env_inv (env : val) : iProp Σ :=
( (X : gset val) (σ : gmap loc level),
( (X : gset val) (σ : gmap loc lvl),
is_set_mut env X
full_locking_heap σ
([ map] l _ σ, v', l {1/2} v')
......@@ -77,29 +77,29 @@ Section a_wp.
(awp e R Φ) (awp e R Φ).
Proof.
iIntros (P R _) "[HP HA]".
rewrite /awp /tc_opaque.
destruct p; simpl;
[ iDestruct "HP" as "#HP" | ];
iMod "HP"; by iApply "HA".
rewrite /awp /tc_opaque /= bi.intuitionistically_if_elim.
iMod "HP". by iApply "HA".
Qed.
End a_wp.
Section a_wp_rules.
Context `{amonadG Σ}.
Lemma a_wp_awp R Φ Ψ e : awp e R Φ - ( v : val, awp v R Φ - Ψ v) - WP e {{ Ψ }}.
Lemma a_wp_awp R Φ Ψ e :
awp e R Φ -
( v : val, awp v R Φ - Ψ v) -
WP e {{ Ψ }}.
Proof.
iIntros "Hwp H". rewrite /awp /=. iApply (wp_wand with "Hwp").
iIntros (v) "Hwp". iApply "H". by iApply wp_value'.
Qed.
Lemma wp_awp_bind R Φ K e :
WP e {{ v, awp (fill K (of_val v)) R Φ }} awp (fill K e) R Φ.
WP e {{ v, awp (fill K (of_val v)) R Φ }} - awp (fill K e) R Φ.
Proof. by apply: wp_bind. Qed.
Lemma wp_awp_bind_inv R Φ K e :
awp (fill K e) R Φ WP e {{ v, awp (fill K (of_val v)) R Φ }}.
awp (fill K e) R Φ - WP e {{ v, awp (fill K (of_val v)) R Φ }}.
Proof. by apply: wp_bind_inv. Qed.
Lemma awp_insert_res e Φ R1 R2 :
......@@ -155,7 +155,7 @@ Section a_wp_rules.
awp e R (λ ev, awp (f ev) R Φ) -
awp (a_bind f e) R Φ.
Proof.
iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iIntros ([fv <-]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_bind (ev env l).
iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
......@@ -168,7 +168,7 @@ Section a_wp_rules.
(R - R', R' awp (ev #()) R' (λ w, R' - R Φ w)) -
awp (a_atomic e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
iIntros (<-) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
iIntros (γ π env l) "#Hlock1 #Hres Hunfl1". do 2 wp_let.
wp_apply (acquire_cancel_spec with "[$]").
iIntros (f) "([Henv HR] & Hcl)". wp_seq.
......@@ -194,7 +194,7 @@ Section a_wp_rules.
WP ev env {{ w, env_inv env R Φ w }}) -
awp (a_atomic_env e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
iIntros (<-) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam.
wp_apply (acquire_cancel_spec with "[$]").
iIntros (f) "([Henv HR] & Hcl)". wp_seq.
......@@ -236,7 +236,7 @@ Section a_wp_run.
R - ( `{amonadG Σ}, awp e R (λ w, R ={}= Φ w)) -
WP a_run e {{ Φ }}.
Proof.
iIntros ([ev <-%of_to_val]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
iIntros ([ev <-]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "Henv". wp_let.
iMod (locking_heap_init ) as (?) "Hσ".
......
......@@ -57,7 +57,7 @@ Section proofs.
Context `{amonadG Σ}.
Lemma a_alloc_spec R Φ e :
awp e R (λ v, l, l U v - Φ #l) -
awp e R (λ v, l, l C v - Φ #l) -
awp (a_alloc e) R Φ.
Proof.
iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
......@@ -71,7 +71,7 @@ Section proofs.
iDestruct "Hlocks" as %Hlocks.
iApply wp_fupd.
wp_let. wp_alloc l as "Hl".
iAssert (⌜σ !! l = None)%I with "[Hl Hls]" as %Hl.
iAssert ⌜σ !! l = None%I with "[Hl Hls]" as %Hl.
{ remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
iDestruct "Hls" as (v') "Hl'".
......@@ -89,7 +89,7 @@ Section proofs.
awp e1 R (λ v, l : loc, v = #l Ψ1 l)-
awp e2 R Ψ2 -
( (l : loc) w,
Ψ1 l - Ψ2 w - ( v, l U v (l L w - Φ w))) -
Ψ1 l - Ψ2 w - ( v, l C v (l C[LLvl] w - Φ w))) -
awp (a_store e1 e2) R Φ.
Proof.
iIntros "H1 H2 HΦ".
......@@ -133,9 +133,8 @@ Section proofs.
iPureIntro. apply lvl_included. destruct b'; eauto.
Qed.
Lemma a_load_spec_exists_frac R Φ e :
awp e R (λ v, (l : loc) (q: frac) (w : val), v = #l l U{q} w (l U{q} w - Φ w)) -
awp e R (λ v, (l : loc) (q: frac) (w : val), v = #l l C{q} w (l C{q} w - Φ w)) -
awp (a_load e) R Φ.
Proof.
iIntros "H".
......@@ -168,7 +167,7 @@ Section proofs.
Qed.
Lemma a_load_spec R Φ q e :
awp e R (λ v, (l : loc) (w : val), v = #l l U{q} w (l U{q} w - Φ w)) -
awp e R (λ v, (l : loc) (w : val), v = #l l C{q} w (l C{q} w - Φ w)) -
awp (a_load e) R Φ.
Proof.
iIntros "H".
......@@ -240,7 +239,7 @@ Section proofs.
awp e R (λ v, U (awp (f v) R Φ)) -
awp (a_seq_bind f e) R Φ.
Proof.
iIntros ([fv <-%of_to_val]) "H". rewrite /a_seq_bind /=. awp_lam.
iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam.
awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
awp_lam. iApply awp_bind. iApply a_seq_spec.
......@@ -265,7 +264,7 @@ Section proofs.
(v = #false awp (e2 #()) R Φ)) -
awp (a_if e e1 e2) R Φ.
Proof.
iIntros ([v1 <-%of_to_val] [v2 <-%of_to_val]) "H".
iIntros ([v1 <-] [v2 <-]) "H".
awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). clear v.
iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
......@@ -277,7 +276,7 @@ Section proofs.
( a, Ψ a - U (R - R', R' (awp (ef a) R' (λ v, R' - R Φ v)))) -
awp (a_invoke ef ea) R Φ.
Proof.
iIntros (<-%of_to_val) "Ha Hfa".
rewrite /IntoVal. iIntros (<-) "Ha Hfa".
rewrite /a_invoke. awp_lam.
awp_apply (a_wp_awp R with "Ha").
iIntros (a) "Ha". awp_let.
......@@ -325,10 +324,9 @@ Section proofs.
- iLeft. iSplit; first eauto. awp_seq.
iApply a_sequence_spec. awp_seq.
iApply (awp_wand with "H").
iIntros (v) "Hi". iModIntro. awp_seq.
iIntros (v) "Hi !>". awp_seq.
by iApply ("IH" with "Hi").
Qed.
End proofs.
(* Make sure that we only use the provided rules and don't break the abstraction *)
......
......@@ -3,14 +3,14 @@ From iris.algebra Require Import frac.
From iris_c.lib Require Import locking_heap.
From iris.proofmode Require Import modalities classes.
Section contents.
Section U.
Context `{heapG Σ, locking_heapG Σ}.
(** * Unlocking modality *)
Definition U (P : iProp Σ) : iProp Σ :=
( ls : list (loc*(frac*val)),
([ list] x ls, x.1 L{x.2.1} x.2.2)
(([ list] x ls, x.1 U{x.2.1} x.2.2) - P))%I.
( ls : list (loc * (frac * val)),
([ list] x ls, x.1 C[LLvl]{x.2.1} x.2.2)
(([ list] x ls, x.1 C{x.2.1} x.2.2) - P))%I.
Lemma U_mono P Q : (P Q) U P U Q.
Proof.
......@@ -20,10 +20,7 @@ Section contents.
Qed.
Lemma U_intro P : P U P.
Proof.
iIntros "HP". iExists [].
rewrite !big_sepL_nil. eauto.
Qed.
Proof. iIntros "HP". iExists []. eauto. Qed.
(** [U] behaves like an applicative functor aka "lax functor with a strength" *)
Lemma U_sep_2 P Q : U P U Q U (P Q).
......@@ -31,12 +28,19 @@ Section contents.
iIntros "[HP HQ]".
iDestruct "HP" as (ls1) "[HP1 HP2]".
iDestruct "HQ" as (ls2) "[HQ1 HQ2]".
iExists (ls1++ls2). rewrite !big_sepL_app. iFrame.
iExists (ls1 ++ ls2). iFrame.
iIntros "[HP1 HQ1]". iSplitL "HP1 HP2".
- by iApply "HP2".
- by iApply "HQ2".
Qed.
Global Instance U_monoid_morphism : MonoidHomomorphism bi_sep bi_sep (flip ()) U.
Proof. split. split; try apply _. solve_proper. apply U_sep_2. apply U_intro. Qed.
Lemma U_big_sepL {A} (l : list A) Φ :
(([ list] ix l, U (Φ i x)) U ([ list] ix l, Φ i x))%I.
Proof. apply big_opL_commute, _. Qed.
Lemma U_stength P Q : P U Q U (P Q).
Proof. by rewrite {1}(U_intro P) U_sep_2. Qed.
......@@ -50,7 +54,7 @@ Section contents.
iApply ("HP2" with "HP1").
Qed.
Lemma U_unlock l q v : l L{q} v U (l U{q} v).
Lemma U_unlock l q v : l C[LLvl]{q} v U (l C{q} v).
Proof.
iIntros "Hl". iExists [(l,(q,v))]. iIntros "/= {$Hl} [$ _]".
Qed.
......@@ -60,7 +64,8 @@ Section contents.
Proof. rewrite /IntoUnlock. reflexivity. Qed.
Global Instance into_unlock_id P : IntoUnlock P P | 10.
Proof. apply U_intro. Qed.
Global Instance into_unlock_unlock l q v : IntoUnlock (l L{q} v)%I (l U{q} v)%I | 0.
Global Instance into_unlock_unlock l q v :
IntoUnlock (l C[LLvl]{q} v)%I (l C{q} v)%I | 0.
Proof. apply U_unlock. Qed.
Lemma modality_U_mixin :
......@@ -73,15 +78,4 @@ Section contents.
Global Instance from_modal_later P : FromModal modality_U (U P) (U P) P.
Proof. by rewrite /FromModal. Qed.
Lemma big_sepL_U {A} (l : list A) Φ :
(([ list] ix l, U (Φ i x)) U ([ list] ix l, Φ i x))%I.
Proof.
iInduction l as [|x l'] "IH" forall (Φ); simpl.
- iIntros "_"; by iModIntro.
- iIntros "[HΦ H]".
iDestruct ("IH" with "H") as "H".
iModIntro. iFrame.
Qed.
End contents.
End U.
This diff is collapsed.
......@@ -18,9 +18,8 @@ Section Sets.
match: "xs" with
NONE => #false
| SOME "p" =>
if: Fst "p" = "x"
then #true else
let: "y" := (Snd "p") in "member" "x" "y"
if: Fst "p" = "x" then #true
else let: "y" := (Snd "p") in "member" "x" "y"
end.
Definition set_add : val := λ: "x" "xs",
......@@ -98,10 +97,8 @@ Section MutableSet_wp.
{{{ True }}} mset_create #() {{{ v, RET v; is_set_mut v }}}.
Proof.
iIntros (Φ) "_ H".
wp_lam. wp_bind (newset #()).
iApply set_newset_spec; first done.
iNext. iIntros (v) "%".
wp_alloc l as "Hl". iApply "H".
wp_lam. wp_apply (set_newset_spec with "[//]").
iIntros (v ?). wp_alloc l as "Hl". iApply "H".
iExists l, v. by iFrame.
Qed.
......@@ -111,10 +108,9 @@ Section MutableSet_wp.
{{{ RET #(bool_decide (x X)); is_set_mut xs X }}}.
Proof.
iIntros (Φ) "Hmut H".
iDestruct "Hmut" as (s hd) "[% [Hs #Hset]]"; subst .
iDestruct "Hmut" as (s hd ->) "[Hs #Hset]".
wp_lam. wp_let. wp_load. wp_let.
iApply (set_member_spec with "[$Hset //]").
iNext. iIntros (v).
wp_apply (set_member_spec with "Hset"). iIntros (v).
iApply ("H" with "[Hset Hs]").
iExists s, hd. eauto.
Qed.
......@@ -126,13 +122,11 @@ Section MutableSet_wp.
mset_add xe xse
{{{ RET #() ; (is_set_mut xs ({[x]} X))}}}.
Proof.
intros ??. rewrite -(of_to_val xe x); last done. rewrite -(of_to_val xse xs); last done.
iIntros (Φ) "[Hmut %] HPost".
iIntros (<- <- Φ) "[Hmut %] HPost".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
do 2 wp_lam; wp_load; wp_let.
wp_bind (set_add x hd).
iApply (set_add_spec with "[$Hset//]").
iNext. iIntros (v) "%". wp_store. iApply "HPost".
wp_apply (set_add_spec with "[$Hset//]").
iIntros (v ?). wp_store. iApply "HPost".
iExists s, v. by iFrame.
Qed.
......@@ -143,10 +137,8 @@ Section MutableSet_wp.
Proof.
iIntros (Φ) "Hmut HPost".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
wp_lam. wp_bind (newset #()).
iApply set_newset_spec; first done.
iNext. iIntros (v) "%". wp_store.
wp_lam. wp_apply (set_newset_spec with "[//]").
iIntros (v ?). wp_store.
iApply "HPost". iExists s, v. by iFrame.
Qed.
End MutableSet_wp.
......@@ -22,19 +22,18 @@ Definition factorial : val := λ: "n",
(a_alloc (a_ret #0%V)))
(a_alloc (a_ret #1%V)).
Section factorial_spec.
Context `{amonadG Σ}.
Lemma incr_spec (l : loc) (n : Z) R Φ :
l U #n - (l L #(n+1) - Φ #(n+1)) -
l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) -
awp (incr #l) R Φ.
Proof.
iIntros "Hl HΦ".
awp_lam.
iApply (a_store_ret with "[Hl HΦ]").
iApply (a_bin_op_spec _ _
(λ v, v = #n l U #n )%I (λ v, v = #1)%I with "[Hl] [] [HΦ]").
(λ v, v = #n l C #n)%I (λ v, v = #1)%I with "[Hl] [] [HΦ]").
+ awp_load_ret l.
+ awp_ret_value.
+ iNext. iIntros (? ?) "(% & Hc) %"; subst.
......@@ -42,16 +41,16 @@ Section factorial_spec.
Qed.
Lemma factorial_body_spec (n k : nat) (c r: loc) R :
(k n c U #k r U #(fact k)) -
(k n c C[ULvl] #k r C #(fact k)) -
awp (factorial_body #n #c #r) R
(λ _, c U #n r U #(fact n))%I.
(λ _, c C #n r C #(fact n))%I.
Proof.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec. iNext.
iDestruct "Hk" as %Hk.
iApply a_if_spec.
iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc]").
(λ v, v = #k c C #k)%I (λ v, v = #n)%I with "[Hc]").
- awp_load_ret c.
- awp_ret_value.
- iNext. iIntros (v1 v2) "[% Hc] %"; subst.
......@@ -63,8 +62,8 @@ Section factorial_spec.
iIntros "Hc". iModIntro. awp_seq.
iApply (a_store_ret with "[Hr Hc]").
iApply (a_bin_op_spec _ _
(λ v, v = #(fact k) r U #(fact k))%I
(λ v, v = #(k + 1) c U #(k+1))%I with "[Hr] [Hc]").
(λ v, v = #(fact k) r C #(fact k))%I
(λ v, v = #(k + 1) c C #(k+1))%I with "[Hr] [Hc]").
* awp_load_ret r.
* awp_load_ret c.
* iNext. iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
......@@ -88,13 +87,12 @@ Section factorial_spec.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec.
iApply (awp_wand _ (λ _, c U #n r U #(fact n))%I with "[Hr Hc]").
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
awp_load_ret r.
Qed.
Lemma factorial_spec_with_inv (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
......@@ -103,11 +101,11 @@ Section factorial_spec.
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec. do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n c U #k r U #(fact k))%I with "[Hr Hc]").
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
- iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)".
iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc]").
(λ v, v = #k c C #k)%I (λ v, v = #n)%I with "[Hc]").
+ awp_load_ret c.
+ awp_ret_value.
+ iNext. iIntros (v1 v2) "[% Hc] %"; subst.
......@@ -119,8 +117,8 @@ Section factorial_spec.
iIntros "Hc". iModIntro. awp_seq.
iApply (a_store_ret with "[Hr Hc]").
iApply (a_bin_op_spec _ _
(λ v, v = #(fact k) r U #(fact k))%I
(λ v, v = #(k + 1) c U #(k+1))%I with "[Hr] [Hc]").
(λ v, v = #(fact k) r C #(fact k))%I
(λ v, v = #(k + 1) c C #(k+1))%I with "[Hr] [Hc]").
** awp_load_ret r.
** awp_load_ret c.
** iNext. iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
......
......@@ -21,12 +21,12 @@ Section gcd_spec.
Lemma gcd_spec (a b : Z) (l r: loc) R :
0 a 0 b
l U #a - r U #b -
l C #a - r C #b -
awp (gcd #l #r) R (λ v, v = #(Z.gcd a b)).
Proof.
iIntros (??) "Hl Hr". do 2 awp_lam. iApply a_sequence_spec.
iApply (a_while_inv_spec ( x y : Z,
0 x 0 y Z.gcd x y = Z.gcd a b l U #x r U #y)%I with "[Hl Hr]").
0 x 0 y Z.gcd x y = Z.gcd a b l C #x r C #y)%I with "[Hl Hr]").
- iExists a, b. eauto with iFrame.
- iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[Hl Hr]".
iApply a_un_op_spec.
......
......@@ -54,14 +54,13 @@ Definition in_place_reverse : val := λ: "hd",
(a_load (a_ret "j"))
) (a_alloc (a_ret NONEV))) (a_alloc (a_ret "hd")).
Section list_spec.
Context `{amonadG Σ}.
Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
match xs with
| [] => hd = NONEV
| x :: xs => (l:loc) hd', hd = SOMEV #l l U (x,hd') is_list hd' xs
| x :: xs => (l:loc) hd', hd = SOMEV #l l C (x,hd') is_list hd' xs
end%I.
Lemma a_list_nil_spec R Φ:
......@@ -70,8 +69,8 @@ Section list_spec.
Lemma a_list_next_spec (e: expr) R Φ :
awp e R (λ v,
(l:loc) hd x xs, v = SOMEV #l l U (x, hd) is_list hd xs
(l U (x, hd) - is_list hd xs - Φ hd)) -
(l:loc) hd x xs, v = SOMEV #l l C (x, hd) is_list hd xs
(l C (x, hd) - is_list hd xs - Φ hd)) -
awp (a_list_next e) R Φ.
Proof.
iIntros "H". rewrite/ a_list_next.
......@@ -89,10 +88,10 @@ Section in_place_reversal.
Lemma a_list_store_next_spec e1 e2 Ψ1 Ψ2 R Φ :
awp e1 R (λ v, (hd:loc) x old,
v = SOMEV #hd hd U (x, old) Ψ1 (x, SOMEV #hd)) -
v = SOMEV #hd hd C (x, old) Ψ1 (x, SOMEV #hd)) -
awp e2 R Ψ2 -
( (hd : loc) x new, Ψ1 (x, SOMEV #hd) - Ψ2 new -
(hd L (x, new) - Φ (x, new)%V)) -
(hd C[LLvl] (x, new) - Φ (x, new)%V)) -
awp (a_list_store_next e1 e2) R Φ.
Proof.
iIntros "H1 H2 HΦ".
......@@ -101,7 +100,7 @@ Section in_place_reversal.
iApply awp_bind. iApply (awp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>".
iDestruct "H1" as (hd x nxt ->) "(Hhd & HΨ1)".
do 4 awp_pure _. iApply awp_bind. awp_load_ret hd. iIntros "Hd".
do 4 awp_pure _. iApply awp_bind. awp_load_ret hd. iIntros "Hd".
awp_let. iApply a_store_ret. do 2 awp_proj; awp_ret_value.
iExists (x, nxt)%V. iFrame. iIntros "Hd".
iSpecialize ("HΦ" $! hd x with "HΨ1 H2"). by iApply "HΦ".
......@@ -115,13 +114,13 @@ Section in_place_reversal.
iApply awp_bind; awp_alloc_ret i "Hi".
iApply awp_bind; awp_alloc_ret j "Hj".
iApply a_sequence_spec.
iApply (a_while_inv_spec ( ls rs rhd hd, i U hd is_list hd ls
j U rhd is_list rhd rs (reverse rs)++ls=xs)%I with "[Hlst Hj Hi]").
iApply (a_while_inv_spec ( ls rs rhd hd, i C hd is_list hd ls
j C rhd is_list rhd rs (reverse rs)++ls=xs)%I with "[Hlst Hj Hi]").
- iExists xs, [], (InjLV #()), hd; eauto with iFrame.
- iModIntro; iIntros "H". clear hd.
iDestruct "H" as (ls rs rhd hd) "(Hi & Hls & Hj & Hrs & %)".
iApply a_un_op_spec. iApply (a_bin_op_spec _ _
(λ x, x = hd i U hd)%I (λ x, x = NONEV)%I with "[Hi] [] [-]").