diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 537d72f2a..bb53d234b 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -19,6 +19,21 @@ This version follows Iris Rocq in fixing the underlying type of fractions to be @[expose] public section +/-! ## Ordered-field lemmas for `Rat` + +This environment has no Mathlib, so `Rat` is missing the ordered-field API (and the +`positivity`/`field_simp` tactics) needed to reason about division. These few lemmas fill the +gap that the `Qp` API below relies on. -/ +namespace Rat + +protected theorem div_pos {a b : Rat} (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by + rw [Rat.div_def]; exact Rat.mul_pos ha (Rat.inv_pos.mpr hb) + +protected theorem mul_div_cancel_left {a b : Rat} (ha : a ≠ 0) : a * (b / a) = b := by + rw [Rat.mul_comm, Rat.div_mul_cancel ha] + +end Rat + namespace Iris /-- The type of positive rational numbers, used as fractions -/ @@ -42,6 +57,16 @@ def Qp.half (q : Qp) : Qp where let ⟨v, P⟩ := q grind +/-- Division of fractions. -/ +def Qp.div (x y : Qp) : Qp := ⟨x.val / y.val, Rat.div_pos x.2 y.2⟩ + +instance instHDivQpQpQp : HDiv Qp Qp Qp where + hDiv := Qp.div + +/-- `q` divided into `n > 0` equal positive parts. -/ +def Qp.divide_even (q : Qp) (n : Nat) (hn : 0 < n) : Qp := + ⟨q.val / n, Rat.div_pos q.2 (by exact_mod_cast hn)⟩ + instance instCOFEQp : COFE Qp := COFE.ofDiscrete _ Eq_Equivalence instance instLeibnizQp : OFE.Leibniz Qp := ⟨id⟩ @@ -75,6 +100,9 @@ instance instCMRAQp : CMRA Qp where @[simp, grind =] theorem Qp.val_add (x y : Qp) : (x + y).val = x.val + y.val := rfl @[simp, grind =] theorem Qp.val_one : (1 : Qp).val = 1 := rfl @[simp, grind =] theorem Qp.val_half (q : Qp) : q.half.val = q.val / 2 := rfl +@[simp, grind =] theorem Qp.val_div (x y : Qp) : (x / y).val = x.val / y.val := rfl +@[simp, grind =] theorem Qp.val_divide_even (q : Qp) (n : Nat) (hn : 0 < n) : + (q.divide_even n hn).val = q.val / n := rfl @[simp, grind =] theorem Qp.val_op (x y : Qp) : (x • y).val = x.val + y.val := rfl @[simp, grind =] theorem Qp.validN_iff {n} {x : Qp} : ✓{n} x ↔ x.val ≤ 1 := Iff.rfl @[simp, grind =] theorem Qp.valid_iff {x : Qp} : ✓ x ↔ x.val ≤ 1 := Iff.rfl @@ -87,6 +115,14 @@ instance instCMRAQp : CMRA Qp where /-- The whole fraction `1` is valid. -/ @[simp, rocq_alias frac_valid_1] theorem Qp.valid_one : ✓ (1 : Qp) := by grind +/-- Two halves make a whole. -/ +@[simp, grind =] theorem Qp.half_add_half (q : Qp) : q.half + q.half = q := Subtype.ext (by grind) + +/-- `a < b` iff `b` is `a` plus some positive remainder. -/ +theorem Qp.lt_iff_exists_add {a b : Qp} : a < b ↔ ∃ c : Qp, a + c = b := by + refine ⟨fun h => ⟨⟨b.val - a.val, by have := Qp.lt_iff.mp h; grind⟩, Subtype.ext (by grind)⟩, ?_⟩ + rintro ⟨c, rfl⟩; have := c.2; grind + #rocq_ignore frac_op_instance "Use CMRA instance" #rocq_ignore frac_pcore_instance "Use CMRA instance" #rocq_ignore frac_valid_instance "Use CMRA instance" diff --git a/Iris/Iris/BI/BigOp/BigSepMap.lean b/Iris/Iris/BI/BigOp/BigSepMap.lean index f5636d7e6..faca2311a 100644 --- a/Iris/Iris/BI/BigOp/BigSepMap.lean +++ b/Iris/Iris/BI/BigOp/BigSepMap.lean @@ -568,8 +568,22 @@ theorem bigSepM_impl_strong [DecidableEq K] {M₂ : Type _ → Type _} {V₂ : T refine sep_mono_right <| sep_mono_right (equiv_iff.mp <| bigOpM_eqv_of_perm Φ fun k => ?_).2 by_cases hki : i = k <;> simp_all [get?_filter, get?_insert, get?_delete] --- TODO: `big_sepM_kmap` and `big_sepM_map_seq` require map operations --- which are not yet available in `PartialMap`. +-- TODO: `big_sepM_kmap` requires map operations which are not yet available in `PartialMap`. + +theorem bigSepM_map_seq {M' : Type _ → Type _} [LawfulFiniteMap M' Nat] {V : Type _} + {Φ : Nat → V → PROP} {start : Nat} {l : List V} : + ([∗map] k ↦ v ∈ FiniteMap.map_seq (M := M') start l, Φ k v) ⊣⊢ + ([∗list] i ↦ v ∈ l, Φ (start + i) v) := by + induction l generalizing start with + | nil => rw [LawfulFiniteMap.map_seq_nil]; simp + | cons v l ih => + have hfun : (fun i (x : V) => Φ (start + 1 + i) x) = (fun i x => Φ (start + (i + 1)) x) := by + funext i x; congr 1; omega + have ih1 := ih (start := start + 1) + rw [hfun] at ih1 + rw [LawfulFiniteMap.map_seq_cons] + exact (bigSepM_insert (by rw [LawfulFiniteMap.get?_map_seq, if_neg (by omega)])).trans + (sep_congr .rfl ih1) /-! ## Map–Set Interaction -/ diff --git a/Iris/Iris/BI/Lib/Fractional.lean b/Iris/Iris/BI/Lib/Fractional.lean index be5d234d8..fe9666c93 100644 --- a/Iris/Iris/BI/Lib/Fractional.lean +++ b/Iris/Iris/BI/Lib/Fractional.lean @@ -12,13 +12,115 @@ public import Iris.ProofMode @[expose] public section namespace Iris -open Iris.Std BI OFE +open Iris.Std BI OFE ProofMode @[rocq_alias Fractional] class Fractional [BI PROP] (Φ : Qp → PROP) where fractional p q : Φ (p + q) ⊣⊢ Φ p ∗ Φ q @[rocq_alias AsFractional] -class AsFractional {PROP: Type u} [bi: BI PROP] (P : PROP) (Φ : Qp → PROP) (q : Qp) where +class AsFractional {PROP : Type u} [BI PROP] (P : PROP) (Φ : Qp → PROP) (q : Qp) where as_fractional : P ⊣⊢ Φ q as_fractional_fractional : Fractional Φ + +section Lemmas +variable {PROP : Type _} [BI PROP] {P P1 P2 : PROP} {Φ : Qp → PROP} {q q1 q2 : Qp} + +/-- Any `Φ q` of a fractional `Φ` is `AsFractional`. -/ +@[rocq_alias fractional_as_fractional] +instance (priority := 100) fractional_as_fractional [h : Fractional Φ] (q : Qp) : + AsFractional (Φ q) Φ q where + as_fractional := .rfl + as_fractional_fractional := h + +/-- Split a fraction `q1 + q2` into the separating conjunction of its parts. -/ +@[rocq_alias fractional_split] +theorem fractional_split [hP : AsFractional P Φ (q1 + q2)] + [hP1 : AsFractional P1 Φ q1] [hP2 : AsFractional P2 Φ q2] : P ⊣⊢ P1 ∗ P2 := + have := hP.as_fractional_fractional + hP.as_fractional.trans <| (Fractional.fractional q1 q2).trans <| + sep_congr hP1.as_fractional.symm hP2.as_fractional.symm + +/-- Halve a fraction into two equal pieces. -/ +@[rocq_alias fractional_half] +theorem fractional_half [hP : AsFractional P Φ q] [hP12 : AsFractional P1 Φ q.half] : + P ⊣⊢ P1 ∗ P1 := + have := hP.as_fractional_fractional + hP.as_fractional.trans <| (Qp.half_add_half q ▸ Fractional.fractional q.half q.half).trans <| + sep_congr hP12.as_fractional.symm hP12.as_fractional.symm + +/-- Merge two fractions back into their sum. -/ +@[rocq_alias fractional_merge] +theorem fractional_merge [Fractional Φ] + [hP1 : AsFractional P1 Φ q1] [hP2 : AsFractional P2 Φ q2] : P1 ∗ P2 ⊢ Φ (q1 + q2) := + (sep_mono hP1.as_fractional.1 hP2.as_fractional.1).trans (Fractional.fractional q1 q2).2 + +set_option synthInstance.checkSynthOrder false in +@[rocq_alias from_sep_fractional] +instance (priority := default - 10) fromSepFractional [hP : AsFractional P Φ (q1 + q2)] : + FromSep P (Φ q1) (Φ q2) where + from_sep := + have := hP.as_fractional_fractional + (Fractional.fractional q1 q2).2.trans hP.as_fractional.2 + +set_option synthInstance.checkSynthOrder false in +@[rocq_alias into_sep_fractional] +instance (priority := default - 10) intoSepFractional [hP : AsFractional P Φ (q1 + q2)] : + IntoSep P (Φ q1) (Φ q2) where + into_sep := + have := hP.as_fractional_fractional + hP.as_fractional.1.trans (Fractional.fractional q1 q2).1 + +set_option synthInstance.checkSynthOrder false in +@[rocq_alias from_sep_fractional_half] +instance (priority := default - 10) fromSepFractionalHalf [hP : AsFractional P Φ q] : + FromSep P (Φ q.half) (Φ q.half) where + from_sep := + have := hP.as_fractional_fractional + (Qp.half_add_half q ▸ Fractional.fractional q.half q.half).2.trans hP.as_fractional.2 + +set_option synthInstance.checkSynthOrder false in +@[rocq_alias into_sep_fractional_half] +instance (priority := default - 10) intoSepFractionalHalf [hP : AsFractional P Φ q] : + IntoSep P (Φ q.half) (Φ q.half) where + into_sep := + have := hP.as_fractional_fractional + hP.as_fractional.1.trans (Qp.half_add_half q ▸ Fractional.fractional q.half q.half).1 + +end Lemmas + +section Divide +variable {PROP : Type _} [BI PROP] +open BI.BigSepL + +/-- Whenever `q = (k+1) * r`, the fraction `Φ q` splits into `k+1` copies of `Φ r`. -/ +theorem fractional_bigSepL_replicate {Φ : Qp → PROP} [Fractional Φ] (r : Qp) : + ∀ (k : Nat) (q : Qp), q.val = ((k : Rat) + 1) * r.val → + Φ q ⊢ [∗list] _x ∈ List.replicate (k + 1) r, Φ r := by + intro k + induction k with + | zero => + intro q hq + rw [show q = r from Subtype.ext (by grind)] + exact (bigSepL_singleton (Φ := fun _ _ => Φ r)).2 + | succ k ih => + intro q hq + have hval : q.val - r.val = ((k : Rat) + 1) * r.val := by grind + have hpos : (0 : Rat) < q.val - r.val := hval ▸ Rat.mul_pos (by grind) r.2 + have hsum : r + (⟨q.val - r.val, hpos⟩ : Qp) = q := Subtype.ext (by grind) + rw [← hsum, List.replicate_succ] + exact ((Fractional.fractional r _).1.trans (sep_mono_right (ih _ hval))).trans + (bigSepL_cons (Φ := fun _ _ => Φ r)).2 + +/-- Splitting `Φ q` into `n+1` equal pieces, each owning the fraction `q / (n+1)`. -/ +theorem fractional_divide_equal {Φ : Qp → PROP} [Fractional Φ] (q : Qp) (n : Nat) : + Φ q ⊢ [∗list] _x ∈ List.replicate (n + 1) (q.divide_even (n + 1) (Nat.succ_pos n)), + Φ (q.divide_even (n + 1) (Nat.succ_pos n)) := by + refine fractional_bigSepL_replicate _ n q ?_ + have hne : ((n : Rat) + 1) ≠ 0 := by + have : (0 : Rat) ≤ (n : Rat) := by exact_mod_cast Nat.zero_le n + grind + have hcast : ((n + 1 : Nat) : Rat) = (n : Rat) + 1 := by grind + rw [Qp.val_divide_even, hcast, Rat.mul_div_cancel_left hne] + +end Divide diff --git a/Iris/Iris/HeapLang/Instances.lean b/Iris/Iris/HeapLang/Instances.lean index 9cf75c38c..77c1bc56b 100644 --- a/Iris/Iris/HeapLang/Instances.lean +++ b/Iris/Iris/HeapLang/Instances.lean @@ -1,6 +1,7 @@ /- Copyright (c) 2026 Sergei Stepanenko. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sergei Stepanenko, Markus de Medeiros -/ module @@ -11,11 +12,12 @@ public import Iris.ProgramLogic.EctxiLanguage public import Std.Data.ExtTreeMap public import Std.Data.ExtTreeSet public import Iris.Std.FromMathlib +public import Iris.Std.GenSetsInstances @[expose] public section namespace Iris.HeapLang -open ProgramLogic +open ProgramLogic ProgramLogic.Language FromMathlib EctxItemLanguage EctxLanguage instance instEctxItemLanguageExp : EctxItemLanguage Exp ECtxItem State Observation Val where baseStep := fun ⟨e, σ⟩ obs ⟨e', σ', eps⟩ => BaseStep e σ obs e' σ' eps @@ -49,210 +51,349 @@ instance instEctxItemLanguageExp : EctxItemLanguage Exp ECtxItem State Observati intro σ obs e' σ' eps h cases h <;> rfl -theorem mk_pure_prim_step {e1 e2 : Exp} - (hstep : ∀ σ, BaseStep e1 σ [] e2 σ []) - (hpure : ∀ σ1 κs e2' σ2 efs, BaseStep e1 σ1 κs e2' σ2 efs → κs = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []) - (hsub : EctxLanguage.SubredexesAreValues e1) : - Language.PurePrimStep e1 e2 := by - constructor - · intro σ - exists e2, σ, [] - refine BaseStep.ContextStep.intro (K := []) (hstep _) - · intro σ1 σ2 κs e2' efs Hstep - have h := (EctxLanguage.baseStep_of_primStep Hstep hsub) - apply hpure; apply h - -instance instPureExecIfTrue: Language.PureExec True 1 hl(if #true then &e1 else &e2) e1 where +@[simp] +theorem fillItem_expToVal_none (Ki : ECtxItem) (e : Exp) : toVal (fillItem Ki e) = none := by + cases Ki <;> rfl + +theorem fill_isSome_empty {K : List ECtxItem} {e : Exp} + (h : (toVal (fill K e)).isSome) : K = [] := by + cases K with + | nil => rfl + | cons Ki K' => + rw [fill_cons] at h + have h2 := EctxLanguage.fill_val (K := K') (e := fillItem Ki e) h + simp [fillItem_expToVal_none] at h2 + +macro "solve_subredex_values" : tactic => + `(tactic| + (apply subredexes_are_values + intro Ki e_inner heq + cases Ki <;> cases heq <;> try rfl <;> try done)) + +theorem mk_pure_prim_step {e1 e2 : Exp} (hstep : ∀ σ, BaseStep e1 σ [] e2 σ []) + (hpure : ∀ {σ1 κs e2' σ2 efs}, BaseStep e1 σ1 κs e2' σ2 efs → κs = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []) + (hsub : SubredexesAreValues e1) : PurePrimStep e1 e2 := by + refine ⟨fun σ => ?_, fun Hstep => ?_⟩ + · exact ⟨e2, σ, [], BaseStep.ContextStep.intro (K := []) (hstep _)⟩ + · exact hpure (baseStep_of_primStep Hstep hsub) + +instance instPureExecIfTrue: PureExec True 1 hl(if #true then &e1 else &e2) e1 where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor · cases hs <;> simp - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq - rfl + · solve_subredex_values -instance instPureExecIfFalse : Language.PureExec True 1 hl(if #false then &e1 else &e2) e2 where +instance instPureExecIfFalse : PureExec True 1 hl(if #false then &e1 else &e2) e2 where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor · cases hs <;> simp - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq - rfl + · solve_subredex_values instance instPureExecCaseInjl {v e1 e2} : - Language.PureExec True 1 (Exp.case hl(v(injl(&v))) e1 e2) (.app e1 (.ofVal v)) where + PureExec True 1 (Exp.case hl(v(injl(&v))) e1 e2) (.app e1 (.ofVal v)) where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor · cases hs <;> simp - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq - rfl + · solve_subredex_values instance instPureExecCaseInjr {v e1 e2} : - Language.PureExec True 1 (Exp.case hl(v(injr(&v))) e1 e2) (.app e2 (.ofVal v)) where + PureExec True 1 (Exp.case hl(v(injr(&v))) e1 e2) (.app e2 (.ofVal v)) where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor · cases hs <;> simp - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq - rfl + · solve_subredex_values -instance PureExec_injl {v : Val} : Language.PureExec True 1 hl(injl(&v)) hl(v(injl(&v))) where +instance instPureExecInjl {v : Val} : PureExec True 1 hl(injl(&v)) hl(v(injl(&v))) where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor · cases hs <;> simp - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq - rfl + · solve_subredex_values -instance PureExec_injr {v : Val} : Language.PureExec True 1 hl(injr(&v)) hl(v(injr(&v))) where +instance instPureExecInjr {v : Val} : PureExec True 1 hl(injr(&v)) hl(v(injr(&v))) where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor · cases hs <;> simp - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq - rfl + · solve_subredex_values instance instPureExecBeta {f x : Binder} {e : Exp} {v : Val} : - Language.PureExec True 1 hl(v(rec &f &x := &e) &v) ((e.subst f (.rec_ f x e)).subst x v) where + PureExec True 1 hl(v(rec &f &x := &e) &v) ((e.subst f (.rec_ f x e)).subst x v) where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor <;> simp · cases hs <;> simp [*] - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq <;> rfl + · solve_subredex_values -instance instPureExecRec {f x e} : Language.PureExec True 1 hl(rec &f &x := &e) hl(v(rec &f &x := &e)) where +instance instPureExecRec {f x e} : + PureExec True 1 hl(rec &f &x := &e) hl(v(rec &f &x := &e)) where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor <;> simp · cases hs <;> simp [*] - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq <;> rfl + · solve_subredex_values -instance PureExec_fst {v1 v2 : Val} : Language.PureExec True 1 hl(fst(v((&v1, &v2)))) v1 where +instance instPureExecFst {v1 v2 : Val} : PureExec True 1 hl(fst(v((&v1, &v2)))) v1 where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor <;> simp · cases hs <;> simp [*] - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq <;> rfl + · solve_subredex_values -instance PureExec_snd {v1 v2 : Val} : Language.PureExec True 1 hl(snd(v((&v1, &v2)))) v2 where +instance instPureExecSnd {v1 v2 : Val} : PureExec True 1 hl(snd(v((&v1, &v2)))) v2 where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor <;> simp · cases hs <;> simp [*] - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq <;> rfl + · solve_subredex_values -instance PureExec_pair {v1 v2 : Val} : Language.PureExec True 1 hl((&v1, &v2)) hl(v((&v1, &v2))) where +instance instPureExecPair {v1 v2 : Val} : PureExec True 1 hl((&v1, &v2)) hl(v((&v1, &v2))) where pureExec _ := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor <;> simp · cases hs <;> simp [*] - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq <;> rfl + · solve_subredex_values set_option synthInstance.checkSynthOrder false in instance instPureExecUnOp {op : UnOp} {v v' : Val} : - Language.PureExec (op.eval v = some v') 1 (Exp.unop op (.ofVal v)) (.ofVal v') where + PureExec (op.eval v = some v') 1 (Exp.unop op (.ofVal v)) (.ofVal v') where pureExec h := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor <;> simp [*] · cases hs <;> simp_all [UnOp.eval] - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq <;> rfl + · solve_subredex_values set_option synthInstance.checkSynthOrder false in instance instPureExecBinOp {op : BinOp} {v1 v2 v' : Val} : - Language.PureExec (op.eval v1 v2 = some v') 1 + PureExec (op.eval v1 v2 = some v') 1 (Exp.binop op (.ofVal v1) (.ofVal v2)) (.ofVal v') where pureExec h := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor <;> simp [*] · cases hs <;> simp_all [BinOp.eval] - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq <;> rfl + · solve_subredex_values -- higher priority than the generic binop instance instance (priority := default + 10) instPureExecEqOp {v1 v2 : Val} : - Language.PureExec (v1.compareSafe v2) 1 + PureExec (v1.compareSafe v2) 1 (Exp.binop .eq (.ofVal v1) (.ofVal v2)) (.ofVal (.lit (.bool (v1 == v2)))) where pureExec h := by - refine .once <| mk_pure_prim_step (fun _ => ?_) (fun _ _ _ _ _ hs => ?_) ?_ + refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_ · constructor <;> simp [BinOp.eval, *] · cases hs <;> simp_all [BinOp.eval] - · apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> cases heq <;> rfl + · solve_subredex_values -instance instAtomicLoad {s} {v : Val} : Language.Atomic s hl(!&v) where +instance instAtomicLoad {s} {v : Val} : Atomic s hl(!&v) where atomic {σ obs e' σ' eₜ} Hstep := by - have hsr : EctxLanguage.SubredexesAreValues hl(!&v) := by - apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> try (cases heq; done) - all_goals (cases heq; rfl) - cases (EctxLanguage.baseStep_of_primStep Hstep hsr) + cases baseStep_of_primStep Hstep (by solve_subredex_values) cases s - · exact Language.val_irreducible rfl _ + · exact val_irreducible rfl _ · rfl - -instance instAtomicStore {s} {v1 v2 : Val} : Language.Atomic s hl(&v1 ← &v2) where +instance instAtomicStore {s} {v1 v2 : Val} : Atomic s hl(&v1 ← &v2) where atomic {σ obs e' σ' eₜ} Hstep := by - have hsr : EctxLanguage.SubredexesAreValues hl(&v1 ← &v2) := by - apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> try (cases heq; done) - all_goals (cases heq; rfl) - cases (EctxLanguage.baseStep_of_primStep Hstep hsr) + cases baseStep_of_primStep Hstep (by solve_subredex_values) rename_i l v Heq cases s - · exact Language.val_irreducible rfl _ + · exact val_irreducible rfl _ + · rfl + +instance instAtomicFst {s} {v1 : Val} : Atomic s hl(fst(&v1)) where + atomic {σ obs e' σ' eₜ} Hstep := by + cases baseStep_of_primStep Hstep (by solve_subredex_values) + cases s + · exact val_irreducible rfl _ + · rfl + +instance instAtomicSnd {s} {v1 : Val} : Atomic s hl(snd(&v1)) where + atomic {σ obs e' σ' eₜ} Hstep := by + cases baseStep_of_primStep Hstep (by solve_subredex_values) + cases s + · exact val_irreducible rfl _ + · rfl + +instance instAtomicAllocN {s} {v1 v2 : Val} : Atomic s hl(allocn(&v1, &v2)) where + atomic {σ obs e' σ' eₜ} Hstep := by + cases baseStep_of_primStep Hstep (by solve_subredex_values) + cases s + · exact val_irreducible rfl _ + · rfl + +instance instAtomicFree {s} {v : Val} : Atomic s hl(free(&v)) where + atomic {σ obs e' σ' eₜ} Hstep := by + cases baseStep_of_primStep Hstep (by solve_subredex_values) + cases s + · exact val_irreducible rfl _ · rfl -instance instAtomicSnd {s} {v1 : Val} : Language.Atomic s hl(snd(&v1)) where +instance instAtomicXchg {s} {v1 v2 : Val} : Atomic s hl(xchg(&v1, &v2)) where atomic {σ obs e' σ' eₜ} Hstep := by - have hsr : EctxLanguage.SubredexesAreValues hl(snd(&v1)) := by - apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> try (cases heq; done) - · cases heq; rfl - cases (EctxLanguage.baseStep_of_primStep Hstep hsr) + cases baseStep_of_primStep Hstep (by solve_subredex_values) cases s - · exact Language.val_irreducible rfl _ + · exact val_irreducible rfl _ · rfl -instance instAtomicCmpXChg {s} {v1 v2 v3 : Val} : Language.Atomic s hl(cmpXchg(&v1, &v2, &v3)) where +instance instAtomicFaa {s} {v1 v2 : Val} : Atomic s hl(faa(&v1, &v2)) where atomic {σ obs e' σ' eₜ} Hstep := by - have hsr : EctxLanguage.SubredexesAreValues hl(cmpXchg(&v1, &v2, &v3)) := by - apply EctxItemLanguage.subredexes_are_values - intro Ki e_inner heq - cases Ki <;> try (cases heq; done) - all_goals (cases heq; rfl) - cases (EctxLanguage.baseStep_of_primStep Hstep hsr) + cases baseStep_of_primStep Hstep (by solve_subredex_values) cases s - · exact Language.val_irreducible rfl _ + · exact val_irreducible rfl _ · rfl +instance instAtomicFork {s} {e : Exp} : Atomic s hl(fork(&e)) where + atomic {σ obs e' σ' eₜ} Hstep := by + cases baseStep_of_primStep Hstep (by solve_subredex_values) + cases s + · exact val_irreducible rfl _ + · rfl + +instance instAtomicNewProph {s} : Atomic s (State := State) Exp.newProph where + atomic {σ obs e' σ' eₜ} Hstep := by + cases baseStep_of_primStep Hstep (by solve_subredex_values) + cases s + · exact val_irreducible rfl _ + · rfl + +instance instAtomicCmpXChg {s} {v1 v2 v3 : Val} : Atomic s hl(cmpXchg(&v1, &v2, &v3)) where + atomic {σ obs e' σ' eₜ} Hstep := by + cases baseStep_of_primStep Hstep (by solve_subredex_values) + cases s + · exact val_irreducible rfl _ + · rfl + +theorem primStep_val_baseStep {e : Exp} {σ : State} {obs : List Observation} + {v : Val} {σ' : State} {efs : List Exp} + (h : PrimStep.primStep (e, σ) obs (Exp.val v, σ', efs)) : + BaseStep e σ obs (Exp.val v) σ' efs := by + generalize hg : (Exp.val v : Exp) = g at h + obtain ⟨Hbase⟩ := h + rename_i a b K + obtain rfl : K = [] := fill_isSome_empty (e := b) (by simp [← hg]) + simp only [EvContext.fill, List.foldl_nil] at hg ⊢ + subst hg + exact Hbase + +theorem base_step_to_val_always_to_val + {e₁ : Exp} {σ₁ₐ : State} {κsₐ : List Observation} {v₂ₐ : Val} {σ₂ₐ : State} + {efsₐ : List Exp} {σ₁ᵦ : State} {κsᵦ : List Observation} + {e₂ᵦ : Exp} {σ₂ᵦ : State} {efsᵦ : List Exp} + (h₁ : BaseStep e₁ σ₁ₐ κsₐ (Exp.val v₂ₐ) σ₂ₐ efsₐ) + (h₂ : BaseStep e₁ σ₁ᵦ κsᵦ e₂ᵦ σ₂ᵦ efsᵦ) : + (toVal e₂ᵦ).isSome := by + cases h₁ <;> cases h₂ <;> simp_all [] <;> grind + +theorem prim_step_to_val_always_to_val + {e₁ : Exp} {σ₁ₐ : State} {κsₐ : List Observation} {v₂ₐ : Val} {σ₂ₐ : State} + {efsₐ : List Exp} {σ₁ᵦ : State} {κsᵦ : List Observation} + {e₂ᵦ : Exp} {σ₂ᵦ : State} {efsᵦ : List Exp} + (h₁ : PrimStep.primStep (e₁, σ₁ₐ) κsₐ (Exp.val v₂ₐ, σ₂ₐ, efsₐ)) + (h₂ : PrimStep.primStep (e₁, σ₁ᵦ) κsᵦ (e₂ᵦ, σ₂ᵦ, efsᵦ)) : + (toVal e₂ᵦ).isSome := by + refine base_step_to_val_always_to_val (primStep_val_baseStep h₁) (baseStep_of_primStep h₂ ?_) + intro K e' heq hnv + rcases base_ctx_step_val (K := K) (e := e') (heq ▸primStep_val_baseStep h₁) with h | h + · rw [hnv] at h; simp at h + · exact h + +theorem base_step_to_val_atomic {e₁ : Exp} {σ₁ₐ : State} {κsₐ : List Observation} {v₂ₐ : Val} + {σ₂ₐ : State} {efsₐ : List Exp} (a : Atomicity) (h : BaseStep e₁ σ₁ₐ κsₐ (Exp.val v₂ₐ) σ₂ₐ efsₐ) : + Atomic (State := State) a e₁ := + stronglyAtomic_atomic ⟨prim_step_to_val_always_to_val (primStep_of_baseStep h)⟩ + +/- TODO: Coq has a `Hint Extern (Atomic _ _) => by eapply base_step_to_val_atomic`. + No Lean equivalent — `BaseStep` is not a typeclass, so we can't make this + a real instance. At use sites, manually apply `base_step_to_val_atomic`. -/ + +theorem base_step_more_proph_ids {e : Exp} {σ : State} {κs : List Observation} + {e' : Exp} {σ' : State} {efs : List Exp} (h : BaseStep e σ κs e' σ' efs) : + σ.usedProphId ⊆ σ'.usedProphId := by + induction h with + | newProphS _ p _ => intro x hx; rw [Std.ExtTreeSet.mem_insert]; right; exact hx + | resolveS _ _ _ _ _ _ _ _ _ _ IH => exact IH + | cmpXchgS _ _ _ _ _ b _ _ _ => cases b <;> intro _ hx <;> exact hx + | _ => intro _ hx; exact hx + +theorem step_resolve {e : Exp} {vp vt : Val} {σ₁ σ₂ : State} {κ : List Observation} {e₂ : Exp} {efs : List Exp} + [hatom : Atomic .StronglyAtomic e] + (hprim : PrimStep.primStep (Exp.resolve e (.val vp) (.val vt), σ₁) κ (e₂, σ₂, efs)) : + BaseStep (Exp.resolve e (.val vp) (.val vt)) σ₁ κ e₂ σ₂ efs := by + generalize hsrc : Exp.resolve e (.val vp) (.val vt) = src at hprim + obtain ⟨Hbase⟩ := hprim + rename_i e₁' e₂' K + cases K using List.reverseRec with + | nil => simp only [fill_nil] at hsrc ⊢; subst hsrc; exact Hbase + | append_singleton K' Ki ih => + clear ih + exfalso + cases Ki <;> + simp only [fillItem, ECtxItem.fill, fill_append, fill_cons, fill_nil, + Exp.resolve.injEq, reduceCtorEq] at hsrc + case resolveL K_inner _ _ => + suffices hp : PrimStep.primStep (e, σ₁) κ (fillItem K_inner (fill K' e₂'), σ₂, efs) by + exact absurd (hatom.atomic hp) (by simp [fillItem_expToVal_none]) + rw [hsrc.1] + exact fill_primStep [K_inner] (fill_primStep K' (primStep_of_baseStep Hbase)) + case resolveM => exact baseStep_fill_eq_val_absurd Hbase hsrc.2.1 + case resolveR => exact baseStep_fill_eq_val_absurd Hbase hsrc.2.2 + +theorem prim_step_resolve_of_inner {e : Exp} {σ σ_e : State} {κ_e : List Observation} + {v_e w : Val} {efs_e : List Exp} {p : ProphId} (Hbase_e : BaseStep e σ κ_e (.val v_e) σ_e efs_e) + (hp_contains : σ.usedProphId.contains p) : + PrimStep.primStep (Exp.resolve e (.val (.lit (.prophecy p))) (.val w), σ) + (κ_e ++ [(p, (v_e, w))]) (Exp.val v_e, σ_e, efs_e) := + primStep_of_baseStep (BaseStep.resolveS p v_e e σ w σ_e κ_e efs_e Hbase_e hp_contains) + +theorem step_resolve_decompose {e : Exp} {p : ProphId} {w : Val} {σ₁ σ₂ : State} {κ : List Observation} + {e₂ : Exp} {efs : List Exp} [hatom : Atomic .StronglyAtomic e] + (hstep : PrimStep.primStep (Exp.resolve e (.val (.lit (.prophecy p))) (.val w), σ₁) κ (e₂, σ₂, efs)) : + ∃ (κ_inner : List Observation) (v_inner : Val), + κ = κ_inner ++ [(p, (v_inner, w))] ∧ + e₂ = Exp.val v_inner ∧ + BaseStep e σ₁ κ_inner (.val v_inner) σ₂ efs := + match step_resolve hstep with + | .resolveS _ v_n _ _ _ _ κs_n _ hb _ => ⟨κs_n, v_n, rfl, rfl, hb⟩ + +theorem resolve_reducible {e : Exp} {σ : State} {p : ProphId} {v : Val} + [hatom : Atomic .StronglyAtomic e] (hred : BaseStep.Reducible (e, σ)) + (hin : σ.usedProphId.contains p) : + BaseStep.Reducible (Exp.resolve e (.val (.lit (.prophecy p))) (.val v), σ) := by + obtain ⟨κ, e', σ', efs, hstep⟩ := hred + obtain ⟨w', rfl⟩ : ∃ w', e' = Exp.val w' := by + have hval : (toVal e').isSome := hatom.atomic (primStep_of_baseStep hstep) + cases e' with | val w' => exact ⟨w', rfl⟩ | _ => simp [toVal] at hval + refine ⟨κ ++ [(p, (w', v))], Exp.val w', σ', efs, ?_⟩ + exact .resolveS p w' e σ v σ' κ efs hstep hin + +theorem prim_step_reducible_resolve {e : Exp} {σ : State} {p : ProphId} {w : Val} + [hatom : Atomic .StronglyAtomic e] (hp_contains : σ.usedProphId.contains p) + (hred : PrimStep.Reducible (e, σ)) : + PrimStep.Reducible (Exp.resolve e (.val (.lit (.prophecy p))) (.val w), σ) := by + obtain ⟨κ, e', σ', efs, hprim⟩ := hred + obtain ⟨v, rfl⟩ : ∃ v, e' = Exp.val v := by + match e', (hatom.atomic hprim) with | .val v, _ => exact ⟨v, rfl⟩ + exact primStep_reducible_of_baseStep_reducible + (resolve_reducible ⟨κ, _, σ', efs, primStep_val_baseStep hprim⟩ hp_contains) + +theorem prim_step_more_proph_ids {e : Exp} {σ : State} {κs : List Observation} {e' : Exp} + {σ' : State} {efs : List Exp} (h : PrimStep.primStep (e, σ) κs (e', σ', efs)) : + σ.usedProphId ⊆ σ'.usedProphId := by + obtain ⟨hbase⟩ := h + exact base_step_more_proph_ids hbase + +/-- `resolve e &vp &vt` is atomic whenever its subexpression `e` is strongly +atomic: any step of the whole expression is a `resolveS` base step, which runs +`e` to a value and produces a value. Mirrors `resolve_atomic` in Rocq. -/ +instance instAtomicResolve {s} {e : Exp} {vp vt : Val} [hatom : Atomic .StronglyAtomic e] : + Atomic s (Exp.resolve e (.val vp) (.val vt)) where + atomic {σ obs e' σ' eₜ} Hstep := by + cases step_resolve Hstep with + | resolveS _ v _ _ _ _ _ _ _ _ => + cases s + · exact val_irreducible rfl _ + · rfl + end Iris.HeapLang diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean index 0d4c736ed..49fc26d1a 100644 --- a/Iris/Iris/HeapLang/PrimitiveLaws.lean +++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean @@ -8,36 +8,78 @@ public import Iris.ProgramLogic.WeakestPre public import Iris.ProgramLogic.Adequacy public import Iris.ProgramLogic.Lifting public import Iris.BI.Lib.GenHeap +public import Iris.BI.Lib.ProphMap +public import Iris.Std.GenSetsInstances public import Iris.ProofMode public import Std.Data.ExtTreeMap @[expose] public section namespace Iris.HeapLang -open Iris ProgramLogic Language.Notation Std +open Iris ProgramLogic Language.Notation Std FromMathlib section HeapLangGS abbrev HeapF := fun V => Std.ExtTreeMap Loc V compare +/-- The finite-map type used by the heap_lang prophecy ghost state: a map from +`ProphId` to the prophecy's outstanding resolution list. Mirrors the Rocq +`gmap proph_id (list val)` used in `proph_map`. -/ +abbrev ProphMapF := fun V => Std.ExtTreeMap ProphId V compare + class HeapLangGpreS (hlc : outParam HasLC) (GF : BundledGFunctors) extends InvGpreS GF where heap_pre : genHeapPreS Loc (Option Val) GF HeapF + proph_pre : prophMapPreS ProphId (Val × Val) GF ProphMapF attribute [reducible, instance] HeapLangGpreS.heap_pre +attribute [reducible, instance] HeapLangGpreS.proph_pre class HeapLangGS (hlc : outParam HasLC) (GF : BundledGFunctors) extends InvGS_gen hlc GF where heap : genHeapGS Loc (Option Val) GF HeapF + proph : prophMapGS ProphId (Val × Val) GF ProphMapF attribute [reducible, instance] HeapLangGS.heap +attribute [reducible, instance] HeapLangGS.proph instance HeapLangState [HeapLangGS hlc GF] : StateInterp State Observation GF where - stateInterp σ _ _ _ := genHeapInterp (GF := GF) (H := HeapF) σ.heap + stateInterp σ _ κs _ := iprop( + genHeapInterp (GF := GF) (H := HeapF) σ.heap ∗ + prophMapInterp (GF := GF) (H := ProphMapF) κs σ.usedProphId) + +/-- The state interpretation as a separating conjunction of the heap interp and +the prophecy-map interp. Used to destruct `Hσ` into its two conjuncts after +`wp_lift_atomic_step`. -/ +theorem stateInterp_split [HeapLangGS hlc GF] (σ : State) (ns : Nat) + (κs : List Observation) (nt : Nat) : + stateInterp (GF := GF) σ ns κs nt ⊣⊢ + iprop(genHeapInterp (GF := GF) (H := HeapF) σ.heap ∗ + prophMapInterp (GF := GF) (H := ProphMapF) κs σ.usedProphId) := + Iris.BI.BIBase.BiEntails.rfl + +/-- Normalize a `[] ++ κs` argument to `κs`. Used to rephrase `prophMapInterp` +hypotheses introduced before a step whose observations are `[]` get substituted +in by `cases`. The two sides are definitionally equal. -/ +theorem prophMapInterp_nil_append [HeapLangGS hlc GF] (κs : List Observation) + (ps : Std.ExtTreeSet ProphId) : + iprop(prophMapInterp (GF := GF) (H := ProphMapF) ([] ++ κs) ps) ⊣⊢ + iprop(prophMapInterp (GF := GF) (H := ProphMapF) κs ps) := + Iris.BI.BIBase.BiEntails.rfl instance HeapLang [HeapLangGS hlc GF] : IrisGS_gen hlc Exp GF where numLatersPerStep n := 0 forkPost v := iprop(True) stateInterp_mono σ ns obs nt := by iintro $ +/-- The state interpretation is closed under bumping the step counter. In +iris-lean this is trivial, since the heap_lang `stateInterp` ignores the step +index. Mirrors `state_interp_step` in `case_studies/heaplang/fixes.v`. -/ +theorem state_interp_step [HeapLangGS hlc GF] (σ : State) (ns : Nat) + (κs : List Observation) (nt : Nat) : + stateInterp (GF := GF) σ ns κs nt ⊢ |==> stateInterp (GF := GF) σ (ns + 1) κs nt := by + iintro H + imodintro + iexact H + def HeapLangS : BundledGFunctors | 0 => ⟨InvMapF, by infer_instance⟩ | 1 => ⟨constOF (DisjointLeibnizSet CoPset), by infer_instance⟩ @@ -46,6 +88,7 @@ def HeapLangS : BundledGFunctors | 4 => ⟨constOF (HeapView Loc (Agree (LeibnizO (Option Val))) HeapF), by infer_instance⟩ | 5 => ⟨constOF (HeapView Loc (Agree (LeibnizO GName)) HeapF), by infer_instance⟩ | 6 => ⟨constOF MetaUR, by infer_instance⟩ + | 7 => ⟨constOF (HeapView ProphId (Agree (LeibnizO (List (Val × Val)))) ProphMapF), by infer_instance⟩ | _ => ⟨constOF Unit, by infer_instance⟩ instance instHeapLangGS_HeapLangS : HeapLangGpreS HasLC.hasLC HeapLangS where @@ -64,6 +107,10 @@ instance instHeapLangGS_HeapLangS : HeapLangGpreS HasLC.hasLC HeapLangS where · constructor exists 5 · exists 6 + proph_pre := by + constructor + · constructor + exists 7 end HeapLangGS @@ -83,19 +130,25 @@ theorem heap_adequacy [HeapLangGpreS .hasLC GF] (e : Exp) σ (φ : Val → Prop) (Std.PartialMap.map (fun g : GName => toAgree (LeibnizO.mk g)) (∅ : HeapF GName))) HeapView.auth_one_valid with ⟨%γm, Hm⟩ - letI _ : HeapLangGS .hasLC GF := ⟨⟨γh, γm⟩⟩ + imod (ProphMap.init (V := Val × Val) (H := ProphMapF) κs σ.usedProphId) + with ⟨%Gproph, Hproph⟩ + letI _ : HeapLangGS .hasLC GF := ⟨⟨γh, γm⟩, Gproph⟩ imodintro - iexists (fun σ _ => Iris.genHeapInterp (GF := GF) (H := HeapF) σ.heap) + iexists (fun σ κs => iprop( + Iris.genHeapInterp (GF := GF) (H := HeapF) σ.heap ∗ + Iris.prophMapInterp (GF := GF) (H := ProphMapF) κs σ.usedProphId)) iexists (fun _ => iprop(True)) - isplitl [Hh Hm] - · simp only [Iris.genHeapInterp] - iexists (∅ : HeapF GName) - isplitr - · ipureintro - intro k hk - simp [Std.PartialMap.dom, LawfulPartialMap.get?_empty] at hk - unfold ghost_map_auth - iframe Hh Hm + isplitl [Hh Hm Hproph] + · isplitl [Hh Hm] + · simp only [Iris.genHeapInterp] + iexists (∅ : HeapF GName) + isplitr + · ipureintro + intro k hk + simp [Std.PartialMap.dom, LawfulPartialMap.get?_empty] at hk + unfold ghost_map_auth + iframe Hh Hm + · iexact Hproph · exact Hwp end Adequacy @@ -124,6 +177,7 @@ theorem wp_fork {e : Exp} : iintro HΦ Hwp iapply wp_lift_atomic_step rfl iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ have Hred : BaseStep.Reducible (hl(fork(&e)), σ₁) := ⟨[], hl(#BaseLit.unit), σ₁, [e], by constructor⟩ isplitr @@ -132,8 +186,41 @@ theorem wp_fork {e : Exp} : exact (primStep_reducible_of_baseStep_reducible Hred) iintro !> %e₂ %σ₂ %eₜ %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq - iframe Hσ + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph imodintro + isplitl [Hσ Hproph] + · iapply (stateInterp_split σ₁ (ns + 1) obs' (nt + [e].length)).mpr + iframe Hσ Hproph + isplitr [Hwp] + · iexists _ + iframe HΦ + ipureintro; rfl + · iapply BI.BigSepL.bigSepL_singleton + iframe Hwp + +/-- Fancy-update-flavoured fork rule. Mirrors `wp_fork_fupd` in +`case_studies/heaplang/fixes.v`. -/ +theorem wp_fork_fupd {e : Exp} : + (▷ |={E}=> (WP e @ s; ⊤ {{ _v, True }} ∗ Φ (hl_val(#())))) ⊢ + WP hl(fork(&e)) @ s; E {{ Φ }} := by + iintro HeΦ + iapply wp_lift_atomic_step rfl + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + have Hred : BaseStep.Reducible (hl(fork(&e)), σ₁) := + ⟨[], hl(#BaseLit.unit), σ₁, [e], by constructor⟩ + isplitr + · ipureintro + cases s <;> simp only [Stuckness.MaybeReducible] + exact (primStep_reducible_of_baseStep_reducible Hred) + iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + cases baseStep_of_primStep_of_baseStep_reducible Hred Heq + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + imod HeΦ with ⟨Hwp, HΦ⟩ + imodintro + isplitl [Hσ Hproph] + · iapply (stateInterp_split σ₁ (ns + 1) obs' (nt + [e].length)).mpr + iframe Hσ Hproph isplitr [Hwp] · iexists _ iframe HΦ @@ -147,7 +234,7 @@ theorem wp_alloc (v : Val) (Φ : Val → IProp GF ) : iintro HΦ iapply wp_lift_atomic_step rfl iintro %σ₁ %ns %obs %obs' %nt Hσ !> - simp only [stateInterp] + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ let l := (List.fresh σ₁.heap.keys).choose have Hne : σ₁.get? l = .none := by simpa [State.get?, get?, getElem?_eq_none_iff, ←Std.ExtTreeMap.mem_keys] @@ -166,14 +253,14 @@ theorem wp_alloc (v : Val) (Φ : Val → IProp GF ) : iintro !> %e₂ %σ₂ %eₜ %Heq Hcr rcases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i l' Hpo Hi - simp only [Int.cast_ofNat_Int, Algebra.BigOpL.bigOpL_nil, Int.toNat_one, List.range_one, - List.foldl_cons, List.foldl_nil] + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + simp only [stateInterp, Int.cast_ofNat_Int, Algebra.BigOpL.bigOpL_nil, Int.toNat_one, + List.range_one, List.foldl_cons, List.foldl_nil] specialize Hi 0 (by simp) (by simp) rw [show l' + (0 : Int) = l' by cases l'; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] at Hi ⊢ imod genHeap_alloc (v := some v) Hi $$ Hσ with ⟨Hσ, Hpt, _Hmt⟩ imodintro - -- FIXME: can iframe should solve emp? - iframe Hσ + iframe Hσ Hproph isplit <;> try itrivial iexists hl_val(#(BaseLit.loc l')) isplit; ipureintro; rfl @@ -186,6 +273,7 @@ theorem wp_load {l : Loc} {q} {v : Val} Φ : iintro >Hpt HΦ iapply wp_lift_atomic_step rfl iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = v⌝ $$ [Hσ Hpt] · ihave >%_ := genHeap_valid $$ [$Hσ $Hpt] itrivial @@ -203,8 +291,9 @@ theorem wp_load {l : Loc} {q} {v : Val} Φ : rw [Hpt] at H; simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H subst H - simp only [Algebra.BigOpL.bigOpL_nil] - iframe Hσ + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + simp only [stateInterp, Algebra.BigOpL.bigOpL_nil] + iframe Hσ Hproph imodintro isplit <;> try itrivial iexists _; isplit @@ -218,7 +307,7 @@ theorem wp_store {l : Loc} {v v' : Val} Φ : iintro >Hpt HΦ iapply wp_lift_atomic_step rfl iintro %σ₁ %ns %obs %obs' %nt Hσ !> - simp only [stateInterp] + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some v')⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -236,12 +325,13 @@ theorem wp_store {l : Loc} {v v' : Val} Φ : rw [Hpt] at H; simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H subst H - simp only [Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, List.foldl_nil, - Algebra.BigOpL.bigOpL_nil] + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + simp only [stateInterp, Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, + List.foldl_nil, Algebra.BigOpL.bigOpL_nil] rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] imod genHeap_update (v₂ := .some v) $$ [$Hσ $Hpt] with ⟨Hσ, Hpt⟩ imodintro - iframe Hσ + iframe Hσ Hproph isplit <;> try itrivial iexists .lit .unit isplit @@ -257,7 +347,7 @@ theorem wp_cmpXchg_fail {l : Loc} {q} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp iintro >Hpt iapply wp_lift_atomic_step rfl iintro %σ₁ %ns %obs %obs' %nt Hσ !> - simp only [stateInterp] + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some v')⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -276,18 +366,21 @@ theorem wp_cmpXchg_fail {l : Loc} {q} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp rw [Hpt] at H simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H subst H + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph simp only [Algebra.BigOpL.bigOpL_nil] subst Heq4; simp only [toVal] at Heq1 Heq2 obtain ⟨rfl⟩ := Heq1 obtain ⟨rfl⟩ := Heq2 simp only [Heq4, Bool.false_eq_true, ↓reduceIte] imodintro - iframe Hσ + simp + simp [stateInterp] + iframe Hσ Hproph isplit <;> try itrivial iexists hl_val((&v', #false)) iframe Hpt - ipureintro; simp [toVal] - rfl + ipureintro + simp theorem wp_cmpXchg_true {l : Loc} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v2 : Val} (Heq1 : toVal e1 = .some v1) (Heq2 : toVal e2 = .some v2) (Heq3 : v'.compareSafe v1) @@ -298,7 +391,7 @@ theorem wp_cmpXchg_true {l : Loc} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v iintro >Hpt iapply wp_lift_atomic_step rfl iintro %σ₁ %ns %obs %obs' %nt Hσ !> - simp only [stateInterp] + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some v')⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -317,7 +410,8 @@ theorem wp_cmpXchg_true {l : Loc} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v rw [Hpt] at H simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H subst H - simp only [Algebra.BigOpL.bigOpL_nil] + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + simp only [stateInterp, Algebra.BigOpL.bigOpL_nil] subst Heq4; simp only [toVal] at Heq1 Heq2 obtain ⟨rfl⟩ := Heq1 obtain ⟨rfl⟩ := Heq2 @@ -326,13 +420,287 @@ theorem wp_cmpXchg_true {l : Loc} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] imod genHeap_update (v₂ := .some v2) $$ [$Hσ $Hpt] with ⟨Hσ, Hpt⟩ imodintro - iframe Hσ + iframe Hσ Hproph isplit <;> try itrivial iexists hl_val((&v', #true)) iframe Hpt ipureintro; simp [toVal] rfl +theorem wp_free {l : Loc} {v : Val} : + ▷ (l ↦ some v) + ⊢@{IProp GF} WP (Exp.free (.val (.lit (.loc l)))) @ s; E + {{ v'', ⌜v'' = Val.lit BaseLit.unit⌝ ∗ (l ↦ (none : Option Val)) }} := by + iintro >Hpt + iapply wp_lift_atomic_step rfl + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + ihave %Hpt : ⌜σ₁.get? l = .some (.some v)⌝ $$ [Hσ Hpt] + · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' + itrivial + ihave %Hred : ⌜BaseStep.Reducible (Exp.free (.val (.lit (.loc l))), σ₁)⌝ $$ [] + · ipureintro + exists [], (.val (.lit .unit)), (σ₁.initHeap l 1 none), [] + refine BaseStep.freeS l v _ ?_; grind + isplitr + · ipureintro + cases s <;> simp only [Stuckness.MaybeReducible] + exact primStep_reducible_of_baseStep_reducible Hred + iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + cases baseStep_of_primStep_of_baseStep_reducible Hred Heq + rename_i v'' H + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + simp only [stateInterp, Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, + List.foldl_nil, Algebra.BigOpL.bigOpL_nil] + rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] + imod genHeap_update (v₂ := (none : Option Val)) $$ [$Hσ $Hpt] with ⟨Hσ, Hpt⟩ + imodintro + iframe Hσ Hproph + isplit <;> try itrivial + iexists .lit .unit + iframe Hpt + ipureintro; simp [toVal]; rfl + +theorem wp_xchg {l : Loc} {v w : Val} : + ▷ (l ↦ some v) + ⊢@{IProp GF} WP (Exp.xchg (.val (.lit (.loc l))) (.val w)) @ s; E + {{ v'', ⌜v'' = v⌝ ∗ (l ↦ some w) }} := by + iintro >Hpt + iapply wp_lift_atomic_step rfl + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + ihave %Hpt : ⌜σ₁.get? l = .some (.some v)⌝ $$ [Hσ Hpt] + · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' + itrivial + ihave %Hred : ⌜BaseStep.Reducible (Exp.xchg (.val (.lit (.loc l))) (.val w), σ₁)⌝ $$ [] + · ipureintro + exists [], (.val v), (σ₁.initHeap l 1 w), [] + refine BaseStep.xchgS l v w _ ?_; grind + isplitr + · ipureintro + cases s <;> simp only [Stuckness.MaybeReducible] + exact primStep_reducible_of_baseStep_reducible Hred + iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + cases baseStep_of_primStep_of_baseStep_reducible Hred Heq + rename_i v1' H + obtain rfl : v = v1' := by + rw [Hpt] at H + simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H + exact H + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + simp only [stateInterp, Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, + List.foldl_nil, Algebra.BigOpL.bigOpL_nil] + rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] + imod genHeap_update (v₂ := (some w : Option Val)) $$ [$Hσ $Hpt] with ⟨Hσ, Hpt⟩ + imodintro + iframe Hσ Hproph + isplit <;> try itrivial + iexists v + iframe Hpt + ipureintro; simp [toVal]; rfl + +theorem wp_faa {l : Loc} {i1 i2 : Int} : + ▷ (l ↦ some (Val.lit (.int i1))) + ⊢@{IProp GF} WP (Exp.faa (.val (.lit (.loc l))) (.val (.lit (.int i2)))) @ s; E + {{ v'', ⌜v'' = Val.lit (.int i1)⌝ ∗ (l ↦ some (Val.lit (.int (i1 + i2)))) }} := by + iintro >Hpt + iapply wp_lift_atomic_step rfl + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + ihave %Hpt : ⌜σ₁.get? l = .some (.some (Val.lit (.int i1)))⌝ $$ [Hσ Hpt] + · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' + itrivial + ihave %Hred : + ⌜BaseStep.Reducible (Exp.faa (.val (.lit (.loc l))) (.val (.lit (.int i2))), σ₁)⌝ $$ [] + · ipureintro + exists [], (.val (.lit (.int i1))), (σ₁.initHeap l 1 (some (.lit (.int (i1 + i2))))), [] + refine BaseStep.faaS l i1 i2 _ ?_; grind + isplitr + · ipureintro + cases s <;> simp only [Stuckness.MaybeReducible] + exact primStep_reducible_of_baseStep_reducible Hred + iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + cases baseStep_of_primStep_of_baseStep_reducible Hred Heq + rename_i i1' H + obtain rfl : i1 = i1' := by + rw [Hpt] at H + simp only [Option.some.injEq, Val.lit.injEq, BaseLit.int.injEq] at H + exact H + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + simp only [stateInterp, Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, + List.foldl_nil, Algebra.BigOpL.bigOpL_nil] + rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] + imod genHeap_update (v₂ := (some (Val.lit (.int (i1 + i2))) : Option Val)) $$ [$Hσ $Hpt] + with ⟨Hσ, Hpt⟩ + imodintro + iframe Hσ Hproph + isplit <;> try itrivial + iexists Val.lit (.int i1) + iframe Hpt + ipureintro; simp [toVal]; rfl + +/-- The state update of a `newProphS` step (insertion into `usedProphId`) is the +same set as `{p} ∪ usedProphId`, which is what `ProphMap.new_proph` returns. -/ +theorem usedProph_insert_eq {ps : Std.ExtTreeSet ProphId compare} {p : ProphId} : + ps.insert p = ({p} ∪ ps : Std.ExtTreeSet ProphId compare) := by + apply Std.ExtTreeSet.ext_mem + intro x + rw [Std.ExtTreeSet.mem_insert, Std.ExtTreeSet.mem_union_iff, + Iris.Std.LawfulSet.mem_singleton, Std.LawfulEqCmp.compare_eq_iff_eq] + constructor + · rintro (rfl | h) + · left; rfl + · right; exact h + · rintro (rfl | h) + · left; rfl + · right; exact h + +/-- Allocate a fresh prophecy variable. Mirrors `wp_new_proph` in `iris.heap_lang.lifting`. -/ +theorem wp_new_proph : + ⊢ WP (Exp.newProph : Exp) @ s; E + {{ v, ∃ p : ProphId, ∃ pvs : List (Val × Val), + ⌜v = .lit (.prophecy p)⌝ ∗ proph p pvs }} := by + iapply wp_lift_atomic_step rfl + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + -- Pick a prophecy id fresh in the current `usedProphId`. + obtain ⟨pf, Hpf⟩ := Iris.Std.List.fresh σ₁.usedProphId.toList + have Hpf_contains : ¬ σ₁.usedProphId.contains pf := by + intro hc; exact Hpf (Std.ExtTreeSet.mem_toList.mpr hc) + have Hred : BaseStep.Reducible (Exp.newProph, σ₁) := + ⟨[], _, _, [], BaseStep.newProphS σ₁ pf Hpf_contains⟩ + isplitr + · ipureintro + cases s <;> simp only [Stuckness.MaybeReducible] + exact primStep_reducible_of_baseStep_reducible Hred + iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + cases baseStep_of_primStep_of_baseStep_reducible Hred Heq + rename_i p' Hp' + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + -- Convert `¬ contains` to `∉` for `ProphMap.new_proph`. + have Hp'_mem : p' ∉ σ₁.usedProphId := + fun hmem => Hp' (Std.ExtTreeSet.mem_iff_contains.symm.mp hmem) + imod (ProphMap.new_proph p' σ₁.usedProphId obs' Hp'_mem) $$ Hproph + with ⟨Hproph', Htok⟩ + imodintro + simp only [stateInterp] + iframe Hσ + isplitl [Hproph'] + · -- Bridge `{p'} ∪ σ₁.usedProphId` (from new_proph) and `σ₁.usedProphId.insert p'` + -- (from the newProphS constructor's output). + rw [show ({p'} ∪ σ₁.usedProphId : Std.ExtTreeSet ProphId compare) + = σ₁.usedProphId.insert p' from usedProph_insert_eq.symm] + iexact Hproph' + isplitl [Htok] + · iexists hl_val(#(BaseLit.prophecy p')) + isplit + · ipureintro; simp [toVal]; rfl + iexists p', _ + iframe Htok + ipureintro; rfl + · simp only [Algebra.BigOpL.bigOpL_nil]; itrivial + +/-- `Resolve e (Val (LitProphecy p)) (Val w)` lifts a WP for the inner expression +`e` through the `Resolve` wrapper, consuming the front observation `(v_e, w)` +from the prophecy `p`. The inner WP is allowed to use the prophecy token +`proph p pvs` while reducing `e`; on completion the postcondition is closed +under reattaching the front observation. Mirrors `wp_resolve_strong` in Rocq +heap_lang's `primitive_laws.v`. -/ +theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)} + (hatom : Language.Atomic (State := State) (Obs := Observation) + Language.Atomicity.StronglyAtomic e) + (hne : toVal e = none) : + proph p pvs -∗ + (proph p pvs -∗ WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ + ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) -∗ + WP (Exp.resolve e (.val (.lit (.prophecy p))) (.val w)) @ s; E {{ Φ }} := by + -- Mirrors Rocq `iris/heap_lang/primitive_laws.v:726–758`. The proof breaks + -- the WP abstraction by unfolding `wp_unfold` directly on the inner WP for + -- `e`, reverse-inducting on the outer observation list, and threading the + -- trailing observation through the prophecy map via `ProphMap.resolve_proph`. + iintro Hp HWPe + iapply wp_lift_step_fupdN rfl + iintro %σ₁ %ns %obs %obs' %nt Hσ + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hheap, Hpmap⟩ + -- Extract `p ∈ σ₁.usedProphId` (pure conclusion via `ProphMap.agree`, + -- preserving `Hpmap` and `Hp` via the `$` frame markers). + icases ProphMap.agree (obs ++ obs') σ₁.usedProphId p pvs $$ [$Hpmap $Hp] + with %Hagree + have Hp_mem : p ∈ σ₁.usedProphId := Hagree.1 + have hp_contains : σ₁.usedProphId.contains p := + Std.ExtTreeSet.mem_iff_contains.mp Hp_mem + -- Feed the prophecy token to the inner WP wand, then open into the step + -- branch via `wp_unfold` + `wp.pre`-reduction (the Lean-eq bridge). + ihave HWPe : iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ + ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) + $$ [Hp HWPe] + · iapply HWPe; iexact Hp + ihave HWPe := (show iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ + ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) ⊢ _ + by rw [wp_unfold.to_eq]; simp only [wp.pre, hne]; exact .rfl) $$ HWPe + -- Reverse-induct on the outer observation list `obs`. + cases obs using List.reverseRec with + | nil => + -- obs = []. Apply inner WP with inner obs = [], inner obs' = obs'. + ihave Hσ_e : iprop(stateInterp σ₁ ns ([] ++ obs') nt) $$ [Hheap Hpmap] + · iapply (stateInterp_split σ₁ ns ([] ++ obs') nt).mpr + iframe Hheap + iexact Hpmap + imod HWPe $$ %_ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, HWPe⟩ + imodintro + isplitr + · ipureintro + cases s <;> simp only [Stuckness.MaybeReducible] + exact prim_step_reducible_resolve hp_contains Hred_e + iintro %e₂ %σ₂ %eₜ %Hstep _Hcred + exfalso + obtain ⟨κ_inner, _, hκ_eq, _, _⟩ := step_resolve_decompose Hstep + exact List.cons_ne_nil _ _ (List.append_eq_nil_iff.mp hκ_eq.symm).2 + | append_singleton init lastObs _ => + -- obs = init ++ [lastObs]. Apply inner WP with inner obs = init, + -- inner obs' = lastObs :: obs'. + have hassoc : (init ++ [lastObs]) ++ obs' = init ++ (lastObs :: obs') := by simp + ihave Hσ_e : iprop(stateInterp σ₁ ns (init ++ (lastObs :: obs')) nt) + $$ [Hheap Hpmap] + · iapply (stateInterp_split σ₁ ns (init ++ (lastObs :: obs')) nt).mpr + iframe Hheap + rw [← hassoc]; iexact Hpmap + imod HWPe $$ %_ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, HWPe⟩ + imodintro + isplitr + · ipureintro + cases s <;> simp only [Stuckness.MaybeReducible] + exact prim_step_reducible_resolve hp_contains Hred_e + iintro %e₂ %σ₂ %eₜ %Hstep Hcred + obtain ⟨κ_inner, v_inner, hκ_eq, he₂_eq, Hbase_e⟩ := step_resolve_decompose Hstep + have h := congrArg List.reverse hκ_eq + simp at h + obtain ⟨hκ_eq_init, hlast_eq⟩ := h + subst hκ_eq_init; subst hlast_eq; subst he₂_eq + have Hprim_e : PrimStep.primStep (e, σ₁) init (Exp.val v_inner, σ₂, eₜ) := + EctxLanguage.primStep_of_baseStep Hbase_e + ispecialize HWPe $$ %_ %_ %_ %Hprim_e Hcred + iapply step_fupdN_wand $$ HWPe + iintro HWPe + imod HWPe with ⟨Hσ_post, HWPval, Hefs⟩ + icases (stateInterp_split σ₂ (ns + 1) ((p, (v_inner, w)) :: obs') (nt + eₜ.length)).mp + $$ Hσ_post with ⟨Hheap_e, Hpmap_e⟩ + ihave HWPval := wp_value_fupd'.mp $$ HWPval + imod HWPval with ⟨%pvs', Hele, HΦ⟩ + icombine Hpmap_e Hele as Hcomb + imod (ProphMap.resolve_proph (V := Val × Val) (H := ProphMapF) + p (v_inner, w) obs' σ₂.usedProphId pvs') $$ Hcomb + with ⟨%pvs'', %hpvs'_eq, Hpmap_e, Hele⟩ + imodintro + isplitl [Hheap_e Hpmap_e] + · iapply (stateInterp_split σ₂ (ns + 1) obs' (nt + eₜ.length)).mpr + iframe Hheap_e + iexact Hpmap_e + isplitr [Hefs] + · iapply wp_value' + iapply HΦ $$ %pvs'' %hpvs'_eq Hele + · iexact Hefs + end Lifting end Iris.HeapLang diff --git a/Iris/Iris/HeapLang/Syntax.lean b/Iris/Iris/HeapLang/Syntax.lean index cc9055bd3..66a3aff68 100644 --- a/Iris/Iris/HeapLang/Syntax.lean +++ b/Iris/Iris/HeapLang/Syntax.lean @@ -69,6 +69,10 @@ instance : Std.LawfulEqOrd ProphId where intros l₁ l₂; unfold compare; unfold instOrdProphId; simp; intros h; ext; assumption +instance : InfiniteType ProphId where + enum n := .mk n + enum_inj n m := by grind + inductive Binder where | anon | named (name : String) diff --git a/Iris/Iris/Instances/Lib/CInvariants.lean b/Iris/Iris/Instances/Lib/CInvariants.lean index ae70b3056..00bade62c 100644 --- a/Iris/Iris/Instances/Lib/CInvariants.lean +++ b/Iris/Iris/Instances/Lib/CInvariants.lean @@ -235,6 +235,8 @@ theorem acc_strong (E : CoPset) (N : Namespace) (γ : GName) (p : Qp) (P : IProp · iexfalso iapply own_one_l $$ Hown' Hown +-- FIXME: Args here should be implicit + @[rocq_alias cinv_acc] theorem acc (E : CoPset) (N : Namespace) (γ : GName) (p : Qp) (P : IProp GF) (Hsub : ↑N ⊆ E) : @@ -250,6 +252,16 @@ theorem acc (E : CoPset) (N : Namespace) (γ : GName) (p : Qp) (P : IProp GF) imodintro itrivial +theorem inv_open_fupd {E : CoPset} {N : Namespace} {P : IProp GF} (Hsub : ↑N ⊆ E) : + ⊢ cinv N γ P -∗ (▷ P ∗ Q ∗ own γ q ={E \ N}=∗ P ∗ R) -∗ + (Q ∗ own γ q) ={E}=∗ R := by + iintro #Hinv H ⟨HQ, Hown⟩ + imod acc _ _ _ _ _ Hsub $$ Hinv Hown with ⟨HP, Hown, Hclose⟩ + imod H $$ [$] with ⟨HP, HR⟩; iframe + imod Hclose $$ [HP] with - + · inext; iframe + itrivial + @[rocq_alias cinv_acc_1] theorem acc_one (E : CoPset) (N : Namespace) (γ : GName) (P : IProp GF) (Hsub : ↑N ⊆ E) : ⊢ cinv N γ P -∗ own γ (1 : Qp) ={E}=∗ diff --git a/Iris/Iris/Instances/Lib/GhostMap.lean b/Iris/Iris/Instances/Lib/GhostMap.lean index 84f47095f..71284b1da 100644 --- a/Iris/Iris/Instances/Lib/GhostMap.lean +++ b/Iris/Iris/Instances/Lib/GhostMap.lean @@ -375,6 +375,8 @@ theorem ghost_map_delete {γ} {m : H V} (k : K) (v : V) : iapply iOwn_mono $$ G exact auth_inc_of_pmap_eqv _ map_delete +-- TODO: Make these implicit + @[rocq_alias ghost_map_update] theorem ghost_map_update {γ} {m : H V} (k : K) (v : V) (w : V) : ⊢@{IProp GF} (γ ↪●MAP m) -∗ (γ ↪◯MAP[k] v) ==∗ (γ ↪●MAP insert m k w) ∗ γ ↪◯MAP[k] w := by diff --git a/Iris/Iris/Instances/Lib/Invariants.lean b/Iris/Iris/Instances/Lib/Invariants.lean index 9be9d1fbc..5ab61b6fb 100644 --- a/Iris/Iris/Instances/Lib/Invariants.lean +++ b/Iris/Iris/Instances/Lib/Invariants.lean @@ -97,6 +97,8 @@ open Iris Std LawfulSet variable {GF : BundledGFunctors} [InvGS_gen hlc GF] +-- FIXME: Use iframe + @[rocq_alias own_inv_acc] theorem own_inv_acc (E : CoPset) (N : Namespace) (P : IProp GF) (Hsub : ↑N ⊆ E) : ⊢ own_inv N P ={E, E \ ↑N}=∗ ▷ P ∗ (▷ P ={E \ ↑N, E}=∗ True) := by @@ -243,6 +245,8 @@ open Iris Std LawfulSet variable {GF : BundledGFunctors} [InvGS_gen hlc GF] +-- FIXME: Arguments E, N and P in this section should be made implicit + @[rocq_alias inv_acc] theorem inv_acc (E : CoPset) (N : Namespace) (P : IProp GF) (Hsub : ↑N ⊆ E) : ⊢ inv N P ={E, E \ ↑N}=∗ ▷ P ∗ (▷ P ={E \ ↑N, E}=∗ True) := by @@ -280,6 +284,15 @@ theorem inv_acc_timeless (E : CoPset) (N : Namespace) (P : IProp GF) [Timeless P iapply H inext; iassumption +theorem inv_open_fupd {E : CoPset} {N : Namespace} {P : IProp GF} (Hsub : ↑N ⊆ E) : + ⊢ inv N P -∗ (▷ P ∗ Q ={E \ N}=∗ P ∗ R) -∗ Q ={E}=∗ R := by + iintro #Hinv H HQ + imod inv_acc _ _ _ Hsub $$ Hinv with ⟨HP, Hclose⟩ + imod H $$ [$] with ⟨HP, HR⟩; iframe + imod Hclose $$ [HP] with - + · inext; iframe + itrivial + end Access section Modification diff --git a/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean b/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean new file mode 100644 index 000000000..958c00132 --- /dev/null +++ b/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean @@ -0,0 +1,168 @@ +/- +Copyright (c) 2026 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.Algebra +public import Iris.BI +public import Iris.ProofMode +public import Iris.ProgramLogic.Language +public import Iris.ProgramLogic.EctxLanguage +public import Iris.ProgramLogic.Adequacy +public import Iris.ProgramLogic.ThreadPool +public import Iris.ProgramLogic.AbstractWeakestPre +public import Iris.ProgramLogic.AbstractLangCompleteness +public import Iris.Instances.Lib.Invariants +public import Iris.Instances.Lib.CInvariants +public import Iris.Instances.Lib.GhostMap +public import Iris.Std.FromMathlib + +namespace Iris.ProgramLogic + +open Iris Iris.BI Iris.Algebra Std FromMathlib +open Iris.ProgramLogic.PrimStep +open Language Language.Notation + +@[expose] public section + +section AbstractEctxCompleteness + +variable {Expr State Obs Val Ectx : Type _} +variable [EctxLanguage Expr Ectx State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable [TI : TpinvGS GF Expr H] + +/-- The body of the `ectx_lang_completeness` field of +`AbstractEctxLangCompletenessGen`; mirrors `ectx_lang_completeness` in +`framework/abstract/abstract_ectx_lang_completeness.v` lines 13–31. -/ +public def ectxLangCompletenessStmt [TI : TpinvGS GF Expr H] (wp : AbstractWP Expr Val GF) + (heap_inv : List Expr → State → IProp GF) (n : Nat) (C : List Expr) (e₁ : Expr) (σ : State) + (K : Ectx) (E : CoPset) : IProp GF := iprop% + ⌜BaseStep.Reducible (e₁, σ)⌝ -∗ + (n ↪thread (EvContext.fill K e₁)) -∗ + heap_inv C σ ∗ tpInv C ∗ ⌜cfgSafe (C, σ)⌝ ={E}=∗ + ((⌜Iris.ProgramLogic.Language.Atomic Atomicity.WeaklyAtomic e₁⌝ ∗ + (∀ Φ, + (▷ ∀ κ v₂ σ' efs, + ⌜PrimStep.primStep (e₁, σ) κ ((ToVal.ofVal v₂ : Expr), σ', efs)⌝ -∗ + isThread n (.own 1) (EvContext.fill K e₁) -∗ + tpInv C ==∗ + (heap_inv ((C.set n (EvContext.fill K (ToVal.ofVal v₂))) ++ efs) σ' -∗ + Φ v₂) ∗ + [∗list] _i ↦ etp ∈ efs, wp ⊤ etp (fun (_ : Val) => iprop(True))) -∗ + wp E e₁ Φ)) + ∨ + (heap_inv C σ ∗ tpInv C ∗ ∀ Ψ, + (▷ ∀ e₂ efs, + (∀ σ₁ C₁, + heap_inv C₁ σ₁ ∗ tpInv C₁ ∗ ⌜cfgSafe (C₁, σ₁)⌝ ={E}=∗ + ∃ κ σ₁', + ⌜PrimSteps e₁ σ₁ κ e₂ σ₁' efs⌝ ∗ + isThread n (.own 1) (EvContext.fill K e₁) ∗ + tpInv C₁ ∗ + heap_inv ((C₁.set n (EvContext.fill K e₂)) ++ efs) σ₁') ={⊤}=∗ + wp ⊤ e₂ Ψ ∗ + ([∗list] _j ↦ etp ∈ efs, wp ⊤ etp (fun (_ : Val) => iprop(True)))) -∗ + wp ⊤ e₁ Ψ)) + +/-- *Abstract ectx-completeness theory*: the ectx-language specialization of +`AbstractLangCompletenessGen`. The soundness equation `ectx_lang_completeness` +is phrased for base steps rather than prim steps. -/ +public class AbstractEctxLangCompletenessGen + (wp : AbstractWP Expr Val GF) [BindAbstractWP wp] where + heap_inv : List Expr → State → IProp GF + heap_inv_timeless (C : List Expr) (σ : State) : Timeless (heap_inv C σ) + ectx_lang_completeness (n : Nat) (C : List Expr) (e₁ : Expr) (σ : State) (K : Ectx) (E : CoPset) : + ⊢ ectxLangCompletenessStmt wp heap_inv n C e₁ σ K E + +attribute [instance] AbstractEctxLangCompletenessGen.heap_inv_timeless + +end AbstractEctxCompleteness + +/-! ### Lifting the ectx-level soundness equation to the prim level. -/ + +section Lifting + +variable {Expr State Obs Val Ectx : Type _} +variable [EctxLanguage Expr Ectx State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable [TI : TpinvGS GF Expr H] +variable {wp : AbstractWP Expr Val GF} +variable [BindAbstractWP wp] [InvOpenAbstractWP wp] +variable [AEC : AbstractEctxLangCompletenessGen wp] +variable [CInvG GF] + +omit [InvOpenAbstractWP wp] [CInvG GF] in +/-- Lift the ectx-level reduction soundness equation to a prim-level one. +Mirrors `weakestpre_ectx_to_prim_completeness` in +`framework/abstract/abstract_ectx_lang_completeness.v` lines 37–53. -/ +theorem weakestpre_ectx_to_prim_completeness : + ∀ (n : Nat) (C : List Expr) (e₁ : Expr) (σ : State) (E : CoPset), + ⊢ abstractECTXLangComplete (TI := TI) wp AEC.heap_inv n C e₁ σ E := by + iintro %n %C %e₁ %σ %E %Hred Htok ⟨Hheap, Htp, %Hsafe⟩ + obtain ⟨κ, e', σ', efs, hstep⟩ := Hred + obtain ⟨Hbase⟩ := hstep + rename_i e₁' e₂' K + have Hbred : BaseStep.Reducible (e₁', σ) := ⟨κ, e₂', σ', efs, Hbase⟩ + have key := AEC.ectx_lang_completeness (wp := wp) n C e₁' σ K E + unfold ectxLangCompletenessStmt at key + imod key $$ %Hbred Htok [Hheap Htp] + with (⟨%Hatom, HH⟩ | ⟨Hheap, Htp, HH⟩) + · iframe Hheap Htp + ipureintro; exact Hsafe + · -- Atomic redex: package the context `fill K` and forward the magic premise. + imodintro + ileft + iexists (fill (Expr := Expr) K), e₁' + have Hctx : Context (fill (Expr := Expr) K) := inferInstance + have Heq : fill (Expr := Expr) K e₁' = fill (Expr := Expr) K e₁' := rfl + have Hnv : ToVal.toVal e₁' = none := EctxLanguage.val_stuck Hbase + iframe %Hctx %Heq %Hnv %Hatom + iintro %Ψ Hpre + iapply HH $$ Hpre + · -- Non-atomic redex: reduce the prim-level WP to the ectx-level one via `wp_bind`. + imodintro + iright + iframe Hheap Htp + iintro %Ψ Hc + iapply ((‹BindAbstractWP wp›).wp_bind (K := fill (Expr := Expr) K) (e := e₁') (Φ := Ψ)).1 + iapply HH + inext + iintro %e₂ %efs H + -- Lift the ectx-level step `H` (on the redex `e₁'`) to a prim-level step under `fill K`. + ihave Hprem : iprop(∀ σ₁ C₁, + AEC.heap_inv C₁ σ₁ ∗ tpInv C₁ ∗ ⌜cfgSafe (C₁, σ₁)⌝ ={E}=∗ + ∃ κ σ₁', ⌜PrimSteps (fill (Expr := Expr) K e₁') σ₁ κ (fill (Expr := Expr) K e₂) σ₁' efs⌝ ∗ + (n ↪thread fill (Expr := Expr) K e₁') ∗ tpInv C₁ ∗ + AEC.heap_inv (C₁.set n (fill (Expr := Expr) K e₂) ++ efs) σ₁') $$ [H] + · iintro %σ₁ %C₁ ⟨Hi, Htp1, %Hs⟩ + imod H $$ [Hi Htp1] with ⟨%κ', %σ₁', %Hps, Htok2, Htp1', Hhp⟩ + · iframe Hi Htp1 + ipureintro; exact Hs + imodintro + iexists κ', σ₁' + iframe Htok2 Htp1' Hhp + ipureintro + exact Hps.fill + imod Hc $$ Hprem with ⟨Hwp, Hlist⟩ + imodintro + isplitl [Hwp] + · iapply ((‹BindAbstractWP wp›).wp_bind (K := fill (Expr := Expr) K) (e := e₂) (Φ := Ψ)).2 $$ Hwp + · iexact Hlist + +/-- Every `AbstractEctxLangCompletenessGen` gives an +`AbstractLangCompletenessGen`. -/ +instance abstract_ectx_to_completeness : + AbstractLangCompletenessGen wp where + heap_inv := AEC.heap_inv + heap_inv_timeless C σ := AEC.heap_inv_timeless C σ + lang_completeness := weakestpre_ectx_to_prim_completeness _ _ _ _ _ + +end Lifting + +end + +end Iris.ProgramLogic diff --git a/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean b/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean new file mode 100644 index 000000000..7a0ad9198 --- /dev/null +++ b/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean @@ -0,0 +1,435 @@ +/- +Copyright (c) 2026 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.Algebra +public import Iris.BI +public import Iris.ProofMode +public import Iris.ProgramLogic.Language +public import Iris.ProgramLogic.Adequacy +public import Iris.ProgramLogic.ThreadPool +public import Iris.ProgramLogic.AbstractWeakestPre +public import Iris.Instances.Lib.Invariants +public import Iris.Instances.Lib.CInvariants +public import Iris.Instances.Lib.GhostMap +public import Iris.Std.FromMathlib + +namespace Iris.ProgramLogic + +open Iris Iris.BI Iris.Algebra Std FromMathlib +open Iris.ProgramLogic.PrimStep +open Language Language.Notation + +@[expose] public section + +section AbstractCompleteness + +variable {Expr State Obs Val : Type _} [Language Expr State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable [TI : TpinvGS GF Expr H] + +public abbrev abstractECTXLangComplete (wp : AbstractWP Expr Val GF) (I : List Expr → State → IProp GF) + (n : Nat) (C : List Expr) (e₁ : Expr) (σ : State) (E : CoPset) : + IProp GF := iprop% + ⌜PrimStep.Reducible (e₁, σ)⌝ -∗ (n ↪thread e₁) -∗ I C σ ∗ tpInv C ∗ ⌜cfgSafe (C, σ)⌝ ={E}=∗ + ((∃ (K : Expr → Expr) (e₁' : Expr), + ⌜Context K⌝ ∗ ⌜e₁ = K e₁'⌝ ∗ ⌜ToVal.toVal e₁' = none⌝ ∗ ⌜Atomic .WeaklyAtomic e₁'⌝ ∗ + ∀ Ψ, + (▷ ∀ κ v₂ σ' efs, + ⌜PrimStep.primStep (e₁', σ) κ ((ToVal.ofVal v₂ : Expr), σ', efs)⌝ -∗ + (n ↪thread e₁) -∗ + tpInv C ==∗ + (I ((C.set n (K (ToVal.ofVal v₂))) ++ efs) σ' -∗ Ψ v₂) ∗ + [∗list] _i ↦ etp ∈ efs, wp ⊤ etp (fun (_ : Val) => iprop% True)) -∗ + wp E e₁' Ψ) ∨ + (I C σ ∗ tpInv C ∗ ∀ Ψ, + (▷ ∀ e₂ efs, + (∀ σ₁ C₁, I C₁ σ₁ ∗ tpInv C₁ ∗ ⌜cfgSafe (C₁, σ₁)⌝ ={E}=∗ + ∃ κ σ₁', + ⌜PrimSteps e₁ σ₁ κ e₂ σ₁' efs⌝ ∗ (n ↪thread e₁) ∗ tpInv C₁ ∗ + I ((C₁.set n e₂) ++ efs) σ₁') ={⊤}=∗ + wp ⊤ e₂ Ψ ∗ ([∗list] _j ↦ etp ∈ efs, wp ⊤ etp (fun (_ : Val) => iprop% True))) -∗ + wp ⊤ e₁ Ψ)) + +/-- A weakest precondition for a Language is complete -/ +public class AbstractLangCompletenessGen + (wp : AbstractWP Expr Val GF) [LawfulAbstractWP wp] where + heap_inv : List Expr → State → IProp GF + heap_inv_timeless (C : List Expr) (σ : State) : Timeless (heap_inv C σ) + lang_completeness {n C e₁ σ E} : ⊢ abstractECTXLangComplete wp heap_inv n C e₁ σ E + +attribute [instance] AbstractLangCompletenessGen.heap_inv_timeless + +end AbstractCompleteness + +section Completeness + +variable {Expr State Obs Val : Type _} [Language Expr State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable [TI : TpinvGS GF Expr H] +variable {wp : AbstractWP Expr Val GF} +variable [LWP : LawfulAbstractWP wp] [IAO : InvOpenAbstractWP wp] +variable [ACG : AbstractLangCompletenessGen wp] +variable [CInvG GF] + +/-- Namespace under which the completeness invariant lives. -/ +public def completenessN : Namespace := nroot .@ (1 : Pos) + +/-- The configuration invariant: ownership of a current configuration +(thread pool + state) reachable from the initial one, with the heap and +thread-pool invariants. -/ +public def cfgInv (Cini : List Expr × State) (f : Forking) : IProp GF := iprop% + ∃ cfg : List Expr × State, + ACG.heap_inv cfg.1 cfg.2 ∗ tpInv cfg.1 ∗ ⌜cfgSafeForking cfg f⌝ ∗ ⌜Cini -·->ₜₚ* cfg⌝ + +/-- `cfgInv` is timeless: `heap_inv` is timeless by the class field, `tpInv` by +`tpInv_timeless`, and the reachability/safety conjunct is pure. This is what +lets the later be stripped off the invariant contents after opening it. -/ +instance cfgInv_timeless (Cini : List Expr × State) (f : Forking) : + Timeless (cfgInv (wp := wp) Cini f) := by + unfold cfgInv; infer_instance + +/-- Cancelable invariant package wrapping `cfgInv`. -/ +public def isCcfg (Cini : List Expr × State) (f : Forking) (γ : GName) : IProp GF := + CancelableInvariant.cinv completenessN γ (cfgInv (wp := wp) Cini f) + +instance isCcfg_persistent (Cini : List Expr × State) (f : Forking) (γ : GName) : + Persistent (isCcfg (wp := wp) Cini f γ : IProp GF) := by + unfold isCcfg; infer_instance + +omit [CInvG GF] in +/-- A separating conjunction over a list with a constant body depends only on the +list's length. -/ +theorem bigSepL_const_congr {α β : Type _} {P : IProp GF} {l1 : List α} {l2 : List β} + (h : l1.length = l2.length) : ([∗list] _x ∈ l1, P) ⊣⊢ ([∗list] _x ∈ l2, P) := by + refine (BigSepL.bigSepL_replicate (l := l1) (P := P)).symm.trans + (BiEntails.trans ?_ (BigSepL.bigSepL_replicate (l := l2) (P := P))) + rw [h]; exact .rfl + +/-- Split the cancelable-invariant fraction `own γ ⟨qc⟩` into `l.length + 1` equal +pieces: one for the current thread, plus one piece per forked thread in `l`. The +fraction type must support `n`-way division, hence the specialization to `Qp`. +Mirrors `fractional_divide_n` in `framework/thread_pool.v`. -/ +theorem own_divide_forks {α : Type _} (γ : GName) (qc : Qp) (l : List α) : + CancelableInvariant.own (GF := GF) γ qc ⊢ + CancelableInvariant.own γ (qc.divide_even (l.length + 1) (Nat.succ_pos _) : Qp) ∗ + ([∗list] _x ∈ l, + CancelableInvariant.own γ (qc.divide_even (l.length + 1) (Nat.succ_pos _) : Qp)) := by + have h := fractional_divide_equal + (Φ := fun p : Qp => CancelableInvariant.own (GF := GF) γ p) qc l.length + rw [List.replicate_succ'] at h + refine h.trans ((BigSepL.bigSepL_snoc (Φ := fun _ _ => CancelableInvariant.own (GF := GF) γ + ((qc.divide_even (l.length + 1) (Nat.succ_pos _)) : Qp))).1.trans + (sep_comm.1.trans (sep_mono_right (bigSepL_const_congr (by simp)).1))) + +/-- When there are no forks (`l = []`), dividing by `l.length + 1 = 1` is the +identity. This is the algebraic fact behind `f = doesNotFork → q = q'`. -/ +theorem qp_div_ofPNat_succ_nil {α : Type _} (qc : Qp) {l : List α} (h : l = []) : + qc.divide_even (l.length + 1) (Nat.succ_pos _) = qc := by + subst h + apply Subtype.ext + simp + grind + +theorem weakestpre_completeness + (Cini : List Expr × State) (f : Forking) (γ : GName) (q : Qp) + (n : Nat) (e : Expr) : + isCcfg (TI := TI) (wp := wp) Cini f γ -∗ + CancelableInvariant.own γ q -∗ + isThread (TI := TI) n (.own 1) e -∗ + wp ⊤ e (fun v => iprop% + isThread (TI := TI) n (.own 1) (ToVal.ofVal v) ∗ + ∃ q' : Qp, CancelableInvariant.own γ q' ∗ ⌜f = .doesNotFork → q = q'⌝) := by + iintro #Hinv + iloeb as IH generalizing %q %n %e + iintro Hq He + have Hn : nclose completenessN ⊆ ⊤ := fun _ _ => CoPset.mem_full + have Hn' : ⊤ \ nclose completenessN ⊆ ⊤ := Std.LawfulSet.diff_subset_left + iapply IAO.inv_open_maybe (E₂ := ⊤ \ nclose completenessN) _ _ _ Hn' + unfold isCcfg + imod CancelableInvariant.acc _ _ _ _ _ Hn $$ [$] [$] with ⟨>Hinv2, Hq, Hclose⟩ + unfold cfgInv + icases Hinv2 with ⟨%cfg, Hheap, HtpInv, %Hx⟩ + rcases Hx with ⟨Hsafe, Hreach⟩ + ihave %Hlu := tpInv_lookup $$ [$] [$] + have ⟨HnotStuck, Hforking⟩ := Hsafe .refl + rcases HnotStuck (List.mem_of_getElem? Hlu) with Hv|HnotStuck' + · replace ⟨v, Hv⟩ := Option.isSome_iff_exists.mp Hv + obtain rfl := (coe_of_toVal_eq_some Hv).symm; clear Hv + imodintro + ileft + -- TODO: Can iframe be improved to supply these directly? + have Hframe1 : Context (Expr := Expr) id := by infer_instance + have Hframe2 : (↑v : Expr) = id ↑v := rfl + have Hframe3 : Atomic Atomicity.WeaklyAtomic (↑v : Expr) := val_atomic + iexists id, v + iframe %Hframe1 %Hframe2 %Hframe3 + clear Hframe1 Hframe2 Hframe3 + simp only [id_eq] + iapply LWP.wp_value + imodintro + imod Hclose $$ [HtpInv Hheap] with - + · inext + iexists cfg + iframe Hheap HtpInv %Hreach %Hsafe + · imodintro + iapply LWP.wp_value + imodintro + iframe + iexists q + iframe + ipureintro + grind + · imod AbstractLangCompletenessGen.lang_completeness $$ %HnotStuck' He [Hheap HtpInv] + with (⟨%K, %e₁, %Hctx, %Heq, %Hval, %Hatom, H⟩|⟨Hheap, Htpinv, H⟩) + · have aux : cfgSafe (cfg.fst, cfg.snd) := cfgSafe_of_cfgSafeForking Hsafe + iframe %aux Hheap HtpInv + · imodintro + ileft + iexists K, e₁ + iframe %Hctx %Heq %Hatom + iapply H + iintro !> %κ %v₂ %σ₂' %Hefs %Hbase He HtpInv + -- Divide the fraction `q` among the current thread and the `length Hefs` forks. + icases own_divide_forks γ q Hefs $$ Hq with ⟨Hq, Hefsfrac⟩ + -- Register the forked threads and update the current thread to `K ↑v₂`. + imod (tpInv_update cfg.fst n e (K ↑v₂)) $$ HtpInv He with ⟨HtpInv, He⟩ + imod (tpInv_new_threads Hefs (cfg.fst.set n (K ↑v₂))) $$ HtpInv with ⟨HtpInv, Hefs_threads⟩ + imodintro + isplitl [Hclose Hq He HtpInv] + · -- Current thread: close the invariant at the new configuration, then recurse. + iintro Hheap + have Hprim : (e, cfg.snd) -<κ>-> (K ↑v₂, σ₂', Hefs) := Heq ▸ Context.primStep_fill Hbase + obtain ⟨Hsafe', Hnf⟩ := cfg_safeStep Hsafe Hlu Hprim + imod Hclose $$ [Hheap HtpInv] with - + · inext + iexists (cfg.fst.set n (K ↑v₂) ++ Hefs, σ₂') + iframe Hheap HtpInv + ipureintro + exact ⟨Hsafe', Hreach.tail ⟨κ, cfg_step Hlu Hprim⟩⟩ + imodintro + iapply LWP.wp_wand $$ [Hq He] + · iapply IH $$ Hq He + iintro %v ⟨Hthread, %q', Hq', %Hfork⟩ + iframe Hthread + iexists q' + iframe Hq' + ipureintro + intro hnf + rw [← Hfork hnf] + congr 1 + exact (qp_div_ofPNat_succ_nil q (Hnf hnf)).symm + · -- Forked threads: recurse on each, discarding the postcondition. + ihave Hcomb : iprop([∗list] k ↦ e' ∈ Hefs, + (((cfg.fst.set n (K ↑v₂)).length + k) ↪thread e') ∗ + CancelableInvariant.own γ + (q.divide_even (Hefs.length + 1) (Nat.succ_pos _) : Qp)) + $$ [Hefs_threads Hefsfrac] + · iapply (BigSepL.bigSepL_sep_eqv).2 + iframe Hefs_threads Hefsfrac + iapply BigSepL.bigSepL_impl $$ Hcomb + iintro !> %k %e' %_ ⟨He, Hq⟩ + iapply LWP.wp_wand $$ [Hq He] + · iapply IH $$ Hq He + iintro %v _ + ipureintro + trivial + · imodintro + iright + imod Hclose $$ [Hheap Htpinv] with - + · inext + iexists cfg + -- FIXME: needs a better proof of this + have Hframe : cfgSafeForking cfg f := @«inferInstanceAs» (cfgSafeForking cfg f) Hsafe + iframe Hheap Htpinv %Hreach %Hframe + imodintro + iapply H + inext + iintro %e₂ %efs H + imod CancelableInvariant.acc _ _ _ _ _ Hn $$ [$] [$] with ⟨>Hinv2, Hq, Hclose⟩ + icases Hinv2 with ⟨%cfg2, Hheap, Htpinv, %Hsafe2, %Hreach2⟩ + -- Use the step-producer `H` against the freshly-opened invariant content. + imod H $$ [Hheap Htpinv] with ⟨%κ, %σ1', %Hprim, He, Htpinv, Hhp⟩ + · iframe Hheap Htpinv + ipureintro + exact cfgSafe_of_cfgSafeForking Hsafe2 + -- Divide the fraction and register the new threads. + icases own_divide_forks γ q efs $$ Hq with ⟨Hq, Hefsfrac⟩ + ihave %Hlu2 := tpInv_lookup $$ Htpinv He + obtain ⟨Hsafe2', Hforking2⟩ := cfg_safeSteps Hsafe2 Hlu2 Hprim + imod (tpInv_update cfg2.fst n e e₂) $$ Htpinv He with ⟨Htpinv, He⟩ + imod (tpInv_new_threads efs (cfg2.fst.set n e₂)) $$ Htpinv with ⟨Htpinv, Hefs_threads⟩ + imod Hclose $$ [Hhp Htpinv] with - + · inext + iexists (cfg2.fst.set n e₂ ++ efs, σ1') + iframe Hhp Htpinv + ipureintro + exact ⟨Hsafe2', Hreach2.trans (cfg_steps Hlu2 Hprim)⟩ + imodintro + isplitl [Hq He] + · -- Current thread continues with `e₂`; recurse. + iapply LWP.wp_wand $$ [Hq He] + · iapply IH $$ Hq He + iintro %v ⟨Hthread, %q', Hq', %Hfork⟩ + iframe Hthread + iexists q' + iframe Hq' + ipureintro + intro hnf + rw [← Hfork hnf] + congr 1 + exact (qp_div_ofPNat_succ_nil q (Hforking2 hnf)).symm + · -- Forked threads: recurse on each, discarding the postcondition. + ihave Hcomb : iprop([∗list] k ↦ e' ∈ efs, + (((cfg2.fst.set n e₂).length + k) ↪thread e') ∗ + CancelableInvariant.own γ + (q.divide_even (efs.length + 1) (Nat.succ_pos _) : Qp)) + $$ [Hefs_threads Hefsfrac] + · iapply (BigSepL.bigSepL_sep_eqv).2 + iframe Hefs_threads Hefsfrac + iapply BigSepL.bigSepL_impl $$ Hcomb + iintro !> %k %e' %_ ⟨He, Hq⟩ + iapply LWP.wp_wand $$ [Hq He] + · iapply IH $$ Hq He + iintro %v _ + ipureintro + trivial + + +/-- **Top-level theorem**: `adequate` gives a WP with a pure postcondition. +This is the entry point consumed by the heap-lang case study. Stated on the +generic `AbstractLangCompletenessGen`, carrying `[InvOpenAbstractWP wp]` +(mirrors Rocq's `abstract_weakestpre_gen_magic` hypothesis). -/ +theorem weakestpre_sem_completeness + (e : Expr) (σ : State) (φ : Val → Prop) + (Hade : adequate .NotStuck e σ (fun v _ => φ v)) : + ⊢ tpInvIni (TI := TI) -∗ + ACG.heap_inv [e] σ -∗ + wp ⊤ e (fun v => iprop% ⌜φ v⌝) := by + have Hsafe0 : cfgSafeForking ([e], σ) .doesFork := + fun {C₂} hreach => + ⟨fun {e2} hmem => Hade.adequate_not_stuck _ _ e2 rfl hreach hmem, + fun hf => Forking.noConfusion hf⟩ + iintro Hini Hheap + iapply LWP.fupd_wp + imod (tpInv_set [e]) $$ Hini with ⟨Hauth, Hfrags⟩ + imod (CancelableInvariant.alloc ⊤ completenessN + (cfgInv (wp := wp) ([e], σ) .doesFork)) $$ [Hauth Hheap] with ⟨%γ, #Hinv, Hq⟩ + · inext + unfold cfgInv + iexists ([e], σ) + iframe Hheap Hauth %Hsafe0 + ipureintro + exact .refl + have Hn0 : (completenessN : CoPset) ⊆ ⊤ := fun _ _ => CoPset.mem_full + ihave He0 := (Iris.BI.BigSepL.bigSepL_singleton + (Φ := fun n e' => isThread (TI := TI) n (.own 1) e') (x := e)).1 $$ Hfrags + imodintro + iapply LWP.wp_fupd + ihave Hccfg : iprop(isCcfg (wp := wp) ([e], σ) .doesFork γ) $$ [Hinv] + · unfold isCcfg; iexact Hinv + ihave Hwp := weakestpre_completeness (wp := wp) ([e], σ) .doesFork γ (One.one : Qp) 0 e + $$ Hccfg Hq He0 + iapply LWP.wp_wand $$ Hwp + iintro %v ⟨Hv, %q', Hq', _⟩ + imod (CancelableInvariant.acc ⊤ completenessN γ q' + (cfgInv (wp := wp) ([e], σ) .doesFork) Hn0) $$ Hinv Hq' with ⟨>Hinv2, Hq', Hclose2⟩ + unfold cfgInv + icases Hinv2 with ⟨%cfg, Hheap, Htpinv, %Hsafe2, %Hreach2⟩ + ihave %Hlu := tpInv_lookup $$ Htpinv Hv + imod Hclose2 $$ [Hheap Htpinv] with - + · inext + iexists cfg + iframe Hheap Htpinv %Hsafe2 %Hreach2 + imodintro + ipureintro + obtain ⟨tp2, σ2⟩ := cfg + rcases tp2 with _ | ⟨hd, rest⟩ + · simp at Hlu + · simp only [List.getElem?_cons_zero, Option.some.injEq] at Hlu + subst Hlu + exact Hade.adequate_result rest σ2 v Hreach2 + +/-- Strong nofork variant. -/ +theorem weakestpre_sem_completeness_nofork_strong + (e : Expr) (σ : State) (φ : Val → State → Prop) + (Hade : AdequateNoFork .NotStuck e σ (fun v σ' => φ v σ')) : + ⊢ tpInvIni (TI := TI) -∗ + ACG.heap_inv [e] σ -∗ + wp ⊤ e (fun v => + iprop% ∃ σ' : State, + tpInv (TI := TI) [ToVal.ofVal v] ∗ + isThread (TI := TI) 0 (.own 1) (ToVal.ofVal v) ∗ + ACG.heap_inv [ToVal.ofVal v] σ' ∗ + ⌜φ v σ'⌝) := by + have Hsafe0 : cfgSafeForking ([e], σ) .doesNotFork := by + rintro ⟨tp2, σ2⟩ hreach + refine ⟨fun {e2} hmem => Hade.not_stuck rfl hreach hmem, ?_⟩ + intro _ e2 hmem e' σ' κ efs hstep + exact adequateNoFork_efs_nil Hade hreach hmem hstep + have Hn0 : (completenessN : CoPset) ⊆ ⊤ := fun _ _ => CoPset.mem_full + iintro Hini Hheap + iapply LWP.fupd_wp + imod (tpInv_set [e]) $$ Hini with ⟨Hauth, Hfrags⟩ + imod (CancelableInvariant.alloc ⊤ completenessN + (cfgInv (wp := wp) ([e], σ) .doesNotFork)) $$ [Hauth Hheap] with ⟨%γ, #Hinv, Hq⟩ + · inext + unfold cfgInv + iexists ([e], σ) + iframe Hheap Hauth %Hsafe0 + ipureintro + exact .refl + ihave He0 := (Iris.BI.BigSepL.bigSepL_singleton + (Φ := fun n e' => isThread (TI := TI) n (.own 1) e') (x := e)).1 $$ Hfrags + imodintro + iapply LWP.wp_fupd + ihave Hccfg : iprop(isCcfg (wp := wp) ([e], σ) .doesNotFork γ) $$ [Hinv] + · unfold isCcfg; iexact Hinv + ihave Hwp := weakestpre_completeness (wp := wp) ([e], σ) .doesNotFork γ (One.one : Qp) 0 e + $$ Hccfg Hq He0 + iapply LWP.wp_wand $$ Hwp + iintro %v ⟨Hv, %q', Hq', %His1⟩ + obtain rfl := His1 rfl + imod (CancelableInvariant.cancel ⊤ completenessN γ + (cfgInv (wp := wp) ([e], σ) .doesNotFork) Hn0) $$ Hinv Hq' with >Hinv2 + unfold cfgInv + icases Hinv2 with ⟨%cfg, Hheap, Htpinv, %Hsafe2, %Hreach2⟩ + ihave %Hlu := tpInv_lookup $$ Htpinv Hv + imodintro + obtain ⟨tp2, σ2⟩ := cfg + rcases tp2 with _ | ⟨hd, rest⟩ + · simp at Hlu + · simp only [List.getElem?_cons_zero, Option.some.injEq] at Hlu + subst Hlu + have hlen := Hade.no_fork Hreach2 + rw [List.length_cons] at hlen + obtain rfl := List.length_eq_zero_iff.mp (by omega : rest.length = 0) + iexists σ2 + iframe Htpinv Hv Hheap + ipureintro + exact Hade.result Hreach2 + +/-- User-facing nofork variant. -/ +theorem weakestpre_sem_completeness_nofork + (e : Expr) (σ : State) (φ : Val → State → Prop) + (Hade : AdequateNoFork .NotStuck e σ (fun v σ' => φ v σ')) : + ⊢ tpInvIni (TI := TI) -∗ + ACG.heap_inv [e] σ -∗ + wp ⊤ e (fun v => + iprop% ∃ σ' : State, ACG.heap_inv [ToVal.ofVal v] σ' ∗ ⌜φ v σ'⌝) := by + iintro Hini Hheap + ihave Hw := weakestpre_sem_completeness_nofork_strong (wp := wp) e σ φ Hade $$ Hini Hheap + iapply LWP.wp_wand $$ Hw + iintro %v ⟨%σ2, _, _, Hh, Hphi⟩ + iexists σ2 + iframe + +end Completeness + +end + +end Iris.ProgramLogic diff --git a/Iris/Iris/ProgramLogic/AbstractWeakestPre.lean b/Iris/Iris/ProgramLogic/AbstractWeakestPre.lean new file mode 100644 index 000000000..c26b3001f --- /dev/null +++ b/Iris/Iris/ProgramLogic/AbstractWeakestPre.lean @@ -0,0 +1,237 @@ +/- +Copyright (c) 2026 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.Algebra +public import Iris.Instances.Lib.FUpd +public import Iris.Instances.Lib.Invariants +public import Iris.BI +public import Iris.BI.WeakestPre +public import Iris.ProofMode +public import Iris.ProgramLogic.Language +public import Iris.ProgramLogic.EctxLanguage +public import Iris.Std.CoPset +public import Iris.ProgramLogic.WeakestPre + +namespace Iris + +open ProgramLogic Language Language.Notation Std + +@[expose] public section + +abbrev AbstractWP (Expr Val : Type _) (GF : BundledGFunctors) := + CoPset → Expr → (Val → IProp GF) → IProp GF + +section AbstractWP + +variable {Expr State Obs Val : Type _} [Λ : Language Expr State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] + +class InvOpenAbstractWP (wp : AbstractWP Expr Val GF) where + inv_open_maybe (e : Expr) (E₁ E₂) Φ (Hsub : E₂ ⊆ E₁) : + (|={E₁, E₂}=> + (∃ K e', ⌜Context K⌝ ∗ ⌜e = K e'⌝ ∗ ⌜Atomic .WeaklyAtomic e'⌝ + ∗ wp E₂ e' (fun v' => iprop% |={E₂, E₁}=> wp E₁ (K v') Φ)) ∨ + (|={E₂, E₁}=> wp E₁ e Φ)) + ⊢ wp E₁ e Φ + +class LawfulAbstractWP (wp : AbstractWP Expr Val GF) where + fupd_wp : (|={E}=> wp E e Φ) ⊢ wp E e Φ + wp_fupd {Φ : Val → IProp GF} : (wp E e (iprop% |={E}=> Φ ·)) ⊢ wp E e Φ + wp_value {v : Val} : wp E v Φ ⊣⊢ |={E}=> Φ v + wp_wand : wp E e Φ ⊢ (∀ v, Φ v -∗ Ψ v) -∗ wp E e Ψ + wp_atomic {e : Expr} (Hatom : Atomic .WeaklyAtomic e) : + (|={E₁, E₂}=> wp E₂ e (iprop% |={E₂, E₁}=> Φ ·)) ⊢ wp E₁ e Φ + +class BindAbstractWP (wp : AbstractWP Expr Val GF) extends LawfulAbstractWP wp where + wp_bind [Context K] : wp E e (fun (v : Val) => iprop% wp E (K v) Φ) ⊣⊢ wp E (K e) Φ + +end AbstractWP + +noncomputable section EctxLanguage + +open Classical + +variable {Expr State Obs Val Ectx : Type _} [EctxLanguage Expr Ectx State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {wp : AbstractWP Expr Val GF} [IWP : BindAbstractWP wp] + +theorem inv_open_maybe_ectxlang {e : Expr} {E₁ E₂ : CoPset} {Φ : Val → IProp GF} + (Hsub : E₂ ⊆ E₁) (Hred : ∃ σ, PrimStep.Reducible (e, σ)) : + (|={E₁, E₂}=> + (∃ (K : Ectx) (e' : Expr), + ⌜e = fill K e'⌝ ∗ ⌜Atomic .WeaklyAtomic e'⌝ ∗ ⌜∃ σ, BaseStep.Reducible (e', σ)⌝ + ∗ wp E₂ e' (fun v => iprop% |={E₂, E₁}=> wp E₁ (fill K v) Φ)) ∨ + (|={E₂, E₁}=> wp E₁ e Φ)) + ⊢ wp E₁ e Φ := by + iintro H + obtain ⟨σ, ⟨obs, e', σ', eₜ, @⟨e₁', e₂', K, Hbase⟩⟩⟩ := Hred + iapply (IWP.wp_bind (K := fill K)).mp + by_cases Atomic .WeaklyAtomic e₁' + next Hatomic => + iapply IWP.toLawfulAbstractWP.wp_atomic Hatomic (E₂ := E₂) + imod H with (⟨%K₁, %e', %Hf, %Hat, %Hred, Hwp⟩| H') + · imodintro + obtain ⟨σ'', Hred⟩ := Hred + have Hred' : BaseStep.Reducible (e₁', σ) := ⟨_, _, _, _, Hbase⟩ + obtain ⟨rfl, rfl⟩ := EctxLanguage.base_redex_unique _ _ _ _ σ _ Hf Hred' Hred + simp only [← EvContext.fill_comp, EvContext.fill_empty] + iapply IWP.toLawfulAbstractWP.wp_wand $$ Hwp + iintro %v >Hwp2 + itrivial + · imodintro + iapply IWP.toLawfulAbstractWP.wp_atomic Hatomic (E₂ := E₁) + imod H' + imodintro + ihave H' := (IWP.wp_bind (K := fill K)).mpr $$ H' + iapply IWP.wp_wand $$ H' [] + iintro %v Hwp + iapply fupd_mask_intro_subseteq Hsub $$ [$] + next Hnonatomic => + iapply IWP.toLawfulAbstractWP.fupd_wp + imod H with (⟨%K₁, %e', %Hf, %Hat, %Hred, Hwp⟩| H') + · obtain ⟨σ'', Hred⟩ := Hred + have Hred' : BaseStep.Reducible (e₁', σ) := ⟨_, _, _, _, Hbase⟩ + obtain ⟨_, rfl⟩ := EctxLanguage.base_redex_unique _ _ _ _ σ _ Hf Hred' Hred + exact Hnonatomic Hat |>.elim + · imod H' + ihave H' := (IWP.wp_bind (K := fill K)).mpr $$ H' + itrivial + +theorem inv_open_maybe_ectxlang_inv (e : Expr) (E : CoPset) (N : Namespace) + (P : IProp GF) (Φ : Val → IProp GF) + (Hsub : ↑N ⊆ E) (Hred : ∃ σ, PrimStep.Reducible (e, σ)) : + (inv N P ∗ + ((▷ P) ={E \ ↑N}=∗ + (∃ (K : Ectx) (e' : Expr), + ⌜e = fill K e'⌝ ∗ ⌜Atomic .WeaklyAtomic e'⌝ ∗ ⌜∃ σ, BaseStep.Reducible (e', σ)⌝ + ∗ wp (E \ ↑N) e' (fun v => iprop% P ∗ wp E (fill K v) Φ)) ∨ + (P ∗ wp E e Φ))) + ⊢ wp E e Φ := by + iintro ⟨#Hinv, H⟩ + iapply inv_open_maybe_ectxlang (E₂ := E \ nclose N) LawfulSet.diff_subset_left Hred + imod inv_acc _ _ _ Hsub $$ Hinv with ⟨HP, Hclose⟩ + imod H $$ HP with (⟨%K, %e', %He, %Hat, %Hred, H⟩|⟨HP, H⟩) + · imodintro + ileft + iexists K + iexists e' + iframe %He %Hat %Hred + iapply IWP.wp_wand $$ H + iintro %v ⟨HP, Hwp⟩ + imod Hclose $$ HP with - + itrivial + · iright + imod Hclose $$ HP with - + iapply fupd_mask_intro_subseteq LawfulSet.diff_subset_left $$ [$] + +end EctxLanguage + +/-! ### Instances of the abstract classes for iris-lean's real `Wp`. -/ + +section IrisWP + +variable {Expr State Obs Val : Type _} [Language Expr State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] + +/-- iris-lean's standard `WP` satisfies the abstract 5-law class. -/ +instance WP_lawful_abstract : + LawfulAbstractWP (Expr := Expr) (Val := Val) + (Wp.wp (PROP := IProp GF) Stuckness.NotStuck) where + fupd_wp := fupd_wp + wp_fupd := wp_fupd _ _ _ _ + wp_value := wp_value_fupd' + wp_wand := wp_wand + wp_atomic _ := wp_atomic + +/-- iris-lean's standard `WP` also satisfies the bind class for ectx +languages. -/ +instance WP_bind_abstract : + BindAbstractWP (Expr := Expr) (Val := Val) + (Wp.wp (PROP := IProp GF) Stuckness.NotStuck) where + wp_bind := ⟨wp_bind _, wp_bind_inv _⟩ + +theorem wp_inv_open_maybe_of_not_val {e : Expr} {E₁ E₂ : CoPset} {Φ : Val → IProp GF} + (Hnv : ToVal.toVal e = none) : + (|={E₁, E₂}=> + (∃ K e', ⌜Context K⌝ ∗ ⌜e = K e'⌝ ∗ ⌜Atomic .WeaklyAtomic e'⌝ ∗ + Wp.wp (Val := Val) Stuckness.NotStuck E₂ e' + (fun v' => iprop% |={E₂, E₁}=> Wp.wp (Val := Val) Stuckness.NotStuck E₁ (K v') Φ)) ∨ + (|={E₂, E₁}=> Wp.wp (Val := Val) Stuckness.NotStuck E₁ e Φ)) + ⊢ Wp.wp (Val := Val) Stuckness.NotStuck E₁ e Φ := by + iintro H + rw [IProp.ext wp_unfold, wp.pre, Hnv] + simp only + imod H with (⟨%K, %e', %Hctx, %Haux, %hato, Hwp⟩| >$) + subst Haux + -- FIXME: Why does this exit the proofmode? + rw [IProp.ext wp_unfold, wp.pre]; iintro Hwp + rcases He' : toVal e' with (_|v'); rotate_left + · imod Hwp; imod Hwp + rw [IProp.ext wp_unfold, wp.pre] + simp [coe_of_toVal_eq_some He', Hnv] + · dsimp only + iintro %σ %n %κ %κs %n₂ Hσ + imod Hwp $$ Hσ with ⟨%Hred, Hc⟩ + imodintro + have aux := Context.reducible_fill K Hred + iframe %aux; clear aux + iintro %e₂ %σ₂ %efs %H Hlc + obtain ⟨e₂, rfl, Hprim⟩ := Context.primStep_fill_inv (toVal_none_of_reducible Hred) H + ispecialize Hc $$ %e₂ %σ₂ %efs %Hprim Hlc + iapply step_fupdN_mono $$ Hc + iintro Hc + imod Hc with ⟨Hst, Hwp, $⟩ + replace Hprim : PrimStep.Irreducible (e₂, σ₂) := hato.atomic Hprim + -- FIXME: Why does this exit the proofmode? + rw [IProp.ext wp_unfold, wp.pre] + iintro ⟨Hst, Hwp⟩ + rcases He₂' : toVal e₂ with (_|v₂) <;> dsimp only + · imod Hwp $$ %_ %_ %κs %.nil [Hst] with ⟨%Hredu, H⟩ + · rw [List.append_nil κs]; iframe + grind + · imod Hwp with >Hwp + rw [coe_of_toVal_eq_some He₂'] + iframe + +theorem wp_inv_open_maybe (e : Expr) (E₁ E₂ : CoPset) (Φ : Val → IProp GF) : + (|={E₁, E₂}=> + (∃ K e', ⌜Context K⌝ ∗ ⌜e = K e'⌝ ∗ ⌜Atomic .WeaklyAtomic e'⌝ ∗ + Wp.wp (PROP := IProp GF) (Val := Val) Stuckness.NotStuck E₂ e' + (fun v' => iprop% |={E₂, E₁}=> Wp.wp (Val := Val) Stuckness.NotStuck E₁ (K v') Φ)) ∨ + (|={E₂, E₁}=> Wp.wp (Val := Val) Stuckness.NotStuck E₁ e Φ)) + ⊢ Wp.wp (Val := Val) Stuckness.NotStuck E₁ e Φ := by + iintro H + rcases Hv : toVal e with (_|v); + iapply wp_inv_open_maybe_of_not_val Hv $$ [$] + rw [← coe_of_toVal_eq_some Hv] + iapply wp_atomic (E2 := E₂) + imod H with (⟨%K, %e', %Hctx, %He, %Hato, H⟩| H); + · rcases Hv' : toVal e' with (_|v') + · exfalso + have h1 := Hctx.toVal_eq_none_fill Hv' + rw [← He] at h1 + simp at h1 + · rw [← coe_of_toVal_eq_some Hv'] + have hKv : K (↑v' : Expr) = ↑v := by rw [coe_of_toVal_eq_some Hv']; exact He.symm + imodintro + iapply wp_value_fupd (v := v) ⟨rfl⟩ + imodintro + imod (wp_value_fupd (v := v') ⟨rfl⟩).mp $$ H with H + imod H + ihave H := (wp_value_fupd (v := v) ⟨hKv.symm⟩).mp $$ H + iframe + · imodintro + iapply wp_value_fupd (v := v) ⟨rfl⟩ + imodintro + imod H + ihave _ := (wp_value_fupd (v := v) ⟨rfl⟩).mp $$ H + iframe + +instance WP_inv_open_abstract : + InvOpenAbstractWP (Expr := Expr) (Val := Val) (Wp.wp (PROP := IProp GF) Stuckness.NotStuck) where + inv_open_maybe e E₁ E₂ Φ _ := wp_inv_open_maybe e E₁ E₂ Φ + +end IrisWP diff --git a/Iris/Iris/ProgramLogic/Adequacy.lean b/Iris/Iris/ProgramLogic/Adequacy.lean index b216ce90d..75078ccf5 100644 --- a/Iris/Iris/ProgramLogic/Adequacy.lean +++ b/Iris/Iris/ProgramLogic/Adequacy.lean @@ -234,8 +234,7 @@ theorem wp_strong_adequacy_gen [InvGpreS GF] (s : Stuckness) (es : List Expr) ( abbrev wp_strong_adequacy := @wp_strong_adequacy_gen .hasLC @[rocq_alias adequate] -structure adequate (s : Stuckness) (e1 : Expr) (σ1 : State) - (φ : Val → State → Prop) : Prop where +structure adequate (s : Stuckness) (e1 : Expr) (σ1 : State) (φ : Val → State → Prop) : Prop where adequate_result : ∀ (t2 : List Expr) (σ2 : State) (v2 : Val), ([e1], σ1) -·->ₜₚ* (ToVal.ofVal v2 :: t2, σ2) → φ v2 σ2 @@ -243,6 +242,11 @@ structure adequate (s : Stuckness) (e1 : Expr) (σ1 : State) ∀ (t2 : List Expr) (σ2 : State) (e2 : Expr), s = .NotStuck → ([e1], σ1) -·->ₜₚ* (t2, σ2) → e2 ∈ t2 → NotStuck (e2, σ2) +structure AdequateNoFork (s : Stuckness) (e₁ : Expr) (σ₁ : State) (φ : Val → State → Prop) : Prop where + no_fork {t₂ σ₂} : ([e₁], σ₁) -·->ₜₚ* (t₂, σ₂) → t₂.length = 1 + result {t₂ σ₂ v₂} : ([e₁], σ₁) -·->ₜₚ* (ToVal.ofVal v₂ :: t₂, σ₂) → φ v₂ σ₂ + not_stuck {t₂ σ₂ e₂} : s = .NotStuck → ([e₁], σ₁) -·->ₜₚ* (t₂, σ₂) → e₂ ∈ t₂ → NotStuck ⟨e₂, σ₂⟩ + @[rocq_alias adequate_alt] theorem adequate_alt (s : Stuckness) (e1 : Expr) (σ1 : State) (φ : Val → State → Prop) : @@ -274,6 +278,25 @@ theorem adequate_tp_safe (e1 : Expr) (t2 : List Expr) (σ1 σ2 : State) obtain ⟨t2', t2'', rfl⟩ := List.append_of_mem hel exact .inr ⟨t2' ++ e3 :: t2'' ++ efs, σ3, obs, Language.Step.of_primStep hstep⟩ +theorem adequateNoFork_step {e₁ e₂ : Expr} {σ₁ σ₂ s Q} + (Hstep : ([e₁], σ₁) -·->ₜₚ* ([e₂], σ₂)) (H : AdequateNoFork s e₁ σ₁ Q) : + AdequateNoFork s e₂ σ₂ Q := + ⟨(H.no_fork <| Hstep.trans ·), (H.result <| Hstep.trans ·), (H.not_stuck · <| Hstep.trans ·)⟩ + +theorem adequateNoFork_primStep {e₁ e₂ : Expr} {κ σ₁ σ₂ s Q} + (Hstep : (e₁, σ₁) -<κ>-> (e₂, σ₂, [])) + (H : AdequateNoFork s e₁ σ₁ Q) : AdequateNoFork s e₂ σ₂ Q := + adequateNoFork_step (.tail .refl ⟨κ, .of_primStep Hstep (t₁ := []) (t₂ := [])⟩) H + +theorem adequateNoFork_efs_nil {e₁ : Expr} {σ₁ s φ} (H : AdequateNoFork s e₁ σ₁ φ) + {t₂ σ₂ e₂} (Hsteps : ([e₁], σ₁) -·->ₜₚ* (t₂, σ₂)) (Hmem : e₂ ∈ t₂) + {κ e' σ' efs} (Hstep : (e₂, σ₂) -<κ>-> (e', σ', efs)) : efs = [] := by + obtain ⟨t₂a, t₂b, rfl⟩ := List.append_of_mem Hmem + have Hlen := H.no_fork (Hsteps.tail ⟨κ, .atomic Hstep t₂a t₂b⟩) + refine List.length_eq_zero_iff.mp ?_ + simp [List.length_append] at Hlen + omega + omit iG in @[rocq_alias wp_adequacy_gen] theorem wp_adequacy_gen [InvGpreS GF] (s : Stuckness) (e : Expr) (σ : State) (φ : Val → Prop) diff --git a/Iris/Iris/ProgramLogic/EctxLanguage.lean b/Iris/Iris/ProgramLogic/EctxLanguage.lean index 4d5ac6b9b..9a53d4c3e 100644 --- a/Iris/Iris/ProgramLogic/EctxLanguage.lean +++ b/Iris/Iris/ProgramLogic/EctxLanguage.lean @@ -210,6 +210,8 @@ variable {e e' e₁ e₂ : Expr} {σ σ' σ₁ σ₂ : State} variable {K K' K₁ K₂ : Ectx} {obs obs' : List Obs} variable {eₜ eₜ : List Expr} +-- FIXME: Implicits + open EvContext in @[rocq_alias base_redex_unique] theorem base_redex_unique K K' (e e' : Expr) σ σ' (heq : fill K e = fill K' e') : diff --git a/Iris/Iris/ProgramLogic/EctxiLanguage.lean b/Iris/Iris/ProgramLogic/EctxiLanguage.lean index 970192711..74e23d39a 100644 --- a/Iris/Iris/ProgramLogic/EctxiLanguage.lean +++ b/Iris/Iris/ProgramLogic/EctxiLanguage.lean @@ -81,6 +81,15 @@ theorem fill_append (K₁ K₂ : Λ.Ectx) (e : Expr) : fill (K₁ ++ K₂) e = f theorem fill_val {K} {e : Expr} : (toVal (fill K e)).isSome = true → (toVal e).isSome = true := by induction K generalizing e <;> grind [fillItem_val] +theorem baseStep_fill_eq_val_absurd {K : Ectx} {e e' : Expr} {σ σ' : State} + {obs : List Obs} {efs : List Expr} {v : Val} + (hbase : (e, σ) -->ᵇ (e', σ', efs)) + (heq : (v : Expr) = fill K e) : False := by + have hfill_isval : (toVal (fill K e)).isSome := heq ▸ by simp + have h_e_val : (toVal e).isSome := fill_val hfill_isval + rw [val_stuck hbase] at h_e_val + simp at h_e_val + -- NOTE: Would it be worth having an `isVal` predicate for `Expr`, basically defined -- as `toVal e |>.isSome`, so that we could rephrase all instances of `(toVal e).isSome` -- as `isVal e` and `toVal e = none` as `¬ isVal e`. That way tactics like `grind` would diff --git a/Iris/Iris/ProgramLogic/Language.lean b/Iris/Iris/ProgramLogic/Language.lean index 84998b24e..896b146cd 100644 --- a/Iris/Iris/ProgramLogic/Language.lean +++ b/Iris/Iris/ProgramLogic/Language.lean @@ -161,6 +161,10 @@ scoped notation (name := ErasedStep) conf:40 " -·->ₜₚ " conf':41 => Languag scoped notation (name := erasedStepStar) conf:40 " -·->ₜₚ* " conf':41 => Relation.ReflTransGen Language.ErasedStep conf conf' +/-- A nonempty sequence of `Language.erasedStep`s -/ +scoped notation (name := erasedStepPlus) conf:40 " -·->ₜₚ+ " conf':41 => + Relation.TransGen Language.ErasedStep conf conf' + end Notation open Notation @@ -243,6 +247,11 @@ theorem stronglyAtomic_atomic {a} : | .StronglyAtomic => id | .WeaklyAtomic => fun ⟨h⟩ => ⟨by grind only [not_reducible_iff_irreducible, val_irreducible]⟩ +theorem prim_val_stuck (h : (↑ v, σ) --> (e', σ', eₜ)) : False := by + simpa using val_stuck h + +instance val_atomic {a : Atomicity} {v : Val} : Atomic a (Λ.ofVal v) := + ⟨fun h => by simpa using val_stuck h⟩ /-- The function `K` models an evaluation context for the language -/ @[rocq_alias LanguageCtx] diff --git a/Iris/Iris/ProgramLogic/ThreadPool.lean b/Iris/Iris/ProgramLogic/ThreadPool.lean new file mode 100644 index 000000000..4330c3630 --- /dev/null +++ b/Iris/Iris/ProgramLogic/ThreadPool.lean @@ -0,0 +1,282 @@ +/- +Copyright (c) 2026 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.ProgramLogic.Language +public import Iris.ProgramLogic.EctxLanguage +public import Iris.ProgramLogic.Adequacy +public import Iris.Instances.Lib.GhostMap +public import Iris.Std.FromMathlib +public import Batteries.Data.List.Lemmas + +namespace Iris.ProgramLogic + +open Iris.ProgramLogic.PrimStep +open Language Language.Notation Relation FromMathlib FromMathlib.Relation.TransGen + +@[expose] public section + +variable {Expr State Obs Val : Type _} [Λ : Language Expr State Obs Val] + +/-! ### Multi-step prim reduction on a single thread -/ + +/-- Transitive closure of `primStep` with accumulated observations and forks. -/ +inductive PrimSteps : Expr → State → List Obs → Expr → State → List Expr → Prop where + | once {e₁ σ₁ κ e₂ σ₂ efs} : + (e₁, σ₁) -<κ>-> (e₂, σ₂, efs) → PrimSteps e₁ σ₁ κ e₂ σ₂ efs + | next {e₁ σ₁ κ₁ e₂ σ₂ efs₁ κ₂ e₃ σ₃ efs₂} : + (e₁, σ₁) -<κ₁>-> (e₂, σ₂, efs₁) → + PrimSteps e₂ σ₂ κ₂ e₃ σ₃ efs₂ → + PrimSteps e₁ σ₁ (κ₁ ++ κ₂) e₃ σ₃ (efs₁ ++ efs₂) + +/-! ### Configuration safety -/ + +inductive Forking where + | doesFork + | doesNotFork + +/-- Every thread in the pool is not stuck at the current state. -/ +def cfgNotStuck (C : List Expr × State) : Prop := + ∀ {e}, e ∈ C.1 → NotStuck (e, C.2) + +/-- If we declared the configuration `DoesNotFork`, every primitive step +of every thread emits empty forks. -/ +def cfgForking (C : List Expr × State) (f : Forking) : Prop := + f = .doesNotFork → ∀ e ∈ C.1, ∀ {e' σ' κ efs}, (e, C.2) -<κ>-> (e', σ', efs) → efs = [] + +/-- The configuration is safe under the given forking discipline: +every reachable configuration is not stuck and respects the forking constraint. -/ +def cfgSafeForking (C : List Expr × State) (f : Forking) : Prop := + ∀ {C₂}, (C -·->ₜₚ* C₂) → cfgNotStuck C₂ ∧ cfgForking C₂ f + +/-- The configuration is safe: every reachable configuration is not stuck. -/ +def cfgSafe (C : List Expr × State) : Prop := + ∀ {C₂}, (C -·->ₜₚ* C₂) → cfgNotStuck C₂ + +theorem cfgSafe_of_cfgSafeForking {C : List Expr × State} {f : Forking} + (H : cfgSafeForking C f) : cfgSafe C := fun Hp _ => H Hp |>.1 + +theorem PrimSteps.fill {K : Expr → Expr} [Context K] {e₁ σ₁ κ e₂ σ₂ efs} + (Hs : PrimSteps e₁ σ₁ κ e₂ σ₂ efs) : PrimSteps (K e₁) σ₁ κ (K e₂) σ₂ efs := + match Hs with + | once hstep => .once <| Context.primStep_fill hstep + | next hstep hsteps => .next (Context.primStep_fill hstep) hsteps.fill + +theorem cfg_step {tp : List Expr} {σ : State} {n : Nat} {e : Expr} + {κ : List Obs} {e' : Expr} {σ' : State} {efs : List Expr} + (Hlu : tp[n]? = some e) (Hprim : (e, σ) -<κ>-> (e', σ', efs)) : + Step (tp, σ) κ (tp.set n e' ++ efs, σ') := by + obtain ⟨hlt, rfl⟩ := List.getElem?_eq_some_iff.mp Hlu + simpa only [List.getElem_cons_drop hlt, List.take_append_drop, + ← List.set_eq_take_cons_drop e' hlt] using + Step.of_primStep Hprim (t₁ := tp.take n) (t₂ := tp.drop (n+1)) + +theorem getElem?_set_append_self {tp : List Expr} {n : Nat} {a : Expr} {efs : List Expr} + (hlt : n < tp.length) : (tp.set n a ++ efs)[n]? = some a := by + rw [List.getElem?_append_left (by rwa [List.length_set]), List.getElem?_set_self hlt] + +theorem set_append_set_append {tp : List Expr} {n : Nat} {a b : Expr} + {efs₁ efs₂ : List Expr} (hlt : n < tp.length) : + (tp.set n a ++ efs₁).set n b ++ efs₂ = tp.set n b ++ (efs₁ ++ efs₂) := by + rw [List.set_append_left _ _ (by rwa [List.length_set]), List.set_set, List.append_assoc] + +theorem cfg_stepsTc {tp : List Expr} {σ : State} {n e κ e' σ' efs} + (Hlu : tp[n]? = some e) (Hprim : PrimSteps e σ κ e' σ' efs) : + Relation.TransGen ErasedStep (tp, σ) (tp.set n e' ++ efs, σ') := by + revert Hlu + induction Hprim generalizing tp with + | once hstep => exact fun Hlu => .single ⟨_, cfg_step Hlu hstep⟩ + | @next _ _ _ e₂ _ efs₁ _ _ _ _ hstep _ ih => + intro Hlu + have hlt : n < tp.length := (List.getElem?_eq_some_iff.mp Hlu).1 + have rest := ih (tp := tp.set n e₂ ++ efs₁) (getElem?_set_append_self hlt) + rw [set_append_set_append hlt] at rest + exact head ⟨_, cfg_step Hlu hstep⟩ rest + +theorem cfg_steps {tp : List Expr} {σ : State} {n e κ e' σ' efs} (Hlu : tp[n]? = some e) + (Hprim : PrimSteps e σ κ e' σ' efs) : (tp, σ) -·->ₜₚ* (tp.set n e' ++ efs, σ') := + to_reflTransGen (cfg_stepsTc Hlu Hprim) + +theorem cfg_safeStep {tp : List Expr} {σ : State} {f n e κ e' σ' efs} + (Hsafe : cfgSafeForking (tp, σ) f) (Hlu : tp[n]? = some e) + (Hprim : (e, σ) -<κ>-> (e', σ', efs)) : + cfgSafeForking (tp.set n e' ++ efs, σ') f ∧ (f = .doesNotFork → efs = []) := by + refine ⟨fun {C₂ Hrtc} => ?_, fun hf => ?_⟩ + · exact Hsafe (.head ⟨κ, cfg_step Hlu Hprim⟩ Hrtc) + · exact Hsafe .refl |>.2 hf e (List.mem_of_getElem? Hlu) Hprim + +theorem cfg_safeSteps {tp : List Expr} {σ : State} {f n e κ e' σ' efs} + (Hsafe : cfgSafeForking (tp, σ) f) (Hlu : tp[n]? = some e) + (Hprim : PrimSteps e σ κ e' σ' efs) : + cfgSafeForking (tp.set n e' ++ efs, σ') f ∧ + (f = .doesNotFork → efs = []) := by + revert Hsafe Hlu + induction Hprim generalizing tp with + | once hstep => exact fun Hsafe Hlu => cfg_safeStep Hsafe Hlu hstep + | @next _ _ _ e₂ _ efs₁ _ _ _ _ hstep _ ih => + intro Hsafe Hlu + have hlt := (List.getElem?_eq_some_iff.mp Hlu).1 + obtain ⟨Hsafe2, Hnf⟩ := cfg_safeStep Hsafe Hlu hstep + obtain ⟨Hsafe3, Hnf2⟩ := + ih (tp := tp.set n e₂ ++ efs₁) Hsafe2 (getElem?_set_append_self hlt) + rw [set_append_set_append hlt] at Hsafe3 + exact ⟨Hsafe3, fun hf => by simp [Hnf hf, Hnf2 hf]⟩ + +theorem nSteps_trans {n m : Nat} {ρ₁ ρ₂ ρ₃ : List Expr × State} {κa κb : List Obs} + (H1 : ρ₁ -<κa>->ₜₚ^[n] ρ₂) (H2 : ρ₂ -<κb>->ₜₚ^[m] ρ₃) : + ρ₁ -<(κa ++ κb)>->ₜₚ^[(n + m)] ρ₃ := by + induction H1 with + | refl ρ => simpa using H2 + | cons hstep _ ih => + rw [Nat.add_right_comm, List.append_assoc] + exact NSteps.cons hstep (ih H2) + +theorem nSteps_one {ρ₁ ρ₂ : List Expr × State} {κ : List Obs} + (H : ρ₁ -<κ>->ₜₚ ρ₂) : ρ₁ -<κ>->ₜₚ^[1] ρ₂ := by + simpa using NSteps.cons H (.refl _) + +theorem nSteps_r {n} {ρ₁ ρ₂ ρ₃ : List Expr × State} {κ κs : List Obs} + (H1 : ρ₁ -<κs>->ₜₚ^[n] ρ₂) (H2 : ρ₂ -<κ>->ₜₚ ρ₃) : ρ₁ -<(κs ++ κ)>->ₜₚ^[(n + 1)] ρ₃ := + nSteps_trans H1 (nSteps_one H2) + +theorem primSteps_atomic {e : Expr} {σ κ e₂ σ' efs} + (Hatom : Atomic .StronglyAtomic e) (Hsteps : PrimSteps e σ κ e₂ σ' efs) : + ((e, σ) -<κ>-> (e₂, σ', efs)) ∧ (ToVal.toVal e₂).isSome := by + cases Hsteps with + | once hstep => exact ⟨hstep, Hatom.atomic hstep⟩ + | next hstep hsteps2 => + have hv := Hatom.atomic hstep + cases hsteps2 with + | once h3 => simp [Language.val_stuck h3] at hv + | next h3 _ => simp [Language.val_stuck h3] at hv + +end + +/-! ### Thread-pool ghost-state invariant -/ + +section ghost +open Iris CMRA Std + +variable {GF : BundledGFunctors} +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable {Expr : Type _} + +/-- The ghost state needed to track a thread-pool invariant -/ +public class TpinvGS (GF : BundledGFunctors) (Expr : Type _) (H : outParam <| Type _ → Type _) + [LawfulFiniteMap H Nat] extends GhostMapG GF Nat Expr H where + tp_name : GName + +variable [TI : TpinvGS GF Expr H] + +/-- Thread `n` in the pool is the expression `e`. -/ +public def isThread (n : Nat) (dq : DFrac) (e : Expr) : IProp GF := + TI.tp_name ↪◯MAP[n]{dq} e + +notation k " ↪thread{" dq "} " v => isThread k dq v +notation k " ↪thread " v => isThread k (DFrac.own 1) v + +/-- The initial thread-pool authority (empty pool). -/ +public def tpInvIni : IProp GF := + TI.tp_name ↪●MAP (∅ : H Expr) + +/-- The thread-pool invariant: the auth-side `ghost_map` agrees pointwise with +the operational thread list `tp`. -/ +public def tpInv (tp : List Expr) : IProp GF := iprop% + ∃ m : H Expr, ⌜∀ n, PartialMap.get? m n = tp[n]?⌝ ∗ TI.tp_name ↪●MAP m + +/-- `tpInv` is timeless: the ghost-map authority is over a discrete camera, and +the rest is pure/existential. Needed to strip the later off invariant contents +after opening (e.g. via `CancelableInvariant.acc`). -/ +public instance tpInv_timeless (tp : List Expr) : Iris.BI.Timeless (tpInv (TI := TI) tp) := by + unfold tpInv; infer_instance + +public theorem tpInv_lookup (tp : List Expr) (n : Nat) (e₁ : Expr) (dq : DFrac) : + tpInv tp ⊢@{IProp GF} (n ↪thread{dq} e₁) -∗ ⌜tp[n]? = some e₁⌝ := by + unfold tpInv isThread + iintro ⟨%m, %He, Hauth⟩ Hfrag + ihave %Hlookup := ghost_map_lookup $$ Hauth Hfrag + ipureintro + rw [← Hlookup, He _] + +public theorem tpInv_update (tp : List Expr) (n : Nat) (e₁ e₂ : Expr) : + tpInv tp ⊢@{IProp GF} + (n ↪thread e₁) ==∗ tpInv (tp.set n e₂) ∗ (n ↪thread e₂) := by + iintro Hinv Hfrag + ihave %Hlookup := tpInv_lookup $$ Hinv Hfrag + unfold tpInv isThread + ihave ⟨%m, %He, Hauth⟩ := Hinv + imod ghost_map_update (w := e₂) $$ Hauth Hfrag with ⟨Hauth, Hfrag⟩ + imodintro + iframe + iexists (Std.insert m n e₂) + iframe; ipureintro; intro n + grind [LawfulPartialMap.get?_insert] + +public theorem tpInv_new_threads (efs tp : List Expr) : + ⊢@{IProp GF} tpInv tp ==∗ (tpInv (tp ++ efs) ∗ ([∗list] n ↦ e' ∈ efs, (tp.length + n) ↪thread e')) := by + unfold tpInv isThread + iintro ⟨%m, %He, Hauth⟩ + have Hdisj : PartialMap.disjoint (FiniteMap.map_seq (M := H) tp.length efs) m := by + rw [PartialMap.disjoint_iff] + intro k + rcases Nat.lt_or_ge k tp.length with h | h + · left; rw [LawfulFiniteMap.get?_map_seq, if_neg (by omega)] + · right; rw [He k, List.getElem?_eq_none h] + imod ghost_map_insert_big (FiniteMap.map_seq tp.length efs) Hdisj $$ Hauth + with ⟨Hauth, Hlist⟩ + imodintro + isplitl [Hauth] + · iexists (FiniteMap.map_seq tp.length efs ∪ m) + iframe + ipureintro + intro n + show get? (PartialMap.union (FiniteMap.map_seq tp.length efs) m) n = (tp ++ efs)[n]? + rw [LawfulPartialMap.get?_union, LawfulFiniteMap.get?_map_seq, He n] + rcases Nat.lt_or_ge n tp.length with h | h + · rw [if_neg (by omega), List.getElem?_append_left h]; rfl + · rw [if_pos h, List.getElem?_append_right h, List.getElem?_eq_none h] + cases efs[n - tp.length]? <;> rfl + · iapply (Iris.BI.BigSepM.bigSepM_map_seq).mp + iexact Hlist + +public theorem tpInv_set (C : List Expr) : + ⊢@{IProp GF} tpInvIni (Expr := Expr) ==∗ tpInv C ∗ ([∗list] n ↦ e ∈ C, n ↪thread e) := by + iintro Hauth + imod tpInv_new_threads C [] $$ [Hauth] with ⟨Hi, Hlist⟩ + · unfold tpInvIni tpInv + iexists ∅ + iframe + ipureintro + exact get?_empty + imodintro + simp + +end ghost + +/-! ### Allocation + +Allocates the empty thread-pool authority and exposes a `TpinvGS` instance +parameterized by the freshly-chosen ghost name. -/ + +section alloc +open Iris CMRA Std + +variable {GF : BundledGFunctors} +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable {Expr : Type _} [GhostMapG GF Nat Expr H] + +open Classical in +public theorem tpInv_alloc : + ⊢@{IProp GF} |==> ∃ γ, + tpInvIni (Expr := Expr) (TI := { toGhostMapG := inferInstance, tp_name := γ }) := by + imod @ghost_map_alloc_empty _ Nat Expr H with ⟨%γ, H⟩ + imodintro + iexists γ + unfold tpInvIni + iexact H + +end alloc + +end Iris.ProgramLogic diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean index 30b004fc7..df405de9f 100644 --- a/Iris/Iris/ProgramLogic/WeakestPre.lean +++ b/Iris/Iris/ProgramLogic/WeakestPre.lean @@ -249,6 +249,8 @@ theorem fupd_wp_iff {s : Stuckness}{E}{e : Expr} {Φ : Val → IProp GF} : WP e @ s ; E {{ Φ }} ⊣⊢ (|={E}=> WP e @ s ; E {{ Φ }}) := ⟨fupd_mask_intro_discard LawfulSet.subset_refl, fupd_wp⟩ +-- FIXME: Implicits + @[rocq_alias wp_fupd] theorem wp_fupd (s : Stuckness) E (e : Expr) (Φ : Val → IProp GF) : WP e @ s ; E {{v, |={E}=> Φ v }} ⊢ WP e @ s ; E {{ Φ }} := by @@ -388,6 +390,8 @@ theorem wp_step_fupdN_strong {s : Stuckness} {E1 E2 : CoPset} {e : Expr} {P : IP imod interp $$ Hσ₁ with %h grind only +-- FIXME: Combine wp_bind and wp_bind_iff into a single bi-entailment + @[rocq_alias wp_bind] theorem wp_bind (K : Expr → Expr) [κ : Language.Context K] {s : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} : diff --git a/Iris/Iris/Std/FromMathlib.lean b/Iris/Iris/Std/FromMathlib.lean index 8ba999c0c..13c65ef28 100644 --- a/Iris/Iris/Std/FromMathlib.lean +++ b/Iris/Iris/Std/FromMathlib.lean @@ -81,8 +81,55 @@ theorem head_induction_on {motive : ∀ a : α, ReflTransGen r a b → Prop} {a theorem cases_head (h : ReflTransGen r a b) : a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b := by induction h using ReflTransGen.head_induction_on <;> grind +theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by + induction hbc with + | refl => exact hab + | tail _ hcd ih => exact ih.tail hcd + +/-- NB. Copied from Mathlib -/ +theorem single (hab : r a b) : ReflTransGen r a b := + refl.tail hab + end Relation.ReflTransGen +/-! ### Lemmas about `Relation.TransGen` (defined in Lean core, `Init.Core`). + +The transitive closure itself is in `_root_.Relation.TransGen`; we add a few +helper lemmas here under `FromMathlib.Relation.TransGen` (mirroring Mathlib's +names without colliding when Mathlib is also imported), bridging to our local +`FromMathlib.Relation.ReflTransGen`. -/ + +namespace Relation.TransGen + +/-- NB. Copied from Mathlib -/ +theorem to_reflTransGen {α} {r : α → α → Prop} {a b} + (h : _root_.Relation.TransGen r a b) : Relation.ReflTransGen r a b := by + induction h with + | single h => exact Relation.ReflTransGen.single h + | tail _ bc ab => exact Relation.ReflTransGen.tail ab bc + +/-- NB. Copied from Mathlib -/ +theorem trans_left {α} {r : α → α → Prop} {a b c} + (hab : _root_.Relation.TransGen r a b) (hbc : Relation.ReflTransGen r b c) : + _root_.Relation.TransGen r a c := by + induction hbc with + | refl => exact hab + | tail _ hcd hac => exact hac.tail hcd + +/-- NB. Copied from Mathlib -/ +theorem head' {α} {r : α → α → Prop} {a b c} + (hab : r a b) (hbc : Relation.ReflTransGen r b c) : + _root_.Relation.TransGen r a c := + trans_left (.single hab) hbc + +/-- NB. Copied from Mathlib -/ +theorem head {α} {r : α → α → Prop} {a b c} + (hab : r a b) (hbc : _root_.Relation.TransGen r b c) : + _root_.Relation.TransGen r a c := + head' hab (to_reflTransGen hbc) + +end Relation.TransGen + namespace List @[grind .] diff --git a/Iris/Iris/Std/PartialMap.lean b/Iris/Iris/Std/PartialMap.lean index 0dc2477f5..3d83baae0 100644 --- a/Iris/Iris/Std/PartialMap.lean +++ b/Iris/Iris/Std/PartialMap.lean @@ -1183,6 +1183,38 @@ theorem toList_dom_set_perm [LawfulFiniteSet S K] (m : M V) : exact ⟨(x, v), toList_get.mpr hv, rfl⟩ · grind [toList_get] +/-! ### `map_seq` -/ + +variable {M' : Type _ → Type _} [LawfulFiniteMap M' Nat] + +@[simp] theorem map_seq_nil {V : Type _} {start : Nat} : + map_seq (M := M') start ([] : List V) = ∅ := by + rw [map_seq, List.mapIdx_nil]; rfl + +theorem map_seq_cons {V : Type _} {start : Nat} {v : V} {l : List V} : + map_seq (M := M') start (v :: l) = insert (map_seq (start + 1) l) start v := by + have hfun : (fun i (x : V) => (start + (i + 1), x)) = (fun i x => (start + 1 + i, x)) := by + funext i x; congr 1; omega + show ofList ((v :: l).mapIdx fun i x => (start + i, x)) = _ + rw [List.mapIdx_cons] + simp only [Nat.add_zero, hfun] + exact ofList_cons + +theorem get?_map_seq {V : Type _} {start k : Nat} {l : List V} : + get? (map_seq (M := M') start l) k = if start ≤ k then l[k - start]? else none := by + induction l generalizing start with + | nil => rw [map_seq_nil]; simp only [List.getElem?_nil, ite_self]; exact get?_empty _ + | cons v l ih => + rw [map_seq_cons] + by_cases hk : k = start + · subst hk; rw [get?_insert_eq rfl, if_pos (Nat.le_refl _)]; simp + · rw [get?_insert_ne (by omega : start ≠ k), ih] + rcases Nat.lt_or_ge k start with h | h + · rw [if_neg (by omega), if_neg (by omega)] + · rw [if_pos h, if_pos (by omega : start + 1 ≤ k), List.getElem?_cons, + if_neg (by omega : k - start ≠ 0)] + congr 1 <;> omega + end LawfulFiniteMap end Iris.Std