feat: Compositional Symbolic Execution (CSE) on slotStore [WIP]#1065
Closed
feat: Compositional Symbolic Execution (CSE) on slotStore [WIP]#1065
Conversation
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Initial implementation of CSE on the slotStore branch (PR #1059): - _cse.py: clean CSE pipeline (callee proof, cover path extraction, summary rule generation, add-module reuse) - cse-simple-callee.rs: simple test program (double(x) = x + x) - test_cse_callee_proof: verifies callee proof completes with covers - cse-spec.md: full specification with slotStore-based design Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…tion - Rebuilt K definition cache to include slotStore cells (OWNEDSLOTS_CELL, SLOTSTORE_CELL, NEXTSLOT_CELL) - Fixed _extract_return_value: match full label name (return(_)_KMIR-CONFIGURATION_RetVal_Value) - Accept stuck nodes from overflow/error paths in callee proofs - test_cse_callee_proof PASSES: double(x) callee proof completes with 1 cover + 1 stuck (overflow), return value extracted Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Complete pipeline: callee proof → cover path extraction → summary rule generation via cterm_build_rule → add-module injection → caller reuse. Key implementation details: - Uses cterm_build_rule (same as APRProver dependency rules) for properly structured KRule with full config cell nesting - Rule LHS: #execTerminatorCall ~> CONT with function name constraint - Rule RHS: #setLocalValue(DEST, RET) ~> #continueAt(TARGET) - Summary injected via CTermSymbolic.add_module(), backend applies automatically — no custom_step needed - Test: double(x)=x+x, callee has 1 cover + 1 stuck (overflow), summary rule generated and reuse proof passes Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
All CSE tests pass with correct structure preservation: - cse-simple-callee.rs: double(x), 1 rule, baseline=reuse structure - cse-branching-callee.rs: classify(x) with if/else, 2 rules from 2 cover paths, reuse produces correct splits - cse-reference-args.rs: add_to(&x, y) with reference argument, slotStore-based reference handling works correctly Fix: sanitize module/rule names for Kore identifier requirements Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Verify in test_cse_callee_proof: - H4: no NDBranch in reuse proof (0 ndbranches) - H2: splits match baseline (reuse_splits == baseline_splits) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Migrate all cheatcode rules from old locals/stack-based Reference format to the new slotStore-based format (PR #1059): p-token.md: - PAccByteRef: (Int, Place, Mutability, Int) → (SlotPlace, Mutability, Int) - Remove #adjustRef for PAccByteRef (no stack offsets needed) - #mkPAccByteRef: resolve PtrLocal via slotStore instead of stack - #mkPAccByteRefLen: use SlotPlace instead of (Int, Place) - #mkPAccountRef: Reference/PtrLocal use slotPlace(SLOT, proj) spl-token.md: - #forceSetPlaceValue: <locals> → <ownedSlots> + <slotStore> - #traverseProjection write rules: toLocal → toSlot, toStack → removed - #setSPLBorrowData: Reference/PtrLocal use slotPlace(SLOT, proj) - #execSPLSolMemset: <locals> → <ownedSlots> in StackFrame Build passes (make build). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Simple u32-to-usize cast test to verify cast semantics work on the slotStore branch for basic cases. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…errors - Add requires/imports for KMIR-P-TOKEN and KMIR-SPL-TOKEN in kmir.md (same as feature/cse-p-token — modules must be in base def, not loaded as extra modules) - Remove obsolete #mapOffset simplification rule (removed with slotStore) - Fix Reference pattern in spl-token.md #initBorrow (old 4-arg → new 3-arg) Build passes. p-token baseline passes: 15 nodes, 3 splits, 4 covers. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
test_process_get_account_data_size with get_mint summary: H1: baseline=PASS, reuse=PASS H2: splits match (3 == 3) H3: stuck=0 H4: ndbranch=0 Structure: 15 nodes, 3 splits, 4 covers (identical) Key technique: pre-condition callee init state with PAccountMint symbolic values (matching p-token cheatcode output) instead of raw Aggregate bytes. This allows standalone callee proofs to succeed without the test harness cheatcode context. Also fixes: _cse.py init_subst parameter for custom init states. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- _prove_callee_with_deps: prove callee with dependency summary modules injected via add-module (e.g. is_initialized uses account_state summary) - _prove_and_summarize_callee: accepts dep_modules for multi-level - evaluate_cse_slotstore.py: Phase A (leaf getters with PAccount) then Phase B (intermediates with leaf summaries as deps) - Added INTERMEDIATE_CALLEES list: account_state, is_initialized, delegate, delegated_amount, is_native, amount, mint_authority, etc. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Proof IDs containing angle brackets (e.g. <Account as Initializable>) cause Kore module name errors. Use _sanitize_name() for proof_id. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Key finding: standalone add_module() registers rules but APRProver doesn't use them during execute() — it only uses the dependency module chain. Rules must be injected via APRProver(extra_module=...) which makes them part of the module chain used for execution. Also: cterm_build_rule makes RHS-only variables existential, which causes Kore parsing issues. Need to construct Kore axiom directly for proper summary rule injection. WIP: rule fires with wildcarded config but existential variable handling in pyk prevents correct result parsing. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Key fixes: - Use cheatcode rule body as template (cell wildcards _Gen1:RetValCell etc.) - Use APRProver(extra_module=merged_module) for rule injection - Clone template body and replace only <k> cell content - Patched pyk Id to accept # in Kore identifiers (Rule#Var...) Result: double(x) summary rule fires, depth 86 → 43 (50% reduction) Proof doesn't pass yet: existential ARG_UINT1 in return value is unbound (not connected to caller's actual argument). Need argument binding via operand matching. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Breakthrough: cheatcode template body + APRProver extra_module + correct return value = working CSE. Result on cse-simple-callee.rs (double(5)): Baseline: depth=86, passed=True Reuse: depth=36, passed=True (58% reduction) Key technique: clone cheatcode rule body (with _Gen cell wildcards), replace <k> cell with #execTerminatorCall → #setLocalValue + #continueAt. Use APRProver(extra_module=...) not standalone add_module(). Also added KMIR-CSE-SUPPORT module with #cseReturn helper for seqstrict operand evaluation. Next: automate return value extraction from callee proof. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Moved to fork: Stevengre/mir-semantics#30 |
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.
Summary
CSE implementation based on slotStore refactor (PR #1059). Resolves #1064.
Status: WIP — summary rules fire and reduce depth 58%, proof passes. Path constraints and slotStore effects not yet encoded.
What works
APRProver(extra_module=...)What's left
See #1064 for full details and
docs/cse-spec.mdfor spec.🤖 Generated with Claude Code