Commit 426f1417 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris (Z_scope).

parent 285fe0ab
Pipeline #28854 failed with stage
in 1 minute and 26 seconds
......@@ -108,14 +108,14 @@ Section proof2.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 (E 2)) (λ _, own γ2 (E 2))
wp_apply (wp_par (λ _, own γ1 (E 2%Z)) (λ _, own γ2 (E 2%Z))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)".
wp_seq. wp_load. wp_op. wp_store.
iDestruct (ghost_var_agree with "Hγ1● Hγ1◯") as %->.
iMod (ghost_var_update γ1 2 with "Hγ1● Hγ1◯") as "[Hγ1● Hγ1◯]".
wp_apply (release_spec with "[- $Hl Hγ1◯]"); [|by auto].
iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2); [done|ring].
iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2)%Z; [done|ring].
- (* exercise *)
admit.
- (* exercise *)
......@@ -137,19 +137,19 @@ Section proof3.
Proof.
iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let.
iMod (own_alloc (F 0%nat F 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
iMod (own_alloc (F 0 F 0)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
{ by apply auth_both_valid. }
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ (F{1/2} 2%nat)) (λ _, own γ (F{1/2} 2%nat))
wp_apply (wp_par (λ _, own γ (F{1/2} 2)) (λ _, own γ (F{1/2} 2))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store.
iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2)%nat with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]".
iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2) with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]".
{ rewrite (comm plus).
by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. }
by apply frac_auth_update, (op_local_update_discrete n 0 2). }
wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto].
iExists _. iFrame. by rewrite Nat2Z.inj_add.
- (* exercise *)
......
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl18.git"
synopsis: "The Iris tutorial at POPL 2018"
depends: [
"coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
"coq-iris" { (= "dev.2020-05-29.0.d5f678ee") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -111,14 +111,14 @@ Section proof2.
wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]").
{ (* exercise *) iExists 0, 0. iFrame. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 (E 2)) (λ _, own γ2 (E 2))
wp_apply (wp_par (λ _, own γ1 (E 2%Z)) (λ _, own γ2 (E 2%Z))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)".
wp_seq. wp_load. wp_op. wp_store.
iDestruct (ghost_var_agree with "Hγ1● Hγ1◯") as %->.
iMod (ghost_var_update γ1 2 with "Hγ1● Hγ1◯") as "[Hγ1● Hγ1◯]".
wp_apply (release_spec with "[- $Hl Hγ1◯]"); [|by auto].
iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2); [done|ring].
iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2)%Z; [done|ring].
- (* exercise *)
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)".
wp_seq. wp_load. wp_op. wp_store.
......@@ -150,26 +150,26 @@ Section proof3.
Proof.
iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let.
iMod (own_alloc (F 0%nat F 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
iMod (own_alloc (F 0 F 0)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
{ by apply auth_both_valid. }
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *) iExists 0%nat. iFrame. }
{ (* exercise *) iExists 0. iFrame. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ (F{1/2} 2%nat)) (λ _, own γ (F{1/2} 2%nat))
wp_apply (wp_par (λ _, own γ (F{1/2} 2)) (λ _, own γ (F{1/2} 2))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store.
iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2)%nat with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]".
iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2) with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]".
{ rewrite (comm plus).
by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. }
by apply frac_auth_update, (op_local_update_discrete n 0 2). }
wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto].
iExists _. iFrame. by rewrite Nat2Z.inj_add.
- (* exercise *)
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store.
iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2)%nat with "Hγ● Hγ2◯") as "[Hγ● Hγ2◯]".
iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2) with "Hγ● Hγ2◯") as "[Hγ● Hγ2◯]".
{ rewrite (comm plus).
by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. }
by apply frac_auth_update, (op_local_update_discrete n 0 2). }
wp_apply (release_spec with "[- $Hl Hγ2◯]"); [|by auto].
iExists _. iFrame. by rewrite Nat2Z.inj_add.
- (* exercise *)
......
......@@ -68,7 +68,7 @@ Section proof.
end)%I.
Lemma parallel_add_mul_spec :
{{{ True }}} parallel_add_mul {{{ z, RET #z; z = 2 z = 4 }}}.
{{{ True }}} parallel_add_mul {{{ z, RET #z; z = 2%Z z = 4%Z }}}.
Proof.
iIntros (Φ) "_ Post".
unfold parallel_add_mul. wp_alloc r as "Hr". wp_let.
......
......@@ -48,7 +48,7 @@ Proof.
iIntros "Hl". wp_lam.
wp_apply (strange_inc_spec with "Hl"); iIntros "Hl"; wp_seq.
wp_apply (strange_inc_spec with "Hl"); iIntros "Hl".
rewrite (_ : 2 + x = 1 + (1 + x)); last lia. auto.
rewrite (_ : 2 + x = 1 + (1 + x))%Z; last lia. auto.
Qed.
Lemma strange_inc_twice_spec `{heapG Σ} l (x : Z) :
......@@ -57,5 +57,5 @@ Proof.
iIntros (Φ) "Hl Post". wp_lam.
wp_apply (strange_inc_spec with "Hl"); iIntros "Hl"; wp_seq.
wp_apply (strange_inc_spec with "Hl"); iIntros "Hl".
iApply "Post". rewrite (_ : 2 + x = 1 + (1 + x)); last lia. done.
iApply "Post". rewrite (_ : 2 + x = 1 + (1 + x))%Z; last lia. done.
Qed.
......@@ -9,7 +9,7 @@ Definition coin_flip : val := λ: <>,
!"l".
Lemma test2_spec `{heapG Σ, spawnG Σ} :
{{{ True }}} coin_flip #() {{{ n, RET #n; n = 0 n = 1 }}}.
{{{ True }}} coin_flip #() {{{ n, RET #n; n = 0%Z n = 1%Z }}}.
Proof.
iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
iMod (inv_alloc N _
......
......@@ -63,7 +63,7 @@ Section proof2.
Lemma frac_auth_update n n1 n2 q γ :
own γ (F n1) -
own γ (F{q} n2) - |==>
own γ (F (n1 + n)%nat) own γ (F{q} (n2 + n)%nat).
own γ (F (n1 + n)) own γ (F{q} (n2 + n)).
Proof.
iIntros "H H'". iMod (own_update_2 with "H H'") as "[$ $]"; last done.
apply frac_auth_update, nat_local_update. lia.
......@@ -84,27 +84,27 @@ Section proof2.
Lemma par_inc_FAA_spec n n' γ l q :
{{{ inv N (proof2_inv γ l) own γ (F{q} n) }}}
FAA #l #n'
{{{ m, RET #m; own γ (F{q} (n + n'))%nat }}}.
{{{ m, RET #m; own γ (F{q} (n + n')) }}}.
Proof.
iIntros (Φ) "[#Hinv Hγ] Post". iInv N as (m) ">[Hauth Hl]" "Hclose".
wp_faa.
iMod (frac_auth_update n' with "Hauth Hγ") as "[Hauth Hγ]".
iMod ("Hclose" with "[Hauth Hl]") as "_".
{ iNext; iExists (m + n')%nat. rewrite Nat2Z.inj_add. iFrame. }
{ iNext; iExists (m + n'). rewrite Nat2Z.inj_add. iFrame. }
by iApply "Post".
Qed.
(* Proof of the whole program *)
Lemma par_inc_spec :
{{{ True }}} par_inc #() {{{ RET #4%nat; True }}}.
{{{ True }}} par_inc #() {{{ RET #4; True }}}.
Proof.
iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
iMod (frac_auth_alloc 0) as (γ) "[Hauth Hγ]".
iDestruct "Hγ" as "[Hγ1 Hγ2]".
iMod (inv_alloc _ _ (proof2_inv γ l) with "[Hl Hauth]") as "#Hinv".
{ iNext. iExists 0%nat. iFrame. }
wp_apply (wp_par (λ _, own γ (F{1/2} 2%nat))
(λ _, own γ (F{1/2} 2%nat)) with "[Hγ1] [Hγ2]").
{ iNext. iExists 0. iFrame. }
wp_apply (wp_par (λ _, own γ (F{1/2} 2))
(λ _, own γ (F{1/2} 2)) with "[Hγ1] [Hγ2]").
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- iIntros (v1 v2) "[Hγ1 Hγ2] !>". iCombine "Hγ1 Hγ2" as "Hγ". simpl.
......@@ -112,14 +112,14 @@ Section proof2.
iDestruct (frac_auth_agree with "Hauth Hγ") as %->.
wp_load.
iMod ("Hclose" with "[Hauth Hx]") as "_".
{ iNext. iExists 4%nat. iFrame. }
{ iNext. iExists 4. iFrame. }
by iApply "Post".
Qed.
Lemma par_incN_helper_spec n γ l q :
{{{ inv N (proof2_inv γ l) own γ (F{q} 0%nat) }}}
{{{ inv N (proof2_inv γ l) own γ (F{q} 0) }}}
par_incN_helper #n #l
{{{ v, RET v; own γ (F{q} (n * 2))%nat }}}.
{{{ v, RET v; own γ (F{q} (n * 2)) }}}.
Proof.
iIntros (Φ) "[#? Hγ] Post /=".
iInduction n as [|n] "IH" forall (q Φ).
......@@ -127,8 +127,8 @@ Section proof2.
rewrite Nat2Z.inj_succ. wp_lam. wp_pures.
case_bool_decide; first (simplify_eq/=; lia). wp_if.
iDestruct "Hγ" as "[Hγ1 Hγ2]".
wp_apply (wp_par (λ _, own γ (F{q/2} 2%nat))
(λ _, own γ (F{q/2} (n * 2)%nat)) with "[Hγ1] [Hγ2]").
wp_apply (wp_par (λ _, own γ (F{q/2} 2))
(λ _, own γ (F{q/2} (n * 2))) with "[Hγ1] [Hγ2]").
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- wp_op. rewrite (_ : Z.succ n - 1 = n)%Z; last lia.
iApply ("IH" with "Hγ2"); auto.
......@@ -142,14 +142,14 @@ Section proof2.
iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
iMod (frac_auth_alloc 0) as (γ) "[Hauth Hγ]".
iMod (inv_alloc _ _ (proof2_inv γ l) with "[Hl Hauth]") as "#Hinv".
{ iNext. iExists 0%nat. iFrame. }
{ iNext. iExists 0. iFrame. }
wp_apply (par_incN_helper_spec with "[$]").
iIntros (v) "Hγ". wp_seq.
iInv N as (m) ">[Hauth Hx]" "Hclose".
iDestruct (frac_auth_agree with "Hauth Hγ") as %->.
wp_load.
iMod ("Hclose" with "[Hauth Hx]") as "_".
{ iNext. iExists (n * 2)%nat. iFrame. }
{ iNext. iExists (n * 2). iFrame. }
by iApply "Post".
Qed.
End proof2.
Supports Markdown
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