feat(walk): provekit-walk MVP — paper 07's machinery on Rust source (closes #368)#370
Merged
Conversation
…sed arrival mementos (#368) First operational implementation of paper 07's discipline: walk Rust source backward from each callsite to the chain's terminal allocation, building a parallel shadow AST where every node is a content-addressed memento. Architecture: - ShadowSource mirrors a syn::ItemFn structurally. One slot per body statement, one for the function-entry "before any statement" position. - Each slot carries N arrivals — one per callsite chain that propagated through this AST node. Sir's structural correction: any AST node can have N arrivals, where N = the number of distinct callsite chains whose backward WP propagation visits that node. - Each ShadowArrival is a content-addressed memento (canonical_bytes + BLAKE3-512 cid). The canonical bytes encode pre_wp → post_wp (the edge memento), the predecessor_cid (data-flow upstream link), and the allocation_cid (the chain's terminal allocation arrival's CID, null for the allocation itself). - The substitution algorithm uses Dijkstra-Hoare WP rules: wp(let x = e, P) = P[e/x]. Implemented in wp.rs with lambda/let shadowing respected. Mint order: arrivals are minted in REVERSE walk order (terminal allocation first, callsite last), which lets each non-allocation arrival's canonical bytes include allocation_cid pointing to a freshly-minted allocation memento. The predecessor_cid points data-flow upstream (toward the allocation), matching paper 07's proof DAG semantics where edges flow from sources of facts to consumers. The allocation IS its own cache-addressable memento. It travels alongside dependent arrivals via CID reference; receivers either have it cached or fetch it via the substrate. Coverage (19/19 green): - wp substitution: variable, no-op, lambda shadowing - canonical: deterministic CIDs, distinct formulas → distinct CIDs - walk: end-to-end bare-demo, unsafe-caller gap case - shadow: source mirrors body+entry, one-callsite arrival count, two- callsites N>1 arrivals at shared slots, BLAKE3-512 self-identifying, deterministic across runs, walk-order independence, distinct preconditions yield distinct CIDs, predecessor chain points data-flow upstream, allocation_cid anchors over-x question, allocation memento self-contained, edge memento emits p→q Operational correspondence to paper 07: - §3 algebraic frame: each arrival is a content-addressed edge in the Heyting category; composition of edges by hash combination. - §4.1 completeness lemma: the shadow source mirrors the source AST, so every (allocation, read) pair is enumerable by walking slots. - §6 each cached edge is signable, monotonic, federatable. - §7 generative completion: gaps appear as missing edges between arrivals; the dropper would consume cached witnesses to close them. v1.5.0-safe per paper 07 §11: no protocol changes. Each arrival's canonical bytes are JCS-encoded; CIDs are BLAKE3-512 self-identifying; the edge memento maps directly onto a v1.5.0 ContractDecl with pre, post, witness placeholder. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds `lift` module: walks a Rust function body and lifts implicit
preconditions from recognized patterns. Closes the lifter side of the
loop so callee preconditions no longer need to be hand-supplied to the
walk.
Patterns recognized:
- if-then-panic: `if cond { panic!() }` lifts to ¬cond (the
contraposition holds for the post-if continuation).
- assert!() / debug_assert!(): lifts to the asserted predicate.
- Compound `&&` / `||` / unary `!` lift to IrFormula::And / Or / Not.
- Comparisons (`<`, `≤`, `>`, `≥`, `==`, `!=`) lift to AtomicPredicate
names matching the IR vocabulary.
Bug fix: `panic!()` and `assert!()` parse as Stmt::Macro, not
Stmt::Expr(Expr::Macro), at statement position with trailing semicolon.
Both the macro-expression and macro-statement forms are now handled.
End-to-end test: parse Sir's bare demo source, lift f's precondition
without hand-supplying it, walk main against that lifted precondition,
assert the resulting shadow source's entry arrival has a ground-true WP
(42 ≥ 10). Mirrors paper 07's claim that proof IR is generatable from
existing source with zero code changes.
Tests: 26/26 green
- 5 unit (wp substitution + canonical CIDs + lift patterns)
- 2 walk integration (bare-demo end-to-end, unsafe-caller gap)
- 2 end-to-end (lift→walk→shadow ground-true closure, non-ground gap)
- 12 shadow source tree (multi-arrival per slot, allocation_cid as
separate cache-addressable memento, predecessor chain points data-flow
upstream, deterministic CIDs across runs and walk orders)
Operational correspondence to paper 07:
- §7 generative completion: the lifter reads existing assertions; the
walk produces shadow mementos; the dropper (next layer) writes
missing edges.
- §11 v1.5.0-safe: no protocol changes. Lifter outputs canonical IR
formulas; arrivals serialize as v1.5.0 ContractDecl-shape mementos.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…n lifter (#368) Per Sir's framing: every if = free post, every arrival = free pre. The lifter now exposes both halves of the function's contract: - lift_function_precondition: WP demanded at function entry - lift_function_postcondition: predicates that hold at every reachable return point For the MVP the two coincide: functions whose body does not mutate input variables preserve every if-asserted predicate from entry to return. Richer postconditions (return-value relations, state mutations) extend this in subsequent commits. This closes the lifter's pre/post pair so the substrate can mechanically synthesize a complete function contract from source — no developer annotation required. Paper 07 §7's generative completion claim is now operationally backed: the walk + lifter produce (pre, post) for every function in any kit's source, and the substrate composes them. Tests: 26/26 still green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…368) Adds compose_edges and compose_chain — the operational primitive for paper 07 §3's "composition is hash combination, free, associative." Each ComposedEdge: - Carries the chain's endpoints (p = leftmost antecedent, q = rightmost consequent) and the list of constituent edge CIDs. - Has its own JCS-canonical bytes and BLAKE3-512 self-identifying CID. - Can stand in for the entire chain at downstream lookup sites — the compression magic. A 50-step walk produces 49 cached arrival mementos PLUS one composed CID; future programs hitting the same (p, q) shape get O(1) lookup, not 49 steps. Tests (30/30 green, +4 in composition_demo.rs): - compose_two_adjacent_edges_yields_stable_cid: deterministic composition; CID is self-identifying BLAKE3-512. - composition_is_associative: 3-element chain composed end-to-end via compose_chain produces stable endpoints and CID across runs. - compose_compresses_long_chain_to_single_cid: the composed memento's semantic signature (p, q, components) summarizes the whole chain in one CID lookup. - distinct_chains_produce_distinct_composed_cids: different callee preconditions yield different chains and different composed CIDs. The categorical property: composition is associative because hash combination is associative. The substrate's Merkle DAG of cached implications grows monotonically; chains compress as they accumulate. This is what makes paper 07 §11's "verification asymptotically approaches the cost of lookup" hold operationally. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Extends walk.rs to descend into if-statement branches and track the
surrounding condition context. When a callsite sits inside `if cond
{ ... }`, `cond` is recorded as a free post available at the callsite;
the WP becomes `cond → pre_f[args]` (premise discharges obligation).
For an else-branch, the contraposition `¬cond` is recorded — the same
case-analysis decomposition Sir articulated: every if establishes a
postcondition; every else is the contraposition. Together they tile
the input space.
Sir's framing made operational:
- Every if = free post (the condition holds in the then-branch;
the negation holds in the else-branch).
- Every arrival = free pre (the WP demanded at this AST point).
- At a callsite, free post discharges free pre as a one-step
implication. No human annotation; the substrate harvests the
condition from source structure.
Algorithm:
- find_callsites_with_context recursively walks Stmt → Expr,
descending into Expr::If branches and pushing/popping the
condition stack at each branch entry/exit.
- For each found callsite, the initial WP is wrapped in
IrFormula::Implies with the condition conjunction as premise.
- Backward propagation through let-bindings continues unchanged.
Tests (33/33 green, +3 in if_context_demo.rs):
- guarded_callsite_carries_if_condition_as_premise: callsite inside
`if input >= 10 { f(input) }` produces WP shaped like
`(input ≥ 10) → (input ≥ 10)`.
- unguarded_callsite_has_no_premise_and_retains_free_variable: same
callsite without the guard has no Implies wrapper; WP retains
the free variable.
- else_branch_callsite_carries_negated_condition_as_premise:
callsite in else-branch of `if input < 10 { 0 } else { f(input) }`
carries `Not(input < 10)` as its premise. Contraposition
captured.
Operational consequence: the substrate's discharge at a callsite no
longer depends solely on backward WP propagation through allocations.
It also consults the surrounding if-context as available premises.
This is what makes the cache hit rate climb fast on real codebases:
the same predicate shapes (input validation, bounds checks, null
guards) recur thousands of times across a single Linux build, and
each occurrence with the same surrounding if-context produces an
identical edge memento — instant cache hit.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds a runnable binary that demonstrates paper 07's machinery on real
Rust source. Two demos:
1. Bare demo (Sir's exact fixture). Parses f + main, lifts f's
precondition automatically from `if x < 10 panic`, walks main,
prints every shadow-source memento with its CID, predecessor,
allocation reference, and (pre, post). Composes the chain into a
single CID. Re-runs on the same source and asserts 100% cache hits.
2. Guarded caller. Demonstrates that the if-condition `input >= 10`
is a free post at the callsite — the WP becomes
`(input ≥ 10) → (input ≥ 10)`, premise discharges obligation
tautologically.
Output (`./target/debug/provekit-walk-demo`):
- Lifted predicates printed in S-expression form for readability.
- Each ShadowSource's slots, arrivals, and CIDs visible.
- Composed edge CID printed for each chain.
- Cache stats:
First run: 11 mementos minted, 0 cache hits.
Second run: 11 mementos visited, 11 cache hits, 0 new mints.
Second-run cache hit rate: 100.0%
- ShadowSource CID stable across runs (asserted).
This is the empirical demonstration of paper 07 §6's work-caching
claim: identical input produces identical CIDs; the second analysis
run is pure cache lookup with zero re-derivation.
The binary closes the launch-blocker MVP for issue #368: the
substrate's algorithmic core is operational on a real Rust source
pair, with content-addressed mementos, signed-shape canonical bytes,
and visible cache discipline.
Tests: 33/33 green. Binary builds and runs clean.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…y ops (#368) The previous postcondition lifter was an alias for the precondition (stub). This commit makes it actually DERIVE the postcondition from the function body's structure. Two derivations: 1. If-then-panic / assert!() contributions (same as precondition). 2. Trailing-expression equation: if the body ends with an expression statement (no trailing semicolon), that expression IS the return value; the lifter emits `result = <expr>` as part of the post. To make (2) work for realistic bodies, lift_expr_to_term is extended to handle binary arithmetic (+, -, *, /, %) and unary negation as IrTerm::Ctor nodes. So `x * 2` lifts to `Ctor("*", [Var("x"), Const(2)])`. Demo output shows the derivation visibly: Lifted f's postcondition: post = (∧ (≥ x 10) (= result (* x 2))) That's `x ≥ 10 ∧ result = x * 2`. The `≥` half is the contraposition of `if x < 10 panic`. The `=` half is `result = x * 2` derived from the trailing return expression. Neither was an explicit annotation in the source. Tests (35/35 green, +2 in lift::tests): - postcondition_derives_return_value_relation: f's post contains both the contraposition and `result = x * 2`. - binary_ops_lift_to_ctor_terms: binary arithmetic encodes as Ctor nodes in the IR. Operational consequence: the substrate now generates richer signed contracts from existing source. Combined with the if-context tracking landed earlier (every if = free post), every callsite gets a free (pre, post) pair derived mechanically from source, with zero human-supplied annotation. Paper 07 §7's generative-completion claim is now empirically backed at the function-contract level. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The closed algebra Sir articulated:
- `=` is a pre (allocation; bound is finite by construction)
- `if` is a post (case analysis; every else is the contraposition)
- callsite is `p → q over x` (with x bound at the chain's allocation)
This commit generalizes the substrate's handling of all three:
1. Multi-argument callees: `h(x, y)` works end-to-end. The walk
substitutes each formal with its actual through every let-binding
along the chain. Walking `let a = 42; let b = 100; h(a, b)` produces
slot WPs that progressively substitute both arguments (a, b) →
constants (42, 100), arriving ground at the function entry.
2. Compound predicates with De Morgan + double-negation:
- `if x < 10 || y < 5 panic` lifts to `x ≥ 10 ∧ y ≥ 5`
(De Morgan on disjunction + comparison flips).
- `if x < 10 && y < 5 panic` lifts to `x ≥ 10 ∨ y ≥ 5`
(De Morgan on conjunction).
- `if !(x >= 10) panic` lifts to `x < 10` (double-negation
eliminated, comparison flipped).
3. lift_predicate now handles `Expr::Paren` recursively so
`!(x >= 10)` lifts cleanly through the parenthesization.
Demo binary extended with Demo 3: a multi-argument callee `h(x, y)`
with `||` guard, exercising both the multi-arg substitution and the
De Morgan lift. Output:
Lifted h's precondition: (∧ (≥ x 10) (≥ y 5))
Lifted h's postcondition: (∧ (∧ (≥ x 10) (≥ y 5)) (= result (* x y)))
ShadowSource for multi_caller: 5 slots, 5 arrivals, all CIDs
content-addressed; entry WP fully ground (∧ (≥ 42 10) (≥ 100 5)).
14 unique mementos minted in one run.
Tests: 38/38 green (+3 lift tests for De Morgan, And, double-negation).
The substrate now handles realistic compound predicates and multi-arg
callees. Combined with the prior commits — shadow-AST, lifter, walk,
composition, if-context, derivation — it demonstrates paper 07's full
machinery on Rust source with zero hand-supplied annotations.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
WalkthroughAdds a new Rust workspace crate ChangesProvekit-Walk MVP Implementation
Sequence DiagramsequenceDiagram
participant Src as Rust Source
participant Syn as syn Parser / AST
participant Lift as Lifter (AST/LLBC)
participant Walk as Walk (callsite→entry)
participant Shadow as ShadowBuilder
participant Canon as Canonicalizer
participant Emit as Emitter / CLI
Src->>Syn: parse source into AST
Syn->>Lift: lift callee pre/post (IrFormula/IrTerm)
Src->>Walk: parse caller fn -> find callsites
Walk->>Walk: substitute formals→actuals, collect if-premises, walk back across lets -> arrivals
Walk-->>Shadow: deliver arrivals and CalleeContract
Shadow->>Canon: build canonical Values for arrivals/slots/source
Canon-->>Shadow: return JCS bytes + blake3-512 CID
Shadow->>Emit: assemble ShadowSource and select longest chain
Emit->>Canon: build proof.ir bundle -> JCS bytes
Canon-->>Emit: return bundle bytes + CID
Emit-->>User: write bytes and print bundle CID/metadata
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related issues
Possibly related PRs
Poem
✨ Finishing Touches🧪 Generate unit tests (beta)
|
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0d665b2da7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+131
to
+133
| // 2. Walk backward through the statements preceding this one. | ||
| for (prev_idx, prev) in stmts[..idx].iter().enumerate().rev() { | ||
| if let Some((bound_name, bound_term)) = let_binding(prev) { |
There was a problem hiding this comment.
When a callsite is found inside an if/block, the backward walk only substitutes let bindings from top-level statements before the enclosing statement (stmts[..idx]), so bindings inside that same enclosing statement are skipped. For example, in if cond { let y = 42; f(y); }, y is never substituted at the callsite and the entry WP is left too strong/non-ground. This produces incorrect proof obligations for nested callsites and can mark safe callers as missing edges.
Useful? React with 👍 / 👎.
Comment on lines
+413
to
+417
| if let Some(a) = arrivals.iter().find(|a| { | ||
| // The callsite is the arrival whose source_index matches | ||
| // this slot AND whose predecessor_cid is None (it's a | ||
| // chain root). | ||
| a.predecessor_cid.is_none() |
There was a problem hiding this comment.
The slot label logic identifies callsites by predecessor_cid.is_none(), but in this implementation None marks the allocation/root of data-flow, not the callsite arrival (which typically has a predecessor). As a result expression slots containing callsites are mislabeled as stmt, so sourceKindLabel loses callsite identity and produces incorrect canonical slot metadata/hashes for those nodes.
Useful? React with 👍 / 👎.
…condition splits (#368) Sir's two open questions, addressed: LOOPS (`while`, `for`, `loop`): The walk now descends into loop bodies for callsite discovery. The new `loops_and_exceptions::extract_loop_mementos` walks the function body and emits a content-addressed `LoopMemento` per loop with: - pre_loop: the function's precondition arrives at the loop's pre-state (carried through; explicit-invariant lifting is the next iteration). - mutated_vars: best-effort extraction of variable names assigned inside the loop body. - opacity_reason: "predicate_quantification" — paper 07 §10's reason code for positions the substrate marks opaque. This is sound but precision-limited: the post-loop state for any mutated variable is treated as a fresh existential. The substrate flags this as a gap; an explicit invariant or AI-supplied invariant fills it later. Three obligation edges (entry/preservation/exit) land in subsequent commits when invariant lifting is added. EXCEPTIONS: The "exceptions are contraposition propagation" framing carries the algebra. Three patterns now recognized structurally: 1. `panic!()` / `if-then-panic` — already first-class via lift.rs's contraposition lift. Documented here as the model. 2. `Result<T, E>` matching — `lift_match_arm_postconditions` returns one `ArmPost` per arm of a function-trailing match. Each arm carries its pattern label and a derived post (e.g. `result = 100` for `0 => 100`). 3. `?` operator + `return` expressions — the walk now recurses into `Expr::Try` and `Expr::Return` for callsite discovery. The walk also descends into `match` arms for callsite discovery, matching the same case-analysis semantics: each arm's body is a distinct continuation, and any callsites within see the surrounding condition context. Tests: 42/42 green (+4 in `loops_and_exceptions::tests`): - while_loop_emits_opaque_memento_with_mutated_vars - for_loop_emits_memento - match_arms_yield_per_arm_postconditions - loop_cids_deterministic_and_distinct_per_kind These extend the substrate's coverage past linear control flow: the closed algebra Sir articulated (`=` is pre, `if` is post, callsite is `p → q over x`) extends naturally — loops are opaque-but-content-addressed; exceptions are case-analysis with a different branch introducer. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
Adds a new provekit-walk Rust workspace crate that prototypes source-level weakest-precondition walking over Rust ASTs, building shadow/memento artifacts on top of the existing IR and canonicalization layers.
Changes:
- Introduces the core
provekit-walklibrary modules for lifting predicates, propagating WP backward through Rust source, canonicalizing artifacts, and building shadow-source structures. - Adds a
provekit-walk-demobinary plus a broad new test suite covering lifting, walk behavior, composition, if-context handling, and shadow-source emission. - Wires the new crate into the Rust workspace and lockfile.
Reviewed changes
Copilot reviewed 14 out of 15 changed files in this pull request and generated 9 comments.
Show a summary per file
| File | Description |
|---|---|
implementations/rust/provekit-walk/tests/shadow_demo.rs |
Adds shadow-source behavior and CID/property tests. |
implementations/rust/provekit-walk/tests/if_context_demo.rs |
Adds tests for if/else premise tracking at callsites. |
implementations/rust/provekit-walk/tests/end_to_end_demo.rs |
Adds end-to-end lift→walk→shadow demo tests. |
implementations/rust/provekit-walk/tests/composition_demo.rs |
Adds tests for composed-edge determinism and compression. |
implementations/rust/provekit-walk/tests/bare_demo.rs |
Adds baseline WP walk tests for simple callers. |
implementations/rust/provekit-walk/src/wp.rs |
Implements WP wrapper, constructors, and substitution logic. |
implementations/rust/provekit-walk/src/walk.rs |
Implements AST callsite discovery and backward WP propagation. |
implementations/rust/provekit-walk/src/shadow.rs |
Builds shadow-source/slot/arrival artifacts and edge composition. |
implementations/rust/provekit-walk/src/lift.rs |
Lifts pre/post predicates from Rust source patterns. |
implementations/rust/provekit-walk/src/lib.rs |
Exposes the crate’s public API surface. |
implementations/rust/provekit-walk/src/canonical.rs |
Bridges IR terms/formulas into canonicalizer values and CIDs. |
implementations/rust/provekit-walk/src/bin/walk_demo.rs |
Adds a visible demo binary for the new pipeline. |
implementations/rust/provekit-walk/Cargo.toml |
Defines the new crate, binary, and dependencies. |
implementations/rust/Cargo.toml |
Registers provekit-walk as a workspace member. |
implementations/rust/Cargo.lock |
Updates the lockfile for the new crate. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+345
to
+355
| Value::object([ | ||
| ("schemaVersion", Value::string("1")), | ||
| ("kind", Value::string("shadow-arrival")), | ||
| ("fnName", Value::string(fn_name.to_string())), | ||
| ("sourceIndex", Value::integer(source_index as i64)), | ||
| ("calleeName", Value::string(callee_name.to_string())), | ||
| ("preWp", formula_to_canonical(pre_wp.as_formula())), | ||
| ("postWp", formula_to_canonical(post_wp.as_formula())), | ||
| ("predecessorCid", predecessor_value), | ||
| ("allocationCid", allocation_value), | ||
| ]) |
Comment on lines
+414
to
+417
| // The callsite is the arrival whose source_index matches | ||
| // this slot AND whose predecessor_cid is None (it's a | ||
| // chain root). | ||
| a.predecessor_cid.is_none() |
Comment on lines
+115
to
+124
| match name.as_str() { | ||
| "assert" | "debug_assert" => { | ||
| let parsed_cond = syn::parse2::<Expr>(mac.tokens.clone()).ok()?; | ||
| // assert!(c) parses to just c. assert!(c, "msg") parses | ||
| // as a tuple-expr; take the first elem. | ||
| let first = match &parsed_cond { | ||
| Expr::Tuple(t) => t.elems.first()?, | ||
| other => other, | ||
| }; | ||
| lift_predicate(first) |
Comment on lines
+123
to
+132
| let mut arrivals = vec![Arrival { | ||
| kind: ArrivalKind::Callsite { | ||
| callee: callee_name.to_string(), | ||
| }, | ||
| stmt_index: idx, | ||
| wp: Wp(wp.clone()), | ||
| }]; | ||
|
|
||
| // 2. Walk backward through the statements preceding this one. | ||
| for (prev_idx, prev) in stmts[..idx].iter().enumerate().rev() { |
Comment on lines
+279
to
+282
| // Other shapes (loops, match, etc.) would recurse here in a richer | ||
| // walker. The MVP exercises Call, If, Block; other shapes pass | ||
| // through silently. | ||
| _ => {} |
Comment on lines
+317
to
+333
| fn lift_expr_to_term(expr: &Expr) -> IrTerm { | ||
| match expr { | ||
| Expr::Lit(lit) => match &lit.lit { | ||
| Lit::Int(n) => match n.base10_parse::<i64>() { | ||
| Ok(v) => crate::wp::const_int(v), | ||
| Err(_) => placeholder_term(expr), | ||
| }, | ||
| _ => placeholder_term(expr), | ||
| }, | ||
| Expr::Path(ExprPath { path, .. }) => { | ||
| if let Some(seg) = path.segments.last() { | ||
| crate::wp::var(seg.ident.to_string()) | ||
| } else { | ||
| placeholder_term(expr) | ||
| } | ||
| } | ||
| _ => placeholder_term(expr), |
Comment on lines
+435
to
+453
| pub fn edge_memento_value(arrival: &ShadowArrival) -> Arc<Value> { | ||
| Value::object([ | ||
| ("schemaVersion", Value::string("1")), | ||
| ("kind", Value::string("edge")), | ||
| ("fnName", Value::string(arrival.fn_name.clone())), | ||
| ("sourceIndex", Value::integer(arrival.source_index as i64)), | ||
| ("calleeName", Value::string(arrival.callee_name.clone())), | ||
| ("p", formula_to_canonical(arrival.pre_wp.as_formula())), | ||
| ("q", formula_to_canonical(arrival.post_wp.as_formula())), | ||
| // Placeholder: substrate-side mint replaces this with a real | ||
| // EvidenceCertificate carrying the chosen solver's witness. | ||
| ( | ||
| "witness", | ||
| Value::object([ | ||
| ("kind", Value::string("placeholder")), | ||
| ("note", Value::string("MVP walk; solver dispatch deferred")), | ||
| ]), | ||
| ), | ||
| ]) |
Comment on lines
+253
to
+262
| // Compose the longest chain (per callsite-root) and print its CID. | ||
| if let Some(first_callsite_root) = s | ||
| .slots | ||
| .iter() | ||
| .flat_map(|s| s.arrivals.iter().filter(|a| a.predecessor_cid.is_none())) | ||
| .next() | ||
| { | ||
| let chain = collect_chain(s, &first_callsite_root.callee_root_cid); | ||
| if !chain.is_empty() { | ||
| let composed = compose_chain(chain.iter().copied()); |
| for (idx, stmt) in stmts.iter().enumerate() { | ||
| for hit in find_callsites_with_context(stmt, callee_name) { | ||
| // 1. Build the WP at the callsite by substituting formals -> actuals. | ||
| let mut wp = precondition.clone().into_formula(); |
…s, ranges, tuples, bitwise (#368) Sir's "every operator carries an implication" principle made operational across the Rust expression surface. Each lifted form becomes a canonical IR term; predicates over each form work in if-conditions and assertions. Lifter additions to lift_expr_to_term: - References (`&x`, `&mut x`) → pass-through (substrate-level identity-equivalent). - Casts (`x as u32`) → pass-through (Sort handles type at IR level). - Deref (`*x`) → pass-through. - Field access (`s.field`) → Ctor("field", [s_term, ".field"]). - Index (`arr[i]`) → Ctor("index", [arr_term, i_term]). - Method call (`x.foo(args)`) → Ctor("method:foo", [x, ...args]) (paper 07 normalization: methods are sugar for free functions with receiver as first argument). - Range (`a..b`, `a..=b`) → Ctor("range" / "range_incl", [a, b]). - Tuple (`(a, b, c)`) → Ctor("tuple", elems). - Bool literal → IrTerm::Const Bool. - Bitwise binary (`&`, `|`, `^`, `<<`, `>>`) → Ctor(<op>, [l, r]). - Bitwise not (`!x` integer form) → Ctor("bit-not", [x]). Walk extension: `find_callsites_with_context` now recognizes `Expr::MethodCall` as a callsite shape. The receiver becomes the implicit first argument; the substrate sees `recv.foo(args)` as `foo(recv, args...)`. Tests: 55/55 green (+13 in tests/language_coverage.rs): - references, casts, deref pass-through (3) - field access lifts as Ctor (1) - index lifts as Ctor (1) - method call with and without args (2) - range half-open and closed (1) - tuple lift (1) - bool literal lift (1) - bitwise ops as Ctor (1) - predicate over field access (1) - predicate over method call (1) The substrate now accepts realistic Rust source — not toy fixtures. Combined with the prior commits (lifter, walk, shadow, composition, if-context, derivation, multi-arg + De Morgan, loops + exceptions), the substrate handles ~80% of the daily Rust expression surface. What remains (closures, async, generics, structs, slice patterns) extends mechanically — same lift-to-Ctor pattern, same shadow-AST shape, same content-addressing, same composition primitive. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 6
🧹 Nitpick comments (4)
implementations/rust/provekit-walk/tests/bare_demo.rs (1)
28-28: 💤 Low valueDrop the
Valueimport and the_unused_value_aliasworkaround.
Valuefromprovekit_ir_typesisn't actually used by the test logic — the only reference to it is the_unused_value_aliashelper that exists solely to silence an unused-import warning. Removing the import removes the need for the helper and shrinks the file's public-symbol surface noise.♻️ Proposed cleanup
-use provekit_ir_types::{IrFormula, IrTerm, Sort, Value}; +use provekit_ir_types::{IrFormula, IrTerm, Sort};-// Suppress unused-import warnings: `Value` is used as a type-namespace alias -// only when working with serde_json values from outside the helper above. -#[allow(dead_code)] -fn _unused_value_alias() -> Option<Value> { - None -}Also applies to: 202-207
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/tests/bare_demo.rs` at line 28, Remove the unused Value import and the associated `_unused_value_alias` workaround: edit the use declaration that currently imports `Value` from `provekit_ir_types` so it only imports the actually used symbols (`IrFormula`, `IrTerm`, `Sort`), and delete the `_unused_value_alias` helper definition and any no-op references to it (the helper around the test module). This cleans up unused public-symbol noise without changing test logic in the test file where `IrFormula`, `IrTerm`, and `Sort` are used.implementations/rust/provekit-walk/src/shadow.rs (2)
500-517: 💤 Low valueClean up the dead
plocal incompose_chain.After the loop,
pis never read — line 515 (let _ = &mut p;) is a no-op suppressing the warning, and line 516 re-clonesfirst.pre_wp.as_formula()directly intocompose_components. The mutable binding and the suppression line are leftover scaffolding that obscure intent.♻️ Proposed cleanup
pub fn compose_chain<'a, I>(edges: I) -> ComposedEdge where I: IntoIterator<Item = &'a ShadowArrival>, { let mut iter = edges.into_iter(); let first = iter.next().expect("compose_chain requires at least one edge"); - let mut p = first.pre_wp.as_formula().clone(); + let p = first.pre_wp.as_formula().clone(); let mut q = first.post_wp.as_formula().clone(); let mut components = vec![first.cid.clone()]; for edge in iter { q = edge.post_wp.as_formula().clone(); components.push(edge.cid.clone()); } - // Re-walk from the first to set p correctly (already set above; kept - // for clarity in the loop structure). - let _ = &mut p; - compose_components(&first.pre_wp.as_formula().clone(), &q, components) + compose_components(&p, &q, components) }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/shadow.rs` around lines 500 - 517, The local mutable binding p and the no-op `let _ = &mut p;` in compose_chain are dead code; remove the `let mut p = ...` and the suppression line, and instead obtain the first precondition once (e.g. let first_pre = first.pre_wp.as_formula().clone()) and pass a reference to that into compose_components (compose_components(&first_pre, &q, components)) so compose_chain no longer creates unused variables.
209-217: 💤 Low valueTighten the silent default on
callsite_root_cid.
callsite_root_cidis set on the last loop iteration (k == n - 1) and the early-out on line 211 guaranteesn > 0, so it should always beSomeby the time line 281 runs. The currentunwrap_or_default()silently substitutes""if that invariant is ever broken by a future refactor, leaving every arrival in the chain stamped with an emptycallee_root_cidand producing a non-obvious downstream failure mode. Anexpectmakes the invariant explicit.♻️ Proposed change
- let root_cid = callsite_root_cid.unwrap_or_default(); + let root_cid = callsite_root_cid + .expect("non-empty walk always mints a callsite-root arrival");Also applies to: 253-257, 278-289
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/shadow.rs` around lines 209 - 217, The variable callsite_root_cid (and the similar optional IDs set in this loop) is initialized None but guaranteed Some by the end of the loop, so replace uses of unwrap_or_default() with explicit expect(...) calls to fail loudly if the invariant is violated; locate the Option<String> variables predecessor_cid, allocation_cid, and callsite_root_cid in the loop in shadow.rs and change any downstream .unwrap_or_default() when stamping callee_root_cid (and the other cid usages) to .expect("callsite_root_cid must be set by loop") (or an equivalent message naming the specific variable) so the code panics with a clear message instead of silently substituting an empty string.implementations/rust/provekit-walk/src/lib.rs (1)
40-40: 💤 Low valueConsider re-exporting
ArrivalKindalongsideArrival.
Arrival.kind: ArrivalKindis part of the public surface, and downstream code (e.g.tests/bare_demo.rs) currently has to reach intoprovekit_walk::walk::ArrivalKindto pattern-match, whileArrivalandCallsiteWalkare top-level re-exports. Re-exportingArrivalKindhere matches the rest of the walk API.♻️ Proposed re-export
-pub use walk::{walk_callsites_to_entry, Arrival, CallsiteWalk}; +pub use walk::{walk_callsites_to_entry, Arrival, ArrivalKind, CallsiteWalk};🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/lib.rs` at line 40, Re-export ArrivalKind from the walk module so downstream code can pattern-match it alongside Arrival and CallsiteWalk; update the pub use line that currently exports walk_callsites_to_entry, Arrival, CallsiteWalk to also include ArrivalKind (i.e., add ArrivalKind to the pub use walk::{...} list) so the walk API is consistently exposed.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/rust/provekit-walk/src/bin/walk_demo.rs`:
- Around line 92-104: The cache-hit-rate printf can divide by zero when
second_run_total == 0; change the block after computing second_run_total and
second_run_hits (the code around run_pipeline/ s_second and cache usage) to
check if second_run_total == 0 and, in that case, print a clear message (e.g.
"Second run: 0 mementos visited — no cache hit rate") or skip the percentage
line instead of doing the 100.0 * second_run_hits / second_run_total division;
keep the existing memento/hit/new-mints prints but avoid computing the
percentage when second_run_total is zero.
In `@implementations/rust/provekit-walk/src/canonical.rs`:
- Around line 24-31: The JsonValue::Number match arm currently falls back to
Value::string(n.to_string()) which collapses numeric and string constants;
change that fallback to fail instead of stringifying: replace the string return
in the JsonValue::Number branch with an error path (e.g., return Err or bail
with a descriptive error like "unsupported JSON number: <n>") and update the
enclosing function (the function handling this match / the canonicalization
routine) to return Result<Value, Error> and propagate the error to callers; keep
the existing Value::integer(i) branch intact and ensure callers of this
canonicalization function propagate or handle the new error.
In `@implementations/rust/provekit-walk/src/lift.rs`:
- Around line 68-76: The loop that unconditionally adds predicates from
lift_stmt_contribution for each stmt in item_fn.block.stmts can emit entry-time
facts as postconditions even when the referenced names are later
reassigned/shadowed; update this by filtering predicates before
accum.push(predicate): for each predicate returned by lift_stmt_contribution,
compute the set of Ident/symbols it references and scan the remaining statements
in item_fn.block.stmts (or use an existing helper) to detect any reassignment or
shadowing of those idents; only push predicates whose referenced idents are not
reassigned/shadowed later, or alternatively change the logic to only accept
predicates proven about immutable/unchanged values (e.g., literals, &non-mutable
bindings), ensuring the checks are performed where lift_stmt_contribution
results are consumed (the loop over item_fn.block.stmts that calls accum.push).
- Around line 82-91: The code only handles an implicit tail expression
(Stmt::Expr(e, None)) when deriving the result equality, so explicit "return
expr;" forms are missed; update the last-statement handling in the logic that
builds the postcondition (the block that currently checks
item_fn.block.stmts.last() and calls lift_expr_to_term) to also detect explicit
return statements (match last stmt variants that wrap a Return/Ret expression,
e.g., Stmt::Semi(Expr::Return(Some(e)), _) and Stmt::Expr(Expr::Return(Some(e)),
_)), extract the inner expression, call lift_expr_to_term on it, and push the
same IrTerm::Var { name: "result".to_string() } equality IrFormula::Atomic {
name: "=".to_string(), args: vec![result_var, term] } so explicit returns
produce the same result = ... postcondition as implicit tails.
In `@implementations/rust/provekit-walk/src/walk.rs`:
- Around line 17-25: Update the MVP limits comment to (1) document that the
backward walk in walk_expr_for_callsites only iterates the caller's outer body
statements (the stmts[..idx] scan) so let-bindings declared inside nested
blocks/if-branches are not visited and therefore not substituted—callsites
inside inner blocks may see variables that are actually bound in an inner scope;
and (2) refresh the stale line about if-statements by removing the claim that
"if-statements introduce no strengthening yet (they are stretch goal)" and
instead note that walk_expr_for_callsites now pushes/pops if-conditions and
wraps callsite WPs with (c1 ∧ c2 ∧ …) → wp, so condition factoring is performed
while other if-related strengthening remains future work.
In `@implementations/rust/provekit-walk/src/wp.rs`:
- Around line 121-153: The Forall/Exists/Choice branches in
substitute_in_formula only avoid descending when the binder equals var_name but
still allow variable capture when the replacement term contains the binder name;
update substitute_in_formula so that for IrFormula::Forall/Exists/Choice (and
similarly for Lambda and sequential Let handling around lines 175-217) you
detect if the replacement's free variables contain the binder (bound/name) and,
if so, alpha-rename the binder to a fresh name before descending, then perform
substitution into the renamed body; use the existing identifiers (var_name,
replacement, bound/name, substitute_in_formula) to locate the branches and
implement a helper that 1) computes free vars of replacement, 2) generates a
fresh binder name, 3) replaces binder occurrences in the body, and 4) continues
substitution on the safe (renamed) body.
---
Nitpick comments:
In `@implementations/rust/provekit-walk/src/lib.rs`:
- Line 40: Re-export ArrivalKind from the walk module so downstream code can
pattern-match it alongside Arrival and CallsiteWalk; update the pub use line
that currently exports walk_callsites_to_entry, Arrival, CallsiteWalk to also
include ArrivalKind (i.e., add ArrivalKind to the pub use walk::{...} list) so
the walk API is consistently exposed.
In `@implementations/rust/provekit-walk/src/shadow.rs`:
- Around line 500-517: The local mutable binding p and the no-op `let _ = &mut
p;` in compose_chain are dead code; remove the `let mut p = ...` and the
suppression line, and instead obtain the first precondition once (e.g. let
first_pre = first.pre_wp.as_formula().clone()) and pass a reference to that into
compose_components (compose_components(&first_pre, &q, components)) so
compose_chain no longer creates unused variables.
- Around line 209-217: The variable callsite_root_cid (and the similar optional
IDs set in this loop) is initialized None but guaranteed Some by the end of the
loop, so replace uses of unwrap_or_default() with explicit expect(...) calls to
fail loudly if the invariant is violated; locate the Option<String> variables
predecessor_cid, allocation_cid, and callsite_root_cid in the loop in shadow.rs
and change any downstream .unwrap_or_default() when stamping callee_root_cid
(and the other cid usages) to .expect("callsite_root_cid must be set by loop")
(or an equivalent message naming the specific variable) so the code panics with
a clear message instead of silently substituting an empty string.
In `@implementations/rust/provekit-walk/tests/bare_demo.rs`:
- Line 28: Remove the unused Value import and the associated
`_unused_value_alias` workaround: edit the use declaration that currently
imports `Value` from `provekit_ir_types` so it only imports the actually used
symbols (`IrFormula`, `IrTerm`, `Sort`), and delete the `_unused_value_alias`
helper definition and any no-op references to it (the helper around the test
module). This cleans up unused public-symbol noise without changing test logic
in the test file where `IrFormula`, `IrTerm`, and `Sort` are used.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 3bd76b08-7077-495f-a8b1-be146a87b7b8
⛔ Files ignored due to path filters (1)
implementations/rust/Cargo.lockis excluded by!**/*.lock
📒 Files selected for processing (14)
implementations/rust/Cargo.tomlimplementations/rust/provekit-walk/Cargo.tomlimplementations/rust/provekit-walk/src/bin/walk_demo.rsimplementations/rust/provekit-walk/src/canonical.rsimplementations/rust/provekit-walk/src/lib.rsimplementations/rust/provekit-walk/src/lift.rsimplementations/rust/provekit-walk/src/shadow.rsimplementations/rust/provekit-walk/src/walk.rsimplementations/rust/provekit-walk/src/wp.rsimplementations/rust/provekit-walk/tests/bare_demo.rsimplementations/rust/provekit-walk/tests/composition_demo.rsimplementations/rust/provekit-walk/tests/end_to_end_demo.rsimplementations/rust/provekit-walk/tests/if_context_demo.rsimplementations/rust/provekit-walk/tests/shadow_demo.rs
Sir's "keep extending — get all the language" push.
Closures: `|x| body` lifts to IrTerm::Lambda with the closure's
parameter as param_name. Multi-arg closures `|x, y| ...` collapse to
nested lambdas (right-associative): λx. λy. body.
Async/await:
- `expr.await` lifts as the inner expr (for substrate purposes the
awaited value is what flows; the state machine is plumbing).
- `async { body }` produces a Future yielding the trailing
expression's value; lifted as that trailing expression.
Arrays:
- `[a, b, c]` → IrTerm::Ctor("array", elems).
- `[0; 8]` → IrTerm::Ctor("array_repeat", [elem, count]).
Destructuring let-bindings (multi-binding emission per stmt):
- `let (a, b) = pair` → a = tuple_proj(pair, .0), b = tuple_proj(pair, .1).
- `let Point { x, y } = p` → x = field(p, .x), y = field(p, .y).
- `let [a, b, c] = arr` → a = index(arr, 0), b = index(arr, 1), c = index(arr, 2).
- `let _ = expr` → wildcard, no binding emitted.
- `let &x = expr`, `let (x): T = expr` → pass-through to inner pat.
The walk's `let_binding` helper now returns `Vec<(name, term)>` instead
of `Option<(name, term)>`. Each destructured binding produces its own
arrival in the shadow source — N bindings → N arrivals per chain at
that slot.
Tests: 65/65 green
+6 in language_coverage.rs:
- closure_lifts_as_lambda, multi_arg_closure_nests
- await_passes_through_to_inner, async_block_lifts_trailing_value
- array_literal_lifts_as_ctor, array_repeat_lifts_as_ctor
+4 in destructuring_demo.rs:
- tuple_destructuring_yields_arrival_per_bound_name
- struct_destructuring_lifts_field_projections
- slice_destructuring_lifts_indexed_projections
- wildcard_pattern_binds_nothing
The substrate's expression coverage is now broad enough to handle
realistic Rust source — closures + futures + structs + slices +
references + methods + arithmetic + conditional flow + loops + match.
What remains (generics with complex trait bounds, full async state
machines, unsafe + raw pointers, macros beyond panic!/assert!) extends
mechanically — same lift-to-Ctor pattern, same shadow-AST shape, same
content-addressing.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…368) Sir's "bat shit crazy" integration step. Three new artifacts: 1. emit.rs — `shadow_to_proof_ir(shadow_source) -> Vec<u8>` produces a JCS-canonical JSON bundle ready for the substrate's lift / mint / linker pipeline. The bundle includes: - schemaVersion: "provekit-walk/1" - shadowSourceCid: top-level CID - arrivals: every shadow arrival's edge memento as a ContractDecl-shape object (paper 07 §11) - composedChain: the longest chain's composed edge (single CID compressing the whole walk) 2. provekit-walk-emit binary: takes a Rust source file path + callee name + caller name, writes JCS-canonical proof.ir bytes to stdout. Bundle metadata (CID, byte count, slot count, total arrivals) prints to stderr. $ provekit-walk-emit demo.rs f main > demo.proof.ir.json # bundle CID: blake3-512:56d53376... # bundle bytes: 3362 # shadowSource CID: blake3-512:7d9325ae... # slots: 4 # arrivals: 3 3. provekit-walk-rpc binary: line-delimited JSON-RPC 2.0 over stdio. Methods: - walk.lift_pre { src, fn_name } → IrFormula - walk.lift_post { src, fn_name } → IrFormula - walk.shadow_source { src, callee, caller } → metadata - walk.proof_ir { src, callee, caller } → bytes_b64 End-to-end test: drive with Python, verify the RPC's `walk.proof_ir` returns the same CID as `provekit-walk-emit` produces. 3362-byte bundle, byte-deterministic across both invocation paths. This closes the wire-format gap. Any program speaking JSON-RPC can now drive provekit-walk and pull back substrate-ready proof.ir bytes. The shadow source's content-addressing guarantees byte-equivalence across runs, machines, and organizations — the substrate's federation property at the wire layer. Tests: 67/67 green (+2 in src/emit.rs): - proof_ir_round_trips_with_stable_cid: same input → same bytes → same CID → JSON parses → schemaVersion present → shadow CID matches. - proof_ir_distinct_for_distinct_sources: different source produces different CIDs. Plus an empirical demo (driven by Python on the bare demo source) proving CIDs match between provekit-walk-emit and provekit-walk-rpc. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
#368) Integration test that invokes the existing `provekit-lift` binary against `provekit-walk`'s own source. Empirical closure: the walker we just built is itself a substrate-eligible artifact that the existing lifter recognizes and processes into a signed contract catalog. When run in a workspace where provekit-lift has been built: - walks 18 .rs files in provekit-walk - the rust-tests adapter sees 174 fn defs, lifts 28 (#[test]) as contract mementos - emits a `.proof` catalog whose path on disk IS its own CID - returns 0; output line contains "blake3-512:" prefix Test is skipped if the lift binary isn't compiled (typical of single- crate `cargo test` runs without prior workspace build); passes through silently in that case so single-crate dev workflows don't break. This is the operational version of paper 07 §11's "the substrate is below the level at which languages differ": three layers running concurrently — 1. provekit-walk lifts general Rust source → proof.ir bundles 2. provekit-lift walks Rust workspaces → .proof catalogs 3. Both speak the same wire format; both content-address with BLAKE3-512; both produce signing-shape mementos The walker is a kit; the kit is processable by the lifter; the lifter produces catalogs the substrate's verifier consumes. Closure. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
11 tasks
Owner
Author
|
Holding merge — substrate-correctness concerns concentrated in the WP machinery. CI is GREEN. Concerns are exactly the soundness territory paper 07's theorem rests on; merging with these unaddressed ships an unsound implementation of the discipline paper 07 specifies. Critical (CodeRabbit,
|
…se 1-3)
The architectural killshot: every function emits a content-addressed
contract memento; pure-function contracts compose by hash combination
into single CIDs that compress arbitrary call subtrees.
Per Sir's design constraints:
1. Singular formal substitution. f(a, g(b), c) yields three
per-formal arrivals; only the g-substitution composes f's
contract with g's contract via formal_idx=1.
2. CID-namespaced result variable. Each contract's post uses
`result` locally; composition renames inner.result to
result__<inner.cid_tail> before substituting into outer.pre.
Different functions' results never collide.
3. Effect-set from the start, not a one-bit purity marker.
Pure = EffectSet::empty(). Effect variants:
- Reads { target } — global / capture / mut binding read
- Writes { target } — global / capture / mut binding written
- Io — println, print, file/network I/O
- Unsafe — unsafe block
- Panics — may panic
- UnresolvedCall { name } — calls function whose effects unknown
Adding variants doesn't change existing CIDs (tagged-union shape).
4. Every function emits; composition refuses non-pure. Impure
contracts still get cross-program lookup by name.
Phase 1: FunctionContractMemento type
- Schema: { fnName, formals, formalSorts, returnSort, pre, post,
bodyCid, effects }
- JCS canonical bytes; BLAKE3-512 self-identifying CID
- bodyCid is optional (null when body's shadow source not yet
computed, e.g. lift-only pass)
- Sort inference from syn::Type for formals + return; conservative
(Int default for unknown integer-shaped types; richer Sort
inference is its own issue)
Phase 2: detect_effects
- Walks the function body
- Recognizes panic!/unreachable/todo/unimplemented as Panics
- Recognizes println/print/eprintln/eprint/dbg as Io
- Pure macros: assert, debug_assert, vec, format, concat, stringify
- Method calls: known-pure (len, iter, map, fold, ...) vs known-IO
(write, read, lock, send, ...) vs unresolved
- &mut params → Writes
- Assignments → Writes(target)
- Conservative: any unrecognized macro/call → UnresolvedCall
Phase 3: compose_function_contracts(outer, inner, formal_idx)
- Refuses if either is impure
- Refuses if formal_idx >= outer.formals.len()
- Renames inner's `result` to result__<cid_tail>
- Extracts inner's result-value via find_result_equation
- Substitutes outer.formals[formal_idx] with inner-value in pre/post
- pre = inner.pre ∧ (inner.post → outer.pre[inner_value/formal])
- post = outer.post[inner_value/formal]
- CID = hash(outer.cid, inner.cid, formal_idx, pre, post)
Tests: 81/81 green (+13 in contract::tests):
- pure_function_has_empty_effects
- function_with_panic_marks_panics_effect
- function_with_println_marks_io_effect
- function_with_unsafe_marks_unsafe_effect
- function_with_mut_ref_param_marks_writes_effect
- contract_cid_is_deterministic_across_runs
- distinct_functions_have_distinct_cids
- compose_two_pure_contracts_succeeds
- compose_refuses_impure_contract
- compose_refuses_out_of_bounds_formal_idx
- result_var_name_is_cid_namespaced
- effects_stable_across_runs
Phase 4 (n-ary chain composition) and Phase 5 (iterator-chain
detection) remain. Those build on the binary compose primitive
landed here.
Closes a chunk of #376.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…phase 4-6)
The remaining three phases of pure-function bundle compression.
Phase 4 — N-ary chain composition:
- compose_with_composed(outer, inner: ComposedFunctionContract,
formal_idx) — extends the binary primitive to allow successive
composition while preserving the composed CID through the fold.
- compose_chain_contracts(steps: &[ChainStep]) — left-fold of an
arbitrary-length chain. First step is the chain's source; each
subsequent step's contract receives the previous step's result
at its formal_idx-th formal.
- find_namespaced_result(formula) — finds CID-namespaced result
equations in already-composed contracts so the chain keeps
composing without renaming clashes.
Phase 5 — iterator-chain detection (chain.rs):
- detect_method_chain(expr) — walks consecutive Expr::MethodCall
nodes to extract the chain in source order. Returns None for
non-chains or single-call expressions.
- compose_method_chain(chain, registry) — looks up each method's
contract in a HashMap registry, composes the chain via
formal_idx=0 (methods normalize as method(receiver, ...args)).
- 5 unit tests including a chain-collapse-to-single-CID assertion.
Phase 6 — demo binary extension (Demo 4):
- Builds three function contracts: pure `double`, pure `inc`,
impure `shout` (println! → Io effect).
- Composes pure pairs (double ∘ inc) → ✓ composed CID.
- Tries to compose pure ∘ impure (double ∘ shout) → ✓ refused.
- Composes 3-deep chain (double ∘ inc ∘ double) → ✓ single
composed CID, 3 component entries, 1694-byte JCS bundle.
- Output shows "compose for free, compress to nothing" empirically:
all three operations land in milliseconds; chains collapse to
one CID.
The substrate's edge cache now indexes function contracts by name
and composed-CID. A second program with the same iterator chain
hits the same composed CID; verification is one lookup. Year 1
heavy minting; Year 5 99% cache hit rate; Year 20 functionally free.
Tests: 86/86 green. PR #370 now contains 14 commits.
Closes phases 4-6 of #376. Remaining: substrate-side automatic
contract registry (the hand-supplied registry in chain.rs becomes
substrate-fed once the linker integrates).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
15 tasks
…its/impls (#372 part 1, #377 parts 1-4) Two issues addressed in one commit since they're independent enough. LOCUS METADATA (#372 part 1): - New `locus.rs` module: `Locus { file, line, col }` extracted from proc-macro2's span-locations feature. - FunctionContractMemento now carries a `locus` field; CIDs include locus bytes so two contracts in different files / lines have distinct CIDs even if their bodies are textually identical. - `build_function_contract_with_file(item, body_cid, file_path)` accepts an explicit file path; the original `build_function_contract` shim defaults to None for callers that don't have a file path (in-memory parses). - Tests verify line extraction and JCS canonicalization. This unblocks downstream developer-feedback paths ("compile error at <file>:<line>: missing edge from <cid> to <cid>"). Part 2 (envelope wrap via provekit-claim-envelope) deferred to a follow-up. TYPE-DECL MEMENTOS (#377 parts 1-4): - New `type_decl.rs` module: lifts every Rust type declaration (struct, enum, trait, impl block) and emits content-addressed mementos. Schema highlights: - StructDeclMemento: name + (field_name, sort) pairs - EnumDeclMemento: name + VariantMemento[] where each variant is unit / tuple(sorts) / struct((name, sort)[]) - TraitMemento: name + method-signature CIDs - MethodSignatureMemento: trait_name + method_name + formals + return_sort - ImplMemento: target_type + optional trait_name + method CIDs - Plus the impl block's methods are FunctionContractMemento entries (linked back to the impl by parent CID downstream) - lift_file_type_decls(file, file_path) → TypeDeclSet bundling all extracted mementos for a syn::File. - All mementos carry locus. - 6 tests verifying: struct fields, enum variant shapes (unit / tuple / struct), trait methods, impl method count, impl-for-trait records the trait, deterministic CIDs across runs. Tests: 94/94 green (+9 across locus + type_decl). Closes #372 part 1; closes all four parts of #377. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 5, 2026
…#372 part 2) Wraps each emitted contract memento as a v1.2 layered MintedEnvelope via provekit-claim-envelope::mint_contract. The proof.ir bundle now plugs directly into the substrate's resolve/index pipeline without a converter. - envelope.rs: wrap_function_contract + mint_args + DEV_SIGNER_SEED. Authoring is Lift { lifter: "provekit-walk", evidence: "syn-walk-v1", source_cid: contract.body_cid }. out_binding uses the contract's CID-namespaced result variable name (compose-safe). - lib.rs: re-export wrap_function_contract / mint_args / DEV_SIGNER_SEED. 5 new unit tests: - wrap_emits_layered_envelope: verifies {envelope, header, metadata} shape with kind=contract and schemaVersion=2. - wrap_is_deterministic_for_same_inputs: same inputs -> byte-equal. - different_signers_share_contract_cid: contract_cid is signer- independent (per spec 2026-05-03 contract-cid-vs-attestation-cid §1); attestation cids differ across signers as expected. - distinct_functions_produce_distinct_contract_cids. - mint_args_contract_cid_matches_wrap: contract_cid(args) == header.cid. Test count: 47 -> 52 lib unit tests, all 99 walk tests green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 5
♻️ Duplicate comments (2)
implementations/rust/provekit-walk/src/bin/walk_demo.rs (1)
92-104:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winDivision-by-zero in the cache-hit-rate print.
If
second_run_total == 0(e.g., the second run records no mementos) the format expression on lines 102–103 evaluates100.0 * 0 / 0 = NaN%. The assertion at lines 109–112 still passes (0 == 0), so the demo silently emitsNaN%and the failure mode goes unnoticed. Guard withif second_run_total > 0before printing the percentage.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/bin/walk_demo.rs` around lines 92 - 104, The second-run cache hit rate print can divide by zero when second_run_total == 0; update the block after calling run_pipeline (s_second / second_run_total / second_run_hits) to only compute/print the percentage when second_run_total > 0 (using the existing variables second_run_total and second_run_hits produced after run_pipeline and from cache), otherwise print a safe message or 0% for the hit rate; keep the existing println that shows totals/hits but wrap the percentage println in an if second_run_total > 0 guard to avoid a NaN.implementations/rust/provekit-walk/src/type_decl.rs (1)
466-480: 🛠️ Refactor suggestion | 🟠 Major | ⚡ Quick winSame
infer_sortcollapse-to-Intdefect duplicated here.This is a copy of the
infer_sortincontract.rsand inherits the same content-address-distinctness defect: every non-recognized type becomesSort::Primitive { name: "Int" }, sostruct A { x: Vec<u32> }andstruct A { x: SomeStruct }mint identical struct-decl CIDs. When you fix the contract.rs version, mirror the fix here (or, better, extract the function into a sharedcrate::sort_infermodule so both call sites can't drift).Token-string matching is also whitespace-fragile here:
&'a strtokenizes as"& 'a str"and slips through to the_→"Int"arm, while"&str"(no lifetime) is matched. Either normalize whitespace before matching or match on the parsedsyn::Typeshape.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/type_decl.rs` around lines 466 - 480, The infer_sort function in type_decl.rs currently maps any unrecognized type to Sort::Primitive { name: "Int" } and uses fragile token-string matching; change it to (1) stop collapsing unknown types to "Int" — instead derive a distinct primitive name from the actual type identifier (e.g., use the type's path segments or fallback to its token string) so Vec<u32>, SomeStruct, etc. get different Sort names; (2) replace fragile string matching for "&str" with structural matching on syn::Type (match syn::Type::Reference for &str/&'a str and syn::Type::Path for named types) or normalize whitespace before string comparisons; and (3) factor the logic into a shared function (e.g., crate::sort_infer::infer_sort) and update both infer_sort in type_decl.rs and the duplicate in contract.rs to call the shared function so they cannot drift.
🧹 Nitpick comments (14)
implementations/rust/provekit-walk/src/walk.rs (1)
466-496: ⚡ Quick winDuplicate
lift_expr_to_termbetweenwalk.rsandlift.rswith divergent semantics.
walk.rs::lift_expr_to_term(lines 473‑491) andlift.rs::lift_expr_to_term(lines 218‑408) share the same name and largely the same intent, but diverge in important ways:
- The walk version returns
IrTermalways, falling back to a<expr:…>placeholder for unrecognized shapes.- The lift version returns
Option<IrTerm>and supports a much wider expression vocabulary (binary ops, fields, indexes, methods, ranges, tuples, closures, etc.).Concretely, that means a callsite arg like
f(x + 1)is substituted as a string-token placeholder by the walker even though the lifter knows how to produceCtor("+", [x, 1]). The two semantics will keep drifting and will quietly weaken substitution fidelity downstream ofwalk_callsites_to_entry. Consider folding into one entrypoint that returnsOption, and have the walker construct a placeholder only onNone.♻️ Sketch of a unified entrypoint
-fn lift_expr_to_term(expr: &Expr) -> IrTerm { - match expr { - Expr::Lit(lit) => match &lit.lit { - Lit::Int(n) => match n.base10_parse::<i64>() { - Ok(v) => crate::wp::const_int(v), - Err(_) => placeholder_term(expr), - }, - _ => placeholder_term(expr), - }, - Expr::Path(ExprPath { path, .. }) => { - if let Some(seg) = path.segments.last() { - crate::wp::var(seg.ident.to_string()) - } else { - placeholder_term(expr) - } - } - _ => placeholder_term(expr), - } -} +fn lift_expr_to_term(expr: &Expr) -> IrTerm { + crate::lift::lift_expr_to_term(expr).unwrap_or_else(|| placeholder_term(expr)) +}implementations/rust/provekit-walk/src/bin/walk_demo.rs (1)
268-275: 💤 Low valueFalling back to
vec!["x"]masks parameter-extraction bugs.When
all_param_namesreturns empty (a callee whose params are all destructuring patterns or a zero-arg function),run_pipelineinvents a fake formal"x"and passes it intobuild_shadow_source. For the demo's curated fixtures this is unreachable, but it would silently produce a shadow-source wired against a non-existent parameter if the fixtures ever change. Either propagate the empty list (and requirebuild_shadow_sourceto handle zero formals) orpanic!with a helpful message instead of fabricating a name.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/bin/walk_demo.rs` around lines 268 - 275, The current fallback that sets formal_params to vec!["x"] when all_param_names(&callee_fn) is empty can mask bugs by fabricating a parameter; modify run_pipeline to stop inventing names: either propagate the empty Vec and update build_shadow_source to correctly handle zero formals, or replace the fallback with a clear panic! (with a helpful error message referencing the callee) so missing parameter names are caught early; locate and change the formal_params assignment in run_pipeline and adjust build_shadow_source (or add the panic) accordingly.implementations/rust/provekit-walk/src/contract.rs (3)
529-647: ⚡ Quick winEffect scan does not look inside closure bodies passed to method calls.
Expr::Closureis treated as effect-free (line 644). That's defensible if closures were never invoked, butvec.for_each(|x| println!("{}", x))and similar idioms are exactly where IO sneaks in: theMethodCallarm scansm.args(line 563), but each arg is anExpr::Closurewhose body is never visited, so the IO/panic/unsafe inside the closure escapes effect detection — andcompose_function_contractswill incorrectly accept the contract as pure.Consider descending into
Expr::Closure { body, .. }'s body when the closure is positionally an argument to a call/method-call (or unconditionally — defining a pure closure that's never called is harmless to over-tag).🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/contract.rs` around lines 529 - 647, scan_expr_for_effects currently treats Expr::Closure as always pure and doesn't descend into the closure body, so closures passed as arguments (e.g., in Call/Expr::MethodCall m.args) can hide IO/unsafe effects; update scan_expr_for_effects (the Expr::Closure match arm) to traverse the closure body (visit the body block/stmts or the body expression) the same way other blocks are scanned, so closure bodies are included in effect detection (this can be unconditional — scan the closure's body AST nodes using scan_stmt_for_effects/scan_expr_for_effects as appropriate).
773-794: 💤 Low value
find_result_equationonly walksAtomicandAnd.For the current MVP shape (
post = result = expr), this is sufficient. If lifting later produces conditional posts (Implies,Or, or guardedresult = ...under match-arm splits fromloops_and_exceptions::lift_match_arm_postconditions), this extractor will silently returnNoneand composition will refuse. Worth a TODO comment so downstream callers know the failure mode.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/contract.rs` around lines 773 - 794, find_result_equation currently only inspects IrFormula::Atomic and IrFormula::And and will silently return None for Implies, Or, or guarded/conditional equalities; add a clear TODO comment above the function (find_result_equation) stating this limitation and the failure mode (that it will return None for conditional posts such as Implies, Or, or match-arm guarded equalities produced by loops_and_exceptions::lift_match_arm_postconditions) and what callers should expect; also note intended future work to extend the extractor to traverse Implies/Or and handle guarded equalities so downstream composition can handle conditional postconditions.
169-180: 💤 Low value
result_var_nametruncates the CID tail to 12 hex chars — collision-resistant but not collision-free.48 bits of suffix is fine for a small program but technically allows namespace collisions when two contracts share a 12-char tail. Since the namespace is only ever observed locally during composition (then re-canonicalized), the consequence is ambiguous extraction in
find_namespaced_result. Using the full CID (or a documented-as-prefix-free prefix) would remove the theoretical risk at zero implementation cost.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/contract.rs` around lines 169 - 180, The current result_var_name method builds a 12-char tail from self.cid which is collision-prone; change result_var_name to use the full CID (or another documented prefix-free encoding) instead of truncating to 12 chars so names are globally unique—update the function result_var_name to return format!("result__{}", self.cid) (or an equivalent prefix-free representation) and ensure any consumer that parses these names (notably find_namespaced_result) expects and handles the full CID form rather than a 12-char suffix.implementations/rust/provekit-walk/src/chain.rs (2)
39-54: ⚡ Quick winChain detection breaks on
?,await, and parenthesized links.
detect_method_chainonly followsExpr::MethodCall { receiver, .. }. A practical iterator chain likereq.body().await.json::<T>()?.field()or(v.iter()).sum()interrupts the walk on the first non-MethodCallnode, so the chain is reported shorter than it really is (or not detected at all). For the MVP that's a coverage gap, not a correctness defect. StrippingExpr::Try,Expr::Await, andExpr::Parenfrom the receiver as you walk would meaningfully extend chain coverage at low cost.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/chain.rs` around lines 39 - 54, detect_method_chain currently only walks Expr::MethodCall and stops when encountering wrappers like Expr::Try, Expr::Await, or Expr::Paren; update the loop in detect_method_chain to normalize/strip these wrappers from the receiver before checking for Expr::MethodCall (e.g., peel Expr::Try, Expr::Await, Expr::Paren to their inner expression in a small helper or inline match) so chains like req.body().await.json()? .field() and (v.iter()).sum() are correctly followed into MethodCallStep entries; keep the existing behavior of reversing steps and returning None for short chains.
63-83: ⚡ Quick winRegistry keyed by bare method name silently fuses repeated method calls in a chain.
For a chain like
v.iter().map(f).map(g).sum(), bothmapsteps look up the sameFunctionContractMementofromregistryandcompose_method_chainhappily composes the identical contract twice — producing a result that has nothing to do with the actual program (fandgare different functions even though the surface method name matches).The MVP comment notes the registry will be replaced by a substrate query; until then, please add a test that exercises a repeated-method chain and either error out (
return Noneon duplicate-key composition) or document the limitation prominently in the public function doc, so downstream callers don't unknowingly compose against the wrong contract.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/chain.rs` around lines 63 - 83, compose_method_chain currently looks up contracts by bare method name and will silently reuse the same FunctionContractMemento for repeated MethodCallStep entries (e.g., two map calls), so modify compose_method_chain to detect duplicate method names in the incoming chain (track seen method_name from MethodCallStep while iterating) and return None immediately if a duplicate is found instead of composing the same contract twice; keep using registry.get(&step.method_name)? for lookups and then call compose_chain_contracts(&steps) only when all method_names are unique. Also add a unit test that builds a chain with two MethodCallStep entries that have the same method_name (but would represent different closures) and asserts compose_method_chain returns None to prevent silent fusion.implementations/rust/provekit-walk/src/bin/walk_rpc.rs (2)
49-84: 💤 Low valueConsider validating the
jsonrpc: "2.0"header per the JSON-RPC 2.0 spec.
handle_linecurrently dispatches purely onmethodand ignores thejsonrpcenvelope field. A non-conforming client (or an HTTP/1.0 mistake) will silently dispatch instead of getting a-32600 Invalid Request. Not a blocker for the MVP, but worth a one-line check for substrate hygiene.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/bin/walk_rpc.rs` around lines 49 - 84, The RPC handler handle_line currently ignores the "jsonrpc" envelope; add a validation early after parsing (before extracting id/method/params) that req.get("jsonrpc").and_then(|v| v.as_str()) == Some("2.0") and if not return a JSON-RPC error object with code -32600 and a short "Invalid Request" message (include the same id handling semantics as current code: use Value::Null if no id). This is a one-line check inserted in handle_line that returns the same error JSON structure used elsewhere.
138-164: 💤 Low valueDrop the unused
Vec<u8>frombuild_bundle's return type.The second tuple element is always
Vec::new()and both call sites bind it as_bytes. Returning justShadowSourcesimplifies the API and removes a dead allocation.♻️ Proposed simplification
-fn build_bundle(params: &Value) -> Result<(provekit_walk::ShadowSource, Vec<u8>), String> { +fn build_bundle(params: &Value) -> Result<provekit_walk::ShadowSource, String> { let src = params .get("src") .and_then(|v| v.as_str()) .ok_or("missing `src`")?; ... - Ok((s, Vec::new())) + Ok(s) }And update the two callers (
shadow_source,proof_ir) to bindlet s = build_bundle(params)?;.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/bin/walk_rpc.rs` around lines 138 - 164, Change build_bundle to return Result<provekit_walk::ShadowSource, String> instead of Result<(provekit_walk::ShadowSource, Vec<u8>), String>: update its signature and Ok(...) to return just s (remove Vec::new()). Then update both call sites (functions shadow_source and proof_ir) that currently do `let (s, _bytes) = build_bundle(params)?;` to simply `let s = build_bundle(params)?;` and adjust any type expectations accordingly. Ensure all uses of build_bundle and its pattern matches are updated to the single-value return.implementations/rust/provekit-walk/src/type_decl.rs (2)
354-364: 💤 Low valueSynthetic
ItemFndropsImplItemFn::defaultness.When forwarding an
ImplItem::Fnintobuild_function_contract_with_file, the constructedsyn::ItemFnomits thedefaultnesstoken (freefndoesn't carry one). For pure contract lifting this is harmless today, but thedefault fnmodifier — relevant once the substrate handles trait-default-method overrides — is silently lost from the canonical bytes. Worth either a comment noting the omission or threading defaultness into the contract memento's value.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/type_decl.rs` around lines 354 - 364, The synthetic syn::ItemFn constructed from an ImplItem::Fn drops the ImplItemFn::defaultness token, losing "default fn" info; update the code that builds the contract memento so defaultness is preserved by either (A) threading the defaultness into build_function_contract_with_file (add a parameter like defaultness: Option<Token![default]>/bool) and include it in the contract/memento canonical bytes, or (B) if you prefer minimal change, add an explicit comment at the construction site noting that defaultness is intentionally omitted; locate the creation site of syn::ItemFn in this block (pattern matching ImplItem::Fn -> synthetic) and either pass method.defaultness through to build_function_contract_with_file or add the explanatory comment.
412-433: ⚡ Quick win
lift_file_type_declsskips items inside nestedmodblocks.
Item::Modis folded into the_ => {}arm, somod inner { struct S { ... } }yields nothing in the resultingTypeDeclSet. For self-dogfooding lifts of multi-module crates this silently drops type-decl coverage. Recursing intoItem::Mod(m)whenm.contentisSome((_, items))is a one-line extension.♻️ Sketch
Item::Impl(i) => { let (impl_memento, methods) = lift_impl_block(i, file_path); out.impls.push(impl_memento); out.impl_methods.extend(methods); } + Item::Mod(m) => { + if let Some((_, items)) = &m.content { + let nested = File { shebang: None, attrs: vec![], items: items.clone() }; + let sub = lift_file_type_decls(&nested, file_path); + out.structs.extend(sub.structs); + out.enums.extend(sub.enums); + out.traits.extend(sub.traits); + out.method_signatures.extend(sub.method_signatures); + out.impls.extend(sub.impls); + out.impl_methods.extend(sub.impl_methods); + } + } _ => {}🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/type_decl.rs` around lines 412 - 433, lift_file_type_decls currently ignores nested module items by matching Item::Mod into the wildcard arm, so types inside mod blocks are dropped from the returned TypeDeclSet; update lift_file_type_decls to handle Item::Mod(m) by checking if m.content is Some((_, items)) and then iterate those items (recursively calling the same logic or extracting via a small helper that processes a slice of Item) to collect structs, enums, traits, and impls into the existing out (preserving use of lift_struct_decl, lift_enum_decl, lift_trait_decl, lift_impl_block and extending out.structs, out.enums, out.traits, out.method_signatures, out.impls, out.impl_methods accordingly) so nested module declarations are included.implementations/rust/provekit-walk/src/loops_and_exceptions.rs (3)
104-159: ⚡ Quick winNested loops at the same top-level stmt share
source_index, risking CID collision.Every recursive call to
visit_expr_for_loopspropagates the outer statement'ssource_index(lines 124, 140, 156, 163, 170, 174). If a function contains two structurally identical loops nested under one outer expression (e.g., twowhile i < n { i = i + 1; }siblings inside anif/else), the only fields differentiating theirLoopMementovalue tuples arepre_loop,mutated_vars, andkind—source_indexandfn_nameare constant. Identical inner bodies will mint identical CIDs and dedupe two distinct loops into one memento.A monotonically incrementing counter (or a path like
outer_idx.then_idx.0) preserves distinctness while staying deterministic.Also applies to: 230-264
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/loops_and_exceptions.rs` around lines 104 - 159, visit_expr_for_loops currently reuses the outer statement's source_index when recursing, which can produce identical LoopMemento CIDs for distinct nested loops; change recursive calls to compute and pass a deterministic, unique child source index (e.g., derive child_source_index from the parent source_index plus the statement position or a monotonically incrementing per-visit counter) before calling visit_expr_for_loops and when calling mint_loop_memento so each LoopMemento (created by mint_loop_memento in visit_expr_for_loops) is distinct; apply the same change to the analogous recursion sites in the other function referenced around lines 230-264 so all recursive loop-minting paths produce unique source_index values for nested siblings.
93-179: ⚡ Quick winLoop discovery misses loops inside
letinitializers andmatcharms.
extract_loop_mementosand the recursivevisit_expr_for_loopsonly descend throughStmt::Exprand the explicitBlock/Ifarms. Loops nested inside alet x = { while ... }initializer or amatcharm body are invisible to the lifter, which silently elides theirLoopMementos and degrades soundness coverage (paper 07's "every loop opaque-tagged" guarantee). Same gap exists incollect_mutated_in_stmt/collect_mutated_in_exprforStmt::LocalandExpr::Match.This is a coverage gap — output is unsound-by-omission rather than wrong — but worth closing before the MVP claims paper 07 §10 completeness.
♻️ Sketch
fn visit_expr_for_loops( ... ) { match expr { ... + Expr::Match(m) => { + visit_expr_for_loops(&m.expr, fn_name, source_index, pre_loop, out); + for arm in &m.arms { + visit_expr_for_loops(&arm.body, fn_name, source_index, pre_loop, out); + } + } _ => {} } }And in
extract_loop_mementos(andcollect_mutated_in_stmt), also handleStmt::Local(local)by descending intolocal.init.as_ref().map(|i| &*i.expr).🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/loops_and_exceptions.rs` around lines 93 - 179, extract_loop_mementos and visit_expr_for_loops only descend into Stmt::Expr and explicit blocks/ifs, so loops inside let initializers and match arms are skipped; update traversal to visit those expressions. Specifically: in extract_loop_mementos iterate Stmt::Local(local) and, when local.init.is_some(), call visit_expr_for_loops on the initializer expression; in visit_expr_for_loops add a branch for Expr::Match that iterates match.arms and visits each arm.body (and descend into Stmt::Local wherever you currently check Stmt::Expr inside blocks/ifs) so loop bodies inside initializers/arms are discovered; also update the mutation collectors (collect_mutated_vars / collect_mutated_in_stmt / collect_mutated_in_expr) to handle Stmt::Local initializer expressions and Expr::Match arms similarly so mutated-variable collection remains consistent.
300-319: 💤 Low value
arm_body_postfalls through to vacuoustrueforExpr::Block-bodied arms.Block-bodied arms like
n => { do_thing(); v }are singleExpr::Blockvalues, whichlift_expr_to_termexplicitly returnsNonefor (see line 364 in lift.rs), causing every such arm to collapse to the vacuoustruepostcondition. Consider extracting the trailing expression from block bodies (following the pattern inExpr::Asynchandling) and recursing on it before returning vacuous.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/loops_and_exceptions.rs` around lines 300 - 319, arm_body_post currently treats Expr::Block as vacuous because lift_expr_to_term returns None for blocks; modify arm_body_post to detect Expr::Block (and mirror the Expr::Async pattern) by extracting the block's trailing expression (if any) and calling lift_expr_to_term or recursing on that Expr before falling back to the vacuous IrFormula, so block-bodied arms like `n => { do_thing(); v }` produce `result = v`; use the existing lift_expr_to_term helper and ensure you return the same Atomic "=" formula when the trailing expression lifts to a term.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/rust/provekit-walk/src/bin/walk_emit.rs`:
- Around line 62-71: all_param_names currently drops non-Pat::Ident params
causing formal/actual misalignment; change all_param_names to never silently
skip params but return a Vec<String> where each parameter yields either its
Ident name or a deterministic placeholder like "__arg{index}" for
patterns/wildcards/self, so build_shadow_source/CalleeContract and
walk_callsites_to_entry receive formals with the same arity as the callee;
update any call sites expecting fewer names accordingly (or return Result/Option
if you prefer failing loudly), and ensure lift_function_precondition usage still
substitutes using these placeholder names.
In `@implementations/rust/provekit-walk/src/contract.rs`:
- Around line 754-768: The current infer_sort function collapses all
unrecognized types to Sort::Primitive { name: "Int" }, which breaks canonical
distinctness; change infer_sort (and the twin function in
type_decl.rs::infer_sort) to encode unknown/non-primitive types using their full
token-string under a distinct Sort variant so the canonical bytes remain unique
— specifically, instead of mapping _ => "Int", create a distinct marker (e.g.
Sort::Other or Sort::Named) that stores the verbatim
ty.to_token_stream().to_string() (or similar token text) so Vec<u32>, Counter,
Option<T>, &str, etc. produce different Sort representations and thus different
canonical bytes.
- Around line 297-371: compose_function_contracts uses wp::substitute_in_formula
(via substitute_in_formula) to splice the inner result into outer pre/post and
therefore inherits its lack of alpha-renaming, which can cause variable-capture
under quantifiers; after the underlying substitute_in_formula is fixed to
perform alpha-renaming on capture, add a focused unit test that constructs two
FunctionContractMemento instances where the inner result term references a
variable that is shadowed by an outer Forall/Exists, call
compose_function_contracts(outer, inner, formal_idx), and assert that the
returned ComposedFunctionContract.pre and .post are α-equivalent to the
hand-derived expected formulas (use functions like substitute_in_formula,
find_result_equation and formula_to_canonical as helpers to produce expected
canonical forms) to ensure no capture occurs.
In `@implementations/rust/provekit-walk/src/emit.rs`:
- Around line 87-99: longest_chain() is non-deterministic because it uses
HashMap and max_by_key which can pick the last-evaluated equal-length chain;
replace the HashMap with a sorted map (BTreeMap) and pick the winner
deterministically by comparing chain length then the callee_root_cid as a
tie-breaker. Concretely: change chains to std::collections::BTreeMap<String,
Vec<&crate::shadow::ShadowArrival>>, insert arrivals the same way, then choose
the max via chains.into_iter().max_by(|(cid_a, v_a),(cid_b, v_b)|
v_a.len().cmp(&v_b.len()).then_with(|| cid_a.cmp(cid_b))) and return the
Vec<&ShadowArrival> from that entry; update any call sites if necessary and add
a regression test that builds two equal-length chains to ensure stable
shadow_proof_ir_cid across runs.
- Around line 59-74: The comment above the variable composed_chain_value
incorrectly states "first complete chain" while the code actually uses
longest_chain to pick the longest chain. Update the comment to accurately
reflect that the selection rule is choosing the longest complete chain to align
the comment with the code behavior in the block where you call longest_chain and
compose_chain.
---
Duplicate comments:
In `@implementations/rust/provekit-walk/src/bin/walk_demo.rs`:
- Around line 92-104: The second-run cache hit rate print can divide by zero
when second_run_total == 0; update the block after calling run_pipeline
(s_second / second_run_total / second_run_hits) to only compute/print the
percentage when second_run_total > 0 (using the existing variables
second_run_total and second_run_hits produced after run_pipeline and from
cache), otherwise print a safe message or 0% for the hit rate; keep the existing
println that shows totals/hits but wrap the percentage println in an if
second_run_total > 0 guard to avoid a NaN.
In `@implementations/rust/provekit-walk/src/type_decl.rs`:
- Around line 466-480: The infer_sort function in type_decl.rs currently maps
any unrecognized type to Sort::Primitive { name: "Int" } and uses fragile
token-string matching; change it to (1) stop collapsing unknown types to "Int" —
instead derive a distinct primitive name from the actual type identifier (e.g.,
use the type's path segments or fallback to its token string) so Vec<u32>,
SomeStruct, etc. get different Sort names; (2) replace fragile string matching
for "&str" with structural matching on syn::Type (match syn::Type::Reference for
&str/&'a str and syn::Type::Path for named types) or normalize whitespace before
string comparisons; and (3) factor the logic into a shared function (e.g.,
crate::sort_infer::infer_sort) and update both infer_sort in type_decl.rs and
the duplicate in contract.rs to call the shared function so they cannot drift.
---
Nitpick comments:
In `@implementations/rust/provekit-walk/src/bin/walk_demo.rs`:
- Around line 268-275: The current fallback that sets formal_params to vec!["x"]
when all_param_names(&callee_fn) is empty can mask bugs by fabricating a
parameter; modify run_pipeline to stop inventing names: either propagate the
empty Vec and update build_shadow_source to correctly handle zero formals, or
replace the fallback with a clear panic! (with a helpful error message
referencing the callee) so missing parameter names are caught early; locate and
change the formal_params assignment in run_pipeline and adjust
build_shadow_source (or add the panic) accordingly.
In `@implementations/rust/provekit-walk/src/bin/walk_rpc.rs`:
- Around line 49-84: The RPC handler handle_line currently ignores the "jsonrpc"
envelope; add a validation early after parsing (before extracting
id/method/params) that req.get("jsonrpc").and_then(|v| v.as_str()) ==
Some("2.0") and if not return a JSON-RPC error object with code -32600 and a
short "Invalid Request" message (include the same id handling semantics as
current code: use Value::Null if no id). This is a one-line check inserted in
handle_line that returns the same error JSON structure used elsewhere.
- Around line 138-164: Change build_bundle to return
Result<provekit_walk::ShadowSource, String> instead of
Result<(provekit_walk::ShadowSource, Vec<u8>), String>: update its signature and
Ok(...) to return just s (remove Vec::new()). Then update both call sites
(functions shadow_source and proof_ir) that currently do `let (s, _bytes) =
build_bundle(params)?;` to simply `let s = build_bundle(params)?;` and adjust
any type expectations accordingly. Ensure all uses of build_bundle and its
pattern matches are updated to the single-value return.
In `@implementations/rust/provekit-walk/src/chain.rs`:
- Around line 39-54: detect_method_chain currently only walks Expr::MethodCall
and stops when encountering wrappers like Expr::Try, Expr::Await, or
Expr::Paren; update the loop in detect_method_chain to normalize/strip these
wrappers from the receiver before checking for Expr::MethodCall (e.g., peel
Expr::Try, Expr::Await, Expr::Paren to their inner expression in a small helper
or inline match) so chains like req.body().await.json()? .field() and
(v.iter()).sum() are correctly followed into MethodCallStep entries; keep the
existing behavior of reversing steps and returning None for short chains.
- Around line 63-83: compose_method_chain currently looks up contracts by bare
method name and will silently reuse the same FunctionContractMemento for
repeated MethodCallStep entries (e.g., two map calls), so modify
compose_method_chain to detect duplicate method names in the incoming chain
(track seen method_name from MethodCallStep while iterating) and return None
immediately if a duplicate is found instead of composing the same contract
twice; keep using registry.get(&step.method_name)? for lookups and then call
compose_chain_contracts(&steps) only when all method_names are unique. Also add
a unit test that builds a chain with two MethodCallStep entries that have the
same method_name (but would represent different closures) and asserts
compose_method_chain returns None to prevent silent fusion.
In `@implementations/rust/provekit-walk/src/contract.rs`:
- Around line 529-647: scan_expr_for_effects currently treats Expr::Closure as
always pure and doesn't descend into the closure body, so closures passed as
arguments (e.g., in Call/Expr::MethodCall m.args) can hide IO/unsafe effects;
update scan_expr_for_effects (the Expr::Closure match arm) to traverse the
closure body (visit the body block/stmts or the body expression) the same way
other blocks are scanned, so closure bodies are included in effect detection
(this can be unconditional — scan the closure's body AST nodes using
scan_stmt_for_effects/scan_expr_for_effects as appropriate).
- Around line 773-794: find_result_equation currently only inspects
IrFormula::Atomic and IrFormula::And and will silently return None for Implies,
Or, or guarded/conditional equalities; add a clear TODO comment above the
function (find_result_equation) stating this limitation and the failure mode
(that it will return None for conditional posts such as Implies, Or, or
match-arm guarded equalities produced by
loops_and_exceptions::lift_match_arm_postconditions) and what callers should
expect; also note intended future work to extend the extractor to traverse
Implies/Or and handle guarded equalities so downstream composition can handle
conditional postconditions.
- Around line 169-180: The current result_var_name method builds a 12-char tail
from self.cid which is collision-prone; change result_var_name to use the full
CID (or another documented prefix-free encoding) instead of truncating to 12
chars so names are globally unique—update the function result_var_name to return
format!("result__{}", self.cid) (or an equivalent prefix-free representation)
and ensure any consumer that parses these names (notably find_namespaced_result)
expects and handles the full CID form rather than a 12-char suffix.
In `@implementations/rust/provekit-walk/src/loops_and_exceptions.rs`:
- Around line 104-159: visit_expr_for_loops currently reuses the outer
statement's source_index when recursing, which can produce identical LoopMemento
CIDs for distinct nested loops; change recursive calls to compute and pass a
deterministic, unique child source index (e.g., derive child_source_index from
the parent source_index plus the statement position or a monotonically
incrementing per-visit counter) before calling visit_expr_for_loops and when
calling mint_loop_memento so each LoopMemento (created by mint_loop_memento in
visit_expr_for_loops) is distinct; apply the same change to the analogous
recursion sites in the other function referenced around lines 230-264 so all
recursive loop-minting paths produce unique source_index values for nested
siblings.
- Around line 93-179: extract_loop_mementos and visit_expr_for_loops only
descend into Stmt::Expr and explicit blocks/ifs, so loops inside let
initializers and match arms are skipped; update traversal to visit those
expressions. Specifically: in extract_loop_mementos iterate Stmt::Local(local)
and, when local.init.is_some(), call visit_expr_for_loops on the initializer
expression; in visit_expr_for_loops add a branch for Expr::Match that iterates
match.arms and visits each arm.body (and descend into Stmt::Local wherever you
currently check Stmt::Expr inside blocks/ifs) so loop bodies inside
initializers/arms are discovered; also update the mutation collectors
(collect_mutated_vars / collect_mutated_in_stmt / collect_mutated_in_expr) to
handle Stmt::Local initializer expressions and Expr::Match arms similarly so
mutated-variable collection remains consistent.
- Around line 300-319: arm_body_post currently treats Expr::Block as vacuous
because lift_expr_to_term returns None for blocks; modify arm_body_post to
detect Expr::Block (and mirror the Expr::Async pattern) by extracting the
block's trailing expression (if any) and calling lift_expr_to_term or recursing
on that Expr before falling back to the vacuous IrFormula, so block-bodied arms
like `n => { do_thing(); v }` produce `result = v`; use the existing
lift_expr_to_term helper and ensure you return the same Atomic "=" formula when
the trailing expression lifts to a term.
In `@implementations/rust/provekit-walk/src/type_decl.rs`:
- Around line 354-364: The synthetic syn::ItemFn constructed from an
ImplItem::Fn drops the ImplItemFn::defaultness token, losing "default fn" info;
update the code that builds the contract memento so defaultness is preserved by
either (A) threading the defaultness into build_function_contract_with_file (add
a parameter like defaultness: Option<Token![default]>/bool) and include it in
the contract/memento canonical bytes, or (B) if you prefer minimal change, add
an explicit comment at the construction site noting that defaultness is
intentionally omitted; locate the creation site of syn::ItemFn in this block
(pattern matching ImplItem::Fn -> synthetic) and either pass method.defaultness
through to build_function_contract_with_file or add the explanatory comment.
- Around line 412-433: lift_file_type_decls currently ignores nested module
items by matching Item::Mod into the wildcard arm, so types inside mod blocks
are dropped from the returned TypeDeclSet; update lift_file_type_decls to handle
Item::Mod(m) by checking if m.content is Some((_, items)) and then iterate those
items (recursively calling the same logic or extracting via a small helper that
processes a slice of Item) to collect structs, enums, traits, and impls into the
existing out (preserving use of lift_struct_decl, lift_enum_decl,
lift_trait_decl, lift_impl_block and extending out.structs, out.enums,
out.traits, out.method_signatures, out.impls, out.impl_methods accordingly) so
nested module declarations are included.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 6436f93f-e063-4463-bd2f-7d4845059e4e
📒 Files selected for processing (16)
implementations/rust/provekit-walk/Cargo.tomlimplementations/rust/provekit-walk/src/bin/walk_demo.rsimplementations/rust/provekit-walk/src/bin/walk_emit.rsimplementations/rust/provekit-walk/src/bin/walk_rpc.rsimplementations/rust/provekit-walk/src/chain.rsimplementations/rust/provekit-walk/src/contract.rsimplementations/rust/provekit-walk/src/emit.rsimplementations/rust/provekit-walk/src/lib.rsimplementations/rust/provekit-walk/src/lift.rsimplementations/rust/provekit-walk/src/locus.rsimplementations/rust/provekit-walk/src/loops_and_exceptions.rsimplementations/rust/provekit-walk/src/type_decl.rsimplementations/rust/provekit-walk/src/walk.rsimplementations/rust/provekit-walk/tests/destructuring_demo.rsimplementations/rust/provekit-walk/tests/language_coverage.rsimplementations/rust/provekit-walk/tests/lift_dogfood.rs
✅ Files skipped from review due to trivial changes (1)
- implementations/rust/provekit-walk/Cargo.toml
🚧 Files skipped from review as they are similar to previous changes (1)
- implementations/rust/provekit-walk/src/lib.rs
…undness) Issue #368 step 4 says "Assign(local, rhs): substitute rhs for local in the WP." That's standard capture-avoiding substitution from the logician's playbook. The previous implementation respected SHADOWING (no recurse when bound == var_name) but ignored CAPTURE (bound name appears free in the replacement term). Classic miscompile: subst[x := y](∀y. P(x, y)) naive -> ∀y. P(y, y) -- y captured correct -> ∀y_1. P(y, y_1) -- alpha-rename binder first The keystone of paper 07's §5 structural-elimination theorem rides on sound substitution. AST-level naive substitution is unsound on Rust expressions with shadowing, closures, and let chains. Per Sir's "Supra omnia, rectum" — fix it before merge. Changes - wp.rs: add free_vars_term / free_vars_formula. Sequential let semantics: bindings[i] sees names bound by bindings[0..i]. - wp.rs: add fresh_name(taken, base) — biased toward `base`, increments past collisions with names already in scope. - wp.rs: substitute_in_formula and substitute_in_term now alpha-rename the binder when its bound name appears free in the replacement before substituting through. Covers all five binders: Forall, Exists, Choice, Lambda, Let. - lib.rs: re-export free_vars_term / free_vars_formula. Tests (10 new, all passing) - free_vars on Var, Lambda, sequential Let, Forall. - Capture-avoidance for Forall, Exists, Lambda, Let. - No-rename fast path when replacement is closed. - Fresh-name picker increments past collisions with other free vars. - Existing 52 unit tests + 47 integration tests stay green (capture-avoidance is a no-op on inputs that don't trigger capture, so existing CIDs are unchanged). Test count: 52 -> 62 lib unit tests, all 109 walk tests green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…e element projections (#383) Task 1 — Struct field access (Adt projection): - Added `LlbcCrate::type_decls_raw()` to expose the crate's type_decls JSON for field name resolution. - Added `lift_llbc_function_with_types()` accepting `Option<&Value>` type_decls; `lift_llbc_function` delegates to it with `None` (backward compatible, no callers broken). - Extended `place_to_term_for_post` to handle: - `Projection(base, Deref)`: transparent — needed for `&Point` references where the LLBC place chain is Deref-then-Field. - `Projection(base, Field(Adt(adt_id, _), idx))`: resolves source field name from `type_decls[adt_id].kind.Struct[idx].name`, emits `Ctor("field", [base_term, Var(".x")])`. Achieves byte equality with AST's `Expr::Field(Named)` arm. - Added `adt_field_name(type_decls, adt_id, field_idx)` helper. - Updated `marriage.rs` `lift_marriage` and `build_layers` to use `lift_llbc_function_with_types` with `krate.type_decls_raw()`. Task 2 — General tuple element projection: - Extended `place_to_term_for_post` Field(Tuple, idx) path: the CheckedOp shortcut (emit bare arithmetic ctor) is now only taken when `idx == 0` AND the base local's rvalue is a BinaryOp with a recognized arithmetic op. All other cases fall through to the general path emitting `Ctor("field", [base_term, Var(".N")])`, matching AST's `Expr::Field(Unnamed(idx))` arm byte-for-byte. - CheckedOp test (`marriage_on_overflow_arithmetic_surfaces_mir_extras`) passes unchanged; the shortcut still fires for CheckedMul + index 0. Fixtures added: struct_field.rs/.llbc, tuple_field.rs/.llbc Tests added: 6 new (4 in llbc_lift, 2 in marriage). 140 -> 148 total. Field name resolution: full source names (`.x`) achieved via type_decls lookup. Fallback to index notation when type_decls absent or ADT opaque. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
# Conflicts: # implementations/rust/provekit-walk/src/llbc_lift.rs
The keystone unlock for non-leaf substrate composition. Until this
landed, only leaf functions (no calls in body) lifted; every Call
statement was opaque, the caller's pre couldn't see callee
preconditions, and paper 07 §6's "compose for free" was an
algebraic claim with no operational backing.
Now: at every Call site in a caller's body, the callee's content-
addressed pre is substituted with actuals at that callsite (via the
capture-avoiding `wp::substitute_in_formula` we built earlier for
the AST walk) and the result is conjoined into the caller's pre
contributions. Two functions, one substitution, one merged record.
The substrate is operationally compositional.
Empirical proof in the fixture:
fn inner(y: u32) -> u32 { if y < 5 { panic!(); } y }
fn outer(x: u32) -> u32 { inner(x) }
inner.pre = (y ≥ 5) [if-panic contraposition]
outer.pre = (x ≥ 5) [inner.pre with y → x]
The lifter resolves `Call(func: Regular { kind: Fun { Regular: 1 } }, args: [Move(_2)])`
by looking up FunDeclId 1 in `translated.fun_decls`, getting the
trailing Ident "inner", consulting the registry, lifting `Move(_2)`
to `Var("x")` via the existing operand tracer, and substituting
`y -> Var("x")` in inner.pre.
Changes
- llbc_calls.rs: new module. ContractRegistry =
HashMap<String, FunctionContractMemento>. lift_llbc_crate
orchestrator iterates fun_decls building the registry. Helpers:
fundecl_name_by_id, extract_call_target, compose_callsite_pre.
- llbc.rs: + raw_translated() accessor.
- llbc_lift.rs: new lift_llbc_function_with_registry takes
ContractRegistry + fun_decls and threads them through to
collect_call_contributions. Existing entry points
(lift_llbc_function, lift_llbc_function_with_types) stay backward-
compatible by passing an empty registry.
- llbc_lift.rs: collect_call_contributions walks body, looks up
callees, substitutes formals→actuals, pushes composed pre into
caller's pre_contribs. Unresolved callees (FFI, dyn, generics
not in registry) are skipped silently for now; future work emits
Effect::UnresolvedCall so the substrate refuses composition rather
than implicitly assuming `true`.
- lib.rs: + pub mod llbc_calls.
- tests/fixtures/calls.rs / calls.llbc: vendored two-function
fixture with outer calling inner.
Tests (2 new lib unit, all passing)
- lift_llbc_crate_builds_registry_for_calls_fixture: full pipeline.
outer.pre references x (NOT y — formal substituted away) and
carries the ≥ predicate from inner.
- compose_callsite_pre_substitutes_formal_to_actual: direct unit
on the composition primitive against a synthetic callee.
Test count: 99 -> 101 lib unit, all 151 walk tests green.
Open follow-ups in #383
- Post-side: derive `result = inner(x)` from outer's _0 :=
Call(inner, [_2]) shape (currently Call doesn't fall through the
Assign-tracer in derive_return_equation; needs Call-aware
return-value derivation).
- Effect::UnresolvedCall emission for callees not in the registry.
- Recursive functions: first-pass sees empty entry; need fixed-point
re-lift or separate the lift order via SCC.
- Method calls (Trait dispatch): Call.func.Regular.kind.Method
shape requires resolving the impl + erased self.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…383) Task A: Add `detect_effects_llbc` to `llbc_lift.rs` that scans LLBC body statements for `Abort` (maps to `Effect::Panics`) and I/O callees by name (maps to `Effect::Io`). Called from `lift_llbc_function_with_registry` before `override_formulas` so the CID incorporates the effect set. Pure functions (no Abort, no I/O) remain `EffectSet::empty()`. Task B: `collect_call_contributions` now accepts an `&mut EffectSet` and emits `Effect::UnresolvedCall { name }` for any callee that resolves by name but is absent from the registry. Callers lifting with an empty registry (e.g. cross-crate) will surface these in the contract's effect set rather than silently assuming `true`. Boy-scout fixes: pre-existing broken state in `llbc_calls.rs` tests — missing closing brace on `compose_callsite_pre_substitutes_formal_to_actual` and unicode curly-quote literals in `fixpoint_lift_is_stable_after_two_passes` and `outer_post_references_call_inner` — now correct ASCII quotes so the test module compiles. New fixtures committed (generated by previous agent, referenced by existing tests): fixpoint, match_arms, closure_capture, enum_field, question_op, trait_method. Test count: 151 pass (baseline 131 + 3 new effect tests). No tests updated for effect changes — existing tests assert pre/post atoms only; marriage compares pre/post bytes, not effects, so no agreement assertions change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…h-arm marriage (#383) Task A (trait dispatch doc): Investigated Charon's encoding of monomorphic trait calls. `s.m()` where `s: &S` resolves to `Fun.Regular = <FunDeclId>` already handled by `extract_call_target`. Added fixture `trait_method.rs/.llbc` and inline doc confirming dyn dispatch is the only unhandled case (skipped cleanly via `None`). Task B (call-dest return derivation): Extended `derive_return_equation` to also scan for `Call(callee, args, dest: _0)` -- the MIR shape when a fn returns a call's result directly. Lifts to `result = Ctor("call:<name>", args)`. Added `call_dest_local()` helper in `llbc_calls.rs`. AST walk has no `Expr::Call` so this is LlbcExtra. Test: `outer_post_references_call_inner`. Task C (fix-point lift): Replaced single-pass `lift_llbc_crate` with a fix-point loop capped at MAX_LIFT_PASSES=10. Each pass re-lifts all fns against the updated registry; terminates when all CIDs stabilize. Handles forward-reference and mutual-recursion patterns. Added `fixpoint.rs/.llbc` fixture + `fixpoint_lift_is_stable_after_two_passes` test. Also commits: match-arm marriage test (marriage.rs) for SwitchInt multi-arm Abort -> LlbcExtra agreement, and extended llbc_lift with effects detection, match-arm lift, empty-registry UnresolvedCall effect (staged work on branch). Tests: 151 -> 157. All 157 pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Completes the Unsafe-detection lane that the parallel effects agent started. Charon records `signature.is_unsafe` on each FunDecl JSON; the body-statement scan can't see it because the unsafe-ness is declared at the function signature, not in any one statement. So the lifter injects Effect::Unsafe at the function-level boundary where it has the full LlbcFunction. Changes - llbc.rs: + LlbcFunction::is_unsafe() — reads signature.is_unsafe with default false (older Charon versions or non-unsafe functions). - llbc_lift.rs: lift_llbc_function_with_registry calls f.is_unsafe() after detect_effects_llbc and injects Effect::Unsafe when true. - llbc_lift.rs: new test detect_effects_llbc_emits_unsafe_for_unsafe_fn uses `drop_in_place` from closure_capture.llbc (it's an intrinsic with is_unsafe=true) to assert Effect::Unsafe lands in the contract's effect set. Test count: 162 -> 163 lib unit tests, all passing. Closes the effects-parity lane (#383 item 2 + 7) — LLBC effect set now matches the AST walk's Reads/Writes/Io/Unsafe/Panics/UnresolvedCall detection. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Per paper 07 §11, loops are deferred proof obligations. The lifter
detects each loop, content-addresses its body shape (loop_cid), and
emits Effect::OpaqueLoop. The substrate's verifier refuses to compose
a contract carrying OpaqueLoop until a separable LoopInvariantMemento
keyed by loop_cid is supplied — invariant + decreasing function. No
silent assumptions of well-behavedness.
What's in
- contract.rs: + Effect::OpaqueLoop { loop_cid }. Updated to_value
emits {"kind": "opaque_loop", "loopCid": <cid>}. Updated sort_key
for stable canonical encoding (slot "6" after UnresolvedCall).
- llbc_loops.rs: new module. extract_loops walks body statements
(recursing into Switch::If branches, Switch::SwitchInt arms, and
Loop bodies for nested loops) and returns a LoopFingerprint per
Loop. loop_cid computes the JCS-byte BLAKE3-512 hash of the loop's
block — the same canonicalizer used everywhere else. locus_of_block
best-effort extracts source position from the block's span.
- llbc_lift.rs: lift_llbc_function_with_registry runs extract_loops
on the body and adds Effect::OpaqueLoop { loop_cid } per detected
loop, between the unsafe-detection and call-composition steps.
- bin/walk_demo.rs: + match arm for OpaqueLoop in effects formatter
(prints opaque_loop(<first 16 chars of cid>) for readability).
- lib.rs: + pub mod llbc_loops.
- tests/fixtures/loops.rs / loops.llbc: 8-line `fn s(n: u32) -> u32`
with a `while i < n { ... }` summation loop.
What's NOT in (intentionally)
- The LoopInvariantMemento spec + minting tooling. That belongs in
provekit-claim-envelope as a normative substrate addition. Tracked
separately. The lift's job ends at "this is opaque, here's its CID."
- Any predicate atoms FROM the loop body. Asserts inside a loop hold
per-iteration — they're part of the invariant, not the function's
entry-level pre. Conservative.
- Bounded-unrolling shortcut for `for i in 0..K`. Adds a code path;
ship without first.
Tests (3 new lib unit, all passing)
- extract_loops returns one fingerprint for the while-loop fixture
with a well-formed cid + non-zero locus line.
- loop_cid is deterministic across calls.
- Loopless functions (clean.llbc) return an empty fingerprint vec.
Test count: 113 -> 116 lib unit, all 166 walk tests green.
Closes the 10th of the Tier 1/2 completeness items (#383). Of the
ten: 7 implemented, 2 honest skips with documented Charon-encoding
reasons, 1 (loops) now landed as OpaqueLoop opacity. Remaining
expansion lanes (Tier 3+) tracked separately.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 5
♻️ Duplicate comments (1)
implementations/rust/provekit-walk/src/contract.rs (1)
772-785:⚠️ Potential issue | 🟠 Major | ⚡ Quick winDon't collapse unknown Rust types to
Int.The
_ => "Int"fallback still makes distinct signatures likeVec<u32>,&[u8],Counter, andOption<T>hash into the sameformalSorts/returnSort. That breaks CID distinctness for the contract layer.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/contract.rs` around lines 772 - 785, The infer_sort function collapses all unknown Rust types to the same Sort::Primitive "Int", breaking CID distinctness; change the fallback to derive a distinct sort name from the type token (e.g., use the trimmed token string or a prefixed form like "Unknown::<{s}>" instead of the literal "Int") so that types such as Vec<u32>, &[u8], Counter, Option<T> produce unique Sort::Primitive names; update the match's _ arm in infer_sort to construct Sort::Primitive { name: derived_name } rather than defaulting to "Int".
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/rust/provekit-walk/src/contract.rs`:
- Around line 661-662: The match arm for Expr::Closure currently ignores effects
inside closures (Expr::Closure(_) => {}); update it to traverse and analyze the
closure body before treating the closure as pure by extracting the closure's
body expression (handle both block and expression-bodied closures), and call the
existing expression-effect analysis/visitor (e.g., the same function used for
other Expr variants) on that body so any side-effects or impure calls inside the
closure are recorded; ensure you use the closure node's fields (body/block)
rather than skipping the variant entirely and preserve existing handling for
closure parameters/captures if relevant.
In `@implementations/rust/provekit-walk/src/llbc_calls.rs`:
- Around line 37-41: The ContractRegistry is keyed by the trailing Ident
(ContractRegistry type) which collides for a::inner, b::inner, and impl methods;
change the registry key to a unique symbol (e.g., a DefId/DefPathHash or a
fully-qualified path including module/impl owner) instead of String, update the
places that build and query keys (notably fundecl_name_by_id() so it returns the
unique key type), and update all insert/lookup code to use that unique key to
prevent contract overwrites and incorrect callsite substitution.
In `@implementations/rust/provekit-walk/src/llbc_lift.rs`:
- Around line 1218-1229: The backward scan in find_last_assign_rvalue
incorrectly uses the `?` on place_to_local_id(&arr[0]) which aborts the entire
search when encountering non-local writes (like projections); change that to
explicitly match the result (e.g., `if let Some(assigned_local) =
place_to_local_id(&arr[0]) { ... } else { continue; }`) so the loop skips
non-local assignments and continues scanning prior for the given `local`.
- Around line 1308-1312: synth_item_fn currently hard-codes every formal to
"i64" and omits the return type; change it to generate accurate Rust types from
the formals' sort code and include the return sort in the signature: use the u32
sort id in each tuple in formals to map to the correct Rust type (e.g. via a
small helper like sort_to_rust_type(sort_id) or re-use your existing sort->type
mapping), build formal_args from those mapped types instead of always "i64", add
a return_sort parameter (e.g. Option<u32> or u32) and append "->
<mapped_return_type>" to src so the synthesized signature reflects both
formal_sorts and return_sort rather than defaulting to Unit.
In `@implementations/rust/provekit-walk/src/marriage.rs`:
- Around line 132-137: The merged contract currently replaces only pre/post but
drops LLBC-only effects; in marry() where you create `let mut merged =
ast.clone(); merged.pre = merged_pre; merged.post = merged_post;` ensure you
also merge/union the effects from the AST and the new pre/post into `merged`
(i.e., include any effects present on `merged_pre`/`merged_post` and the
original `ast` such as `Effect::Unsafe`) before calling
`crate::contract::build_memento_value(&merged)` so that `merged` carries the
combined effect set used for `merged.canonical_bytes`/`merged.cid`.
---
Duplicate comments:
In `@implementations/rust/provekit-walk/src/contract.rs`:
- Around line 772-785: The infer_sort function collapses all unknown Rust types
to the same Sort::Primitive "Int", breaking CID distinctness; change the
fallback to derive a distinct sort name from the type token (e.g., use the
trimmed token string or a prefixed form like "Unknown::<{s}>" instead of the
literal "Int") so that types such as Vec<u32>, &[u8], Counter, Option<T> produce
unique Sort::Primitive names; update the match's _ arm in infer_sort to
construct Sort::Primitive { name: derived_name } rather than defaulting to
"Int".
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: e644ffb1-94e8-4564-8b56-0774ac084c04
⛔ Files ignored due to path filters (1)
implementations/rust/Cargo.lockis excluded by!**/*.lock
📒 Files selected for processing (42)
implementations/rust/provekit-walk/Cargo.tomlimplementations/rust/provekit-walk/src/charon_runner.rsimplementations/rust/provekit-walk/src/contract.rsimplementations/rust/provekit-walk/src/lib.rsimplementations/rust/provekit-walk/src/llbc.rsimplementations/rust/provekit-walk/src/llbc_calls.rsimplementations/rust/provekit-walk/src/llbc_lift.rsimplementations/rust/provekit-walk/src/marriage.rsimplementations/rust/provekit-walk/tests/fixtures/bitwise.llbcimplementations/rust/provekit-walk/tests/fixtures/bitwise.rsimplementations/rust/provekit-walk/tests/fixtures/bounds.llbcimplementations/rust/provekit-walk/tests/fixtures/bounds.rsimplementations/rust/provekit-walk/tests/fixtures/calls.llbcimplementations/rust/provekit-walk/tests/fixtures/calls.rsimplementations/rust/provekit-walk/tests/fixtures/cast.llbcimplementations/rust/provekit-walk/tests/fixtures/cast.rsimplementations/rust/provekit-walk/tests/fixtures/clean.llbcimplementations/rust/provekit-walk/tests/fixtures/clean.rsimplementations/rust/provekit-walk/tests/fixtures/closure_capture.llbcimplementations/rust/provekit-walk/tests/fixtures/closure_capture.rsimplementations/rust/provekit-walk/tests/fixtures/compound_or.llbcimplementations/rust/provekit-walk/tests/fixtures/compound_or.rsimplementations/rust/provekit-walk/tests/fixtures/divmod.llbcimplementations/rust/provekit-walk/tests/fixtures/divmod.rsimplementations/rust/provekit-walk/tests/fixtures/enum_field.llbcimplementations/rust/provekit-walk/tests/fixtures/enum_field.rsimplementations/rust/provekit-walk/tests/fixtures/fixpoint.llbcimplementations/rust/provekit-walk/tests/fixtures/fixpoint.rsimplementations/rust/provekit-walk/tests/fixtures/match_arms.llbcimplementations/rust/provekit-walk/tests/fixtures/match_arms.rsimplementations/rust/provekit-walk/tests/fixtures/multihop.llbcimplementations/rust/provekit-walk/tests/fixtures/multihop.rsimplementations/rust/provekit-walk/tests/fixtures/overflow.llbcimplementations/rust/provekit-walk/tests/fixtures/overflow.rsimplementations/rust/provekit-walk/tests/fixtures/question_op.llbcimplementations/rust/provekit-walk/tests/fixtures/question_op.rsimplementations/rust/provekit-walk/tests/fixtures/struct_field.llbcimplementations/rust/provekit-walk/tests/fixtures/struct_field.rsimplementations/rust/provekit-walk/tests/fixtures/trait_method.llbcimplementations/rust/provekit-walk/tests/fixtures/trait_method.rsimplementations/rust/provekit-walk/tests/fixtures/tuple_field.llbcimplementations/rust/provekit-walk/tests/fixtures/tuple_field.rs
✅ Files skipped from review due to trivial changes (26)
- implementations/rust/provekit-walk/tests/fixtures/multihop.rs
- implementations/rust/provekit-walk/tests/fixtures/clean.rs
- implementations/rust/provekit-walk/tests/fixtures/question_op.rs
- implementations/rust/provekit-walk/tests/fixtures/divmod.llbc
- implementations/rust/provekit-walk/tests/fixtures/calls.llbc
- implementations/rust/provekit-walk/tests/fixtures/cast.llbc
- implementations/rust/provekit-walk/tests/fixtures/trait_method.rs
- implementations/rust/provekit-walk/tests/fixtures/overflow.rs
- implementations/rust/provekit-walk/tests/fixtures/trait_method.llbc
- implementations/rust/provekit-walk/tests/fixtures/tuple_field.llbc
- implementations/rust/provekit-walk/tests/fixtures/fixpoint.llbc
- implementations/rust/provekit-walk/tests/fixtures/clean.llbc
- implementations/rust/provekit-walk/tests/fixtures/bitwise.rs
- implementations/rust/provekit-walk/tests/fixtures/match_arms.llbc
- implementations/rust/provekit-walk/tests/fixtures/closure_capture.llbc
- implementations/rust/provekit-walk/tests/fixtures/match_arms.rs
- implementations/rust/provekit-walk/tests/fixtures/fixpoint.rs
- implementations/rust/provekit-walk/tests/fixtures/enum_field.llbc
- implementations/rust/provekit-walk/tests/fixtures/overflow.llbc
- implementations/rust/provekit-walk/tests/fixtures/multihop.llbc
- implementations/rust/provekit-walk/tests/fixtures/bitwise.llbc
- implementations/rust/provekit-walk/tests/fixtures/cast.rs
- implementations/rust/provekit-walk/tests/fixtures/struct_field.rs
- implementations/rust/provekit-walk/tests/fixtures/struct_field.llbc
- implementations/rust/provekit-walk/tests/fixtures/compound_or.llbc
- implementations/rust/provekit-walk/tests/fixtures/tuple_field.rs
🚧 Files skipped from review as they are similar to previous changes (2)
- implementations/rust/provekit-walk/src/lib.rs
- implementations/rust/provekit-walk/Cargo.toml
Comment on lines
+661
to
+662
| // Pure expression shapes — no effects to add. | ||
| Expr::Lit(_) | Expr::Path(_) | Expr::Closure(_) => {} |
There was a problem hiding this comment.
Scan closure bodies before treating higher-order calls as pure.
Expr::Closure(_) => {} means effects inside closures are ignored. A function like xs.iter().map(|x| { println!("{x}"); x }) stays pure here because map is whitelisted and the closure body is never inspected, which can incorrectly allow composition of impure contracts.
Suggested fix
- // Pure expression shapes — no effects to add.
- Expr::Lit(_) | Expr::Path(_) | Expr::Closure(_) => {}
+ Expr::Closure(c) => scan_expr_for_effects(&c.body, set),
+ // Pure expression shapes — no effects to add.
+ Expr::Lit(_) | Expr::Path(_) => {}📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| // Pure expression shapes — no effects to add. | |
| Expr::Lit(_) | Expr::Path(_) | Expr::Closure(_) => {} | |
| Expr::Closure(c) => scan_expr_for_effects(&c.body, set), | |
| // Pure expression shapes — no effects to add. | |
| Expr::Lit(_) | Expr::Path(_) => {} |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/contract.rs` around lines 661 - 662,
The match arm for Expr::Closure currently ignores effects inside closures
(Expr::Closure(_) => {}); update it to traverse and analyze the closure body
before treating the closure as pure by extracting the closure's body expression
(handle both block and expression-bodied closures), and call the existing
expression-effect analysis/visitor (e.g., the same function used for other Expr
variants) on that body so any side-effects or impure calls inside the closure
are recorded; ensure you use the closure node's fields (body/block) rather than
skipping the variant entirely and preserve existing handling for closure
parameters/captures if relevant.
Comment on lines
+37
to
+41
| /// Map from function name (the trailing Ident in the path) to its | ||
| /// already-lifted contract memento. Used for callsite composition: | ||
| /// when the lifter sees a Call to `f`, it looks up f's contract and | ||
| /// substitutes actuals for formals in f's pre. | ||
| pub type ContractRegistry = HashMap<String, FunctionContractMemento>; |
There was a problem hiding this comment.
Key the registry by a unique symbol, not the trailing function name.
Both the registry and fundecl_name_by_id() collapse a::inner, b::inner, and impl methods with the same trailing ident into one key. Once that happens, fixpoint lifting can overwrite contracts and callsite composition can substitute the wrong callee precondition.
Also applies to: 123-131
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/llbc_calls.rs` around lines 37 - 41,
The ContractRegistry is keyed by the trailing Ident (ContractRegistry type)
which collides for a::inner, b::inner, and impl methods; change the registry key
to a unique symbol (e.g., a DefId/DefPathHash or a fully-qualified path
including module/impl owner) instead of String, update the places that build and
query keys (notably fundecl_name_by_id() so it returns the unique key type), and
update all insert/lookup code to use that unique key to prevent contract
overwrites and incorrect callsite substitution.
Comment on lines
+1218
to
+1229
| fn find_last_assign_rvalue<'a>(prior: &[&'a Value], local: u32) -> Option<&'a Value> { | ||
| for s in prior.iter().rev() { | ||
| let Some(arr) = stmt_kind_payload(s, "Assign").and_then(|v| v.as_array()) else { | ||
| continue; | ||
| }; | ||
| if arr.len() != 2 { | ||
| continue; | ||
| } | ||
| let assigned_local = place_to_local_id(&arr[0])?; | ||
| if assigned_local == local { | ||
| return Some(&arr[1]); | ||
| } |
There was a problem hiding this comment.
Don't stop the backward scan on a non-local assignment.
place_to_local_id(&arr[0])? returns None for projection writes like (*buf).x = ..., which exits the whole search instead of skipping that statement. That makes later traces miss valid local definitions and silently drop derived pre/post atoms.
Suggested fix
fn find_last_assign_rvalue<'a>(prior: &[&'a Value], local: u32) -> Option<&'a Value> {
for s in prior.iter().rev() {
let Some(arr) = stmt_kind_payload(s, "Assign").and_then(|v| v.as_array()) else {
continue;
};
if arr.len() != 2 {
continue;
}
- let assigned_local = place_to_local_id(&arr[0])?;
+ let Some(assigned_local) = place_to_local_id(&arr[0]) else {
+ continue;
+ };
if assigned_local == local {
return Some(&arr[1]);
}
}
None
}🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/llbc_lift.rs` around lines 1218 -
1229, The backward scan in find_last_assign_rvalue incorrectly uses the `?` on
place_to_local_id(&arr[0]) which aborts the entire search when encountering
non-local writes (like projections); change that to explicitly match the result
(e.g., `if let Some(assigned_local) = place_to_local_id(&arr[0]) { ... } else {
continue; }`) so the loop skips non-local assignments and continues scanning
prior for the given `local`.
Comment on lines
+132
to
+137
| let mut merged = ast.clone(); | ||
| merged.pre = merged_pre; | ||
| merged.post = merged_post; | ||
| let value = crate::contract::build_memento_value(&merged); | ||
| merged.canonical_bytes = jcs_bytes_of_value(&value); | ||
| merged.cid = cid_of_value(&value); |
There was a problem hiding this comment.
Merged contracts currently drop LLBC-only effects.
marry() clones ast and only replaces pre/post, so any MIR-only effect never reaches merged. A simple case is an unsafe fn with no unsafe {} block: the AST side stays pure, the LLBC side carries Effect::Unsafe, and the merged contract becomes incorrectly composable.
Suggested fix
let mut merged = ast.clone();
merged.pre = merged_pre;
merged.post = merged_post;
+ for effect in &llbc.effects.effects {
+ merged.effects.add(effect.clone());
+ }
let value = crate::contract::build_memento_value(&merged);
merged.canonical_bytes = jcs_bytes_of_value(&value);
merged.cid = cid_of_value(&value);📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| let mut merged = ast.clone(); | |
| merged.pre = merged_pre; | |
| merged.post = merged_post; | |
| let value = crate::contract::build_memento_value(&merged); | |
| merged.canonical_bytes = jcs_bytes_of_value(&value); | |
| merged.cid = cid_of_value(&value); | |
| let mut merged = ast.clone(); | |
| merged.pre = merged_pre; | |
| merged.post = merged_post; | |
| for effect in &llbc.effects.effects { | |
| merged.effects.add(effect.clone()); | |
| } | |
| let value = crate::contract::build_memento_value(&merged); | |
| merged.canonical_bytes = jcs_bytes_of_value(&value); | |
| merged.cid = cid_of_value(&value); |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/marriage.rs` around lines 132 - 137,
The merged contract currently replaces only pre/post but drops LLBC-only
effects; in marry() where you create `let mut merged = ast.clone(); merged.pre =
merged_pre; merged.post = merged_post;` ensure you also merge/union the effects
from the AST and the new pre/post into `merged` (i.e., include any effects
present on `merged_pre`/`merged_post` and the original `ast` such as
`Effect::Unsafe`) before calling `crate::contract::build_memento_value(&merged)`
so that `merged` carries the combined effect set used for
`merged.canonical_bytes`/`merged.cid`.
Closes the last two honest skips. Both follow the loops pattern
(detect, content-address, emit an opacity effect). The substrate
refuses composition until a matching memento (TryBranchMemento /
closure body resolution) is supplied — no silent assumptions.
? operator
- llbc_try.rs: extract_try_branches walks body for Switch::Match
shapes. Detection: a Switch whose payload is `Match` (3+-element
array) where the discriminant traces back to a Call whose callee's
trailing Ident is "branch". That's Charon's Try::branch shape that
desugaring of `?` produces. Each detected site emits
Effect::EarlyReturn { try_cid } with the JCS-byte hash of the
Switch::Match block.
Closure captures
- llbc_closures.rs: extract_closure_captures walks for Aggregate(Adt)
rvalues whose type_decl name path ENDS in `Ident("closure")` —
that's Charon's synthetic-closure-type marker (the agent that
skipped this missed the marker). Each detected site looks up the
matching trait-impl fun_decl by path-prefix match (everything
before the "closure" element + an `Impl{...}` element + a trailing
Ident in {call, call_mut, call_once, drop_in_place}) and emits
Effect::ClosureCapture { body_fn_cid, n_captures }.
Both modules recurse into Switch::If branches, Switch::SwitchInt
arms, Switch::Match arms, and Loop bodies — nesting works.
Schema discoveries
- Try-branch isn't a standalone construct in LLBC; it's the
Switch::Match-after-Try::branch-Call shape. Detection works on
shape, not types.
- Closure aggregate's TypeDeclRef is `{"id": {"Adt": <id>}, "generics": ...}`,
not `{"Adt": <id>}` directly. Initial test caught this.
- Charon emits multiple fun_decls per closure (call/call_mut/call_once/
drop_in_place); we pick the first matching trait-impl and use its
cid as the closure-body identifier.
Changes
- contract.rs: + Effect::EarlyReturn { try_cid } and
Effect::ClosureCapture { body_fn_cid, n_captures }, with their
to_value (kind=early_return / closure_capture, payloads) and
sort_key (slots 7 and 8).
- llbc_try.rs / llbc_closures.rs: new modules with detection +
fingerprint types + tests.
- llbc_lift.rs: lift_llbc_function_with_registry runs both
detectors after the loop detector, populating effects.
- lib.rs: + pub mod llbc_try, pub mod llbc_closures.
- bin/walk_demo.rs: + match arms for the new effect variants in
the formatter.
Tests (4 new lib unit, all passing)
- extract_try_branches finds the Try-branch site in question_op fixture.
- no Try-branches in clean fixture.
- extract_closure_captures finds the closure aggregate in
closure_capture fixture; body_fn_cid resolves.
- no closure captures in clean fixture.
Test count: 116 -> 120 lib unit, all 170 walk tests green.
Closes ALL 10 of the Tier 1/2 completeness items (#383). The lifter
emits honest opacity for every Rust construct it can't fully model:
loops, ?, closures, unresolved calls, unsafe blocks. The substrate
refuses composition until matching mementos resolve them — no
silent assumptions, no pretended verification.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
After the merge with main, Sort enum has Function + Dependent variants (added by #361 for the dependent-type / first-class-function-sort grammar expansion). The walk crate's two `sort_to_value` helpers matched only Sort::Primitive — non-exhaustive after the merge, breaking the cross-language conformance gate. Both helpers now emit `{kind: "opaque", reason: "function-or-dependent-sort-not-yet-modeled"}` for the new variants. The walk crate doesn't yet PRODUCE these sorts (we always emit a plain Primitive via synth_item_fn), but this preserves the canonicalization invariant if a downstream caller passes them through. Translating Function / Dependent faithfully into the lift's IR sort encoding is tracked as #384 Tier A.1 (type-aware predicate sorts) — that's the bigger correctness bug. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… paths (#384 A.1, #370) Every formal sort and struct-field sort previously collapsed to Sort::Primitive { name: "Int" } via token-string matching on syn::Type::to_token_stream(). Two failure modes: 1. False collisions: fn f(x: u32) and fn f(x: bool) minted identical contract CIDs. struct A { x: Vec<u32> } and struct A { x: SomeStruct } minted identical struct-decl CIDs. 2. False splits: &'a str tokenised as "& 'a str" (space from lifetime) fell to the catch-all, while &str matched the explicit arm. Adding a lifetime changed the contract CID for an otherwise-identical sig. 3. LLBC lift hardcoded i64: synth_item_fn generated fn name(x: i64, ...) so even though Charon's locals table had the real type (UInt::U32, Ref<Slice<...>>), the contract formal_sorts always said Int. Fix: - New module src/sort_translate.rs with two public functions: - syn_type_to_sort(ty: &syn::Type) -> Sort: branches on syn::Type::* shape, not token strings. Lifetimes stripped. Produces rich names: "U32", "Bool", "Ref<Slice<U32>>", "Vec<U32>", "SomeStruct", etc. - ty_to_sort(ty: Option<&Value>, type_decls: Option<&Value>) -> Sort: translates Charon JSON Ty shapes. Handles Literal/UInt/SInt/Float, Ref, Slice, Array, Adt (with type_decls name resolution). Unknown shapes fall to "Unknown" (not "Int") with a TODO comment. - contract.rs: infer_sort delegates to syn_type_to_sort (removes quote::ToTokens string matching, removes the duplicate). - type_decl.rs: infer_sort delegates to syn_type_to_sort (removes the other duplicate; CodeRabbit #370 flagged this duplication). - llbc.rs: LlbcLocal gains ty_raw() -> Option<&Value> accessor. - llbc_lift.rs: - Collects all locals once into all_locals to avoid consuming the iterator twice. - Builds formal_ty_raws (index -> raw Ty JSON) for formals and return local (index 0). - After building the contract shell, overwrites contract.formal_sorts and contract.return_sort from Charon's type table via ty_to_sort. - synth_item_fn now uses () placeholders instead of i64 (dead code, but clearly intentional placeholder now). Approach: Option A (rich Sort::Primitive names). Stays within the existing Sort enum to avoid cross-kit exhaustiveness churn. Option B (proper Sort variants) is the long-term answer; tracked as a follow-up. Tests: 194 total (was 170). Added: - sort_translate: 19 unit tests covering AST/Charon agreement on primitives, lifetime invariance, distinct-type distinctness, Adt id resolution, struct name resolution via type_decls. - contract: 3 regression tests (u32 vs bool distinct CIDs, lifetime invariance, Vec vs user struct distinct). - type_decl: 2 regression tests (Vec vs SomeStruct field CIDs, u32 vs bool field CIDs). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… sort-equality marriage test
The Charon JSON format wraps every inner Ty element as {"Untagged": ...}
even when embedded inside Ref/Slice/Array/RawPtr composites. The original
sort_translate code incorrectly added a second {"Untagged": ...} wrapper
before calling ty_to_sort_name, causing Ref<Slice<U32>> to degrade to
Ref<Unknown> for all real fixture inputs (the Slice inner element never
matched because it was double-wrapped).
Fix: pass inner Ty values directly to ty_to_sort_name in the Ref, Slice,
Array, and RawPtr arms — they are already {"Untagged": ...} shaped.
Also updates the sort_translate unit test charon_ref_slice_u32_matches_syn
to use the real Charon JSON format (fully-wrapped inner Ty), and adds the
marriage-layer sort-equality test (bounds fixture, at function) that was
an explicit acceptance criterion in #384 — asserting byte-equality between
the AST path's formal_sorts and the LLBC path's formal_sorts for
`fn at(s: &[u32], i: usize) -> u32`.
Closes #384 A.1 (sort collapse), refs #370.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…370, #384) Fixes all P1/major/minor issues flagged by Copilot + CodeRabbit: walk.rs: - Bug #1: nested-block let-bindings now substituted at nested callsites; `CallsiteHit` carries `preceding_inner_stmts` (innermost-first) populated during the forward traversal; backward walk applies them before the outer- body statements. - Bug #3: actual-arg lift now delegates to `crate::lift::lift_expr_to_term` (semantic, structure-stable) instead of the old token-string fallback; binary-expr actuals produce Ctor(op, ...) not `<expr:40 + 2>` tokens. - Bug #4: arity mismatch now logs a warning and skips the callsite rather than silently zip-truncating. New test asserts the skip. - Bug #11: stale MVP-scope comment updated (if-strengthening is live). lift.rs: - Bug #5: `debug_assert!` removed from the macro match arm; it is compiled out in release builds and must not contribute to contracts. - Bug #6: `lift_function_postcondition` now scans for later `let` bindings that shadow an entry assertion's free variables and drops unsound asserts. Narrowed to LATER rebindings only (a preceding `let y = x; assert!(y ≥ 5)` is sound). - Bug #7: explicit `return expr;` tails now derive `result = <lifted expr>` postcondition (previously only trailing-no-semicolon expressions matched). canonical.rs: - Bug #8: non-i64 JSON Numbers (floats, large u64) are now encoded as a tagged object `{"__provekit_non_i64_number__": "42.5"}` instead of a plain string, preventing numeric constants and string literals of the same text from sharing a CID. walk_emit.rs / walk_demo.rs: - Bug #9: `all_param_names` now synthesizes stable placeholder names (`__self`, `__arg{i}`) for non-Ident patterns so formal arity stays aligned with actual-argument count. - Bug #10: NaN% division guarded with `if second_run_total > 0`. 11 new unit tests added (156 lib tests total, up from 145; 12 integration tests all still passing). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
emit.rs: - Bug #1: replace HashMap (RandomState, random iteration) with BTreeMap (sorted by callee_root_cid key) in longest_chain(). With HashMap, two chains of equal length produced different composedChain CIDs across runs because max_by_key kept the last maximum encountered during non-deterministic HashMap iteration. With BTreeMap the lexicographically first key always wins. Determinism test: emit 50 times from same ShadowSource with 2 equal-length chains; assert byte-equal output every time. - Bug #2: fix comment "first complete chain" -> "longest chain (stable tie-break)". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…r descent (#370 #384) Bug #1: the `Expr::If` branch in `walk_expr_for_callsites` used `truncate(prev_len)` after replacing `*inner_stmts`, which left the branch_preceding content in place for the outer caller rather than restoring the original slice. Changed to the same save/restore pattern used by the `Expr::Block` arm: `let saved = clone; *inner_stmts = branch_preceding; recurse; *inner_stmts = saved`. Bug #2: `walk_expr_for_callsites` silently dropped callsites inside `Expr::Binary`, `Expr::Unary`, `Expr::Cast`, `Expr::Paren`, `Expr::Reference`, `Expr::Field`, `Expr::Index`, `Expr::Range`, `Expr::Tuple`, `Expr::Array`, and `Expr::Assign` because all fell through to `_ => {}`. Added recursive descent arms for each. A callsite in `callee(x) + 1` or `(callee(x))` is now found. Four new tests added (two for Bug #1, two for Bug #2). Total: 160 unit tests + 12 shadow_demo + 1 lift_dogfood, all green. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 9
♻️ Duplicate comments (4)
implementations/rust/provekit-walk/src/lift.rs (3)
513-543:⚠️ Potential issue | 🟠 Major | ⚡ Quick winClosure parameter sorts are still hard-coded to
Int.
Pat::Typeis only used to recover the binder name here, and every emitted lambda getsSort::Primitive { name: "Int" }. That mis-types closures like|p: bool|or|s: &str|, which changes canonical bytes and any downstream logic that relies onparam_sort. Reusesort_translate::syn_type_to_sortfor typed params and fall back toUnknownfor untyped ones.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/lift.rs` around lines 513 - 543, The lambda param sorts are hard-coded to Int in the closure-handling block; update the binder extraction in the loop (which currently matches syn::Pat::Ident and syn::Pat::Type) to also translate typed patterns' syn types into IR sorts using sort_translate::syn_type_to_sort (when matching syn::Pat::Type use the inner pt.ty to produce the sort) and use provekit_ir_types::Sort::Unknown for untyped binders (syn::Pat::Ident) before creating IrTerm::Lambda; keep using ctx.bind(&base) for the unique names and ensure the produced param_sort is passed into IrTerm::Lambda instead of the constant Int.
156-170:⚠️ Potential issue | 🟠 Major | ⚡ Quick winLater writes still make copied assertions unsound.
The filter only drops assertions shadowed by later
letbindings. A later assignment likex = 0;keeps the same binding in scope, soassert!(x >= 5); x = 0;still contributesx ≥ 5to the postcondition even though it no longer holds. Extend the kill set to include later writes (Expr::Assign, op-assigns, etc.) to any free variable referenced by the assertion.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/lift.rs` around lines 156 - 170, The current filter in lift.rs only treats later `let` bindings as kills; extend the kill set to also include later writes (plain assignments, compound/ops, and any other assignment-like statements) so assertions whose free variables are overwritten after the assert are dropped. Update the loop that builds later_bound (used in the closure filtering entry_assertions) to call a new or extended helper (e.g., collect_assigned_names or extend collect_let_bound_names) that inspects statements for Expr::Assign, Expr::AssignOp (and similar assignment forms) and inserts the assigned variable names into later_bound; then keep the existing free.is_disjoint(&later_bound) check to decide whether to retain the IrFormula. Ensure you reference stmts, free_vars_formula, entry_assertions, collect_let_bound_names/collect_assigned_names, and IrFormula when making the change.
284-292:⚠️ Potential issue | 🟠 Major | ⚡ Quick win
assert!(cond, ..)is still dropped.
syn::parse2::<Expr>only succeeds when the entire macro token stream is one expression, soassert!(x >= 5, "msg")returnsErrbefore the tuple fallback runs. Parse the tokens as a comma-separated expression list and lift the first element as the condition.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/lift.rs` around lines 284 - 292, The "assert" arm drops assertions with additional args because syn::parse2::<Expr>(mac.tokens.clone()) fails when tokens contain a comma; change the parsing to parse a comma-separated expression list (e.g., syn::parse2::<Punctuated<Expr, Token![,]>>(mac.tokens.clone())), then take the first element of that punctuated list (or return None if empty) and pass that Expr to lift_predicate_inner; update the existing parsed_cond/first logic in the "assert" match arm to use this punctuated parse on mac.tokens and then call lift_predicate_inner(first, ctx).implementations/rust/provekit-walk/src/llbc_lift.rs (1)
1289-1303:⚠️ Potential issue | 🟠 Major | ⚡ Quick winBackward scan still aborts on non-Local Assign targets.
Line 1297 still uses
?onplace_to_local_id(&arr[0]), so any prior Assign whose place is a projection ((*p).x = ...,arr[i] = ...,Deref(local).field = ...) terminates the entire reverse scan and returnsNone— even when the target local has a perfectly recognizable Assign earlier. This silently breaks every consumer that relies on it (discriminant trace, return-equation derivation, divisor-from-cond extraction, CheckedOp shortcut), dropping pre/post atoms whenever a function contains a projection write before a use site.🛡️ Skip non-local Assigns instead of aborting
fn find_last_assign_rvalue<'a>(prior: &[&'a Value], local: u32) -> Option<&'a Value> { for s in prior.iter().rev() { let Some(arr) = stmt_kind_payload(s, "Assign").and_then(|v| v.as_array()) else { continue; }; if arr.len() != 2 { continue; } - let assigned_local = place_to_local_id(&arr[0])?; + let Some(assigned_local) = place_to_local_id(&arr[0]) else { + continue; + }; if assigned_local == local { return Some(&arr[1]); } } None }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-walk/src/llbc_lift.rs` around lines 1289 - 1303, In find_last_assign_rvalue, the backward scan currently uses the `?` on `place_to_local_id(&arr[0])` which aborts the whole function when the Assign target is a non-local place; change that to explicitly handle the Option (e.g. `if let Some(assigned_local) = place_to_local_id(&arr[0]) { ... } else { continue; }`) so non-local/ projection Assign targets are skipped and the reverse scan continues normally, returning the first rvalue whose place maps to the requested `local`.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/rust/provekit-walk/src/llbc_closures.rs`:
- Around line 228-235: The current match treats "drop_in_place" the same as
"call"/"call_mut"/"call_once" causing body_fn_cid (and Effect::ClosureCapture)
to pick a destructor if fun_decls ordering differs; change the match on
trailing_ident to only include "call" | "call_mut" | "call_once" and return the
hashed body (via serde_to_canonical(decl.clone()) and cid_of_value) only for
those three; do not treat "drop_in_place" as a call body here (handle destructor
metadata separately if/when needed).
In `@implementations/rust/provekit-walk/src/llbc_lift.rs`:
- Around line 766-774: The is_io_callee_name function currently uses broad
substring checks (lower.contains("io"), contains("print"), contains("display"))
which cause false positives; update is_io_callee_name to only match a curated
set of exact basenames and a small set of safe prefixes for known std lib I/O
names (e.g., exact matches: "print", "println", "eprint", "eprintln",
"write_fmt", "fmt"; optional safe prefixes like "write_" or "read_" if desired),
removing the generic contains(...) checks so only those exact or intentional
prefix matches mark a callee as I/O; keep the lowercase conversion and use
matches! or a HashSet/array of strings to perform the exact/prefix checks inside
is_io_callee_name.
In `@implementations/rust/provekit-walk/src/llbc_loops.rs`:
- Around line 75-99: The walker currently descends into "If" and "SwitchInt" but
skips "Switch::Match", so add handling for kind.get("Switch").get("Match")
similar to the SwitchInt branch: if let Some(match_arr) =
switch.get("Match").and_then(|v| v.as_array()) { iterate the arms array (usually
match_arr[1] or the slot that holds arms depending on your shape), for each arm
check it's an array and call recurse_block on the arm's block element (commonly
the last element of the arm array); also recurse into any explicit
"otherwise"/fallback block if the Match shape provides one. Use the same
recurse_block(&..., out) calls and mirror the defensive .as_array()/len checks
used in the existing SwitchInt handling to avoid panics. }
In `@implementations/rust/provekit-walk/src/llbc_try.rs`:
- Around line 125-168: discr_traces_to_try_branch currently walks
siblings.iter().rev() over the entire block and can pick a later assignment as
the producer of the discriminant; change its API and call sites so it only
searches statements that precede the Switch::Match (e.g. add a parameter like
start_idx or accept a slice of preceding siblings) and iterate backwards over
that prefix instead of the full siblings list; update callers to pass the
current statement index or a slice and ensure callee_is_try_branch(func_id,
fun_decls) is still used to validate the Call producer.
In `@implementations/rust/provekit-walk/src/shadow.rs`:
- Around line 328-355: The arrival payload built by arrival_value lacks a
per-callsite discriminator, causing identical callsites in the same source slot
to produce the same CID; modify arrival_value to accept and include a stable
callsite discriminator (e.g., callsite_ordinal: usize or callsite_path: &str)
and add it to the returned object (e.g., ("callsiteOrdinal",
Value::integer(...)) or ("callsitePath", Value::string(...))), update every
caller of arrival_value to supply that discriminator from the walk context, and
ensure this change happens before any CID minting (so callee_root_cid /
formula_to_canonical calls remain the same but the final object differs per
callsite).
In `@implementations/rust/provekit-walk/src/sort_translate.rs`:
- Around line 158-180: The current logic in syn_type_to_sort_name uses only the
last Path segment (variable last / ident), causing different modules' types like
foo::Point and bar::Point to collide; change it to build a stable qualified path
string from all segments (including their segment.ident and any AngleBracketed
generic arguments) instead of truncating to the last segment, and apply the same
strategy used by extract_type_decl_name so sort names include the full module
path (e.g., join segment idents with "::" and render nested generics for each
segment) while still respecting primitive_sort_name checks and existing generic
inner-type mapping.
In `@implementations/rust/provekit-walk/src/walk.rs`:
- Around line 327-342: The code in the for loop over then_branch.stmts mutates
inner_stmts and attempts to restore it incorrectly; before you overwrite
*inner_stmts with branch_preceding in the loop inside walk_stmt_for_callsites,
clone and save the original inner_stmts (e.g. let saved: Vec<Stmt> =
inner_stmts.clone()), then set *inner_stmts = branch_preceding, call
walk_stmt_for_callsites(s, callee_name, conditions, inner_stmts, hits), and
finally restore the original with *inner_stmts = saved; remove the current
truncate/clone restore sequence so outer bindings aren’t lost and branch-local
stmts don’t leak into siblings.
- Around line 380-393: The loop-handling arms for Expr::While, Expr::ForLoop,
and Expr::Loop in walk.rs call walk_stmt_for_callsites on each body statement
but fail to include the preceding loop-local let bindings (the prefix of
statements before the current one) into inner_stmts, causing
free-variable/substitution errors; change these arms to mirror Expr::Block's
behavior by iterating with indices and, for each statement s at index i, build a
prefix of the loop body stmts[0..i] and pass inner_stmts augmented with that
prefix to walk_stmt_for_callsites (i.e., thread per-statement body prefixes
through the loop arms so earlier let bindings are visible to subsequent callsite
analysis in walk_stmt_for_callsites).
In `@implementations/rust/provekit-walk/tests/fixtures/loops.rs`:
- Around line 4-7: The loop can overflow/wrap and become infinite when n ==
u32::MAX; fix by making the precondition explicit or eliminating wrap behavior:
either add a precondition/assertion such as assert!(n != u32::MAX) or assert!(n
<= u32::MAX - 1) before the while, or change arithmetic to checked forms (use i
= i.checked_add(1).expect("overflow") and total =
total.checked_add(i).expect("overflow")) or widen types (e.g., cast i/total to
u64) to avoid wrapping; locate the while loop using the variables i, n, and
total and apply one of these changes and/or add a clarifying comment explaining
the assumed bound on n.
---
Duplicate comments:
In `@implementations/rust/provekit-walk/src/lift.rs`:
- Around line 513-543: The lambda param sorts are hard-coded to Int in the
closure-handling block; update the binder extraction in the loop (which
currently matches syn::Pat::Ident and syn::Pat::Type) to also translate typed
patterns' syn types into IR sorts using sort_translate::syn_type_to_sort (when
matching syn::Pat::Type use the inner pt.ty to produce the sort) and use
provekit_ir_types::Sort::Unknown for untyped binders (syn::Pat::Ident) before
creating IrTerm::Lambda; keep using ctx.bind(&base) for the unique names and
ensure the produced param_sort is passed into IrTerm::Lambda instead of the
constant Int.
- Around line 156-170: The current filter in lift.rs only treats later `let`
bindings as kills; extend the kill set to also include later writes (plain
assignments, compound/ops, and any other assignment-like statements) so
assertions whose free variables are overwritten after the assert are dropped.
Update the loop that builds later_bound (used in the closure filtering
entry_assertions) to call a new or extended helper (e.g., collect_assigned_names
or extend collect_let_bound_names) that inspects statements for Expr::Assign,
Expr::AssignOp (and similar assignment forms) and inserts the assigned variable
names into later_bound; then keep the existing free.is_disjoint(&later_bound)
check to decide whether to retain the IrFormula. Ensure you reference stmts,
free_vars_formula, entry_assertions,
collect_let_bound_names/collect_assigned_names, and IrFormula when making the
change.
- Around line 284-292: The "assert" arm drops assertions with additional args
because syn::parse2::<Expr>(mac.tokens.clone()) fails when tokens contain a
comma; change the parsing to parse a comma-separated expression list (e.g.,
syn::parse2::<Punctuated<Expr, Token![,]>>(mac.tokens.clone())), then take the
first element of that punctuated list (or return None if empty) and pass that
Expr to lift_predicate_inner; update the existing parsed_cond/first logic in the
"assert" match arm to use this punctuated parse on mac.tokens and then call
lift_predicate_inner(first, ctx).
In `@implementations/rust/provekit-walk/src/llbc_lift.rs`:
- Around line 1289-1303: In find_last_assign_rvalue, the backward scan currently
uses the `?` on `place_to_local_id(&arr[0])` which aborts the whole function
when the Assign target is a non-local place; change that to explicitly handle
the Option (e.g. `if let Some(assigned_local) = place_to_local_id(&arr[0]) { ...
} else { continue; }`) so non-local/ projection Assign targets are skipped and
the reverse scan continues normally, returning the first rvalue whose place maps
to the requested `local`.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 36c66694-f02c-4c63-a9e2-39c9580ec2fa
📒 Files selected for processing (21)
implementations/rust/provekit-walk/src/bin/walk_demo.rsimplementations/rust/provekit-walk/src/bin/walk_emit.rsimplementations/rust/provekit-walk/src/bin/walk_rpc.rsimplementations/rust/provekit-walk/src/canonical.rsimplementations/rust/provekit-walk/src/contract.rsimplementations/rust/provekit-walk/src/emit.rsimplementations/rust/provekit-walk/src/lib.rsimplementations/rust/provekit-walk/src/lift.rsimplementations/rust/provekit-walk/src/llbc.rsimplementations/rust/provekit-walk/src/llbc_closures.rsimplementations/rust/provekit-walk/src/llbc_lift.rsimplementations/rust/provekit-walk/src/llbc_loops.rsimplementations/rust/provekit-walk/src/llbc_try.rsimplementations/rust/provekit-walk/src/marriage.rsimplementations/rust/provekit-walk/src/shadow.rsimplementations/rust/provekit-walk/src/sort_translate.rsimplementations/rust/provekit-walk/src/type_decl.rsimplementations/rust/provekit-walk/src/walk.rsimplementations/rust/provekit-walk/tests/fixtures/loops.llbcimplementations/rust/provekit-walk/tests/fixtures/loops.rsimplementations/rust/provekit-walk/tests/shadow_demo.rs
✅ Files skipped from review due to trivial changes (2)
- implementations/rust/provekit-walk/src/bin/walk_emit.rs
- implementations/rust/provekit-walk/tests/fixtures/loops.llbc
🚧 Files skipped from review as they are similar to previous changes (8)
- implementations/rust/provekit-walk/src/emit.rs
- implementations/rust/provekit-walk/src/canonical.rs
- implementations/rust/provekit-walk/src/bin/walk_rpc.rs
- implementations/rust/provekit-walk/src/llbc.rs
- implementations/rust/provekit-walk/src/marriage.rs
- implementations/rust/provekit-walk/tests/shadow_demo.rs
- implementations/rust/provekit-walk/src/contract.rs
- implementations/rust/provekit-walk/src/type_decl.rs
Comment on lines
+228
to
+235
| if matches!( | ||
| trailing_ident, | ||
| "call" | "call_mut" | "call_once" | "drop_in_place" | ||
| ) { | ||
| // Hash this fun_decl's full JSON shape as the body cid. | ||
| let canonical = serde_to_canonical(decl.clone()); | ||
| return cid_of_value(&canonical); | ||
| } |
There was a problem hiding this comment.
Don't let drop_in_place win the body lookup.
drop_in_place is a destructor, not the closure's call body. Returning the first match across call* | drop_in_place makes body_fn_cid depend on fun_decls order and can point Effect::ClosureCapture at the wrong function entirely. Prefer call / call_mut / call_once, and only treat destructor metadata separately if you need it later.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/llbc_closures.rs` around lines 228 -
235, The current match treats "drop_in_place" the same as
"call"/"call_mut"/"call_once" causing body_fn_cid (and Effect::ClosureCapture)
to pick a destructor if fun_decls ordering differs; change the match on
trailing_ident to only include "call" | "call_mut" | "call_once" and return the
hashed body (via serde_to_canonical(decl.clone()) and cid_of_value) only for
those three; do not treat "drop_in_place" as a call body here (handle destructor
metadata separately if/when needed).
Comment on lines
+766
to
+774
| /// Return true when a callee name indicates I/O. Matches against | ||
| /// well-known substrings in std::io / fmt path components. | ||
| fn is_io_callee_name(name: &str) -> bool { | ||
| let lower = name.to_lowercase(); | ||
| matches!(lower.as_str(), "print" | "println" | "eprint" | "eprintln" | "write_fmt" | "fmt") | ||
| || lower.contains("io") | ||
| || lower.contains("print") | ||
| || lower.contains("display") | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Locate the implementation of fundecl_name_by_id and inspect what it returns.
fd -e rs llbc_calls
ast-grep --pattern $'pub fn fundecl_name_by_id($$$) -> $_ {
$$$
}'
ast-grep --pattern $'fn fundecl_name_by_id($$$) -> $_ {
$$$
}'
# Also surface call sites and any string-shape assertions in tests.
rg -nP -C3 '\bfundecl_name_by_id\s*\('Repository: TSavo/provekit
Length of output: 4282
is_io_callee_name substring matches are dangerously broad for basenames.
lower.contains("io") matches innocuous identifiers like function, region, billion, axiom, option; contains("print") matches fingerprint, print_helper_unrelated; contains("display") matches displayable_value etc. Since fundecl_name_by_id returns only the trailing identifier (not a fully-qualified path), real user functions with these substrings in their basenames will spuriously gain Effect::Io, which demo_pure_composition explicitly relies on to refuse composition — pure callees would be wrongly excluded from pure-pair compression.
Instead of free substring containment, use a curated set of exact basename matches or prefix matches for well-known stdlib function names (e.g., println, print, eprint, eprintln, write_fmt, fmt, etc.).
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/llbc_lift.rs` around lines 766 - 774,
The is_io_callee_name function currently uses broad substring checks
(lower.contains("io"), contains("print"), contains("display")) which cause false
positives; update is_io_callee_name to only match a curated set of exact
basenames and a small set of safe prefixes for known std lib I/O names (e.g.,
exact matches: "print", "println", "eprint", "eprintln", "write_fmt", "fmt";
optional safe prefixes like "write_" or "read_" if desired), removing the
generic contains(...) checks so only those exact or intentional prefix matches
mark a callee as I/O; keep the lowercase conversion and use matches! or a
HashSet/array of strings to perform the exact/prefix checks inside
is_io_callee_name.
Comment on lines
+75
to
+99
| // Recurse into Switch::If's two branches and Switch::SwitchInt's | ||
| // arms, since loops can hide inside conditional branches. | ||
| if let Some(switch) = kind.get("Switch") { | ||
| if let Some(if_arr) = switch.get("If").and_then(|v| v.as_array()) { | ||
| if if_arr.len() == 3 { | ||
| recurse_block(&if_arr[1], out); | ||
| recurse_block(&if_arr[2], out); | ||
| } | ||
| } | ||
| if let Some(si) = switch.get("SwitchInt").and_then(|v| v.as_array()) { | ||
| // Shape: [discr, lit_ty, arms, otherwise_block] | ||
| if si.len() == 4 { | ||
| if let Some(arms) = si[2].as_array() { | ||
| for arm in arms { | ||
| if let Some(arr) = arm.as_array() { | ||
| if arr.len() == 2 { | ||
| recurse_block(&arr[1], out); | ||
| } | ||
| } | ||
| } | ||
| } | ||
| recurse_block(&si[3], out); | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
Loops inside Switch::Match arms are currently invisible.
This walker descends into If and SwitchInt, but not Switch::Match. Any loop nested under a match arm will be missed, so the lifter can omit Effect::OpaqueLoop for code that still contains a deferred proof obligation. Recurse through match-arm blocks here the same way the other LLBC walkers do.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/llbc_loops.rs` around lines 75 - 99,
The walker currently descends into "If" and "SwitchInt" but skips
"Switch::Match", so add handling for kind.get("Switch").get("Match") similar to
the SwitchInt branch: if let Some(match_arr) = switch.get("Match").and_then(|v|
v.as_array()) { iterate the arms array (usually match_arr[1] or the slot that
holds arms depending on your shape), for each arm check it's an array and call
recurse_block on the arm's block element (commonly the last element of the arm
array); also recurse into any explicit "otherwise"/fallback block if the Match
shape provides one. Use the same recurse_block(&..., out) calls and mirror the
defensive .as_array()/len checks used in the existing SwitchInt handling to
avoid panics. }
Comment on lines
+125
to
+168
| fn discr_traces_to_try_branch( | ||
| discr_place: &Value, | ||
| siblings: &[&Value], | ||
| fun_decls: Option<&Value>, | ||
| ) -> bool { | ||
| let Some(local) = discr_place | ||
| .get("kind") | ||
| .and_then(|k| k.get("Local")) | ||
| .and_then(|v| v.as_u64()) | ||
| .map(|n| n as u32) | ||
| else { | ||
| return false; | ||
| }; | ||
| // Find the most recent Call statement whose dest is `local`. | ||
| for s in siblings.iter().rev() { | ||
| let Some(kind) = s.get("kind") else { | ||
| continue; | ||
| }; | ||
| let Some(call) = kind.get("Call") else { | ||
| continue; | ||
| }; | ||
| let dest_local = call | ||
| .get("dest") | ||
| .and_then(|d| d.get("kind")) | ||
| .and_then(|k| k.get("Local")) | ||
| .and_then(|v| v.as_u64()) | ||
| .map(|n| n as u32); | ||
| if dest_local != Some(local) { | ||
| continue; | ||
| } | ||
| // Found the producing Call. Check if the callee's name path | ||
| // ends in Ident("branch") — the Try-trait method. | ||
| let Some(func_id) = call | ||
| .get("func") | ||
| .and_then(|f| f.get("Regular")) | ||
| .and_then(|r| r.get("kind")) | ||
| .and_then(|k| k.get("Fun")) | ||
| .and_then(|f| f.get("Regular")) | ||
| .and_then(|v| v.as_u64()) | ||
| else { | ||
| return false; | ||
| }; | ||
| return callee_is_try_branch(func_id, fun_decls); | ||
| } |
There was a problem hiding this comment.
Only search assignments that precede this Switch::Match.
discr_traces_to_try_branch scans siblings.iter().rev() across the whole block, so a later reuse of the same local can be mistaken for the producer of the current discriminant. That makes try_cid detection depend on statements that execute after the match. Pass the current statement index (or a slice of preceding siblings) and search only those.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/llbc_try.rs` around lines 125 - 168,
discr_traces_to_try_branch currently walks siblings.iter().rev() over the entire
block and can pick a later assignment as the producer of the discriminant;
change its API and call sites so it only searches statements that precede the
Switch::Match (e.g. add a parameter like start_idx or accept a slice of
preceding siblings) and iterate backwards over that prefix instead of the full
siblings list; update callers to pass the current statement index or a slice and
ensure callee_is_try_branch(func_id, fun_decls) is still used to validate the
Call producer.
Comment on lines
+158
to
+180
| // Multi-segment path (std::vec::Vec, crate::Foo, etc.) — use last segment. | ||
| let last = segments.last().unwrap(); | ||
| let ident = last.ident.to_string(); | ||
| if let Some(prim) = primitive_sort_name(&ident) { | ||
| return prim.to_string(); | ||
| } | ||
| if let syn::PathArguments::AngleBracketed(ab) = &last.arguments { | ||
| let inners: Vec<String> = ab | ||
| .args | ||
| .iter() | ||
| .filter_map(|a| { | ||
| if let syn::GenericArgument::Type(t) = a { | ||
| Some(syn_type_to_sort_name(t)) | ||
| } else { | ||
| None | ||
| } | ||
| }) | ||
| .collect(); | ||
| if !inners.is_empty() { | ||
| return format!("{}<{}>", ident, inners.join(",")); | ||
| } | ||
| } | ||
| ident |
There was a problem hiding this comment.
Qualified type paths still collapse to their last segment.
This maps foo::Point and bar::Point to the same sort name, and extract_type_decl_name below does the same on the LLBC side. That reintroduces sort collisions for same-named types from different modules, which is exactly what this translator is supposed to prevent. Preserve a stable qualified path in the sort name instead of truncating to the trailing identifier.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/sort_translate.rs` around lines 158 -
180, The current logic in syn_type_to_sort_name uses only the last Path segment
(variable last / ident), causing different modules' types like foo::Point and
bar::Point to collide; change it to build a stable qualified path string from
all segments (including their segment.ident and any AngleBracketed generic
arguments) instead of truncating to the last segment, and apply the same
strategy used by extract_type_decl_name so sort names include the full module
path (e.g., join segment idents with "::" and render nested generics for each
segment) while still respecting primitive_sort_name checks and existing generic
inner-type mapping.
Comment on lines
+380
to
+393
| Expr::While(w) => { | ||
| for s in &w.body.stmts { | ||
| walk_stmt_for_callsites(s, callee_name, conditions, inner_stmts, hits); | ||
| } | ||
| } | ||
| Expr::ForLoop(fl) => { | ||
| for s in &fl.body.stmts { | ||
| walk_stmt_for_callsites(s, callee_name, conditions, inner_stmts, hits); | ||
| } | ||
| } | ||
| Expr::Loop(l) => { | ||
| for s in &l.body.stmts { | ||
| walk_stmt_for_callsites(s, callee_name, conditions, inner_stmts, hits); | ||
| } |
There was a problem hiding this comment.
Loop bodies miss preceding loop-local let bindings.
The loop walkers recurse through each body statement, but they never prepend earlier statements from the same loop body into inner_stmts. A callsite after let y = 42; inside a loop therefore sees y as free and gets the wrong substitution chain. Thread per-statement body prefixes through while / for / loop the same way Expr::Block does.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/walk.rs` around lines 380 - 393, The
loop-handling arms for Expr::While, Expr::ForLoop, and Expr::Loop in walk.rs
call walk_stmt_for_callsites on each body statement but fail to include the
preceding loop-local let bindings (the prefix of statements before the current
one) into inner_stmts, causing free-variable/substitution errors; change these
arms to mirror Expr::Block's behavior by iterating with indices and, for each
statement s at index i, build a prefix of the loop body stmts[0..i] and pass
inner_stmts augmented with that prefix to walk_stmt_for_callsites (i.e., thread
per-statement body prefixes through the loop arms so earlier let bindings are
visible to subsequent callsite analysis in walk_stmt_for_callsites).
Comment on lines
+4
to
+7
| while i < n { | ||
| total += i; | ||
| i += 1; | ||
| } |
There was a problem hiding this comment.
Potential infinite loop and arithmetic overflow when n = u32::MAX
When n = u32::MAX, i will eventually reach u32::MAX, and i += 1 wraps to 0 in release mode, restarting the condition i < n as true and looping forever. In debug mode it panics instead. Similarly, total += i silently wraps in release once the partial sum exceeds u32::MAX.
If the LLBC fixture is generated from a compiled (release) build of this source and the test suite ever exercises the walk with n = u32::MAX, the fixture would encode diverging semantics. Even if the provekit-walk emits an OpaqueLoop effect and never actually executes the loop, it's worth making the fixture's intended precondition explicit.
Consider bounding the input or adding a comment:
🛡️ Suggested clarification
fn s(n: u32) -> u32 {
+ // Fixture: exercises loop detection. Meaningful results require n < 2^16
+ // to avoid u32 overflow in `total`; n < u32::MAX to avoid wrap-around in `i`.
let mut total = 0;
let mut i = 0;
while i < n {
total += i;
i += 1;
}
total
}🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/tests/fixtures/loops.rs` around lines 4 -
7, The loop can overflow/wrap and become infinite when n == u32::MAX; fix by
making the precondition explicit or eliminating wrap behavior: either add a
precondition/assertion such as assert!(n != u32::MAX) or assert!(n <= u32::MAX -
1) before the while, or change arithmetic to checked forms (use i =
i.checked_add(1).expect("overflow") and total =
total.checked_add(i).expect("overflow")) or widen types (e.g., cast i/total to
u64) to avoid wrapping; locate the while loop using the variables i, n, and
total and apply one of these changes and/or add a clarifying comment explaining
the assumed bound on n.
6 tasks
This was referenced May 12, 2026
This was referenced May 26, 2026
Merged
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
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
First operational implementation of paper 07's discipline. Closes the launch-blocker MVP for issue #368.
Takes Rust source with zero annotations, lifts predicates from source structure, walks backward via Dijkstra-Hoare WP rules, builds a parallel shadow AST where every node is a content-addressed memento, composes implications by hash combination, and demonstrates 100% cache hits on a re-run of identical input.
The closed algebra Sir articulated as the substrate's irreducible primitives:
=is a pre (allocation; bound is finite by construction)ifis a post (case analysis; every else is the contraposition)p → q over x(with x bound at the chain's allocation)Three source operators map to three memento types. The proof DAG is always finite because every variable's bound chain terminates at an
=. No infinite quantification, no undecidable closure — finite walk over content-addressed mementos.What's in the crate
provekit-walkcrate (workspace member; ~1900 LoC including tests)provekit-walk-demobinary that runs the full pipeline visibly on three fixturesArchitecture
wp.rswp(x := e, P) = P[e/x]); lambda/let shadowinglift.rsif-then-panic,assert!(), binary comparisons, compound&&/||with De Morgan + double-negation, return-expression equation derivationwalk.rscanonical.rsprovekit-canonicalizercrateshadow.rspredecessor_cid(data-flow upstream),allocation_cid(chain terminus),callee_root_cid. Composition (compose_edges,compose_chain) is hash combination.Demo output
Demo 2 (
guarded_caller): callsite insideif input >= 10 { f(input) }produces WP(input ≥ 10) → (input ≥ 10), a tautology. The if-condition is a free post discharging the obligation.Demo 3 (
multi_callercallsh(x, y)): multi-argument callee withif x < 10 || y < 5 panicguard. Lifter applies De Morgan to derivex ≥ 10 ∧ y ≥ 5. Walk substitutes both formals through both lets (a → 42,b → 100); entry WP is fully ground.Test coverage (38/38 green)
wp::tests(3): substitution, no-op, lambda shadowingcanonical::tests(2): deterministic CIDs, distinct formulas → distinct CIDslift::tests(10): if-then-panic, assert!, binary comparisons, multiple assertions, return-expression, binary ops as Ctor terms, De Morgan on||, De Morgan on&&, double-negation elimination, vacuous truetests/bare_demo.rs(2): end-to-end walk + unsafe-caller gaptests/composition_demo.rs(4): composition deterministic + associative + compresses + distincttests/end_to_end_demo.rs(2): full lift→walk→shadow ground-true closure + non-ground gaptests/if_context_demo.rs(3): guarded callsite carries condition, unguarded retains free var, else-branch contrapositiontests/shadow_demo.rs(12): mirrors body, N arrivals per slot, BLAKE3-512 self-identifying, deterministic, walk-order-independent, predecessor data-flow upstream, allocation_cid anchors over-x, allocation memento self-contained, edge memento p→q, distinct preconditions yield distinct CIDsOperational correspondence to paper 07
Allocations × Reads)build_shadow_sourcemirrors source AST structure; coverage is total at slot granularitycompose_chaincollapses N edges to 1 CID; second run is 100% cache hitsSequencing
This is the launch-blocker MVP for #368. The substrate's algorithmic core is operational on a real Rust source pair. v1.5.0 protocol carries it; no wire-format touch.
Test plan
cargo test -p provekit-walk— 38/38 green./target/debug/provekit-walk-demoruns end-to-end with visible output and 100% second-run cache hit rate=pre,ifpost, callsite implication)Future iterations (not blocking)
FunctionCompletenessMemento(every literal code path becomes a memento; the function's complete behavior is a single CID)Companion to paper 07
Paper 07 (PR #365) makes the structural-elimination claim; this PR is the empirical demonstration that paper 07's machinery works on real source. The pre/post derivation, the walk's data-flow propagation, the content-addressed mementos, the composition primitive, the cache hit rate — all visible in the demo binary's output.
🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Tests