diff --git a/Iris/Iris/HeapLang/Completeness.lean b/Iris/Iris/HeapLang/Completeness.lean new file mode 100644 index 000000000..254ac40c4 --- /dev/null +++ b/Iris/Iris/HeapLang/Completeness.lean @@ -0,0 +1,879 @@ +/- +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.HeapLang.PrimitiveLaws +public import Iris.BI.BigOp.BigSepSet +public import Iris.ProgramLogic.ThreadPool +public import Iris.ProgramLogic.AbstractWeakestPre +public import Iris.ProgramLogic.AbstractLangCompleteness +public import Iris.ProgramLogic.AbstractEctxLangCompleteness +public import Iris.Instances.Lib.CInvariants +public import Iris.Instances.Lib.GhostMap +public import Iris.ProofMode + +/-! # HeapLang completeness + +Ports `case_studies/heaplang/completeness_generic.v` and +`completeness_classical.v`. `heap_inv` carries Rocq's two conjuncts: per-cell +`heapCellPts ∗ meta_token` (mirroring `from_option (λ v, ℓ ↦ v) ⌜True⌝` — a live +cell owns its points-to, a freed `none` cell owns nothing), and +`∃ pvs, proph p pvs` for every prophecy id in `σ.usedProphId`. `stateInterp` +includes `prophMapInterp κs σ.usedProphId` alongside `genHeapInterp σ.heap`. + +Status of `wp_base_completeness` (the base-step case analysis): +* pure branches (`rec`/`pair`/`injL`/`injR`/`beta`/`unop`/`binop`/`if`/`fst`/ + `snd`/`case`) — via `wp_base_pure` + the `PureExec` instances/lemmas; +* atomic heap branches (`load`/`store`/`free`/`xchg`/`faa`/`cmpXchg`) — via + `wp_base_atomic`(`_nochange`) + the per-op determinism lemmas; +* `fork` — via the non-atomic disjunct and `wp_fork_fupd`; +* `alloc` — via `genHeap_alloc_big`, with location freshness from `meta_token_ne`; +* `newProph` — atomic lift, fresh `p` picked in `σ₁.usedProphId`, then + `ProphMap.new_proph` allocates a proph token; freshness in `σ` follows from + `proph_exclusive` against the proph conjunct of `heap_inv σ`; +* `resolve` — `sorry` body, but `wp_base_completeness` is now a well-founded + recursion on `e₁` (declared via `termination_by e₁`), so the resolveS branch + has the inductive hypothesis `IH : heap_inv σ ⊢ |={E}=> baseCompletenessGoal + e σ E` in scope for the inner expression `e`. What remains is the body that + combines `IH` with the outer Resolve wrapping (mirror of Rocq lines 127–159): + extract `proph p` from `heap_inv σ`'s proph conjunct via `bigSepS_elem_of_acc` + + `hp : p ∈ σ.usedProphId`, then either inline a `wp_resolve_strong`-style + argument or split on `IH`'s atomic/non-atomic disjunction and use + `ProphMap.resolve_proph` to consume the front observation `(p,(v,w))` of + `κs`. All other supporting infrastructure (`prophMapInterp`, `proph p pvs`, + `ProphMap.resolve_proph`, the proph conjunct of `heap_inv`, the recursion) + is in place. +-/ + +@[expose] public section +namespace Iris.HeapLang + +open Iris ProgramLogic Iris.BI Language Language.Notation Std + +variable {hlc : HasLC} {GF : BundledGFunctors} [HeapLangGS hlc GF] + +/-- Ownership of a single heap cell's points-to. Mirrors Rocq's +`from_option (λ v, ℓ ↦ v) ⌜True⌝`: a live cell `some v` contributes `l ↦ some v`, +while a freed cell `none` contributes no ownership (`emp`). Note iris-lean's +`l ↦ ·` is the raw `gen_heap` points-to over `Option Val`, unlike Rocq heap_lang's +sealed `↦` which always wraps `Some`; hence the explicit `match` here. -/ +@[reducible] def heapCellPts (l : Loc) (vo : Option Val) : IProp GF := + match vo with + | some _ => iprop(l ↦ vo) + | none => iprop(emp) + +instance heapCellPts_timeless (l : Loc) (vo : Option Val) : + Timeless (heapCellPts (GF := GF) l vo) := by + cases vo <;> (unfold heapCellPts; infer_instance) + +/-- The raw points-to entails the cell invariant: for a live cell it is the same +resource, for a freed cell the points-to is dropped (affinely). -/ +theorem pointsTo_heapCellPts (l : Loc) (vo : Option Val) : + (l ↦ vo) ⊢ heapCellPts (GF := GF) l vo := by + cases vo with + | some v => exact .rfl + | none => exact BI.Affine.affine + +/-- The heap-lang configuration invariant: ownership of every live heap cell's +points-to together with the `meta_token` of every cell (live or freed), and a +`proph` token for every used prophecy id. +Mirrors `heap_inv` in `case_studies/heaplang/completeness_generic.v`. -/ +@[reducible] def heap_inv (σ : State) : IProp GF := iprop( + (bigSepM (M := HeapF) (K := Loc) + (fun (l : Loc) (vo : Option Val) => iprop(heapCellPts l vo ∗ metaToken l ⊤)) σ.heap) ∗ + ([∗set] p ∈ σ.usedProphId, ∃ pvs : List (Val × Val), proph p pvs)) + +instance heap_inv_timeless (σ : State) : Timeless (heap_inv (GF := GF) σ) := by + unfold heap_inv; infer_instance + +/-- Common shape of the completeness equation for a single base step, packaged so +the per-branch proofs only have to supply the (atomic / non-atomic) disjunct. -/ +abbrev baseCompletenessGoal (e₁ : Exp) (σ : State) (E : CoPset) : IProp GF := iprop( + ((⌜Atomic Atomicity.StronglyAtomic e₁⌝ ∗ + ∀ (Φ : Val → IProp GF), + (▷ ∀ κ v₂ σ' efs, ⌜PrimStep.primStep (e₁, σ) κ ((ToVal.ofVal v₂ : Exp), σ', efs)⌝ ==∗ + ((heap_inv σ' -∗ Φ v₂) ∗ + [∗list] _i ↦ etp ∈ efs, WP etp @ Stuckness.NotStuck; ⊤ {{ _v, True }})) -∗ + WP e₁ @ Stuckness.NotStuck; E {{ v, Φ v }}) ∨ + (heap_inv σ ∗ + ∀ (Φ : Val → IProp GF) (E₂ : CoPset), + (▷ ∀ e₂ efs, (∀ σ₁, heap_inv σ₁ ={E}=∗ + ∃ κ σ₁', ⌜PrimSteps e₁ σ₁ κ e₂ σ₁' efs⌝ ∗ heap_inv σ₁') ={E₂}=∗ + WP e₂ @ Stuckness.NotStuck; E₂ {{ v, Φ v }} ∗ + [∗list] _i ↦ etp ∈ efs, WP etp @ Stuckness.NotStuck; ⊤ {{ _v, True }}) -∗ + WP e₁ @ Stuckness.NotStuck; E₂ {{ v, Φ v }}))) + +/-- Pure-step branch of `wp_base_completeness`: a pure base step `e₁ → e₂` lands in +the non-atomic disjunct, stepping the WP with `PureExec` and witnessing the +trajectory with the (state-independent) base step. -/ +theorem wp_base_pure {e₁ e₂ : Exp} {φ : Prop} [hpe : Language.PureExec φ 1 e₁ e₂] (hφ : φ) + (σ : State) (E : CoPset) + (hbase : ∀ σ' : State, BaseStep e₁ σ' [] e₂ σ' []) : + heap_inv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e₁ σ E) := by + iintro Hinv + unfold baseCompletenessGoal + imodintro + iright + iframe Hinv + iintro %Φ %E₂ H + iapply wp_pure_step_later (Hexec := hpe) (Hφ := hφ) + iintro !> _ + ihave Htraj : iprop(∀ σ₁, heap_inv σ₁ ={E}=∗ + ∃ κ σ₁', ⌜PrimSteps e₁ σ₁ κ e₂ σ₁' []⌝ ∗ heap_inv σ₁') $$ [] + · iintro %σ₁ Hinv₁ + imodintro + iexists [], σ₁ + iframe Hinv₁ + ipureintro + exact PrimSteps.once (EctxLanguage.primStep_of_baseStep (hbase σ₁)) + iapply fupd_wp + imod H $$ Htraj with ⟨Hwp, _⟩ + imodintro + iexact Hwp + +/-- Atomic heap-step branch of `wp_base_completeness`: a deterministic heap +operation at a live location `l` (reading cell `some vlive`, writing `vnew`, +returning `v₂`) lands in the atomic disjunct. The WP's own step (via +`wp_lift_atomic_step`) exposes the later needed to strip the magic premise. -/ +theorem wp_base_atomic {e₁ : Exp} {v₂ : Val} (l : Loc) (vlive : Val) (vnew : Option Val) + (σ : State) (E : CoPset) + (hatom : Atomic Atomicity.StronglyAtomic e₁) + (hcell : get? (M := HeapF) σ.heap l = some (some vlive)) + (hbase : ∀ σ'' : State, get? (M := HeapF) σ''.heap l = some (some vlive) → + BaseStep e₁ σ'' [] (ToVal.ofVal v₂) (σ''.initHeap l 1 vnew) []) + (hdet : ∀ {σ'' : State} {obs e' σ''' efs}, + get? (M := HeapF) σ''.heap l = some (some vlive) → + BaseStep e₁ σ'' obs e' σ''' efs → + obs = [] ∧ e' = (ToVal.ofVal v₂ : Exp) ∧ σ''' = σ''.initHeap l 1 vnew ∧ efs = []) : + heap_inv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e₁ σ E) := by + iintro ⟨Hmap, Hproph_inv⟩ + unfold baseCompletenessGoal + imodintro + ileft + iframe %hatom + iintro %Φ Hstep + -- For the live cell, `heapCellPts l (some vlive)` reduces to `l ↦ some vlive`. + icases (BigSepM.bigSepM_insert_acc (M := HeapF) + (Φ := fun (k : Loc) (vo : Option Val) => iprop(heapCellPts k vo ∗ metaToken k ⊤)) hcell) + $$ Hmap with ⟨⟨Hpt, Hmeta⟩, Hclose⟩ + iapply wp_lift_atomic_step (EctxLanguage.val_stuck (hbase σ hcell)) + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + ihave %hcell1 : ⌜get? (M := HeapF) σ₁.heap l = some (some vlive)⌝ $$ [Hσ Hpt] + · icases genHeap_valid $$ [$Hσ $Hpt] with >%hh + itrivial + isplitr + · ipureintro + simp only [Stuckness.MaybeReducible] + exact EctxLanguage.primStep_reducible_of_baseStep_reducible + ⟨[], _, _, [], hbase σ₁ hcell1⟩ + iintro !> %e₂ %σ₂ %eₜ %Hprim Hcr + obtain ⟨rfl, rfl, rfl, rfl⟩ := + hdet hcell1 (EctxLanguage.baseStep_of_primStep_of_baseStep_reducible ⟨[], _, _, [], hbase σ₁ hcell1⟩ Hprim) + imod genHeap_update (v₂ := vnew) $$ [$Hσ $Hpt] with ⟨Hσ, Hpt⟩ + imod Hstep $$ [] with ⟨Hpost, _⟩ + · ipureintro + exact EctxLanguage.primStep_of_baseStep (hbase σ hcell) + imodintro + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + have hl0 : l + (0 : Int) = l := by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind + simp only [stateInterp, State.initHeap, Int.toNat_one, List.range_one, List.foldl_cons, + Int.cast_ofNat_Int, List.foldl_nil, hl0, + Algebra.BigOpL.bigOpL_nil] + iframe Hσ Hproph + isplitl [Hpost Hclose Hpt Hmeta Hproph_inv] + · iexists v₂ + isplit + · ipureintro; simp [toVal]; rfl + iapply Hpost + simp only [heap_inv] + isplitl [Hclose Hpt Hmeta] + · iapply Hclose + isplitl [Hpt] + -- Convert the raw points-to back into the cell invariant (`emp` if freed). + · iapply (pointsTo_heapCellPts l vnew); iexact Hpt + · iexact Hmeta + · iexact Hproph_inv + · itrivial + +/-- Atomic heap-step branch that leaves the heap unchanged (read-only ops: `load`, +failing `cmpXchg`). -/ +theorem wp_base_atomic_nochange {e₁ : Exp} {v₂ : Val} (l : Loc) (vlive : Val) + (σ : State) (E : CoPset) + (hatom : Atomic Atomicity.StronglyAtomic e₁) + (hcell : get? (M := HeapF) σ.heap l = some (some vlive)) + (hbase : ∀ σ'' : State, get? (M := HeapF) σ''.heap l = some (some vlive) → + BaseStep e₁ σ'' [] (ToVal.ofVal v₂) σ'' []) + (hdet : ∀ {σ'' : State} {obs e' σ''' efs}, + get? (M := HeapF) σ''.heap l = some (some vlive) → + BaseStep e₁ σ'' obs e' σ''' efs → + obs = [] ∧ e' = (ToVal.ofVal v₂ : Exp) ∧ σ''' = σ'' ∧ efs = []) : + heap_inv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e₁ σ E) := by + iintro ⟨Hmap, Hproph_inv⟩ + unfold baseCompletenessGoal + imodintro + ileft + iframe %hatom + iintro %Φ Hstep + iapply wp_lift_atomic_step (EctxLanguage.val_stuck (hbase σ hcell)) + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + ihave %hcell1 : ⌜get? (M := HeapF) σ₁.heap l = some (some vlive)⌝ $$ [Hσ Hmap] + · icases (BigSepM.bigSepM_lookup_acc (M := HeapF) + (Φ := fun (k : Loc) (vo : Option Val) => iprop(heapCellPts k vo ∗ metaToken k ⊤)) hcell).1 + $$ Hmap with ⟨⟨Hpt, _⟩, _⟩ + icases genHeap_valid $$ [$Hσ $Hpt] with >%hh + itrivial + isplitr + · ipureintro + simp only [Stuckness.MaybeReducible] + exact EctxLanguage.primStep_reducible_of_baseStep_reducible + ⟨[], _, _, [], hbase σ₁ hcell1⟩ + iintro !> %e₂ %σ₂ %eₜ %Hprim Hcr + obtain ⟨rfl, rfl, rfl, rfl⟩ := + hdet hcell1 (EctxLanguage.baseStep_of_primStep_of_baseStep_reducible + ⟨[], _, _, [], hbase σ₁ hcell1⟩ Hprim) + imod Hstep $$ [] with ⟨Hpost, _⟩ + · ipureintro + exact EctxLanguage.primStep_of_baseStep (hbase σ hcell) + imodintro + ihave Hproph := (prophMapInterp_nil_append obs' σ₂.usedProphId).mp $$ Hproph + simp only [stateInterp] + iframe Hσ Hproph + isplitl [Hpost Hmap Hproph_inv] + · iexists v₂ + isplit + · ipureintro; simp [toVal]; rfl + iapply Hpost + simp only [heap_inv] + iframe Hmap Hproph_inv + · itrivial + +/-! ### Per-operation determinism facts. + +These discharge the `hdet` argument of `wp_base_atomic`(`_nochange`): for a fixed +redex and a fixed value of the cell being acted on, the base step's output is +uniquely determined. In Rocq these are obtained for free by reasoning forward +with the concrete `wp_load`/`wp_store`/… rules; here the generic atomic helper +takes the determinism as an explicit side condition. Each is a one-constructor +`cases` followed by reading off the cell equation. -/ + +theorem loadS_det {l : Loc} {v : Val} {σ : State} {obs e' σ' efs} + (h : get? (M := HeapF) σ.heap l = some (some v)) + (hs : BaseStep (.load (.val (.lit (.loc l)))) σ obs e' σ' efs) : + obs = [] ∧ e' = (ToVal.ofVal v : Exp) ∧ σ' = σ ∧ efs = [] := by + cases hs with + | loadS _ v' _ h' => + simp only [State.get?] at h' + rw [h] at h' + simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at h' + subst h' + refine ⟨rfl, rfl, rfl, rfl⟩ + +theorem storeS_det {l : Loc} {w : Val} {σ : State} {obs e' σ' efs} + (hs : BaseStep (.store (.val (.lit (.loc l))) (.val w)) σ obs e' σ' efs) : + obs = [] ∧ e' = (ToVal.ofVal (Val.lit .unit) : Exp) ∧ + σ' = σ.initHeap l 1 (some w) ∧ efs = [] := by + cases hs with + | storeS _ _ _ _ _ => refine ⟨rfl, rfl, rfl, rfl⟩ + +theorem freeS_det {l : Loc} {σ : State} {obs e' σ' efs} + (hs : BaseStep (.free (.val (.lit (.loc l)))) σ obs e' σ' efs) : + obs = [] ∧ e' = (ToVal.ofVal (Val.lit .unit) : Exp) ∧ + σ' = σ.initHeap l 1 none ∧ efs = [] := by + cases hs with + | freeS _ _ _ _ => refine ⟨rfl, rfl, rfl, rfl⟩ + +theorem xchgS_det {l : Loc} {v1 v2 : Val} {σ : State} {obs e' σ' efs} + (h : get? (M := HeapF) σ.heap l = some (some v1)) + (hs : BaseStep (.xchg (.val (.lit (.loc l))) (.val v2)) σ obs e' σ' efs) : + obs = [] ∧ e' = (ToVal.ofVal v1 : Exp) ∧ σ' = σ.initHeap l 1 (some v2) ∧ efs = [] := by + cases hs with + | xchgS _ v1' _ _ h' => + simp only [State.get?] at h' + rw [h] at h' + simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at h' + subst h' + refine ⟨rfl, rfl, rfl, rfl⟩ + +theorem faaS_det {l : Loc} {i1 i2 : Int} {σ : State} {obs e' σ' efs} + (h : get? (M := HeapF) σ.heap l = some (some (Val.lit (.int i1)))) + (hs : BaseStep (.faa (.val (.lit (.loc l))) (.val (.lit (.int i2)))) σ obs e' σ' efs) : + obs = [] ∧ e' = (ToVal.ofVal (Val.lit (.int i1)) : Exp) ∧ + σ' = σ.initHeap l 1 (some (Val.lit (.int (i1 + i2)))) ∧ efs = [] := by + cases hs with + | faaS _ i1' _ _ h' => + simp only [State.get?] at h' + rw [h] at h' + simp only [Option.some.injEq, Val.lit.injEq, BaseLit.int.injEq] at h' + subst h' + refine ⟨rfl, rfl, rfl, rfl⟩ + +theorem cmpXchgS_det_true {l : Loc} {v1 v2 vl : Val} {σ : State} {obs e' σ' efs} + (h : get? (M := HeapF) σ.heap l = some (some vl)) (htrue : decide (vl = v1) = true) + (hs : BaseStep (.cmpXchg (.val (.lit (.loc l))) (.val v1) (.val v2)) σ obs e' σ' efs) : + obs = [] ∧ e' = (ToVal.ofVal (Val.pair vl (.lit (.bool true))) : Exp) ∧ + σ' = σ.initHeap l 1 (some v2) ∧ efs = [] := by + cases hs with + | cmpXchgS _ _ _ vl' _ b' h' hcs' hb' => + simp only [State.get?] at h' + rw [h] at h' + simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at h' + subst h' + rw [htrue] at hb' + subst hb' + refine ⟨rfl, rfl, rfl, rfl⟩ + +theorem cmpXchgS_det_false {l : Loc} {v1 v2 vl : Val} {σ : State} {obs e' σ' efs} + (h : get? (M := HeapF) σ.heap l = some (some vl)) (hfalse : decide (vl = v1) = false) + (hs : BaseStep (.cmpXchg (.val (.lit (.loc l))) (.val v1) (.val v2)) σ obs e' σ' efs) : + obs = [] ∧ e' = (ToVal.ofVal (Val.pair vl (.lit (.bool false))) : Exp) ∧ + σ' = σ ∧ efs = [] := by + cases hs with + | cmpXchgS _ _ _ vl' _ b' h' hcs' hb' => + simp only [State.get?] at h' + rw [h] at h' + simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at h' + subst h' + rw [hfalse] at hb' + subst hb' + refine ⟨rfl, rfl, rfl, rfl⟩ + +/-! ### Multi-cell allocation helpers (for the `allocN` branch). + +`allocN n v` writes `v` into `n` consecutive fresh locations. The state update +`State.initHeap` is a left-fold of single inserts; the lemmas below characterise +its heap pointwise and as a left-biased union with a freshly-built block +`allocCells`, which is what lets `genHeap_alloc_big` produce the new points-to and +meta tokens. -/ + +/-- A block of `n` cells all holding `v`, starting at `l` (`l, l+1, …, l+(n-1)`). +This is `(State.initHeap σ l n v).heap` with the existing heap `σ.heap` removed. -/ +def allocCells (l : Loc) (n : Nat) (v : Option Val) : HeapF (Option Val) := + (List.range n).foldl (fun h (i : Nat) => Std.insert (M := HeapF) h (l + (i : Int)) v) ∅ + +theorem get?_foldl_insert (l : Loc) (v : Option Val) (m : HeapF (Option Val)) (n : Nat) (k : Loc) : + get? (M := HeapF) ((List.range n).foldl + (fun h (i : Nat) => Std.insert (M := HeapF) h (l + (i : Int)) v) m) k + = if (∃ i, i < n ∧ k = l + (i : Int)) then some v else get? (M := HeapF) m k := by + induction n with + | zero => simp + | succ n ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, + Iris.Std.LawfulPartialMap.get?_insert, ih] + by_cases hk : (l + (n : Int)) = k + · rw [if_pos hk, if_pos ⟨n, Nat.lt_succ_self n, hk.symm⟩] + · rw [if_neg hk] + by_cases hex : ∃ i, i < n ∧ k = l + (i : Int) + · obtain ⟨i, hi, hki⟩ := hex + rw [if_pos ⟨i, hi, hki⟩, if_pos ⟨i, Nat.lt_succ_of_lt hi, hki⟩] + · rw [if_neg hex, if_neg] + rintro ⟨i, hi, hki⟩ + rcases Nat.lt_succ_iff_lt_or_eq.mp hi with hi' | rfl + · exact hex ⟨i, hi', hki⟩ + · exact hk hki.symm + +theorem get?_allocCells {l : Loc} {n : Nat} {v : Option Val} {k : Loc} : + get? (M := HeapF) (allocCells l n v) k + = if (∃ i, i < n ∧ k = l + (i : Int)) then some v else none := by + rw [allocCells, get?_foldl_insert] + simp only [LawfulPartialMap.get?_empty] + +/-- `State.initHeap` is the left-biased union of the fresh block with the old heap. -/ +theorem initHeap_heap_eq {σ : State} {l : Loc} {n : Int} {v : Option Val} : + Iris.Std.PartialMap.equiv (M := HeapF) (σ.initHeap l n v).heap + (Iris.Std.PartialMap.union (allocCells l n.toNat v) σ.heap) := by + intro k + show get? (M := HeapF) ((List.range n.toNat).foldl + (fun h (i : Nat) => Std.insert (M := HeapF) h (l + (i : Int)) v) σ.heap) k = _ + rw [get?_foldl_insert] + simp only [Iris.Std.PartialMap.union, Iris.Std.LawfulPartialMap.get?_merge, get?_allocCells] + by_cases hex : ∃ i, i < n.toNat ∧ k = l + (i : Int) + · simp only [if_pos hex]; cases get? (M := HeapF) σ.heap k <;> rfl + · simp only [if_neg hex]; cases get? (M := HeapF) σ.heap k <;> rfl + +theorem allocCells_disjoint {l : Loc} {n : Int} {v : Val} {m : HeapF (Option Val)} + (hf : ∀ i : Int, 0 ≤ i → i < n → get? (M := HeapF) m (l + i) = none) : + Std.PartialMap.disjoint (M := HeapF) (allocCells l n.toNat (some v)) m := by + intro k ⟨h1, h2⟩ + rw [get?_allocCells] at h1 + split at h1 <;> rename_i hcond + · obtain ⟨i, hi, hki⟩ := hcond + rw [hki, hf (i : Int) (Int.natCast_nonneg i) (by omega)] at h2 + simp at h2 + · simp at h1 + +private theorem mem_le_foldr_max (x : Int) (L : List Int) (h : x ∈ L) : + x ≤ L.foldr max 0 := by + induction L with + | nil => simp at h + | cons a L ih => + simp only [List.foldr_cons] + rcases List.mem_cons.mp h with rfl | h + · omega + · have := ih h; omega + +/-- Any heap has a fresh block of `n` consecutive locations: pick a base strictly +above every used location's address. This is the reducibility witness for the +`allocN` lift, replacing Rocq's built-in `fresh_locs`. -/ +theorem exists_fresh_block (m : HeapF (Option Val)) (n : Int) : + ∃ l : Loc, ∀ i : Int, 0 ≤ i → i < n → get? (M := HeapF) m (l + i) = none := by + refine ⟨Loc.mk ((m.keys.map Loc.n).foldr max 0 + 1), fun i hi0 hin => ?_⟩ + have hnotmem : (Loc.mk ((m.keys.map Loc.n).foldr max 0 + 1) + i) ∉ m.keys := by + intro hmem + have hle : (Loc.mk ((m.keys.map Loc.n).foldr max 0 + 1) + i).n + ≤ (m.keys.map Loc.n).foldr max 0 := + mem_le_foldr_max _ _ (List.mem_map_of_mem hmem) + simp only [loc_add_n] at hle + omega + simpa [get?, getElem?_eq_none_iff, ← Std.ExtTreeMap.mem_keys] using hnotmem + +private theorem coPset_top_ne_empty : (⊤ : CoPset) ≠ ∅ := by + intro h + have hm : Pos.xH ∈ (⊤ : CoPset) := CoPset.mem_full + rw [h] at hm + exact CoPset.mem_empty hm + +/-- Inserting a prophecy id into the used-id set is the same as unioning in the +singleton, phrased for the native `ExtTreeSet.insert`. -/ +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_union_iff, Std.ExtTreeSet.mem_insert, + Iris.Std.mem_singleton_extTreeSet, Std.LawfulEqCmp.compare_eq_iff_eq] + exact ⟨fun h => h.imp Eq.symm id, fun h => h.imp Eq.symm id⟩ + +/-- The heap-only completeness equation: case analysis on the base step. Mirrors +`wp_base_completeness` in `case_studies/heaplang/completeness_generic.v`. -/ +theorem wp_base_completeness (e₁ : Exp) (σ : State) (E : CoPset) + (Hred : BaseStep.Reducible (e₁, σ)) : + heap_inv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e₁ σ E) := by + iintro Hinv + obtain ⟨κ, e', σ', efs, Hstep⟩ := Hred + cases Hstep with + | recS f x e σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.recS f x e σ')) $$ Hinv + | pairS v1 v2 σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.pairS v1 v2 σ')) $$ Hinv + | injLS v σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.injLS v σ')) $$ Hinv + | injRS v σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.injRS v σ')) $$ Hinv + | betaS f x eb v2 e' σ h => + subst h + iapply (wp_base_pure trivial σ E + (fun σ' => BaseStep.betaS f x eb v2 _ σ' rfl)) $$ Hinv + | unOpS op v v' σ h => + iapply (wp_base_pure (hpe := instPureExecUnOp) h σ E + (fun σ' => BaseStep.unOpS op v v' σ' h)) $$ Hinv + | binOpS op v1 v2 v' σ h => + iapply (wp_base_pure (hpe := instPureExecBinOp) h σ E + (fun σ' => BaseStep.binOpS op v1 v2 v' σ' h)) $$ Hinv + | ifTrueS et ee σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.ifTrueS e' ee σ')) $$ Hinv + | ifFalseS et ee σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.ifFalseS et e' σ')) $$ Hinv + | fstS v1 v2 σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.fstS v1 v2 σ')) $$ Hinv + | sndS v1 v2 σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.sndS v1 v2 σ')) $$ Hinv + | caseLS v et ee σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.caseLS v et ee σ')) $$ Hinv + | caseRS v et ee σ => + iapply (wp_base_pure trivial σ E (fun σ' => BaseStep.caseRS v et ee σ')) $$ Hinv + | loadS l v σ hl => + iapply (wp_base_atomic_nochange (v₂ := v) l v σ E + (base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.loadS l v σ hl)) hl + (fun σ'' h => BaseStep.loadS l v σ'' h) loadS_det) $$ Hinv + | storeS l v w σ hl => + iapply (wp_base_atomic (v₂ := .lit .unit) l v (some w) σ E + (base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.storeS l v w σ hl)) hl + (fun σ'' h => BaseStep.storeS l v w σ'' h) (fun _ hs => storeS_det hs)) $$ Hinv + | freeS l v σ hl => + iapply (wp_base_atomic (v₂ := .lit .unit) l v none σ E + (base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.freeS l v σ hl)) hl + (fun σ'' h => BaseStep.freeS l v σ'' h) (fun _ hs => freeS_det hs)) $$ Hinv + | xchgS l v1 v2 σ hl => + iapply (wp_base_atomic (v₂ := v1) l v1 (some v2) σ E + (base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.xchgS l v1 v2 σ hl)) hl + (fun σ'' h => BaseStep.xchgS l v1 v2 σ'' h) xchgS_det) $$ Hinv + | faaS l i1 i2 σ hl => + iapply (wp_base_atomic (v₂ := .lit (.int i1)) l (.lit (.int i1)) + (some (.lit (.int (i1 + i2)))) σ E + (base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.faaS l i1 i2 σ hl)) hl + (fun σ'' h => BaseStep.faaS l i1 i2 σ'' h) faaS_det) $$ Hinv + | cmpXchgS l v1 v2 vl σ b hl hcs hb => + cases hb1 : decide (vl = v1) with + | true => + iapply (wp_base_atomic (v₂ := .pair vl (.lit (.bool true))) l vl (some v2) σ E + (base_step_to_val_atomic Atomicity.StronglyAtomic + (BaseStep.cmpXchgS l v1 v2 vl σ true hl hcs (by rw [hb1]))) + hl + (fun σ'' h => by + have := BaseStep.cmpXchgS l v1 v2 vl σ'' true h hcs (by rw [hb1]) + simpa using this) + (fun h hs => cmpXchgS_det_true h hb1 hs)) $$ Hinv + | false => + iapply (wp_base_atomic_nochange (v₂ := .pair vl (.lit (.bool false))) l vl σ E + (base_step_to_val_atomic Atomicity.StronglyAtomic + (BaseStep.cmpXchgS l v1 v2 vl σ false hl hcs (by rw [hb1]))) + hl + (fun σ'' h => by + have := BaseStep.cmpXchgS l v1 v2 vl σ'' false h hcs (by rw [hb1]) + simpa using this) + (fun h hs => cmpXchgS_det_false h hb1 hs)) $$ Hinv + | forkS e σ => + -- Fork lands in the non-atomic disjunct: the forked thread `e` becomes the + -- single forked expression `efs = [e]`, and the parent steps to `#()`. + imodintro + iright + iframe Hinv + iintro %Φ %E₂ H + iapply wp_fork_fupd + iintro !> + ihave Htraj : iprop(∀ σ₁, heap_inv σ₁ ={E}=∗ + ∃ κ σ₁', ⌜PrimSteps (.fork e) σ₁ κ (.val (.lit .unit)) σ₁' [e]⌝ ∗ heap_inv σ₁') $$ [] + · iintro %σ₁ Hheap + imodintro + iexists [], σ₁ + iframe Hheap + ipureintro + exact PrimSteps.once (EctxLanguage.primStep_of_baseStep (BaseStep.forkS e σ₁)) + imod H $$ Htraj with ⟨HwpUnit, Hefs⟩ + isplitl [Hefs] + · iapply (BI.BigSepL.bigSepL_singleton (PROP := IProp GF)).1 $$ Hefs + · iapply (wp_value_fupd' (v := .lit .unit)).1 $$ HwpUnit + | allocNS n v σ l hn hfresh => + -- `allocN` is atomic and allocates a fresh block of `n` cells. + imodintro + ileft + have hatom : Atomic Atomicity.StronglyAtomic (Exp.allocN (.val (.lit (.int n))) (.val v)) := + base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.allocNS n v σ l hn hfresh) + iframe %hatom + iintro %Φ Hstep + iapply wp_lift_atomic_step + (EctxLanguage.val_stuck (BaseStep.allocNS n v σ l hn hfresh)) + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + -- Reducibility in `σ₁` from a fresh block. + obtain ⟨lf, hlf⟩ := exists_fresh_block σ₁.heap n + have Hred₁ : BaseStep.Reducible (Exp.allocN (.val (.lit (.int n))) (.val v), σ₁) := + ⟨[], _, _, [], BaseStep.allocNS n v σ₁ lf hn hlf⟩ + isplitr + · ipureintro + simp only [Stuckness.MaybeReducible] + exact EctxLanguage.primStep_reducible_of_baseStep_reducible Hred₁ + iintro !> %e₂ %σ₂ %eₜ %Hprim Hcr + cases EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred₁ Hprim + rename_i l' Hpo Hi + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + -- Destructure `heap_inv σ` into its heap and prophecy conjuncts. + icases Hinv with ⟨Hmap, Hproph_inv⟩ + -- Allocate the new block in the state interpretation. + imod (genHeap_alloc_big (allocCells l' n.toNat (some v)) σ₁.heap (allocCells_disjoint Hi)) + $$ Hσ with ⟨Hσ', Hnewpts, Hnewmeta⟩ + -- Freshness of the block in `σ` (the `heap_inv` state), via `meta_token_ne`. + ihave %hfreshσ : ⌜∀ i : Int, 0 ≤ i → i < n → get? (M := HeapF) σ.heap (l' + i) = none⌝ + $$ [Hmap Hnewmeta] + · iintro %i %hi0 %hin + rcases hgc : get? (M := HeapF) σ.heap (l' + i) with _ | vo + · itrivial + · icases (BigSepM.bigSepM_lookup_acc (M := HeapF) + (Φ := fun (k : Loc) (vo : Option Val) => iprop(heapCellPts k vo ∗ metaToken k ⊤)) hgc).1 + $$ Hmap with ⟨⟨_, Hmeta1⟩, _⟩ + have hcell_new : get? (M := HeapF) (allocCells l' n.toNat (some v)) (l' + i) + = some (some v) := by + rw [get?_allocCells, if_pos ⟨i.toNat, by omega, by rw [Int.toNat_of_nonneg hi0]⟩] + icases (BigSepM.bigSepM_lookup_acc (M := HeapF) + (Φ := fun (k : Loc) (_vo : Option Val) => iprop(metaToken k ⊤)) hcell_new).1 + $$ Hnewmeta with ⟨Hmeta2, _⟩ + icases metaToken_ne coPset_top_ne_empty $$ Hmeta1 Hmeta2 with %hne + exact absurd rfl hne + -- Instantiate the magic premise with the base step from `σ` at `l'`. + imod Hstep $$ [] with ⟨Hpost, _⟩ + · ipureintro + exact EctxLanguage.primStep_of_baseStep (BaseStep.allocNS n v σ l' hn hfreshσ) + imodintro + isplitl [Hσ' Hproph] + · simp only [stateInterp] + isplitl [Hσ'] + · iapply genHeapInterp_eqv (Iris.Std.PartialMap.equiv.symm _ _ initHeap_heap_eq) + iexact Hσ' + · iexact Hproph + isplitl [Hpost Hmap Hproph_inv Hnewpts Hnewmeta] + · iexists (.lit (.loc l')) + isplit + · ipureintro; simp [toVal]; rfl + iapply Hpost + simp only [heap_inv] + isplitl [Hmap Hnewpts Hnewmeta] + · iapply (BigSepM.bigSepM_eqv_of_perm + (Φ := fun (k : Loc) (vo : Option Val) => iprop(heapCellPts k vo ∗ metaToken k ⊤)) + initHeap_heap_eq).2 + iapply (BigSepM.bigSepM_union + (Φ := fun (k : Loc) (vo : Option Val) => iprop(heapCellPts k vo ∗ metaToken k ⊤)) + (allocCells_disjoint hfreshσ)).2 + isplitl [Hnewpts Hnewmeta] + · iapply (Iris.BI.equiv_iff.mp (BigSepM.bigSepM_sep_eqv (M := HeapF) + (Φ := fun (k : Loc) (vo : Option Val) => heapCellPts k vo) + (Ψ := fun (k : Loc) (_vo : Option Val) => iprop(metaToken k ⊤)))).2 + -- Convert the raw points-tos of the freshly-allocated (live) cells + -- into cell invariants before framing. + ihave Hnewpts := (BigSepM.bigSepM_mono_of_forall + (fun {k vo} => pointsTo_heapCellPts k vo)) $$ Hnewpts + iframe Hnewpts Hnewmeta + · iexact Hmap + · iexact Hproph_inv + · itrivial + | newProphS σ p hp => + -- `newProph` is atomic and allocates a fresh prophecy variable. + imodintro + ileft + have hatom : Atomic Atomicity.StronglyAtomic (Exp.newProph : Exp) := + base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.newProphS σ p hp) + iframe %hatom + iintro %Φ Hstep + iapply wp_lift_atomic_step + (EctxLanguage.val_stuck (BaseStep.newProphS σ p hp)) + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + -- Pick a prophecy id fresh in `σ₁.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 + simp only [Stuckness.MaybeReducible] + exact EctxLanguage.primStep_reducible_of_baseStep_reducible Hred₁ + iintro !> %e₂ %σ₂ %eₜ %Hprim Hcr + cases EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred₁ Hprim + rename_i p' Hp' + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + 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⟩ + -- Destructure `heap_inv σ` and derive that `p'` is fresh in `σ` via + -- `proph_exclusive` against `Hproph_inv`. + icases Hinv with ⟨Hmap, Hproph_inv⟩ + ihave %Hfresh_σ : ⌜p' ∉ σ.usedProphId⌝ $$ [Hproph_inv Htok] + · iintro %hmem + icases Iris.BI.BigSepS.bigSepS_elem_of_acc hmem $$ Hproph_inv with ⟨⟨%pvs', Htok'⟩, _⟩ + iapply proph_exclusive $$ Htok Htok' + have Hfresh_σ_contains : ¬ σ.usedProphId.contains p' := fun hc => + Hfresh_σ (Std.ExtTreeSet.mem_iff_contains.symm.mpr hc) + -- Instantiate the magic premise with the `newProph` step from `σ` at `p'`. + imod Hstep $$ [] with ⟨Hpost, _⟩ + · ipureintro + exact EctxLanguage.primStep_of_baseStep (BaseStep.newProphS σ p' Hfresh_σ_contains) + imodintro + isplitl [Hσ Hproph'] + · simp only [stateInterp] + iframe Hσ + rw [show ({p'} ∪ σ₁.usedProphId : Std.ExtTreeSet ProphId compare) + = σ₁.usedProphId.insert p' from usedProph_insert_eq.symm] + iexact Hproph' + isplitl [Hpost Hmap Hproph_inv Htok] + · iexists (.lit (.prophecy p')) + isplit + · ipureintro; simp [toVal]; rfl + iapply Hpost + simp only [heap_inv] + isplitl [Hmap] + · iexact Hmap + · -- goal: bigSepS (σ.usedProphId.insert p') (∃ pvs, proph) + rw [usedProph_insert_eq (ps := σ.usedProphId) (p := p')] + have hdisj : ({p'} : Std.ExtTreeSet ProphId compare) ## σ.usedProphId := by + intro x ⟨h1, h2⟩ + rw [Iris.Std.LawfulSet.mem_singleton] at h1 + subst h1 + exact Hfresh_σ h2 + iapply (Iris.BI.BigSepS.bigSepS_union hdisj).mpr + isplitl [Htok] + · iapply Iris.BI.BigSepS.bigSepS_singleton.mpr + iexists (prophListResolves obs' p') + iexact Htok + · iexact Hproph_inv + · itrivial + | resolveS p v e σ w σ' κs ts hbase hp => + -- Mirror of `completeness_generic.v:127–159`. Resolve is atomic since the + -- inner step `hbase` produces a value in one base step. We recurse on + -- `hbase` to get the completeness equation for `e`, then lift through + -- the `Resolve` wrapper via `wp_resolve_strong`. + have IH : heap_inv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e σ E) := + wp_base_completeness e σ E ⟨κs, _, _, _, hbase⟩ + have hatom : Atomic Atomicity.StronglyAtomic + (Exp.resolve e (.val (.lit (.prophecy p))) (.val w)) := + base_step_to_val_atomic Atomicity.StronglyAtomic + (BaseStep.resolveS p v e σ w σ' κs efs hbase hp) + have hatom_e : Atomic Atomicity.StronglyAtomic e := + base_step_to_val_atomic Atomicity.StronglyAtomic hbase + have hne_e : toVal e = none := EctxLanguage.val_stuck hbase + have hp_mem : p ∈ σ.usedProphId := Std.ExtTreeSet.mem_iff_contains.symm.mpr hp + imodintro + ileft + iframe %hatom + iintro %Φ Hstep + icases Hinv with ⟨Hmap, Hproph_inv⟩ + icases Iris.BI.BigSepS.bigSepS_elem_of_acc hp_mem $$ Hproph_inv + with ⟨⟨%pvs, Htok⟩, HcloseProph⟩ + iapply (wp_resolve_strong hatom_e hne_e) $$ Htok + iintro Hele + ihave Hinv_full : iprop(heap_inv σ) $$ [Hmap HcloseProph Hele] + · unfold heap_inv + iframe Hmap + iapply HcloseProph + iexists pvs; iexact Hele + ihave Hinner : iprop(|={E}=> baseCompletenessGoal e σ E) $$ [Hinv_full] + · iapply IH; iexact Hinv_full + iapply fupd_wp + imod Hinner with H + imodintro + icases H with (⟨_hatom_e', Hrst⟩ | ⟨Hinv_back, Hrst_nonatom⟩) + · -- Atomic disjunct: feed `Hrst` the resolve-strong post for `e`. + iapply Hrst + iintro !> %κ_e %v_e %σ_e %efs_e %Hprim_e + have Hbase_e : BaseStep e σ κ_e (.val v_e) σ_e efs_e := + primStep_val_baseStep Hprim_e + imod Hstep $$ %_ %_ %_ %_ %(prim_step_resolve_of_inner (w := w) Hbase_e hp) + with ⟨Hwp_outer, Hefs⟩ + imodintro + iframe Hefs + iintro ⟨Hmap_e, Hproph_inv_e⟩ + have hp_mem_e : p ∈ σ_e.usedProphId := + base_step_more_proph_ids Hbase_e p hp_mem + icases Iris.BI.BigSepS.bigSepS_elem_of_acc hp_mem_e $$ Hproph_inv_e + with ⟨⟨%pvs2, Hele2⟩, HcloseProph_e⟩ + iexists pvs2 + iframe Hele2 + iintro %pvs'' %heq Hele2' + subst heq + iapply Hwp_outer + unfold heap_inv + iframe Hmap_e + iapply HcloseProph_e + iexists pvs''; iexact Hele2' + · -- Non-atomic disjunct: symmetric to the atomic case, plus extracting + -- the single prim step from the trajectory via `primSteps_atomic`. + iapply Hrst_nonatom + iintro !> %e₂_e %efs_e Htraj_e + imod Htraj_e $$ %_ Hinv_back with ⟨%κ_e, %σ_e, %Hprims, ⟨Hmap_e, Hproph_inv_e⟩⟩ + obtain ⟨Hprim_e, hval_e⟩ := + ProgramLogic.primSteps_atomic (e := e) hatom_e Hprims + obtain ⟨v_e, rfl⟩ : ∃ v_e, e₂_e = Exp.val v_e := by + match e₂_e, hval_e with + | .val v_e, _ => exact ⟨v_e, rfl⟩ + have Hbase_e : BaseStep e σ κ_e (.val v_e) σ_e efs_e := + primStep_val_baseStep Hprim_e + imod Hstep $$ %_ %_ %_ %_ %(prim_step_resolve_of_inner (w := w) Hbase_e hp) + with ⟨Hwp_outer, Hefs⟩ + imodintro + have hp_mem_e : p ∈ σ_e.usedProphId := + base_step_more_proph_ids Hbase_e p hp_mem + icases Iris.BI.BigSepS.bigSepS_elem_of_acc hp_mem_e $$ Hproph_inv_e + with ⟨⟨%pvs2, Hele2⟩, HcloseProph_e⟩ + isplitl [Hele2 Hwp_outer Hmap_e HcloseProph_e] + · -- WP (Val v_e) {{ strong-post }} — apply wp_value', witness pvs2. + iapply wp_value' + iexists pvs2 + iframe Hele2 + iintro %pvs'' %heq Hele2' + subst heq + iapply Hwp_outer + unfold heap_inv + iframe Hmap_e + iapply HcloseProph_e + iexists pvs''; iexact Hele2' + · iexact Hefs +termination_by e₁ + +section Framework + +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] [TI : TpinvGS GF Exp H] + +/-- The framework-facing heap-lang completeness equation: the `ectx`-level +soundness equation specialized to heap_lang's `heap_inv`. Mirrors +`wp_base_completeness_actual` in `case_studies/heaplang/completeness_generic.v`. -/ +theorem wp_base_completeness_actual + (n : Nat) (C : List Exp) (e₁ : Exp) (σ : State) (K : List ECtxItem) (E : CoPset) : + ⊢ ectxLangCompletenessStmt (Wp.wp (PROP := IProp GF) Stuckness.NotStuck) + (fun (_ : List Exp) (σ : State) => heap_inv σ) n C e₁ σ K E := by + unfold ectxLangCompletenessStmt + iintro %Hred Htok ⟨Hheap, Htp, %Hsafe⟩ + imod (wp_base_completeness e₁ σ E Hred) $$ Hheap with (⟨%Hatom, H⟩ | ⟨Hheap, H⟩) + · -- Atomic redex. + imodintro + ileft + have Hwa : Atomic Atomicity.WeaklyAtomic e₁ := stronglyAtomic_atomic Hatom + iframe %Hwa + iintro %Φ Hx + iapply H + iintro !> %κ %v₂ %σ' %efs %Hprim + iapply Hx $$ [] Htok Htp + ipureintro; exact Hprim + · -- Non-atomic redex. + imodintro + iright + iframe Hheap Htp + iintro %Φ Hx + iapply H + iintro !> %e₂ %efs HH + iapply Hx + iintro %σ₁ %C₁ ⟨Hsi, Htp, %_Hs⟩ + imod HH $$ Hsi with ⟨%κ, %σ₁', %Hprims, Hhp⟩ + imodintro + iexists κ, σ₁' + iframe Htok Htp Hhp + ipureintro + exact Hprims + +/-- HeapLang is an instance of the abstract ectx-completeness theory. Mirrors +`heap_lang_completeness` in `case_studies/heaplang/completeness_generic.v`. -/ +instance heap_lang_completeness : + AbstractEctxLangCompletenessGen (Expr := Exp) (Ectx := List ECtxItem) + (Wp.wp (PROP := IProp GF) Stuckness.NotStuck) where + heap_inv _C σ := heap_inv σ + heap_inv_timeless _C σ := heap_inv_timeless σ + ectx_lang_completeness n _C e₁ σ K E := wp_base_completeness_actual n _C e₁ σ K E + +end Framework + +section Endpoint + +/-- **Top-level heap-lang completeness**: an adequate program admits a WP with the +adequacy postcondition. Mirrors `heap_lang_sem_completeness` in +`case_studies/heaplang/completeness_classical.v`. -/ +theorem heap_lang_sem_completeness {H : Type _ → Type _} [LawfulFiniteMap H Nat] + [GhostMapG GF Nat Exp H] [CInvG GF] + (e : Exp) (σ : State) (φ : Val → Prop) + (Hade : adequate Stuckness.NotStuck e σ (fun v _ => φ v)) : + ⊢ heap_inv (GF := GF) σ -∗ WP e @ Stuckness.NotStuck; ⊤ {{ v, ⌜φ v⌝ }} := by + iintro Hheap + imod (tpInv_alloc (GF := GF) (Expr := Exp) (H := H)) with ⟨%γ, Hini⟩ + letI TI : TpinvGS GF Exp H := { toGhostMapG := inferInstance, tp_name := γ } + ihave Hwp := weakestpre_sem_completeness + (wp := Wp.wp (PROP := IProp GF) Stuckness.NotStuck) e σ φ Hade $$ Hini Hheap + iexact Hwp + +/-- Nofork variant. Mirrors `heap_lang_sem_completeness_nofork`. -/ +theorem heap_lang_sem_completeness_nofork {H : Type _ → Type _} [LawfulFiniteMap H Nat] + [GhostMapG GF Nat Exp H] [CInvG GF] + (e : Exp) (σ : State) (φ : Val → State → Prop) + (Hade : AdequateNoFork Stuckness.NotStuck e σ (fun v σ' => φ v σ')) : + ⊢ heap_inv (GF := GF) σ -∗ + WP e @ Stuckness.NotStuck; ⊤ {{ v, ∃ σ' : State, heap_inv σ' ∗ ⌜φ v σ'⌝ }} := by + iintro Hheap + imod (tpInv_alloc (GF := GF) (Expr := Exp) (H := H)) with ⟨%γ, Hini⟩ + letI TI : TpinvGS GF Exp H := { toGhostMapG := inferInstance, tp_name := γ } + ihave Hwp := weakestpre_sem_completeness_nofork + (wp := Wp.wp (PROP := IProp GF) Stuckness.NotStuck) e σ φ Hade $$ Hini Hheap + iexact Hwp + +end Endpoint + +end Iris.HeapLang diff --git a/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean b/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean new file mode 100644 index 000000000..e23d3334e --- /dev/null +++ b/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean @@ -0,0 +1,169 @@ +/- +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`: for a base-reducible redex `e₁` under an +evaluation context `K`, either `e₁` is weakly atomic and its post-step +obligation discharges the WP, or the configuration reduces and the WP follows by +binding under `K`. -/ +public def ectxLangCompletenessStmt (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}=∗ + ((⌜Atomic .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 [BWP : BindAbstractWP wp] +variable [AEC : AbstractEctxLangCompletenessGen wp] + +/-- Lift the ectx-level reduction soundness equation to a prim-level one: a prim +step decomposes as a base step under some evaluation context `K`, so the +ectx-level statement transfers to the prim level via `wp_bind`. -/ +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 %Hred Htok ⟨Hheap, Htp, %Hsafe⟩ + obtain ⟨κ, e', σ', efs, hstep⟩ := Hred + obtain @⟨e₁', e₂', K, Hbase⟩ := hstep + have Hbred : BaseStep.Reducible (e₁', σ) := ⟨κ, e₂', σ', efs, Hbase⟩ + have key := AEC.ectx_lang_completeness 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 (BWP.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 (BWP.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 := AEC.heap_inv_timeless + lang_completeness {n C e₁ σ E} := weakestpre_ectx_to_prim_completeness n C e₁ σ E + +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..57d030907 --- /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 (E := ⊤) (N := completenessN) (γ := γ) (p := q') + (P := 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..0ebfb6e4b --- /dev/null +++ b/Iris/Iris/ProgramLogic/AbstractWeakestPre.lean @@ -0,0 +1,238 @@ +/- +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, 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 generic `Wp`. -/ + +section IrisWP + +variable {Expr State Obs Val : Type _} [Language Expr State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] + +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 + +instance WP_bind_abstract : BindAbstractWP (Expr := Expr) (Val := Val) + (Wp.wp (PROP := IProp GF) Stuckness.NotStuck) where + wp_bind := ⟨wp_bind _, wp_bind_inv _⟩ + +-- TODO: Any idea how to get rid of the istops? + +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? + refine .trans wp_unfold.mp ?_ + rw (occs := [1]) [wp.pre] + iintro Hwp + rcases He' : toVal e' with (_|v'); rotate_left + · imod Hwp; imod Hwp + istop + refine .trans wp_unfold.mp ?_ + rw (occs := [1]) [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? + istop + refine .trans (BI.sep_mono .rfl wp_unfold.mp) ?_ + rw (occs := [1]) [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 := He.symm ▸ Hctx.toVal_eq_none_fill Hv' + 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 9cd153298..19b451411 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/ThreadPool.lean b/Iris/Iris/ProgramLogic/ThreadPool.lean new file mode 100644 index 000000000..8ddef6005 --- /dev/null +++ b/Iris/Iris/ProgramLogic/ThreadPool.lean @@ -0,0 +1,283 @@ +/- +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? (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 + iframe + +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