Commit e738e7a0 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (Z scope).

parent c962f679
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-05-26.1.d80e7abf") | (= "dev") }
"coq-iris" { (= "dev.2020-05-28.2.2643cb7d") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
"coq-iris-string-ident"
]
......
......@@ -380,7 +380,7 @@ Section contents.
- iNext. by iApply runner_runTasks_spec.
- iNext. wp_seq. wp_op.
(* Set Printing Coercions. *)
assert ((Z.of_nat i + 1) = Z.of_nat (i + 1)) as -> by lia.
assert ((Z.of_nat i + 1)%Z = Z.of_nat (i + 1)) as -> by lia.
iApply ("IH" with "HΦ").
Qed.
......
......@@ -42,16 +42,16 @@ Section contents.
iLöb as "IH" forall (n Φ).
wp_rec. simpl. wp_op. case_bool_decide; simplify_eq; wp_if.
{ assert (n = O) as -> by lia.
by iApply ("HΦ" $! 1%nat). }
by iApply ("HΦ" $! 1). }
wp_op. case_bool_decide; simplify_eq; wp_if.
{ assert (n = 1%nat) as -> by lia.
by iApply ("HΦ" $! 1%nat). }
{ assert (n = 1) as -> by lia.
by iApply ("HΦ" $! 1). }
wp_op. destruct n as [|[|n]]=> //.
rewrite !Nat2Z.inj_succ.
replace (Z.succ (Z.succ n) - 2) with (Z.of_nat n) by lia.
replace (Z.succ (Z.succ n) - 2)%Z with (Z.of_nat n) by lia.
wp_apply "IH". iIntros (? <-).
wp_op.
replace (Z.succ (Z.succ n) - 1) with (Z.of_nat (S n)) by lia.
replace (Z.succ (Z.succ n) - 1)%Z with (Z.of_nat (S n)) by lia.
wp_apply "IH". iIntros (? <-). wp_op.
rewrite -Nat2Z.inj_add. by iApply "HΦ".
Qed.
......@@ -84,8 +84,8 @@ Section contents.
- do 2 (wp_op; wp_let).
destruct n as [|[|n]]=> //.
rewrite !Nat2Z.inj_succ.
replace (Z.succ (Z.succ n) - 2) with (Z.of_nat n) by lia.
replace (Z.succ (Z.succ n) - 1) with (Z.succ n) by lia.
replace (Z.succ (Z.succ n) - 2)%Z with (Z.of_nat n) by lia.
replace (Z.succ (Z.succ n) - 1)%Z with (Z.succ n) by lia.
wp_apply (runner_Fork_spec).
{ iFrame "Hrunner". iExists (S n). by rewrite Nat2Z.inj_succ. }
iIntros (γ1 γ1' t1) "Ht1". wp_let.
......
......@@ -16,14 +16,14 @@ Proof. solve_inG. Qed.
Section ccounter.
Context `{!heapG Σ, !cntG Σ, !ccounterG Σ} (N : namespace).
Lemma ccounterRA_valid (m n : natR) (q : frac): (F m F{q} n) (n m)%nat.
Lemma ccounterRA_valid (m n : natR) (q : frac): (F m F{q} n) n m.
Proof.
intros ?.
(* This property follows directly from the generic properties of the relevant RAs. *)
by apply nat_included, (frac_auth_included_total q).
Qed.
Lemma ccounterRA_valid_full (m n : natR): (F m F n) (n = m)%nat.
Lemma ccounterRA_valid_full (m n : natR): (F m F n) n = m.
Proof.
by intros ?%frac_auth_agree.
Qed.
......@@ -41,7 +41,7 @@ Section ccounter.
(** The main proofs. *)
Lemma is_ccounter_op γ₁ γ₂ q1 q2 (n1 n2 : nat) :
is_ccounter γ₁ γ₂ (q1 + q2) (n1 + n2)%nat is_ccounter γ₁ γ₂ q1 n1 is_ccounter γ₁ γ₂ q2 n2.
is_ccounter γ₁ γ₂ (q1 + q2) (n1 + n2) is_ccounter γ₁ γ₂ q1 n1 is_ccounter γ₁ γ₂ q2 n2.
Proof.
apply bi.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
- iIntros "[? #?]".
......@@ -53,12 +53,12 @@ Section ccounter.
Lemma newcounter_contrib_spec (R : iProp Σ) m:
{{{ True }}}
newcounter #m
{{{ γ₁ γ₂ , RET #; is_ccounter γ₁ γ₂ 1 m%nat }}}.
{{{ γ₁ γ₂ , RET #; is_ccounter γ₁ γ₂ 1 m }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
wp_apply newcounter_spec; auto.
iIntros () "H"; iDestruct "H" as (γ₂) "[#HCnt Hown]".
iMod (own_alloc (F m%nat F m%nat)) as (γ₁) "[Hγ Hγ']"; first by apply auth_both_valid.
iMod (own_alloc (F m F m)) as (γ₁) "[Hγ Hγ']"; first by apply auth_both_valid.
iMod (inv_alloc (N .@ "counter") _ (ccounter_inv γ₁ γ₂) with "[Hγ Hown]").
{ iNext. iExists _. by iFrame. }
iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
......@@ -91,10 +91,11 @@ Section ccounter.
Lemma read_contrib_spec γ₁ γ₂ q n :
{{{ is_ccounter γ₁ γ₂ q n }}}
read #
{{{ (c : Z), RET #c; Z.of_nat n c is_ccounter γ₁ γ₂ q n }}}.
{{{ (c : Z), RET #c; (Z.of_nat n c)%Z is_ccounter γ₁ γ₂ q n }}}.
Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
wp_apply (read_spec N γ₂ _ (own γ₁ (F{q} n))%I (λ m, n m (own γ₁ (F{q} n)))%I with "[] [Hown]"); first set_solver.
wp_apply (read_spec N γ₂ _ (own γ₁ (F{q} n))%I (λ m,
(n m)%Z (own γ₁ (F{q} n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->.
......
......@@ -69,13 +69,13 @@ Section proof.
and we make it an Iris assertion by using ⌜ ... ⌝. Semantically, the
embedding is such that the embedded assertion either holds for all
resources, or none. *)
Definition incr_inv ( : loc) (n : Z) : iProp := ( (m : Z), n m #m)%I.
Definition incr_inv ( : loc) (n : Z) : iProp := ( (m : Z), (n m)%Z #m)%I.
(** The main proofs. *)
(* As in example 7.5 in the notes we will show the following specification.
The specification is parametrized by any location ℓ and natural number n *)
Lemma parallel_incr_spec ( : loc) (n : Z):
{{{ #n }}} (incr ) ||| (incr ) ;; !# {{{m, RET #m; n m }}}.
{{{ #n }}} (incr ) ||| (incr ) ;; !# {{{m, RET #m; (n m)%Z }}}.
Proof.
(* We first unfold the triple notation. Recall its definition from Section 9
of the lecture notes. *)
......@@ -202,7 +202,7 @@ Section proof.
iInv N as (k) ">[% Hpt]" "Hclose".
wp_store.
iMod ("Hclose" with "[Hpt]") as "_".
{ iNext; iExists (m+1); iFrame; iIntros "!%"; lia. }
{ iNext; iExists (m+1)%Z; iFrame; iIntros "!%"; lia. }
(* And we are left with proving |={T}=> True, which is trivial. *)
done.
+ (* The second thread is exactly the same as the first, so the proof is
......@@ -221,7 +221,7 @@ Section proof.
iInv N as (k) ">[% Hpt]" "Hclose".
wp_store.
iMod ("Hclose" with "[Hpt]") as "_"; last done.
{ iExists (m+1); iFrame; iIntros "!%"; lia. }
{ iExists (m+1)%Z; iFrame; iIntros "!%"; lia. }
+ (* And the last goal is before us. We first simplify to get rid of
superflous assumptions and variables. As above, the pattern _ means
ignore this assumption. It is always safe to ignore True as an
......
......@@ -98,20 +98,20 @@ Section factorial_client.
| S n' => S n' * factorial n'
end.
Lemma factorial_spec_S (n : nat) : factorial (S n) = ((S n) * factorial n)%nat.
Lemma factorial_spec_S (n : nat) : factorial (S n) = (S n) * factorial n.
Proof.
reflexivity.
Qed.
Definition fac_int (x : Z) := Z.of_nat (factorial (Z.to_nat x)).
Lemma fac_int_eq_0: fac_int 0 = 1.
Lemma fac_int_eq_0: fac_int 0 = 1%Z.
Proof.
reflexivity.
Qed.
Lemma fac_int_eq (x : Z):
1 x fac_int x = fac_int (x - 1) * x.
(1 x)%Z fac_int x = (fac_int (x - 1) * x)%Z.
Proof.
intros ?.
rewrite Z.mul_comm.
......@@ -147,7 +147,7 @@ Section factorial_client.
wp_bind ((times _) _).
iApply "IH"; iNext.
wp_binop; first
by replace (m + ((n - 1) * m)) with (n * m) by lia.
by replace (m + ((n - 1) * m))%Z with (n * m)%Z by lia.
Qed.
Lemma times_spec (n m : Z):
......@@ -175,13 +175,13 @@ Section factorial_client.
(* Finally, here is the specification that our implementation of factorial
really does implement the mathematical factorial function. *)
Lemma myfac_spec (n: Z):
(0 n)
(0 n)%Z
{{{ True }}}
myfac #n
{{{ v, RET v; v = #(fac_int n) }}}.
Proof.
iIntros (Hleq Φ) "_ ret"; simplify_eq. unfold myfac. wp_pures.
iApply (myrec_spec (fun v => m' : Z, 0 m' to_val v = Some #m'%I)
iApply (myrec_spec (fun v => m' : Z, (0 m')%Z to_val v = Some #m'%I)
(fun u => fun v => m' : Z, to_val v = Some #m' u = #(fac_int m')%I)).
- iSplit; last eauto. iIntros (f v). iAlways. iIntros (Φ') "spec_f ret".
wp_lam. wp_let. iDestruct "spec_f" as "[spec_f %]".
......@@ -193,7 +193,7 @@ Section factorial_client.
wp_binop. wp_bind (f _ )%E.
iApply ("spec_f" $! (#(m'-1))).
* iIntros "!%".
exists (m'-1); split; first lia; last auto.
exists (m'-1)%Z; split; first lia; last auto.
* iNext. iIntros (u) "**". destruct a as [x [Heq ->]].
iApply times_spec; first done.
iNext; iIntros (u) "%"; subst; iApply "ret".
......
......@@ -186,7 +186,7 @@ Section conditional_counter.
Definition pau P Q γs f :=
( P - AU << (b : bool) (n : Z), counter_content γs n f _(λ _, True) #b >> @ ∖↑N∖↑inv_heapN,
<< counter_content γs (if b then n + 1 else n) f _(λ _, True) #b, COMM Q >>)%I.
<< counter_content γs (if b then n + 1 else n)%Z f _(λ _, True) #b, COMM Q >>)%I.
Definition counter_inv γ_n c :=
( (l : loc) (q : Qp) (s : abstract_state),
......@@ -385,7 +385,7 @@ Section conditional_counter.
wp_load.
iMod ("Hfclose" with "[//] Hf") as "[Hf Hfclose]".
iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
iMod (update_counter_value _ _ _ (if b then n2 + 1 else n2) with "Hn● Hn◯")
iMod (update_counter_value _ _ _ (if b then n2 + 1 else n2)%Z with "Hn● Hn◯")
as "[Hn● Hn◯]".
iMod ("Hclose" with "[Hn◯ Hf]") as "Q"; first by iFrame.
iModIntro. iMod "Hfclose" as "_".
......@@ -431,7 +431,7 @@ Section conditional_counter.
is_counter γs v -
<<< (b : bool) (n : Z), counter_content γs n f _(λ _, True) #b >>>
cinc v #f @∖↑N∖↑inv_heapN
<<< counter_content γs (if b then n + 1 else n) f _(λ _, True) #b, RET #() >>>.
<<< counter_content γs (if b then n + 1 else n)%Z f _(λ _, True) #b, RET #() >>>.
Proof.
iIntros "#InvC". iDestruct "InvC" as (c_l [-> ?]) "[#GC #InvC]".
iIntros (Φ) "AU". iLöb as "IH".
......@@ -499,7 +499,7 @@ Section conditional_counter.
iIntros (?) "#GC". iIntros (Φ) "!# _ HΦ". wp_lam. wp_apply wp_fupd.
wp_alloc l_n as "Hl_n".
wp_alloc l_c as "Hl_c".
iMod (own_alloc ( Excl' 0 Excl' 0)) as (γ_n) "[Hn● Hn◯]".
iMod (own_alloc ( Excl' 0%Z Excl' 0%Z)) as (γ_n) "[Hn● Hn◯]".
{ by apply auth_both_valid. }
iMod (inv_alloc counterN _ (counter_inv γ_n l_c)
with "[Hl_c Hl_n Hn●]") as "#InvC".
......
......@@ -33,7 +33,7 @@ Record atomic_cinc {Σ} `{!heapG Σ} := AtomicCinc {
is_counter N γs v -
<<< (b : bool) (n : Z), counter_content γs n f _(λ _, True) #b >>>
cinc v #f @∖↑N∖↑inv_heapN
<<< counter_content γs (if b then n + 1 else n) f _(λ _, True) #b, RET #() >>>;
<<< counter_content γs (if b then n + 1 else n)%Z f _(λ _, True) #b, RET #() >>>;
get_spec N γs v:
is_counter N γs v -
<<< (n : Z), counter_content γs n >>>
......
This diff is collapsed.
......@@ -248,8 +248,8 @@ Section atomic_snapshot.
(* close invariant *)
iModIntro. iSplitR "HΦ".
+ iNext. rewrite /snapshot_inv.
set (<[ v'' + 1 := x2]> T) as T'.
iExists 1%Qp, l1'new, T', x2, (v'' + 1).
set (<[ (v'' + 1)%Z := x2]> T) as T'.
iExists 1%Qp, l1'new, T', x2, (v'' + 1)%Z.
iFrame.
iPureIntro. split.
* apply: lookup_insert.
......@@ -365,11 +365,11 @@ Section atomic_snapshot.
iIntros (vs') "[Eq _]"; iDestruct "Eq" as %->; wp_seq; wp_if.
+ inversion H; subst; clear H. wp_pures.
assert (v_x2 = v_y) as ->. {
assert (v_x2 <= v_y) as vneq. {
assert (v_x2 v_y)%Z as vneq. {
apply Hdom_y.
eapply (iffRL (elem_of_dom T_y _)). eauto using mk_is_Some.
}
assert (v_y <= v_x2) as vneq'. {
assert (v_y v_x2)%Z as vneq'. {
apply Hdom_x2.
eapply (iffRL (elem_of_dom T_x2 _)). eauto using mk_is_Some.
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment