feat(libprovekit): wp_rule schema + substitute/apply formula nodes + the wp evaluator (wp-as-formula PR 1/N)#620
Merged
Conversation
…sites
Per spec protocol/specs/2026-05-13-wp-as-formula.md §2.3: the wp-rule
schema needs two new IrFormula nodes the language cannot express today:
- `substitute` — explicit, capture-avoiding, single-variable
substitution on a formula (`Q[var := term]`), needed as a node
because in a `wp_rule` schema the target is the postcondition
meta-variable `Q`, not yet known.
- `apply` — application of a slot-transformer meta-variable
(`wp_<slot>`) to one formula argument, the "weakest precondition of
the term in slot `<slot>`."
Both are conservative extensions (an existing IrFormula is still an
IrFormula) and reduce to the existing grammar when fully instantiated;
`libprovekit::wp` (next commit) eliminates them before any formula
reaches a solver or compiler backend.
- protocol/provekit-ir.cddl: add SubstituteFormula / ApplyFormula to
the IrFormula union with locked key orders.
- provekit-ir-types: add the two enum variants (manual codegen
extension, like the Sort grow; CDDL stays source of truth).
- sweep every now-non-exhaustive `match` on IrFormula across the
workspace (coq + smt-lib + lean compilers, ir-symbolic conversion,
smt-lib validator, aarch64 lifter) with a uniform refusal arm:
these nodes never reach those sites once `libprovekit::wp` has run,
so reaching the arm is a bug. (The substitution / free-var sites in
libprovekit::compose and provekit-walk are intentionally left
non-exhaustive here; the next commit folds them into the shared
libprovekit::wp module.)
PR 1 of the wp-as-formula sub-project, step 1.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ose wp duplication
Per spec protocol/specs/2026-05-13-wp-as-formula.md §2: the
weakest-precondition rule of an operation is now consumed as *data* (the
`wp_rule` field, an IrFormula over the op's formals plus the reserved
meta-vars `Q` and `wp_<slot>`) rather than as hardcoded per-language
match-arms. This commit lands the evaluator that consumes it, plus the
dedup refactor it enables.
`implementations/rust/libprovekit/src/wp.rs` — a new module with three
things:
1. The capture-avoiding substitution algebra over IrFormula / IrTerm,
plus free-variable computation. This was previously *duplicated*
between `provekit-walk`'s `wp.rs` and `libprovekit::compose`; it now
has a single canonical home here (CCP §5: one primitive, every
consumer). `compose.rs` deletes its copy and re-exports from
`wp`; `provekit-walk/src/wp.rs` does the same. No observable
behavior change to either (their `result == value_expr` extraction,
their byte-identical output, etc. are unaffected).
2. The two wp-rule schema-node reductions (spec §2.3):
- `substitute { target, var, term }` with a ground `target` is
eliminated by performing the capture-avoiding substitution;
- `apply { fn: "wp_<slot>", args: [X] }` is eliminated by inlining
the actual slot transformer — recursing into the slot's
sub-term with `X` as the postcondition.
The postcondition meta-var `Q` is the nullary atomic predicate
`Atomic { name: "Q", args: [] }` (the IR formula grammar has no
`var` node; a propositional variable is a nullary atomic). After
`wp(t, Q)` with a ground `Q` the result formula contains no
`Substitute` / `Apply` nodes and no placeholder — verified by a
`contains_schema_node` assertion in the tests.
3. The evaluator `wp(t, Q)` — structural recursion over the term `t`.
For each op node: look up its contract; take its authored `wp_rule`
or *synthesize* one for a value-op from `pre`/`post`
(`pre ∧ Q[result := value_expr]`, with `value_expr` read off the
`post`'s `result == value_expr` shape); instantiate that rule with
this `Q`, the recursively-computed `wp`s of `t`'s `Stmt`-typed
sub-terms (substituted for the `wp_<slot>` meta-vars), and the
values of `t`'s value-typed sub-terms (substituted for the
formals). Handles: `seq(s1,s2)` → `wp_s1(wp_s2(Q))`; `if`-style →
the Dijkstra rule `(c ⇒ wp_s1(Q)) ∧ (¬c ⇒ wp_s2(Q))`; `while`/loops
→ `Refusal::OpaqueLoop { loop_cid }` naming the missing
`LoopInvariantMemento` (until the resolver supplies an instantiated
rule); unresolved/indirect calls and unknown ops →
`Refusal::OpaqueCall { callee }`. The evaluator is total (always a
formula or a named `Refusal`/`WpError`, never a panic),
deterministic (recursion order fixed by slot order; no
nondeterminism — the computed `wp` is canonicalized + content-
addressed downstream), and makes no solver call (pure formula
construction; z3 comes later, at the discharge step of spec §3).
`OpContractInfo` + `OpContractResolver` are the consumed-contract view +
lookup trait; the catalog-backed resolver lands with the hub-op
migration (PR2). The test fixtures here carry authored `wp_rule`s for the
control-flow ops (`if` = the Dijkstra rule, `seq` = `wp_first(wp_second(Q))`,
`return` = `Q[result := value]`, `skip` = `Q`) so the evaluator has real
rules to chew on; value-ops (`add`, `div`, `uop_neg`, `bop_eq`) carry
only `pre`/`post` and exercise the synthesis path.
17 tests in `wp::tests`, including: synthesized `wp` for `add`
(`pre ∧ Q[result := lhs+rhs]`) and `div` (`not_zero(rhs) ∧ Q[result := lhs/rhs]`),
including a Q that mentions `result`; the authored Dijkstra-`if` rule
instantiated on `if(bop_eq(x,0), return(uop_neg(22)), return(x))`; the
evaluator on `seq(if(c, return(x), return(y)), skip)`; the
opaque-loop / unresolved-call / unknown-op / malformed-rule / arity-mismatch
paths; `substitute` / `apply` serde round-trip + pinned BLAKE3-512 CIDs
(byte-determinism — *Supra omnia, rectum*).
Plus: `provekit-ir-codegen/tests/cddl_valid.rs` — the protocol grammar
must parse and validate under the `cddl` crate (guards the grammar file
when new node kinds like `substitute` / `apply` are added).
Note on `provekit-walk`: the Rust `provekit-walk` crate is not currently
a workspace member (it was dropped from `members` at commit 5ec1622,
PR #387, in a baselines chore — nothing in CI builds it, and `version.workspace`
makes it unbuildable standalone). Its `src/wp.rs` is updated for the
refactor (re-exports the moved substitution functions from
`libprovekit::wp`); the change lands ready for the moment walk re-joins
the workspace. `walk/src/contract.rs` keeps importing
`libprovekit::compose::substitute_in_formula`, which still resolves via
the new re-export.
PR 1 of the wp-as-formula sub-project, step 2 (schema + grammar + evaluator
+ walk/compose dedup).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
WalkthroughThis PR introduces a weakest-precondition evaluator as a new ChangesWeakest-Precondition Evaluator & Substitution Centralization
Sequence Diagram(s)sequenceDiagram
participant Caller
participant wp
participant OpContractResolver
participant reduce_formula
participant Backend
Caller->>wp: wp(term, postcondition, resolver)
wp->>wp: structural recursion on term
wp->>OpContractResolver: lookup(op_name)
OpContractResolver-->>wp: OpContractInfo with rule
wp->>wp: wp_op: instantiate rule with value-slot subst
wp->>reduce_formula: eliminate Substitute/Apply nodes
reduce_formula->>reduce_formula: substitute_in_formula, apply inline
reduce_formula-->>wp: normal IrFormula (no schema nodes)
wp-->>Caller: Result<IrFormula, WpError>
Caller->>Backend: emit(formula)
Backend->>Backend: match formula nodes
Backend->>Backend: no Substitute/Apply arms match
Backend-->>Caller: valid output
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
implementations/rust/provekit-ir-types/src/lib.rs (1)
279-354: 🛠️ Refactor suggestion | 🟠 Major | 🏗️ Heavy liftManual edits in generated file create maintenance hazard.
The
IrFormulaenum has been manually extended withSubstituteandApplyvariants because the codegen (provekit-ir-codegen) does not yet emit them, despite the CDDL defining them. The comment warns that regenerating will clobber these manual additions, requiring developers to remember to re-apply them.This is a high-effort, high-risk maintenance pattern. Consider:
- Short-term: Add a workspace-level integration test that fails if the manual variants are missing (e.g., attempt to deserialize a
{"kind":"substitute",...}payload and assert it succeeds).- Medium-term: Update
provekit-ir-codegento emit all CDDL union variants, eliminating the need for manual edits.🤖 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-ir-types/src/lib.rs` around lines 279 - 354, The generated IrFormula enum is missing the Substitute and Apply variants (manual additions to IrFormula::Substitute and IrFormula::Apply are being clobbered on regen), so add a failing integration test that deserializes {"kind":"substitute",...} and {"kind":"apply",...} into IrFormula (use serde_json::from_str and assert_ok/assert_eq) to detect regressions, and then update the codegen (provekit-ir-codegen) to emit all CDDL-defined union arms (ensure it generates the Substitute and Apply variants with the same field names and serde attributes as the current manual definitions) so future regenerations do not require manual edits.implementations/rust/provekit-ir-compiler-smt-lib/src/generated.rs (1)
14-83:⚠️ Potential issue | 🔴 Critical | ⚡ Quick winCritical: Duplicate match arms in
emit_termcause dead code.The
emit_termfunction contains duplicate match arms forTerm::Ctor,Term::Lambda, andTerm::Let(lines 29-37 duplicate lines 56-64, lines 38-47 duplicate lines 65-73, and lines 48-55 duplicate lines 74-81). The first set of arms will always match, making the second set unreachable dead code.🐛 Proposed fix
pub fn emit_term(term: &Term) -> String { match term { Term::Var { name, .. } => name.clone(), Term::Const { value, sort, .. } => { let sort_name = match sort { Sort::Primitive { name } => name.as_str(), Sort::Function { .. } | Sort::Dependent { .. } | Sort::Float { .. } | Sort::Region { .. } => { panic!("smt-lib: Const cannot carry a Function/Dependent/Float/Region sort in pure SMT-LIB v2.6"); } }; emit_const_value(value, sort_name) } Term::Ctor { name, args, .. } => { if args.is_empty() { return name.clone(); }; let args_str = args.iter(); let args_str = args_str.map(emit_term); let args_str: Vec<String> = args_str.collect(); format!("({} {})", name, args_str.join(" ")) } Term::Lambda { param_name, param_sort, body, .. } => { let sort_str = emit_sort(param_sort); let body_str = emit_term(body); format!("(lambda (({} {})) {})", param_name, sort_str, body_str) } Term::Let { bindings, body, .. } => { let mut binding_strs = bindings.iter(); let binding_strs = binding_strs.map(|b| format!("({} {})", b.name, emit_term(&b.bound_term))); let binding_strs: Vec<String> = binding_strs.collect(); let body_str = emit_term(body); format!("(let ({}) {})", binding_strs.join(" "), body_str) } - Term::Ctor { name, args } => { - if args.is_empty() { - return name.clone(); - }; - let args_str = args.iter(); - let args_str = args_str.map(emit_term); - let args_str: Vec<String> = args_str.collect(); - format!("({} {})", name, args_str.join(" ")) - } - Term::Lambda { - param_name, - param_sort, - body, - } => { - let sort_str = emit_sort(param_sort); - let body_str = emit_term(body); - format!("(lambda (({} {})) {})", param_name, sort_str, body_str) - } - Term::Let { bindings, body } => { - let binding_strs = bindings.iter(); - let binding_strs = - binding_strs.map(|b| format!("({} {})", b.name, emit_term(&b.bound_term))); - let binding_strs: Vec<String> = binding_strs.collect(); - let body_str = emit_term(body); - format!("(let ({}) {})", binding_strs.join(" "), body_str) - } } }🤖 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-ir-compiler-smt-lib/src/generated.rs` around lines 14 - 83, The emit_term function has duplicate match arms for Term::Ctor, Term::Lambda, and Term::Let making the later arms unreachable; remove the redundant duplicate arms so each variant is handled only once (keep one consistent implementation for Term::Ctor, Term::Lambda, and Term::Let), ensure the kept arms cover the correct pattern shapes (use the existing field names like name/args, param_name/param_sort/body, and bindings/body or use .../.. consistently) and consolidate any differing logic so emit_term produces the same output as before without duplicate match branches.
🧹 Nitpick comments (3)
implementations/rust/provekit-ir-codegen/tests/cddl_valid.rs (1)
12-14: ⚡ Quick winUse
CARGO_MANIFEST_DIRfor robust test path resolution.The test currently depends on process CWD. Building the path from
env!("CARGO_MANIFEST_DIR")avoids flaky failures across different runners.Suggested patch
- let path = "../../../protocol/provekit-ir.cddl"; - let text = std::fs::read_to_string(path) - .unwrap_or_else(|e| panic!("read {path}: {e}")); + let path = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("../../../protocol/provekit-ir.cddl"); + let text = std::fs::read_to_string(&path) + .unwrap_or_else(|e| panic!("read {}: {e}", path.display()));🤖 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-ir-codegen/tests/cddl_valid.rs` around lines 12 - 14, The test builds a relative path that depends on the process CWD (variable path) and uses std::fs::read_to_string to load the file; change it to construct the path using env!("CARGO_MANIFEST_DIR") (e.g., format! or Path/PathBuf joining with env!("CARGO_MANIFEST_DIR")) so the test locates "protocol/provekit-ir.cddl" reliably, then call std::fs::read_to_string on that constructed path and keep the existing unwrap_or_else panic behavior for errors.implementations/rust/libprovekit/src/wp.rs (2)
1071-1085: 💤 Low valueTheoretical
u32overflow infresh_namefunction.The
fresh_namefunction uses an unbounded loop with au32counter (line 1077). If all ~4 billion{base}_1through{base}_4294967295variants are taken, the counter will overflow and wrap, causing an infinite loop.While extremely unlikely in practice (requires 4 billion identically-named variables in scope), consider using
u64or saturating at a reasonable limit with a panic to surface the pathological case.♻️ Optional hardening
fn fresh_name(taken: &HashSet<String>, base: &str) -> String { if !taken.contains(base) { return base.to_string(); } - let mut n: u32 = 1; + let mut n: u64 = 1; loop { let candidate = format!("{}_{}", base, n); if !taken.contains(&candidate) { return candidate; } n += 1; + if n > 1_000_000 { + panic!("fresh_name: failed to find fresh name after 1M attempts for base '{}'", base); + } } }🤖 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/libprovekit/src/wp.rs` around lines 1071 - 1085, The fresh_name function uses a u32 counter `n` in the loop which can overflow and wrap if ~4 billion name variants are present; change `n` to a wider integer type (e.g., u64) or implement a safe bound check that panics or returns an error if `n` would overflow to prevent an infinite loop—update the `fresh_name` signature body where `let mut n: u32 = 1;` and the loop generating `candidate` to use the chosen strategy (e.g., `u64` counter or explicit overflow check) so lookup against `taken: &HashSet<String>` and the `base: &str` formatting remain correct and safe.
627-645: ⚡ Quick winConsider validating
Applyarity per CDDL specification.The CDDL defines
ApplyFormula { args: [+ IrFormula], ... }(one or more formula arguments), but line 641 handles emptyargsby falling back toq.clone(). While this is defensive, it silently accepts malformed rules that violate the CDDL spec.Consider adding validation:
♻️ Proposed validation
IrFormula::Apply { args, r#fn } => { if !is_slot_transformer_name(&r#fn) { return Err(WpError::MalformedRule { op: op_name.to_string(), fn_name: r#fn, }); } + if args.is_empty() { + return Err(WpError::MalformedRule { + op: op_name.to_string(), + fn_name: format!("{} (empty args)", r#fn), + }); + } let slot_name = &r#fn[SLOT_TRANSFORMER_PREFIX.len()..]; let Some((_, slot_term)) = stmt_transformers.iter().find(|(n, _)| n == slot_name) else { return Err(WpError::MalformedRule { op: op_name.to_string(), fn_name: r#fn, }); }; - let arg = match args.into_iter().next() { - Some(a) => reduce_formula(a, q, stmt_transformers, op_name, resolver)?, - None => q.clone(), - }; + let arg = reduce_formula(args.into_iter().next().unwrap(), q, stmt_transformers, op_name, resolver)?; wp(slot_term, &arg, resolver) }🤖 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/libprovekit/src/wp.rs` around lines 627 - 645, The Apply arm currently accepts empty args and substitutes q.clone(), which silently permits malformed CDDL ApplyFormula; update IrFormula::Apply handling to validate arity: ensure args is non-empty (per CDDL ApplyFormula { args: [+ IrFormula] }) before proceeding, and return Err(WpError::MalformedRule { op: op_name.to_string(), fn_name: r#fn.clone() }) (or an appropriate WpError) when args is empty; locate the match in wp.rs where IrFormula::Apply uses is_slot_transformer_name, SLOT_TRANSFORMER_PREFIX, stmt_transformers, reduce_formula and wp, and replace the fallback q.clone() behavior with the explicit validation and error path.
🤖 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-ir-compiler-smt-lib/src/generated.rs`:
- Around line 727-731: The handling of schema nodes in has_outlives_predicate is
inconsistent: change the Formula::Substitute and Formula::Apply arms in
has_outlives_predicate (currently traversing into target/args) to match other
functions by making them unreachable (e.g., replace with unreachable!()) if
schema nodes must be reduced before SMT-LIB, or alternatively keep traversal but
add a clear comment above has_outlives_predicate explaining why this pass must
accept unreduced schema nodes and document the expected temporary validation
state; reference the Formula::Substitute and Formula::Apply arms and the
has_outlives_predicate function when making the change.
---
Outside diff comments:
In `@implementations/rust/provekit-ir-compiler-smt-lib/src/generated.rs`:
- Around line 14-83: The emit_term function has duplicate match arms for
Term::Ctor, Term::Lambda, and Term::Let making the later arms unreachable;
remove the redundant duplicate arms so each variant is handled only once (keep
one consistent implementation for Term::Ctor, Term::Lambda, and Term::Let),
ensure the kept arms cover the correct pattern shapes (use the existing field
names like name/args, param_name/param_sort/body, and bindings/body or use
.../.. consistently) and consolidate any differing logic so emit_term produces
the same output as before without duplicate match branches.
In `@implementations/rust/provekit-ir-types/src/lib.rs`:
- Around line 279-354: The generated IrFormula enum is missing the Substitute
and Apply variants (manual additions to IrFormula::Substitute and
IrFormula::Apply are being clobbered on regen), so add a failing integration
test that deserializes {"kind":"substitute",...} and {"kind":"apply",...} into
IrFormula (use serde_json::from_str and assert_ok/assert_eq) to detect
regressions, and then update the codegen (provekit-ir-codegen) to emit all
CDDL-defined union arms (ensure it generates the Substitute and Apply variants
with the same field names and serde attributes as the current manual
definitions) so future regenerations do not require manual edits.
---
Nitpick comments:
In `@implementations/rust/libprovekit/src/wp.rs`:
- Around line 1071-1085: The fresh_name function uses a u32 counter `n` in the
loop which can overflow and wrap if ~4 billion name variants are present; change
`n` to a wider integer type (e.g., u64) or implement a safe bound check that
panics or returns an error if `n` would overflow to prevent an infinite
loop—update the `fresh_name` signature body where `let mut n: u32 = 1;` and the
loop generating `candidate` to use the chosen strategy (e.g., `u64` counter or
explicit overflow check) so lookup against `taken: &HashSet<String>` and the
`base: &str` formatting remain correct and safe.
- Around line 627-645: The Apply arm currently accepts empty args and
substitutes q.clone(), which silently permits malformed CDDL ApplyFormula;
update IrFormula::Apply handling to validate arity: ensure args is non-empty
(per CDDL ApplyFormula { args: [+ IrFormula] }) before proceeding, and return
Err(WpError::MalformedRule { op: op_name.to_string(), fn_name: r#fn.clone() })
(or an appropriate WpError) when args is empty; locate the match in wp.rs where
IrFormula::Apply uses is_slot_transformer_name, SLOT_TRANSFORMER_PREFIX,
stmt_transformers, reduce_formula and wp, and replace the fallback q.clone()
behavior with the explicit validation and error path.
In `@implementations/rust/provekit-ir-codegen/tests/cddl_valid.rs`:
- Around line 12-14: The test builds a relative path that depends on the process
CWD (variable path) and uses std::fs::read_to_string to load the file; change it
to construct the path using env!("CARGO_MANIFEST_DIR") (e.g., format! or
Path/PathBuf joining with env!("CARGO_MANIFEST_DIR")) so the test locates
"protocol/provekit-ir.cddl" reliably, then call std::fs::read_to_string on that
constructed path and keep the existing unwrap_or_else panic behavior for errors.
🪄 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: ce31ddfe-a0e8-4c99-b610-2dbac0966f9e
📒 Files selected for processing (14)
implementations/rust/libprovekit/src/compose.rsimplementations/rust/libprovekit/src/lib.rsimplementations/rust/libprovekit/src/wp.rsimplementations/rust/libprovekit/src/wp/tests.rsimplementations/rust/provekit-ir-codegen/tests/cddl_valid.rsimplementations/rust/provekit-ir-compiler-coq/src/generated.rsimplementations/rust/provekit-ir-compiler-lean/src/lib.rsimplementations/rust/provekit-ir-compiler-smt-lib/src/generated.rsimplementations/rust/provekit-ir-compiler-smt-lib/src/lib.rsimplementations/rust/provekit-ir-symbolic/src/convert.rsimplementations/rust/provekit-ir-types/src/lib.rsimplementations/rust/provekit-lift-asm-aarch64/src/lib.rsimplementations/rust/provekit-walk/src/wp.rsprotocol/provekit-ir.cddl
Comment on lines
+727
to
+731
| // wp-rule schema nodes (spec 2026-05-13-wp-as-formula.md §2.3): | ||
| // see the note in `emit_formula`. | ||
| // TODO(wp-as-formula PR1+): teach provekit-ir-codegen to emit this arm. | ||
| Formula::Substitute { target, .. } => has_outlives_predicate(target), | ||
| Formula::Apply { args, .. } => args.iter().any(has_outlives_predicate), |
There was a problem hiding this comment.
Inconsistent schema-node handling in has_outlives_predicate.
While all other functions treat Formula::Substitute and Formula::Apply as unreachable (they must be reduced before reaching SMT-LIB), has_outlives_predicate traverses into them to check for Outlives predicates. This is inconsistent with the stated requirement that schema nodes "must be reduced via libprovekit::wp first."
If schema nodes truly cannot reach this backend, these arms should also unreachable!. If they can temporarily exist during validation, the comment should explain why this function has different semantics.
🔍 Recommended approach
If schema nodes genuinely cannot reach has_outlives_predicate, align with other functions:
- Formula::Substitute { target, .. } => has_outlives_predicate(target),
- Formula::Apply { args, .. } => args.iter().any(has_outlives_predicate),
+ Formula::Substitute { .. } | Formula::Apply { .. } => {
+ unreachable!(
+ "wp-rule schema node reached has_outlives_predicate; \
+ must be reduced via libprovekit::wp first"
+ )
+ }Otherwise, add a comment explaining why this predicate-detection pass must handle unreduced schema nodes.
📝 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
| // wp-rule schema nodes (spec 2026-05-13-wp-as-formula.md §2.3): | |
| // see the note in `emit_formula`. | |
| // TODO(wp-as-formula PR1+): teach provekit-ir-codegen to emit this arm. | |
| Formula::Substitute { target, .. } => has_outlives_predicate(target), | |
| Formula::Apply { args, .. } => args.iter().any(has_outlives_predicate), | |
| // wp-rule schema nodes (spec 2026-05-13-wp-as-formula.md §2.3): | |
| // see the note in `emit_formula`. | |
| // TODO(wp-as-formula PR1+): teach provekit-ir-codegen to emit this arm. | |
| Formula::Substitute { .. } | Formula::Apply { .. } => { | |
| unreachable!( | |
| "wp-rule schema node reached has_outlives_predicate; \ | |
| must be reduced via libprovekit::wp first" | |
| ) | |
| } |
🤖 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-ir-compiler-smt-lib/src/generated.rs` around
lines 727 - 731, The handling of schema nodes in has_outlives_predicate is
inconsistent: change the Formula::Substitute and Formula::Apply arms in
has_outlives_predicate (currently traversing into target/args) to match other
functions by making them unreachable (e.g., replace with unreachable!()) if
schema nodes must be reduced before SMT-LIB, or alternatively keep traversal but
add a clear comment above has_outlives_predicate explaining why this pass must
accept unreduced schema nodes and document the expected temporary validation
state; reference the Formula::Substitute and Formula::Apply arms and the
has_outlives_predicate function when making the change.
There was a problem hiding this comment.
Pull request overview
Adds first-phase support for “wp-as-formula” across the Provekit Rust workspace by extending the IR formula grammar with schema nodes and introducing a new libprovekit::wp evaluator + shared substitution algebra, while sweeping downstream backends to explicitly reject (or mark unreachable) unreduced schema nodes.
Changes:
- Extend IR CDDL + Rust
IrFormulawithsubstituteandapplyschema-node variants forwp_rule. - Introduce
libprovekit::wp(evaluator + schema-node reduction + canonical capture-avoiding substitution/free-vars) and re-export substitution helpers fromcompose/provekit-walk. - Update compiler/lifter/symbolic backends to refuse or
unreachable!()on schema nodes, plus add a CDDL-parse validation test.
Reviewed changes
Copilot reviewed 14 out of 14 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| protocol/provekit-ir.cddl | Extends IrFormula grammar with SubstituteFormula and ApplyFormula. |
| implementations/rust/provekit-walk/src/wp.rs | Re-exports substitution/free-var helpers from libprovekit::wp; removes local duplicated implementation. |
| implementations/rust/provekit-lift-asm-aarch64/src/lib.rs | Adds explicit handling for schema nodes (currently unreachable!()). |
| implementations/rust/provekit-ir-types/src/lib.rs | Manually extends IrFormula enum with Substitute/Apply serde variants. |
| implementations/rust/provekit-ir-symbolic/src/convert.rs | Marks schema nodes as unreachable in IR→symbolic conversion. |
| implementations/rust/provekit-ir-compiler-smt-lib/src/lib.rs | SMT-LIB validator rejects schema nodes with an explicit error. |
| implementations/rust/provekit-ir-compiler-smt-lib/src/generated.rs | Adds schema-node unreachable!() arms (+ limited traversal in has_outlives_predicate). |
| implementations/rust/provekit-ir-compiler-lean/src/lib.rs | Lean collector/emitter returns internal error on schema nodes. |
| implementations/rust/provekit-ir-compiler-coq/src/generated.rs | Marks schema nodes unreachable in Coq emitter/free-var collector. |
| implementations/rust/provekit-ir-codegen/tests/cddl_valid.rs | New integration test ensuring protocol CDDL parses/validates. |
| implementations/rust/libprovekit/src/wp.rs | New WP evaluator + schema-node reduction + shared substitution/free-var algebra. |
| implementations/rust/libprovekit/src/wp/tests.rs | New test suite for synthesized/authored wp rules + schema-node CID pinning. |
| implementations/rust/libprovekit/src/lib.rs | Exposes the new wp module. |
| implementations/rust/libprovekit/src/compose.rs | Removes duplicated substitution algebra; re-exports from libprovekit::wp. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+641
to
+644
| let arg = match args.into_iter().next() { | ||
| Some(a) => reduce_formula(a, q, stmt_transformers, op_name, resolver)?, | ||
| None => q.clone(), | ||
| }; |
| callee: callee.clone(), | ||
| } | ||
| .into()); | ||
| } |
Comment on lines
+704
to
+721
| /// Substitute `replacement` for every free occurrence of | ||
| /// `Var { name == var_name }` in `formula`. Capture-avoiding: a binder | ||
| /// whose bound name appears free in `replacement` is alpha-renamed to a | ||
| /// fresh name before the substitution proceeds; a binder that rebinds | ||
| /// `var_name` shadows it (substitution stops at the binder). | ||
| /// | ||
| /// Note on the schema nodes: `substitute` and `apply` are *not* binders | ||
| /// over the surrounding scope (`substitute`'s `var` is a substitution | ||
| /// operator's bound name; `apply`'s `fn` is a meta-var name), so | ||
| /// term-substitution passes straight through them — they keep their | ||
| /// shape and their sub-parts are substituted into. (`reduce_formula` is | ||
| /// what eliminates these nodes; this function only moves a *term* into a | ||
| /// formula's leaves.) The postcondition placeholder | ||
| /// `Atomic { name: "Q", args: [] }` has no term args and is therefore | ||
| /// unaffected by term-substitution, which is correct: a value-slot value | ||
| /// must not be substituted *into* the postcondition until the rule is | ||
| /// applied to a concrete `Q`. | ||
| pub fn substitute_in_formula( |
Comment on lines
+11
to
+14
| // Tests run with CWD = the crate dir (`implementations/rust/provekit-ir-codegen`). | ||
| let path = "../../../protocol/provekit-ir.cddl"; | ||
| let text = std::fs::read_to_string(path) | ||
| .unwrap_or_else(|e| panic!("read {path}: {e}")); |
TSavo
commented
May 12, 2026
Owner
Author
TSavo
left a comment
TSavo
left a comment
There was a problem hiding this comment.
Verdict: MERGE-WITH-NITS
Adversarial review for Supra omnia, rectum. This is the foundation the rest of the wp-as-formula chain (PRs 2-6) builds on, so I went hard on totality, determinism, schema-node elimination, and whether the dedup is truly behavior-preserving. The evaluator is correct, the grammar extension is well-locked, the tests pin the wire encoding, and the swept backends fail loudly rather than silently. Nothing here blocks; the nits should land before PR2 if cheap.
What I verified
cargo test -p libprovekit— 17wp::tests+ compose + everything else: green.cargo test -p provekit-ir-types -p provekit-canonicalizer -p provekit-ir-codegen -p provekit-ir-compiler-{smt-lib,coq,lean} -p provekit-ir-symbolic -p provekit-lift-asm-aarch64: all green, including the newcddl_valid.rs(the protocol grammar parses + validates under thecddlcrate).cargo build --workspace: clean (only pre-existing warnings inprovekit-lsp/provekit-lift-openapi).git diff --check: clean.- Pre-existing red spot-check on
origin/main(pk-main-620worktree,3e7b021f):rust_kit_contract_set_cid_is_pinned_to_self_contracts_canonical,cpp_kit_contract_set_cid_is_pinned_to_self_contracts_canonical, andkits_with_real_contracts_produce_nonempty_contract_setfail identically there. Confirmed pre-existing, not introduced by this PR. provekit-walkis genuinely not a workspace member (implementations/rust/Cargo.tomlline-checked;libprovekit, noprovekit-walk). The refactor inprovekit-walk/src/wp.rsis dead-code-until-walk-rejoins — acceptable.menagerie/cross-language-port/driver.sh: exits 0 on this branch; same artifact-driftgit statusas on pristineorigin/main, so pre-existing menagerie behavior, not caused by this PR.menagerie/concept-shapes/scripts/mint.sh: does not exist on this branch (only.pyfiles). Not exercised; the diff touches no canonicalizer/mint/transport surface, so mint flow is unaffected by construction.
Correctness of the evaluator (the load-bearing piece)
- Value-op synthesis
pre ∧ Q[result := value_expr]:find_result_equationextractsvalue_exprfrompost = (result == value_expr)in either argument order, recursing intoAnd. TheSubstitutenode uses the placeholder as target and the per-contractresult_var. Aprethat is literallytrueis dropped (sound:true ∧ φ = φ). Correct WP for an assignment. seq→wp_first(wp_second(Q)): the authored rule isapply("wp_first", apply("wp_second", Q)).reduce_formula'sApplyarm reduces the arg first (innerapply("wp_second",Q)→wp(second_term,Q)) then recurseswp(first_term, that). Order correct.- Dijkstra
if: authored, instantiated as(cond ⇒ wp_then(Q)) ∧ (¬cond ⇒ wp_else(Q)). The evaluator has no built-in opinion aboutif— pure data-driven, exactly what the spec calls for. No-else is the authoring lifter's responsibility (else_branch := skip). - Loops:
Refusal::OpaqueLoopis checked before recursion into the loop body. The body is never recursed into. Loops cannot cause non-termination of the evaluator. Right call for PR1. - Unresolved / unknown ops:
Refusal::OpaqueCallfor both. Naming the callee. Correct. - Totality: every
Termvariant covered; everyIrFormulavariant covered inreduce_formula. The one.unwrap()(synthesize_value_ruleline 292) is guarded byif conj.len() == 1. Recursion bottoms out on finite term trees; loops refuse; no cyclic-vocabulary risk. No panic path under normal data. - Determinism:
HashSet(infree_vars_*) is used only for.containsandfresh_name'su32counter walk — no iteration order leaks into output.reduce_eachis.into_iter().map().collect(). Rule lookup by name. ✓ - Schema-node elimination:
reduce_formularecurses through every operand / body / target / args.Substitutereduces the target first, thensubstitute_in_formula(which preserves but does not eliminate nestedSubstitute/Apply) — but the target is already reduced, and thetermside is anIrTerm(cannot contain formula schema nodes).Applyreturnswp(slot_term, arg)which is itself fully reduced. The tests'contains_schema_nodeassertions are tight.
Grammar extension is correctly locked
IrFormula::Substitute { target, term, var }with JCS key orderkind, target, term, var(CDDLSubstituteFormula);IrFormula::Apply { args, fn }with key orderargs, fn, kind(CDDLApplyFormula). Verified against#[serde(rename = ...)]and the CDDL file. Pinned CIDs (PINNED_SUBSTITUTE_NODE_CID/PINNED_APPLY_NODE_CID) lock the wire encoding.- The
Qplaceholder =Atomic { name: "Q", args: [] }encoding is sound. Collision risk with a legitimately-named predicateQis theoretical only — the convention is documented and the placeholder is reserved by name; a contract author choosingQas an unrelated atomic name would be self-inflicting. Worth keeping an eye on once the hub ops migrate (PR2). - Every previously-exhaustive
matchonIrFormulagot a new arm: coq, lean, smt-lib emitter/validator/opacity/free-vars/ctor-decls/outlives, ir-symbolic, aarch64. None silently miscompile; they all refuse loudly (unreachable!orErr).
Nits (none blocking)
- PR-body "byte-equivalent" claim is slightly overstated. In
substitute_in_term'sLetarm, the newlibprovekit::wpversion (a) checksb.name == var_nameshadowing before the alpha-rename block, and (b) extends thetakenset with prior bindings' (possibly-renamed) names. Both are strict improvements over the oldcompose.rscopy. Concretely: the old code, when aLetbinder's name equalsvar_nameandvar_nameis free in the replacement, would alpha-rename the shadowing binder away instead of stopping substitution. The new code shadows correctly. Under Supra omnia, rectum the new behavior is strictly more correct, but the PR body should say "no observable behavior change on any currently-exercised input; the dedup'd version closes a latent capture-edge inLetshadowing" rather than "byte-equivalent by construction." - CDDL
ApplyFormula.args: [+ IrFormula](one-or-more) vs RustVec<IrFormula>(allows empty). Minor laxness;reduce_formula'sApplyarm explicitly handles empty args (None => q.clone()). Either tighten the Rust side to a non-empty vec, or relax the CDDL to[* IrFormula]. Pick one when PR2 lands. - Backend dispatch posture asymmetry. Coq / SMT-LIB-generated / ir-symbolic / aarch64 use
unreachable!()(panic). Lean and the SMT-LIB validator returnErr(CompileError::Internal(...)). Both are loud-not-silent, but the inconsistency deserves a unified posture: I'd lean towardErreverywhere (a compiler backend reached by a malformed input panicking-out is a worse posture than refusing-out, especially when this same plumbing eventually carries attacker-influenced lifter output). Follow-up, not a blocker. - No automated guard that the manual
IrFormulaextension stays in sync withprovekit-ir.cddl. The newcddl_valid.rschecks the grammar file parses; it does not check the Rust enum matches. The comment inprovekit-ir-types/src/lib.rswarns that regenerating from codegen will clobber the manual arms. Inherent to the manual-extension pattern (already used forSort). Worth a follow-up issue for a JSON-roundtrip test against a wire-shape fixture so a CDDL drift is caught.
Why this merges
The evaluator is total, deterministic, schema-node-clean, and the test suite pins both the externally-observable formula shapes (synthesized add / div, Dijkstra if, seq;if;skip body) and the wire encoding of the two new node kinds (BLAKE3-512 CIDs). The grammar extension is conservative — an existing IrFormula is still an IrFormula — and every backend got a refusal arm. provekit-walk is genuinely unbuildable today, so its refactor lands dead-code-ready, which is the right call rather than reverting and re-doing later.
The wp definition itself — pre ∧ Q[result := value_expr] for value-ops, Dijkstra for if, wp(s1, wp(s2, Q)) for seq, refuse for loops / unresolved calls — is textbook Dijkstra-Hoare WP. PR5's ∀Q. wp(concept:op, Q) ⇒ φ(wp(lang:op, Q)) discharge will sit on top of this and it'll hold.
Ship it. Land the nit on the PR-body language before PR2 ideally; the rest can ride along in follow-up issues.
— Opus 4.7 reviewing for Supra omnia, rectum
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…os error 26) flake (#621) Linux refuses exec on a file that still has an open writer fd anywhere on the system. The parallel cargo test runner would write a plugin .sh script then immediately spawn provekit, which internally exec'd the script before the kernel had fully closed the writer fd -- producing intermittent ETXTBSY ("Text file busy", os error 26) on ci (PR #620 run 25707800831). Two-layer fix applied to all five write_executable+spawn sites: 1. write_executable now uses OpenOptions + write_all + sync_all + explicit drop, guaranteeing the fd is fully closed and durably flushed before set_permissions and before the caller spawns. 2. New output_retrying_etxtbsy helper wraps every provekit Command::output() call at a write_executable spawn site, retrying up to 5x with 20-100ms backoff on ETXTBSY stderr hits. The retry is the durable safety net; sync_all+drop is the actual fix. All 13 cli_surface tests pass locally (macOS). The race is Linux-only; the CI green on the new branch is the real signal. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 12, 2026
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…al-wp-rule-abstraction discharge (wp-as-formula PR 3/N) Adds machine-checkable wp_rule to c11 and rust control-flow op specs (if, seq, skip, source-unit), per spec section 1.2: wp_rule is REQUIRED on Stmt-sorted ops and OPTIONAL (synthesizable) on value-ops. Key design decisions: - wp_rule is a per-language annotation in language-sig specs; concept-shape hub ops do NOT yet carry it (deferred to #633 per spec s1.4). concept_spec_from_base strips wp_rule after deep-copy so hub op CIDs do not change when a language spec adds it (PR3+). Once #633 lands the strip should be replaced by an OPS-table-driven authoritative wp_rule. - A new 4th structural discharge strategy "structural-wp-rule-abstraction" handles morphisms where the only CID difference is the presence of wp_rule in the language spec that the concept spec lacks. - The 6 control-flow PRIMITIVE_STEMS (c11+rust if/seq/skip) are removed from the short-circuit cache because their source CIDs changed when wp_rule was added. Return and eq stems are unaffected and remain cached. Morphism count: 143 (matches HEAD baseline, no regression). Byte-stable: two consecutive mint runs produce zero file changes. Tests: libprovekit transport (4/4), ci (7/7), ci_check (15/15), transport_cli (8/8), lower_formula (2/2) all pass. Depends on #620 (wp_rule schema + evaluator, PR 1/N). Note: #633 (feat/wp-as-formula-2-hub-op-rules) will add wp_rule to concept hub op specs and supersede the strip in concept_spec_from_base. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…al-wp-rule-abstraction discharge (wp-as-formula PR 3/N) Adds machine-checkable wp_rule to c11 and rust control-flow op specs (if, seq, skip, source-unit), per spec section 1.2: wp_rule is REQUIRED on Stmt-sorted ops and OPTIONAL (synthesizable) on value-ops. Key design decisions: - wp_rule is a per-language annotation in language-sig specs; concept-shape hub ops do NOT yet carry it (deferred to #633 per spec s1.4). concept_spec_from_base strips wp_rule after deep-copy so hub op CIDs do not change when a language spec adds it (PR3+). Once #633 lands the strip should be replaced by an OPS-table-driven authoritative wp_rule. - A new 4th structural discharge strategy "structural-wp-rule-abstraction" handles morphisms where the only CID difference is the presence of wp_rule in the language spec that the concept spec lacks. - The 6 control-flow PRIMITIVE_STEMS (c11+rust if/seq/skip) are removed from the short-circuit cache because their source CIDs changed when wp_rule was added. Return and eq stems are unaffected and remain cached. Morphism count: 143 (matches HEAD baseline, no regression). Byte-stable: two consecutive mint runs produce zero file changes. Tests: libprovekit transport (4/4), ci (7/7), ci_check (15/15), transport_cli (8/8), lower_formula (2/2) all pass. Depends on #620 (wp_rule schema + evaluator, PR 1/N). Note: #633 (feat/wp-as-formula-2-hub-op-rules) will add wp_rule to concept hub op specs and supersede the strip in concept_spec_from_base. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…al-wp-rule-abstraction discharge (wp-as-formula PR 3/N) Adds machine-checkable wp_rule to c11 and rust control-flow op specs (if, seq, skip, source-unit), per spec section 1.2: wp_rule is REQUIRED on Stmt-sorted ops and OPTIONAL (synthesizable) on value-ops. Key design decisions: - wp_rule is a per-language annotation in language-sig specs; concept-shape hub ops do NOT yet carry it (deferred to #633 per spec s1.4). concept_spec_from_base strips wp_rule after deep-copy so hub op CIDs do not change when a language spec adds it (PR3+). Once #633 lands the strip should be replaced by an OPS-table-driven authoritative wp_rule. - A new 4th structural discharge strategy "structural-wp-rule-abstraction" handles morphisms where the only CID difference is the presence of wp_rule in the language spec that the concept spec lacks. - The 6 control-flow PRIMITIVE_STEMS (c11+rust if/seq/skip) are removed from the short-circuit cache because their source CIDs changed when wp_rule was added. Return and eq stems are unaffected and remain cached. Morphism count: 143 (matches HEAD baseline, no regression). Byte-stable: two consecutive mint runs produce zero file changes. Tests: libprovekit transport (4/4), ci (7/7), ci_check (15/15), transport_cli (8/8), lower_formula (2/2) all pass. Depends on #620 (wp_rule schema + evaluator, PR 1/N). Note: #633 (feat/wp-as-formula-2-hub-op-rules) will add wp_rule to concept hub op specs and supersede the strip in concept_spec_from_base. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…al-wp-rule-abstraction discharge (wp-as-formula PR 3/N) Adds machine-checkable wp_rule to c11 and rust control-flow op specs (if, seq, skip, source-unit), per spec section 1.2: wp_rule is REQUIRED on Stmt-sorted ops and OPTIONAL (synthesizable) on value-ops. Key design decisions: - wp_rule is a per-language annotation in language-sig specs; concept-shape hub ops do NOT yet carry it (deferred to #633 per spec s1.4). concept_spec_from_base strips wp_rule after deep-copy so hub op CIDs do not change when a language spec adds it (PR3+). Once #633 lands the strip should be replaced by an OPS-table-driven authoritative wp_rule. - A new 4th structural discharge strategy "structural-wp-rule-abstraction" handles morphisms where the only CID difference is the presence of wp_rule in the language spec that the concept spec lacks. - The 6 control-flow PRIMITIVE_STEMS (c11+rust if/seq/skip) are removed from the short-circuit cache because their source CIDs changed when wp_rule was added. Return and eq stems are unaffected and remain cached. Morphism count: 143 (matches HEAD baseline, no regression). Byte-stable: two consecutive mint runs produce zero file changes. Tests: libprovekit transport (4/4), ci (7/7), ci_check (15/15), transport_cli (8/8), lower_formula (2/2) all pass. Depends on #620 (wp_rule schema + evaluator, PR 1/N). Note: #633 (feat/wp-as-formula-2-hub-op-rules) will add wp_rule to concept hub op specs and supersede the strip in concept_spec_from_base. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…al-wp-rule-abstraction discharge (wp-as-formula PR 3/N) Adds machine-checkable wp_rule to c11 and rust control-flow op specs (if, seq, skip, source-unit), per spec section 1.2: wp_rule is REQUIRED on Stmt-sorted ops and OPTIONAL (synthesizable) on value-ops. Key design decisions: - wp_rule is a per-language annotation in language-sig specs; concept-shape hub ops do NOT yet carry it (deferred to #633 per spec s1.4). concept_spec_from_base strips wp_rule after deep-copy so hub op CIDs do not change when a language spec adds it (PR3+). Once #633 lands the strip should be replaced by an OPS-table-driven authoritative wp_rule. - A new 4th structural discharge strategy "structural-wp-rule-abstraction" handles morphisms where the only CID difference is the presence of wp_rule in the language spec that the concept spec lacks. - The 6 control-flow PRIMITIVE_STEMS (c11+rust if/seq/skip) are removed from the short-circuit cache because their source CIDs changed when wp_rule was added. Return and eq stems are unaffected and remain cached. Morphism count: 143 (matches HEAD baseline, no regression). Byte-stable: two consecutive mint runs produce zero file changes. Tests: libprovekit transport (4/4), ci (7/7), ci_check (15/15), transport_cli (8/8), lower_formula (2/2) all pass. Depends on #620 (wp_rule schema + evaluator, PR 1/N). Note: #633 (feat/wp-as-formula-2-hub-op-rules) will add wp_rule to concept hub op specs and supersede the strip in concept_spec_from_base. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…a PR 3/N) (#663) * feat(lift-{c11,rust}): emit wp_rule on control-flow ops; add structural-wp-rule-abstraction discharge (wp-as-formula PR 3/N) Adds machine-checkable wp_rule to c11 and rust control-flow op specs (if, seq, skip, source-unit), per spec section 1.2: wp_rule is REQUIRED on Stmt-sorted ops and OPTIONAL (synthesizable) on value-ops. Key design decisions: - wp_rule is a per-language annotation in language-sig specs; concept-shape hub ops do NOT yet carry it (deferred to #633 per spec s1.4). concept_spec_from_base strips wp_rule after deep-copy so hub op CIDs do not change when a language spec adds it (PR3+). Once #633 lands the strip should be replaced by an OPS-table-driven authoritative wp_rule. - A new 4th structural discharge strategy "structural-wp-rule-abstraction" handles morphisms where the only CID difference is the presence of wp_rule in the language spec that the concept spec lacks. - The 6 control-flow PRIMITIVE_STEMS (c11+rust if/seq/skip) are removed from the short-circuit cache because their source CIDs changed when wp_rule was added. Return and eq stems are unaffected and remain cached. Morphism count: 143 (matches HEAD baseline, no regression). Byte-stable: two consecutive mint runs produce zero file changes. Tests: libprovekit transport (4/4), ci (7/7), ci_check (15/15), transport_cli (8/8), lower_formula (2/2) all pass. Depends on #620 (wp_rule schema + evaluator, PR 1/N). Note: #633 (feat/wp-as-formula-2-hub-op-rules) will add wp_rule to concept hub op specs and supersede the strip in concept_spec_from_base. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix(concept-shapes): eliminate primitive_ops.py dual-mint; add one-name-one-CID invariant Both primitive_ops.py and mint_language_morphisms.py were independently minting the same c11/rust morphisms for conditional/seq/skip/return/eq, producing duplicate catalog files with different CIDs. Root cause: primitive_ops.py built concept specs from c11 source specs directly (stale component-cids.json, no union-effects), while mint_language_morphisms.py used canonical_cid_spec + union-effects across all languages. Fix: - Clear primitive_ops.py OPS list; mint_language_morphisms.py is now the single source of truth for all language morphisms including the five former primitives. - Clear PRIMITIVE_STEMS in mint_language_morphisms.py (no pre-minted stems remain). - Add sweep_stale_catalog_files() to remove orphan CID-named files after each mint. - Raise in append_cids() on (kind,name) conflict with different CID (one-name-one-CID invariant enforced at mint time; previously silently kept the first-registered stale CID). - Add CidInvariantTests.test_one_name_one_cid_in_cids_tsv to test_discharge.py so the invariant is also asserted as a unittest on every subsequent mint run. Two consecutive mint.sh runs produce byte-identical cids.tsv (verified). morphism_count = 172; no duplicate stems in catalog/algorithms. c11/rust x {if,seq,skip} receipts use structural-wp-rule-abstraction discharge. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix(discharge): combine notes-tolerant + wp_rule-aware structural subsumption (rebase merge of #688 + #663) Rebase of feat/wp-as-formula-3-c11-rust-lifters onto origin/main resolved a code conflict in try_structural_subsumption between #688's notes_match guard and #663's wp_rule-aware guard. Both guards are additive over the same early-return condition and over _make_relaxed's wp branch: - #688: adds notes_match to the byte-equality guard; strips documentation-only keys (notes) from the relaxed copy. - #663: adds 'not after_has_wp_rule' to the byte-equality guard; unconditionally pops wp_rule from relaxed['post']. Combined guard (strictly more conservative -- subsumes both prior verdicts under Supra omnia, rectum): if pre_matches and wp_matches and notes_match \ and effects_match and not after_has_wp_rule: Combined _make_relaxed: applies both strip operations. Regenerated mint artifacts (cids.tsv + catalog/index.json) are byte-stable across two consecutive mint.sh runs. morphism_count=161 (main mint) + 12 cell-pattern morphisms = 174 total morphism rows in cids.tsv. Both morphism_java_throw_to_throw and morphism_typescript_throw_to_throw present. morphism_ruby_source_unit_to_source_unit minted (no longer the ghost orphan post-#688). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
3 tasks
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.
Implements PR 1 of the wp-as-formula sub-project, per the normative spec
protocol/specs/2026-05-13-wp-as-formula.md(merged, #613).What this PR is scoped to
Schema + grammar + evaluator + the walk/compose dedup refactor it enables. Not in scope (later PRs): migrating the ~45 concept hub ops to carry
wp_rule(PR 2), the c11 + rust lifters (PR 3), the other 8 lifters (PR 4, one PR with per-lifter receipts), flipping the morphism discharge to a real⊑check (PR 5), moving the desugaringwp-preservation obligations onto the evaluator (PR 6). The hub-op / lifterwp_rules are not touched here; thewp_rulefield is supported and exercised by local test fixtures only.The
wp_rulefield (spec §1)wp_ruleis a term in the existing IR formula language, a sibling ofpre/poston an operation contract, parametric in the reserved postcondition meta-varQand per-Stmt-slot transformer meta-varswp_<slot>. It is synthesized for value-ops frompre/post(wp(op, Q) = pre ∧ Q[result := value_expr], withvalue_exprread off thepost'sresult == value_exprshape), so it is REQUIRED only on the ~10–20 control-flow ops per language; the old prosewpbecomes an optional non-load-bearingwp_note. The operation-contract CDDL with these fields is already in the merged spec (§1.4); the on-wire shape (thepostblock of analgorithmspec, copied verbatim byprovekit-mint-amp) flowswp_rulethrough unchanged, and the JCS canonicalizer handles the new optional field byte-deterministically — nothing in the mint path or the canonicalizer needed editing for that. Test fixtures inwp::testscarry authoredwp_rules for the control-flow ops (if= the Dijkstra rule,seq=wp_first(wp_second(Q)),return=Q[result := value],skip=Q); value-ops (add,div,uop_neg,bop_eq) carry onlypre/postand exercise the synthesis path.The
substitute/applygrammar nodes (spec §2.3)Two new
IrFormulanodes — the smallest addition that lets awp_rulebe written in the formula language the rest of the substrate already speaks:substitute { target, var, term }— explicit, capture-avoiding, single-variable substitution on a formula:Q[var := term]. Needed as a node because in awp_ruleschema thetargetis the postcondition meta-var, not yet known; oncetargetis ground the node is eliminated by performing the substitution. CDDL locked key order:kind, target, term, var.apply { fn, args }— application of a slot-transformer meta-var (wp_<slot>) to one formula argument:apply(wp_<slot>, X)is "the weakest precondition of the term in slot<slot>w.r.t. X." Eliminated by inlining the actual slot transformer. CDDL locked key order:args, fn, kind.Both are conservative extensions (an existing IrFormula is still an IrFormula) and reduce to the existing grammar when fully instantiated. The postcondition meta-var
Qis the nullary atomic predicateAtomic { name: "Q", args: [] }(the IR formula grammar has novarnode; a propositional variable is a nullary atomic — confirmed against howprovekit-walklifts branch conditions). Added toprotocol/provekit-ir.cddl, toprovekit-ir-types(manual codegen extension, like theSortgrow; CDDL stays source of truth), and swept across every now-non-exhaustivematchonIrFormulain the workspace (the coq + smt-lib + lean compilers,provekit-ir-symbolic's conversion, the smt-lib validator, the aarch64 lifter) with a uniform refusal arm — these nodes never reach those sites oncelibprovekit::wphas run, so reaching the arm is a bug. Plusprovekit-ir-codegen/tests/cddl_valid.rs— the protocol grammar must parse + validate under thecddlcrate (guards the grammar file when new node kinds are added).libprovekit::wp— the evaluator (spec §2)New module
implementations/rust/libprovekit/src/wp.rs(+wp/tests.rs), three things:IrFormula/IrTerm, plus free-variable computation. Previously duplicated betweenprovekit-walk'swp.rsandlibprovekit::compose(the latter's source comments call it out: "duplicated from walk's wp.rs"). Now a single canonical home here (CCP §5: one primitive, every consumer).compose.rsdeletes its copy and re-exports fromwp;provekit-walk/src/wp.rsdoes the same. No observable behavior change towalkorcompose(theirresult == value_exprextraction, their byte-identical output, their tests are unaffected).substitutewith a groundtarget→ perform the substitution;apply(wp_<slot>, X)→ recurse into the slot's sub-term withX. Afterwp(t, Q)with a groundQthe result formula contains noSubstitute/Applynodes and noQ-placeholder — asserted in the tests viacontains_schema_node.wp(t, Q)— structural recursion over the term. For each op node: look up its contract; take its authoredwp_ruleor synthesize one for a value-op frompre/post; instantiate with thisQ, the recursively-computedwps of theStmt-typed sub-terms (for thewp_<slot>meta-vars), and the values of the value-typed sub-terms (for the formals). Handles:seq(s1,s2)→wp_s1(wp_s2(Q));if-style → the Dijkstra rule(c ⇒ wp_s1(Q)) ∧ (¬c ⇒ wp_s2(Q));while/loops →Refusal::OpaqueLoop { loop_cid }naming the missingLoopInvariantMemento(until the resolver supplies an instantiated rule); unresolved/indirect calls and unknown ops →Refusal::OpaqueCall { callee }. The evaluator is total (always a formula or a namedRefusal/WpError— never a panic), deterministic (recursion order fixed by slot order; the computedwpis canonicalized + content-addressed downstream, so nondeterminism would be a correctness bug), and makes no solver call (pure formula construction; z3 comes in at the discharge step of spec §3, later).OpContractInfo+OpContractResolverare the consumed-contract view + lookup trait; the catalog-backed resolver lands with the hub-op migration (PR 2).Module structure
wp.rs: reserved-name constants +postcondition_placeholder();Refusal(OpaqueLoop / OpaqueCall);SlotKind/SlotInfo/OpContractInfo(withvalue_expr(),synthesize_value_rule(),rule()) /OpContractResolver;WpError(ArityMismatch / NoRule / MalformedRule / Refused);wp+wp_with_result_var(the public entry) →wp_op→value_expr_of_term;reduce_formula(the schema-node eliminator);find_result_equation; the substitution algebra + free-vars (the canonical home).wp/tests.rs: 17 tests — synthesizedwpforadd(pre ∧ Q[result := lhs+rhs]) anddiv(not_zero(rhs) ∧ Q[result := lhs/rhs]), incl. aQthat mentionsresult; the authored Dijkstra-ifrule instantiated onif(bop_eq(x,0), return(uop_neg(22)), return(x)); the evaluator onseq(if(c, return(x), return(y)), skip); the opaque-loop / unresolved-call / unknown-op / malformed-rule / arity-mismatch paths;substitute/applyserde round-trip + pinned BLAKE3-512 CIDs (byte-determinism — Supra omnia, rectum).Verification
cargo test -p libprovekit(incl.wp+compose): all pass (17 inwp::tests).cargo test -p provekit-ir-types -p provekit-canonicalizer: all pass.cargo test -p provekit-ir-compiler-{smt-lib,coq,lean} -p provekit-ir-symbolic -p provekit-lift-asm-aarch64: all pass (the swept crates).cargo test -p provekit-ir-codegen --test cddl_valid: pass —protocol/provekit-ir.cddlparses + validates under thecddlcrate.cargo build --manifest-path implementations/rust/Cargo.toml: clean, no warnings inlibprovekit.git diff --check: clean.cargo test --workspace --no-fail-fasthas some red —provekit-bug-zoo/provekit-supply-chain-railssmoke,provekit-cli mint_kit_integrationCID pins,provekit-linker --doc("can't find crate forprovekit_verifier"). These are pre-existing: verified by runningrust_kit_contract_set_cid_is_pinned_to_self_contracts_canonicalon a pristineorigin/mainworktree — it fails identically there. Not caused by this PR.Note on
provekit-walkThe Rust
provekit-walkcrate is not currently a workspace member — it was dropped fromimplementations/rust/Cargo.toml'smembersat commit5ec16225(PR #387, a baselines chore), and itsversion.workspace = truemakes it unbuildable standalone; nothing in CI builds it. Itssrc/wp.rsis updated here for the refactor (it re-exports the moved substitution functions fromlibprovekit::wp;src/contract.rskeeps importinglibprovekit::compose::substitute_in_formula, which still resolves via the new re-export) — the change lands ready for the momentwalkre-joins the workspace. The task'scargo test -p provekit-walkverify line therefore can't run today regardless of this PR.Next PRs (~6 total)
wp_rule(+ renamewp→wp_note); 3. the c11 + rust lifters; 4. the other 8 lifters (one PR, per-lifter receipts); 5. flip the morphism discharge from the two structural relaxations to a real∀Q. wp(concept:op,Q) ⇒ φ(wp(lang:op,Q))check; 6. move the desugaringwp-preservation obligations onto the evaluator (wp(lhs,Q) ⇔ wp(rhs,Q)as a portfolio bi-implication).🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Bug Fixes
Tests