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
  • abstraction
  • 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/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/exact_vm
  • ci/ralf/lia-experiment
  • 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/iprop_structures
  • ci/robbert/naive_solver
  • ci/robbert/pm_faster_alt
  • ci/weak_mem
  • coqbug/match
  • experiments
  • fast_string
  • fnlft
  • gen_big_op
  • gpirlea/pinning
  • 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
  • sharedrw
  • sharedrw2
  • simple
  • simulation
  • skiplist
  • stackedborrows
  • stackedborrows-20200517
  • strong_cas_fail
  • stuck
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
61 results
Show changes
Hide whitespace changes
Inline Side-by-side
Showing
with 575 additions and 424 deletions
theories/lang/lifting.v → lambda-rust/lang/lifting.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
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.
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
......@@ -30,38 +31,38 @@ Ltac inv_bin_op_eval :=
end.
Local Hint Extern 0 (atomic _) => solve_atomic : core.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (base_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Constructors head_step bin_op_eval lit_neq lit_eq : core.
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 κ κs n') "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 κ κs n') "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 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
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 κ κs n) "Hσ".
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_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 n.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ' κs' n') "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 κ κs n) "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 κ κs n) "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 κ' κs' n') "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 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
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 κ κs n) "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 κ κs n) "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 κ κs n) "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 κ κs n') "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.
......@@ -372,6 +374,6 @@ Proof.
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.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Export proofmode.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting.
From lrust.lang Require Export tactics lifting.
Set Default Proof Using "Type".
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.
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.
Open Scope Z_scope.
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.
......@@ -20,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.
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]. *)
......@@ -86,21 +87,23 @@ Section borrow.
lctx_lft_alive E L κ →
⊢ 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.
......@@ -116,17 +119,19 @@ Section borrow.
lctx_lft_alive E L κ →
⊢ 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.
......@@ -142,24 +147,26 @@ Section borrow.
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
⊢ 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' :
......@@ -174,21 +181,25 @@ Section borrow.
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
⊢ 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.
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.
......@@ -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' :
......@@ -16,9 +16,11 @@ Section typing.
tctx_incl E L T (T' (list_to_vec argsv)) →
⊢ 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_to_vec argsv). iApply ("HC" with "Hna HL HT").
......@@ -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,19 +66,19 @@ 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.
......@@ -86,10 +86,12 @@ Section cont_context.
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.
......@@ -107,11 +109,11 @@ Section cont_context.
cctx_incl E C1 (k ◁cont(L, T2) :: C2).
Proof.
intros Hin ??. rewrite <-cctx_incl_cons; try done.
clear -Hin. iIntros (?) "_ #HE HC".
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.
......@@ -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.
......
theories/typing/fixpoint.v → lambda-rust/typing/fixpoint.v
View file @ 0f4ebd6d
From lrust.lang Require Import proofmode.
From lrust.typing Require Export lft_contexts type bool.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Import uPred.
Section fixpoint_def.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Context (T : type → type) {HT: TypeContractive T}.
Global Instance type_inhabited : Inhabited type := populate bool.
......@@ -12,7 +12,7 @@ Section fixpoint_def.
Local Instance type_2_contractive : Contractive (Nat.iter 2 T).
Proof using Type*.
intros n ? **. simpl.
by apply dist_later_dist, type_dist2_dist_later, HT, HT, type_later_dist2_later.
by apply dist_later_S, type_dist2_dist_later, HT, HT, type_later_dist2_later.
Qed.
Definition type_fixpoint : type := fixpointK 2 T.
......@@ -28,25 +28,25 @@ Section fixpoint_def.
Global Instance type_fixpoint_wf `{!∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
let lfts :=
let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
(T type_fixpoint).(ty_lfts)
ty_lfts (T type_fixpoint)
in
let wf_E :=
let _ : TyWf type_fixpoint := {| ty_lfts := lfts; ty_wf_E := [] |} in
(T type_fixpoint).(ty_wf_E)
ty_wf_E (T type_fixpoint)
in
{| ty_lfts := lfts; ty_wf_E := wf_E |}.
End fixpoint_def.
Lemma type_fixpoint_ne `{!typeG Σ} (T1 T2 : type → type)
Lemma type_fixpoint_ne `{!typeGS Σ} (T1 T2 : type → type)
`{!TypeContractive T1, !TypeContractive T2} n :
(∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
Section fixpoint.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Context (T : type → type) {HT: TypeContractive T}.
Global Instance fixpoint_copy :
Global Instance type_fixpoint_copy :
(∀ `(!Copy ty), Copy (T ty)) → Copy (type_fixpoint T).
Proof.
intros ?. unfold type_fixpoint. apply fixpointK_ind.
......@@ -61,11 +61,11 @@ Section fixpoint.
{ split; (intros [H1 H2]; split; [apply H1|apply H2]). }
apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
+ apply bi.limit_preserving_Persistent; solve_proper.
+ apply limit_preserving_impl, bi.limit_preserving_entails;
+ apply limit_preserving_impl', bi.limit_preserving_emp_valid;
solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
Qed.
Global Instance fixpoint_send :
Global Instance type_fixpoint_send :
(∀ `(!Send ty), Send (T ty)) → Send (type_fixpoint T).
Proof.
intros ?. unfold type_fixpoint. apply fixpointK_ind.
......@@ -77,7 +77,7 @@ Section fixpoint.
apply bi.limit_preserving_entails; solve_proper.
Qed.
Global Instance fixpoint_sync :
Global Instance type_fixpoint_sync :
(∀ `(!Sync ty), Sync (T ty)) → Sync (type_fixpoint T).
Proof.
intros ?. unfold type_fixpoint. apply fixpointK_ind.
......@@ -89,16 +89,15 @@ Section fixpoint.
apply bi.limit_preserving_entails; solve_proper.
Qed.
Lemma type_fixpoint_unfold : type_fixpoint T ≡ T (type_fixpoint T).
Proof. apply fixpointK_unfold. by apply type_contractive_ne. Qed.
Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
Proof.
unfold eqtype, subtype, type_incl.
setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
split; iIntros (qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
Qed.
Proof. apply type_equal_eqtype, type_equal_equiv, type_fixpoint_unfold. Qed.
End fixpoint.
Section subtyping.
Context `{!typeG Σ} (E : elctx) (L : llctx).
Context `{!typeGS Σ} (E : elctx) (L : llctx).
(* TODO : is there a way to declare these as a [Proper] instances ? *)
Lemma fixpoint_mono T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
......@@ -141,11 +140,11 @@ Section subtyping.
Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
End subtyping.
Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
Global Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
(* These hints can loop if [fixpoint_mono] and [fixpoint_proper] have
not been tried before, so we give them a high cost *)
Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.
Global Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
Global Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
Global Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
Global Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.
theories/typing/function.v → lambda-rust/typing/function.v
View file @ 0f4ebd6d
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From iris.algebra Require Import vector list.
From lrust.typing Require Export type.
From lrust.typing Require Import own programs cont.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section fn.
Context `{!typeG Σ} {A : Type} {n : nat}.
Context `{!typeGS Σ} {A : Type} {n : nat}.
Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
Definition FP_wf E (tys : vec type n) `{!TyWfLst tys} ty `{!TyWf ty} :=
Definition FP_wf E (tys : vec type n) `{!ListTyWf tys} ty `{!TyWf ty} :=
FP (λ ϝ, E ϝ ++ tyl_wf_E tys ++ tyl_outlives_E tys ϝ ++
ty.(ty_wf_E) ++ ty_outlives_E ty ϝ)
ty_wf_E ty ++ ty_outlives_E ty ϝ)
tys ty.
(* The other alternative for defining the fn type would be to state
......@@ -23,7 +23,7 @@ Section fn.
{| st_own tid vl := tc_opaque (∃ fb kb xb e H,
⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
▷ ∀ (x : A) (ϝ : lft) (k : val) (xl : vec val (length xb)),
□ typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
□ typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
[k◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
(zip_with (TCtx_hasty ∘ of_val) xl
(box <$> (vec_to_list (fp x).(fp_tys))))
......@@ -76,12 +76,13 @@ Section fn.
Proper (pointwise_relation A (fn_params_rel (type_dist2_later n')) ==>
type_dist2 n') fn.
Proof.
intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
intros fp1 fp2 Hfp. apply ty_of_st_type_ne. dist_later_fin_intro.
constructor; unfold ty_own; simpl.
(* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
(* The clean way to do this would be to have a metric on type contexts. Oh well. *)
intros tid vl. unfold typed_body.
do 12 f_equiv. f_contractive. do 16 ((eapply fp_E_proper; try reflexivity) || exact: Hfp || f_equiv).
do 12 f_equiv. f_contractive_fin.
do 18 ((eapply fp_E_proper; try reflexivity) || exact: Hfp || f_equiv).
- rewrite !cctx_interp_singleton /=. do 5 f_equiv.
rewrite !tctx_interp_singleton /tctx_elt_interp /=.
do 5 f_equiv. apply type_dist2_dist. apply Hfp.
......@@ -93,8 +94,8 @@ Section fn.
end)%I).
{ intros Hprop. apply Hprop, list_fmap_ne; last first.
- symmetry. eapply Forall2_impl; first apply Hfp. intros.
apply dist_later_dist, type_dist2_dist_later. done.
- apply _. }
apply dist_later_S, type_dist2_dist_later. done.
- solve_proper. }
clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
case _ : (x !! i)=>[tyx|]; case _ : (y !! i)=>[tyy|];
inversion_clear 1; [solve_proper|done].
......@@ -103,7 +104,7 @@ Section fn.
Global Instance fn_ne n' :
Proper (pointwise_relation A (fn_params_rel (dist n')) ==> dist n') fn.
Proof.
intros ?? Hfp. apply dist_later_dist, type_dist2_dist_later.
intros ?? Hfp. apply dist_later_S, type_dist2_dist_later.
apply fn_type_contractive=>u. split; last split.
- eapply Forall2_impl; first apply Hfp. intros. simpl.
apply type_dist_dist2. done.
......@@ -112,7 +113,7 @@ Section fn.
Qed.
End fn.
Arguments fn_params {_ _} _.
Global Arguments fn_params {_ _} _.
(* We use recursive notation for binders as well, to allow patterns
like '(a, b) to be used. In practice, only one binder is ever used,
......@@ -138,10 +139,10 @@ Notation "'fn(' E ')' '→' R" :=
(at level 99, R at level 200,
format "'fn(' E ')' '→' R") : lrust_type_scope.
Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
Global Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
Section typing.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
(∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in
......@@ -150,7 +151,7 @@ Section typing.
subtype EE L0 (fp x).(fp_ty) (fp' x).(fp_ty)) →
subtype E0 L0 (fn fp) (fn fp').
Proof.
intros Hcons. apply subtype_simple_type=>//= qL. iIntros "HL0".
intros Hcons. apply subtype_simple_type=>//= qmax qL. iIntros "HL0".
(* We massage things so that we can throw away HL0 before going under the box. *)
iAssert (∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in □ (elctx_interp EE -∗
elctx_interp ((fp x).(fp_E) ϝ) ∗
......@@ -158,17 +159,17 @@ Section typing.
type_incl (fp x).(fp_ty) (fp' x).(fp_ty)))%I as "#Hcons".
{ iIntros (x ϝ). destruct (Hcons x ϝ) as (HE &Htys &Hty). clear Hcons.
iDestruct (HE with "HL0") as "#HE".
iDestruct (subtype_Forall2_llctx with "HL0") as "#Htys"; first done.
iDestruct (subtype_Forall2_llctx_noend with "HL0") as "#Htys"; first done.
iDestruct (Hty with "HL0") as "#Hty".
iClear "∗". iIntros "!# #HEE".
iClear "∗". iIntros "!> #HEE".
iSplit; last iSplit.
- by iApply "HE".
- by iApply "Htys".
- by iApply "Hty". }
iClear "∗". clear Hcons. iIntros "!# #HE0 * Hf".
iClear "∗". clear Hcons. iIntros "!> #HE0 * Hf".
iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
rewrite /typed_body. iIntros (x ϝ k xl) "!# * #LFT #HE' Htl HL HC HT".
iExists fb, kb, xb, e, _. iSplit; first done. iSplit; first done. iNext.
rewrite /typed_body. iIntros (x ϝ k xl) "!> * #LFT #HE' Htl HL HC HT".
iDestruct ("Hcons" with "[$]") as "#(HE & Htys & Hty)".
iApply ("Hf" with "LFT HE Htl HL [HC] [HT]").
- unfold cctx_interp. iIntros (elt) "Helt".
......@@ -181,10 +182,10 @@ Section typing.
iDestruct (box_type_incl with "[$Hty]") as "(_ & #Hincl & _)".
by iApply "Hincl".
- iClear "Hf". rewrite /tctx_interp
-{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
-{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
-{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?length_vec_to_list //
-{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?length_vec_to_list //
!zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
iApply (big_sepL_impl with "HT"). iIntros "!#".
iApply (big_sepL_impl with "HT"). iIntros "!>".
iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
iDestruct "H" as (v) "[? Hown]". iExists v. iFrame.
rewrite !lookup_zip_with.
......@@ -227,31 +228,31 @@ Section typing.
Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 fp :
subtype E0 L0 (fn (n:=n) fp) (fn (fp ∘ σ)).
Proof.
apply subtype_simple_type=>//= qL.
iIntros "_ !# _ * Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
apply subtype_simple_type=>//= qmax qL.
iIntros "_ !> _ * Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit; first done. iSplit; first done.
rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
Qed.
(* In principle, proving this hard-coded to an empty L would be sufficient --
but then we would have to require elctx_sat as an Iris assumption. *)
Lemma type_call_iris' E L (κs : list lft) {A} x (ps : list path) qκs qL tid
Lemma type_call_iris' E L (κs : list lft) {A} x (ps : list path) qκs qmax qL tid
p (k : expr) (fp : A → fn_params (length ps)) :
(∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
AsVal k →
lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp L qL -∗
lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp_noend qmax L qL -∗
qκs.[lft_intersect_list κs] -∗
tctx_elt_interp tid (p ◁ fn fp) -∗
([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)),
tctx_elt_interp tid y) -∗
(∀ ret, na_own tid top -∗ llctx_interp L qL -∗ qκs.[lft_intersect_list κs] -∗
(∀ ret, na_own tid top -∗ llctx_interp_noend qmax L qL -∗ qκs.[lft_intersect_list κs] -∗
(box (fp x).(fp_ty)).(ty_own) tid [ret] -∗
WP k [of_val ret] {{ _, cont_postcondition }}) -∗
WP (call: p ps → k) {{ _, cont_postcondition }}.
Proof.
iIntros (HE [k' <-]) "#LFT #HE Htl HL Hκs Hf Hargs Hk".
wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#☠ ;; #☠) ;; k' ["_r"])%V⌝):::
iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], k' ["_r"])%V⌝):::
vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
with "[Hargs]").
- rewrite /=. iSplitR "Hargs".
......@@ -267,28 +268,37 @@ Section typing.
iIntros "[-> Hvl]". iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl.
revert vl fp HE. rewrite /= -EQl=>vl fp HE. wp_rec.
iMod (lft_create with "LFT") as (ϝ) "[Htk #Hinh]"; first done.
iMod (lft_create with "LFT") as (ϝ_inner) "[Htk #Hend]"; first done.
set (ϝ := ϝ_inner ⊓ lft_intersect_list κs).
iSpecialize ("Hf" $! x ϝ _ vl). iDestruct (HE ϝ with "HL") as "#HE'".
iMod (bor_create _ ϝ with "LFT Hκs") as "[Hκs HκsI]"; first done.
iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
{ iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
+ iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
{ iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
iApply "IH". iModIntro. iApply lft_incl_trans; first done.
iApply lft_intersect_incl_r.
+ iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
iFrame "#∗".
+ iIntros (y) "IN". iDestruct "IN" as %->%elem_of_list_singleton.
destruct (Qp.lower_bound qκs 1) as (q0 & q'1 & q'2 & -> & Hsum1).
rewrite Hsum1. assert (q0 < 1)%Qp as Hq0.
{ apply Qp.lt_sum. eauto. }
clear Hsum1.
iDestruct "Htk" as "[Htk1 Htk2]".
iDestruct "Hκs" as "[Hκs1 Hκs2]".
iApply ("Hf" $! _ q0 with "LFT [] Htl [Hκs1 Htk1 Htk2] [Hk HL Hκs2]").
+ iApply "HE'". iFrame "HE".
iIntros "{$# Hf Hend HE' LFT HE %}". subst ϝ.
iApply big_sepL_forall.
iIntros (i [κ1 κ2] [κ [Hpair Helem]]%elem_of_list_lookup_2%elem_of_list_fmap).
injection Hpair as -> ->. iPureIntro. simpl.
eapply lft_incl_syn_trans; first by apply lft_intersect_incl_syn_r.
apply lft_intersect_list_elem_of_incl_syn.
done.
+ iSplitL; last done. iExists ϝ. rewrite left_id. iSplit; first done.
rewrite decide_False; last first.
{ apply Qp.lt_nge. done. }
subst ϝ. rewrite -!lft_tok_sep. iFrame. iIntros "[Htk1 _]".
rewrite -lft_dead_or. rewrite -bi.or_intro_l. iApply "Hend". iFrame.
+ iIntros (y) "IN {Hend}". iDestruct "IN" as %->%elem_of_list_singleton.
iIntros (args) "Htl [Hϝ _] [Hret _]". inv_vec args=>r.
iDestruct "Hϝ" as (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
rewrite /= left_id in EQ. subst κ'. simpl. wp_rec. wp_bind Endlft.
iSpecialize ("Hinh" with "Htk"). iClear "Hκs".
iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
iApply (wp_step_fupd with "Hinh"); [set_solver-..|]. wp_seq.
iIntros "#Htok !>". wp_seq. iMod ("HκsI" with "Htok") as ">Hκs".
iApply ("Hk" with "Htl HL Hκs"). rewrite tctx_hasty_val. done.
rewrite /= left_id in EQ. subst κ' ϝ.
rewrite decide_False; last first.
{ apply Qp.lt_nge. done. }
rewrite -lft_tok_sep. iDestruct "Htk" as "[_ Hκs1]". wp_rec.
iApply ("Hk" with "Htl HL [$Hκs1 $Hκs2]"). rewrite tctx_hasty_val. done.
+ rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
(zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
iApply (big_sepL_mono' with "Hvl"); last done. by iIntros (i [v ty']).
......@@ -310,7 +320,7 @@ Section typing.
Proof.
iIntros (HE Hk') "#LFT #HE Htl Hκs Hf Hargs Hk". rewrite -tctx_hasty_val.
iApply (type_call_iris' with "LFT HE Htl [] Hκs Hf Hargs [Hk]"); [done..| |].
- instantiate (1 := 1%Qp). by rewrite /llctx_interp.
- instantiate (1 := 1%Qp). instantiate (1 := 1%Qp). by rewrite /llctx_interp_noend.
- iIntros "* Htl _". iApply "Hk". done.
Qed.
......@@ -324,7 +334,7 @@ Section typing.
T)
(call: p ps → k).
Proof.
iIntros (Hκs HE tid) "#LFT #HE Htl HL HC (Hf & Hargs & HT)".
iIntros (Hκs HE tid qmax) "#LFT #HE Htl HL HC (Hf & Hargs & HT)".
iMod (lctx_lft_alive_tok_list _ _ κs with "HE HL") as (q) "(Hκs & HL & Hclose)"; [done..|].
iApply (type_call_iris' with "LFT HE Htl HL Hκs Hf Hargs"); [done|].
iIntros (r) "Htl HL Hκs Hret". iMod ("Hclose" with "Hκs HL") as "HL".
......@@ -333,13 +343,13 @@ Section typing.
rewrite tctx_interp_cons tctx_hasty_val. iFrame.
Qed.
(* Specialized type_call': Adapted for use by solve_typing; fixed "list of
alive lifetimes" to be the local ones. *)
Lemma type_call {A} x E L C T T' T'' p (ps : list path)
(* Specialized type_call': Adapted for use by solve_typing.
κs is still expected to be given manually. *)
Lemma type_call {A} κs x E L C T T' T'' p (ps : list path)
(fp : A → fn_params (length ps)) k :
p ◁ fn fp ∈ T →
Forall (lctx_lft_alive E L) (L.*1) →
(∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> (L.*1)) ++ E) L ((fp x).(fp_E) ϝ)) →
Forall (lctx_lft_alive E L) κs →
(∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
tctx_extract_ctx E L (zip_with TCtx_hasty ps
(box <$> vec_to_list (fp x).(fp_tys))) T T' →
k ◁cont(L, T'') ∈ C →
......@@ -347,9 +357,10 @@ Section typing.
⊢ typed_body E L C T (call: p ps → k).
Proof.
intros Hfn HL HE HTT' HC HT'T''.
rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
- etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
apply cctx_incl_cons; first done. intros args. by inv_vec args.
iApply typed_body_mono; [| |done|by iApply type_call']; simpl.
- etrans.
+ eapply (incl_cctx_incl _ [_]); by intros ? ->%elem_of_list_singleton.
+ apply cctx_incl_cons; first done. intros args. by inv_vec args.
- etrans; last by apply (tctx_incl_frame_l [_]).
apply copy_elem_of_tctx_incl; last done. apply _.
Qed.
......@@ -376,12 +387,14 @@ Section typing.
intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
- iIntros (k).
(* TODO : make [simpl_subst] work here. *)
change (subst' "_k" k (p ((λ: ["_r"], (#☠ ;; #☠) ;; "_k" ["_r"])%E :: ps))) with
((subst "_k" k p) ((λ: ["_r"], (#☠ ;; #☠) ;; k ["_r"])%E :: map (subst "_k" k) ps)).
change (subst' "_k" k (p ((λ: ["_r"], "_k" ["_r"])%E :: ps))) with
((subst "_k" k p) ((λ: ["_r"], k ["_r"])%E :: map (subst "_k" k) ps)).
rewrite is_closed_nil_subst //.
assert (map (subst "_k" k) ps = ps) as ->.
{ clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
iApply type_call; try done. constructor. done.
iApply type_call; try done.
+ constructor.
+ done.
- simpl. iIntros (k ret). inv_vec ret=>ret. rewrite /subst_v /=.
rewrite ->(is_closed_subst []); last set_solver+; last first.
{ apply subst'_is_closed; last done. apply is_closed_of_val. }
......@@ -391,7 +404,7 @@ Section typing.
Lemma type_rec {A} E L fb (argsb : list binder) ef e n
(fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
IntoVal ef (funrec: fb argsb := e) →
IntoVal ef (fnrec: fb argsb := e) →
n = length argsb →
□ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
......@@ -402,11 +415,11 @@ Section typing.
(subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
typed_instruction_ty E L T ef (fn fp).
Proof.
iIntros (<- ->) "#Hbody /=". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
iIntros (<- ->) "#Hbody /=". iIntros (tid qmax) "#LFT _ $ $ #HT". iApply wp_value.
rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
{ simpl. rewrite decide_left. done. }
iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.
iIntros (x ϝ k args) "!#". iIntros (tid') "_ HE Htl HL HC HT'".
{ simpl. rewrite decide_True_pi. done. }
iExists fb, _, argsb, e, _. iSplit; first done. iSplit; first done. iNext.
iIntros (x ϝ k args) "!>". iIntros (tid' qmax') "_ HE Htl HL HC HT'".
iApply ("Hbody" with "LFT HE Htl HL HC").
rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
by iApply sendc_change_tid.
......@@ -414,20 +427,21 @@ Section typing.
Lemma type_fn {A} E L (argsb : list binder) ef e n
(fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
IntoVal ef (funrec: <> argsb := e) →
IntoVal ef (fn: argsb := e) →
n = length argsb →
□ (∀ x ϝ k (args : vec val (length argsb)),
typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
typed_body ((fp x).(fp_E) ϝ)
[ϝ ⊑ₗ []]
[k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
(zip_with (TCtx_hasty ∘ of_val) args
(box <$> vec_to_list (fp x).(fp_tys)) ++ T)
(subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
typed_instruction_ty E L T ef (fn fp).
Proof.
iIntros (??) "#He". iApply type_rec; try done. iIntros "!# *".
iIntros (??) "#He". iApply type_rec; try done. iIntros "!> *".
iApply typed_body_mono; last iApply "He"; try done.
eapply contains_tctx_incl. by constructor.
Qed.
End typing.
Hint Resolve fn_subtype : lrust_typing.
Global Hint Resolve fn_subtype : lrust_typing.
theories/typing/int.v → lambda-rust/typing/int.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 bool programs.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Section int.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Program Definition int : type :=
{| st_own tid vl :=
......@@ -22,11 +22,11 @@ Section int.
End int.
Section typing.
Context `{!typeG Σ}.
Context `{!typeGS Σ}.
Lemma type_int_instr (z : Z) : typed_val #z int.
Proof.
iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
iIntros (E L tid ?) "_ _ $ $ _". iApply wp_value.
by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
......@@ -39,7 +39,7 @@ Section typing.
Lemma type_plus_instr E L p1 p2 :
⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
Proof.
iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
......@@ -55,7 +55,7 @@ Section typing.
Lemma type_minus_instr E L p1 p2 :
⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
Proof.
iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
......@@ -71,7 +71,7 @@ Section typing.
Lemma type_le_instr E L p1 p2 :
⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
Proof.
iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op; case_bool_decide; by rewrite tctx_interp_singleton tctx_hasty_val' //.
......