From ac6d473a94f4ebba49cb7a42896bb77c8af8154a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Klaus=20Kra=C3=9Fnitzer?= Date: Thu, 16 Jul 2026 17:17:04 +0200 Subject: [PATCH 1/3] feat: heap-operation tactics for HeapLang MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Port the heap-operation half of iris_heap_lang/proofmode.v: wp_load, wp_store, wp_xchg, wp_faa, wp_free, wp_alloc, and wp_cmpxchg{,_suc,_fail}. Tactic signatures mirror Rocq (`wp_alloc l as H`, `wp_cmpxchg as H1 | H2`), and every heap tactic first normalizes pure redexes (the `wp_pures;` prefix in the Rocq notations). The elaborators share three pieces of machinery: - runTacticHeapWp (prologue): runs wp_pures, parses the WP goal, extracts the HeapLangGS instance, and strips one later off the hypotheses. - lookupPointsTo: locates `l ↦{dq} some v` in the spatial context; the expected fraction is baked into the split certificate's type — writes pass the literal `DFrac.own 1`, reads a metavariable recording the fraction found. - finishHeapOp (epilogue): fills the result value back into the evaluation context and finishes the continuation. `set_option trace.wp_heap true` traces an invocation end to end. Tests cover the happy paths, harder positives, and #guard_msgs negatives locking the error messages and the writes' full-ownership discipline. --- Iris/Iris/HeapLang/ProofMode.lean | 458 +++++++++++++++++++++- Iris/Iris/Tests/HeapLang.lean | 1 + Iris/Iris/Tests/HeapLang/HeapTactics.lean | 453 +++++++++++++++++++++ 3 files changed, 906 insertions(+), 6 deletions(-) create mode 100644 Iris/Iris/Tests/HeapLang/HeapTactics.lean diff --git a/Iris/Iris/HeapLang/ProofMode.lean b/Iris/Iris/HeapLang/ProofMode.lean index 9492c94b2..e13a0c2e0 100644 --- a/Iris/Iris/HeapLang/ProofMode.lean +++ b/Iris/Iris/HeapLang/ProofMode.lean @@ -208,7 +208,6 @@ public meta def iWpValueHead {u} {ehyps : Q($prop)} (hyps : Hyps bi ehyps) (ι : Q(IrisGS_gen $hlc Exp $GF)) - (κ : Q(Wp $prop Exp Val Stuckness)) (s : Q(Stuckness)) (E : Q(CoPset)) (e : Q(Exp)) @@ -217,6 +216,7 @@ public meta def iWpValueHead {u} (_hu : QuotedLevelDefEq u 0 := ⟨⟩) (_hprop : $prop =Q IProp $GF := ⟨⟩) (_hbi : $bi =Q UPred.instBIUPred := ⟨⟩) + (κ : Q(Wp $prop Exp Val Stuckness) := q(wp.def)) (_hwp : $κ =Q wp.def := ⟨⟩) : ProofModeM (Option Q($ehyps ⊢ Wp.wp $s $E $e $Φ)) := do let ~q(ProgramLogic.ToVal.ofVal $v) := e @@ -241,7 +241,7 @@ public meta def iWpValueHead {u} elab "wp_value_head" : tactic => ProofModeM.runTacticWp fun mvar {bi, hyps, ι, s, E, e, Φ, hbi, ..} => do have : $bi =Q UPred.instBIUPred := hbi - let some pf ← iWpValueHead hyps ι q(wp.def) s E e Φ + let some pf ← iWpValueHead hyps ι s E e Φ | throwTacticEx `wp_value_head mvar s!"{e} is not a value" mvar.assign pf @@ -277,7 +277,6 @@ public meta def iWpFinish {u} {ehyps : Q($prop)} (hyps : Hyps bi ehyps) (ι : Q(IrisGS_gen $hlc Exp $GF)) - (κ : Q(Wp $prop Exp Val Stuckness)) (s : Q(Stuckness)) (E : Q(CoPset)) (e : Q(Exp)) @@ -286,16 +285,17 @@ public meta def iWpFinish {u} (_hu : QuotedLevelDefEq u 0 := ⟨⟩) (_hprop : $prop =Q IProp $GF := ⟨⟩) (_hbi : $bi =Q UPred.instBIUPred := ⟨⟩) + (κ : Q(Wp $prop Exp Val Stuckness) := q(wp.def)) (_hwp : $κ =Q wp.def := ⟨⟩) : ProofModeM (Q($ehyps ⊢ Wp.wp $s $E $e $Φ)) := do let ⟨e', pfeq⟩ ← iWpExprSimp e - let nextPf ← (← iWpValueHead hyps ι q(wp.def) s E e' Φ).getDM + let nextPf ← (← iWpValueHead hyps ι s E e' Φ).getDM (addBIGoal hyps q(Wp.wp $s $E $e' $Φ)) return q(tac_wp_expr_simp $nextPf $pfeq) elab "wp_finish" : tactic => ProofModeM.runTacticWp fun mvar {hyps, ι, s, E, e, Φ, ..} => do - let pf ← iWpFinish hyps ι q(wp.def) s E e Φ + let pf ← iWpFinish hyps ι s E e Φ mvar.assign pf public theorem tac_wp_bind [ι : IrisGS_gen hlc Exp GF] {Δ} {s : Stuckness} {E : CoPset} {K : List ECtxItem} {e' : Exp} {Φ : Val → IProp GF} @@ -364,7 +364,7 @@ elab "wp_pure " colGt ppSpace focus:hl_exp:10 : tactic => let ⟨inner, .up _⟩ ← HeapLang.fillQ K e₂ - let nextPf ← iWpFinish hyps' ι q(wp.def) s E inner Φ + let nextPf ← iWpFinish hyps' ι s E inner Φ let HΦ ← iSolveSidecondition q($φ) (failOnUnsolved := false) @@ -393,5 +393,451 @@ macro "wp_pair" : tactic => `(tactic | wp_pure ((_, _))) macro "wp_closure" : tactic => `(tactic | wp_pure (rec &_ &_ := _)) macro "wp_match" : tactic => `(tactic | (wp_case; wp_closure; wp_lam)) +/-! ## Tactic lemmas for the heap tactics -/ + +/-- Helper lemma for the heap `tac_wp_*` lemmas. -/ +theorem tac_wp_heap_op [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' P P' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {e : Exp} {r : Val} {Φ} + (hval : ProgramLogic.toVal e = none) + (hwp : ▷ P ⊢ WP e @ s ; E {{ v', ⌜v' = r⌝ ∗ P' }}) + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ P) + (hcont : Δ'' ∗ P' ⊢ WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) r)) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K e) @ s ; E {{ Φ }} := by + refine hlater.trans ?_ + refine .trans ?_ (wp_bind (ProgramLogic.fill K)) + refine (later_mono hsplit.1).trans ?_ + refine later_sep.1.trans ?_ + refine (sep_mono .rfl hwp).trans ?_ + refine (wp_frame_step_l' hval Std.LawfulSet.subset_refl).trans (wp_mono fun v' => ?_) + iintro ⟨HΔ, %hv, HP⟩ + subst hv + iapply hcont + iframe + +public theorem tac_wp_alloc [ι : HeapLangGS hlc GF] {Δ Δ' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {v : Val} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hcont : ∀ l : Loc, Δ' ∗ (l ↦ some v) ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#l))) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(ref(&v))) @ s ; E {{ Φ }} := by + refine hlater.trans ?_ + refine .trans ?_ (wp_bind (ProgramLogic.fill K)) + refine .trans ?_ (wand_entails (wp_alloc v _)) + exact later_mono <| forall_intro fun l => wand_intro (hcont l) + +public theorem tac_wp_free [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v : Val} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v)) + (hcont : Δ'' ⊢ WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#()))) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(free(#l))) @ s ; E {{ Φ }} := + tac_wp_heap_op rfl wp_free hlater hsplit (sep_elim_left.trans hcont) + +public theorem tac_wp_load [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {q} {v : Val} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦{q} some v)) + (hcont : Δ' ⊢ WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) v)) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(!v(#l))) @ s ; E {{ Φ }} := by + refine hlater.trans ?_ + refine .trans ?_ (wp_bind (ProgramLogic.fill K)) + iapply wand_apply (wand_entails (wp_load _)) + refine .trans ?_ later_sep.1 + refine later_mono ?_ + refine hsplit.1.trans ?_ + refine .trans sep_comm.mp ?_ + exact sep_mono .rfl (wand_intro (hsplit.2.trans hcont)) + +public theorem tac_wp_store [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v' : Val} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v)) + (hcont : Δ'' ∗ (l ↦ some v') ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#()))) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(v(#l) ← &v')) @ s ; E {{ Φ }} := by + refine hlater.trans ?_ + refine .trans ?_ (wp_bind (ProgramLogic.fill K)) + iapply wand_apply (wand_entails (wp_store _)) + refine .trans ?_ later_sep.1 + refine later_mono ?_ + refine hsplit.1.trans ?_ + refine .trans sep_comm.mp ?_ + exact sep_mono .rfl (wand_intro hcont) + +public theorem tac_wp_xchg [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v' : Val} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v)) + (hcont : Δ'' ∗ (l ↦ some v') ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) v)) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(xchg(#l, &v'))) @ s ; E {{ Φ }} := + tac_wp_heap_op rfl wp_xchg hlater hsplit hcont + +public theorem tac_wp_cmpXchg_fail [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {q} {v v1 v2 : Val} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦{q} some v)) + (hne : v ≠ v1) (hsafe : v.compareSafe v1) + (hcont : Δ' ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val((&v, #false)))) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(cmpXchg(v(#l), v(&v1), v(&v2)))) @ s ; E {{ Φ }} := + tac_wp_heap_op rfl (wp_cmpXchg_fail rfl rfl hsafe (decide_eq_false hne)) hlater hsplit + (hsplit.2.trans hcont) + +public theorem tac_wp_cmpXchg_suc [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v1 v2 : Val} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v)) + (heq : v = v1) (hsafe : v.compareSafe v1) + (hcont : Δ'' ∗ (l ↦ some v2) ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val((&v, #true)))) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(cmpXchg(v(#l), v(&v1), v(&v2)))) @ s ; E {{ Φ }} := + tac_wp_heap_op rfl (wp_cmpXchg_true rfl rfl hsafe (decide_eq_true heq)) hlater hsplit hcont + +public theorem tac_wp_cmpXchg [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v1 v2 : Val} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v)) + (hsafe : v.compareSafe v1) + (hsuc : v = v1 → Δ'' ∗ (l ↦ some v2) ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val((&v, #true)))) @ s ; E {{ Φ }}) + (hfail : v ≠ v1 → Δ' ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val((&v, #false)))) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(cmpXchg(v(#l), v(&v1), v(&v2)))) @ s ; E {{ Φ }} := + if heq : v = v1 then tac_wp_cmpXchg_suc hlater hsplit heq hsafe (hsuc heq) + else tac_wp_cmpXchg_fail hlater hsplit heq hsafe (hfail heq) + +public theorem tac_wp_faa [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {z1 z2 : Int} {Φ} + (hlater : Δ ⊢ ▷ Δ') + (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some hl_val(#z1))) + (hcont : Δ'' ∗ (l ↦ some hl_val(#(z1 + z2))) ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#z1))) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(faa(#l, #z2))) @ s ; E {{ Φ }} := + tac_wp_heap_op rfl wp_faa hlater hsplit hcont + +-- TODO: port `tac_wp_allocN` once `array` and `wp_allocN` are ported + +/-! ## Shared machinery for the heap tactics -/ + +/-- Epilogue shared by the keep/consume heap tactics: fill the result value `r` back into +the evaluation context `K` and run `iWpFinish` over the continuation context `hyps`. Returns +the continuation proof typed against `fill K (Exp.ofVal r)`, so the caller's `assign` matches +the tac lemma's `hcont`. -/ +meta def finishHeapOp {u} {GF : Q(BundledGFunctors.{0, 0, 0})} {hlc : Q(HasLC)} + {prop : Q(Type u)} {bi : Q(BI $prop)} {ehyps : Q($prop)} + (hyps : Hyps bi ehyps) (ι : Q(IrisGS_gen $hlc Exp $GF)) + (s : Q(Stuckness)) (E : Q(CoPset)) (K : Q(List ECtxItem)) (r : Q(Val)) (Φ : Q(Val → $prop)) + (_hu : QuotedLevelDefEq u 0 := ⟨⟩) (_hprop : $prop =Q IProp $GF := ⟨⟩) + (κ : Q(Wp $prop Exp Val Stuckness) := q(wp.def)) (_hwp : $κ =Q wp.def := ⟨⟩) : + ProofModeM Q($ehyps ⊢ Wp.wp (self := $κ) $s $E (ProgramLogic.fill $K (Exp.ofVal $r)) $Φ) := do + let ⟨inner, .up _⟩ ← HeapLang.fillQ K q(Exp.ofVal $r) + iWpFinish hyps ι s E inner Φ (κ := κ) + +/-- The points-to hypothesis located by `lookupPointsTo` for location `l` +in the (later-stripped) context `eΔ'`, together with the pruned context `eΔ''`/`hyps''` and +the splitting proof `pfSplit`, whose type is already recast to the `pointsTo` shape that the +`tac_wp_*` lemmas expect. -/ +structure PointsToLookup {u : Level} {GF : Q(BundledGFunctors.{0, 0, 0})} + {hlc : Q(HasLC)} (hgs : Q(HeapLangGS $hlc $GF)) {prop : Q(Type u)} (bi : Q(BI $prop)) + (eΔ' : Q($prop)) (l : Q(Loc)) (dq : Q(DFrac)) (hu : QuotedLevelDefEq u 0) + (hprop : $prop =Q IProp $GF) where + /-- The value stored at `l`. -/ + v : Q(Val) + /-- The user-facing name of the found hypothesis. -/ + name : Name + /-- The `IVarId` of the found hypothesis. -/ + vid : IVarId + /-- The context with the points-to hypothesis removed. -/ + eΔ'' : Q($prop) + hyps'' : @Hyps u prop bi eΔ'' + /-- The split certificate, recast to the shape the `tac_wp_*` lemmas expect. -/ + pfSplit : Q($eΔ' ⊣⊢ $eΔ'' ∗ pointsTo $l $dq (some $v)) + +/-- Locate and remove a spatial hypothesis `l ↦{dq} some v`. +Reading operations pass a fresh metavariable, which the lookup assigns to whatever +fraction is found and the lemmas' `↦{q}` implicit then picks up. +Throws if no matching hypothesis exists. -/ +meta def lookupPointsTo {u} {GF : Q(BundledGFunctors.{0, 0, 0})} {hlc : Q(HasLC)} + {prop : Q(Type u)} {bi : Q(BI $prop)} {eΔ' : Q($prop)} + (tacName : Name) (mvar : MVarId) (hgs : Q(HeapLangGS $hlc $GF)) + (hyps' : Hyps bi eΔ') (l : Q(Loc)) (dq : Q(DFrac)) + (hu : QuotedLevelDefEq u 0 := ⟨⟩) + (hprop : $prop =Q IProp $GF := ⟨⟩) : + ProofModeM (@PointsToLookup u GF hlc hgs prop bi eΔ' l dq hu hprop) := do + let some ⟨⟨v, name, vid⟩, eΔ'', hyps'', _, _, _, _, pf⟩ ← + hyps'.removeG false fun name vid p ty => do + -- ignore intuitionistic hyps + if isTrue p then return none + have ty : Q(IProp $GF) := ty + -- destructure ty to get the location l', fraction dq' and stored value v + let ~q(pointsTo $l' $dq' (some $v)) := ty | return none + unless ← isDefEq l' l do return none + -- a literal `dq` rejects other fractions; a metavariable records the one found + unless ← isDefEq dq' dq do return none + return some ((v : Q(Val)), name, vid) + | throwTacticEx tacName mvar (if dq.isMVar + then m!"cannot find a points-to hypothesis for location {l}" + else m!"cannot find a full-ownership points-to hypothesis for location {l}") + trace[wp_heap.lookup] "found {name} : pointsTo {l} ({dq}) (some {v})" + have pfSplit : Q($eΔ' ⊣⊢ $eΔ'' ∗ pointsTo $l $dq (some $v)) := pf + return { v, name, vid, eΔ'', hyps'', pfSplit } + +/-- The goal handed to a heap tactic by `ProofModeM.runTacticHeapWp`: `WpGoal` fields, +plus the `HeapLangGS` instance `hgs` extracted from the goal's `IrisGS_gen`, and the +context `hyps'`/`eΔ'` after stripping the WP's step modality, with `pfLater` witnessing +the strip. -/ +structure HeapWpGoal extends WpGoal where + hgs : Q(HeapLangGS $hlc $GF) + {eΔ' : Q($prop)} + hyps' : @Hyps u prop bi eΔ' + pfLater : Q($ehyps ⊢ (modality_laterN 1).M $eΔ') + hι : $ι =Q @HeapLang $hlc $GF $hgs + +/-- Shared prologue for the heap tactics: run the tactic on a WP goal, check that it is a +HeapLang WP (from the `HeapLangGS` instance), and strip the WP's step modality +off the hypotheses. -/ +meta def runTacticHeapWp {α} (tacName : Name) + (k : MVarId → HeapWpGoal → ProofModeM α) : TacticM α := do + -- Rocq parity: every heap tactic first normalizes pure redexes + evalTactic (← `(tactic| wp_pures)) + ProofModeM.runTacticWp fun mvar {hyps, GF, hlc, ι, s, E, e, Φ, hu, hprop, hbi, ..} => do + have ιQ : Q(IrisGS_gen $hlc Exp $GF) := ι + let ~q(@HeapLang _ _ $hgs) := ιQ + | throwTacticEx tacName mvar "the goal is not a HeapLang WP" + trace[wp_heap] "{tacName}: e = {e}" + -- currently specialized to later (no twp exists yet) + let ⟨_, hyps', pfLater⟩ ← iModAction hyps q(modality_laterN 1) + k mvar { hyps, ι, s, E, e, Φ, hu, hprop, hbi, hgs, hyps', pfLater, hι := ⟨⟩ } + +/-! ## The heap tactics -/ + +elab "wp_load" : tactic => + runTacticHeapWp `wp_load fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := l, K, ..} ← findECtx e fun e' => do + let ~q(Exp.load (Exp.ofVal (Val.lit (BaseLit.loc $l)))) := e' | failure + return l + | throwTacticEx `wp_load mvar "cannot find a `load` redex" + trace[wp_heap.redex] "load {l}; K = {K}" + + -- find `l ↦{dq} some v` in the spatial context and extract `dq` + let dq ← mkFreshExprMVarQ q(DFrac) + let ⟨v, _, _, _, _, pfSplit⟩ ← lookupPointsTo `wp_load mvar hgs hyps' l dq + + -- fill the loaded value back into `K` and finish the continuation + -- (over `hyps'`: the points-to hypothesis is kept) + let pfCont ← finishHeapOp hyps' ι s E K v Φ + + mvar.assign q(tac_wp_load (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) + +elab "wp_store" : tactic => + runTacticHeapWp `wp_store fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := (l, v'), K, ..} ← findECtx e fun e' => do + let ~q(Exp.store (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v')) := e' | failure + return (l, v') + | throwTacticEx `wp_store mvar "cannot find a `store` redex" + trace[wp_heap.redex] "store {l} ← {v'}; K = {K}" + + -- find and remove `l ↦ some v` (stores need full ownership) + let ⟨_, name, vid, _, hyps'', pfSplit⟩ ← + lookupPointsTo `wp_store mvar hgs hyps' l q(DFrac.own 1) + + let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v')) + + let pfCont ← finishHeapOp hyps''' ι s E K q(hl_val(#())) Φ + + mvar.assign q(tac_wp_store (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) + +elab "wp_xchg" : tactic => + runTacticHeapWp `wp_xchg fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := (l, v'), K, ..} ← findECtx e fun e' => do + let ~q(Exp.xchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v')) := e' | failure + return (l, v') + | throwTacticEx `wp_xchg mvar "cannot find an `xchg` redex" + trace[wp_heap.redex] "xchg {l} ← {v'}; K = {K}" + + -- find and remove `l ↦ some v` (xchg writes, so it needs full ownership) + let ⟨v, name, vid, _, hyps'', pfSplit⟩ ← lookupPointsTo `wp_xchg mvar hgs hyps' l q(DFrac.own 1) + + let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v')) + + let pfCont ← finishHeapOp hyps''' ι s E K v Φ + + mvar.assign q(tac_wp_xchg (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) + +elab "wp_faa" : tactic => + runTacticHeapWp `wp_faa fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := (l, z2), K, ..} ← findECtx e fun e' => do + -- faa is only defined on integers + let ~q(Exp.faa (Exp.ofVal (Val.lit (BaseLit.loc $l))) + (Exp.ofVal (Val.lit (BaseLit.int $z2)))) := e' | failure + return (l, z2) + | throwTacticEx `wp_faa mvar "cannot find a `faa` redex" + trace[wp_heap.redex] "faa {l} += {z2}; K = {K}" + + -- find and remove `l ↦ some v` (faa writes, so it needs full ownership) + let ⟨v, name, vid, eΔ'', hyps'', pfSplit⟩ ← + lookupPointsTo `wp_faa mvar hgs hyps' l q(DFrac.own 1) + + -- check that the points-to value is an integer (FAA requirement) + let ~q(Val.lit (BaseLit.int $z1)) := v + | throwTacticEx `wp_faa mvar + m!"the points-to hypothesis for location {l} does not store an integer" + have pfSplit : Q($eΔ' ⊣⊢ $eΔ'' ∗ + pointsTo $l (DFrac.own 1) (some (Val.lit (BaseLit.int $z1)))) := pfSplit + + let hyps''' := hyps''.add bi name vid q(false) + q(pointsTo $l (DFrac.own 1) (some (Val.lit (BaseLit.int ($z1 + $z2))))) + + let pfCont ← finishHeapOp hyps''' ι s E K q(Val.lit (BaseLit.int $z1)) Φ + + mvar.assign q(tac_wp_faa (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) + +elab "wp_cmpxchg_suc" : tactic => + runTacticHeapWp `wp_cmpxchg_suc fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do + let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) + (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure + return (l, v1, v2) + | throwTacticEx `wp_cmpxchg_suc mvar "cannot find a `cmpXchg` redex" + trace[wp_heap.redex] "cmpXchg {l}: {v1} → {v2}; K = {K}" + + -- find and remove `l ↦ some v` (a successful cmpXchg writes, so full ownership) + let ⟨v, name, vid, _, hyps'', pfSplit⟩ ← + lookupPointsTo `wp_cmpxchg_suc mvar hgs hyps' l q(DFrac.own 1) + + -- check safety, don't throw hard error to match Rocq behavior + let pfSafe ← iSolveSidecondition q(($v).compareSafe $v1 = true) (failOnUnsolved := false) + + -- check equality, don't throw hard error to match Rocq behavior + let pfEq ← iSolveSidecondition q($v = $v1) (failOnUnsolved := false) + + let hyps''' := hyps''.add bi name vid q(false) + q(pointsTo $l (DFrac.own 1) (some $v2)) + + let pfCont ← finishHeapOp hyps''' ι s E K + q(Val.pair $v (Val.lit (BaseLit.bool true))) Φ + + mvar.assign + q(tac_wp_cmpXchg_suc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfEq $pfSafe $pfCont) + +elab "wp_cmpxchg_fail" : tactic => + runTacticHeapWp `wp_cmpxchg_fail fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do + let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) + (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure + return (l, v1, v2) + | throwTacticEx `wp_cmpxchg_fail mvar "cannot find a `cmpXchg` redex" + trace[wp_heap.redex] "cmpXchg {l}: {v1} → {v2}; K = {K}" + + -- any fraction suffices for a failing compare (the points-to is only read) + let dq ← mkFreshExprMVarQ q(DFrac) + let ⟨v, _, _, _, _, pfSplit⟩ ← lookupPointsTo `wp_cmpxchg_fail mvar hgs hyps' l dq + + -- check safety, don't throw hard error to match Rocq behavior + let pfSafe ← iSolveSidecondition q(($v).compareSafe $v1 = true) (failOnUnsolved := false) + + -- check equality, don't throw hard error to match Rocq behavior + let pfNeq ← iSolveSidecondition q($v ≠ $v1) (failOnUnsolved := false) + + let pfCont ← finishHeapOp hyps' ι s E K + q(Val.pair $v (Val.lit (BaseLit.bool false))) Φ + + mvar.assign + q(tac_wp_cmpXchg_fail (ι := $hgs) (Δ' := $eΔ') (v2 := $v2) + $pfLater $pfSplit $pfNeq $pfSafe $pfCont) + +elab "wp_cmpxchg" " as " h1:binderIdent " | " h2:binderIdent : tactic => + runTacticHeapWp `wp_cmpxchg fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do + let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) + (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure + return (l, v1, v2) + | throwTacticEx `wp_cmpxchg mvar "cannot find a `cmpXchg` redex" + trace[wp_heap.redex] "cmpXchg {l}: {v1} → {v2}; K = {K}" + + -- find and remove `l ↦ some v` (the success branch writes, so full ownership) + let ⟨v, name, vid, eΔ'', hyps'', pfSplit⟩ ← + lookupPointsTo `wp_cmpxchg mvar hgs hyps' l q(DFrac.own 1) + + let hypsSuc := hyps''.add bi name vid q(false) + q(pointsTo $l (DFrac.own 1) (some $v2)) + + -- check safety, don't throw hard error to match Rocq behavior + let pfSafe ← iSolveSidecondition q(($v).compareSafe $v1 = true) (failOnUnsolved := false) + + let (sucName, _) ← getFreshName h1 + let pfSuc : Q($v = $v1 → ($eΔ'' ∗ pointsTo $l (DFrac.own 1) (some $v2) ⊢ + Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) + (Val.pair $v (Val.lit (BaseLit.bool true))))) $Φ)) ← + Qq.withLocalDeclDQ sucName q($v = $v1) fun _h => do + let ⟨innerSuc, .up _⟩ ← HeapLang.fillQ K + q(Exp.ofVal (Val.pair $v (Val.lit (BaseLit.bool true)))) + let pf ← iWpFinish hypsSuc ι s E innerSuc Φ + mkLambdaFVars #[_h] pf + + let (failName, _) ← getFreshName h2 + let pfFail : Q($v ≠ $v1 → $eΔ' ⊢ + Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) + (Val.pair $v (Val.lit (BaseLit.bool false))))) $Φ) ← + Qq.withLocalDeclDQ failName q($v ≠ $v1) fun _h => do + let ⟨innerFail, .up _⟩ ← HeapLang.fillQ K + q(Exp.ofVal (Val.pair $v (Val.lit (BaseLit.bool false)))) + let pf ← iWpFinish hyps' ι s E innerFail Φ + mkLambdaFVars #[_h] pf + + mvar.assign + q(tac_wp_cmpXchg (ι := $hgs) (Δ' := $eΔ') (v2 := $v2) + $pfLater $pfSplit $pfSafe $pfSuc $pfFail) + +elab "wp_free" : tactic => + runTacticHeapWp `wp_free fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := l, K, ..} ← findECtx e fun e' => do + let ~q(Exp.free (Exp.ofVal (Val.lit (BaseLit.loc $l)))) := e' | failure + return l + | throwTacticEx `wp_free mvar "cannot find a `free` redex" + trace[wp_heap.redex] "free {l}; K = {K}" + + -- find and remove `l ↦ some v` (freeing needs full ownership); the continuation + -- runs over the pruned context `hyps''` since the points-to is consumed + let ⟨_, _, _, _, hyps'', pfSplit⟩ ← lookupPointsTo `wp_free mvar hgs hyps' l q(DFrac.own 1) + + let pfCont ← finishHeapOp hyps'' ι s E K q(hl_val(#())) Φ + + mvar.assign q(tac_wp_free (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) + + +elab "wp_alloc" ppSpace loc:binderIdent " as " hyp:binderIdent : tactic => + runTacticHeapWp `wp_alloc fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := v, K, ..} ← findECtx e fun e' => do + let ~q(Exp.allocN (Exp.ofVal (Val.lit (BaseLit.int 1))) + (Exp.ofVal $v)) := e' | failure + return v + | throwTacticEx `wp_alloc mvar "cannot find a `ref` alloc" + trace[wp_heap.redex] "ref {v}; K = {K}" + + -- get location name from tactic call + let (locName, _) ← getFreshName loc + + let pfCont : Q(∀ l : Loc, $eΔ' ∗ pointsTo l (DFrac.own 1) (some $v) ⊢ + Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) (Val.lit (BaseLit.loc l)))) $Φ) ← + Qq.withLocalDeclDQ locName q(Loc) fun l => do + let ⟨_, hyps''⟩ ← hyps'.addWithInfo bi hyp q(false) + q(pointsTo $l (DFrac.own 1) (some $v)) + + let ⟨inner, .up _⟩ ← HeapLang.fillQ K q(Exp.ofVal (Val.lit (BaseLit.loc $l))) + let pf ← iWpFinish hyps'' ι s E inner Φ + mkLambdaFVars #[l] pf + + mvar.assign q(tac_wp_alloc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfCont) + +macro "wp_alloc" ppSpace loc:binderIdent : tactic => `(tactic| wp_alloc $loc as _) + +-- Register the trace classes emitted by the tactics above; enables +-- `set_option trace.wp_bind true` (and analogously for the others). initialize registerTraceClass `wp_bind initialize registerTraceClass `wp_pure +initialize registerTraceClass `wp_heap +initialize registerTraceClass `wp_heap.redex (inherited := true) +initialize registerTraceClass `wp_heap.lookup (inherited := true) diff --git a/Iris/Iris/Tests/HeapLang.lean b/Iris/Iris/Tests/HeapLang.lean index af432f07a..2acd7f17e 100644 --- a/Iris/Iris/Tests/HeapLang.lean +++ b/Iris/Iris/Tests/HeapLang.lean @@ -2,4 +2,5 @@ module public import Iris.Tests.HeapLang.Notation public import Iris.Tests.HeapLang.WeakestPre +public import Iris.Tests.HeapLang.HeapTactics public import Iris.Tests.HeapLang.Linter diff --git a/Iris/Iris/Tests/HeapLang/HeapTactics.lean b/Iris/Iris/Tests/HeapLang/HeapTactics.lean new file mode 100644 index 000000000..417057992 --- /dev/null +++ b/Iris/Iris/Tests/HeapLang/HeapTactics.lean @@ -0,0 +1,453 @@ +/- +Copyright (c) 2026 Klaus Kraßnitzer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Klaus Kraßnitzer +-/ +module + +public import Iris.BI +public import Iris.Instances +public import Iris.HeapLang.Notation +public import Iris.HeapLang.ProofMode +public import Iris.HeapLang.Instances +public import Iris.ProgramLogic.WeakestPre + +/-! Tests for the heap-operation tactics (`wp_load`, ...). Unlike the tests in +`Tests.HeapLang.WeakestPre`, these need the `IrisGS_gen` instance to be the one +derived from `HeapLangGS`, so no generic `IrisGS_gen` variable is in scope. -/ + +namespace Iris.HeapLang + +variable {hlc} {GF : BundledGFunctors} [ι : HeapLangGS hlc GF] +variable {s : Stuckness} {E : CoPset} {Φ : Val → IProp GF} + +section wp_load + +example {l : Loc} {v : Val} : + (l ↦ some v) ∗ ((l ↦ some v) -∗ Φ v) ⊢ WP hl(!v(#l)) @ s ; E {{ Φ }} := by + iintro ⟨Hpt, HΦ⟩ + wp_load + imodintro + iapply HΦ $$ Hpt + +-- with a ▷ on the points-to and the load inside an evaluation context +example {l l' : Loc} : + ▷ (l ↦ some hl_val(#2)) ∗ ▷ (l' ↦ some hl_val(#3)) ⊢ + WP hl(#1 + !v(#l)) @ s ; E {{ w, ⌜w = hl_val(#3)⌝ ∗ (l ↦ some hl_val(#2)) }} := by + iintro ⟨Hpt, Hpt'⟩ + wp_load + wp_binop + imodintro + iframe Hpt + ipureintro + rfl + +-- `wp_load` accepts *fractional* ownership (where store/faa/free would reject) +example {l : Loc} {dq : DFrac} {v : Val} : + (l ↦{dq} some v) ∗ ((l ↦{dq} some v) -∗ Φ v) ⊢ WP hl(!v(#l)) @ s ; E {{ Φ }} := by + iintro ⟨Hl, HΦ⟩ + wp_load + imodintro + iapply HΦ $$ Hl + +/-- +error: Tactic `wp_load` failed: cannot find a points-to hypothesis for location l + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ : Val → IProp GF +l l' : Loc +v : Val +⊢ + ∗Hpt : l' ↦ some v + ⊢ WP hl(!#l) @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {l l' : Loc} {v : Val} : + (l' ↦ some v) ⊢ WP hl(!v(#l)) @ s ; E {{ Φ }} := by + iintro Hpt + wp_load + +/-- +error: Tactic `wp_load` failed: cannot find a `load` redex + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ : Val → IProp GF +l : Loc +v v' : Val +⊢ + ∗Hpt : l ↦ some v + ⊢ WP hl(#l ← v(&v')) @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {l : Loc} {v v' : Val} : + (l ↦ some v) ⊢ WP hl(v(#l) ← &v') @ s ; E {{ Φ }} := by + iintro Hpt + wp_load + +end wp_load + +section wp_store + +example {l : Loc} {v v' : Val} : + (l ↦ some v) ∗ ((l ↦ some v') -∗ Φ hl_val(#())) ⊢ WP hl(v(#l) ← &v') @ s ; E {{ Φ }} := by + iintro ⟨Hpt, HΦ⟩ + wp_store + imodintro + iapply HΦ $$ Hpt + +-- `wp_store` must pick the `l` points-to and leave the `l'` one untouched +example {l l' : Loc} {v v' w : Val} : + (l ↦ some v) ∗ (l' ↦ some w) ⊢ + WP hl(v(#l) ← &v') @ s ; E {{ _r, (l ↦ some v') ∗ (l' ↦ some w) }} := by + iintro ⟨Hl, Hl'⟩ + wp_store + imodintro + iframe + +example {l : Loc} {v v' v'' : Val} : + (l ↦ some v) ⊢ + WP hl(if #true then (v(#l) ← &v') else (v(#l) ← &v'')) @ s ; E + {{ _r, l ↦ some v' }} := by + iintro Hpt + wp_store + imodintro + iframe + +/-- +error: Tactic `wp_store` failed: cannot find a full-ownership points-to hypothesis for location l + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ : Val → IProp GF +l : Loc +dq : DFrac +v v' : Val +⊢ + ∗Hpt : l ↦{dq} some v + ⊢ WP hl(#l ← v(&v')) @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {l : Loc} {dq : DFrac} {v v' : Val} : + (l ↦{dq} some v) ⊢ WP hl(v(#l) ← &v') @ s ; E {{ Φ }} := by + iintro Hpt + wp_store + +end wp_store + +section wp_faa + +example {l : Loc} {z1 z2 : Int} : + (l ↦ some hl_val(#z1)) ∗ ((l ↦ some hl_val(#(z1 + z2))) -∗ Φ hl_val(#z1)) ⊢ + WP hl(faa(#l, #z2)) @ s ; E {{ Φ }} := by + iintro ⟨Hpt, HΦ⟩ + wp_faa + imodintro + iapply HΦ $$ Hpt + +-- `wp_faa` buried in an evaluation context (`#1 + •`), with a `▷` on the points-to +example {l : Loc} {z : Int} : + ▷ (l ↦ some hl_val(#z)) ⊢ + WP hl(#1 + faa(#l, #2)) @ s ; E + {{ w, ⌜w = hl_val(#((1 : Int) + z))⌝ ∗ l ↦ some hl_val(#(z + (2 : Int))) }} := by + iintro Hl + wp_faa + wp_binop + imodintro + iframe + ipureintro + rfl + +-- `wp_faa` failing: writes need full ownership, fractional is rejected +/-- +error: Tactic `wp_faa` failed: cannot find a full-ownership points-to hypothesis for location l + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ : Val → IProp GF +l : Loc +dq : DFrac +z : Int +⊢ + ∗Hpt : l ↦{dq} some hl_val(#z) + ⊢ WP hl(faa(#l, #1)) @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {l : Loc} {dq : DFrac} {z : Int} : + (l ↦{dq} some hl_val(#z)) ⊢ WP hl(faa(#l, #1)) @ s ; E {{ Φ }} := by + iintro Hpt + wp_faa + +-- `wp_faa` failing: the stored value must be an integer literal +/-- +error: Tactic `wp_faa` failed: the points-to hypothesis for location l does not store an integer + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ : Val → IProp GF +l : Loc +v : Val +⊢ + ∗Hpt : l ↦ some v + ⊢ WP hl(faa(#l, #1)) @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {l : Loc} {v : Val} : + (l ↦ some v) ⊢ WP hl(faa(#l, #1)) @ s ; E {{ Φ }} := by + iintro Hpt + wp_faa + +end wp_faa + +section wp_xchg + +-- `xchg` returns the old value and stores the new one +example {l : Loc} {v v' : Val} : + (l ↦ some v) ∗ ((l ↦ some v') -∗ Φ v) ⊢ WP hl(xchg(#l, &v')) @ s ; E {{ Φ }} := by + iintro ⟨Hpt, HΦ⟩ + wp_xchg + imodintro + iapply HΦ $$ Hpt + +-- `wp_xchg` under a `▷`, returning the old value +example {l : Loc} {v v' : Val} : + ▷ (l ↦ some v) ⊢ WP hl(xchg(#l, &v')) @ s ; E {{ w, ⌜w = v⌝ ∗ l ↦ some v' }} := by + iintro Hl + wp_xchg + imodintro + iframe + ipureintro + rfl + +-- `wp_xchg` failing: writes need full ownership, fractional is rejected +/-- +error: Tactic `wp_xchg` failed: cannot find a full-ownership points-to hypothesis for location l + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ : Val → IProp GF +l : Loc +dq : DFrac +v v' : Val +⊢ + ∗Hpt : l ↦{dq} some v + ⊢ WP hl(xchg(#l, v(&v'))) @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {l : Loc} {dq : DFrac} {v v' : Val} : + (l ↦{dq} some v) ⊢ WP hl(xchg(#l, &v')) @ s ; E {{ Φ }} := by + iintro Hpt + wp_xchg + +end wp_xchg + +section wp_free + +-- `free` consumes the points-to (its resource is gone in the continuation) +example {l : Loc} {v : Val} : + (l ↦ some v) ∗ Φ hl_val(#()) ⊢ WP hl(free(#l)) @ s ; E {{ Φ }} := by + iintro ⟨Hpt, HΦ⟩ + wp_free + imodintro + iexact HΦ + +-- `wp_free` on a `▷`-wrapped points-to, among several; the survivor stays +example {l l' : Loc} {v w : Val} : + ▷ (l ↦ some v) ∗ (l' ↦ some w) ⊢ + WP hl(free(#l)) @ s ; E {{ _r, l' ↦ some w }} := by + iintro ⟨Hl, Hl'⟩ + wp_free + imodintro + iframe + +-- `wp_free` failing: deallocation needs full ownership, fractional is rejected +/-- +error: Tactic `wp_free` failed: cannot find a full-ownership points-to hypothesis for location l + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ : Val → IProp GF +l : Loc +dq : DFrac +v : Val +⊢ + ∗Hpt : l ↦{dq} some v + ⊢ WP hl(free(#l)) @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {l : Loc} {dq : DFrac} {v : Val} : + (l ↦{dq} some v) ⊢ WP hl(free(#l)) @ s ; E {{ Φ }} := by + iintro Hpt + wp_free + +end wp_free + +section wp_alloc + +-- `alloc` produces a fresh `l ↦ some v`; `wp_alloc l as Hl` names both +example {v : Val} : + ⊢ WP hl(ref(&v)) @ s ; E {{ w, ∃ l : Loc, ⌜w = hl_val(#l)⌝ ∗ l ↦ some v }} := by + wp_alloc l as Hl + imodintro + iexists l + isplit + · ipureintro; rfl + · iexact Hl + +-- anonymous variant: `wp_alloc l` auto-names the points-to; `iframe` picks it up +example {v : Val} : + ⊢ WP hl(ref(&v)) @ s ; E {{ w, ∃ l : Loc, ⌜w = hl_val(#l)⌝ ∗ l ↦ some v }} := by + wp_alloc l + imodintro + iexists l + iframe + ipureintro + rfl + +end wp_alloc + +section wp_cmpxchg_suc + +-- concrete equal values: the `v = v1` and `compareSafe` side conditions are +-- discharged automatically, the slot is updated to `v2`, result is `(v, #true)` +example {l : Loc} {v2 : Val} : + ▷ (l ↦ some hl_val(#1)) ⊢ + WP hl(cmpXchg(v(#l), v(#1), &v2)) @ s ; E + {{ w, ⌜w = hl_val((#1, #true))⌝ ∗ l ↦ some v2 }} := by + iintro Hl + wp_cmpxchg_suc + imodintro + iframe + ipureintro + rfl + +-- `wp_cmpxchg_suc` failing: a successful CAS writes, so fractional is rejected +/-- +error: Tactic `wp_cmpxchg_suc` failed: cannot find a full-ownership points-to hypothesis for +location l + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ : Val → IProp GF +l : Loc +dq : DFrac +v2 : Val +⊢ + ∗Hl : l ↦{dq} some hl_val(#1) + ⊢ WP hl(cmpXchg(#l, #1, v(&v2))) @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {l : Loc} {dq : DFrac} {v2 : Val} : + (l ↦{dq} some hl_val(#1)) ⊢ + WP hl(cmpXchg(v(#l), v(#1), &v2)) @ s ; E {{ Φ }} := by + iintro Hl + wp_cmpxchg_suc + +end wp_cmpxchg_suc + +section wp_cmpxchg_fail + +-- distinct concrete values with *fractional* ownership: the points-to is only +-- read and kept at its fraction; result is `(v, #false)`. Both side conditions +-- (`≠` and `compareSafe`) are discharged automatically for concrete values. +example {l : Loc} {dq : DFrac} {v2 : Val} : + ▷ (l ↦{dq} some hl_val(#1)) ⊢ + WP hl(cmpXchg(v(#l), v(#2), &v2)) @ s ; E + {{ w, ⌜w = hl_val((#1, #false))⌝ ∗ l ↦{dq} some hl_val(#1) }} := by + iintro Hl + wp_cmpxchg_fail + imodintro + iframe + ipureintro + rfl + +end wp_cmpxchg_fail + +section wp_cmpxchg + +-- symbolic compare value: both continuations appear as goals, with the +-- (dis)equality introduced into the Lean context under the given names; +-- `compareSafe` is discharged since the stored value is an unboxed literal +example {l : Loc} {v1 : Val} : + ▷ (l ↦ some hl_val(#1)) ⊢ + WP hl(cmpXchg(v(#l), &v1, v(#7))) @ s ; E + {{ w, (⌜w = hl_val((#1, #true))⌝ ∗ l ↦ some hl_val(#7)) ∨ + (⌜w = hl_val((#1, #false))⌝ ∗ l ↦ some hl_val(#1)) }} := by + iintro Hl + wp_cmpxchg as Heq | Hne + · imodintro + ileft + iframe + ipureintro + rfl + · imodintro + iright + iframe + ipureintro + rfl + +end wp_cmpxchg + +section goal_shape + +-- heap tactics reject WPs over a non-HeapLang `IrisGS_gen` instance +/-- +error: Tactic `wp_load` failed: the goal is not a HeapLang WP + +hlc : HasLC +GF : BundledGFunctors +ι : HeapLangGS hlc GF +s : Stuckness +E : CoPset +Φ✝ : Val → IProp GF +hlc' : HasLC +GF' : BundledGFunctors +inst✝ : IrisGS_gen hlc' Exp GF' +e : Exp +Φ : Val → IProp GF' +⊢ + ⊢ WP e @ s ; E {{ Φ }} +-/ +#guard_msgs (whitespace := lax) in +example {hlc'} {GF' : BundledGFunctors} [IrisGS_gen hlc' Exp GF'] + {e : Exp} {Φ : Val → IProp GF'} : + ⊢ WP e @ s ; E {{ Φ }} := by + wp_load + +-- heap tactics reject goals that are not WPs at all +/-- +error: The goal P must be a WP +-/ +#guard_msgs (whitespace := lax) in +example {P : IProp GF} : P ⊢ P := by + iintro HP + wp_load + +end goal_shape + +end Iris.HeapLang From 8a5034d34916b002ba58d714e9b04c600ca9cec7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Klaus=20Kra=C3=9Fnitzer?= Date: Thu, 16 Jul 2026 17:17:04 +0200 Subject: [PATCH 2/3] refactor: use the heap tactics in the HeapLang libraries MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the manual heap-op sequences in Spawn, SpinLock, LandinsKnot, and Quicksort — wp_bind + iapply wp_ and their glue (rfl side goals, imodintro, wp_finish, the wp_wand postcondition adaptor and compareSafe simp battery around cmpXchg) — with the corresponding heap tactics. --- Iris/Iris/HeapLang/Lib/LandinsKnot.lean | 22 +++++++++------------- Iris/Iris/HeapLang/Lib/Quicksort.lean | 25 ++++++++++--------------- Iris/Iris/HeapLang/Lib/Spawn.lean | 15 +++++---------- Iris/Iris/HeapLang/Lib/SpinLock.lean | 24 ++++++++++-------------- 4 files changed, 34 insertions(+), 52 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/LandinsKnot.lean b/Iris/Iris/HeapLang/Lib/LandinsKnot.lean index 953f65a1c..72f85ecc5 100644 --- a/Iris/Iris/HeapLang/Lib/LandinsKnot.lean +++ b/Iris/Iris/HeapLang/Lib/LandinsKnot.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alex Bai, Klaus Kraßnitzer +-/ module public import Iris.Instances.Lib.Invariants @@ -37,17 +42,9 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F iintro !> %Φ ⟨#H, HP⟩ HQ wp_bind &landinsKnot _ wp_rec - wp_bind ref(_) - wp_pures - iapply wp_alloc - iintro !> %r Hr - wp_pures - wp_bind (_ ← _) - iapply wp_store $$ Hr - iintro !> Hr - wp_pures - iapply wp_load $$ Hr - iintro !> Hr + wp_alloc r as Hr + wp_store + wp_load imod inv_alloc landinN ⊤ _ $$ Hr with #Hinv ihave HQ : ▷ (∀ u, Q u v1 -∗ Φ u) $$ [HQ] · inext; iexact HQ @@ -58,8 +55,7 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F imod inv_acc $$ Hinv with ⟨Hr, Hcl⟩ simp only [CoPset.subseteq_top] imodintro - iapply wp_load $$ Hr - iintro !> Hr + wp_load imod Hcl $$ Hr iapply H $$ [HP] [$] iframe HP diff --git a/Iris/Iris/HeapLang/Lib/Quicksort.lean b/Iris/Iris/HeapLang/Lib/Quicksort.lean index a57c78bda..ada195e90 100644 --- a/Iris/Iris/HeapLang/Lib/Quicksort.lean +++ b/Iris/Iris/HeapLang/Lib/Quicksort.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros, Michael Sammler, Klaus Kraßnitzer +-/ module public import Iris.HeapLang.PrimitiveLaws @@ -115,9 +120,7 @@ theorem cons_spec x l ls Φ : WP hl(&cons #x &l) {{ Φ }} := by iintro Hl HΦ wp_rec; wp_pures - wp_bind ref(_) - iapply wp_alloc - iintro !> %l Hl + wp_alloc l wp_pures imodintro iapply HΦ @@ -142,9 +145,7 @@ theorem append_spec l1 ls1 l2 ls2 Φ : | cons x xs => icases isList_cons $$ Hl1 with ⟨%l, %tl, %heq, Hpt, Hl⟩ subst heq; wp_pures - wp_bind !_ - iapply wp_load $$ Hpt - iintro !> Hpt + wp_load wp_pures wp_bind &append _ _ iapply IH $$ Hl Hl2 @@ -177,9 +178,7 @@ theorem partition_spec x l ls Φ : simp only icases Hl with ⟨%_, %tl, %hl, Hpt, Hl⟩; subst hl wp_pures - wp_bind !_ - iapply wp_load $$ [$] - iintro !> Hpt + wp_load wp_pures wp_bind &partition _ _ iapply IH $$ Hl @@ -231,9 +230,7 @@ theorem quicksort_spec l ls Φ : dsimp only icases Hl with ⟨%l, %tl, %heq, Hpt, Hl⟩; subst heq wp_pures - wp_bind !_ - iapply wp_load $$ [$] - iintro !> Hpt + wp_load wp_pures wp_bind &partition _ _ iapply partition_spec $$ [$] @@ -317,9 +314,7 @@ theorem wp_checkSorted (v vacc : Val) (l : List Int) (Φ : Val → IProp GF) : icases isList_cons $$ H with ⟨%loc, %tlv, %heq, Hpt, Htl⟩ subst heq wp_pures - wp_bind !_ - iapply wp_load $$ Hpt - iintro !> Hpt + wp_load rcases hinv with rfl | ⟨va, rfl, hva⟩ · wp_pures iapply IH $$ %_ %tl %_ %((List.pairwise_cons.mp hsorted).2) diff --git a/Iris/Iris/HeapLang/Lib/Spawn.lean b/Iris/Iris/HeapLang/Lib/Spawn.lean index c8758eb27..da9241efa 100644 --- a/Iris/Iris/HeapLang/Lib/Spawn.lean +++ b/Iris/Iris/HeapLang/Lib/Spawn.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Zongyuan Liu +Authors: Zongyuan Liu, Klaus Kraßnitzer -/ module @@ -73,10 +73,7 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) : WP hl(&spawn &f) {{ Φ }} := by iintro !> %Φ Hf HΦ wp_rec - wp_bind ref(_) - wp_pures - iapply wp_alloc - iintro !> %l Hl + wp_alloc l as Hl imod token_alloc with ⟨%γ, Hγ⟩ iapply fupd_wp imod inv_alloc N ⊤ (spawnInv γ l Ψ) $$ [Hl] with #Hinv @@ -106,11 +103,10 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) : unfold spawnInv icases Hpt with ⟨%_, Hl, _⟩ imodintro - iapply wp_store $$ Hl - iintro !> Hpt + wp_store iapply Hclose inext - iexists _; iframe Hpt + iexists _; iframe Hl iright; iexists v; isplit · itrivial · iframe @@ -131,8 +127,7 @@ theorem join_spec (Ψ : Val → IProp GF) (l : Loc) : unfold spawnInv icases Hpt with ⟨%lv, Hl, Hcond⟩ imodintro - iapply wp_load $$ Hl - iintro !> Hl + wp_load icases Hcond with (%Heq | ⟨%w, %Heq, (HΨw | Hγ')⟩) <;> subst Heq · imod Hclose $$ [Hl] · inext diff --git a/Iris/Iris/HeapLang/Lib/SpinLock.lean b/Iris/Iris/HeapLang/Lib/SpinLock.lean index f632130c9..ecdca93da 100644 --- a/Iris/Iris/HeapLang/Lib/SpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/SpinLock.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Sammler, ayhon, Klaus Kraßnitzer +-/ module public import Iris.HeapLang.Lib.Lock @@ -85,8 +90,8 @@ theorem newlock_spec : iintro !> %Φ Hcont wp_rec imod token_alloc with ⟨%γ, Hγ⟩ - iapply wp_alloc - iintro !> %l Hpt + wp_alloc l as Hpt + imodintro iapply Hcont iintro %R %E HR imod inv_alloc spinlockN E (lockInv γ l R) $$ [Hpt HR Hγ] with H @@ -118,11 +123,7 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) : icases G1 with ⟨%b, Hpt, Hcond⟩ cases b · simp only [Bool.false_eq_true, ↓reduceIte] - iapply wp_wand $$ [Hpt] - · iapply wp_cmpXchg_true rfl rfl $$ Hpt <;> - simp [Val.compareSafe, Val.isUnboxed, BaseLit.isUnboxed] - iintro %v ⟨%Heq, Hpt⟩ - subst Heq + wp_cmpxchg_suc imod G2 $$ [Hpt] · iexists true simp only [↓reduceIte] @@ -134,11 +135,7 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) : simp only [↓reduceIte] iframe · simp only [↓reduceIte] - iapply wp_wand $$ [Hpt] - · iapply wp_cmpXchg_fail rfl rfl $$ Hpt <;> - simp [Val.compareSafe, Val.isUnboxed, BaseLit.isUnboxed] - iintro %v ⟨%Heq, Hpt⟩ - subst Heq + wp_cmpxchg_fail imod G2 $$ [Hpt] · iexists true simp only [↓reduceIte] @@ -187,8 +184,7 @@ theorem release_spec (γ : GName) (lk : Val) (R : IProp GF) : unfold lockInv imodintro icases G1 with ⟨%b, Hpt, Hcond⟩ - iapply wp_store $$ Hpt - iintro !> Hpt + wp_store imod G2 $$ [- Hcont] · inext iexists false From af2c03f5e74ec1b4d041252b10f00b13983675b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Klaus=20Kra=C3=9Fnitzer?= Date: Wed, 22 Jul 2026 21:17:39 +0200 Subject: [PATCH 3/3] refactor: consolidate the heap-tactic epilogue, adopt `with` syntax MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Address the review feedback on #521. finishHeapOp is now used by all nine heap tactics. The three sites that were left bespoke — cmpxchg's two branch continuations and wp_alloc's — build their continuation under a binder, which turned out not to obstruct the shared epilogue at all. It also takes the HeapLangGS instance instead of an opaque IrisGS_gen, pinning the WP instance to HeapLang at the iWpFinish call. That makes HeapWpGoal's hι bridge unnecessary, so it is gone. Two consequences: ι drops out of the tactics' destructuring patterns (as a Qq-registered local instance it shadowed hgs during synthesis), and the three continuations built under binders now spell the instance out in their type ascriptions, since those elaborate with no unifier to guide them. Tactic syntax follows Lean rather than Rocq for the introduced names: `wp_alloc l with H`, and `wp_cmpxchg with H1 H2` as a flat list in the style of `split_ifs`. Bare `wp_alloc l` is unchanged, and wp_cmpxchg still requires both names, matching Rocq in both cases. The name binders take colGt. Without it, omitting a name made the parser consume the next line's tactic as a binder name — `wp_cmpxchg with Heq` followed by `imodintro` bound the failure branch to the name `imodintro` and silently dropped the tactic. --- Iris/Iris/HeapLang/Lib/LandinsKnot.lean | 2 +- Iris/Iris/HeapLang/Lib/Spawn.lean | 2 +- Iris/Iris/HeapLang/Lib/SpinLock.lean | 2 +- Iris/Iris/HeapLang/ProofMode.lean | 80 +++++++++++------------ Iris/Iris/Tests/HeapLang/HeapTactics.lean | 6 +- 5 files changed, 46 insertions(+), 46 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/LandinsKnot.lean b/Iris/Iris/HeapLang/Lib/LandinsKnot.lean index 72f85ecc5..7a1c9e687 100644 --- a/Iris/Iris/HeapLang/Lib/LandinsKnot.lean +++ b/Iris/Iris/HeapLang/Lib/LandinsKnot.lean @@ -42,7 +42,7 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F iintro !> %Φ ⟨#H, HP⟩ HQ wp_bind &landinsKnot _ wp_rec - wp_alloc r as Hr + wp_alloc r with Hr wp_store wp_load imod inv_alloc landinN ⊤ _ $$ Hr with #Hinv diff --git a/Iris/Iris/HeapLang/Lib/Spawn.lean b/Iris/Iris/HeapLang/Lib/Spawn.lean index da9241efa..27bc366e7 100644 --- a/Iris/Iris/HeapLang/Lib/Spawn.lean +++ b/Iris/Iris/HeapLang/Lib/Spawn.lean @@ -73,7 +73,7 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) : WP hl(&spawn &f) {{ Φ }} := by iintro !> %Φ Hf HΦ wp_rec - wp_alloc l as Hl + wp_alloc l with Hl imod token_alloc with ⟨%γ, Hγ⟩ iapply fupd_wp imod inv_alloc N ⊤ (spawnInv γ l Ψ) $$ [Hl] with #Hinv diff --git a/Iris/Iris/HeapLang/Lib/SpinLock.lean b/Iris/Iris/HeapLang/Lib/SpinLock.lean index ecdca93da..d4b92e8cd 100644 --- a/Iris/Iris/HeapLang/Lib/SpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/SpinLock.lean @@ -90,7 +90,7 @@ theorem newlock_spec : iintro !> %Φ Hcont wp_rec imod token_alloc with ⟨%γ, Hγ⟩ - wp_alloc l as Hpt + wp_alloc l with Hpt imodintro iapply Hcont iintro %R %E HR diff --git a/Iris/Iris/HeapLang/ProofMode.lean b/Iris/Iris/HeapLang/ProofMode.lean index e13a0c2e0..25e27144c 100644 --- a/Iris/Iris/HeapLang/ProofMode.lean +++ b/Iris/Iris/HeapLang/ProofMode.lean @@ -521,19 +521,19 @@ public theorem tac_wp_faa [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} /-! ## Shared machinery for the heap tactics -/ -/-- Epilogue shared by the keep/consume heap tactics: fill the result value `r` back into -the evaluation context `K` and run `iWpFinish` over the continuation context `hyps`. Returns -the continuation proof typed against `fill K (Exp.ofVal r)`, so the caller's `assign` matches -the tac lemma's `hcont`. -/ +/-- Epilogue shared by the heap tactics: fill the result value `r` back into the evaluation +context `K` and run `iWpFinish` over the continuation context `hyps`. Returns the continuation +proof typed against `fill K (Exp.ofVal r)`, so the caller's `assign` matches the tac lemma's +`hcont`. -/ meta def finishHeapOp {u} {GF : Q(BundledGFunctors.{0, 0, 0})} {hlc : Q(HasLC)} {prop : Q(Type u)} {bi : Q(BI $prop)} {ehyps : Q($prop)} - (hyps : Hyps bi ehyps) (ι : Q(IrisGS_gen $hlc Exp $GF)) + (hyps : Hyps bi ehyps) (hgs : Q(HeapLangGS $hlc $GF)) (s : Q(Stuckness)) (E : Q(CoPset)) (K : Q(List ECtxItem)) (r : Q(Val)) (Φ : Q(Val → $prop)) (_hu : QuotedLevelDefEq u 0 := ⟨⟩) (_hprop : $prop =Q IProp $GF := ⟨⟩) (κ : Q(Wp $prop Exp Val Stuckness) := q(wp.def)) (_hwp : $κ =Q wp.def := ⟨⟩) : ProofModeM Q($ehyps ⊢ Wp.wp (self := $κ) $s $E (ProgramLogic.fill $K (Exp.ofVal $r)) $Φ) := do let ⟨inner, .up _⟩ ← HeapLang.fillQ K q(Exp.ofVal $r) - iWpFinish hyps ι s E inner Φ (κ := κ) + iWpFinish hyps q(@HeapLang $hlc $GF $hgs) s E inner Φ (κ := κ) /-- The points-to hypothesis located by `lookupPointsTo` for location `l` in the (later-stripped) context `eΔ'`, together with the pruned context `eΔ''`/`hyps''` and @@ -593,7 +593,6 @@ structure HeapWpGoal extends WpGoal where {eΔ' : Q($prop)} hyps' : @Hyps u prop bi eΔ' pfLater : Q($ehyps ⊢ (modality_laterN 1).M $eΔ') - hι : $ι =Q @HeapLang $hlc $GF $hgs /-- Shared prologue for the heap tactics: run the tactic on a WP goal, check that it is a HeapLang WP (from the `HeapLangGS` instance), and strip the WP's step modality @@ -609,12 +608,12 @@ meta def runTacticHeapWp {α} (tacName : Name) trace[wp_heap] "{tacName}: e = {e}" -- currently specialized to later (no twp exists yet) let ⟨_, hyps', pfLater⟩ ← iModAction hyps q(modality_laterN 1) - k mvar { hyps, ι, s, E, e, Φ, hu, hprop, hbi, hgs, hyps', pfLater, hι := ⟨⟩ } + k mvar { hyps, ι, s, E, e, Φ, hu, hprop, hbi, hgs, hyps', pfLater } /-! ## The heap tactics -/ elab "wp_load" : tactic => - runTacticHeapWp `wp_load fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + runTacticHeapWp `wp_load fun mvar {s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := l, K, ..} ← findECtx e fun e' => do let ~q(Exp.load (Exp.ofVal (Val.lit (BaseLit.loc $l)))) := e' | failure return l @@ -627,12 +626,12 @@ elab "wp_load" : tactic => -- fill the loaded value back into `K` and finish the continuation -- (over `hyps'`: the points-to hypothesis is kept) - let pfCont ← finishHeapOp hyps' ι s E K v Φ + let pfCont ← finishHeapOp hyps' hgs s E K v Φ mvar.assign q(tac_wp_load (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) elab "wp_store" : tactic => - runTacticHeapWp `wp_store fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + runTacticHeapWp `wp_store fun mvar {bi, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := (l, v'), K, ..} ← findECtx e fun e' => do let ~q(Exp.store (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v')) := e' | failure return (l, v') @@ -645,12 +644,12 @@ elab "wp_store" : tactic => let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v')) - let pfCont ← finishHeapOp hyps''' ι s E K q(hl_val(#())) Φ + let pfCont ← finishHeapOp hyps''' hgs s E K q(hl_val(#())) Φ mvar.assign q(tac_wp_store (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) elab "wp_xchg" : tactic => - runTacticHeapWp `wp_xchg fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + runTacticHeapWp `wp_xchg fun mvar {bi, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := (l, v'), K, ..} ← findECtx e fun e' => do let ~q(Exp.xchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v')) := e' | failure return (l, v') @@ -662,12 +661,12 @@ elab "wp_xchg" : tactic => let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v')) - let pfCont ← finishHeapOp hyps''' ι s E K v Φ + let pfCont ← finishHeapOp hyps''' hgs s E K v Φ mvar.assign q(tac_wp_xchg (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) elab "wp_faa" : tactic => - runTacticHeapWp `wp_faa fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + runTacticHeapWp `wp_faa fun mvar {bi, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := (l, z2), K, ..} ← findECtx e fun e' => do -- faa is only defined on integers let ~q(Exp.faa (Exp.ofVal (Val.lit (BaseLit.loc $l))) @@ -690,12 +689,12 @@ elab "wp_faa" : tactic => let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some (Val.lit (BaseLit.int ($z1 + $z2))))) - let pfCont ← finishHeapOp hyps''' ι s E K q(Val.lit (BaseLit.int $z1)) Φ + let pfCont ← finishHeapOp hyps''' hgs s E K q(Val.lit (BaseLit.int $z1)) Φ mvar.assign q(tac_wp_faa (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) elab "wp_cmpxchg_suc" : tactic => - runTacticHeapWp `wp_cmpxchg_suc fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + runTacticHeapWp `wp_cmpxchg_suc fun mvar {bi, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure @@ -716,14 +715,14 @@ elab "wp_cmpxchg_suc" : tactic => let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v2)) - let pfCont ← finishHeapOp hyps''' ι s E K + let pfCont ← finishHeapOp hyps''' hgs s E K q(Val.pair $v (Val.lit (BaseLit.bool true))) Φ mvar.assign q(tac_wp_cmpXchg_suc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfEq $pfSafe $pfCont) elab "wp_cmpxchg_fail" : tactic => - runTacticHeapWp `wp_cmpxchg_fail fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + runTacticHeapWp `wp_cmpxchg_fail fun mvar {s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure @@ -741,15 +740,16 @@ elab "wp_cmpxchg_fail" : tactic => -- check equality, don't throw hard error to match Rocq behavior let pfNeq ← iSolveSidecondition q($v ≠ $v1) (failOnUnsolved := false) - let pfCont ← finishHeapOp hyps' ι s E K + let pfCont ← finishHeapOp hyps' hgs s E K q(Val.pair $v (Val.lit (BaseLit.bool false))) Φ mvar.assign q(tac_wp_cmpXchg_fail (ι := $hgs) (Δ' := $eΔ') (v2 := $v2) $pfLater $pfSplit $pfNeq $pfSafe $pfCont) -elab "wp_cmpxchg" " as " h1:binderIdent " | " h2:binderIdent : tactic => - runTacticHeapWp `wp_cmpxchg fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do +-- `colGt` on the names keeps an omitted one from swallowing the next line's tactic +elab "wp_cmpxchg" " with" colGt ppSpace h1:binderIdent colGt ppSpace h2:binderIdent : tactic => + runTacticHeapWp `wp_cmpxchg fun mvar {bi, GF, hlc, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure @@ -769,22 +769,22 @@ elab "wp_cmpxchg" " as " h1:binderIdent " | " h2:binderIdent : tactic => let (sucName, _) ← getFreshName h1 let pfSuc : Q($v = $v1 → ($eΔ'' ∗ pointsTo $l (DFrac.own 1) (some $v2) ⊢ - Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) - (Val.pair $v (Val.lit (BaseLit.bool true))))) $Φ)) ← + Wp.wp (self := wp.def (ι := @HeapLang $hlc $GF $hgs)) $s $E + (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) + (Val.pair $v (Val.lit (BaseLit.bool true))))) $Φ)) ← Qq.withLocalDeclDQ sucName q($v = $v1) fun _h => do - let ⟨innerSuc, .up _⟩ ← HeapLang.fillQ K - q(Exp.ofVal (Val.pair $v (Val.lit (BaseLit.bool true)))) - let pf ← iWpFinish hypsSuc ι s E innerSuc Φ + let pf ← finishHeapOp hypsSuc hgs s E K + q(Val.pair $v (Val.lit (BaseLit.bool true))) Φ mkLambdaFVars #[_h] pf let (failName, _) ← getFreshName h2 let pfFail : Q($v ≠ $v1 → $eΔ' ⊢ - Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) - (Val.pair $v (Val.lit (BaseLit.bool false))))) $Φ) ← + Wp.wp (self := wp.def (ι := @HeapLang $hlc $GF $hgs)) $s $E + (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) + (Val.pair $v (Val.lit (BaseLit.bool false))))) $Φ) ← Qq.withLocalDeclDQ failName q($v ≠ $v1) fun _h => do - let ⟨innerFail, .up _⟩ ← HeapLang.fillQ K - q(Exp.ofVal (Val.pair $v (Val.lit (BaseLit.bool false)))) - let pf ← iWpFinish hyps' ι s E innerFail Φ + let pf ← finishHeapOp hyps' hgs s E K + q(Val.pair $v (Val.lit (BaseLit.bool false))) Φ mkLambdaFVars #[_h] pf mvar.assign @@ -792,7 +792,7 @@ elab "wp_cmpxchg" " as " h1:binderIdent " | " h2:binderIdent : tactic => $pfLater $pfSplit $pfSafe $pfSuc $pfFail) elab "wp_free" : tactic => - runTacticHeapWp `wp_free fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + runTacticHeapWp `wp_free fun mvar {s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := l, K, ..} ← findECtx e fun e' => do let ~q(Exp.free (Exp.ofVal (Val.lit (BaseLit.loc $l)))) := e' | failure return l @@ -803,13 +803,13 @@ elab "wp_free" : tactic => -- runs over the pruned context `hyps''` since the points-to is consumed let ⟨_, _, _, _, hyps'', pfSplit⟩ ← lookupPointsTo `wp_free mvar hgs hyps' l q(DFrac.own 1) - let pfCont ← finishHeapOp hyps'' ι s E K q(hl_val(#())) Φ + let pfCont ← finishHeapOp hyps'' hgs s E K q(hl_val(#())) Φ mvar.assign q(tac_wp_free (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont) -elab "wp_alloc" ppSpace loc:binderIdent " as " hyp:binderIdent : tactic => - runTacticHeapWp `wp_alloc fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do +elab "wp_alloc" colGt ppSpace loc:binderIdent " with" colGt ppSpace hyp:binderIdent : tactic => + runTacticHeapWp `wp_alloc fun mvar {bi, GF, hlc, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do let some {result := v, K, ..} ← findECtx e fun e' => do let ~q(Exp.allocN (Exp.ofVal (Val.lit (BaseLit.int 1))) (Exp.ofVal $v)) := e' | failure @@ -821,18 +821,18 @@ elab "wp_alloc" ppSpace loc:binderIdent " as " hyp:binderIdent : tactic => let (locName, _) ← getFreshName loc let pfCont : Q(∀ l : Loc, $eΔ' ∗ pointsTo l (DFrac.own 1) (some $v) ⊢ - Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) (Val.lit (BaseLit.loc l)))) $Φ) ← + Wp.wp (self := wp.def (ι := @HeapLang $hlc $GF $hgs)) $s $E + (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) (Val.lit (BaseLit.loc l)))) $Φ) ← Qq.withLocalDeclDQ locName q(Loc) fun l => do let ⟨_, hyps''⟩ ← hyps'.addWithInfo bi hyp q(false) q(pointsTo $l (DFrac.own 1) (some $v)) - let ⟨inner, .up _⟩ ← HeapLang.fillQ K q(Exp.ofVal (Val.lit (BaseLit.loc $l))) - let pf ← iWpFinish hyps'' ι s E inner Φ + let pf ← finishHeapOp hyps'' hgs s E K q(Val.lit (BaseLit.loc $l)) Φ mkLambdaFVars #[l] pf mvar.assign q(tac_wp_alloc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfCont) -macro "wp_alloc" ppSpace loc:binderIdent : tactic => `(tactic| wp_alloc $loc as _) +macro "wp_alloc" colGt ppSpace loc:binderIdent : tactic => `(tactic| wp_alloc $loc with _) -- Register the trace classes emitted by the tactics above; enables -- `set_option trace.wp_bind true` (and analogously for the others). diff --git a/Iris/Iris/Tests/HeapLang/HeapTactics.lean b/Iris/Iris/Tests/HeapLang/HeapTactics.lean index 417057992..12929f34e 100644 --- a/Iris/Iris/Tests/HeapLang/HeapTactics.lean +++ b/Iris/Iris/Tests/HeapLang/HeapTactics.lean @@ -306,10 +306,10 @@ end wp_free section wp_alloc --- `alloc` produces a fresh `l ↦ some v`; `wp_alloc l as Hl` names both +-- `alloc` produces a fresh `l ↦ some v`; `wp_alloc l with Hl` names both example {v : Val} : ⊢ WP hl(ref(&v)) @ s ; E {{ w, ∃ l : Loc, ⌜w = hl_val(#l)⌝ ∗ l ↦ some v }} := by - wp_alloc l as Hl + wp_alloc l with Hl imodintro iexists l isplit @@ -399,7 +399,7 @@ example {l : Loc} {v1 : Val} : {{ w, (⌜w = hl_val((#1, #true))⌝ ∗ l ↦ some hl_val(#7)) ∨ (⌜w = hl_val((#1, #false))⌝ ∗ l ↦ some hl_val(#1)) }} := by iintro Hl - wp_cmpxchg as Heq | Hne + wp_cmpxchg with Heq Hne · imodintro ileft iframe