Commit 778406b2 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent b9e22933
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [ depends: [
"coq-iris" { (= "dev.2018-07-13.2.af5611c8") | (= "dev") } "coq-iris" { (= "dev.2018-07-13.2.464c2449") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -61,7 +61,7 @@ Section ClosedProofs. ...@@ -61,7 +61,7 @@ Section ClosedProofs.
Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ]. 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. Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
End ClosedProofs. End ClosedProofs.
......
...@@ -15,7 +15,9 @@ Set Default Proof Using "Type". ...@@ -15,7 +15,9 @@ Set Default Proof Using "Type".
(** Coarse-grained bag implementation using a spin lock *) (** Coarse-grained bag implementation using a spin lock *)
Definition newBag : val := λ: <>, Definition newBag : val := λ: <>,
(ref NONE, newlock #()). let: "r" := ref NONE in
let: "l" := newlock #() in
("r", "l").
Definition pushBag : val := λ: "b" "v", Definition pushBag : val := λ: "b" "v",
let: "l" := Snd "b" in let: "l" := Snd "b" in
let: "r" := Fst "b" in let: "r" := Fst "b" in
...@@ -102,12 +104,11 @@ Section proof. ...@@ -102,12 +104,11 @@ Section proof.
Proof. Proof.
iIntros (Φ) "_ HΦ". iIntros (Φ) "_ HΦ".
unfold newBag. wp_rec. unfold newBag. wp_rec.
wp_alloc r as "Hr". wp_alloc r as "Hr". wp_let.
iMod (own_alloc (1%Qp, to_agree )) as (γb) "[Ha Hf]"; first done. iMod (own_alloc (1%Qp, to_agree )) as (γb) "[Ha Hf]"; first done.
wp_apply (newlock_spec N (bag_inv γb r) with "[Hr Ha]"). wp_apply (newlock_spec N (bag_inv γb r) with "[Hr Ha]").
{ iExists []. iFrame. } { iExists []. iFrame. }
iIntros (lk γ) "#Hlk". iIntros (lk γ) "#Hlk". wp_let. iApply "HΦ".
iApply wp_value. iApply "HΦ".
rewrite /is_bag /bag_contents. iFrame. rewrite /is_bag /bag_contents. iFrame.
iExists _,_,_. by iFrame "Hlk". iExists _,_,_. by iFrame "Hlk".
Qed. Qed.
......
...@@ -221,8 +221,8 @@ Section contents. ...@@ -221,8 +221,8 @@ Section contents.
Proof. Proof.
iIntros (Φ) "[#Hrunner HP] HΦ". iIntros (Φ) "[#Hrunner HP] HΦ".
unfold newTask. do 2 wp_rec. iApply wp_fupd. unfold newTask. do 2 wp_rec. iApply wp_fupd.
wp_alloc status as "Hstatus".
wp_alloc res as "Hres". wp_alloc res as "Hres".
wp_alloc status as "Hstatus".
iMod (new_pending) as (γ) "[Htoken Htask]". iMod (new_pending) as (γ) "[Htoken Htask]".
iMod (new_INIT) as (γ') "[Hinit Hinit']". 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". 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. ...@@ -377,12 +377,12 @@ Section contents.
iLöb as "IH" forall (i). iLöb as "IH" forall (i).
wp_rec. wp_op. case_bool_decide; wp_if; last first. wp_rec. wp_op. case_bool_decide; wp_if; last first.
{ by iApply "HΦ". } { by iApply "HΦ". }
wp_bind (Fork _). iApply wp_fork. iSplitL. wp_bind (Fork _). iApply (wp_fork with "[]").
- iNext. by iApply runner_runTasks_spec.
- iNext. wp_rec. wp_op. - iNext. wp_rec. wp_op.
(* Set Printing Coercions. *) (* Set Printing Coercions. *)
assert ((Z.of_nat i + 1) = Z.of_nat (i + 1)) as -> by lia. assert ((Z.of_nat i + 1) = Z.of_nat (i + 1)) as -> by lia.
iApply ("IH" with "HΦ"). iApply ("IH" with "HΦ").
- iNext. by iApply runner_runTasks_spec.
Qed. Qed.
Lemma newRunner_spec P Q (fe ne : expr) (f : val) (n : nat) : Lemma newRunner_spec P Q (fe ne : expr) (f : val) (n : nat) :
......
...@@ -26,6 +26,7 @@ Section contents. ...@@ -26,6 +26,7 @@ Section contents.
| S n' => fib n + fib n' | S n' => fib n + fib n'
end end
end. end.
Arguments fib !_ / : simpl nomatch.
Definition seqFib : val := rec: "fib" "a" := Definition seqFib : val := rec: "fib" "a" :=
if: "a" = #0 if: "a" = #0
...@@ -38,30 +39,21 @@ Section contents. ...@@ -38,30 +39,21 @@ Section contents.
{{{ True }}} seqFib #n {{{ (m : nat), RET #m; fib n = m }}}. {{{ True }}} seqFib #n {{{ (m : nat), RET #m; fib n = m }}}.
Proof. Proof.
iIntros (Φ) "_ HΦ". iIntros (Φ) "_ HΦ".
iLöb as "IH" forall (n Φ). rewrite /seqFib. iLöb as "IH" forall (n Φ).
wp_rec. wp_op. case_bool_decide; simplify_eq; wp_if. wp_rec. simpl. wp_op. case_bool_decide; simplify_eq; wp_if.
{ assert (n = O) as -> by lia. { assert (n = O) as -> by lia.
assert (1 = S O) as -> by lia. by iApply ("HΦ" $! 1%nat). }
by iApply "HΦ". }
wp_op. case_bool_decide; simplify_eq; wp_if. wp_op. case_bool_decide; simplify_eq; wp_if.
{ assert (n = S O) as -> by lia. { assert (n = 1%nat) as -> by lia.
assert (1 = S O) as -> by lia. by iApply ("HΦ" $! 1%nat). }
by iApply "HΦ". } wp_op. destruct n as [|[|n]]=> //.
wp_op. wp_bind ((rec: "fib" "a" := _)%V #(n - 1)). rewrite !Nat2Z.inj_succ.
assert ( m, n = S (S m)) as [m ->]. replace (Z.succ (Z.succ n) - 2) with (Z.of_nat n) by lia.
{ assert (n O) by naive_solver. wp_apply "IH". iIntros (? <-).
assert (n S O) by naive_solver. wp_op.
exists (n - (S (S O)))%nat. lia. } replace (Z.succ (Z.succ n) - 1) with (Z.of_nat (S n)) by lia.
assert ((S (S m) - 1) = S m) as -> by lia. wp_apply "IH". iIntros (? <-). wp_op.
iApply "IH". iNext. iIntros (? <-). rewrite -Nat2Z.inj_add. by iApply "HΦ".
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).
iApply "IH". iNext. iIntros (? <-).
wp_op. rewrite -Nat2Z.inj_add.
iApply "HΦ". iPureIntro.
Local Transparent fib. done.
Qed. Qed.
Definition parFib : val := λ: "r" "a", Definition parFib : val := λ: "r" "a",
...@@ -85,38 +77,30 @@ Section contents. ...@@ -85,38 +77,30 @@ Section contents.
Proof. Proof.
iIntros (Φ) "[#Hrunner HP] HΦ". iIntros (Φ) "[#Hrunner HP] HΦ".
iDestruct "HP" as (n) "%"; simplify_eq. iDestruct "HP" as (n) "%"; simplify_eq.
do 2 wp_rec. wp_op. case_bool_decide; wp_if. do 2 wp_rec. simpl. wp_op. case_bool_decide; wp_if.
- iApply seqFib_spec; eauto. - iApply seqFib_spec; eauto.
iNext. iIntros (? <-). iApply "HΦ". iNext. iIntros (? <-). iApply "HΦ".
iExists n; done. iExists n; done.
- do 2 (wp_op; wp_let). - do 2 (wp_op; wp_let).
assert ( m : nat, n = S (S m)) as [m ->]. destruct n as [|[|n]]=> //.
{ exists (n - 2)%nat. lia. } rewrite !Nat2Z.inj_succ.
assert ((S (S m) - 1) = S m) as -> by lia. replace (Z.succ (Z.succ n) - 2) with (Z.of_nat n) by lia.
assert ((S (S m) - 2) = m) as -> by lia. replace (Z.succ (Z.succ n) - 1) with (Z.succ n) by lia.
wp_bind (runner_Fork b r _). wp_apply (runner_Fork_spec).
iApply (runner_Fork_spec). { iFrame "Hrunner". iExists (S n). by rewrite Nat2Z.inj_succ. }
{ iFrame "Hrunner". iExists (S m). eauto. } iIntros (γ1 γ1' t1) "Ht1". wp_let.
iNext. iIntros (γ1 γ1' t1) "Ht1". wp_let. wp_apply (runner_Fork_spec).
wp_bind (runner_Fork b r _).
iApply (runner_Fork_spec).
{ iFrame "Hrunner". eauto. } { iFrame "Hrunner". eauto. }
iNext. iIntros (γ2 γ2' t2) "Ht2". wp_let. iIntros (γ2 γ2' t2) "Ht2". wp_let.
wp_bind (task_Join _). wp_apply (task_Join_spec with "[$Ht2]"); try done.
iApply (task_Join_spec with "[$Ht1]"); try done. iIntros (v2) "HQ"; simplify_eq.
iNext. iIntros (v1) "HQ"; simplify_eq.
iDestruct "HQ" as (m1' m1) "%". simplify_eq.
assert (m1' = S m) as -> by lia.
Local Opaque fib.
wp_bind (task_Join _).
iApply (task_Join_spec with "[$Ht2]"); try done.
iNext. iIntros (v2) "HQ"; simplify_eq.
iDestruct "HQ" as (m2' m2) "%". simplify_eq. iDestruct "HQ" as (m2' m2) "%". simplify_eq.
wp_op. iApply "HΦ". wp_apply (task_Join_spec with "[$Ht1]"); try done.
Local Transparent fib. iIntros (v1) "HQ"; simplify_eq.
iExists (S (S m2')). iSplit; eauto. iDestruct "HQ" as (m1' m1) "%". simplify_eq.
assert ((fib (S m2') + fib m2') = (fib (S m2') + fib m2')%nat) as -> by lia. wp_op. iApply "HΦ". iExists (S (S m2')).
done. rewrite !Nat2Z.inj_succ -Nat2Z.inj_add.
by replace m1' with (S m2') by lia.
Qed. Qed.
Lemma fibRunner_spec (n a : nat) : Lemma fibRunner_spec (n a : nat) :
...@@ -136,4 +120,3 @@ Section contents. ...@@ -136,4 +120,3 @@ Section contents.
by iApply "HΦ". by iApply "HΦ".
Qed. Qed.
End contents. End contents.
...@@ -24,35 +24,36 @@ Section lang_rules. ...@@ -24,35 +24,36 @@ Section lang_rules.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto. Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step. Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec := Local Ltac solve_pure_exec :=
unfold IntoVal in *; subst; unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ]. intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_lam e1 e2 `{!AsVal e2} : Global Instance pure_lam e1 e2 `{!AsVal e2} :
PureExec True (App (Lam e1) e2) e1.[e2 /]. PureExec True 1 (App (Lam e1) e2) e1.[e2 /].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_tlam e : PureExec True (TApp (TLam e)) e. Global Instance pure_tlam e : PureExec True 1 (TApp (TLam e)) e.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_fold e `{!AsVal e}: Global Instance pure_fold e `{!AsVal e}:
PureExec True (Unfold (Fold e)) e. PureExec True 1 (Unfold (Fold e)) e.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} : Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} :
PureExec True (Fst (Pair e1 e2)) e1. PureExec True 1 (Fst (Pair e1 e2)) e1.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} : Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} :
PureExec True (Snd (Pair e1 e2)) e2. PureExec True 1 (Snd (Pair e1 e2)) e2.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}: Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}:
PureExec True (Case (InjL e0) e1 e2) e1.[e0/]. PureExec True 1 (Case (InjL e0) e1 e2) e1.[e0/].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}: Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}:
PureExec True (Case (InjR e0) e1 e2) e2.[e0/]. PureExec True 1 (Case (InjR e0) e1 e2) e2.[e0/].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
End lang_rules. End lang_rules.
...@@ -7,7 +7,7 @@ Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' : ...@@ -7,7 +7,7 @@ Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
rtc step ([e], σ) (thp, σ') e' thp rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'. is_Some (to_val e') reducible e' σ'.
Proof. 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. eapply (wp_adequacy Σ); eauto.
iIntros (Hinv). iModIntro. iExists (λ _, True%I). iSplit=> //. iIntros (Hinv). iModIntro. iExists (λ _, True%I). iSplit=> //.
rewrite -(empty_env_subst e). rewrite -(empty_env_subst e).
......
...@@ -94,34 +94,35 @@ Section lang_rules. ...@@ -94,34 +94,35 @@ Section lang_rules.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto. Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step. Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec := Local Ltac solve_pure_exec :=
unfold IntoVal in *; subst; unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ]. intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_lam e1 e2 `{!AsVal e2} : Global Instance pure_lam e1 e2 `{!AsVal e2} :
PureExec True (App (Lam e1) e2) e1.[e2 /]. PureExec True 1 (App (Lam e1) e2) e1.[e2 /].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_tlam e : PureExec True (TApp (TLam e)) e. Global Instance pure_tlam e : PureExec True 1 (TApp (TLam e)) e.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_fold e `{!AsVal e}: Global Instance pure_fold e `{!AsVal e}:
PureExec True (Unfold (Fold e)) e. PureExec True 1 (Unfold (Fold e)) e.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} : Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} :
PureExec True (Fst (Pair e1 e2)) e1. PureExec True 1 (Fst (Pair e1 e2)) e1.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} : Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} :
PureExec True (Snd (Pair e1 e2)) e2. PureExec True 1 (Snd (Pair e1 e2)) e2.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}: Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}:
PureExec True (Case (InjL e0) e1 e2) e1.[e0/]. PureExec True 1 (Case (InjL e0) e1 e2) e1.[e0/].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}: Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}:
PureExec True (Case (InjR e0) e1 e2) e2.[e0/]. PureExec True 1 (Case (InjR e0) e1 e2) e2.[e0/].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
End lang_rules. End lang_rules.
...@@ -13,7 +13,7 @@ Theorem soundness Σ `{heapPreG Σ} e τ e' thp σ σ' : ...@@ -13,7 +13,7 @@ Theorem soundness Σ `{heapPreG Σ} e τ e' thp σ σ' :
rtc step ([e], σ) (thp, σ') e' thp rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'. is_Some (to_val e') reducible e' σ'.
Proof. 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. eapply (wp_adequacy Σ _); eauto.
iIntros (Hinv). iIntros (Hinv).
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh". iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
......
...@@ -11,7 +11,7 @@ Lemma basic_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)} ...@@ -11,7 +11,7 @@ Lemma basic_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)}
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp')). ( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp')).
Proof. Proof.
intros Hlog Hsteps. intros Hlog Hsteps.
cut (adequate NotStuck e (λ _, thp' h v, rtc step ([e'], ) (of_val v :: thp', h))). cut (adequate NotStuck e (λ _ _, thp' h v, rtc step ([e'], ) (of_val v :: thp', h))).
{ destruct 1; naive_solver. } { destruct 1; naive_solver. }
eapply (wp_adequacy Σ); first by apply _. eapply (wp_adequacy Σ); first by apply _.
iIntros (Hinv). iIntros (Hinv).
......
...@@ -124,47 +124,48 @@ Section lang_rules. ...@@ -124,47 +124,48 @@ Section lang_rules.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto. Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step. Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec := Local Ltac solve_pure_exec :=
unfold IntoVal in *; subst; unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ]. intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_rec e1 e2 `{!AsVal e2} : Global Instance pure_rec e1 e2 `{!AsVal e2} :
PureExec True (App (Rec e1) e2) e1.[(Rec e1), e2 /]. PureExec True 1 (App (Rec e1) e2) e1.[(Rec e1), e2 /].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_tlam e : PureExec True (TApp (TLam e)) e. Global Instance pure_tlam e : PureExec True 1 (TApp (TLam e)) e.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_fold e `{!AsVal e}: Global Instance pure_fold e `{!AsVal e}:
PureExec True (Unfold (Fold e)) e. PureExec True 1 (Unfold (Fold e)) e.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} : Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} :
PureExec True (Fst (Pair e1 e2)) e1. PureExec True 1 (Fst (Pair e1 e2)) e1.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} : Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} :
PureExec True (Snd (Pair e1 e2)) e2. PureExec True 1 (Snd (Pair e1 e2)) e2.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}: Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}:
PureExec True (Case (InjL e0) e1 e2) e1.[e0/]. PureExec True 1 (Case (InjL e0) e1 e2) e1.[e0/].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}: Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}:
PureExec True (Case (InjR e0) e1 e2) e2.[e0/]. PureExec True 1 (Case (InjR e0) e1 e2) e2.[e0/].
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance wp_if_true e1 e2 : Global Instance wp_if_true e1 e2 :
PureExec True (If (# true) e1 e2) e1. PureExec True 1 (If (# true) e1 e2) e1.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance wp_if_false e1 e2 : Global Instance wp_if_false e1 e2 :
PureExec True (If (# false) e1 e2) e2. PureExec True 1 (If (# false) e1 e2) e2.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance wp_nat_binop op a b : Global Instance wp_nat_binop op a b :
PureExec True (BinOp op (#n a) (#n b)) (of_val (binop_eval op a b)). PureExec True 1 (BinOp op (#n a) (#n b)) (of_val (binop_eval op a b)).
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
End lang_rules. End lang_rules.
...@@ -11,7 +11,7 @@ Lemma basic_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} ...@@ -11,7 +11,7 @@ Lemma basic_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp')). ( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp')).
Proof. Proof.
intros Hlog Hsteps. intros Hlog Hsteps.
cut (adequate NotStuck e (λ _, thp' h v, rtc step ([e'], ) (of_val v :: thp', h))). cut (adequate NotStuck e (λ _ _, thp' h v, rtc step ([e'], ) (of_val v :: thp', h))).
{ destruct 1; naive_solver. } { destruct 1; naive_solver. }
eapply (wp_adequacy Σ _); iIntros (Hinv). eapply (wp_adequacy Σ _); iIntros (Hinv).
iMod (own_alloc ( to_gen_heap )) as (γ) "Hh". iMod (own_alloc ( to_gen_heap )) as (γ) "Hh".
......
...@@ -13,7 +13,7 @@ Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' : ...@@ -13,7 +13,7 @@ Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
rtc step ([e], σ) (thp, σ') e' thp rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'. is_Some (to_val e') reducible e' σ'.
Proof. 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). eapply (wp_adequacy Σ _). iIntros (Hinv).
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh". iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). } { apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
......
...@@ -25,30 +25,31 @@ Section stlc_rules. ...@@ -25,30 +25,31 @@ Section stlc_rules.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto. Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step. Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec := Local Ltac solve_pure_exec :=
unfold IntoVal in *; subst; unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ]. intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
(** Helper Lemmas for weakestpre. *) (** Helper Lemmas for weakestpre. *)
Global Instance pure_lam e1 e2 `{!AsVal e2}: Global Instance pure_lam e1 e2 `{!AsVal e2}:
PureExec True (App (Lam e1) e2) (e1.[e2 /]). PureExec True 1 (App (Lam e1) e2) (e1.[e2 /]).
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.