Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • ci/ike/frame_exist
  • ci/janno/reduction_no_check
  • ci/janno/strict-tc-resolution
  • ci/pinning
  • ci/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/sections
  • ci/weak_mem
  • coqbug/match
  • ghostcell
  • gpirlea/pin_semantic
  • gpirlea/pinning
  • jh/closures
  • jh/dynamic_masks
  • jh/lifetime_no_dead_trade
  • jh/typecheck_foo
  • master
  • masters/rusthornbelt
  • masters/weak_mem
  • msammler/new-contractive
  • msammler/rustverify_talk
  • notations
  • ralf/acc
  • ralf/prop-level-wand
  • refmut_sync
  • robbert/Z_of_nat
  • robbert/sprop
  • rusthornbelt
  • skiplist
  • step_indexing_controlled_by_ghosts
  • strong_cas_fail
  • xldenis/option
  • xldenis/pldi-submission
  • xldenis/smallvec-push
  • xldenis/type-sum
  • yusuke/tlist_for_prophecy
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
40 results

Target

Select target project
  • Villetaneuse/lambda-rust
  • iris/lambda-rust
  • maximedenes/LambdaRust-coq
  • msammler/lambda-rust
  • daniel.louwrink/lambda-rust
  • simonspies/lambda-rust
  • xldenis/lambda-rust
  • lgaeher/lambda-rust
  • JasonHuZS/lambda-rust
  • snyke7/lambda-rust
  • ivanbakel/lambda-rust
  • HumamAlhusaini/lambda-rust
12 results
Select Git revision
  • ci/debug
  • ci/gen_proofmode
  • ci/iris-dev-performance
  • ci/janno/reduction_no_check
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/exact_vm
  • ci/ralf/sections
  • ci/ralf/weak_mem
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/naive_solver
  • ci/robbert/pm_faster_alt
  • ci/weak_mem
  • coqbug/match
  • fast_string
  • feature/ty_own_loc
  • fnlft
  • gen_big_op
  • iris-update
  • jh/bug
  • jh/closures
  • jh/dynamic_masks
  • jh/lifetime_no_dead_trade
  • jh/ofe_problems
  • jh/popl_submission
  • jh/typecheck_foo
  • jh/undiscriminated_hintdb
  • jh_nondependent_expr
  • master
  • new_lifetime_logic
  • no-opaque
  • notations
  • ralf/acc
  • ralf/anomaly
  • ralf/call
  • ralf/old-asval
  • ralf/prophecy
  • ralf/sections-open
  • skiplist
  • strong_cas_fail
  • stuck
  • popl18
  • popl18-aec
