...
 
Commits (32)
......@@ -34,39 +34,43 @@ This repository contains the following case studies:
* [barrier](theories/barrier): Implementation and proof of a barrier as
described in ["Higher-Order Ghost State"](http://doi.acm.org/10.1145/2818638).
* [logrel](theories/logrel): Logical relations from the
[IPM paper](http://doi.acm.org/10.1145/3093333.3009855):
- STLC
- Unary logical relations proving type safety
- F_mu (System F with recursive types)
- Unary logical relations proving type safety
- F_mu_ref (System F with recursive types and references)
- Unary logical relations proving type safety
- Binary logical relations for proving contextual refinements
- F_mu_ref_conc (System F with recursive types, references and concurrency)
- Unary logical relations proving type safety
- Binary logical relations for proving contextual refinements
- Proof of refinement for a pair of fine-grained/coarse-grained
concurrent counter implementations
- Proof of refinement for a pair of fine-grained/coarse-grained
concurrent stack implementations
* [logrel_heaplang](theories/logrel_heaplang): A unary logical relation for
semantic typing of heap lang.
* [logrel](logrel): Logical relations.
- [logrel/stlc](theories/logrel/stlc): A unary logical relation for semantic
typing STLC (simply-typed lambda calculus) with De Bruijn indices (using
Autosubst).
- [logrel/F_mu_ref_conc](theories/logrel/F_mu_ref_conc): The logical relations
for F_mu_ref_conc (System F with recursive types, references and concurrency)
with De Bruijn indices (using Autosubst) from the
[IPM paper](http://doi.acm.org/10.1145/3093333.3009855):
+ Unary logical relations proving type safety.
+ Binary logical relations for proving contextual refinements.
+ Proof of refinement for a pair of fine-grained/coarse-grained
concurrent counter implementations.
+ Proof of refinement for a pair of fine-grained/coarse-grained
concurrent stack implementations.
- [logrel/heaplang](theories/logrel/heaplang): A unary logical relation for
semantic typing of heap lang (by Robbert Krebbers).
* [logatom](theories/logrel_heaplang): Proofs of various logically atomic specifications:
- Elimination Stack (by Ralf Jung)
- Conditional increment (inspired by [this paper](https://people.mpi-sws.org/~dreyer/papers/relcon/paper.pdf)) and RDCSS (as in [this paper](https://timharris.uk/papers/2002-disc.pdf)) (by Marianna Rapoport, Rodolphe Lepigre and Gaurav Parthasarathy)
- [Herlihy-Wing-Queue](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf) (by Rodolphe Lepigre)
- Atomic Snapshot (by Marianna Rapoport)
- Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre)
- Flat Combiner (by Zhen Zhang, also see [this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs))
- Elimination Stack (by Ralf Jung).
- Conditional increment (inspired by [this paper](https://people.mpi-sws.org/~dreyer/papers/relcon/paper.pdf))
and RDCSS (as in [this paper](https://timharris.uk/papers/2002-disc.pdf))
(by Marianna Rapoport, Rodolphe Lepigre and Gaurav Parthasarathy).
- [Herlihy-Wing-Queue](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)
(by Rodolphe Lepigre).
- Atomic Snapshot (by Marianna Rapoport).
- Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre).
- Flat Combiner (by Zhen Zhang, also see
[this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs)).
* [spanning-tree](theories/spanning_tree): Proof of a concurrent spanning tree
algorithm by Amin Timany.
algorithm (by Amin Timany).
* [concurrent-stacks](theories/concurrent_stacks): Proof of an implementation of
concurrent stacks with helping by Daniel Gratzer et. al., as described in the
[report](http://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf).
* [lecture-notes](theories/lecture_notes): Coq examples for the
[Iris lecture notes](http://iris-project.org/tutorial-material.html).
* [hocap](theories/hocap): Formalisations of the concurrent bag and concurrent runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283). See the associated [README](theories/hocap/README.md).
* [hocap](theories/hocap): Formalizations of the concurrent bag and concurrent
runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283)
(by Dan Frumin). See the associated [README](theories/hocap/README.md).
## For Developers: How to update the Iris dependency
......
......@@ -37,30 +37,14 @@ theories/concurrent_stacks/concurrent_stack2.v
theories/concurrent_stacks/concurrent_stack3.v
theories/concurrent_stacks/concurrent_stack4.v
theories/logrel/prelude/base.v
theories/logrel/stlc/lang.v
theories/logrel/stlc/typing.v
theories/logrel/stlc/rules.v
theories/logrel/stlc/typing.v
theories/logrel/stlc/logrel.v
theories/logrel/stlc/fundamental.v
theories/logrel/stlc/soundness.v
theories/logrel/F_mu/lang.v
theories/logrel/F_mu/typing.v
theories/logrel/F_mu/rules.v
theories/logrel/F_mu/logrel.v
theories/logrel/F_mu/fundamental.v
theories/logrel/F_mu/soundness.v
theories/logrel/F_mu_ref/lang.v
theories/logrel/F_mu_ref/typing.v
theories/logrel/F_mu_ref/rules.v
theories/logrel/F_mu_ref/rules_binary.v
theories/logrel/F_mu_ref/logrel.v
theories/logrel/F_mu_ref/logrel_binary.v
theories/logrel/F_mu_ref/fundamental.v
theories/logrel/F_mu_ref/fundamental_binary.v
theories/logrel/F_mu_ref/soundness.v
theories/logrel/F_mu_ref/context_refinement.v
theories/logrel/F_mu_ref/soundness_binary.v
theories/logrel/stlc/fundamental.v
theories/logrel/F_mu_ref_conc/base.v
theories/logrel/F_mu_ref_conc/lang.v
theories/logrel/F_mu_ref_conc/rules.v
theories/logrel/F_mu_ref_conc/typing.v
......@@ -78,11 +62,17 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/logrel/F_mu_ref_conc/examples/queue/common.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue_alt.v
theories/logrel/F_mu_ref_conc/examples/queue/CG_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_variant.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_original.v
theories/logrel/F_mu_ref_conc/examples/fact.v
theories/logrel_heaplang/ltyping.v
theories/logrel_heaplang/ltyping_safety.v
theories/logrel_heaplang/lib/symbol_adt.v
theories/logrel/heaplang/ltyping.v
theories/logrel/heaplang/ltyping_safety.v
theories/logrel/heaplang/lib/symbol_adt.v
theories/hocap/abstract_bag.v
theories/hocap/cg_bag.v
......@@ -106,7 +96,6 @@ theories/logatom/flat_combiner/peritem.v
theories/logatom/flat_combiner/atomic_sync.v
theories/logatom/flat_combiner/misc.v
theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v
......
......@@ -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.0.e3f87a95") | (= "dev") }
"coq-iris" { (= "dev.2020-05-28.3.38f177d3") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
"coq-iris-string-ident"
]
......
......@@ -4,7 +4,7 @@
This file: abstract bag specification
*)
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Export invariants.
From stdpp Require Import gmultiset.
Set Default Proof Using "Type".
......
......@@ -64,7 +64,6 @@ Section proof.
Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
( ls : list val, b (val_of_list ls) own γb ((1/2)%Qp, to_agree (list_to_set_disj ls)))%I.
Definition is_bag (γb : gname) (x : val) :=
( (lk : val) (b : loc) (γ : gname),
x = PairV #b lk is_lock γ lk (bag_inv γb b))%I.
Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ :=
......
......@@ -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".
......
From stdpp Require Import namespaces.
From iris.base_logic.lib Require Export gen_inv_heap.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Export proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
......@@ -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 >>>
......
From stdpp Require Import namespaces.
From iris.algebra Require Import excl auth list.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import proofmode atomic_heap.
From iris.heap_lang Require Import proofmode notation atomic_heap.
From iris_examples.logatom.elimination_stack Require spec.
Set Default Proof Using "Type".
......
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for a stack. *)
......
......@@ -3,7 +3,7 @@ From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode atomic_heap.
From iris.heap_lang Require Import proofmode notation atomic_heap.
From iris_examples.logatom.elimination_stack Require Import spec.
Set Default Proof Using "Type".
......
This diff is collapsed.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for Herlihy-Wing queues. *)
......
From stdpp Require Import namespaces.
From iris.base_logic.lib Require Export gen_inv_heap.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Export proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for RDCSS.
......
......@@ -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.
}
......
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** Specifying snapshots with histories
......
From iris_examples.logrel.F_mu Require Export logrel.
From iris.program_logic Require Import lifting.
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu Require Import rules.
Definition log_typed `{irisG F_mu_lang Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs,
env_Persistent Δ
Γ * Δ vs τ ⟧ₑ Δ e.[env_subst vs].
Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).
Section fundamental.
Context `{irisG F_mu_lang Σ}.
Notation D := (valO -n> iProp Σ).
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (wp_bind (fill[ctx]));
iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
iIntros (v) Hv.
Theorem fundamental Γ e τ : Γ e : τ Γ e : τ.
Proof.
induction 1; iIntros (Δ vs HΔ) "#HΓ"; cbn.
- (* var *)
iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
erewrite env_subst_lookup; eauto. by iApply wp_value.
- (* unit *) by iApply wp_value.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
iApply wp_value; eauto 10.
- (* fst *)
smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
simpl. iApply wp_pure_step_later; auto. by iApply wp_value.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
simpl. iApply wp_pure_step_later; eauto. by iApply wp_value.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn.
iApply wp_value; eauto.
- (* injr *)
smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn.
iApply wp_value; eauto.
- (* case *)
smart_wp_bind (CaseCtx _ _) v "#Hv" IHtyped1; cbn.
iDestruct (interp_env_length with "HΓ") as %?.
iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
+ iApply wp_pure_step_later; auto; asimpl. iNext.
iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
+ iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
- (* lam *)
iApply wp_value; simpl; iAlways; iIntros (w) "#Hw".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl.
iApply (IHtyped Δ (w :: vs)). iApply interp_env_cons; auto.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
iApply wp_value; simpl.
iAlways; iIntros (τi) "%". iApply wp_pure_step_later; auto. iNext.
iApply IHtyped. by iApply interp_env_ren.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! ( τ' Δ)); iPureIntro; apply _|].
iIntros (w) "?". by rewrite interp_subst.
- (* Fold *)
smart_wp_bind FoldCtx v "#Hv" IHtyped; cbn. iApply wp_value.
rewrite /= -interp_subst fixpoint_interp_rec1_eq /=.
iAlways; eauto.
- (* Unfold *)
iApply (wp_bind (fill [UnfoldCtx]));
iApply wp_wand_l; iSplitL; [|iApply IHtyped; trivial].
iIntros (v) "#Hv /=". rewrite /= fixpoint_interp_rec1_eq.
change (fixpoint _) with ( TRec τ Δ); simpl.
iDestruct "Hv" as (w) "#[% Hw]"; subst; simpl.
iApply wp_pure_step_later; auto. iApply wp_value; iNext.
by rewrite -interp_subst.
Qed.
End fundamental.
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris_examples.logrel.prelude Require Export base.
Module F_mu.
Inductive expr :=
| Var (x : var)
| Lam (e : {bind 1 of expr})
| App (e1 e2 : expr)
(* Unit *)
| Unit
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
(* Recursive Types *)
| Fold (e : expr)
| Unfold (e : expr)
(* Polymorphic Types *)
| TLam (e : expr)
| TApp (e : expr).
Instance Ids_expr : Ids expr. derive. Defined.
Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
Inductive val :=
| LamV (e : {bind 1 of expr})
| TLamV (e : {bind 1 of expr})
| UnitV
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
| FoldV (v : val).
Fixpoint of_val (v : val) : expr :=
match v with
| LamV e => Lam e
| TLamV e => TLam e
| UnitV => Unit
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
| FoldV v => Fold (of_val v)
end.
Notation "# v" := (of_val v) (at level 20).
Fixpoint to_val (e : expr) : option val :=
match e with
| Lam e => Some (LamV e)
| TLam e => Some (TLamV e)
| Unit => Some UnitV
| Pair e1 e2 => v1 to_val e1; v2 to_val e2; Some (PairV v1 v2)
| InjL e => InjLV <$> to_val e
| InjR e => InjRV <$> to_val e
| Fold e => v to_val e; Some (FoldV v)
| _ => None
end.
(** Evaluation contexts *)
Inductive ectx_item :=
| AppLCtx (e2 : expr)
| AppRCtx (v1 : val)
| TAppCtx
| PairLCtx (e2 : expr)
| PairRCtx (v1 : val)
| FstCtx
| SndCtx
| InjLCtx
| InjRCtx
| CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
| FoldCtx
| UnfoldCtx.
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx e2 => App e e2
| AppRCtx v1 => App (of_val v1) e
| TAppCtx => TApp e
| PairLCtx e2 => Pair e e2
| PairRCtx v1 => Pair (of_val v1) e
| FstCtx => Fst e
| SndCtx => Snd e
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| FoldCtx => Fold e
| UnfoldCtx => Unfold e
end.
Definition state : Type := ().
Inductive head_step : expr state list Empty_set expr state list expr Prop :=
(* β *)
| BetaS e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Lam e1) e2) σ [] e1.[e2/] σ []
(* Products *)
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Fst (Pair e1 e2)) σ [] e1 σ []
| SndS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Snd (Pair e1 e2)) σ [] e2 σ []
(* Sums *)
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ []
(* Recursive Types *)
| Unfold_Fold e v σ :
to_val e = Some v
head_step (Unfold (Fold e)) σ [] e σ []
(* Polymorphic Types *)
| TBeta e σ :
head_step (TApp (TLam e)) σ [] e σ [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof. by induction v; simplify_option_eq. Qed.
Lemma of_to_val e v : to_val e = Some v of_val v = e.
Proof.
revert v; induction e; intros; simplify_option_eq; auto with f_equal.
Qed.
Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. Qed.
Lemma val_stuck e1 σ1 κ e2 σ2 ef :
head_step e1 σ1 κ e2 σ2 ef to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 ef :
head_step (fill_item Ki e) σ1 κ e2 σ2 ef is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None to_val e2 = None
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2.
Proof.
destruct Ki1, Ki2; intros; try discriminate; simplify_eq;
repeat match goal with
| H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
end; auto.
Qed.
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Proof.
split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
Canonical Structure stateO := leibnizO state.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
End F_mu.
(** Language *)
Canonical Structure F_mu_ectxi_lang := EctxiLanguage F_mu.lang_mixin.
Canonical Structure F_mu_ectx_lang := EctxLanguageOfEctxi F_mu_ectxi_lang.
Canonical Structure F_mu_lang := LanguageOfEctx F_mu_ectx_lang.
Export F_mu.
Hint Extern 20 (PureExec _ _ _) => progress simpl : typeclass_instances.
Hint Extern 5 (IntoVal _ _) => eapply of_to_val; fast_done : typeclass_instances.
Hint Extern 10 (IntoVal _ _) =>
rewrite /IntoVal; eapply of_to_val; rewrite /= !to_of_val /=; solve [ eauto ] : typeclass_instances.
Hint Extern 5 (AsVal _) => eexists; eapply of_to_val; fast_done : typeclass_instances.
Hint Extern 10 (AsVal _) =>
eexists; rewrite /IntoVal; eapply of_to_val; rewrite /= !to_of_val /=; solve [ eauto ] : typeclass_instances.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_examples.logrel.F_mu Require Export lang typing.
From iris.algebra Require Import list.
Import uPred.
(** interp : is a unary logical relation. *)
Section logrel.
Context `{irisG F_mu_lang Σ}.
Notation D := (valO -n> iPropO Σ).
Implicit Types τi : D.
Implicit Types Δ : listO D.
Implicit Types interp : listO D D.
Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper.
Definition interp_unit : listO D -n> D := λne Δ w, (w = UnitV)%I.
Program Definition interp_prod
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
( w1 w2, w = PairV w1 w2 interp1 Δ w1 interp2 Δ w2)%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_sum
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
(( w1, w = InjLV w1 interp1 Δ w1) ( w2, w = InjRV w2 interp2 Δ w2))%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_arrow
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
( v, interp1 Δ v WP App (# w) (# v) {{ interp2 Δ }})%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_forall
(interp : listO D -n> D) : listO D -n> D := λne Δ w,
( τi : D,
v, Persistent (τi v) WP TApp (# w) {{ interp (τi :: Δ) }})%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Definition interp_rec1
(interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne w,
( ( v, w = FoldV v interp (τi :: Δ) v))%I.
Global Instance interp_rec1_contractive
(interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
Proof. by solve_contractive. Qed.
Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
fixpoint (interp_rec1 interp Δ) x interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
Next Obligation.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
Qed.
Fixpoint interp (τ : type) : listO D -n> D :=
match τ return _ with
| TUnit => interp_unit
| TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2)
| TSum τ1 τ2 => interp_sum (interp τ1) (interp τ2)
| TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2)
| TVar x => ctx_lookup x
| TForall τ' => interp_forall (interp τ')
| TRec τ' => interp_rec (interp τ')
end%I.
Notation "⟦ τ ⟧" := (interp τ).
Definition interp_env (Γ : list type)
(Δ : listO D) (vs : list val) : iProp Σ :=
(length Γ = length vs [] zip_with (λ τ, τ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listO D) (e : expr) : iProp Σ :=
WP e {{ τ Δ }}%I.
Class env_Persistent Δ :=
ctx_persistent : Forall (λ τi, v, Persistent (τi v)) Δ.
Global Instance ctx_persistent_nil : env_Persistent [].
Proof. by constructor. Qed.
Global Instance ctx_persistent_cons τi Δ :
( v, Persistent (τi v)) env_Persistent Δ env_Persistent (τi :: Δ).
Proof. by constructor. Qed.
Global Instance ctx_persistent_lookup Δ x v :
env_Persistent Δ Persistent (ctx_lookup x Δ v).
Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
Global Instance interp_persistent τ Δ v :
env_Persistent Δ Persistent ( τ Δ v).
Proof.
revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _.
rewrite /Persistent fixpoint_interp_rec1_eq /interp_rec1 /= intuitionistically_into_persistently.
by apply persistently_intro'.
Qed.
Global Instance interp_env_base_persistent Δ Γ vs :
env_Persistent Δ TCForall Persistent (zip_with (λ τ, τ Δ) Γ vs).
Proof.
intros HΔ. revert vs.
induction Γ => vs; simpl; destruct vs; constructor; apply _.
Qed.
Global Instance interp_env_persistent Γ Δ vs :
env_Persistent Δ Persistent ( Γ * Δ vs) := _.
Lemma interp_weaken Δ1 Π Δ2 τ :
τ.[upn (length Δ1) (ren (+ length Π))] (Δ1 ++ Π ++ Δ2)
τ (Δ1 ++ Δ2).
Proof.
revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τi w /=.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
Lemma interp_subst_up Δ1 Δ2 τ τ' :
τ (Δ1 ++ interp τ' Δ2 :: Δ2)
τ.[upn (length Δ1) (τ' .: ids)] (Δ1 ++ Δ2).
Proof.
revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl.
- done.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τi w /=.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..].
case EQ: (x - length Δ1) => [|n]; simpl.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
Lemma interp_subst Δ2 τ τ' v : τ ( τ' Δ2 :: Δ2) v τ.[τ'/] Δ2 v.
Proof. apply (interp_subst_up []). Qed.
Lemma interp_env_length Δ Γ vs : Γ * Δ vs length Γ = length vs.
Proof. by iIntros "[% ?]". Qed.
Lemma interp_env_Some_l Δ Γ vs x τ :
Γ !! x = Some τ Γ * Δ vs v, vs !! x = Some v τ Δ v.
Proof.
iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
iExists v; iSplit. done. iApply (big_sepL_elem_of with "HΓ").
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; by simplify_option_eq.
Qed.
Lemma interp_env_nil Δ : [] * Δ [].
Proof. iSplit; rewrite ?zip_with_nil_r; auto. Qed.
Lemma interp_env_cons Δ Γ vs τ v :
τ :: Γ * Δ (v :: vs) τ Δ v Γ * Δ vs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; lia|].
Qed.
Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi :
subst (ren (+1)) <$> Γ * (τi :: Δ) vs Γ * Δ vs.
Proof.
apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
revert Δ vs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto.
apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
Qed.
End logrel.
Notation "⟦ τ ⟧" := (interp τ).
Notation "⟦ τ ⟧ₑ" := (interp_expr τ).
Notation "⟦ Γ ⟧*" := (interp_env Γ).
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris_examples.logrel.F_mu Require Export lang.
From stdpp Require Import fin_maps.
Section lang_rules.
Context `{irisG F_mu_lang Σ}.
Implicit Types e : expr.
Ltac inv_head_step :=
repeat match goal with
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : head_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Constructors head_step : core.
Local Hint Resolve to_of_val : core.
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_pure_exec :=
unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_lam e1 e2 `{!AsVal e2} :
PureExec True 1 (App (Lam e1) e2) e1.[e2 /].
Proof. solve_pure_exec. Qed.
Global Instance pure_tlam e : PureExec True 1 (TApp (TLam e)) e.
Proof. solve_pure_exec. Qed.
Global Instance pure_fold e `{!AsVal e}:
PureExec True 1 (Unfold (Fold e)) e.
Proof. solve_pure_exec. Qed.
Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} :
PureExec True 1 (Fst (Pair e1 e2)) e1.
Proof. solve_pure_exec. Qed.
Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} :
PureExec True 1 (Snd (Pair e1 e2)) e2.
Proof. solve_pure_exec. Qed.
Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}:
PureExec True 1 (Case (InjL e0) e1 e2) e1.[e0/].
Proof. solve_pure_exec. Qed.
Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}:
PureExec True 1 (Case (InjR e0) e1 e2) e2.[e0/].
Proof. solve_pure_exec. Qed.
End lang_rules.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris_examples.logrel.F_mu Require Export fundamental.
Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
( `{irisG F_mu_lang Σ}, [] e : τ)
rtc erased_step ([e], σ) (thp, σ') e' thp not_stuck e' σ'.
Proof.
intros Hlog ??.
cut (adequate NotStuck e σ (λ _ _, True));
first by intros [_ Hsafe]; eapply Hsafe; eauto.
eapply (wp_adequacy Σ); eauto.
iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=> //.
replace e with e.[env_subst[]] by by asimpl.
set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
Qed.
Corollary type_soundness e τ e' thp σ σ' :
[] e : τ
rtc erased_step ([e], σ) (thp, σ') e' thp not_stuck e' σ'.
Proof.
intros ??. set (Σ := invΣ).
eapply (soundness Σ); eauto using fundamental.
Qed.
From iris_examples.logrel.F_mu Require Export lang.
Inductive type :=
| TUnit : type
| TProd : type type type
| TSum : type type type
| TArrow : type type type
| TRec (τ : {bind 1 of type})
| TVar (x : var)
| TForall (τ : {bind 1 of type}).
Instance Ids_type : Ids type. derive. Defined.
Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74,