Skip to content

Commit 123ff35

Browse files
Stevengreclaude
Stevengre
and
claude
committed
feat(cse): slotStore-based CSE skeleton with callee proof test
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>
1 parent 02bfc0b commit 123ff35

4 files changed

Lines changed: 921 additions & 0 deletions

File tree

‎docs/cse-spec.md‎

Lines changed: 364 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,364 @@
1+
# CSE (Compositional Symbolic Execution) Specification
2+
3+
## 1. Overview
4+
5+
CSE enables modular verification of MIR programs by:
6+
1. **Summarizing** callee functions as rewrite rules (pre-condition → post-condition)
7+
2. **Reusing** those summaries in caller proofs to skip re-executing callee internals
8+
9+
**Prerequisite**: This specification assumes the `slotStore` refactor (PR #1059), where runtime locals are stored in a global `<slotStore>` map keyed by stable slot handles, and `Value::Reference` uses `slotPlace(SLOT, projections)` instead of stack-relative offsets.
10+
11+
A summary is a **K rewrite rule** that matches a function call by name and rewrites it to the function's effect:
12+
13+
```k
14+
rule <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND, _SPAN)
15+
=> #setLocalValue(DEST, RET_VALUE) ~> #execBlockIdx(TARGET)
16+
</k>
17+
<slotStore> ... SLOT_A |-> VAL_A SLOT_B |-> VAL_B ... </slotStore>
18+
requires #functionName(FUNC) ==String "package::module::function_name"
19+
andBool PATH_CONSTRAINTS
20+
[priority(30)]
21+
```
22+
23+
This is structurally identical to how p-token cheatcodes work (e.g., `cheatcode_is_account`). CSE summaries are **automatically generated cheatcodes**.
24+
25+
## 2. Definitions
26+
27+
- **Callee proof**: A standalone proof of a function `f`, producing summaries
28+
- **Summary rule**: A K rewrite rule encoding one execution path of `f`
29+
- **Reachable slot set**: The set of slotStore entries reachable by following reference chains from `f`'s arguments
30+
- **Terminal value**: A value in slotStore that is not a Reference or PtrLocal (the end of a dereference chain)
31+
- **Caller proof**: A proof that uses summary rules instead of re-executing callee bodies
32+
- **Split**: A deterministic branch with mutually exclusive constraints (from `SwitchInt`)
33+
- **Cover**: A leaf node that is subsumed by the target node
34+
35+
## 3. Why slotStore Enables CSE
36+
37+
### 3.1 The Problem with Stack-Relative References (Pre-PR #1059)
38+
39+
Before slotStore, references encoded stack depth:
40+
```
41+
Reference(offset=2, place(local(3), proj), mut, meta)
42+
```
43+
- `#traverseProjection` needed `STACK[offset-1]` to dereference
44+
- Callee summaries were bound to a specific caller stack depth
45+
- Summaries could not be reused across different callers
46+
47+
### 3.2 Slot-Based References (Post-PR #1059)
48+
49+
After slotStore, references encode a global slot handle:
50+
```
51+
Reference(slotPlace(SLOT_ID, proj), mut, meta)
52+
```
53+
- `#traverseProjection` looks up `<slotStore>[SLOT_ID]` — no stack needed
54+
- `WriteTo` is `toSlot(SLOT_ID)` instead of `toStack(FRAME, LOCAL)`
55+
- `#adjustRef` (stack offset adjustment) is eliminated entirely
56+
57+
### 3.3 Consequence for CSE
58+
59+
Summary rules only need `<k>` and optionally `<slotStore>`:
60+
- No `<stack>` — push/pop is internal to the callee, invisible in the summary
61+
- No `<currentFrame>` — `#setLocalValue` internally resolves the caller's frame
62+
- No `<locals>` — replaced by slotStore
63+
64+
## 4. Summary Rule Format
65+
66+
### 4.1 Function Name Matching
67+
68+
Summary rules match by **function name**, not by `Ty` (type ID). This follows the cheatcode pattern:
69+
70+
```k
71+
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::get_account"
72+
```
73+
74+
Rationale: `Ty` is a monomorphization-specific key that may differ across compilations. Function names are stable identifiers.
75+
76+
### 4.2 Pure Function (No SlotStore Side Effects)
77+
78+
For functions that only read data through references and return a value:
79+
80+
```k
81+
rule [cse-get_account-path-1]:
82+
<k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND, _SPAN)
83+
=> #setLocalValue(DEST, RET_VALUE_1) ~> #execBlockIdx(TARGET)
84+
</k>
85+
<slotStore>
86+
...
87+
SLOT_A |-> typedValue(ACCT_INFO_VAL, TY_A, MUT_A)
88+
SLOT_B |-> typedValue(PAccountAccount(PACC, IAcc(MINT, OWNER, AMOUNT, DELEGATE, STATE, ...)), TY_B, MUT_B)
89+
...
90+
</slotStore>
91+
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::get_account"
92+
andBool STATE ==K accountStateInitialized
93+
[priority(30)]
94+
```
95+
96+
The `<slotStore>` appears without `=>` — it is read-only. The `...` on both sides enables partial map matching.
97+
98+
### 4.3 Function with Side Effects
99+
100+
For functions that modify data through `&mut` references:
101+
102+
```k
103+
rule [cse-set_delegate-path-1]:
104+
<k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND, _SPAN)
105+
=> #setLocalValue(DEST, RET_VALUE_1) ~> #execBlockIdx(TARGET)
106+
</k>
107+
<slotStore>
108+
...
109+
SLOT_B |-> (typedValue(OLD_ACCOUNT, TY_B, MUT_B) => typedValue(NEW_ACCOUNT, TY_B, MUT_B))
110+
...
111+
</slotStore>
112+
requires #functionName(FUNC) ==String "pinocchio_token_interface::state::account::Account::set_delegate"
113+
andBool PATH_CONSTRAINTS
114+
[priority(30)]
115+
```
116+
117+
Only the modified slots have `=>` rewrites. Unmodified slots are matched read-only or omitted entirely.
118+
119+
### 4.4 Reference Chain Resolution for Slot Selection
120+
121+
To determine which slots appear in a summary rule, follow the reference chain from each argument:
122+
123+
```
124+
Argument: operandCopy(place(local(I), proj))
125+
→ evaluates to Reference(slotPlace(SLOT_A, proj_a), ...)
126+
→ SLOT_A |-> typedValue(VAL_A, ...)
127+
→ if VAL_A contains Reference(slotPlace(SLOT_B, ...), ...)
128+
→ SLOT_B |-> typedValue(VAL_B, ...)
129+
→ if VAL_B is NOT a Reference/PtrLocal → STOP (terminal value)
130+
```
131+
132+
**Rule**: Follow references until reaching a non-reference value. All slots visited along the chain are included in the rule's `<slotStore>` pattern. This is the **reachable slot set**.
133+
134+
### 4.5 Variable Scoping
135+
136+
Summary rules must only reference:
137+
- Variables from the caller's argument operands (which resolve to slot handles)
138+
- SlotStore entries in the reachable slot set
139+
- Fresh variables for return values
140+
141+
Callee-internal variables (temporaries, inner locals) must be eliminated. They are not visible in the summary because:
142+
- Callee's `ownedSlots` are created by `setupCalleeData` and cleaned up on return
143+
- Only the callee's effects on pre-existing slots (via `&mut` references) persist
144+
145+
## 5. Callee Proof Requirements
146+
147+
### 5.1 Initial State
148+
149+
The callee proof starts from a **normalized** initial state:
150+
- Symbolic arguments matching the function signature
151+
- Standard callee setup (`setupCalleeData`)
152+
- Target set to `noBasicBlockIdx` (standalone callee)
153+
- Symbolic `<slotStore>` with entries for argument-reachable slots
154+
155+
### 5.2 Proof Completion
156+
157+
A callee proof is **complete** when all leaf nodes are **covers** (subsumed by target) and there are zero stuck nodes.
158+
159+
### 5.3 Extracting Summary Rules from Cover Paths
160+
161+
For each cover node `c` in the callee proof:
162+
1. Trace the path from `init` to `c` through the KCFG
163+
2. Collect all path constraints (from splits along the path)
164+
3. Extract the return value from the final state's `RETVAL_CELL` or `locals[0]`
165+
4. Diff the `<slotStore>` between init and final state to identify modified slots
166+
5. Generate a K rule with:
167+
- LHS: `#execTerminatorCall(_, FUNC, ...)` + slotStore pattern (reachable slots)
168+
- RHS: `#setLocalValue(DEST, RET_VALUE) ~> #execBlockIdx(TARGET)` + slotStore updates
169+
- `requires`: function name match + path constraints
170+
171+
### 5.4 No Cut-Points for Callee Proofs
172+
173+
Cut-point rules (e.g., `termReturnSome`, `termReturnNone`) must NOT be used. They block all returns including inner function returns.
174+
175+
## 6. Interaction with pyk APIs
176+
177+
### 6.1 Summary Rules via `add-module`
178+
179+
Summary rules are compiled K rules injected into the backend:
180+
181+
```python
182+
from pyk.kast.inner import KApply, KVariable, KRewrite, KToken
183+
from pyk.kast.outer import KRule, KFlatModule, KImport
184+
185+
# Build rule for each callee execution path
186+
rules = []
187+
for path in callee_paths:
188+
rule = KRule(
189+
body=KRewrite(lhs=..., rhs=...),
190+
requires=path.constraints,
191+
ensures=TRUE,
192+
att=KAtt({'priority': '30', 'label': f'cse-{callee_name}-path-{path.id}'}),
193+
)
194+
rules.append(rule)
195+
196+
# Inject as module
197+
module = KFlatModule(f'CSE-SUMMARY-{callee_name}', rules, [KImport('KMIR')])
198+
module_name = cterm_symbolic.add_module(module, name_as_id=True)
199+
```
200+
201+
The backend applies these rules automatically during execution. No `custom_step` needed for summary application.
202+
203+
### 6.2 When `custom_step` IS Needed
204+
205+
`custom_step` is only needed during the **gen phase** to:
206+
- Observe call sites and record argument patterns
207+
- Trigger callee proving on first encounter
208+
209+
During the **reuse phase**, `custom_step` is NOT used for summary application — the compiled rules handle it.
210+
211+
### 6.3 Split vs NDBranch
212+
213+
When multiple summary rules exist for the same function (one per execution path), the backend produces a **Split** because the rules have mutually exclusive `requires` clauses. This is the correct behavior — callee paths are deterministic branches.
214+
215+
`custom_step` must NOT return `NDBranch` for summary application.
216+
217+
## 7. Which Functions to Summarize
218+
219+
### 7.1 Selection Criteria
220+
221+
A function should be summarized if:
222+
1. It has a MIR body (not an intrinsic or extern)
223+
2. It is called by at least one function being verified
224+
3. It is "summary-worthy" (not a trivial std-lib wrapper)
225+
4. Its proof completes within reasonable bounds
226+
227+
### 7.2 Recursive Summarization
228+
229+
Functions are summarized bottom-up:
230+
1. Leaf functions (no further callees) are summarized first
231+
2. Their summaries are used to prove intermediate functions
232+
3. Intermediate functions are then summarized
233+
4. A function like `process_approve` CAN be summarized once its callees are
234+
235+
## 8. Correctness Criteria
236+
237+
### 8.1 Soundness
238+
239+
For each summary rule `pre => post requires C`:
240+
- Execution of `f` from states satisfying `C` must produce states subsumed by `post`
241+
- The union of all path constraints must cover all reachable inputs
242+
243+
### 8.2 Structure Preservation
244+
245+
When a caller proof uses summaries:
246+
- `reuse_splits == baseline_splits`
247+
- `reuse_covers == baseline_covers`
248+
- `reuse_stuck == 0`
249+
- `reuse_ndbranch == 0`
250+
251+
### 8.3 Completeness
252+
253+
A summary is complete if it covers all execution paths of the callee.
254+
255+
## 9. Implementation Phases
256+
257+
### Phase A: Single-Function Summaries as K Rules
258+
259+
1. Rebase CSE on PR #1059 (slotStore)
260+
2. Prove callee functions to completion (all covers)
261+
3. Extract pre/post state pairs, diff slotStore
262+
4. Generate K rewrite rules with function name matching and slot patterns
263+
5. Add rules via `add-module`
264+
6. Prove caller with summary rules active
265+
7. Verify: `reuse_splits == baseline_splits`, `reuse_passed == baseline_passed`
266+
267+
### Phase B: Multi-Level Composition
268+
269+
1. Summarize leaf functions first
270+
2. Use leaf summaries to prove and summarize intermediate functions
271+
3. Summary cache persists across the verification suite
272+
273+
### Phase C: Incremental Re-verification
274+
275+
1. When a callee changes, re-prove only that callee
276+
2. If summary is equivalent, no caller re-verification needed
277+
278+
## 10. Repository Structure and Branches
279+
280+
### 10.1 mir-semantics Repository
281+
282+
| Branch | Purpose | Base |
283+
|--------|---------|------|
284+
| `master` | Upstream baseline | — |
285+
| PR #1059 | slotStore refactor | `master` |
286+
| `feature/cse` | CSE feature | PR #1059 |
287+
| `feature/cse-p-token` | CSE + p-token cheatcodes | `feature/cse` + p-token |
288+
289+
**Branch policy**:
290+
- `feature/cse` must NOT contain p-token-specific rules
291+
- `feature/cse` is rebased on PR #1059
292+
- All CSE logic changes go to `feature/cse` first
293+
294+
### 10.2 solana-token Repository
295+
296+
| Branch | Purpose |
297+
|--------|---------|
298+
| `feature/cse-eval` | CSE evaluation harness |
299+
300+
### 10.3 Branch Sync Flow
301+
302+
```
303+
master ──> PR#1059 (slotStore) ──> feature/cse ──> feature/cse-p-token
304+
|
305+
(embedded in solana-token/feature/cse-eval)
306+
```
307+
308+
## 11. Validation and Acceptance Testing
309+
310+
### 11.1 Unit-Level Validation (mir-semantics)
311+
312+
**Test**: `test_prove[cse-multi-function]`
313+
314+
Validates:
315+
- CSE proof passes
316+
- Summary generated as K rules (not frontier configs)
317+
- Reuse produces Split (not NDBranch)
318+
- Structure matches baseline
319+
320+
### 11.2 Integration Validation (p-token)
321+
322+
**Hard acceptance criteria** (all must hold):
323+
324+
| # | Criterion | Failure meaning |
325+
|---|-----------|-----------------|
326+
| H1 | CSE reuse PASSES when baseline PASSES | Summary unsound |
327+
| H2 | `reuse_splits == baseline_splits` | Summary loses branches |
328+
| H3 | `reuse_stuck == 0` | Summary incomplete |
329+
| H4 | `reuse_ndbranch == 0` | Using NDBranch instead of Split |
330+
| H5 | Summary rules are K rules via `add-module` | Not compiled rules |
331+
| H6 | Callee proofs have covers, no stuck | Callee proof incomplete |
332+
333+
**Soft optimization targets**:
334+
335+
| # | Target | Goal |
336+
|---|--------|------|
337+
| S1 | Per-test speedup | > 1.0x |
338+
| S2 | Geomean speedup | > 3x |
339+
| S3 | Booster fast path | 100% |
340+
341+
### 11.3 Reproducer Tests
342+
343+
| Reproducer | Tests |
344+
|------------|-------|
345+
| `cse-multi-function.rs` | Basic summary gen + reuse |
346+
| `cse-branching-callee.rs` | Multiple paths → multiple rules → Split |
347+
| `cse-reference-args.rs` | Reference arguments, slotStore pattern matching |
348+
| `cse-side-effects.rs` | `&mut` reference modifications → slotStore diff |
349+
350+
## 12. Paper Artifacts
351+
352+
```bash
353+
cd ~/solana-token-cse-eval/p-token/test-properties
354+
python3 evaluate_cse.py --suite all
355+
```
356+
357+
Generates: `cse_evaluation_results.json`, `cse_paper_table.csv`, `cse_paper_table.tex`
358+
359+
## 13. Non-Goals (Current Scope)
360+
361+
- Loop summarization (loops are unrolled)
362+
- Concurrent/parallel verification
363+
- Summary inference from tests or specifications
364+
- Cross-crate summary sharing (summaries are per-SMIR)

0 commit comments

Comments
 (0)