49 results
Show changes
Hide whitespace changes
Inline Side-by-side
Showing
with 502 additions and 363 deletions
theories/lang/lib/spawn.v → lambda-rust/lang/lib/spawn.v
View file @ 0f4ebd6d
From iris.program_logic Require Import weakestpre.
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From iris.algebra Require Import excl.
From lrust.lang Require Import proofmode notation.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Definition spawn : val :=
λ: ["f"],
......@@ -28,15 +28,15 @@ Definition join : val :=
"join" ["c"].
(** The CMRA & functor we need. *)
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
Class spawnG Σ := SpawnG { spawn_tokG :: inG Σ (exclR unitO) }.
Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
Context `{!lrustGS Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(own γf (Excl ()) ∗ own γj (Excl ()) ∨
......@@ -70,7 +70,7 @@ Proof.
wp_let. wp_alloc l as "Hl" "H†". wp_let.
iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hl" as "[Hc Hd]". wp_write.
iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
{ iNext. iRight. iExists false. auto. }
......@@ -90,7 +90,7 @@ Proof.
auto. }
iDestruct "Hinv" as (b) "[>Hc _]". wp_write.
iMod ("Hclose" with "[-HΦ]").
- iNext. iRight. iExists true. iFrame. iExists _. iFrame.
- iNext. iRight. iExists true. iFrame.
- iModIntro. wp_seq. by iApply "HΦ".
Qed.
......@@ -111,7 +111,7 @@ Proof.
{ iNext. iLeft. iFrame. }
iModIntro. wp_if. wp_op. wp_read. wp_let.
iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
{ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. iFrame. }
wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
Qed.
......@@ -119,10 +119,10 @@ Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c :
□ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
Proof.
iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!# * ?".
iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!> * ?".
iApply "HΨ". iApply "HΨ'". done.
Qed.
End proof.
Typeclasses Opaque finish_handle join_handle.
Global Typeclasses Opaque finish_handle join_handle.
theories/lang/lib/swap.v → lambda-rust/lang/lib/swap.v
View file @ 0f4ebd6d
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Definition swap : val :=
rec: "swap" ["p1";"p2";"len"] :=
......@@ -10,7 +10,7 @@ Definition swap : val :=
"p2" <- "x";;
"swap" ["p1" +ₗ #1 ; "p2" +ₗ #1 ; "len" - #1].
Lemma wp_swap `{!lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
Lemma wp_swap `{!lrustGS Σ} E l1 l2 vl1 vl2 (n : Z):
Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
swap [ #l1; #l2; #n] @ E
......@@ -22,7 +22,7 @@ Proof.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_pointsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
wp_read; wp_let; wp_read; do 2 wp_write. do 3 wp_op.
......
theories/lang/lib/tests.v → lambda-rust/lang/lib/tests.v
View file @ 0f4ebd6d
From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.lang Require Import lang proofmode notation.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section tests.
Context `{!lrustG Σ}.
Context `{!lrustGS Σ}.
Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
{{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
......
theories/lang/lifting.v → lambda-rust/lang/lifting.v
View file @ 0f4ebd6d
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From lrust.lang Require Export lang heap.
From lrust.lang Require Import tactics.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Import uPred.
Class lrustG Σ := LRustG {
lrustG_invG : invG Σ;
lrustG_gen_heapG :> heapG Σ
Class lrustGS Σ := LRustGS {
lrustGS_invGS : invGS Σ;
lrustGS_heapGS :: heapGS Σ
}.
Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
iris_invG := lrustG_invG;
state_interp σ κs _ := heap_ctx σ;
Global Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
iris_invGS := lrustGS_invGS;
state_interp σ _ κs _ := heap_ctx σ;
fork_post _ := True%I;
num_laters_per_step _ := 0%nat;
state_interp_mono _ _ _ _ := fupd_intro _ _
}.
Global Opaque iris_invG.
Ltac inv_lit :=
repeat match goal with
......@@ -29,39 +30,39 @@ Ltac inv_bin_op_eval :=
| H : bin_op_eval _ ?c _ _ _ |- _ => is_constructor c; inversion H; clear H; simplify_eq/=
end.
Local Hint Extern 0 (atomic _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (atomic _) => solve_atomic : core.
Local Hint Extern 0 (base_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Constructors head_step bin_op_eval lit_neq lit_eq.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Local Hint Constructors base_step bin_op_eval lit_neq lit_eq : core.
Local Hint Resolve alloc_fresh : core.
Local Hint Resolve to_of_val : core.
Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
as_rec : e = Rec f xl erec.
Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
Instance AsRec_rec_locked_val v f xl e :
Global Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
Global Instance AsRec_rec_locked_val v f xl e :
AsRec (of_val v) f xl e → AsRec (of_val (locked v)) f xl e.
Proof. by unlock. Qed.
Class DoSubst (x : binder) (es : expr) (e er : expr) :=
do_subst : subst' x es e = er.
Hint Extern 0 (DoSubst _ _ _ _) =>
Global Hint Extern 0 (DoSubst _ _ _ _) =>
rewrite /DoSubst; simpl_subst; reflexivity : typeclass_instances.
Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
do_subst_l : subst_l xl esl e = Some er.
Instance do_subst_l_nil e : DoSubstL [] [] e e.
Global Instance do_subst_l_nil e : DoSubstL [] [] e e.
Proof. done. Qed.
Instance do_subst_l_cons x xl es esl e er er' :
Global Instance do_subst_l_cons x xl es esl e er er' :
DoSubstL xl esl e er' → DoSubst x es er' er →
DoSubstL (x :: xl) (es :: esl) e er.
Proof. rewrite /DoSubstL /DoSubst /= => -> <- //. Qed.
Instance do_subst_vec xl (vsl : vec val (length xl)) e :
Global Instance do_subst_vec xl (vsl : vec val (length xl)) e :
DoSubstL xl (of_val <$> vec_to_list vsl) e (subst_v xl vsl e).
Proof. by rewrite /DoSubstL subst_v_eq. Qed.
Section lifting.
Context `{!lrustG Σ}.
Context `{!lrustGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types e : expr.
Implicit Types ef : option expr.
......@@ -70,9 +71,9 @@ Implicit Types ef : option expr.
Lemma wp_fork E e :
{{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
Proof.
iIntros (?) "?HΦ". iApply wp_lift_atomic_head_step; [done|].
iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iFrame.
iIntros (?) "?HΦ". iApply wp_lift_atomic_base_step; [done|].
iIntros (σ1 κ ? κs n) "Hσ !>"; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step. iFrame.
iModIntro. by iApply "HΦ".
Qed.
......@@ -80,9 +81,9 @@ Qed.
Local Ltac solve_exec_safe :=
intros; destruct_and?; subst; do 3 eexists; econstructor; simpl; eauto with lia.
Local Ltac solve_exec_puredet :=
simpl; intros; destruct_and?; inv_head_step; inv_bin_op_eval; inv_lit; done.
simpl; intros; destruct_and?; inv_base_step; inv_bin_op_eval; inv_lit; done.
Local Ltac solve_pure_exec :=
intros ?; apply nsteps_once, pure_head_step_pure_step;
intros ?; apply nsteps_once, pure_base_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_rec e f xl erec erec' el :
......@@ -139,9 +140,9 @@ Lemma wp_alloc E (n : Z) :
{{{ True }}} Alloc (Lit $ LitInt n) @ E
{{{ l (sz: nat), RET LitV $ LitLoc l; ⌜n = sz⌝ ∗ †l…sz ∗ l ↦∗ repeat (LitV LitPoison) sz }}}.
Proof.
iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n') "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
iModIntro; iSplit=> //. iFrame.
iApply ("HΦ" $! _ (Z.to_nat n)). iFrame. iPureIntro. rewrite Z2Nat.id; lia.
......@@ -153,11 +154,11 @@ Lemma wp_free E (n:Z) l vl :
Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
{{{ RET LitV LitPoison; True }}}.
Proof.
iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ".
iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n') "Hσ".
iMod (heap_free _ _ _ n with "Hσ Hmt Hf") as "(% & % & Hσ)"=>//.
iModIntro; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto.
Qed.
......@@ -165,10 +166,10 @@ Lemma wp_read_sc E l q v :
{{{ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
{{{ RET v; l ↦{q} v }}}.
Proof.
iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -176,17 +177,17 @@ Lemma wp_read_na E l q v :
{{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
{{{ RET v; l ↦{q} v }}}.
Proof.
iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
iMod (heap_read_na with "Hσ Hv") as (n) "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
iIntros (Φ) ">Hv HΦ". iApply wp_lift_base_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iNext; iIntros (e2 σ2 efs Hstep) "_"; inv_base_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
clear dependent σ1 n.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_base_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
Qed.
......@@ -195,11 +196,11 @@ Lemma wp_write_sc E l e v v' :
{{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
{{{ RET LitV LitPoison; l ↦ v }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iMod (heap_write _ _ _ v with "Hσ Hv") as "[Hσ Hv]".
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -209,16 +210,16 @@ Lemma wp_write_na E l e v v' :
{{{ RET LitV LitPoison; l ↦ v }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ".
iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
iApply wp_lift_base_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iNext; iIntros (e2 σ2 efs Hstep) "_"; inv_base_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
clear dependent σ1. iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_base_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
Qed.
......@@ -229,10 +230,10 @@ Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
{{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
Proof.
iIntros (<- ? Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; inv_lit.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -243,10 +244,10 @@ Lemma wp_cas_suc E l lit1 e2 lit2 :
{{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
Proof.
iIntros (<- ? Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iModIntro; iSplit; first (destruct lit1; by eauto).
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; [inv_lit|].
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; [inv_lit|].
iMod (heap_write with "Hσ Hv") as "[$ Hv]".
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -273,12 +274,12 @@ Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
l ↦{q} LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
Proof.
iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; inv_lit.
iModIntro; iSplit=> //. iFrame. iApply "HΦ"; iFrame.
Qed.
......@@ -291,10 +292,10 @@ Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll) }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia.
iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; last lia.
- inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
iApply "HΦ"; simpl; auto.
- iMod (heap_write with "Hσ Hv") as "[$ Hv]".
......@@ -302,18 +303,19 @@ Proof.
Qed.
Lemma wp_eq_loc E (l1 : loc) (l2: loc) q1 q2 v1 v2 P Φ :
(P -∗ ▷ l1 ↦{q1} v1) →
(P -∗ ▷ l2 ↦{q2} v2) →
(P -∗ ▷ Φ (LitV (bool_decide (l1 = l2)))) →
P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
(P ⊢ ▷ l1 ↦{q1} v1) →
(P ⊢ ▷ l2 ↦{q2} v2) →
(P ⊢ ▷ Φ (LitV (bool_decide (l1 = l2)))) →
P ⊢ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
Proof.
iIntros (Hl1 Hl2 Hpost) "HP".
destruct (bool_decide_reflect (l1 = l2)) as [->|].
- iApply wp_lift_pure_det_head_step_no_fork';
- iApply wp_lift_pure_det_base_step_no_fork';
[done|solve_exec_safe|solve_exec_puredet|].
iApply wp_value. by iApply Hpost.
- iApply wp_lift_atomic_head_step_no_fork; subst=>//.
iIntros (σ1 ???) "Hσ1". iModIntro. inv_head_step.
iPoseProof (Hpost with "HP") as "?".
iIntros "!> _". by iApply wp_value.
- iApply wp_lift_atomic_base_step_no_fork; subst=>//.
iIntros (σ1 ? κ κs n') "Hσ1". iModIntro. inv_base_step.
iSplitR.
{ iPureIntro. repeat eexists. econstructor. eapply BinOpEqFalse. by auto. }
(* We need to do a little gymnastics here to apply Hne now and strip away a
......@@ -323,8 +325,8 @@ Proof.
+ iExists _, _. by iApply Hl1.
+ iExists _, _. by iApply Hl2.
+ by iApply Hpost. }
clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "!>".
inv_head_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "_ !>".
inv_base_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
+ iExFalso. iDestruct "HP" as "[Hl1 _]".
iDestruct "Hl1" as (??) "Hl1".
iDestruct (heap_read σ2 with "Hσ1 Hl1") as %[??]; simplify_eq.
......@@ -349,7 +351,7 @@ Proof.
change (App (of_val vf) ((of_val <$> vs) ++ e :: el)) with (fill_item (AppRCtx vf vs el) e).
iApply wp_bind. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
rewrite cons_middle (assoc app) -(fmap_app _ _ [v]).
iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
iApply (IH _ _ with "Hl"). iIntros "%vl Hvl". rewrite -assoc.
iApply ("HΦ" $! (v:::vl)). iFrame.
Qed.
......@@ -369,9 +371,9 @@ Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
WP App f el @ E {{ Φ }}.
Proof.
iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_of_list Ql).
iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_to_vec Ql).
generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
iApply (wp_app_vec with "Hel"). iIntros (vl) "Hvl".
iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
iApply ("HΦ" with "[%] Hvl"). by rewrite length_vec_to_list.
Qed.
End lifting.
theories/lang/notation.v → lambda-rust/lang/notation.v
View file @ 0f4ebd6d
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Coercion LitInt : Z >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
......@@ -35,6 +35,8 @@ Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
(at level 50, left associativity) : expr_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E)
(at level 70) : expr_scope.
Notation "e1 < e2" := (e1+#1 ≤ e2)%E
(at level 70) : expr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%E e2%E)
(at level 70) : expr_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
......@@ -59,10 +61,14 @@ Notation "λ: xl , e" := (Lam xl%binder e%E)
Notation "λ: xl , e" := (locked (LamV xl%binder e%E))
(at level 102, xl at level 1, e at level 200) : val_scope.
Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E
(only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope.
Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
(only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope.
Notation "'fnrec:' f xl := e" := (rec: f (BNamed "return"::xl) := e)%E
(at level 102, f, xl at level 1, e at level 200) : expr_scope.
Notation "'fnrec:' f xl := e" := (rec: f (BNamed "return"::xl) := e)%V
(at level 102, f, xl at level 1, e at level 200) : val_scope.
Notation "'fn:' xl := e" := (fnrec: <> xl := e)%E
(at level 102, xl at level 1, e at level 200) : expr_scope.
Notation "'fn:' xl := e" := (fnrec: <> xl := e)%V
(at level 102, xl at level 1, e at level 200) : val_scope.
Notation "'return:'" := "return" : expr_scope.
Notation "'let:' x := e1 'in' e2" :=
......@@ -84,7 +90,7 @@ Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
((Lam (@cons binder k1%binder nil) e1%E) [Rec k2%binder ((fun _ : eq k1%binder k2%binder => xl%binder) eq_refl) e2%E])
(only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], Endlft ;; k ["_r"]) args))%E
Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], k ["_r"]) args))%E
(only parsing, at level 102, f, args, k at level 1) : expr_scope.
Notation "'letcall:' x := f args 'in' e" :=
(letcont: "_k" [ x ] := e in call: f args → "_k")%E
......@@ -94,6 +100,6 @@ Notation "'letcall:' x := f args 'in' e" :=
we would even want them to print in general.
TODO: Introduce a Definition. *)
Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
(only parsing, at level 80, format "e1 <-{Σ i } ()" ) : expr_scope.
(only parsing, at level 80) : expr_scope.
Notation "e1 '<-{Σ' i } e2" := (e1 <-{Σ i} () ;; e1+ₗ#1 <- e2)%E
(at level 80, format "e1 <-{Σ i } e2") : expr_scope.
theories/lang/proofmode.v → lambda-rust/lang/proofmode.v
View file @ 0f4ebd6d
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Export tactics.
From lrust.lang Require Export tactics lifting.
From iris.proofmode Require Export proofmode.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting.
Set Default Proof Using "Type".
From lrust.lang Require Export tactics lifting.
From iris.prelude Require Import options.
Import uPred.
Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
Lemma tac_wp_value `{!lrustGS Σ} Δ E Φ e v :
IntoVal e v →
envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
Proof. rewrite envs_entails_unseal=> ? ->. by apply wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
Ltac wp_value_head := eapply tac_wp_value; [tc_solve|reduction.pm_prettify].
Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
Lemma tac_wp_pure `{!lrustGS Σ} K Δ Δ' E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
MaybeIntoLaterNEnvs n Δ Δ' →
envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite -wp_bind HΔ' -wp_pure_step_later //. by rewrite -wp_bind_inv.
rewrite envs_entails_unseal=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite -wp_bind HΔ' -wp_pure_step_later //. rewrite -wp_bind_inv.
f_equiv. apply wand_intro_l. by rewrite sep_elim_r.
Qed.
Tactic Notation "wp_pure" open_constr(efoc) :=
......@@ -30,22 +31,22 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
| |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
unify e' efoc;
eapply (tac_wp_pure K);
[simpl; iSolveTC (* PureExec *)
[simpl; tc_solve (* PureExec *)
|try done (* The pure condition for PureExec *)
|iSolveTC (* IntoLaters *)
|tc_solve (* IntoLaters *)
|simpl_subst; try wp_value_head (* new goal *)])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
| _ => fail "wp_pure: not a 'wp'"
end.
Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
Lemma tac_wp_eq_loc `{!lrustGS Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
envs_entails Δ' (WP fill K (Lit (bool_decide (l1 = l2))) @ E {{ Φ }}) →
envs_entails Δ (WP fill K (BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2))) @ E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ? /envs_lookup_sound /=. rewrite sep_elim_l=> ?.
rewrite envs_entails_unseal=> ? /envs_lookup_sound /=. rewrite sep_elim_l=> ?.
move /envs_lookup_sound; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind.
rewrite into_laterN_env_sound /=. eapply wp_eq_loc; eauto using later_mono.
Qed.
......@@ -55,7 +56,7 @@ Tactic Notation "wp_eq_loc" :=
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' => eapply (tac_wp_eq_loc K));
[iSolveTC|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
[tc_solve|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
| _ => fail "wp_pure: not a 'wp'"
end.
......@@ -67,10 +68,10 @@ Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
Tactic Notation "wp_if" := wp_pure (If _ _ _).
Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
Lemma tac_wp_bind `{!lrustGS Σ} K Δ E Φ e :
envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
Proof. rewrite envs_entails_unseal=> ->. apply: wp_bind. Qed.
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
......@@ -89,7 +90,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
end.
Section heap.
Context `{!lrustG Σ}.
Context `{!lrustGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (uPredI (iResUR Σ)).
......@@ -103,8 +104,8 @@ Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
envs_entails Δ'' (WP fill K (Lit $ LitLoc l) @ E {{ Φ }})) →
envs_entails Δ (WP fill K (Alloc (Lit $ LitInt n)) @ E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ?? HΔ. rewrite -wp_bind.
eapply wand_apply; first exact:wp_alloc.
rewrite envs_entails_unseal=> ?? HΔ. rewrite -wp_bind.
eapply wand_apply; first by apply wand_entails, wp_alloc.
rewrite -persistent_and_sep. apply and_intro; first by auto.
rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
......@@ -124,8 +125,8 @@ Lemma tac_wp_free K Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
envs_entails Δ''' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
envs_entails Δ (WP fill K (Free (Lit $ LitInt n) (Lit $ LitLoc l)) @ E {{ Φ }}).
Proof.
rewrite envs_entails_eq; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
eapply wand_apply; first exact:wp_free; simpl.
rewrite envs_entails_unseal; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
eapply wand_apply; first by apply wand_entails, wp_free; simpl.
rewrite into_laterN_env_sound -!later_sep; apply later_mono.
do 2 (rewrite envs_lookup_sound //). by rewrite HΔ True_emp emp_wand -assoc.
Qed.
......@@ -137,11 +138,11 @@ Lemma tac_wp_read K Δ Δ' E i l q v o Φ :
envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
envs_entails Δ (WP fill K (Read o (Lit $ LitLoc l)) @ E {{ Φ }}).
Proof.
rewrite envs_entails_eq; intros [->| ->] ???.
- rewrite -wp_bind. eapply wand_apply; first exact:wp_read_na.
rewrite envs_entails_unseal; intros [->| ->] ???.
- rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_read_na.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
- rewrite -wp_bind. eapply wand_apply; first exact:wp_read_sc.
- rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_read_sc.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -155,11 +156,11 @@ Lemma tac_wp_write K Δ Δ' Δ'' E i l v e v' o Φ :
envs_entails Δ'' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
envs_entails Δ (WP fill K (Write o (Lit $ LitLoc l) e) @ E {{ Φ }}).
Proof.
rewrite envs_entails_eq; intros ? [->| ->] ????.
- rewrite -wp_bind. eapply wand_apply; first by apply wp_write_na.
rewrite envs_entails_unseal; intros ? [->| ->] ????.
- rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_write_na.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
- rewrite -wp_bind. eapply wand_apply; first by apply wp_write_sc.
- rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_write_sc.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -185,7 +186,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc K _ _ _ H Hf))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
[try fast_done
|iSolveTC
|tc_solve
|let sz := fresh "sz" in let Hsz := fresh "Hsz" in
first [intros l sz Hsz | fail 1 "wp_alloc:" l "not fresh"];
(* If Hsz is "constant Z = nat", change that to an equation on nat and
......@@ -213,7 +214,7 @@ Tactic Notation "wp_free" :=
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_free K))
|fail 1 "wp_free: cannot find 'Free' in" e];
[try fast_done
|iSolveTC
|tc_solve
|let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
|pm_reflexivity
......@@ -234,7 +235,7 @@ Tactic Notation "wp_read" :=
|fail 1 "wp_read: cannot find 'Read' in" e];
[(right; fast_done) || (left; fast_done) ||
fail "wp_read: order is neither Na2Ord nor ScOrd"
|iSolveTC
|tc_solve
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
|simpl; try wp_value_head]
......@@ -246,11 +247,11 @@ Tactic Notation "wp_write" :=
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [iSolveTC|..])
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [tc_solve|..])
|fail 1 "wp_write: cannot find 'Write' in" e];
[(right; fast_done) || (left; fast_done) ||
fail "wp_write: order is neither Na2Ord nor ScOrd"
|iSolveTC
|tc_solve
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
|pm_reflexivity
......
theories/lang/races.v → lambda-rust/lang/races.v
View file @ 0f4ebd6d
From stdpp Require Import gmap.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import adequacy.
From lrust.lang Require Import tactics.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
(* This is a crucial definition; if we forget to sync it with head_step,
(* This is a crucial definition; if we forget to sync it with base_step,
the results proven here are worthless. *)
Inductive next_access_head : expr → state → access_kind * order → loc → Prop :=
| Access_read ord l σ :
......@@ -28,27 +27,27 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
σ (FreeAcc, Na2Ord) (l +ₗ i).
(* Some sanity checks to make sure the definition above is not entirely insensible. *)
Goal ∀ e1 e2 e3 σ, head_reducible (CAS e1 e2 e3) σ →
Goal ∀ e1 e2 e3 σ, base_reducible (CAS e1 e2 e3) σ →
∃ a l, next_access_head (CAS e1 e2 e3) σ a l.
Proof.
intros ??? σ (?&?&?&?&?). inversion H; do 2 eexists;
intros ??? σ (?&?&?&?&H). inversion H; do 2 eexists;
(eapply Access_cas_fail; done) || eapply Access_cas_suc; done.
Qed.
Goal ∀ o e σ, head_reducible (Read o e) σ →
Goal ∀ o e σ, base_reducible (Read o e) σ →
∃ a l, next_access_head (Read o e) σ a l.
Proof.
intros ?? σ (?&?&?&?&?). inversion H; do 2 eexists; eapply Access_read; done.
intros ?? σ (?&?&?&?&H). inversion H; do 2 eexists; eapply Access_read; done.
Qed.
Goal ∀ o e1 e2 σ, head_reducible (Write o e1 e2) σ →
Goal ∀ o e1 e2 σ, base_reducible (Write o e1 e2) σ →
∃ a l, next_access_head (Write o e1 e2) σ a l.
Proof.
intros ??? σ (?&?&?&?&?). inversion H; do 2 eexists;
intros ??? σ (?&?&?&?&H). inversion H; do 2 eexists;
eapply Access_write; try done; eexists; done.
Qed.
Goal ∀ e1 e2 σ, head_reducible (Free e1 e2) σ →
Goal ∀ e1 e2 σ, base_reducible (Free e1 e2) σ →
∃ a l, next_access_head (Free e1 e2) σ a l.
Proof.
intros ?? σ (?&?&?&?&?). inversion H; do 2 eexists; eapply Access_free; done.
intros ?? σ (?&?&?&?&H). inversion H; do 2 eexists; eapply Access_free; done.
Qed.
Definition next_access_thread (e: expr) (σ : state)
......@@ -71,20 +70,20 @@ Definition nonracing_threadpool (el : list expr) (σ : state) : Prop :=
∀ l a1 a2, next_accesses_threadpool el σ a1 a2 l →
nonracing_accesses a1 a2.
Lemma next_access_head_reductible_ctx e σ σ' a l K :
next_access_head e σ' a l → reducible (fill K e) σ → head_reducible e σ.
Lemma next_access_base_reductible_ctx e σ σ' a l K :
next_access_head e σ' a l → reducible (fill K e) σ → base_reducible e σ.
Proof.
intros Hhead Hred. apply prim_head_reducible.
- eapply (reducible_fill (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
intros Hhead Hred. apply prim_base_reducible.
- eapply (reducible_fill_inv (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
- apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hhead; eauto.
Qed.
Definition head_reduce_not_to_stuck (e : expr) (σ : state) :=
∀ κ e' σ' efs, ectx_language.head_step e σ κ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
Definition base_reduce_not_to_stuck (e : expr) (σ : state) :=
∀ κ e' σ' efs, ectx_language.base_step e σ κ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
Lemma next_access_head_reducible_state e σ a l :
next_access_head e σ a l → head_reducible e σ →
head_reduce_not_to_stuck e σ →
Lemma next_access_base_reducible_state e σ a l :
next_access_head e σ a l → base_reducible e σ →
base_reduce_not_to_stuck e σ →
match a with
| (ReadAcc, (ScOrd | Na1Ord)) => ∃ v n, σ !! l = Some (RSt n, v)
| (ReadAcc, Na2Ord) => ∃ v n, σ !! l = Some (RSt (S n), v)
......@@ -93,65 +92,70 @@ Lemma next_access_head_reducible_state e σ a l :
| (FreeAcc, _) => ∃ v ls, σ !! l = Some (ls, v)
end.
Proof.
intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
- destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_base_step; eauto.
- rename select nat into n.
destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
by eapply CasStuckS.
- exfalso. eapply Hrednonstuck; last done.
eapply CasStuckS; done.
- match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
- match goal with H : ∀ m, _ |- context[_ +ₗ ?i] => destruct (H i) as [_ [[]?]] end; eauto.
Qed.
Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
Lemma next_access_base_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
next_access_head e1 σ1 (a, Na1Ord) l →
head_step e1 σ1 κ e2 σ2 ef →
base_step e1 σ1 κ e2 σ2 ef →
next_access_head e2 σ2 (a, Na2Ord) l.
Proof.
intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor; by rewrite to_of_val.
intros Ha Hstep. inversion Ha; subst; clear Ha; inv_base_step; constructor; by rewrite to_of_val.
Qed.
Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
Lemma next_access_base_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
next_access_head e1 σ (a1, Na1Ord) l →
head_step e1 σ κ e1' σ' e'f →
base_step e1 σ κ e1' σ' e'f →
next_access_head e2 σ a2 l →
next_access_head e2 σ' a2 l.
Proof.
intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_base_step;
destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
(* Oh my. FIXME. *)
- eapply lit_eq_state; last done.
setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
rename select loc into l.
rename select state into σ.
cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
- eapply lit_eq_state; last done.
setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
rename select loc into l.
rename select state into σ.
cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
Qed.
Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
next_access_head e1 σ (FreeAcc, o1) l → head_step e1 σ κ e1' σ' e'f →
next_access_head e2 σ a2 l → head_reducible e2 σ' →
Lemma next_access_base_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
next_access_head e1 σ (FreeAcc, o1) l → base_step e1 σ κ e1' σ' e'f →
next_access_head e2 σ a2 l → base_reducible e2 σ' →
False.
Proof.
intros Ha1 Hstep Ha2 Hred2.
assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! (l +ₗ i) = None).
{ clear. intros l n i Hi.
replace n with (Z.of_nat (Z.to_nat n)) in Hi by (apply Z2Nat.id; lia).
revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi. lia.
revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi; first lia.
destruct (decide (i = 0)).
- subst. by rewrite /shift_loc Z.add_0_r -surjective_pairing lookup_delete.
- replace i with (1+(i-1)) by lia.
rewrite lookup_delete_ne -shift_loc_assoc ?IH //. lia.
destruct l; intros [=?]. lia. }
rewrite lookup_delete_ne -shift_loc_assoc ?IH //; first lia.
destruct l; intros [= ?]. lia. }
assert (FREE' : σ' !! l = None).
{ inversion Ha1; clear Ha1; inv_head_step. auto. }
{ inversion Ha1; clear Ha1; inv_base_step. auto. }
destruct Hred2 as (κ'&e2'&σ''&ef&?).
inversion Ha2; clear Ha2; inv_head_step.
inversion Ha2; clear Ha2; inv_base_step.
eapply (@is_Some_None (lock_state * val)). rewrite -FREE'. naive_solver.
Qed.
Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef κ :
(∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
e' ∈ el' → to_val e' = None → reducible e' σ') →
fill K e ∈ el → head_step e σ κ e' σ' ef → head_reduce_not_to_stuck e' σ'.
fill K e ∈ el → base_step e σ κ e' σ' ef → base_reduce_not_to_stuck e' σ'.
Proof.
intros Hsafe Hi Hstep κ1 e1 σ1 ? Hstep1 Hstuck.
cut (reducible (fill K e1) σ1).
......@@ -159,8 +163,8 @@ Proof.
destruct (elem_of_list_split _ _ Hi) as (?&?&->).
eapply Hsafe; last by (apply: fill_not_val; subst).
- eapply rtc_l, rtc_l, rtc_refl.
+ eexists. econstructor. done. done. econstructor; done.
+ eexists. econstructor. done. done. econstructor; done.
+ eexists. econstructor; [done..|]. econstructor; done.
+ eexists. econstructor; [done..|]. econstructor; done.
- subst. set_solver+.
Qed.
......@@ -168,7 +172,7 @@ Qed.
Lemma safe_not_reduce_to_stuck el σ K e :
(∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
e' ∈ el' → to_val e' = None → reducible e' σ') →
fill K e ∈ el → head_reduce_not_to_stuck e σ.
fill K e ∈ el → base_reduce_not_to_stuck e σ.
Proof.
intros Hsafe Hi κ e1 σ1 ? Hstep1 Hstuck.
cut (reducible (fill K e1) σ1).
......@@ -176,7 +180,7 @@ Proof.
destruct (elem_of_list_split _ _ Hi) as (?&?&->).
eapply Hsafe; last by (apply: fill_not_val; subst).
- eapply rtc_l, rtc_refl.
+ eexists. econstructor. done. done. econstructor; done.
+ eexists. econstructor; [done..|]. econstructor; done.
- subst. set_solver+.
Qed.
......@@ -187,90 +191,94 @@ Theorem safe_nonracing el σ :
Proof.
intros Hsafe l a1 a2 (t1&?&t2&?&t3&->&(K1&e1&Ha1&->)&(K2&e2&Ha2&->)).
assert (to_val e1 = None). by destruct Ha1.
assert (Hrede1:head_reducible e1 σ).
{ eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
assert (to_val e1 = None) by by destruct Ha1.
assert (Hrede1:base_reducible e1 σ).
{ eapply (next_access_base_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
abstract set_solver. }
assert (Hnse1:head_reduce_not_to_stuck e1 σ).
{ eapply safe_not_reduce_to_stuck with (K:=K1); first done. set_solver+. }
assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
assert (Hnse1:base_reduce_not_to_stuck e1 σ).
{ eapply (safe_not_reduce_to_stuck _ _ K1); first done. set_solver+. }
assert (Hσe1:=next_access_base_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
destruct Hrede1 as (κ1'&e1'&σ1'&ef1&Hstep1). clear Hnse1.
assert (Ha1' : a1.2 = Na1Ord → next_access_head e1' σ1' (a1.1, Na2Ord) l).
{ intros. eapply next_access_head_Na1Ord_step, Hstep1.
{ intros. eapply next_access_base_Na1Ord_step, Hstep1.
by destruct a1; simpl in *; subst. }
assert (Hrtc_step1:
rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
(t1 ++ fill K1 e1' :: t2 ++ fill K2 e2 :: t3 ++ ef1, σ1')).
{ eapply rtc_l, rtc_refl. eexists. eapply step_atomic, Ectx_step, Hstep1; try done.
by rewrite -assoc. }
assert (Hrede1: a1.2 = Na1Ord → head_reducible e1' σ1').
assert (Hrede1: a1.2 = Na1Ord → base_reducible e1' σ1').
{ destruct a1 as [a1 []]=>// _.
eapply (next_access_head_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
eapply (next_access_base_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
fill_not_val=>//.
by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
{ eapply safe_step_not_reduce_to_stuck with (K:=K1); first done; last done. set_solver+. }
- by auto.
- abstract set_solver.
- by destruct Hstep1; inversion Ha1. }
assert (Hnse1: base_reduce_not_to_stuck e1' σ1').
{ eapply (safe_step_not_reduce_to_stuck _ _ K1); first done; last done. set_solver+. }
assert (to_val e2 = None). by destruct Ha2.
assert (Hrede2:head_reducible e2 σ).
{ eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
assert (to_val e2 = None) by by destruct Ha2.
assert (Hrede2:base_reducible e2 σ).
{ eapply (next_access_base_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
abstract set_solver. }
assert (Hnse2:head_reduce_not_to_stuck e2 σ).
{ eapply safe_not_reduce_to_stuck with (K:=K2); first done. set_solver+. }
assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
assert (Hnse2:base_reduce_not_to_stuck e2 σ).
{ eapply (safe_not_reduce_to_stuck _ _ K2); first done. set_solver+. }
assert (Hσe2:=next_access_base_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
destruct Hrede2 as (κ2'&e2'&σ2'&ef2&Hstep2).
assert (Ha2' : a2.2 = Na1Ord → next_access_head e2' σ2' (a2.1, Na2Ord) l).
{ intros. eapply next_access_head_Na1Ord_step, Hstep2.
{ intros. eapply next_access_base_Na1Ord_step, Hstep2.
by destruct a2; simpl in *; subst. }
assert (Hrtc_step2:
rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
(t1 ++ fill K1 e1 :: t2 ++ fill K2 e2' :: t3 ++ ef2, σ2')).
{ eapply rtc_l, rtc_refl. rewrite app_comm_cons assoc. eexists.
eapply step_atomic, Ectx_step, Hstep2; try done. by rewrite -assoc. }
assert (Hrede2: a2.2 = Na1Ord → head_reducible e2' σ2').
assert (Hrede2: a2.2 = Na1Ord → base_reducible e2' σ2').
{ destruct a2 as [a2 []]=>// _.
eapply (next_access_head_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
eapply (next_access_base_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
fill_not_val=>//.
by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
{ eapply safe_step_not_reduce_to_stuck with (K:=K2); first done; last done. set_solver+. }
- by auto.
- abstract set_solver.
- by destruct Hstep2; inversion Ha2. }
assert (Hnse2':base_reduce_not_to_stuck e2' σ2').
{ eapply (safe_step_not_reduce_to_stuck _ _ K2); first done; last done. set_solver+. }
assert (Ha1'2 : a1.2 = Na1Ord → next_access_head e2 σ1' a2 l).
{ intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
{ intros HNa. eapply next_access_base_Na1Ord_concurent_step=>//.
by rewrite <-HNa, <-surjective_pairing. }
assert (Hrede1_2: head_reducible e2 σ1').
{ intros. eapply (next_access_head_reductible_ctx e2 σ1' σ a2 l K2), Hsafe, fill_not_val=>//.
assert (Hrede1_2: base_reducible e2 σ1').
{ intros. eapply (next_access_base_reductible_ctx e2 σ1' σ a2 l K2), Hsafe, fill_not_val=>//.
abstract set_solver. }
assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
{ eapply safe_not_reduce_to_stuck with (K:=K2).
- intros. eapply Hsafe. etrans; last done. done. done. done.
assert (Hnse1_2:base_reduce_not_to_stuck e2 σ1').
{ eapply (safe_not_reduce_to_stuck _ _ K2).
- intros. eapply Hsafe; [|done..]. etrans; last done. done.
- set_solver+. }
assert (Hσe1'1:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
λ Hord, next_access_base_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
assert (Hσe1'2:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
λ Hord, next_access_base_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
assert (Ha2'1 : a2.2 = Na1Ord → next_access_head e1 σ2' a1 l).
{ intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
{ intros HNa. eapply next_access_base_Na1Ord_concurent_step=>//.
by rewrite <-HNa, <-surjective_pairing. }
assert (Hrede2_1: head_reducible e1 σ2').
{ intros. eapply (next_access_head_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
assert (Hrede2_1: base_reducible e1 σ2').
{ intros. eapply (next_access_base_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
abstract set_solver. }
assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
{ eapply safe_not_reduce_to_stuck with (K:=K1).
- intros. eapply Hsafe. etrans; last done. done. done. done.
assert (Hnse2_1:base_reduce_not_to_stuck e1 σ2').
{ eapply (safe_not_reduce_to_stuck _ _ K1).
- intros. eapply Hsafe; [|done..]. etrans; last done. done.
- set_solver+. }
assert (Hσe2'1:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
λ Hord, next_access_base_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
assert (Hσe2'2:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
λ Hord, next_access_base_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
assert (a1.1 = FreeAcc → False).
{ destruct a1 as [[]?]; inversion 1.
eauto using next_access_head_Free_concurent_step. }
eauto using next_access_base_Free_concurent_step. }
assert (a2.1 = FreeAcc → False).
{ destruct a2 as [[]?]; inversion 1.
eauto using next_access_head_Free_concurent_step. }
eauto using next_access_base_Free_concurent_step. }
destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
repeat match goal with
......@@ -282,9 +290,9 @@ Proof.
clear κ2' e2' Hnse2' Hnse2_1 Hstep2 σ2' Hrtc_step2 Hrede2_1.
destruct Hrede1_2 as (κ2'&e2'&σ'&ef&?).
inv_head_step.
inv_base_step.
match goal with
| H : <[l:=_]> σ !! l = _ |- _ => by rewrite lookup_insert in H
| H : <[?l:=_]> ?σ !! ?l = _ |- _ => by rewrite lookup_insert in H
end.
Qed.
......@@ -294,6 +302,7 @@ Corollary adequate_nonracing e1 t2 σ1 σ2 φ :
nonracing_threadpool t2 σ2.
Proof.
intros [_ Had] Hrtc. apply safe_nonracing. intros el' σ' e' ?? He'.
edestruct (Had el' σ' e') as [He''|]; try done. etrans; eassumption.
rewrite /language.to_val /= He' in He''. by edestruct @is_Some_None.
edestruct (Had el' σ' e') as [He''|]; try done.
- etrans; eassumption.
- rewrite /language.to_val /= He' in He''. by edestruct @is_Some_None.
Qed.
theories/lang/tactics.v → lambda-rust/lang/tactics.v
View file @ 0f4ebd6d
From stdpp Require Import fin_maps.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
(** We define an alternative representation of expressions in which the
embedding of values and closed expressions is explicit. By reification of
......@@ -87,10 +87,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
end.
Lemma is_closed_correct X e : is_closed X e → lang.is_closed X (to_expr e).
Proof.
revert e X. fix FIX 1; destruct e=>/=;
revert e X. fix FIX 1; intros e; destruct e=>/=;
try naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
- induction el=>/=; naive_solver.
- induction el=>/=; naive_solver.
- rename select (list expr) into el. induction el=>/=; naive_solver.
- rename select (list expr) into el. induction el=>/=; naive_solver.
Qed.
(* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
......@@ -139,10 +139,10 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
Lemma to_expr_subst x er e :
to_expr (subst x er e) = lang.subst x (to_expr er) (to_expr e).
Proof.
revert e x er. fix FIX 1; destruct e=>/= ? er; repeat case_bool_decide;
revert e x er. fix FIX 1; intros e; destruct e=>/= ? er; repeat case_bool_decide;
f_equal; eauto using is_closed_nil_subst, is_closed_to_val, eq_sym.
- induction el=>//=. f_equal; auto.
- induction el=>//=. f_equal; auto.
- rename select (list expr) into el. induction el=>//=. f_equal; auto.
- rename select (list expr) into el. induction el=>//=. f_equal; auto.
Qed.
Definition is_atomic (e: expr) : bool :=
......@@ -157,7 +157,7 @@ Definition is_atomic (e: expr) : bool :=
Lemma is_atomic_correct e : is_atomic e → Atomic WeaklyAtomic (to_expr e).
Proof.
intros He. apply ectx_language_atomic.
- intros σ e' σ' ef.
- intros σ ef e' σ'.
destruct e; simpl; try done; repeat (case_match; try done);
inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
......@@ -175,7 +175,7 @@ Ltac solve_closed :=
let e' := W.of_expr e in change (Closed X (W.to_expr e'));
apply W.is_closed_correct; vm_compute; exact I
end.
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Global Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Ltac solve_into_val :=
match goal with
......@@ -184,7 +184,7 @@ Ltac solve_into_val :=
apply W.to_val_Some; simpl; unfold W.to_expr;
((unlock; exact eq_refl) || (idtac; exact eq_refl))
end.
Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
Global Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
Ltac solve_as_val :=
match goal with
......@@ -192,7 +192,7 @@ Ltac solve_as_val :=
let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end.
Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
Global Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
Ltac solve_atomic :=
match goal with
......@@ -200,7 +200,24 @@ Ltac solve_atomic :=
let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
apply W.is_atomic_correct; vm_compute; exact I
end.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
Global Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
Global Instance skip_atomic : Atomic WeaklyAtomic Skip.
Proof.
apply strongly_atomic_atomic, ectx_language_atomic.
- inversion 1. naive_solver.
- apply ectxi_language_sub_redexes_are_values. intros [] * Hskip; try naive_solver.
+ inversion Hskip. simpl. rewrite decide_True_pi. eauto.
+ inversion Hskip. rename select ([Lit _] = _) into Hargs.
assert (length [Lit LitPoison] = 1%nat) as Hlen by done. move:Hlen.
rewrite Hargs. rewrite length_app length_fmap /=.
rename select (list val) into vl. rename select (list expr) into el.
destruct vl; last first.
{ simpl. intros. exfalso. lia. }
destruct el; last first.
{ simpl. intros. exfalso. lia. }
simpl in *. intros _. inversion Hargs. eauto.
Qed.
(** Substitution *)
Ltac simpl_subst :=
......@@ -212,15 +229,15 @@ Ltac simpl_subst :=
rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
end;
unfold W.to_expr; simpl.
Arguments W.to_expr : simpl never.
Arguments subst : simpl never.
Global Arguments W.to_expr : simpl never.
Global Arguments subst : simpl never.
(** The tactic [inv_head_step] performs inversion on hypotheses of the
shape [head_step]. The tactic will discharge head-reductions starting
(** The tactic [inv_base_step] performs inversion on hypotheses of the
shape [base_step]. The tactic will discharge head-reductions starting
from values, and simplifies hypothesis related to conversions from and
to values, and finite map operations. This tactic is slightly ad-hoc
and tuned for proving our lifting lemmas. *)
Ltac inv_head_step :=
Ltac inv_base_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
......@@ -228,7 +245,7 @@ Ltac inv_head_step :=
apply (f_equal (to_val)) in H; rewrite to_of_val in H;
injection H; clear H; intro
| H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
| H : head_step ?e _ _ _ _ _ |- _ =>
| H : base_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
......
theories/typing/base.v → lambda-rust/typing/base.v
View file @ 0f4ebd6d
From stdpp Require Import namespaces.
From lrust.lang Require Export proofmode.
From lrust.lifetime Require Export frac_borrow.
From iris.prelude Require Import options.
(* Last, so that we make sure we shadow the defintion of delete for
sets coming from the prelude. *)
From lrust.lang.lib Require Export new_delete.
Global Open Scope Z_scope.
Definition lft_userN : namespace := nroot .@ "lft_usr".
(* The "user mask" of the lifetime logic. This needs to be disjoint with ↑lftN.
If a client library desires to put invariants in lft_userE, then it is
encouraged to place it in the already defined lft_userN. On the other hand,
extensions to the model of RustBelt itself (such as gpfsl for
the weak-mem extension) can require extending [lft_userE] with the relevant
namespaces. In that case all client libraries need to be re-checked to
ensure disjointness of [lft_userE] with their masks is maintained where
necessary. *)
Definition lft_userE : coPset := ↑lft_userN.
Create HintDb lrust_typing.
Create HintDb lrust_typing_merge.
......@@ -14,18 +34,18 @@ Ltac solve_typing :=
(typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
(typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
Global Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
Global Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
: lrust_typing.
Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
Global Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
(etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : lrust_typing.
Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
Global Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
(etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
Hint Resolve <- elem_of_app : lrust_typing.
Global Hint Resolve <- elem_of_app : lrust_typing.
(* done is there to handle equalities with constants *)
Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
\ No newline at end of file
Global Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
Global Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
Global Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
theories/typing/bool.v → lambda-rust/typing/bool.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import programs.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section bool.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Program Definition bool : type :=
{| st_own tid vl :=
......@@ -22,11 +22,11 @@ Section bool.
End bool.
Section typing.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
Proof.
iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
iIntros (E L tid ?) "_ _ $ $ _". iApply wp_value.
rewrite tctx_interp_singleton tctx_hasty_val' //. by destruct b.
Qed.
......@@ -41,7 +41,7 @@ Section typing.
typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
typed_body E L C T (if: p then e1 else e2).
Proof.
iIntros (Hp) "He1 He2". iIntros (tid) "#LFT #HE Htl HL HC HT".
iIntros (Hp) "He1 He2". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
wp_bind p. iApply (wp_hasty with "Hp").
iIntros ([[| |[|[]|]]|]) "_ H1"; try done; wp_case.
......
theories/typing/borrow.v → lambda-rust/typing/borrow.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.lang Require Import proofmode.
From lrust.typing Require Export uniq_bor shr_bor own.
From lrust.typing Require Import lft_contexts type_context programs.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
(** The rules for borrowing and derferencing borrowed non-Copy pointers are in
a separate file so make sure that own.v and uniq_bor.v can be compiled
concurrently. *)
Section borrow.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Lemma tctx_borrow E L p n ty κ :
tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
Proof.
iIntros (tid ?) "#LFT _ $ [H _]".
iIntros (tid ??) "#LFT _ $ [H _]".
iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
iMod (bor_create with "LFT Hmt") as "[Hbor Hext]"; first done.
iModIntro. rewrite /tctx_interp /=. iSplitL "Hbor"; last iSplit; last done.
- iExists _. auto.
- iExists _. iSplit. done. by iFrame.
- iExists _. iSplit; first done. by iFrame.
Qed.
Lemma tctx_share E L p κ ty :
lctx_lft_alive E L κ → tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &shr{κ}ty].
Proof.
iIntros (Hκ ??) "#LFT #HE HL Huniq".
iIntros (Hκ ???) "#LFT #HE HL Huniq".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
rewrite !tctx_interp_singleton /=.
iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
......@@ -69,7 +69,8 @@ Section borrow.
((p ◁{κ} own_ptr n ty)::T).
Proof.
intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
by apply tctx_borrow. by f_equiv.
- by apply tctx_borrow.
- by f_equiv.
Qed.
(* See the comment above [tctx_extract_hasty_share]. *)
......@@ -84,23 +85,25 @@ Section borrow.
Lemma type_deref_uniq_own_instr {E L} κ p n ty :
lctx_lft_alive E L κ →
typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ tid) "#LFT HE $ HL Hp".
iIntros (Hκ tid qmax) "#LFT HE $ HL Hp".
rewrite tctx_interp_singleton.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
wp_apply (wp_hasty with "Hp"). iIntros ([[|l|]|]) "_ Hown"; try done.
iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']"; first done.
iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
iDestruct "Hown" as "[Hown H†]". rewrite heap_pointsto_vec_singleton -wp_fupd. wp_read.
iMod ("Hclose'" $! (l↦#l' ∗ freeable_sz n (ty_size ty) l' ∗ _)%I
with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
iMod ("Hclose" with "Htok") as "($ & $)".
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]"; first done.
iMod (bor_sep with "LFT Hbor") as "[_ Hbor]"; first done.
iMod ("Hclose" with "Htok") as "HL".
iDestruct ("HLclose" with "HL") as "$".
by rewrite tctx_interp_singleton tctx_hasty_val' //=.
- iIntros "!>(?&?&?)!>". iNext. iExists _.
rewrite -heap_mapsto_vec_singleton. iFrame. by iFrame.
rewrite -heap_pointsto_vec_singleton. iFrame. by iFrame.
- iFrame.
Qed.
......@@ -114,19 +117,21 @@ Section borrow.
Lemma type_deref_shr_own_instr {E L} κ p n ty :
lctx_lft_alive E L κ →
typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
⊢ typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
Proof.
iIntros (Hκ tid) "#LFT HE $ HL Hp".
iIntros (Hκ tid qmax) "#LFT HE $ HL Hp".
rewrite tctx_interp_singleton.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iDestruct "Hown" as (l') "#[H↦b #Hown]".
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']"; first done.
iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
iMod ("Hclose" with "[Htok1 Htok2]") as "HL"; first by iFrame.
iDestruct ("HLclose" with "HL") as "$".
rewrite tctx_interp_singleton tctx_hasty_val' //. auto.
Qed.
......@@ -140,26 +145,28 @@ Section borrow.
Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
iIntros (Hκ Hincl tid qmax) "#LFT #HE $ HL Hp".
rewrite tctx_interp_singleton.
iDestruct (Hincl with "HL HE") as "#Hincl".
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iDestruct (Hincl with "HL HE") as "%".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
iMod (bor_exists with "LFT Hown") as (vl) "Hbor"; first done.
iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]"; first done.
destruct vl as [|[[]|][]];
try by iMod (bor_persistent with "LFT Hbor Htok") as "[>[] _]".
iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
rewrite heap_mapsto_vec_singleton.
iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']"; first done.
rewrite heap_pointsto_vec_singleton.
iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
iApply wp_fupd. wp_read.
iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
iMod ("Hclose" with "Htok") as "($ & $)".
iMod ("Hclose" with "Htok") as "HL".
iDestruct ("HLclose" with "HL") as "$".
rewrite tctx_interp_singleton tctx_hasty_val' //.
iApply (bor_shorten with "[] Hbor").
iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
iApply lft_incl_glb; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
Qed.
Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
......@@ -172,25 +179,29 @@ Section borrow.
Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
⊢ typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
Proof.
iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
iDestruct (Hincl with "HL HE") as "#Hincl".
iIntros (Hκ Hincl tid qmax) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iDestruct (Hincl with "HL HE") as "%".
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
iDestruct "Hshr" as (l') "[H↦ Hown]".
iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']"; first done.
iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
{ iApply lft_incl_glb.
+ by iApply lft_incl_syn_sem.
+ by iApply lft_incl_refl. }
iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']"; first solve_ndisj.
iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose''" with "Htok2") as "Htok2".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
rewrite tctx_interp_singleton tctx_hasty_val' //.
by iApply (ty_shr_mono with "Hincl' Hshr").
{ iApply ("Hown" with "[%] Htok2"); first solve_ndisj. }
iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose''" with "Htok2") as "Htok2".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "HL"; first by iFrame.
iDestruct ("HLclose" with "HL") as "$".
rewrite tctx_interp_singleton tctx_hasty_val' //.
by iApply (ty_shr_mono with "Hincl' Hshr").
Qed.
Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
......@@ -202,7 +213,7 @@ Section borrow.
Proof. iIntros. iApply type_let; [by apply type_deref_shr_uniq_instr|solve_typing|done]. Qed.
End borrow.
Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
Global Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
| 10 : lrust_typing.
Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.
Global Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
Global Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.
theories/typing/cont.v → lambda-rust/typing/cont.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import programs.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section typing.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
(** Jumping to and defining a continuation. *)
Lemma type_jump args argsv E L C T k T' :
......@@ -14,14 +14,16 @@ Section typing.
Forall2 (λ a av, to_val a = Some av ∨ a = of_val av) args argsv →
k ◁cont(L, T') ∈ C →
tctx_incl E L T (T' (list_to_vec argsv)) →
typed_body E L C T (k args).
⊢ typed_body E L C T (k args).
Proof.
iIntros (Hargs HC Hincl tid) "#LFT #HE Hna HL HC HT".
iIntros (Hargs HC Hincl tid qmax) "#LFT #HE Hna HL HC HT".
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iMod (Hincl with "LFT HE HL HT") as "(HL & HT)".
iSpecialize ("HC" with "[]"); first done.
iDestruct ("HLclose" with "HL") as "HL".
assert (args = of_val <$> argsv) as ->.
{ clear -Hargs. induction Hargs as [|a av ?? [<-%of_to_val| ->] _ ->]=>//=. }
rewrite -{3}(vec_to_list_of_list argsv). iApply ("HC" with "Hna HL HT").
rewrite -{3}(vec_to_list_to_vec argsv). iApply ("HC" with "Hna HL HT").
Qed.
Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
......@@ -32,7 +34,7 @@ Section typing.
(subst_v (kb::argsb) (k:::args) econt)) -∗
typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
wp_let. iApply ("He2" with "LFT HE Htl HL [HC] HT").
iLöb as "IH". iIntros (x) "H".
......@@ -48,7 +50,7 @@ Section typing.
typed_body E L1 C (T' args) (subst_v (kb :: argsb) (k:::args) econt)) -∗
typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
wp_let. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
iIntros (x) "H".
......
theories/typing/cont_context.v → lambda-rust/typing/cont_context.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.lang Require Import notation.
From lrust.typing Require Import type lft_contexts type_context.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section cont_context_def.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Definition cont_postcondition : iProp Σ := True%I.
......@@ -20,21 +20,21 @@ Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T)
(at level 70, format "k ◁cont( L , T )").
Section cont_context.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
Definition cctx_elt_interp (tid : thread_id) (qmax: Qp) (x : cctx_elt) : iProp Σ :=
let '(k ◁cont(L, T)) := x in
(∀ args, na_own tid top -∗ llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
(∀ args, na_own tid top -∗ llctx_interp qmax L -∗ tctx_interp tid (T args) -∗
WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
(∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid x)%I.
Definition cctx_interp (tid : thread_id) (qmax: Qp) (C : cctx) : iProp Σ :=
(∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid qmax x)%I.
Global Instance cctx_interp_permut tid:
Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid).
Global Instance cctx_interp_permut tid qmax :
Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid qmax).
Proof. solve_proper. Qed.
Lemma cctx_interp_cons tid x T :
cctx_interp tid (x :: T) ≡ (cctx_elt_interp tid x ∧ cctx_interp tid T)%I.
Lemma cctx_interp_cons tid qmax x T :
cctx_interp tid qmax (x :: T) ≡ (cctx_elt_interp tid qmax x ∧ cctx_interp tid qmax T)%I.
Proof.
iSplit.
- iIntros "H". iSplit; [|iIntros (??)]; iApply "H"; rewrite elem_of_cons; auto.
......@@ -43,22 +43,22 @@ Section cont_context.
+ iDestruct "H" as "[_ H]". by iApply "H".
Qed.
Lemma cctx_interp_nil tid : cctx_interp tid [] ≡ True%I.
Lemma cctx_interp_nil tid qmax : cctx_interp tid qmax [] ≡ True%I.
Proof. iSplit; first by auto. iIntros "_". iIntros (? Hin). inversion Hin. Qed.
Lemma cctx_interp_app tid T1 T2 :
cctx_interp tid (T1 ++ T2) ≡ (cctx_interp tid T1 ∧ cctx_interp tid T2)%I.
Lemma cctx_interp_app tid qmax T1 T2 :
cctx_interp tid qmax (T1 ++ T2) ≡ (cctx_interp tid qmax T1 ∧ cctx_interp tid qmax T2)%I.
Proof.
induction T1 as [|?? IH]; first by rewrite /= cctx_interp_nil left_id.
by rewrite /= !cctx_interp_cons IH assoc.
Qed.
Lemma cctx_interp_singleton tid x :
cctx_interp tid [x] ≡ cctx_elt_interp tid x.
Lemma cctx_interp_singleton tid qmax x :
cctx_interp tid qmax [x] ≡ cctx_elt_interp tid qmax x.
Proof. rewrite cctx_interp_cons cctx_interp_nil right_id //. Qed.
Lemma fupd_cctx_interp tid C :
(|={⊤}=> cctx_interp tid C) -∗ cctx_interp tid C.
Lemma fupd_cctx_interp tid qmax C :
(|={⊤}=> cctx_interp tid qmax C) -∗ cctx_interp tid qmax C.
Proof.
rewrite /cctx_interp. iIntros "H". iIntros ([k L n T]) "%".
iIntros (args) "HL HT". iMod "H".
......@@ -66,30 +66,32 @@ Section cont_context.
Qed.
Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
∀ tid, lft_ctx -∗ elctx_interp E -∗ cctx_interp tid C1 -∗ cctx_interp tid C2.
∀ tid qmax, lft_ctx -∗ elctx_interp E -∗ cctx_interp tid qmax C1 -∗ cctx_interp tid qmax C2.
Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
Proof.
split.
- iIntros (??) "_ _ $".
- iIntros (??? H1 H2 ?) "#LFT #HE HC".
- iIntros (???) "_ _ $".
- iIntros (??? H1 H2 ??) "#LFT #HE HC".
iApply (H2 with "LFT HE"). by iApply (H1 with "LFT HE").
Qed.
Lemma incl_cctx_incl E C1 C2 : C1 ⊆ C2 → cctx_incl E C2 C1.
Proof.
rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid) "_ #HE H * %".
rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid ?) "_ #HE H * %".
iApply ("H" with "[%]"). by apply HC1C2.
Qed.
Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n → tctx) C1 C2 :
Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
cctx_incl E (k ◁cont(L, T1) :: C1) (k ◁cont(L, T2) :: C2).
Proof.
iIntros (HC1C2 HT1T2 ?) "#LFT #HE H". rewrite /cctx_interp.
iIntros (HC1C2 HT1T2 ??) "#LFT #HE H". rewrite /cctx_interp.
iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
- iIntros (args) "Htl HL HT".
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iMod (HT1T2 with "LFT HE HL HT") as "(HL & HT)".
iDestruct ("HLclose" with "HL") as "HL".
iApply ("H" $! (_ ◁cont(_, _)) with "[%] Htl HL HT").
constructor.
- iApply (HC1C2 with "LFT HE [H] [%]"); last done.
......@@ -99,18 +101,19 @@ Section cont_context.
Lemma cctx_incl_nil E C : cctx_incl E C [].
Proof. apply incl_cctx_incl. by set_unfold. Qed.
Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
(* Extra strong cctx inclusion rule that we do not have on paper. *)
Lemma cctx_incl_cons_dup E k L n (T1 T2 : vec val n → tctx) C1 C2 :
k ◁cont(L, T1) ∈ C1 →
(∀ args, tctx_incl E L (T2 args) (T1 args)) →
cctx_incl E C1 C2 →
cctx_incl E C1 (k ◁cont(L, T2) :: C2).
Proof.
intros Hin ??. rewrite <-cctx_incl_cons_match; try done.
iIntros (?) "_ #HE HC".
intros Hin ??. rewrite <-cctx_incl_cons; try done.
clear -Hin. iIntros (??) "_ #HE HC".
rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
[iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
Qed.
End cont_context.
Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
Global Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
lambda-rust/typing/examples/fixpoint.v 0 → 100644
View file @ 0f4ebd6d
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
From iris.prelude Require Import options.
Section fixpoint.
Context `{!typeGS Σ}.
Local Definition my_list_pre l : type := sum [ unit; box l].
Local Instance my_list_contractive : TypeContractive my_list_pre.
Proof.
(* FIXME: solve_type_proper should handle this. *)
intros n l1 l2 Hl. rewrite /my_list_pre.
f_equiv. constructor; last constructor; last by constructor.
- done.
- f_equiv. done.
Qed.
Definition my_list := type_fixpoint my_list_pre.
Local Lemma my_list_unfold :
my_list ≡ my_list_pre my_list.
Proof. apply type_fixpoint_unfold. Qed.
Lemma my_list_size : my_list.(ty_size) = 2%nat.
Proof. rewrite my_list_unfold. done. Qed.
End fixpoint.
theories/typing/examples/get_x.v → lambda-rust/typing/examples/get_x.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section get_x.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Definition get_x : val :=
funrec: <> ["p"] :=
fn: ["p"] :=
let: "p'" := !"p" in
letalloc: "r" <- "p'" +ₗ #0 in
delete [ #1; "p"] ;; return: ["r"].
......@@ -14,7 +14,7 @@ Section get_x.
Lemma get_x_type :
typed_val get_x (fn(∀ α, ∅; &uniq{α}(Π[int; int])) → &shr{α}int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>". iIntros (α ϝ ret p).
inv_vec p=>p. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
......
theories/typing/examples/init_prod.v → lambda-rust/typing/examples/init_prod.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section init_prod.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Definition init_prod : val :=
funrec: <> ["x"; "y"] :=
fn: ["x"; "y"] :=
let: "x'" := !"x" in let: "y'" := !"y" in
let: "r" := new [ #2] in
"r" +ₗ #0 <- "x'";; "r" +ₗ #1 <- "y'";;
......@@ -14,7 +14,7 @@ Section init_prod.
Lemma init_prod_type : typed_val init_prod (fn(∅; int, int) → Π[int;int]).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([] ϝ ret p). inv_vec p=>x y. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
......
theories/typing/examples/lazy_lft.v → lambda-rust/typing/examples/lazy_lft.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section lazy_lft.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Definition lazy_lft : val :=
funrec: <> [] :=
fn: [] :=
Newlft;;
let: "t" := new [ #2] in let: "f" := new [ #1] in let: "g" := new [ #1] in
let: "42" := #42 in "f" <- "42";;
......@@ -19,7 +19,7 @@ Section lazy_lft.
Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([] ϝ ret p). inv_vec p. simpl_subst.
iApply (type_newlft []). iIntros (α).
iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
......
theories/typing/examples/nonlexical.v → lambda-rust/typing/examples/nonlexical.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing lib.option.
From iris.prelude Require Import options.
(* Typing "problem case #3" from:
http://smallcultfollowing.com/babysteps/blog/2016/04/27/non-lexical-lifetimes-introduction/
......@@ -13,7 +14,7 @@ From lrust.typing Require Import typing lib.option.
*)
Section non_lexical.
Context `{!typeG Σ} (HashMap K V : type)
Context `{!typeGS Σ} (HashMap K V : type)
`{!TyWf hashmap, !TyWf K, !TyWf V, !Copy K}
(defaultv get_mut insert: val).
......@@ -28,7 +29,7 @@ Section non_lexical.
typed_val insert (fn(∀ α, ∅; &uniq{α} hashmap, K, V) → option V).
Definition get_default : val :=
funrec: <> ["map"; "key"] :=
fn: ["map"; "key"] :=
let: "get_mut" := get_mut in
let: "map'" := !"map" in
......@@ -74,8 +75,8 @@ Section non_lexical.
Lemma get_default_type :
typed_val get_default (fn(∀ m, ∅; &uniq{m} hashmap, K) → &uniq{m} V).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
Proof using Type*.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (m ϝ ret p). inv_vec p=>map key. simpl_subst.
iApply type_let; [iApply get_mut_type|solve_typing|].
iIntros (get_mut'). simpl_subst.
......@@ -88,7 +89,7 @@ Section non_lexical.
iApply type_endlft.
iApply (type_cont [_] [ϝ ⊑ₗ []]
(λ r, [o ◁ box (Π[uninit 1;uninit 1]); map ◁ box (uninit 1);
key ◁ box K; r!!!0 ◁ box (&uniq{m} V)])).
key ◁ box K; (r!!!0%fin:val) ◁ box (&uniq{m} V)])).
{ iIntros (k). simpl_subst.
iApply type_case_own;
[solve_typing| constructor; [|constructor; [|constructor]]; left].
......@@ -116,11 +117,20 @@ Section non_lexical.
iIntros (unwrap'). simpl_subst.
iApply (type_letcall ()); [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_jump; solve_typing.
- iApply type_equivalize_lft.
- (* Use lifetime equalization to replace one lifetime by another:
[&uniq{κ} V] becomes [&uniq{m} V] in the type of [o +ₗ #1]. *)
iApply (type_equivalize_lft _ _ _ _ [_; _; _; _; _; _; _; _]).
{ iIntros (tid) "#LFT #Hκ1 #Hκ2 ($ & Href & $ & $ & $ & $ & $ & $ & _)".
rewrite -tctx_interp_singleton.
iApply (type_incl_tctx_incl with "[] Href").
iApply own_type_incl; first done.
iNext. iApply uniq_type_incl.
- iApply "Hκ2".
- iApply type_equal_refl. }
iApply (type_letalloc_n (&uniq{m}V) (own_ptr _ (&uniq{m}V))); [solve_typing..|].
iIntros (r). simpl_subst.
iApply type_jump; solve_typing. }
iIntros "!# *". inv_vec args=>r. simpl_subst.
iIntros "!> %k %args". inv_vec args=>r. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
......
theories/typing/examples/rebor.v → lambda-rust/typing/examples/rebor.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section rebor.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Definition rebor : val :=
funrec: <> ["t1"; "t2"] :=
fn: ["t1"; "t2"] :=
Newlft;;
letalloc: "x" <- "t1" in
let: "x'" := !"x" in let: "y" := "x'" +ₗ #0 in
......@@ -19,7 +19,7 @@ Section rebor.
Lemma rebor_type :
typed_val rebor (fn(∅; Π[int; int], Π[int; int]) → int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([] ϝ ret p). inv_vec p=>t1 t2. simpl_subst.
iApply (type_newlft []). iIntros (α).
iApply (type_letalloc_1 (&uniq{α}(Π[int; int]))); [solve_typing..|]. iIntros (x). simpl_subst.
......
theories/typing/examples/unbox.v → lambda-rust/typing/examples/unbox.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section unbox.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Definition unbox : val :=
funrec: <> ["b"] :=
fn: ["b"] :=
let: "b'" := !"b" in let: "bx" := !"b'" in
letalloc: "r" <- "bx" +ₗ #0 in
delete [ #1; "b"] ;; return: ["r"].
......@@ -14,7 +14,7 @@ Section unbox.
Lemma ubox_type :
typed_val unbox (fn(∀ α, ∅; &uniq{α}(box(Π[int; int]))) → &uniq{α}int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α ϝ ret b). inv_vec b=>b. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (b'); simpl_subst.
iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
......