feat: port HeapLang heap tactics#521
Open
kdvkrs wants to merge 3 commits into
Open
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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