Commit 44f9e668 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (Z_scope).

parent 44dd07c4
Pipeline #28784 failed with stage
in 10 minutes and 57 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
"coq-iris" { (= "dev.2020-05-28.2.2643cb7d") | (= "dev") }
]
......@@ -251,7 +251,7 @@ Section proofs.
CWP e1 @ R {{ Ψ1 }} -
CWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - n : nat,
v1 = #n n 0%nat
v1 = #n n 0
cl, block_info cl true n - cl C replicate n v2 - Φ (cloc_to_val cl)) -
CWP alloc(e1, e2) @ R {{ Φ }}.
Proof.
......
......@@ -29,13 +29,13 @@ Section factorial_spec.
iApply (cwp_wand _ (λ _, c C #n r C #(fact n))%I with "[-]"); last first.
{ iIntros (?) "[Hc Hr]". vcg_continue. eauto with iFrame. }
iAssert ( k : nat, k n c C #k r C #(fact k))%I with "[-]" as (k Hk) "[??]".
{ iExists 0%nat. eauto with lia iFrame. }
{ iExists 0. eauto with lia iFrame. }
iLöb as "IH" forall (n k Hk). iApply cwp_whileV; iNext.
vcg. iIntros "**". case_bool_decide.
+ iLeft. iSplit; eauto. iModIntro. vcg.
iIntros "Hc Hr $ !> !>". iApply (inc_spec with "Hc"); iIntros "Hc".
vcg_continue. iIntros "Hc Hr !>".
assert (fact k * S k = fact (S k)) as -> by (simpl; lia).
assert (fact k * S k = fact (S k))%Z as -> by (simpl; lia).
iApply ("IH" $! n (S k) with "[%] Hc Hr"). lia.
+ iRight. iSplit; eauto. iModIntro.
assert (k = n) as -> by lia. by iFrame.
......
......@@ -29,13 +29,13 @@ Section gcd_spec.
Context `{cmonadG Σ}.
Lemma gcd_spec l r a b R :
0 a 0 b
(0 a)%Z (0 b)%Z
l C #a - r C #b -
CWP gcd (cloc_to_val l, cloc_to_val r)%V @ R {{ v, v = #(Z.gcd a b) }}.
Proof.
iIntros (??) "**". iApply cwp_fun; simpl. vcg; iIntros.
iApply (cwp_whileV_inv ( x y : Z,
0 x 0 y Z.gcd x y = Z.gcd a b l C #x r C #y)%I with "[-]").
(0 x)%Z (0 y)%Z Z.gcd x y = Z.gcd a b l C #x r C #y)%I with "[-]").
{ iExists a, b. eauto with iFrame. }
iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[??]". vcg. iIntros "** /=".
case_bool_decide; simpl; [iLeft | iRight]; iSplit; eauto.
......@@ -44,9 +44,9 @@ Section gcd_spec.
+ iModIntro. iApply cwp_if. vcg. iIntros "** /=".
case_bool_decide; simpl; [ iLeft | iRight ];
(iSplit; first done); iModIntro.
* vcg. iIntros "** !>". iExists x, (y - x); iFrame.
* vcg. iIntros "** !>". iExists x, (y - x)%Z; iFrame.
iPureIntro. rewrite Z.gcd_sub_diag_r. lia.
* vcg. iIntros "** !>". iExists (x-y), y; iFrame.
* vcg. iIntros "** !>". iExists (x - y)%Z, y; iFrame.
iPureIntro. rewrite Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. lia.
Qed.
......
......@@ -22,22 +22,22 @@ Section par_inc.
CWP par_inc (cloc_to_val cl) @ R {{ v, v = #2 cl C #(2 + n) }}.
Proof.
iIntros "Hl". iApply cwp_fun; simpl.
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|].
set (par_inc_inv := ( n' : nat, cl C #(n' + n) own γ (F n'))%I).
iApply (cwp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
{ iExists 0%nat. iFrame. }
iAssert ( (own γ (F{1 / 2} 0%nat) -
{ iExists 0. iFrame. }
iAssert ( (own γ (F{1 / 2} 0) -
CWP call (c_ret inc) (c_ret (cloc_to_val cl)) @ par_inc_inv R
{{ v, v = #1 own γ (F{1 / 2} 1%nat) }}))%I as "#H".
{{ v, v = #1 own γ (F{1 / 2} 1) }}))%I as "#H".
{ iIntros "!> Hγ'". vcg; iIntros "[HR $] !> !>". iDestruct "HR" as (n') "[Hl Hγ]".
iApply cwp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl".
iMod (own_update_2 with "Hγ Hγ'") as "[Hγ Hγ']".
{ apply frac_auth_update, (nat_local_update _ _ (S n') 1); lia. }
iModIntro. iSplitL "Hl Hγ"; last vcg_continue; eauto.
iExists (S n'). rewrite Nat2Z.inj_succ -Z.add_1_l -Z.add_assoc. iFrame. }
iApply (cwp_bin_op _ _ (λ v, v = #1 own γ (F{1 / 2} 1%nat))%I
(λ v, v = #1 own γ (F{1 / 2} 1%nat))%I with "[Hγ1] [Hγ2]").
iApply (cwp_bin_op _ _ (λ v, v = #1 own γ (F{1 / 2} 1))%I
(λ v, v = #1 own γ (F{1 / 2} 1))%I with "[Hγ1] [Hγ2]").
- by iApply "H".
- by iApply "H".
- iIntros (v1 v2) "[-> Hγ1] [-> Hγ2]". iExists #2; iSplit; first done.
......
......@@ -63,7 +63,7 @@ Section test.
end)%I.
Lemma test_spec R cl `{inG Σ testR, inG Σ fracR} :
cl C #0%nat -
cl C #0 -
CWP "x" ←ᶜ test (cloc_to_val cl); c_ret "x" @ R {{ v, v = #21
(cl C #10 cl C #11) }}.
Proof.
......
......@@ -41,7 +41,7 @@ Section tests_vcg.
Qed.
Lemma test3_NOMATCH (n m : Z) :
1 n
(1 n)%Z
CWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }}%I.
Proof.
intros. vcg.
......
......@@ -27,7 +27,7 @@ Fixpoint denv_wf_val (E : known_locs) (m : denv) : bool :=
end.
Definition denv_wf_len (E : known_locs) (m : denv) : bool :=
bool_decide (length m length E)%nat.
bool_decide (length m length E).
Definition denv_wf (E : known_locs) (m : denv) : bool :=
denv_wf_val E m && denv_wf_len E m.
......
......@@ -311,7 +311,7 @@ Section vcg_spec.
denv_wf E m dval_wf E dv1 dval_wf E dv2
denv_interp E m -
vcg_alloc E dv1 dv2 m Φ -
n : nat, dval_interp E dv1 = #n n O%nat
n : nat, dval_interp E dv1 = #n n O
( cl, block_info cl true n -
cl C replicate n (dval_interp E dv2) -
vcg_continuation E Φ (cloc_to_val cl)).
......
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