feat(lifter): v0.6: expanded assert! body predicate grammar#82
Conversation
Brings the TS vitest-tests adapter toward Rust v0.5 PR #55 parity. A chained method call on an operand (e.g. `"hello".toUpperCase()`) now lifts as `Ctor("toUpperCase", [recv])` instead of skipping. Receiver and every argument compose recursively through liftOperand, so nested shapes like `f(a).g(b)` are handled when both halves are themselves liftable. The previous v0.5 negative test (asserting method-chain skip) was inverted in place to assert the new positive behavior, with a comment flagging the inversion. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Relax the v0 single-arg gate. `f(a, b, c)` and `Module.fn(a, b)` now
lift as `Ctor("f", [a, b, c])` and `Ctor("Module.fn", [a, b])`
respectively. Every argument must itself be liftable; the recursion
makes nested calls and the slice-1 method calls compose without
extra plumbing.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`a + b`, `a - b`, `a * b`, `a / b`, `a % b` in operand position now
lift to `Ctor("<op>", [a, b])`. Both operands recurse through
liftOperand, so `f(x) + g(y)` composes via the slice-2 multi-arg path.
Comparison and short-circuit logical operators are deliberately
excluded from term position; they belong in formula position and
will be added in a separate predicate-level slice.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`[a, b, c]` in operand position now lifts as `Ctor("array", [a, b, c])`,
matching Rust v0.5's naming. Sparse elements and spreads skip with a
named reason instead of falling through to the catch-all whitelist
message. Composes with the multi-arg call slice so a property like
`expect(sort([3, 1, 2])).toEqual([1, 2, 3])` lifts end to end.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… catch-all
Two improvements to skip-reporting:
1. Ternary `cond ? a : b` in operand position now skips with a v0.6-
specific reason ("ternary ... operand is not lifted in v0.6") rather
than falling through to the catch-all. Searchable in lift reports
so a future v0.7 can target this shape directly.
2. The catch-all reason was bumped from "v0 lift whitelist" to "v0.6
lift whitelist" and the enumerated unsupported shapes were brought
in line with what slices 1-4 now accept (method chains, multi-arg
calls, and arithmetic ops removed from the bullet list).
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. |
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (2)
WalkthroughThe PR extends the TypeScript vitest adapter to support v0.6 operand lifting forms: free-function and method calls are lifted as constructor terms with arguments; array literals become ChangesExtended Operand Lifting for v0.6
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~20 minutes Poem
🚥 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. Review rate limit: 0/1 reviews remaining, refill in 60 minutes.Comment |
There was a problem hiding this comment.
Pull request overview
Updates the TypeScript vitest-tests lifter adapter to accept additional v0.6 operand shapes (closer to Rust v0.5 parity), with corresponding vitest-driven witnesses.
Changes:
- Expand
liftOperandto lift UFCS-style method calls, multi-arg/zero-arg calls, array literals, and selected arithmetic binary operators; add a dedicated ternary skip reason. - Add new adapter-level tests covering the newly supported operand shapes and the improved ternary skip reason.
- Refresh the generic “operand whitelist” skip reason to reference v0.6 and enumerate unsupported shapes.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| implementations/typescript/src/lift/vitest-tests.test.ts | Adds new positive/negative tests for v0.6 operand lifting (method calls, multi-arg calls, binops, arrays, ternary skip reason). |
| implementations/typescript/src/lift/adapters/vitest-tests.ts | Extends operand lifting grammar (calls/methods/arrays/binops/ternary) and adds binaryOperatorCtorName. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // Free-function call (zero-or-more args) and `Module.fn(...)` static | ||
| // call. v0.6 relaxes v0's single-arg gate; every argument must itself | ||
| // lift. Method calls (`recv.fn(...)`) are handled by the next clause. | ||
| if ( | ||
| ts.isCallExpression(expr) && | ||
| (ts.isIdentifier(expr.expression) || | ||
| (ts.isPropertyAccessExpression(expr.expression) && | ||
| ts.isIdentifier(expr.expression.expression) && | ||
| ts.isIdentifier(expr.expression.name))) | ||
| ) { | ||
| const callee = expr.expression; | ||
| let name: string | null = null; | ||
| if (ts.isIdentifier(callee)) name = callee.text; | ||
| else if ( | ||
| ts.isPropertyAccessExpression(callee) && | ||
| ts.isIdentifier(callee.expression) && | ||
| ts.isIdentifier(callee.name) | ||
| ) { | ||
| // Allow `Module.fn(arg)` style ctor-call only when the receiver | ||
| // is itself a bare identifier (no chains). | ||
| name = `${callee.expression.text}.${callee.name.text}`; | ||
| let name: string; | ||
| if (ts.isIdentifier(callee)) { | ||
| name = callee.text; | ||
| } else { | ||
| // PropertyAccess; bare-identifier receiver only (no chains). | ||
| const pa = callee as ts.PropertyAccessExpression; | ||
| name = `${(pa.expression as ts.Identifier).text}.${pa.name.text}`; | ||
| } | ||
| const argTerms: IrTerm[] = []; | ||
| for (const a of expr.arguments) { | ||
| const lifted = liftOperand(a); | ||
| if (lifted.kind === "skip") return lifted; | ||
| argTerms.push(lifted.term); | ||
| } | ||
| return { kind: "ok", term: { kind: "ctor", name, args: argTerms } }; | ||
| } | ||
| // v0.6: method call on operand. `recv.method(...args)` lifts as a | ||
| // UFCS-style ctor where the receiver becomes the first argument. | ||
| // Mirrors Rust v0.5 PR #55. We require both receiver and every | ||
| // argument to themselves be liftable; this composes recursively | ||
| // through nested chains. | ||
| if ( | ||
| ts.isCallExpression(expr) && | ||
| ts.isPropertyAccessExpression(expr.expression) && | ||
| ts.isIdentifier(expr.expression.name) && | ||
| !expr.expression.questionDotToken | ||
| ) { | ||
| const recv = liftOperand(expr.expression.expression); | ||
| if (recv.kind === "skip") return recv; | ||
| const argTerms: IrTerm[] = []; | ||
| for (const a of expr.arguments) { | ||
| const lifted = liftOperand(a); | ||
| if (lifted.kind === "skip") return lifted; | ||
| argTerms.push(lifted.term); | ||
| } | ||
| if (!name) return { kind: "skip", reason: "call target shape unsupported" }; | ||
| const inner = liftOperand(expr.arguments[0]!); | ||
| if (inner.kind === "skip") return inner; | ||
| return { kind: "ok", term: { kind: "ctor", name, args: [inner.term] } }; | ||
| return { | ||
| kind: "ok", | ||
| term: { kind: "ctor", name: expr.expression.name.text, args: [recv.term, ...argTerms] }, | ||
| }; |
| if ( | ||
| ts.isCallExpression(expr) && | ||
| (ts.isIdentifier(expr.expression) || | ||
| (ts.isPropertyAccessExpression(expr.expression) && | ||
| ts.isIdentifier(expr.expression.expression) && | ||
| ts.isIdentifier(expr.expression.name))) | ||
| ) { | ||
| const callee = expr.expression; | ||
| let name: string | null = null; | ||
| if (ts.isIdentifier(callee)) name = callee.text; | ||
| else if ( | ||
| ts.isPropertyAccessExpression(callee) && | ||
| ts.isIdentifier(callee.expression) && | ||
| ts.isIdentifier(callee.name) | ||
| ) { | ||
| // Allow `Module.fn(arg)` style ctor-call only when the receiver | ||
| // is itself a bare identifier (no chains). | ||
| name = `${callee.expression.text}.${callee.name.text}`; | ||
| let name: string; | ||
| if (ts.isIdentifier(callee)) { | ||
| name = callee.text; | ||
| } else { | ||
| // PropertyAccess; bare-identifier receiver only (no chains). | ||
| const pa = callee as ts.PropertyAccessExpression; | ||
| name = `${(pa.expression as ts.Identifier).text}.${pa.name.text}`; | ||
| } |
| kind: "skip", | ||
| reason: "operand shape not in v0 lift whitelist (no method chains, member chains, multi-arg calls, complex nesting)", | ||
| reason: | ||
| "operand shape not in v0.6 lift whitelist (no member chains, indexing, field access, closures, blocks, ranges, comparisons in operand position, or template literals)", |
Step #1 of the substrate-types wiring sequence (per admissibility-spine #796 next phase). Adapts every Rust caller of compose_chain_contracts to the new Result<_, CompositionRefusalMemento> signature landed in #827. Call sites updated: - libprovekit/src/ffi.rs:390 — FfiError::ComposeRefused carries the refusal memento, formats CID + serialized refusal artifact - provekit-cli/src/cmd_compose.rs:343 — compose RPC maps refusal into refusal_cid + full refusal JSON payload - provekit-walk/src/chain.rs:85 — walk method-chain wrapper now returns Result<Option<_>, CompositionRefusalMemento> Integration tests added: - ffi_smoke::rust_jcs_entrypoint_impure_input_returns_stable_refusal_cid - compose_rpc_smoke::compose_rpc_impure_input_returns_refusal_memento_with_stable_cid - compose_method_chain_refusal::compose_method_chain_impure_input_returns_stable_refusal_cid Each test exercises an impure-input failure and asserts the refusal CID is non-empty AND deterministic across two runs (per spec §0.1 determinism guarantee). Pre-existing failures (NOT introduced here): - provekit-bridgeworks::smoke::checked_add_exhibit_passes (also fails on clean main without this PR applied) - provekit-cli::cli_surface::lift_zig_shows_production_composes_but_unit_tests_conflict (Zig .zig-cache PermissionDenied, environment flake; matches the ETXTBSY/zig flake notes in memory #72/#82) Co-authored-by: T Savo <agentwopr@gmail.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Summary
Brings the TypeScript
vitest-testslift adapter toward Rust v0.5 (PR #55) parity. Five coherent slices, one commit per slice, TDD throughout. Every shape gets a positive-or-negative test invitest-tests.test.tsbefore its implementation lands; full suite stays green at 760 passing.New shapes accepted
UFCS method calls.
recv.method(...args)lifts asCtor("method", [recv, ...args]). The previous v0.5 negative test (expect("hello".toUpperCase()).toBe("HELLO")skips) was inverted in place to assert the new positive behavior, with a comment flagging the inversion.Multi-arg AND zero-arg free-function calls. Relaxes the v0 single-arg gate to accept any arity, including zero. Every argument must itself be liftable.
Binary arithmetic in operand position.
+,-,*,/,%lift toCtor("<op>", [a, b]). Comparison and short-circuit logical operators are deliberately excluded from term position.Array literals.
[a, b, c]lifts asCtor("array", [a, b, c]), matching Rust v0.5's naming. Sparse and spread elements skip with a named reason. Composes with slices 1-3, soexpect(sort([3, 1, 2])).toEqual([1, 2, 3])lifts end to end.Better error reporting. Ternary
cond ? a : bin operand position now skips with a v0.6-specific reason (ternary ... operand is not lifted in v0.6) rather than falling through to the catch-all. The catch-all reason itself was bumped from "v0" to "v0.6" and the enumerated unsupported shapes were brought in line with what the new slices accept.Considered but deferred
Ctor("ternary", [cond, a, b]), but the semantics carry a control-flow choice that the IR currently models in formula position viaif-then-else. Defer to a future slice that decides which side of the term/formula boundary it belongs on.expect(a > b).toBe(true)). Currently skip because the binary-op clause excludes comparisons. Lifting them would conflate term and formula position; better to extend the matcher dispatcher to detectexpect(<comparison>).toBe(true)and rewrite it to the equivalent atomic.a && b,a || b,!x). Same reasoning: formula position, not term position.Test plan
pnpm testfrom repo root passes (760 / 766, 2 skipped + 4 todo unchanged from baseline)vitest-tests.test.ts, up from 8)🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Tests