feat: port HeapLang heap tactics#521
Conversation
Port the wp_pure wrapper tactic family from iris_heap_lang/proofmode.v: wp_lam, wp_let, wp_seq, wp_closure, wp_if, wp_if_true, wp_if_false, wp_proj, wp_inj, wp_pair, wp_unop, wp_binop, wp_op, wp_case, and wp_match. The Lean implementation follows the Rocq implementation with these tactics being thin wrappers around wp_pure. Raise the precedence of wp_pure's focus argument to hl_exp:10 mirroring wp_bind. At default precedence, e.g. `wp_pure <pat>; wp_lam` misparses the focus pattern instead of sequencing. Import PrimitiveLaws from HeapLang/ProofMode, since the wp_rec macro expands to an application of the wp_rec lemma defined there. Add a test section per tactic covering at least one successful and one failing case
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.
Replace the manual heap-op sequences in Spawn, SpinLock, LandinsKnot, and Quicksort — wp_bind + iapply wp_<op> 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.
|
I haven't read the code, but looking at the commit messages got me thinking, do we want to support a |
# Conflicts: # Iris/Iris/HeapLang/ProofMode.lean
Absolutely, this is also something I was wondering about. Happy to adapt it like that. |
| {eΔ' : Q($prop)} | ||
| hyps' : @Hyps u prop bi eΔ' | ||
| pfLater : Q($ehyps ⊢ (modality_laterN 1).M $eΔ') | ||
| hι : $ι =Q @HeapLang $hlc $GF $hgs |
There was a problem hiding this comment.
It is possible to get rid of this field, by providing the HeapLang instance at the iWpFinish call in finishHeapOp.
| 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 Φ |
There was a problem hiding this comment.
You should be able to use finishHeapOp here.
| 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 Φ |
| 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 Φ |
Agreed that we should use |
3 participants
Description
Stacked on #516, the comments below pertain to this PR.
Partially addresses #480
This PR ports the heap-operation half of
iris_heap_lang/proofmode.v: symbolic-execution tactics for the primitive heap operations, resolving points-to hypotheses from the spatial context. It involves two commits.The first commit adds the tactics:
wp_load,wp_store,wp_xchg,wp_faa,wp_free,wp_alloc, andwp_cmpxchg/wp_cmpxchg_suc/wp_cmpxchg_fail. Their signatures mirror the Rocq counterparts (wp_alloc l as H,wp_cmpxchg as H1 | H2). As in Rocq, every heap tactic first normalizes pure redexes.runTacticHeapWp(prologue:wp_pures, WP-goal parsing,HeapLangGSextraction, one-later strip),lookupPointsTo(theenvs_lookupanalogue), andfinishHeapOp(epilogue: refill the evaluation context, finish the continuation). The per-tactic bodies reduce to: match redex, look up, [possibly update], finish, assign.DFrac.own 1as theirtac_wp_*lemmas demand full ownership syntactically while the reading operations (wp_load,wp_cmpxchg_fail) pass a metavariable that records whatever fraction is found. This allows a dedicated error message for the tactics that do not need full-ownership points-tos.set_option trace.wp_heap truetraces the tactic invocations (trace.wp_heap.redex/trace.wp_heap.lookup).▷-stripping, fractional load, redexes inside evaluation contexts), and#guard_msgsnegatives locking the error messages.The second commit migrates the HeapLang libraries (
Spawn,SpinLock,LandinsKnot,Quicksort) to the new tactics.Remarks
wp_apply/wp_smart_applyare planned for a follow-up PR.wp_allocNneeds array definitions inderived_laws.v.The later-stripping is confined to a single call site in
runTacticHeapWp, should the step handling ofwpever change shape upstream.This is my first foray into Lean metaprogramming, so I would greatly appreciate feedback on Qq usage and helper factoring in particular.
AI disclosure: I used Claude Code (Opus 4.8 + Fable 5) to help navigate the codebase, get me started on metaprogramming, and write test boilerplate. All design decisions, the code, and the proofs were reviewed and are owned by me.
Checklist
authorssection of any appropriate files