Commit 0e421695 authored by Ralf Jung's avatar Ralf Jung

begin bumping Iris

parent b9e22933
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2018-07-13.2.af5611c8") | (= "dev") }
"coq-iris" { (= "dev.2018-10-04.7.fc21b664") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -61,7 +61,7 @@ Section ClosedProofs.
Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
Lemma client_adequate σ : adequate NotStuck client σ (λ _, True).
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
End ClosedProofs.
......
......@@ -221,8 +221,8 @@ Section contents.
Proof.
iIntros (Φ) "[#Hrunner HP] HΦ".
unfold newTask. do 2 wp_rec. iApply wp_fupd.
wp_alloc status as "Hstatus".
wp_alloc res as "Hres".
wp_alloc status as "Hstatus".
iMod (new_pending) as (γ) "[Htoken Htask]".
iMod (new_INIT) as (γ') "[Hinit Hinit']".
iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
......@@ -377,12 +377,12 @@ Section contents.
iLöb as "IH" forall (i).
wp_rec. wp_op. case_bool_decide; wp_if; last first.
{ by iApply "HΦ". }
wp_bind (Fork _). iApply wp_fork. iSplitL.
wp_bind (Fork _). iApply wp_fork.
- iNext. by iApply runner_runTasks_spec.
- iNext. wp_rec. wp_op.
(* Set Printing Coercions. *)
assert ((Z.of_nat i + 1) = Z.of_nat (i + 1)) as -> by lia.
iApply ("IH" with "HΦ").
- iNext. by iApply runner_runTasks_spec.
Qed.
Lemma newRunner_spec P Q (fe ne : expr) (f : val) (n : nat) :
......
......@@ -47,17 +47,17 @@ Section contents.
{ assert (n = S O) as -> by lia.
assert (1 = S O) as -> by lia.
by iApply "HΦ". }
wp_op. wp_bind ((rec: "fib" "a" := _)%V #(n - 1)).
wp_op. wp_bind ((rec: "fib" "a" := _)%V #(n - 2)).
assert ( m, n = S (S m)) as [m ->].
{ assert (n O) by naive_solver.
assert (n S O) by naive_solver.
exists (n - (S (S O)))%nat. lia. }
assert ((S (S m) - 1) = S m) as -> by lia.
assert ((S (S m) - 2) = m) as -> by lia.
iApply "IH". iNext. iIntros (? <-).
assert (Z.of_nat (S (S m)) = m + 2) as -> by lia.
Local Opaque fib.
wp_op. assert (m + 2 - 2 = m) as -> by lia.
wp_bind ((rec: "fib" "a" := _)%V #m).
wp_op. assert (m + 2 - 1 = S m) as -> by lia.
wp_bind ((rec: "fib" "a" := _)%V #(S m)).
iApply "IH". iNext. iIntros (? <-).
wp_op. rewrite -Nat2Z.inj_add.
iApply "HΦ". iPureIntro.
......@@ -136,4 +136,3 @@ Section contents.
by iApply "HΦ".
Qed.
End contents.
......@@ -7,7 +7,7 @@ Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _, True)); first (intros [_ ?]; eauto).
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ); eauto.
iIntros (Hinv). iModIntro. iExists (λ _, True%I). iSplit=> //.
rewrite -(empty_env_subst e).
......
......@@ -13,7 +13,7 @@ Theorem soundness Σ `{heapPreG Σ} e τ e' thp σ σ' :
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _, True)); first (intros [_ ?]; eauto).
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ _); eauto.
iIntros (Hinv).
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
......
......@@ -13,7 +13,7 @@ Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _, True)); first (intros [_ ?]; eauto).
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ _). iIntros (Hinv).
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
......
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