Triangle oracle: test-suite execution via per-framework adapters#2
Merged
Conversation
Shipped as a separate PR stacked on refinements so the adapter layer
can be reviewed independently from the larger property-test body of work.
## Architecture
src/testAdapters/
Adapter.ts — TestAdapter interface, TestInvocation, TestOutcome.
TestOutcomeKind covers pass / fail / error / skipped /
timeout / adapter-error. Every adapter must reduce
every exit condition into one of these.
index.ts — registry. getAdapter(framework) returns the
corresponding adapter or null. New framework =
one new file + one register line.
vitest.ts — VitestAdapter. Spawns `vitest run <file> [-t name]
--reporter=json`, parses testResults[].assertionResults
for pass/fail/error/skip counts. Exports runCommand()
helper reused by the other adapters.
jest.ts — JestAdapter. `jest <file> [-t name] --json --silent`.
Escapes testName so the regex -t behaves as substring.
mocha.ts — MochaAdapter. `mocha <file> [--grep name]
--reporter json`. Reads stats + failures[].
nodeTest.ts — NodeTestAdapter. `node --test <file>`; parses TAP
output because node --test has no CLI name filter.
Filters by testName post-hoc on the parsed lines.
src/testCache.ts
Caches per-test outcomes keyed by
(testFile mtime, testName, sourceFile, sourceFile mtime)
so that unchanged code + unchanged tests skip re-invocation.
Source mtime is included because the test's outcome depends on
the code under test, not just the test file itself.
src/testOracle.ts (extended)
- runTest(projectRoot, framework, reference, sourceFile, timeoutMs)
dispatches to the registry, consults the cache, spawns, caches.
Returns { reference, outcome, cached }.
- runTestsForReferences bounded by maxTests (default 5) so a
function with dozens of referencing tests doesn't explode runtime.
- summarizeTriangle(harnessKind, oracleResults) renders the
agreement / disagreement summary that the caller attaches to the
CheckResult.
src/checkers/PropertyTestChecker.ts (integrated)
After the harness execution step, when NEURALLOG_RUN_ORACLE_TESTS=1
and the project has a detectable test framework, the checker runs
up to 3 referencing tests with a 30s per-test timeout, cross-
references their outcomes against the harness verdict, and
annotates the CheckResult.error with the triangle note. Marks
triangle-disagreement explicitly when harness and tests disagree.
## Opt-in gates
NEURALLOG_RUN_ORACLE_TESTS=1 Enables the execution path.
Off by default — the advisory path
from the refinements branch still
runs when harness synthesis builds
its prompt.
## What the triangle catches
Rigged harnesses the audit (#17) couldn't catch because they test
the wrong property entirely: the audit reads harness code in
isolation; the oracle runs the same function against the project's
own tests, which were written without knowledge of our SMT encoding.
When tests and harness agree, it's strong corroboration. When they
disagree, the encoding is under suspicion.
## Intentionally not included
Actual runtime mutation (take the Z3 witness, modify the test input
to that witness, re-run) is a deeper move requiring per-framework
fixture introspection. Out of scope for v1. The existing-tests-as-
calibration signal is where the yield is.
83 unit tests pass (13 new). Adapter classes unit-tested via the
registry; the spawn-path itself is hard to unit-test without
live processes and is left for integration verification.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Important Review skippedAuto reviews are disabled on base/target branches other than the default branch. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
WalkthroughThis PR introduces a comprehensive test execution framework with standardized adapters for Jest, Mocha, Vitest, and Node.js built-in test runners. It integrates oracle-based test execution into harness synthesis, includes filesystem-backed caching of test outcomes, and provides diagnostic comparison between harness results and actual test execution results. Changes
Sequence Diagram(s)sequenceDiagram
participant Checker as PropertyTestChecker
participant Oracle as Test Oracle
participant Cache as TestCache
participant Adapter as Test Adapter
participant Framework as Test Framework
Checker->>Checker: Start synthesizeAndRunHarnesses
Checker->>Oracle: Detect framework (once per run)
Checker->>Checker: Generate harness outcome
alt NEURALLOG_RUN_ORACLE_TESTS enabled
Checker->>Oracle: runTestsForReferences(outcome)
Oracle->>Cache: get(testFile, testName, source)
alt Cache hit
Cache-->>Oracle: TestOutcome
else Cache miss
Oracle->>Adapter: runTest(invocation)
Adapter->>Framework: Execute test (npx jest/mocha/vitest/node --test)
Framework-->>Adapter: stdout/stderr/exitCode
Adapter->>Adapter: Parse output (JSON/TAP)
Adapter-->>Oracle: TestOutcome
Oracle->>Cache: put(testFile, testName, source, outcome)
end
Oracle-->>Checker: ExecutedOracleResult[]
Checker->>Checker: summarizeTriangle(harness kind, oracle results)
Checker->>Checker: Annotate result with agreement/disagreement
end
Checker->>Checker: Store result in harnessResults
Estimated code review effort🎯 4 (Complex) | ⏱️ ~75 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 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 |
There was a problem hiding this comment.
Pull request overview
This PR adds the “execution” half of the triangle-oracle design: when enabled via NEURALLOG_RUN_ORACLE_TESTS=1, the property-test checker can invoke the project’s existing test runner (via per-framework adapters), cache outcomes, and annotate harness results with a summarized triangle agreement/disagreement signal.
Changes:
- Introduces a test-adapter interface + registry, with initial adapters for vitest/jest/mocha/node
--test. - Adds a test outcome cache (
.neurallog/test-cache) and wires test execution + triangle summarization intoPropertyTestChecker. - Adds unit tests covering triangle summarization, cache behavior, and registry lookup.
Reviewed changes
Copilot reviewed 10 out of 11 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
| src/testOracle.ts | Adds execution API (runTest, runTestsForReferences) and triangle summarization logic. |
| src/checkers/PropertyTestChecker.ts | Runs oracle tests (env-gated) and appends triangle notes to harness results. |
| src/testCache.ts | Implements disk cache for adapter outcomes keyed by test/source metadata. |
| src/testAdapters/Adapter.ts | Defines shared adapter interface and outcome types. |
| src/testAdapters/index.ts | Registers and exposes adapters via a simple registry. |
| src/testAdapters/vitest.ts | Runs vitest with JSON reporter and parses results; provides shared runCommand. |
| src/testAdapters/jest.ts | Runs jest with JSON output and parses results. |
| src/testAdapters/mocha.ts | Runs mocha with JSON reporter and parses results. |
| src/testAdapters/nodeTest.ts | Runs node --test and parses TAP-ish output. |
| src/testOracle.triangle.test.ts | Adds unit tests for triangle summary, cache invalidation, and adapter registry. |
| .gitignore | Ignores .neurallog/test-cache/ artifacts. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+742
to
+748
| const framework = detectTestFramework(this.projectRoot); | ||
| if (framework) { | ||
| const refs = findTestsForFunction(this.projectRoot, cand.contract.function); | ||
| if (refs.length > 0) { | ||
| const oracleResults = await runTestsForReferences( | ||
| this.projectRoot, | ||
| framework, |
Comment on lines
+7
to
+9
| * Cache for test-adapter outcomes. Keyed by (test file mtime-ns, | ||
| * test name, source file hash) so that unchanged code + unchanged | ||
| * tests skips re-invocation. Source file hash is included because |
Comment on lines
+206
to
+223
| /** | ||
| * Run every test reference for a function. Bounded by maxTests to keep | ||
| * total runtime predictable — excess references are skipped with a note. | ||
| */ | ||
| export async function runTestsForReferences( | ||
| projectRoot: string, | ||
| framework: TestFramework, | ||
| references: TestReference[], | ||
| sourceFile: string, | ||
| opts: { maxTests?: number; timeoutMsEach?: number } = {} | ||
| ): Promise<ExecutedOracleResult[]> { | ||
| const maxTests = opts.maxTests ?? 5; | ||
| const timeoutMsEach = opts.timeoutMsEach ?? 30000; | ||
| const results: ExecutedOracleResult[] = []; | ||
| for (const ref of references.slice(0, maxTests)) { | ||
| results.push(await runTest(projectRoot, framework, ref, sourceFile, timeoutMsEach)); | ||
| } | ||
| return results; |
| if (fails.length > 0) agreementFragments.push(`${fails.length} test(s) fail`); | ||
| if (errors.length > 0) agreementFragments.push(`${errors.length} test(s) could not run`); | ||
|
|
||
| const note = `triangle: harness=${harnessKind}, ${agreementFragments.join(", ")}`; |
Comment on lines
+240
to
+255
| const fails = oracleResults.filter((r) => r.outcome.kind === "fail" || r.outcome.kind === "error"); | ||
| const errors = oracleResults.filter((r) => r.outcome.kind === "adapter-error" || r.outcome.kind === "timeout"); | ||
| const harnessSuggestsProblem = harnessKind === "encoding-gap" || harnessKind === "fail" || harnessKind === "violation"; | ||
|
|
||
| const agreementFragments: string[] = []; | ||
| if (passes.length > 0) agreementFragments.push(`${passes.length} test(s) pass`); | ||
| if (fails.length > 0) agreementFragments.push(`${fails.length} test(s) fail`); | ||
| if (errors.length > 0) agreementFragments.push(`${errors.length} test(s) could not run`); | ||
|
|
||
| const note = `triangle: harness=${harnessKind}, ${agreementFragments.join(", ")}`; | ||
| const hasAgreement = | ||
| (harnessSuggestsProblem && fails.length > 0) || | ||
| (!harnessSuggestsProblem && passes.length > 0 && fails.length === 0); | ||
| const hasDisagreement = | ||
| (harnessSuggestsProblem && passes.length > 0 && fails.length === 0) || | ||
| (!harnessSuggestsProblem && fails.length > 0); |
Comment on lines
+741
to
+745
| if (process.env.NEURALLOG_RUN_ORACLE_TESTS === "1") { | ||
| const framework = detectTestFramework(this.projectRoot); | ||
| if (framework) { | ||
| const refs = findTestsForFunction(this.projectRoot, cand.contract.function); | ||
| if (refs.length > 0) { |
1. "unknown" framework wastes work detectTestFramework returns "unknown" when a test script exists but no supported framework is identifiable. Previously we'd still scan every function for referencing tests and then fail adapter lookup per-candidate. Now we classify "unknown" the same as null (no oracle available) up front and short-circuit. 2. TestCache docstring mismatch Docstring claimed "mtime-ns + source file hash"; implementation uses mtimeMs (ms resolution) for both test and source mtimes, no content hashing. Rewrote the docstring to describe reality and explain why mtime is sufficient (note left re: switching to sha256 if content-addressing becomes necessary). 3. runTestsForReferences silent truncation Docstring promised "excess references skipped with a note"; implementation just sliced without telling the caller. Now the excess references are returned with outcome kind "skipped" and a specific message naming the cap, so the caller sees the full picture. 4. summarizeTriangle trailing comma When all oracle outcomes were skipped/errored, the note produced "triangle: harness=pass, " with a trailing comma and empty fragment list. Added an actionable-outcomes check: if no test actually produced a verdict, the note explicitly says "no actionable oracle verdicts" and returns no-agreement/no- disagreement regardless of harness kind. 5. summarizeTriangle harness-error/timeout mis-bucketing The old logic bucketed any harnessKind != "encoding-gap|fail| violation" as "harness suggests no problem" — which would then interpret failing tests under a harness-error (or timeout, or synthesis-failed) as disagreement. Now distinguishes three classes: suggests-problem / suggests-ok / neutral. Neutral harness outcomes always return no-agreement/no-disagreement because the harness itself didn't provide a verdict about the claim. 6. Per-candidate detectTestFramework + findTestsForFunction Both were called inside the synthesizeAndRunHarnesses loop body, parsing package.json + walking test directories for every contract. Hoisted framework detection to once per run. Added oracleRefCache on the checker instance so findTestsForFunction is called at most once per distinct function name. Three new tests covering the corrected summarizeTriangle behaviour: neutral harness kinds, all-skipped outcomes, and the fragment- format regression guard. 85 tests pass (up from 83). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Owner
Author
|
@coderabbitai review |
✅ Actions performedReview triggered.
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 11
🧹 Nitpick comments (1)
src/checkers/PropertyTestChecker.ts (1)
78-84: Use the oracle reference cache for prompt discovery too.
preparestill callsfindTestsForFunctiondirectly, so the new cache only helps execution and not the synthesis prompt path. ReusegetOracleRefsCachedthere to keep discovery once per function per run.Proposed fix
- const testRefs = findTestsForFunction(this.projectRoot, cand.contract.function); + const testRefs = this.getOracleRefsCached(cand.contract.function);Also applies to: 641-648, 676-678
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/checkers/PropertyTestChecker.ts` around lines 78 - 84, prepare is still calling findTestsForFunction directly which bypasses the oracleRefCache; change prepare (and the other occurrences that call findTestsForFunction) to call the existing getOracleRefsCached(fnName) instead so discovery is cached. Locate calls to findTestsForFunction in prepare and the other similar sites and replace them with getOracleRefsCached, ensuring the return types match and removing any duplicate caching logic around oracleRefCache.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@src/testAdapters/mocha.ts`:
- Around line 25-35: The current parsing grabs the first brace match from stdout
(jsonMatch) which can pick up earlier logged objects; change parsing in the
runCommand callback to locate the last JSON object instead (e.g., find the last
'{' and the last '}' or use a regex that returns the last {...} block),
JSON.parse that last block into report, and validate report.stats exists before
returning success; if parsing fails or stats is missing return an adapter-error
with a clear message. Ensure you update the error branches around JSON.parse and
the "no JSON block" case to reflect the new last-block extraction and the stats
validation so non-reporter logs no longer break mocha adapter.
In `@src/testAdapters/nodeTest.ts`:
- Around line 5-21: The NodeTestAdapter's runTest invocation must add the Node
flags to force TAP output and enable name filtering: include
"--test-reporter=tap" unconditionally and, when inv.testName is present, pass
"--test-name-pattern" with the testName (instead of running the whole file and
post-filtering). Update the runCommand call construction in runTest (and any
arg-building helper) to conditionally append "--test-name-pattern" based on
inv.testName. Also relax the TAP-parsing regexes used later in this file (the
patterns that detect individual test lines and the TAP summary) to allow
optional leading whitespace so they match lines with indentation or leading
spaces.
In `@src/testAdapters/vitest.ts`:
- Around line 105-114: In the child.on("close") handler, guard the call to
parse(stdout, stderr, exitCode) with a try/catch so any thrown errors don't
escape; if parse throws, produce/resolve an adapter-error result instead of
letting the exception propagate. Specifically, wrap the parse call inside a try
block within the child.on("close") callback (where settled, timer, stdout,
stderr, start are in scope), and in the catch create/resolve the promise with an
adapter-error payload (or a standardized error object expected by the adapter)
and still include durationMs and rawOutput before returning.
- Around line 17-18: The code currently pushes inv.testName directly into args
(in the block with if (inv.testName) { args.push("-t", inv.testName); }), which
passes unescaped text to Vitest's RegExp-based -t option; fix this by escaping
regex metacharacters before pushing: implement or use an escapeRegExp helper
that replaces characters like . * + ? ^ $ { } ( ) | [ ] \ / with escaped
versions and then call args.push("-t", escapeRegExp(inv.testName)); ensure the
helper is named so it’s easy to find and reused within this module.
- Around line 78-83: The current spawn call (spawn(cmd, args, { cwd, env:
process.env })) only kills the direct child via child.kill("SIGKILL") so workers
survive; change the spawn to set detached: true on non-Windows platforms
(preserving cwd and env) so the child runs in its own process group, and on
timeout kill the whole group using process.kill(-child.pid, "SIGKILL") (guard
for child.pid and platform). For Windows, instead of child.kill, call taskkill
/PID <pid> /T /F (using child.pid) to terminate the full process tree. Update
the timer cleanup branch around the timer/settled logic (where
child.kill("SIGKILL") is called) to perform platform-specific full-tree
termination and still resolve/reject as before.
In `@src/testCache.ts`:
- Around line 24-43: The key() function uses statSync(testFile) and
statSync(sourceFile) relative to process.cwd(), so resolve those paths against
the repository root stored in the class before statting: update the constructor
to retain projectRoot (e.g., this.projectRoot = projectRoot) and in key()
compute resolvedTest = path.resolve(this.projectRoot, testFile) and
resolvedSource = path.resolve(this.projectRoot, sourceFile) (or join) and call
statSync on those resolved paths; keep existing try/catch behavior and the rest
of the hash logic unchanged (references: constructor, this.dir, key,
createHash).
In `@src/testOracle.triangle.test.ts`:
- Line 5: The mtime-based invalidation test flakes because it waits 10ms for the
filesystem timestamp to change; instead of sleeping, after rewriting the file
call fs.utimesSync (or fs.promises.utimes) to explicitly advance the file mtime
so TestCache observes a different timestamp. Locate the rewrite step in
src/testOracle.triangle.test.ts (the block that writes the file and currently
waits ~10ms around lines 100-112), remove the delay and after writeFileSync call
utimesSync(filePath, newAtime, newMtime) with a newMtime (e.g., Date.now()/1000
+ 1 or Date.now()/1000 + 2) to force a changed mtime so TestCache invalidation
becomes deterministic.
In `@src/testOracle.ts`:
- Line 219: The default maxTests value in src/testOracle.ts currently allows 5
when callers omit opts.maxTests; change the default to 3 to match the PR
contract by replacing the initialization of maxTests (const maxTests =
opts.maxTests ?? 5) with a default of 3 (opts.maxTests ?? 3) in the function
that defines maxTests (look for the test/oracle entry function that declares
maxTests) so callers that omit maxTests are capped at 3 tests.
- Around line 192-197: The code awaits adapter.runTest(...) directly so any
thrown exception causes the checker to reject instead of returning an oracle
result; wrap the adapter.runTest call in a try/catch around the await (where
outcome is assigned) and on error return/assign a structured "adapter-error"
outcome object (matching the oracle result shape your system uses) containing
the error message/stack and contextual fields (projectRoot, testFile, testName,
timeoutMs) so failures from adapter.runTest are normalized into an adapter-error
outcome instead of bubbling as exceptions.
- Around line 289-294: The current logic in src/testOracle.ts sets hasAgreement
when any failure exists for harnessSuggestsProblem even if there are passing
tests, which hides mixed verdicts; update the definitions of hasAgreement and
hasDisagreement (the variables named hasAgreement, hasDisagreement) so that
agreement requires unanimous oracle results that match the harness suggestion
(for harnessSuggestsProblem: fails.length > 0 and passes.length === 0; for
harnessSuggestsOk: passes.length > 0 and fails.length === 0), and disagreement
is true whenever any oracle result contradicts the harness suggestion (for
harnessSuggestsProblem: passes.length > 0; for harnessSuggestsOk: fails.length >
0), using the existing symbols harnessSuggestsProblem, harnessSuggestsOk,
passes, and fails to locate and change the logic.
- Around line 180-181: The cache lookup uses only testFile/testName/source
(cache.get(testFile, reference.testName, sourceAbs)) but TestCache.key must
include the framework/adapter identity so results from one adapter aren’t reused
for another; update all cache.get and cache.set calls (e.g., the lines using
cache.get(...) at src/testOracle.ts) to pass the framework/adapter identifier
(e.g., frameworkId or adapterName) and modify TestCache.key (testCache.ts:29–45)
signature to accept and incorporate that identifier into the hash generation so
the cache key is unique per framework/adapter.
---
Nitpick comments:
In `@src/checkers/PropertyTestChecker.ts`:
- Around line 78-84: prepare is still calling findTestsForFunction directly
which bypasses the oracleRefCache; change prepare (and the other occurrences
that call findTestsForFunction) to call the existing getOracleRefsCached(fnName)
instead so discovery is cached. Locate calls to findTestsForFunction in prepare
and the other similar sites and replace them with getOracleRefsCached, ensuring
the return types match and removing any duplicate caching logic around
oracleRefCache.
🪄 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: fcdc042b-f8a8-4c9c-b259-2b4c7f55c134
📒 Files selected for processing (11)
.gitignoresrc/checkers/PropertyTestChecker.tssrc/testAdapters/Adapter.tssrc/testAdapters/index.tssrc/testAdapters/jest.tssrc/testAdapters/mocha.tssrc/testAdapters/nodeTest.tssrc/testAdapters/vitest.tssrc/testCache.tssrc/testOracle.triangle.test.tssrc/testOracle.ts
Comment on lines
+25
to
+35
| return runCommand("npx", args, inv.projectRoot, inv.timeoutMs, start, (stdout) => { | ||
| const jsonMatch = stdout.match(/\{[\s\S]*\}/); | ||
| if (!jsonMatch) { | ||
| return { kind: "adapter-error" as const, message: "no JSON block in mocha output" }; | ||
| } | ||
| let report: any; | ||
| try { | ||
| report = JSON.parse(jsonMatch[0]); | ||
| } catch (e: any) { | ||
| return { kind: "adapter-error" as const, message: `could not parse mocha JSON: ${e?.message?.slice(0, 80)}` }; | ||
| } |
There was a problem hiding this comment.
Avoid parsing from the first brace in stdout.
A Mocha test that logs an object before the JSON reporter can make this greedy match include non-report output, turning a valid run into adapter-error. Parse the reporter object from the end and validate it has stats.
Proposed fix
- const jsonMatch = stdout.match(/\{[\s\S]*\}/);
- if (!jsonMatch) {
- return { kind: "adapter-error" as const, message: "no JSON block in mocha output" };
- }
let report: any;
- try {
- report = JSON.parse(jsonMatch[0]);
- } catch (e: any) {
- return { kind: "adapter-error" as const, message: `could not parse mocha JSON: ${e?.message?.slice(0, 80)}` };
+ let parseError: any;
+ for (let i = stdout.lastIndexOf("{"); i >= 0; i = stdout.lastIndexOf("{", i - 1)) {
+ try {
+ const candidate = JSON.parse(stdout.slice(i));
+ if (candidate?.stats) {
+ report = candidate;
+ break;
+ }
+ } catch (e: any) {
+ parseError = e;
+ }
+ }
+ if (!report) {
+ return { kind: "adapter-error" as const, message: `could not parse mocha JSON: ${parseError?.message?.slice(0, 80) || "no JSON report in mocha output"}` };
}🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testAdapters/mocha.ts` around lines 25 - 35, The current parsing grabs
the first brace match from stdout (jsonMatch) which can pick up earlier logged
objects; change parsing in the runCommand callback to locate the last JSON
object instead (e.g., find the last '{' and the last '}' or use a regex that
returns the last {...} block), JSON.parse that last block into report, and
validate report.stats exists before returning success; if parsing fails or stats
is missing return an adapter-error with a clear message. Ensure you update the
error branches around JSON.parse and the "no JSON block" case to reflect the new
last-block extraction and the stats validation so non-reporter logs no longer
break mocha adapter.
Comment on lines
+5
to
+21
| * Node built-in test runner adapter. Invokes `node --test <file>` and | ||
| * parses the TAP output. Node's test runner doesn't have a name-filter | ||
| * CLI flag equivalent to -t/--grep, so when testName is provided we | ||
| * run the whole file and filter the results by test name afterwards. | ||
| * | ||
| * Detects the TAP summary (# tests, # pass, # fail) for an overall | ||
| * verdict and scans individual test lines for name-specific outcomes. | ||
| */ | ||
| export class NodeTestAdapter implements TestAdapter { | ||
| readonly framework = "node-test"; | ||
| readonly name = "node --test TAP output"; | ||
|
|
||
| async runTest(inv: TestInvocation): Promise<TestOutcome> { | ||
| const start = Date.now(); | ||
| const args = ["--test", inv.testFile]; | ||
|
|
||
| return runCommand("node", args, inv.projectRoot, inv.timeoutMs, start, (stdout, _stderr, exitCode) => { |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
cat -n src/testAdapters/nodeTest.ts | head -80Repository: TSavo/provekit
Length of output: 2929
🌐 Web query:
Node.js test runner default reporter TAP spec
💡 Result:
The default reporter for the Node.js test runner (node:test module) is the spec reporter. This has been the case for TTY (interactive terminal) output since its introduction. In Node.js v23.0.0 (2024), the default was changed to spec for all non-TTY stdout as well, aligning both contexts. TAP is available via --test-reporter=tap but is no longer the default in current versions (as of 2026).
Citations:
- 1: https://nodejs.org/docs/latest/api/test.html
- 2: https://nodejs.org/docs/latest-v25.x/api/test.html
- 3: https://nodejs.org/api/test.html
- 4: https://nodejs.org/dist/latest-v20.x/docs/api/test.html
🌐 Web query:
Node.js --test-name-pattern flag filtering tests by name
💡 Result:
The --test-name-pattern flag in Node.js test runner filters tests by running only those whose names match the provided JavaScript regular expression pattern. It is used with the --test flag, e.g., node --test --test-name-pattern="pattern". Key details: - Patterns are JS regex; use /pattern/flags for flags like 'i' for case-insensitive. - Can specify multiple times for multiple patterns or nested tests. - Matches full test name path (ancestors separated by space) for specificity, e.g., --test-name-pattern="test 1 some test" runs only 'some test' under 'test 1'. - Runs corresponding hooks (beforeEach, etc.) for matched tests; skips others silently. - Does not affect which test files are loaded. - Pair with --test-skip-pattern to skip matching tests. - Flags must precede file paths in CLI; npm scripts may need workarounds like NODE_OPTIONS. Examples: node --test --test-name-pattern="test [1-3]" # Runs tests 1,2,3 node --test --test-name-pattern="/test [4-5]/i" # Case-insensitive regex node --test --test-name-pattern="pattern1" --test-name-pattern="pattern2" Added in Node.js v18.11.0 (via commit d762a34); improved for ancestor matching in later versions. Current as of v25.9.0 docs.
Citations:
- 1: https://nodejs.org/api/test.html
- 2: nodejs/node@d762a34128
- 3: https://nodejs.org/docs/latest/api/test.html
- 4: https://blog.appsignal.com/2024/07/17/exploring-the-nodejs-native-test-runner.html
- 5: nodejs/node@00dc6d9d97
Add --test-reporter=tap flag and use --test-name-pattern for filtering.
Node.js v23+ defaults to the spec reporter, but this parser expects TAP format. Without specifying --test-reporter=tap, parsing will fail and return "no TAP test lines parsed" error. Node.js also supports --test-name-pattern (available since v18.11.0), eliminating the need to run the entire file and post-process results.
Update the command to:
- const args = ["--test", inv.testFile];
+ const args = ["--test", "--test-reporter=tap", inv.testFile];
+ if (inv.testName) {
+ const escaped = inv.testName.replace(/[.*+?^${}()|[\]\\]/g, "\\$&");
+ args.push("--test-name-pattern", escaped);
+ }Also update the regex patterns to handle potential leading whitespace in TAP output:
- const testLineRe = /^(ok|not ok)\s+\d+\s*(?:-\s*)?(.*?)(?:\s+#\s*(.+))?$/;
+ const testLineRe = /^\s*(ok|not ok)\s+\d+\s*(?:-\s*)?(.*?)(?:\s+#\s*(.+))?$/;- const failureLine = matchingLines.find((l) => l.startsWith("not ok")) || "";
+ const failureLine = matchingLines.find((l) => /^\s*not ok/.test(l)) || "";🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testAdapters/nodeTest.ts` around lines 5 - 21, The NodeTestAdapter's
runTest invocation must add the Node flags to force TAP output and enable name
filtering: include "--test-reporter=tap" unconditionally and, when inv.testName
is present, pass "--test-name-pattern" with the testName (instead of running the
whole file and post-filtering). Update the runCommand call construction in
runTest (and any arg-building helper) to conditionally append
"--test-name-pattern" based on inv.testName. Also relax the TAP-parsing regexes
used later in this file (the patterns that detect individual test lines and the
TAP summary) to allow optional leading whitespace so they match lines with
indentation or leading spaces.
Comment on lines
+17
to
+18
| if (inv.testName) { | ||
| args.push("-t", inv.testName); |
There was a problem hiding this comment.
🧩 Analysis chain
🌐 Web query:
Vitest 4.1 CLI -t --testNamePattern argument regex or literal string semantics
💡 Result:
In Vitest 4.1 CLI, the -t or --testNamePattern argument accepts a string that is directly passed to the RegExp constructor for matching against the full test name (including describe blocks, e.g., "container the data-quality data-quality: has pattern"). It supports regex semantics: the string is used as new RegExp(pattern), so regex features like ^, $, ., , flags (e.g., ^data-quality/i) work. Literal strings are treated as regex patterns matching the substring anywhere in the full name (unless anchored). No special prefix like /regex/ is needed or parsed; slashes would be literal characters in the regex. Examples: - vitest -t "data-quality" matches tests where full name contains "data-quality" - vitest -t "^data-quality" matches full names starting with "data-quality" - vitest -t "data-quality.$" matches ending with "data-quality" followed by anything - vitest -t "^data-quality/i" case-insensitive start match
Citations:
- 1: testNamePattern doesn't parse RegEx'es in the CLI, or documentation is unclear vitest-dev/vitest#5735
- 2: https://v4.vitest.dev/config/testnamepattern
- 3: https://vitest.dev/config/testnamepattern
- 4: https://github.com/vitest-dev/vitest/blob/6fdb2ba6/test/core/test/cli-test.test.ts
- 5: https://github.com/vitest-dev/vitest/blob/6fdb2ba6/packages/vitest/src/runtime/config.ts
Escape test names before passing them to Vitest -t.
Vitest's -t/--testNamePattern argument is passed directly to the RegExp constructor, so names containing regex metacharacters like +, [, (, ?, ., *, etc. will be interpreted as regex operators rather than literal characters. This causes tests with these characters in their names to either not match or match unintended tests.
Proposed fix
+function escapeRegExp(value: string): string {
+ return value.replace(/[.*+?^${}()|[\]\\]/g, "\\$&");
+}
+
export class VitestAdapter implements TestAdapter {
readonly framework = "vitest";
readonly name = "vitest JSON reporter";
async runTest(inv: TestInvocation): Promise<TestOutcome> {
const start = Date.now();
const args = ["vitest", "run", inv.testFile, "--reporter=json"];
if (inv.testName) {
- args.push("-t", inv.testName);
+ args.push("-t", escapeRegExp(inv.testName));
}📝 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
| if (inv.testName) { | |
| args.push("-t", inv.testName); | |
| if (inv.testName) { | |
| args.push("-t", escapeRegExp(inv.testName)); |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testAdapters/vitest.ts` around lines 17 - 18, The code currently pushes
inv.testName directly into args (in the block with if (inv.testName) {
args.push("-t", inv.testName); }), which passes unescaped text to Vitest's
RegExp-based -t option; fix this by escaping regex metacharacters before
pushing: implement or use an escapeRegExp helper that replaces characters like .
* + ? ^ $ { } ( ) | [ ] \ / with escaped versions and then call args.push("-t",
escapeRegExp(inv.testName)); ensure the helper is named so it’s easy to find and
reused within this module.
Comment on lines
+78
to
+83
| const child = spawn(cmd, args, { cwd, env: process.env }); | ||
| const timer = setTimeout(() => { | ||
| if (settled) return; | ||
| settled = true; | ||
| try { child.kill("SIGKILL"); } catch {} | ||
| resolve({ |
There was a problem hiding this comment.
🧩 Analysis chain
🌐 Web query:
Node.js child_process kill detached process group descendants npx Vitest timeout
💡 Result:
To kill a detached Node.js child_process and its process group descendants (especially relevant for npx Vitest timeout scenarios where workers hang), use these methods: 1. Spawn with detached: true (non-Windows): This makes the child the leader of a new process group. const { spawn } = require('node:child_process'); const child = spawn('command', ['args'], { detached: true, stdio: 'ignore' }); // To kill child + all descendants: process.kill(-child.pid, 'SIGTERM'); // Negative PID targets process group 2. For cross-platform or non-detached: Use tree-kill npm package. npm i tree-kill const kill = require('tree-kill'); kill(child.pid); Node.js docs note: On Linux, killing parent doesn't kill grandchildren by default. Detached + process.kill(-pid) solves this for Unix. For npx Vitest timeouts/hanging (e.g., "close timed out", zombie workers on Ctrl+C): - Run with --pool=forks (uses child_process, easier to kill): npx vitest --pool=forks - Or in vite.config.ts: test: { pool: 'forks' } - Avoids worker_threads issues (e.g., undici fetch hangs); forks terminate better on timeout/Ctrl+C. - Recent Vitest versions improved fork worker termination on forceful exits. This prevents orphaned high-CPU processes after Vitest timeouts or aborts.
Citations:
- 1: https://nodejs.org/docs/latest/api/child%5Fprocess.html
- 2: https://nodejs.org/api/child%5Fprocess.html
- 3: https://stackoverflow.com/questions/63470352/kill-detached-child-process-in-node
- 4: https://medium.com/@almenon214/killing-processes-with-node-772ffdd19aad
- 5: child_process.spawn sh not killable nodejs/node#2098
- 6: https://www.npmjs.com/package/tree-kill
- 7: Timeout abort can leave process(es) running in the background vitest-dev/vitest#3077
- 8: Timeout abort can leave process(es) running in the background vitest-dev/vitest#3077
- 9: Cancelling with CTRL+c leaves zombie processes of forks workers vitest-dev/vitest#9123
🏁 Script executed:
#!/bin/bash
# Check if the file exists and examine the actual code at lines 78-83
if [ -f "src/testAdapters/vitest.ts" ]; then
echo "=== File found: src/testAdapters/vitest.ts ==="
wc -l src/testAdapters/vitest.ts
echo ""
echo "=== Lines 70-90 context ==="
sed -n '70,90p' src/testAdapters/vitest.ts
else
echo "File not found. Listing available test adapter files:"
find . -name "*.ts" -path "*/testAdapters/*" 2>/dev/null | head -20
fiRepository: TSavo/provekit
Length of output: 836
🏁 Script executed:
#!/bin/bash
# Check for any existing platform detection patterns in the file
echo "=== Searching for platform detection in vitest.ts ==="
rg "process\.platform" src/testAdapters/vitest.ts -A 2 -B 2Repository: TSavo/provekit
Length of output: 111
🏁 Script executed:
#!/bin/bash
# Check the full context of the spawn call and timeout handler
echo "=== Full context around lines 78-83 ==="
sed -n '75,95p' src/testAdapters/vitest.tsRepository: TSavo/provekit
Length of output: 757
Kill the full process tree on timeout, not just the direct npx process.
When npx spawns Vitest and Vitest spawns workers, calling child.kill("SIGKILL") only terminates the direct child. On Unix systems, worker processes become grandchildren in a separate process group and survive the timeout, continuing to run tests after the adapter returns.
Use detached: true when spawning (non-Windows) to create a process group, then target the entire group on timeout. On Windows, use taskkill /T to kill the process tree.
Proposed fix
- const child = spawn(cmd, args, { cwd, env: process.env });
+ const child = spawn(cmd, args, {
+ cwd,
+ env: process.env,
+ detached: process.platform !== "win32",
+ });
const timer = setTimeout(() => {
if (settled) return;
settled = true;
- try { child.kill("SIGKILL"); } catch {}
+ try {
+ if (child.pid && process.platform === "win32") {
+ spawn("taskkill", ["/pid", String(child.pid), "/T", "/F"]);
+ } else if (child.pid) {
+ process.kill(-child.pid, "SIGKILL");
+ } else {
+ child.kill("SIGKILL");
+ }
+ } catch {}
resolve({📝 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
| const child = spawn(cmd, args, { cwd, env: process.env }); | |
| const timer = setTimeout(() => { | |
| if (settled) return; | |
| settled = true; | |
| try { child.kill("SIGKILL"); } catch {} | |
| resolve({ | |
| const child = spawn(cmd, args, { | |
| cwd, | |
| env: process.env, | |
| detached: process.platform !== "win32", | |
| }); | |
| const timer = setTimeout(() => { | |
| if (settled) return; | |
| settled = true; | |
| try { | |
| if (child.pid && process.platform === "win32") { | |
| spawn("taskkill", ["/pid", String(child.pid), "/T", "/F"]); | |
| } else if (child.pid) { | |
| process.kill(-child.pid, "SIGKILL"); | |
| } else { | |
| child.kill("SIGKILL"); | |
| } | |
| } catch {} | |
| resolve({ |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testAdapters/vitest.ts` around lines 78 - 83, The current spawn call
(spawn(cmd, args, { cwd, env: process.env })) only kills the direct child via
child.kill("SIGKILL") so workers survive; change the spawn to set detached: true
on non-Windows platforms (preserving cwd and env) so the child runs in its own
process group, and on timeout kill the whole group using
process.kill(-child.pid, "SIGKILL") (guard for child.pid and platform). For
Windows, instead of child.kill, call taskkill /PID <pid> /T /F (using child.pid)
to terminate the full process tree. Update the timer cleanup branch around the
timer/settled logic (where child.kill("SIGKILL") is called) to perform
platform-specific full-tree termination and still resolve/reject as before.
Comment on lines
+105
to
+114
| child.on("close", (exitCode) => { | ||
| if (settled) return; | ||
| settled = true; | ||
| clearTimeout(timer); | ||
| const parsed = parse(stdout, stderr, exitCode); | ||
| resolve({ | ||
| ...parsed, | ||
| durationMs: Date.now() - start, | ||
| rawOutput: stdout.slice(0, 8192), | ||
| }); |
There was a problem hiding this comment.
Guard parser failures inside the close handler.
Line 109 calls parse from an async event callback. If it throws, the promise is not resolved into an adapter-error; the exception can escape the adapter path.
🛡️ Proposed fix
child.on("close", (exitCode) => {
if (settled) return;
settled = true;
clearTimeout(timer);
- const parsed = parse(stdout, stderr, exitCode);
+ let parsed: { kind: TestOutcomeKind; message: string };
+ try {
+ parsed = parse(stdout, stderr, exitCode);
+ } catch (e: any) {
+ parsed = {
+ kind: "adapter-error",
+ message: `could not parse test runner output: ${e?.message?.slice(0, 120) || "unknown"}`,
+ };
+ }
resolve({
...parsed,
durationMs: Date.now() - start,
rawOutput: stdout.slice(0, 8192),
});📝 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
| child.on("close", (exitCode) => { | |
| if (settled) return; | |
| settled = true; | |
| clearTimeout(timer); | |
| const parsed = parse(stdout, stderr, exitCode); | |
| resolve({ | |
| ...parsed, | |
| durationMs: Date.now() - start, | |
| rawOutput: stdout.slice(0, 8192), | |
| }); | |
| child.on("close", (exitCode) => { | |
| if (settled) return; | |
| settled = true; | |
| clearTimeout(timer); | |
| let parsed: { kind: TestOutcomeKind; message: string }; | |
| try { | |
| parsed = parse(stdout, stderr, exitCode); | |
| } catch (e: any) { | |
| parsed = { | |
| kind: "adapter-error", | |
| message: `could not parse test runner output: ${e?.message?.slice(0, 120) || "unknown"}`, | |
| }; | |
| } | |
| resolve({ | |
| ...parsed, | |
| durationMs: Date.now() - start, | |
| rawOutput: stdout.slice(0, 8192), | |
| }); |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testAdapters/vitest.ts` around lines 105 - 114, In the child.on("close")
handler, guard the call to parse(stdout, stderr, exitCode) with a try/catch so
any thrown errors don't escape; if parse throws, produce/resolve an
adapter-error result instead of letting the exception propagate. Specifically,
wrap the parse call inside a try block within the child.on("close") callback
(where settled, timer, stdout, stderr, start are in scope), and in the catch
create/resolve the promise with an adapter-error payload (or a standardized
error object expected by the adapter) and still include durationMs and rawOutput
before returning.
| import { summarizeTriangle } from "./testOracle"; | ||
| import { TestCache } from "./testCache"; | ||
| import { getAdapter, listAdapters } from "./testAdapters"; | ||
| import { mkdirSync, writeFileSync, rmSync } from "fs"; |
There was a problem hiding this comment.
Make the mtime invalidation test deterministic.
Line 110 only waits 10ms before rewriting the file. On filesystems with coarse timestamp granularity, TestCache may see the same mtime and this test can flake. Force the mtime instead of relying on wall-clock delay.
🧪 Proposed fix
-import { mkdirSync, writeFileSync, rmSync } from "fs";
+import { mkdirSync, writeFileSync, rmSync, utimesSync } from "fs";- it("invalidates on source file mtime change", async () => {
+ it("invalidates on source file mtime change", () => {
const testFile = join(tmpRoot, "b.test.ts");
const sourceFile = join(tmpRoot, "b.ts");
writeFileSync(testFile, "// test");
writeFileSync(sourceFile, "// v1");
const cache = new TestCache(tmpRoot);
cache.put(testFile, "t", sourceFile, { kind: "pass", message: "ok", durationMs: 1 });
expect(cache.get(testFile, "t", sourceFile)).not.toBeNull();
// Bump source mtime
- await new Promise((r) => setTimeout(r, 10));
writeFileSync(sourceFile, "// v2");
+ const bumped = new Date(Date.now() + 2000);
+ utimesSync(sourceFile, bumped, bumped);
expect(cache.get(testFile, "t", sourceFile)).toBeNull();
});Also applies to: 100-112
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testOracle.triangle.test.ts` at line 5, The mtime-based invalidation test
flakes because it waits 10ms for the filesystem timestamp to change; instead of
sleeping, after rewriting the file call fs.utimesSync (or fs.promises.utimes) to
explicitly advance the file mtime so TestCache observes a different timestamp.
Locate the rewrite step in src/testOracle.triangle.test.ts (the block that
writes the file and currently waits ~10ms around lines 100-112), remove the
delay and after writeFileSync call utimesSync(filePath, newAtime, newMtime) with
a newMtime (e.g., Date.now()/1000 + 1 or Date.now()/1000 + 2) to force a changed
mtime so TestCache invalidation becomes deterministic.
Comment on lines
+180
to
+181
| const cached = cache.get(testFile, reference.testName, sourceAbs); | ||
| if (cached) return { reference, outcome: cached, cached: true }; |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Inspect TestCache key construction and get/put signatures.
# Expectation: cache keys include framework/adapter identity, or runner config/package metadata is part of invalidation.
fd -a '^testCache\.ts$' . | while read -r file; do
echo "== $file =="
sed -n '1,260p' "$file"
doneRepository: TSavo/provekit
Length of output: 2522
Include framework/adapter identity in the oracle cache key.
Lines 180 and 200 cache by test file/name/source only. The TestCache.key() method (testCache.ts:29–45) hashes testFile, testMtime, testName, sourceFile, and sourceMtime, but omits framework identity. A result cached under one adapter (Vitest) is incorrectly reused when the framework changes to another (Jest/Mocha/Node) without modifying the test or source file, producing a stale oracle signal.
Also applies to: 199–200
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testOracle.ts` around lines 180 - 181, The cache lookup uses only
testFile/testName/source (cache.get(testFile, reference.testName, sourceAbs))
but TestCache.key must include the framework/adapter identity so results from
one adapter aren’t reused for another; update all cache.get and cache.set calls
(e.g., the lines using cache.get(...) at src/testOracle.ts) to pass the
framework/adapter identifier (e.g., frameworkId or adapterName) and modify
TestCache.key (testCache.ts:29–45) signature to accept and incorporate that
identifier into the hash generation so the cache key is unique per
framework/adapter.
Comment on lines
+192
to
+197
| const outcome = await adapter.runTest({ | ||
| projectRoot, | ||
| testFile, | ||
| testName: reference.testName, | ||
| timeoutMs, | ||
| }); |
There was a problem hiding this comment.
Normalize adapter exceptions into adapter-error outcomes.
Line 192 awaits adapter code directly. If an adapter throws, the checker rejects instead of returning a structured oracle result, despite adapter failures being modeled as adapter-error.
🛡️ Proposed fix
- const outcome = await adapter.runTest({
- projectRoot,
- testFile,
- testName: reference.testName,
- timeoutMs,
- });
+ let outcome: TestOutcome;
+ try {
+ outcome = await adapter.runTest({
+ projectRoot,
+ testFile,
+ testName: reference.testName,
+ timeoutMs,
+ });
+ } catch (e: any) {
+ outcome = {
+ kind: "adapter-error",
+ message: `adapter threw: ${e?.message?.slice(0, 120) || "unknown"}`,
+ durationMs: 0,
+ };
+ }📝 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
| const outcome = await adapter.runTest({ | |
| projectRoot, | |
| testFile, | |
| testName: reference.testName, | |
| timeoutMs, | |
| }); | |
| let outcome: TestOutcome; | |
| try { | |
| outcome = await adapter.runTest({ | |
| projectRoot, | |
| testFile, | |
| testName: reference.testName, | |
| timeoutMs, | |
| }); | |
| } catch (e: any) { | |
| outcome = { | |
| kind: "adapter-error", | |
| message: `adapter threw: ${e?.message?.slice(0, 120) || "unknown"}`, | |
| durationMs: 0, | |
| }; | |
| } |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testOracle.ts` around lines 192 - 197, The code awaits
adapter.runTest(...) directly so any thrown exception causes the checker to
reject instead of returning an oracle result; wrap the adapter.runTest call in a
try/catch around the await (where outcome is assigned) and on error
return/assign a structured "adapter-error" outcome object (matching the oracle
result shape your system uses) containing the error message/stack and contextual
fields (projectRoot, testFile, testName, timeoutMs) so failures from
adapter.runTest are normalized into an adapter-error outcome instead of bubbling
as exceptions.
| sourceFile: string, | ||
| opts: { maxTests?: number; timeoutMsEach?: number } = {} | ||
| ): Promise<ExecutedOracleResult[]> { | ||
| const maxTests = opts.maxTests ?? 5; |
There was a problem hiding this comment.
Align the default execution cap with the PR contract.
Line 219 defaults to 5 tests, but the PR objective says oracle execution is capped at 3 tests per contract. Callers that omit maxTests can exceed the intended runtime budget.
⏱️ Proposed fix
- const maxTests = opts.maxTests ?? 5;
+ const maxTests = opts.maxTests ?? 3;📝 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
| const maxTests = opts.maxTests ?? 5; | |
| const maxTests = opts.maxTests ?? 3; |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testOracle.ts` at line 219, The default maxTests value in
src/testOracle.ts currently allows 5 when callers omit opts.maxTests; change the
default to 3 to match the PR contract by replacing the initialization of
maxTests (const maxTests = opts.maxTests ?? 5) with a default of 3
(opts.maxTests ?? 3) in the function that defines maxTests (look for the
test/oracle entry function that declares maxTests) so callers that omit maxTests
are capped at 3 tests.
Comment on lines
+289
to
+294
| const hasAgreement = | ||
| (harnessSuggestsProblem && fails.length > 0) || | ||
| (harnessSuggestsOk && passes.length > 0 && fails.length === 0); | ||
| const hasDisagreement = | ||
| (harnessSuggestsProblem && passes.length > 0 && fails.length === 0) || | ||
| (harnessSuggestsOk && fails.length > 0); |
There was a problem hiding this comment.
Handle mixed oracle verdicts consistently.
For encoding-gap/problem harnesses, mixed pass+fail oracle results currently report agreement only because Line 293 suppresses disagreement when any failure exists. That hides passing tests that contradict the harness problem signal.
🔎 Proposed fix
+ const onlyPasses = passes.length > 0 && fails.length === 0;
+ const onlyFails = fails.length > 0 && passes.length === 0;
+
const hasAgreement =
- (harnessSuggestsProblem && fails.length > 0) ||
- (harnessSuggestsOk && passes.length > 0 && fails.length === 0);
+ (harnessSuggestsProblem && onlyFails) ||
+ (harnessSuggestsOk && onlyPasses);
const hasDisagreement =
- (harnessSuggestsProblem && passes.length > 0 && fails.length === 0) ||
+ (harnessSuggestsProblem && passes.length > 0) ||
(harnessSuggestsOk && fails.length > 0);🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/testOracle.ts` around lines 289 - 294, The current logic in
src/testOracle.ts sets hasAgreement when any failure exists for
harnessSuggestsProblem even if there are passing tests, which hides mixed
verdicts; update the definitions of hasAgreement and hasDisagreement (the
variables named hasAgreement, hasDisagreement) so that agreement requires
unanimous oracle results that match the harness suggestion (for
harnessSuggestsProblem: fails.length > 0 and passes.length === 0; for
harnessSuggestsOk: passes.length > 0 and fails.length === 0), and disagreement
is true whenever any oracle result contradicts the harness suggestion (for
harnessSuggestsProblem: passes.length > 0; for harnessSuggestsOk: fails.length >
0), using the existing symbols harnessSuggestsProblem, harnessSuggestsOk,
passes, and fails to locate and change the logic.
1. Vitest -t regex unescaped (Major)
Vitest 4's -t/--testNamePattern is a regex. Now escapes testName
the same way jest and mocha adapters already do, so a testName
containing regex metacharacters no longer mis-filters.
2. Process-group kill not reaching descendants (Major)
runCommand spawned without detached, so killing the npx shim left
the actual vitest/jest/mocha grandchild running on timeout. Now
spawns with detached: true on POSIX and kills the negative PID to
reach the whole process group. Windows falls back to the single-
process kill (no process groups on win32 by default).
3. parse callback could throw out of runCommand (Major)
The close-handler called parse() directly; an exception escaped the
resolve path. Wrapped in try/catch, converted to adapter-error.
4. First-brace-greedy JSON extraction (Minor)
mocha (and vitest, jest) matched /\{[\s\S]*\}/, which takes everything
from first-brace to last-brace. If the runner logs any object before
the reporter's JSON output, the match includes non-report noise.
New extractLastJsonBlock walks stdout from the last "}" backwards,
finds the matching open brace with balanced depth, and returns that
block. Robust to leading log noise.
5. Node --test reporter assumption (Major)
Node 23+ changed the default reporter from TAP to spec. Explicitly
requests --test-reporter=tap. Also now uses --test-name-pattern
(Node 18.17+) with regex-escaped testName for server-side filtering;
the post-hoc TAP-line filter still runs as a fallback for older Node
versions that ignore the flag.
6. TestCache path-resolution bug (Major)
statSync(testFile) and statSync(sourceFile) used the process cwd
when paths were project-relative, producing mtime=0 and making the
cache invalidation unreliable. TestCache now takes projectRoot in
the constructor and resolves all paths against it before statting.
7. TestCache ignored framework identity (Major)
Cache keys didn't include framework/adapter identity, so if the
same test file+name+source was queried under different frameworks,
the first cached outcome would be reused regardless. get/put now
take framework as the first argument; keys hash it alongside mtimes.
8. runTestsForReferences maxTests default mismatched the PR cap (Major)
Default was 5 but the PR description advertised a 3-test cap.
Aligned the default to 3.
9. Adapter-error not normalized at oracle boundary (Major)
runTest awaited adapter.runTest directly. If an adapter's documented
never-throw contract were violated, the rejected promise escaped the
checker instead of producing an adapter-error outcome. Wrapped in
try/catch with explicit normalization and a "contract violation"
note in the message so the source is clear.
10. Mixed-verdict oracle results mis-classified as agreement (Major)
For problem-signalling harnesses, any presence of failing tests
produced hasAgreement=true regardless of how many tests were also
passing. Now requires uniform oracle direction: hasAgreement only
when passes>0 & fails==0 (with ok-harness) or fails>0 & passes==0
(with problem-harness). Mixed outcomes return neither agreement
nor disagreement — the note still shows the counts so operators
see the ambiguity.
11. Flaky mtime-invalidation test (Minor)
Relied on a 10ms sleep to bump mtime, which is below the
granularity of some filesystems and causes test flakes. Now uses
utimesSync to force mtime forward by 10 seconds, which is
deterministic regardless of filesystem mtime resolution.
Additionally added a "different frameworks are cached independently"
test covering the #7 fix.
87 tests pass (up from 85).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
6 tasks
TSavo
added a commit
that referenced
this pull request
Apr 24, 2026
Add LLMProvider.agent() as an optional method to both LLMProvider interfaces (llm/Provider.ts and fix/types.ts). ClaudeAgentProvider implements it via the claude-agent-sdk query() with cwd/allowedTools/ maxTurns routing. StubLLMProvider gets an optional agentResponses constructor arg that, when supplied, assigns the agent() field. New captureChange.ts reconstructs a CodePatch from git diff after the agent completes, excluding .neurallog/ overlay internals. The C3 stage (generateFixCandidate.ts) dispatches to the agent path when llm.agent is defined, falling back to the existing JSON-patch path for providers without agent() support. One retry with oracle-#2 feedback is included. 18/18 tests pass (15 existing + 3 new captureChange + 2 new candidateGen). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
When the principle proxy still matches after a guard-based fix (division expression still present), oracle #2 now extracts dominating IfStatement guards over the binding's use-site and conjoins them as SMT assertions. If Z3 returns unsat, the guard makes the violation unreachable — fix passes. Handles literal-eq, !=, !==, >, <, >=, <= comparisons; falls back gracefully to the proxy verdict for unsupported cases. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
…erification Drives integration-gap rate from 75% to 0% on the 12-scenario corpus. Part 1, C1.5 fidelity stub coverage. Add commonStubs.ts with a shared traceability stub plus three per-binding adversarial-fixture builders (intZeroFixtureStub, boolFixtureStub, intEqualityFixtureStub). The runner appends shared stubs after each scenario's own responses so scenarios can override; cross-LLM agreement passes naturally because the C1.5 adversary prompt re-uses the C1 "formal verification expert" prefix and matches the scenario's own invariant stub. Each curated scenario now ships a citations field (required by traceability) and a per-binding fixture stub. Ternary scenarios switched from String to Int sort so the fixture pre-validator can constrain bindings. null-001 source_expr changed from "user === null" to "user !== null" so oracle #2's post-fix substring search correctly classifies the patched file as bug-removed (null-002 worked by accident with the same pattern; null-001 had the polarity flipped). Part 2, SemGrep importer. import-semgrep.ts walks a local clone of github.com/semgrep/semgrep-rules, picks TS/JS rules with a sibling fixture file containing at least one ruleid annotation, and emits a CorpusScenario per rule into scenarios/imported/. Bug-class is inferred from the rule id (divide / null / ternary), unmatched rules become bugClass:"novel" with expected.outcome:"out_of_scope". index.ts now appends scenarios/imported/ via runtime require glob in addition to the curated explicit imports. scripts/import-semgrep.ts is a one-shot CLI; no clone is fetched from the agent. Tried ~/semgrep-rules, ~/src/semgrep-rules, ~/Code/semgrep-rules; no clone present so 0 imports run. Part 3, fast-check verification. All 8 properties pass; properties make non-trivial assertions (audit-trail consistency, stage-completion implied by outcome, chronological timestamps, failedStage-failureReason pairing). numRuns:3 with corpus of 12 is intentional given each run spins up a scratch project plus full fix loop. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
…avioral gate Promote classifyInvariantKind to shared src/fix/invariantKind.ts. Oracle #2 (runOracleTwo) now routes by kind: keep bug_site_removed as the kind-agnostic structural gate, then for ABSTRACT invariants whose source expressions still appear post-fix, return new "deferred_behavioral" verdict instead of falling into Z3 (which would just re-confirm the same SAT formula). For abstract invariants, Z3 has no formula linking source-code sanitization to the abstract Bool predicate; oracle #9 (mutation-verified regression test in C5) IS the proof — test must fail on original code AND pass on fixed code. verifyCandidate treats deferred_behavioral as pass-forward; C5 throws on either failure, so the proof actually lands. Concrete (Int/Real) path unchanged — guard-augmented Z3 + plain Z3 fallback. Test #18 locks in the existing concrete-path behavior; #16 + #17 cover the new abstract paths (defer when site preserved, bug_site_removed when not). Tests: 728 pass (+3 new). Pre-existing apply.test.ts test 7 flake when running in parallel under the full suite is unrelated (passes in isolation).
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
The surface SMT shape lies when the LLM encodes Bool taint as Int (writes '(declare-const input Int)' to express a shell-metacharacter taint predicate). C1.5's fixtures-based demotion (concrete → abstract when 0/N negatives classified) catches this, but the decision was not propagated. Add InvariantClaim.effectiveKind. formulateInvariant stamps the post-demotion kind from runInvariantFidelity onto the returned claim. runOracleTwo prefers effectiveKind over re-running classifyInvariantKind on the lying SMT body. Test #17b locks in the actual real-LLM regression: Int-shaped formal expression with effectiveKind='abstract' must yield deferred_behavioral. This was the gap that caused the v5 dogfood to fail at oracle #2 even with the routing logic in place — kind=concrete beat the abstract path because the LLM wrote Int.
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
setupOverlayForTest now returns boolean instead of throwing. When the main repo has no node_modules (bare fixtures like /tmp/shell-injection-dogfood/), runTestInOverlay emits the existing no-runner sentinel so oracle #9 is cleanly skipped instead of crashing the loop at C5. Surfaced from real-LLM shell-injection dogfood: with d35df4d the loop now gets past oracle #2 (adaptive abstract path) but C5 threw on missing node_modules in the bare fixture, blocking D1/D2. Adds 3 unit tests covering the three reachable states: pre-existing node_modules, bare main repo, main repo with node_modules to symlink. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
… at center)
Architectural correction: the principle library IS the bug-recognition
mechanism, mechanically. Every principle is a compiled SAST query.
Recognition is a database query that runs in microseconds, not an LLM
judgment. Today's pipeline put the LLM in the recognition path; this
moves recognition upstream to a new stage B3, between Locate and
Classify, and mechanizes ALL downstream stages when it hits.
Pipeline shape:
intake -> locate -> B3:RECOGNIZE -> + HIT -> C1m -> C3m -> C5m -> C6m -> D1 -> D2 (zero LLM, seconds)
+ MISS -> C1 -> C3 -> C5 -> C6 -> D1 -> D2 (LLM-driven, minutes)
When B3 fires, the orchestrator routes C1/C3/C5/C6 through their
mechanical-mode arms. Each stage instantiates stored templates from
the matched LibraryPrinciple instead of calling the LLM:
- C1m: smtTemplate substitution + oracle #1 verification
- C3m: fixTemplate AST instantiation + applyPatchToOverlay + oracle #2
- C5m: testTemplate instantiation + oracle #9 mutation verification
- C6m: append provenance to existing principle, no harvest
LibraryPrinciple schema extended with optional fixTemplate +
testTemplate fields. division-by-zero principle backfilled with both.
Migration: provenance changed from single-object to array form to
support multi-source provenance (seed + customer-fix + bugsjs-import).
Test isolation: PROVEKIT_DISABLE_RECOGNIZE=1 set globally in
vitest.config.ts. This prevents test fixtures from triggering
mechanical mode and polluting the canonical principle JSONs with
provenance entries pointing at /var/folders/T/* tmpdir paths. The
new recognize.test.ts opts back in by deleting the env var per-suite.
Test count: 739 passing, 0 logical failures. The 4 remaining
suite-level failures (cli.fix gap_report, two overlay lifecycle, one
recognize wall-time) are all parallel-execution timing flakes that
pass solo.
Wall time targets:
- Recognized path: ~4-5 seconds (verified on division-by-zero fixture)
- Novel path: ~6 minutes (post-Leak 6 tier calibration)
Unblocks #97 (BugsJS harvest as strict subset). Once a principle has
fixTemplate + testTemplate populated, BugsJS bootstrap reduces to
identifying clusters: first-of-class harvests via C6, cluster members
recognize for free.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
…r SAST Two findings from Bug-1 (Express duplicate-methods-in-Allow-header) hand-staging surfaced gaps: 1. SAST indexer in cli.ts:171 only accepted .ts/.tsx, blocking any harvest from JavaScript-only BugsJS projects (Express, Mocha, ESLint, Karma, etc.). ts-morph parses .js/.jsx fine; widening the extension whitelist unblocks JS bootstrap. 2. The invariant kind classifier missed cardinality phrasing that real-LLM output naturally produced for Bug-1: 'at most once', 'appears more than once', 'no more than five'. The classifier defaulted to concrete because Int bindings were present and no set/order keywords matched, leading to oracle #2 trying SMT-prove the dedup (which Z3 cannot reason about for array indexOf ops). Expanded ABSTRACT_PROSE_KEYWORDS with the full cardinality vocabulary (at most/at least/more than/exactly + once/one/twice/two) and added a CARDINALITY_RE catch-all for occurrence-count phrasing ('occurs N times', 'fires twice', etc.). 16+7 new test cases anchored to real-world phrasings from past dogfoods and Bug-1's actual prose. The deeper architectural fix (C1 emits 'kind' field directly so the post-hoc classifier becomes a validator, not a guesser) is queued as task #99. Test count: 57 in invariantKind suite + invariantFidelity, all passing. Bug-1 v3 ran end-to-end after this landed: B3, C1, C1.5, C2, C3, C4, C5, C6, D1, D2 all completed; bundle assembled with all 4 coherence flags green; Claude's filter-based fix is functionally equivalent to Express's appendMethods production fix. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Apr 25, 2026
#1 (uncovered by Bug-1 v6) — C1 binding validator was too narrow. The validator only matched (declare-const NAME ...) and rejected any binding whose smt_constant referred to a (declare-fun NAME ...) or (declare-sort NAME). Set-uniqueness invariants commonly use uninterpreted functions to express things like "the value at index i" without inventing concrete representations; rejecting them forced the LLM to over-flatten the SMT shape. Validator regex now accepts declare-const, declare-fun, and declare-sort. The set-uniqueness canonical example in the C1 prompt also got rewritten to lead with the (distinct ...) form, which doesn't need uninterpreted functions. The paired-equality alternative is shown second. The previous example used (header_method k1) without declaring header_method, which was the exact trap Bug-1 v6 hit. #2 (test flake) — capabilityExecutor.test had the same shape as the apply.test flake fixed in 76d53d0: it inspected the shared node_modules/.cache directory for provekit-extractor-* dirs created during the test, but other concurrent test runs polluted the count. executeExtractorSpec now accepts an optional cacheDirOverride parameter; production callers omit it and use the default. Tests pass a per-test mkdtempSync directory and inspect ONLY that for cleanup verification. Test count: 779 passing across 81 test files. Two consecutive full-suite runs verified. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
5 tasks
TSavo
added a commit
that referenced
this pull request
May 4, 2026
…closes #211) Side A substrate-conformance work for the swift kit. Two related changes, both required for issue #211 acceptance: 1. SwiftSyntax-based lifter (Path B): replaces regex-v0 in `SwiftLifter.swift` with a real AST walker using Apple's official swift-syntax 600.x library. The wire shape (declarations, callEdges, warnings) is byte-preserved; LSPTests' 11 integration tests pass unmodified. Adds InitializerDeclSyntax handling (regex-v0 never matched `init`); the addition is additive and downstream-safe. 2. swift-self-contracts lift surface + RPC mode (Path A): mirrors the PR #220 daemon-lifecycle pattern (ts Side A) and PR #217 (cpp Side A wiring). The swift mint binary now speaks the lift-plugin protocol over NDJSON-on-stdio: initialize -> lift (proof-envelope shape) -> shutdown, with stdin-EOF graceful exit per architect rule #3. * `MintSwiftSelfContracts/main.swift`: thin entry-point that branches on `--rpc` argv. Slab moved to `Slab.swift`; RPC handlers in `RPC.swift`. SPM compiles all three into one module. * `Slab.swift`: pure function `swiftSelfContracts() -> [Declaration]` authoring all 11 lift-plugin-protocol contracts (C1-C8, 11 facets), callable from both human and RPC entry points. * `RPC.swift`: NDJSON loop; `handleLift` walks the slab, computes content-meaningful CIDs, emits a proof-envelope. * `.provekit/lift/swift-self-contracts/manifest.toml`: declares surface + capabilities + binary path. Mirrors the ts/go/cpp peers. * `cmd_mint.rs`: KIT_TABLE swift entry routes to swift-self-contracts. Cross-kit IR byte-equality (per dispatch directive): - contractSetCid: byte-equivalent. Computed via the canonical formula blake3_512(JCS(sorted([contract_cid(c) for c in slab]))) where each contract_cid = blake3_512(JCS({name, outBinding, pre?, post?, inv?})), matching `provekit-claim-envelope::contract_cid` and `provekit-claim-envelope::compute_contract_set_cid` exactly. - proof-envelope bytes: NOT byte-equivalent. The swift kit emits a JCS-JSON catalog with self-identifying `kind: "swift-self-contracts-catalog-phase3-pending"` rather than the cross-kit CBOR-signed catalog. This is consistent with the existing Phase 3 deferral noted in `MintSwiftSelfContracts/main.swift:208-211` (now `main.swift:46-48`); a follow-up PR can land the full CBOR + Ed25519 envelope (mirroring PR #221 for python). The dispatcher only requires `kind:"proof-envelope"`, non-empty `filename_cid`, and decodable `bytes_base64` — all satisfied. The filename_cid changes whenever the slab changes, satisfying acceptance gate #2. Acceptance gate #4 ("provekit prove --kit=swift exits 0"): provekit prove doesn't accept --kit (see `provekit-cli/src/main.rs:119`); the intent is read as "mint pipeline succeeds end-to-end on macOS." `make mint-swift` runs cleanly and `verify-self-contracts` returns OK against the new attestation, demonstrating the full pipeline. - [x] `swift run conformance` (10/10 PASS) - [x] `swift run test-swift-lsp` (11/11 PASS — wire shape preserved) - [x] `swift run mint-swift-self-contracts` human mode (CID matches) - [x] `mint-swift-self-contracts --rpc` direct subprocess (initialize/lift/shutdown trip) - [x] `cargo test cmd_mint` (9/9 unit tests pass) - [x] `cargo test mint_kit_integration swift_kit_pins_expected_contract_set_cid` (PASS) - [x] `make mint-swift` end-to-end: contractSetCid pinned, attestation OK - [x] Three independent paths agree on contractSetCid blake3-512:272543ef... - swift contractSetCid: blake3-512:272543efe7c47b911659e1fc6a7368431b6eaa6010d2560a5d3e6717fcd470b50b24b607b481272941764b731d890d6973ab88e6000bde96fd306163a5742c56 Pre-existing test failures unrelated to #211: rust/cpp self-contracts binaries are not built in this worktree, causing `rust_kit_contract_set_cid_is_pinned_to_self_contracts_canonical` and `cpp_kit_contract_set_cid_is_pinned_to_self_contracts_canonical` to fall back to empty-set CIDs. Not a regression introduced by #211. Closes #211. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 5, 2026
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>
TSavo
added a commit
that referenced
this pull request
May 5, 2026
…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>
This was referenced May 6, 2026
Merged
3 tasks
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…#596/#598/#599/#600 Per-kit changes: - rust/provekit-cli: extend KNOWN_SURFACES anchor test to assert ruby-source, csharp-source, swift-source, zig-source are all registered (were in the array, not in the test) - Makefile: wire test-ruby and test-php into test-all so the new lift kits run under ci (boy-scout -- flagged in #598 review) - typescript-language-signature/mint.sh: replace find with explicit enumeration to match c11/rust pattern and remove portability footgun (PR #595 nit #3) - ruby/ruby_source.rb: add instance_variable_get, instance_variable_set, const_get, const_set to METAPROGRAMMING_CALLS (PR #598 nit #4) - php/PhpSourceCompiler.php: simplify isUnit() to remove precedence-reliant double-condition (PR #600 nit #2) Already swept on origin/main (codex/lift-kit-nits-cleanup, empty cherry-picks confirmed): - effect sort-key alignment: 5:unresolved_call -> 5:unresolved: (ruby + swift) - csharp-source backfill in KNOWN_SURFACES - swift: emit Refusal for unparseable function signatures + ThrowStmt API fix Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…#596/#598/#599/#600 Per-kit changes: - rust/provekit-cli: extend KNOWN_SURFACES anchor test to assert ruby-source, csharp-source, swift-source, zig-source are all registered (were in the array, not in the test) - Makefile: wire test-ruby and test-php into test-all so the new lift kits run under ci (boy-scout -- flagged in #598 review) - typescript-language-signature/mint.sh: replace find with explicit enumeration to match c11/rust pattern and remove portability footgun (PR #595 nit #3) - ruby/ruby_source.rb: add instance_variable_get, instance_variable_set, const_get, const_set to METAPROGRAMMING_CALLS (PR #598 nit #4) - php/PhpSourceCompiler.php: simplify isUnit() to remove precedence-reliant double-condition (PR #600 nit #2) Already swept on origin/main (codex/lift-kit-nits-cleanup, empty cherry-picks confirmed): - effect sort-key alignment: 5:unresolved_call -> 5:unresolved: (ruby + swift) - csharp-source backfill in KNOWN_SURFACES - swift: emit Refusal for unparseable function signatures + ThrowStmt API fix Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 12, 2026
…599/#600 (#632) * chore(lift-kits): sweep accumulated MERGE-WITH-NITS nits from PRs #595/#596/#598/#599/#600 Per-kit changes: - rust/provekit-cli: extend KNOWN_SURFACES anchor test to assert ruby-source, csharp-source, swift-source, zig-source are all registered (were in the array, not in the test) - Makefile: wire test-ruby and test-php into test-all so the new lift kits run under ci (boy-scout -- flagged in #598 review) - typescript-language-signature/mint.sh: replace find with explicit enumeration to match c11/rust pattern and remove portability footgun (PR #595 nit #3) - ruby/ruby_source.rb: add instance_variable_get, instance_variable_set, const_get, const_set to METAPROGRAMMING_CALLS (PR #598 nit #4) - php/PhpSourceCompiler.php: simplify isUnit() to remove precedence-reliant double-condition (PR #600 nit #2) Already swept on origin/main (codex/lift-kit-nits-cleanup, empty cherry-picks confirmed): - effect sort-key alignment: 5:unresolved_call -> 5:unresolved: (ruby + swift) - csharp-source backfill in KNOWN_SURFACES - swift: emit Refusal for unparseable function signatures + ThrowStmt API fix Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix(ruby-language-signature): regen op_source-unit.spec.json with notes field The generator `generate_assets.py` was updated to emit a `notes` field on the `source-unit` op spec but the committed file was never regenerated. CI gate at Makefile:606 (`generate_assets.py --check`) caught the staleness. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * ci: add composer to conformance job apt block (fixes test-php exit 127) test-php runs `composer install && composer test`; the conformance job installed php-cli but never composer, so the command was not found. Adds the `composer` Ubuntu apt package to the shared system-deps step so make test-all (and make ci) can reach it. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This was referenced May 12, 2026
TSavo
added a commit
that referenced
this pull request
May 13, 2026
…838) Step #2 of the substrate-types wiring sequence. provekit prove now persists content-addressed ProofRunMemento + StageReceipt artifacts for each verifier run under .provekit/runs. Per stage: captures input_cids (sorted ascending), output_cids (sorted), refusal_cids (sorted), diagnostics (preserve order), started_at/finished_at ISO-8601 timestamps, verdict in {ok, warned, refused, skipped}, stage_name, kind="stage-receipt", schemaVersion="1". header.cid via StageReceipt::recompute_header_cid(). Per run: aggregates stage_receipt_cids in execution order (preserve order in CID input per spec §2.1), input_artifact_cids sorted, output_artifact_cids sorted (set semantics), proof_envelope_cid + link_bundle_cid + plugin_registry_cid + verifier_pipeline_cid (deterministic placeholder blake3_512(JCS(stage_vocabulary)) until VerifierPipelineMemento #799 follow-up lands), verdict in {admissible, refused, partial}. Integration test: prove_run_emits_durable_content_addressed_run_and_stage_receipts asserts the .proof bundle contains a ProofRunMemento + stage receipts, stage count matches VERIFIER_STAGE_VOCABULARY, receipt CIDs recompute, JCS round-trips, run CID recomputes, input artifact CIDs recorded, and the bundle reloads cleanly through load_all_proofs. cargo test -p provekit-verifier -p provekit-ir-types -p libprovekit: 427 passed, 0 failed. Note: cargo check -p provekit-cli currently blocked by a pre-existing provekit-walk/src/chain.rs Result vs Option mismatch — that's PR #837 (step #1, currently open) which adapts the CCP caller in provekit-walk. Co-authored-by: T Savo <agentwopr@gmail.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
pushed a commit
that referenced
this pull request
May 13, 2026
…pperMemento, validate_against, ParametricRealizationMemento Blocker #1: Mint RealizationPlanMemento after each kit dispatch in realize_function / apply_canonical_rewrite. Blocker #2: Call plan.validate_against(&realization) after construction; propagate RealizationPlanError. Blocker #3: Build synthetic ParametricRealizationMemento inline (one slot per param) via mint_realization_artifacts; catalog lookup path acknowledged as future enhancement per cmd_bind.rs gap comment. Blocker #4: Mint ObservationWrapperMemento when mode in {witness, monitor, dispatcher} and kit returns observation_wrapper_emission_record; call wrapper.validate before persisting; set plan.observation_wrapper_cid. Nit: used_sugars subset check in invoke_realize returns ext:unauthorized-sugar error when kit returns a CID not in the cited set. Add observation_wrapper_emission_record to RealizedSource (both kit_dispatch and cmd_transport layers) extracted from kit JSON response. Extend EngineResult with realization_plan_mementos and observation_wrapper_mementos; write to .provekit/bindings/ realization-plans/ and observation-wrappers/. Add three unit tests in cmd_transport for mint_realization_artifacts asserting: plan IS minted, validate_against passes, and wrapper IS minted for mode=witness. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 13, 2026
* Route contract sugar through realize kits * Add four substrate-side mints: RealizationPlanMemento, ObservationWrapperMemento, validate_against, ParametricRealizationMemento Blocker #1: Mint RealizationPlanMemento after each kit dispatch in realize_function / apply_canonical_rewrite. Blocker #2: Call plan.validate_against(&realization) after construction; propagate RealizationPlanError. Blocker #3: Build synthetic ParametricRealizationMemento inline (one slot per param) via mint_realization_artifacts; catalog lookup path acknowledged as future enhancement per cmd_bind.rs gap comment. Blocker #4: Mint ObservationWrapperMemento when mode in {witness, monitor, dispatcher} and kit returns observation_wrapper_emission_record; call wrapper.validate before persisting; set plan.observation_wrapper_cid. Nit: used_sugars subset check in invoke_realize returns ext:unauthorized-sugar error when kit returns a CID not in the cited set. Add observation_wrapper_emission_record to RealizedSource (both kit_dispatch and cmd_transport layers) extracted from kit JSON response. Extend EngineResult with realization_plan_mementos and observation_wrapper_mementos; write to .provekit/bindings/ realization-plans/ and observation-wrappers/. Add three unit tests in cmd_transport for mint_realization_artifacts asserting: plan IS minted, validate_against passes, and wrapper IS minted for mode=witness. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Code <agentwopr@gmail.com> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This was referenced May 14, 2026
TSavo
added a commit
that referenced
this pull request
May 21, 2026
…twise + Field + symbol-leaf let
Final closure of the same-language realize regression introduced when
source_text left the substrate channel. The rust kit now consumes its
own structural ProofIR end-to-end: 9 exact + 0 lossy + 0 refused on
libprovekit-rpc-cross-platform. Substrate-canonical channel + structural
ProofIR + substrate-honest realize round-trip — all three hold.
Closes the three engineering gaps surfacing from yesterday's source_text
removal:
1. walk_rpc: local-let target is a kind:"symbol" leaf carrying the
binding name, not non_operation_shape {} relying on operand_bindings
position-threading (fragile for nested lets in loop/conditional bodies).
`let n = c as u32;` now lifts as concept:assign(symbol:n, cast(...)).
2. walk_rpc: Expr::Field handler — `receiver.field` (named or tuple-index)
lifts as concept:field(receiver_shape, field_symbol_leaf). Closes the
gap on closure bodies like `|a, b| a.0.cmp(b.0)` where field access
inside the closure body fell through to non_operation_shape.
3. realize-rust-core: operation_expression handles concept:bitand /
bitor / bitxor / shl / shr. Closes `(n >> 4) & 0xF` and similar
bitwise expressions in the jcs encode_string body.
4. realize-rust-core: concept:field lowering — `receiver.field`. Pairs
with #2.
menagerie/concept-shapes/catalog/algorithms/concept:field.*.json:
- New substrate-canonical primitive operator (was missing).
Registered in catalog/index.json.
4 rust shims re-minted with the structural Field + symbol-leaf-let lifts.
End-to-end invariants:
- Cross-language materialize (rust → java): 9 site(s), 9 resolve + 0
ambiguous + 0 refused.
- Cycle invariance (rust ↔ java concept-hub identity): 9/9 preserved.
- Same-language materialize (rust → rust): **9 exact + 0 lossy + 0 refused.**
- Zero source_text leaves in any shim term_shape.
- Zero kit-internal source strings in the substrate channel.
The substrate carries identity. Each kit consumes the structural ProofIR
via its own catalog and emits idiomatic target syntax. Source code is now
a projection of the substrate-canonical proof envelope.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 22, 2026
Closes 16 findings from Codex + CodeRabbit reviews, plus a pre-existing
body-template header.cid bug surfaced during verification.
P1 / Major (correctness):
1. Out-dir file collision (Codex P1, CodeRabbit Major):
cmd_materialize.rs — out_path was built from file_stem() only, silently
overwriting same-basename files in different dirs (src/lib.rs vs
tests/lib.rs). Now preserves source-relative path under --out-dir
and creates intermediate directories.
2. Body templates not keyed by library:
SugarRealizer.java + RpcServer.java + lower_plugin.rs — body-template
lookup matched only (concept, mode, arity), making selection load-
order-dependent when two libraries shipped templates for the same
concept. Added explicit target_library_tag to RealizeRequest, plumbed
from kit_dispatch via the resolved manifest. Java realize threads
it via ThreadLocal; BodyTemplateEntry now carries targetLibraryTag;
matcher skips entries whose tag doesn't match the dispatcher.
3. Refusal guard bypass (substrate-honesty self-violation):
SugarRealizer.java + RpcServer.java + JsonUtil.java — legacy emitStub
forwarded List.of() / "" to the new overload, making zero-param cross-
lang calls indistinguishable from legacy. Replaced empties-check with
explicit isCrossLang flag; RpcServer detects via JsonUtil.hasField()
on the RPC params object (field-present = cross-lang signal).
4. Mojibake in JCS Java template:
`�` (UTF-8-as-Latin-1 em-dash corruption) emitted into
realized java source verbatim. Replaced with comma (per project style:
no em-dashes).
5. RFC 8785 number canonicalization (substrate-honesty self-violation):
Both rust and java JCS shims claimed `loss = []` while documenting in
the body that JsonNode.asText() / Number::to_string() are NOT ECMA-262
§7.1.12.1 compliant (RFC 8785 §3.2.2.3 requires it). Declared loss as
`rfc8785-number-serialization-non-ecma262` on encode_jcs + encode_value
in both rust + java shim sources AND in the three body-template JSONs.
6. Java FQN handling:
JavaBindLifter.javaTypeToConceptHubSortCid — was only stripping
`java.lang.` / `java.util.` prefixes. javac TypeMirror.toString()
returns FQNs for declared types (com.fasterxml.jackson...). Now
reduces to simple class name via last-dot.
7. Ref<T> filename (Windows-incompatible):
menagerie/concept-shapes/catalog/sorts/Ref<T>.<cid>.json — `<>` are
reserved on NTFS, repo unbuildable on Windows. Renamed to
`Ref_of_T.<cid>.json`. Updated mint_concept_ref_and_json.py to
sanitize filenames at mint time.
8. Java ForLoopTree multi-init/update lost:
JavaBindLifter — `for (i=0, j=0; ...; i++, j++)` only kept index 0.
Now wraps multi-clause lists as concept:seq so all side effects
survive the lift.
9. Java try-lift dropped finally + catch type/binding:
JavaBindLifter — concept:try only carried [body, seq(catch-bodies)].
Catch type/binding-name unrecoverable, finally entirely dropped.
Minted concept:catch-arm + concept:finally-arm. concept:try now
carries [body, catch-arm1(type, binding, body), ..., finally-arm?(body)].
10. Java MethodInvocation shape doesn't match rust (cycle invariance):
JavaBindLifter — `obj.method(x)` was emitted as `call(method:"obj.method", x)`,
folding receiver into callee leaf. Rust emits `call(receiver, method:"method", x)`.
Java now matches: receiver as args[0], method-leaf as args[1], call
args from index 2. Restores cross-language clustering for instance methods.
11. operand_bindings threading through structural control flow:
walk_rpc.rs::bindings_of_expr — If/While/ForLoop/Loop/Match/Cast/
Index/Field now thread bindings through the operator's argument
layout matching shape_of_expr. References to outer-scope symbols
inside loop bodies / conditional branches / match arms now appear
in operand_bindings at the expected positions.
12. Free Expr::Path symbol-leaf dead-code fix:
walk_rpc.rs::bindings_of_expr — operand_symbol() emitted a binding
for EVERY bare path, including free identifiers (None, Some, etc.).
Leaf resolution checks operand_bindings BEFORE kind:"symbol", so the
structural symbol-leaf fallback never fired. Now operand_symbol-
derived bindings are only emitted for identifiers in ctx.vars
(scoped names); free identifiers fall through to the leaf.
Minor:
13. "body bodies" typo in EMIT log (CodeRabbit Minor).
14. bcprov-jdk18on 1.78.1 → 1.81.1 (GHSA-c3fc-8qff-9hwx, GHSA-p93r-85wp-75v3).
15. mint_while_foreach_try.py wrote to catalog/abstractions/; checked-in
files live in catalog/algorithms/. Rerunning wouldn't reproduce.
Now writes to ALGORITHMS_DIR with filesystem-safe filename.
16. mint_unit_ref_json_morphisms.py duplicate check ignored source sort.
A second realization for the same concept (e.g. java:JsonNode vs
java:JsonElement) got silently skipped. Now keys on (lang, lang_sort,
concept_sort).
Pre-existing body-template header.cid bug (surfaced by verification):
cmd_mint.rs::project_body_templates_for_sugar_bindings never wrote
header.cid even though cmd_bind_migrate required it. Added computation
of header.cid as blake3-512 of JCS-canonical content. Backfilled into
all 14 existing body-template files. Also updated cmd_mint to write
target_library_tag per entry (matches what body_template_normalization
expects and what reviewer concern #2 wired up the reading side for).
Workspace verification:
- cargo test --workspace: 760 tests pass, 3 pre-existing fixture failures
in cross_platform_point_query_receipt_test (fixture_4/5/6) which were
ALREADY failing on the PR's pre-session starting commit 0af7430
(verified by checking that arity-2 sql-query body-template variant
has never existed — entries cover only arities 1 and 3).
- Same-language materialize (rust → rust): 9 exact + 0 lossy + 0 refused.
- Cross-language materialize (rust → java): 9 site(s), 9 resolve + 0
ambiguous + 0 refused.
- Cycle invariance (rust ↔ java concept-hub identity): 9/9 preserved.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 22, 2026
…es (#1365) * feat(materialize): cross-language --out-dir emits target-language files Extends cross-language discovery mode (commit 4ac270b6b) with actual target-language file emission. When --out-dir is passed alongside --source-lang and --target, RESOLVE'd boundaries are written into composite target-language files: one per source file, with imports (from each used library's realize-manifest scope_bringings) prepended and each boundary's emitted body concatenated. The substrate-honest invariant holds throughout: cmd_materialize does NO target-syntax translation. It routes concept-hub-typed carrier payloads to the target kit's realize binary (which owns its own concept-hub → kit-internal → target-syntax knowledge) and writes the realize binary's returned source verbatim. provekit-cli/src/cmd_materialize.rs: - run_cross_language_discovery accepts an optional out_dir: Option<&Path>. - EmittedFile struct accumulates per-source-file output: - bodies: Vec<String> of realize-binary responses for each RESOLVE'd boundary in this file. - imports: BTreeSet<String> dedup'd across all libraries used. - target_lang_file_extension: heuristic file-extension map (rs/py/ts/ java/c/cs/go/php/rb/zig). The kit could declare its extension in its manifest in a follow-up substrate-mint. - After the discovery loop, writes each EmittedFile to <out-dir>/<source-stem>.<ext> with imports block followed by bodies separated by blank lines. End-to-end verified: $ provekit materialize --source-lang rust --target python \ --library sqlite3 \ --source-dir examples/cross-lang-sql-family-demo/src \ --project /Users/tsavo/provekit \ --out-dir /tmp/xlang-out RESOLVE concept:sql-connection-open → python manifest `sqlite3` target body preview: def run_open(path): return sqlite3.connect(path) EMIT wrote /tmp/xlang-out/lib.py (1 body bodies, 0 imports) materialize cross-language emission: 1 file(s) written to /tmp/xlang-out Output file (/tmp/xlang-out/lib.py): def run_open(path): return sqlite3.connect(path) Same-language materialize regression: 9 exact + 0 lossy + 0 refused (no behavior change for the rust → rust path). Stack state after this commit: - Source kit lifts to concept-hub CIDs at kit/substrate boundary. - ProofIR carries concept-hub identities only (kit-internal sorts never visible to substrate). - cmd_materialize routes concept-hub-typed payloads kit → kit. - Target kit emits target-language source (its own concept-hub → target-syntax internally). - cmd_materialize writes the bytes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(java-stdio-shim): first L0 sister shim — concept:family:stdio-stream in java Mints provekit-shim-stdio-java as the java sister to provekit-shim-stdio-rust under concept:family:stdio-stream. Three @ProveKitSugar methods wrap System.in / System.out / System.err: - concept:stdio-read-line → BufferedReader(InputStreamReader(System.in)).readLine() - concept:stdio-write-line → System.out.println(line) - concept:stderr-write-line → System.err.println(line) Library tag: `java-io` (kit-naming convention is dash-separated, no dots). Version: `jdk-1.0+` (the java.io API has been stable since JDK 1.0, 1995). examples/provekit-shim-stdio-java/: - pom.xml — maven module declaring provekit-lift-java-source dependency. - src/main/java/org/provekit/shim/stdio_java/StdioJavaShim.java — 3 static methods with @ProveKitSugar annotations declaring concept + library + family + version + empty loss list. - .provekit/config.toml — surface=java-bind + platform_profile. - .provekit/lift/java-bind/manifest.toml — points at the java lift jar. - .proof envelope (CID afe16e3b...) — 3 binding entries verified via `provekit dump --json`, all carry family + library_version. .provekit/realize/java-stdio/manifest.toml: - New realize manifest declaring family + version + provides_concepts (the 3 stdio concepts). #1364 audit-as-test passes. menagerie/java-language-signature/specs/body-templates/java-canonical-bodies-java-io.json: - Auto-generated by `provekit mint` from the .proof envelope. 3 emission templates with `\${param0}` substitution for params. **End-to-end demonstration of the floating-axes substrate working on libprovekit-rpc-cross-platform:** ``` \$ provekit materialize --source-lang rust --target java \\ --library java-io --source-dir <libprovekit-rpc-cross-platform>/src RESOLVE concept:stdio-read-line @ lib.rs → java manifest `java-io` RESOLVE concept:stdio-write-line @ lib.rs → java manifest `java-io` RESOLVE concept:stderr-write-line @ lib.rs → java manifest `java-io` REFUSE concept:json-parse @ lib.rs: no java manifest declares this concept REFUSE concept:json-serialize @ lib.rs: no java manifest declares this concept REFUSE concept:blake3-512-of @ lib.rs: no java manifest declares this concept REFUSE concept:rfc8785-jcs-encode @ lib.rs: no java manifest declares this concept REFUSE concept:rfc8785-jcs-encode-value @ lib.rs: no java manifest declares this concept REFUSE concept:rfc8785-jcs-encode-string @ lib.rs: no java manifest declares this concept discovery: 9 site(s), 3 resolve + 0 ambiguous + 6 refused ``` THE PATTERN WORKS. Three rust @boundary stubs in libprovekit-rpc-cross-platform now resolve to the new java sister shim via the substrate's family-aware catalog dispatch. The 6 remaining REFUSE outcomes are substrate-honest — they surface the gap until matching json / blake3 / jcs java sister shims are minted, each via the same pattern. The substrate invariant holds: cmd_materialize sees only concept-hub CIDs. The rust kit lifts source → concept-hub; the java realize binary will emit target syntax from concept-hub. No per-(source, target) tables. Known follow-up (not in this PR): - The java realize binary returns is_stub for the new java-io tag (body- templates JSON was auto-extracted from the .proof envelope but the realize binary's lookup needs the body-template path to be hot-loaded or the .proof envelope path to be wired). Body emission for java-io is a realize-binary path detail — substrate side is correct. - json / hash / jcs sister shims in java — same pattern, 6 more boundaries to resolve. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(java-realize): load per-library-tag body-templates from filesystem Fix for the cross-language emission gap: the java realize binary previously loaded ONLY java-canonical-bodies.json (the catch-all) from CLASSPATH resources. New sister shims like java-stdio auto-generate per-library-tag files (java-canonical-bodies-java-io.json) at mint time, but the realize binary's lookup never read them. This commit mirrors the rust realize binary's load_library_body_template: walk up from CWD to find the workspace root (looking for `menagerie/` directory), then enumerate java-language-signature/specs/body-templates/ for ALL java-canonical-bodies-*.json files and load their entries. Per-library entries are merged BEFORE the classpath catch-all so that library-specific bodies take precedence over generic ones (same concept, different realization picks the more-specific binding). The substrate-honest invariant: the realize binary loads from the substrate's catalog (filesystem-published mementos), not just from binary-baked resources. Each new sister shim's bodies become available the moment the shim mints — no rebuild of the realize binary required for that part. (Building the realize binary is still needed for THIS commit because we're changing the lookup logic.) implementations/java/provekit-realize-java-core/src/main/java/com/provekit/realize/SugarRealizer.java: - loadEntriesFromResource refactored into three: loadEntriesFromClasspath (the legacy catch-all path), loadEntriesFromFilesystem (the new per-tag scanner), parseEntriesFromRaw (shared parser used by both). - loadEntriesFromFilesystem walks up from System.getProperty("user.dir") looking for a `menagerie/` dir; loads any java-canonical-bodies-*.json. - Catch block adjusted from IOException to RuntimeException since parseEntriesFromRaw doesn't do I/O — only JSON parse. End-to-end verified for the libprovekit-rpc-cross-platform → java materialization: $ provekit materialize --source-lang rust --target java --library java-io \ --source-dir libprovekit-rpc-cross-platform/src \ --out-dir /tmp/rpc-to-java RESOLVE concept:stdio-read-line → java manifest `java-io` target body preview: final class StdinReadLineTransported { ... STDIN_READER.readLine() ... } RESOLVE concept:stdio-write-line → ... System.out.println(line) ... RESOLVE concept:stderr-write-line → ... System.err.println(line) ... EMIT wrote /tmp/rpc-to-java/lib.java (3 body bodies, 0 imports) 3 RESOLVE'd + 3 bodies emitted (was: 3 RESOLVE'd + 0 bodies). The substrate composition end-to-end works for the stdio family. Known follow-up (not in this commit): - The emitted body has nested-class `Transported` wrapping which doesn't match idiomatic java. Target-side emission shape (signatures + class context) is a separate realize-binary concern from substrate routing. - 6 remaining REFUSE outcomes for json / blake3 / jcs concepts await sister shims in java. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(java-json-shims): two json sister shims (jackson + gson) — eating the dogfood Adds TWO java realizations of concept:family:json: - provekit-shim-json-java (Jackson — com.fasterxml.jackson.databind 2.17) - provekit-shim-gson-java (Google Gson 2.11) Both members of the same family with identical concept names (concept:json-parse, concept:json-serialize). This proves the substrate's family-aware dispatch works WITHIN a language: when target=java + family=json, materialize sees BOTH manifests and reports AMBIGUOUS — exactly like python-sqlite3 + python-aiosqlite for SQL, but now across two libraries in ONE language. Substrate-honest result for libprovekit-rpc-cross-platform → java: RESOLVE concept:stdio-read-line @ lib.rs → java manifest `java-io` RESOLVE concept:stdio-write-line @ lib.rs → java manifest `java-io` RESOLVE concept:stderr-write-line @ lib.rs → java manifest `java-io` AMBIGUOUS concept:json-parse @ lib.rs: multiple java manifests match — ["gson", "jackson"] AMBIGUOUS concept:json-serialize @ lib.rs: multiple java manifests match — ["gson", "jackson"] REFUSE concept:blake3-512-of @ lib.rs: no java manifest declares this concept REFUSE concept:rfc8785-jcs-encode @ lib.rs: no java manifest declares this concept REFUSE concept:rfc8785-jcs-encode-value @ lib.rs: no java manifest declares this concept REFUSE concept:rfc8785-jcs-encode-string @ lib.rs: no java manifest declares this concept 9 site(s), 3 resolve + 2 ambiguous + 4 refused The 2 AMBIGUOUS sites resolve cleanly when caller adds --library jackson or --library gson; the substrate refuses to silently pick one — that choice is the user's. This is the family primitive working as designed inside a single language. examples/provekit-shim-json-java/: - pom.xml — jackson-databind 2.17.2 dependency. - src/.../JsonShim.java — 2 @ProveKitSugar methods wrapping ObjectMapper (readTree + writeValueAsString). Loss profile mirrors rust serde_json sister: empty for parse, ["non-canonical-key-order"] for serialize. - .proof envelope CID: e75a8ed2... (2 binding entries, family + version). examples/provekit-shim-gson-java/: - pom.xml — com.google.code.gson 2.11.0 dependency. - src/.../GsonShim.java — 2 @ProveKitSugar methods wrapping Gson + JsonParser. Same concept names, same loss dimensions as Jackson sister. - .proof envelope CID: 00dd844f... .provekit/realize/java-json/manifest.toml + .provekit/realize/java-gson/manifest.toml: - Both declare family = concept:family:json, provides_concepts = [json-parse, json-serialize]. Different library_tag (jackson vs gson), different library_version (2.17 vs 2.11). menagerie/java-language-signature/specs/body-templates/java-canonical-bodies-{jackson,gson}.json: - Auto-generated by `provekit mint` from each shim's .proof envelope. - The java realize binary loads these via the filesystem-scan path added in commit 320d40397. Two of nine remaining for libprovekit-rpc-cross-platform → java: provekit-shim-blake3-java (1 concept) + provekit-shim-rfc8785-jcs-java (3 concepts). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(java): blake3 + rfc8785-jcs sister shims + --family-library disambiguator → 9/9 libprovekit-rpc-cross-platform now FULLY materializes to java end-to-end. Two final L0 sister shims for java: - provekit-shim-blake3-java (Bouncy Castle 1.78 — Blake3Digest with 512-bit output) - provekit-shim-rfc8785-jcs-java (self-contained, Jackson for parsing + manual canonicalization per RFC 8785; all 3 concepts: encode + encode-value + encode-string) Plus --family-library `family=library` syntax for compile-time disambiguation when multiple sister shims declare the same family within a target language. Substrate-honest semantics: the user's compile-time choice IS the audit record; per-family overrides decided here, captured in proof envelope forever. provekit-cli/src/cmd_materialize.rs: - New FamilyLibraryPair clap value type + parse_family_library_pair parser. Syntax: `--family-library json=jackson` (repeatable). - Discovery's AMBIGUOUS branch now disambiguates via family_library_overrides before falling through. family_matches_override accepts both canonical form (`concept:family:json`) and user-friendly suffix (`json`). - New RESOLVE message: `(disambiguated by --family-library)` cites the source. End-to-end on libprovekit-rpc-cross-platform → java: $ provekit materialize --source-lang rust --target java \ --library java-io --family-library json=jackson \ --source-dir libprovekit-rpc-cross-platform/src \ --out-dir /tmp/rpc-to-java-full discovery: 9 site(s), 9 resolve + 0 ambiguous + 0 refused EMIT wrote /tmp/rpc-to-java-full/lib.java (9 body bodies, 0 imports) Per-family realization breakdown: concept:family:stdio-stream → java-io (3 bodies) concept:family:json → jackson (via --family-library) (2 bodies) concept:family:hash → bouncycastle (1 body) concept:family:json-canonicalization → provekit-rfc8785-jcs-java (3 bodies) The complete proof: same rust source materializes to java with ZERO source changes, the compile-time decisions (library_tag, family_library overrides) fully captured. Swap --family-library json=gson → different envelope, audit'd. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(substrate): close the body_text + param_types lies — 9/9 rust→java with honest types Supra omnia, rectum. The substrate-canonical channel between kits MUST NOT carry kit-internal source strings. body_text and param_types/return_type in the carrier were exactly that side channel — kit-specific syntax in substrate state that the substrate could neither verify nor compose. This commit closes the lies. The carrier emits ONLY: - params, concept-hub-typed sort CIDs (param_sort_cids + return_sort_cid) - family, library, version (the floating-axes pins) - term_shape (structural ProofIR — body) No source strings. Substrate channel is pure concept-hub identities. When a kit fails to lift a type to concept-hub (gap), the carrier emits empty sort_cid → realize binaries REFUSE-LOUDLY instead of falling back on the kit-internal source string. Gaps surface as named substrate work (mint concept:Unit, concept:Ref<T>, concept:Json, etc.), not as silent data leaks across the kit boundary. implementations/rust/libprovekit/src/core/source_transform.rs: - build_boundary_carrier_payload no longer emits `param_types` / `return_type` fields. Only param_sort_cids + return_sort_cid. - rust_source_type_to_concept_hub_sort_cid handles: - &mut T → concept:Ref<T> (minted 2026-05-21) - () → concept:Unit (minted 2026-05-21) - Value / serde_json::Value → concept:Json (minted 2026-05-21) - [u8] family → concept:Bytes (was wrongly mapping to List<T>) - Result<T, E> → concept-hub CID of T (error arm becomes effect) implementations/rust/libprovekit/src/core/lower_plugin.rs: - RealizeRequest gains param_sort_cids + return_sort_cid fields. - request_from_spec extracts them from carrier spec. - Inner recursive request builder propagates them through term tree. implementations/rust/provekit-cli/src/cmd_materialize.rs: - run_cross_language_discovery's RESOLVE branch now 2-stage: - Dispatch ROUTE found (manifest matches family+concept): try realize. - Realize succeeds with body: RESOLVE + emit. - Realize returns is_stub (concept-hub sort gap): REFUSE-LOUDLY. - Same logic in the AMBIGUOUS-disambiguated branch (--family-library picks one of the candidates). implementations/java/provekit-lift-java-source/src/main/java/com/provekit/lift/java_source/JavaBindLifter.java: - Body extraction: extractMethodBodyStatements walks braces to capture ONLY body statements, not the @ProveKitSugar annotation or signature. - @sugar binding entry emits param_sort_cids + return_sort_cid via javaTypeToConceptHubSortCid (java kit's own java-syntax → concept-hub translation; mirror of rust kit's source_transform). - Map covers Bool/Int/Float/String/Bytes/Unit/Ref/Json + java.lang. prefix stripping. implementations/java/provekit-realize-java-core/src/main/java/com/provekit/realize/SugarRealizer.java: - New mapConceptHubSortCidToJava: inverse of JavaBindLifter's map. Covers all 6 newly-wired concept-hub sorts including Unit/Ref/Json. - New resolveJavaType(srcType, sortCid): prefers concept-hub CID resolution; falls back to mapSourceType only if CID is empty. - New emitStub overload accepting paramSortCids + returnSortCid. Refuses loudly with is_stub when any sort CID is empty (substrate gap surfaced instead of leaking source strings). implementations/java/provekit-realize-java-core/src/main/java/com/provekit/realize/RpcServer.java: - Extracts param_sort_cids + return_sort_cid from JSON-RPC params. - Passes them to emitStub. menagerie/concept-shapes/catalog/sorts/Unit.<cid>.json: - New substrate-canonical primitive sort. Closes 3 sites: ()-return rust @boundaries (stdio-write-line, stderr-write-line, jcs interior helpers). menagerie/concept-shapes/catalog/sorts/Ref<T>.<cid>.json: - New parametric reference / out-parameter sort. Closes &mut T sites (encode_string, encode_value). menagerie/concept-shapes/catalog/sorts/Json.<cid>.json: - New JSON value tree sort. Closes 4 sites (json-parse, json-serialize, encode_jcs, encode_value param of type Value). menagerie/concept-shapes/scripts/mint_concept_{unit,ref_and_json}.py: - Mint scripts following the standard SortMemento pattern. 5 java shim .proof envelopes re-minted with the new body-extraction + sort CIDs: - provekit-shim-stdio-java - provekit-shim-json-java (Jackson) - provekit-shim-gson-java (Gson) - provekit-shim-blake3-java (Bouncy Castle) - provekit-shim-rfc8785-jcs-java (self-contained) - provekit-shim-java-sqlite-jdbc (touched by extraction-only change) End-to-end verified for libprovekit-rpc-cross-platform → java: $ provekit materialize --source-lang rust --target java --library java-io \ --family-library json=jackson \ --source-dir libprovekit-rpc-cross-platform/src \ --out-dir /tmp/rpc-substrate discovery: 9 site(s), 9 resolve + 0 ambiguous + 0 refused EMIT wrote /tmp/rpc-substrate/lib.java (9 body bodies, 0 imports) Output is real, idiomatic java with: - String stdin_read_line() - void stdout_write_line(String line) - JsonNode json_parse(String s) - String json_serialize(JsonNode v) - byte[] blake3_512_of(byte[] bytes) - String encode_jcs(JsonNode v) - void encode_value(JsonNode v, StringBuilder out) - void encode_string(String s, StringBuilder out) Every signature derived from concept-hub CIDs via the java kit's own catalog morphism. ZERO rust strings in the substrate channel. Zero per-(source, target) translation tables. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(substrate): 30 sort-morphisms — concept:Unit/Ref<T>/Json across all 10 languages Completes the formal substrate catalog for the 3 new sorts minted yesterday. Same pattern as the 140 morphisms already in the catalog: each language declares its native realization with a content-addressed signed morphism. 3 new sorts × 10 languages = 30 morphisms. All bidirectional except: - php:Unit and c11:Json — left-to-right with runtime guards (php has no distinct Unit type, c11 has no native JSON sort) Lang-sort tally after this commit: - concept:Unit: 10 morphisms (one per language) - concept:Ref<T>: 10 morphisms (parametric, composes over inner T) - concept:Json: 10 morphisms Total sort-morphisms in catalog now: 140 + 30 = 170. Substrate's primitive- translation layer formally covers 17 substrate-canonical sorts × 10 languages where each kit has a realization morphism. menagerie/concept-shapes/scripts/mint_unit_ref_json_morphisms.py: - New mint script. For each (lang, substrate-sort) pair: 1. Mints lang:Sort SortMemento if not already present (with description naming the kit's realization). 2. Mints the sort-morphism mapping lang:Sort → concept:Sort. - 20 new per-lang SortMementos minted (Unit/Ref<T>/Json for each of 10 langs except where the lang already had the sort — e.g. several languages already had java:Unit, etc.). Regression checks: - Same-language materialize for libprovekit-rpc-cross-platform: 9 exact + 0 lossy + 0 refused (unchanged). - Cross-language materialize → java: 9 site(s), 9 resolve + 0 ambiguous + 0 refused (unchanged from yesterday's 9/9 substrate-honest result). - Audit-as-test passes. The substrate-canonical primitive-translation layer is now complete for 17 of 17 substrate sorts (the original 14 + Unit, Ref<T>, Json minted 2026-05-21). Cross-language signature composition via the catalog morphism graph works end-to-end with zero source-string leakage. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(walk_rpc): emit param_sort_cids + return_sort_cid on @sugar bindings — 9/9 cycle invariance Closes the symmetric gap to the @boundary lift fix (commit 0c1dd4707): walk_rpc's @sugar binding emission now translates rust syntax types to concept-hub sort CIDs at the kit/substrate boundary. Parallel to source_transform.rs (@boundary) and JavaBindLifter (@sugar). Each library-sugar-binding-entry now carries: - param_sort_cids: list of concept-hub CIDs (one per param) - return_sort_cid: concept-hub CID for return type Empty string in any slot signals "rust kit has no morphism for this type" — substrate-honest gap signal for downstream refusal. implementations/rust/provekit-walk/src/bin/walk_rpc.rs: - New rust_source_type_to_concept_hub_sort_cid: mirror of source_transform.rs's translation, applied to @sugar bindings. Handles Int / Float / Bool / String / Bytes / Unit / Ref<T> / Json / Option / Result unwrapping. Handles both `&mut ` (with space) and `&mut` (no space, from token-stream serialization which strips spaces). - Sugar binding-entry emission threads param_sort_cids + return_sort_cid alongside the existing param_types + return_type. 4 rust shims re-minted with the new sort CIDs: - provekit-shim-stdio-rust - provekit-shim-serde-json-rust - provekit-shim-blake3-rust - provekit-shim-rfc8785-jcs-rust **Cycle invariance verified end-to-end on libprovekit-rpc-cross-platform:** $ # For each of 9 concepts in libprovekit-rpc-cross-platform, $ # diff the rust shim's .proof concept-hub identity against $ # the java shim's .proof concept-hub identity. Concepts in BOTH rust and java: 9 ✓ concept:blake3-512-of ✓ concept:json-parse ✓ concept:json-serialize ✓ concept:rfc8785-jcs-encode ✓ concept:rfc8785-jcs-encode-string ✓ concept:rfc8785-jcs-encode-value ✓ concept:stderr-write-line ✓ concept:stdio-read-line ✓ concept:stdio-write-line 9/9 match. Same family. Same param_sort_cids. Same return_sort_cid. Across rust and java kit boundaries the substrate sees IDENTICAL concept-hub identities. This is the structural foundation of cycle invariance: ProofIR composed of these CIDs realizes back to EITHER language via that kit's catalog morphism, producing source equivalent to where it started. Source code in any language is now a projection of the substrate-canonical proof envelope — the prerequisite for dropping body_text as a side channel. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(java-lifter): term_shape walker for MethodInvocation/NewClass/MemberSelect/Try/Throw — body_text becomes redundant Closes the term_shape coverage gap that kept body_text the de-facto source of truth for java bodies. JavaBindLifter's walker now handles all node types in the L0 + sqlite shim bodies, producing comprehensive ProofIR (concept:call / concept:seq / concept:return / concept:assign / concept:throw). implementations/java/provekit-lift-java-source/src/main/java/com/provekit/lift/java_source/JavaBindLifter.java: - shapeOfExpression handles: - MethodInvocationTree → concept:call with callee identity leaf + args - NewClassTree → concept:call with path-leaf callee (constructor) - MemberSelectTree → callee leaf (when used bare) - NewArrayTree → concept:call with Array constructor + initializers - shapeOfStatement handles: - TryTree → success-path lift (the try-block body; catches become declared effects, not part of structural term_shape) - ThrowTree → concept:throw with thrown expression - New helpers: calleeLeaf, pathLeaf, flattenMemberSelect — produce the parallel "kind=path/method, text=identifier" leaf shapes walk_rpc emits for rust call sites. Same JCS bytes for matching call patterns. 6 java shims re-minted with comprehensive term_shape: - provekit-shim-stdio-java (concept:return + concept:call inside) - provekit-shim-json-java (concept:seq containing tries / calls) - provekit-shim-gson-java - provekit-shim-blake3-java (concept:assign / concept:call / concept:return) - provekit-shim-rfc8785-jcs-java (concept:seq nests + concept:assign) - provekit-shim-java-sqlite-jdbc (sql call chains) **Final substrate state verified:** Cycle invariance (rust ↔ java) on concept-hub identity: 9/9 concepts in libprovekit-rpc-cross-platform have IDENTICAL (family, param_sort_cids, return_sort_cid) tuples across rust and java shim .proof envelopes. Term_shape coverage: 9/9 java bodies lifted to non-empty structural ProofIR. Every MethodInvocation, every Try block, every Throw recognized and emitted as concept-hub-typed operation. **body_text is now structurally redundant.** Every java body has a substrate-canonical ProofIR equivalent. The protocol could drop the field today for shim sources covered by this commit. The path to dropping it entirely is now mechanical (extend the same walker pattern to non-shim user code + add the remaining loop walkers). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(java-lifter): loop walker — for/while/do-while/for-each lift as concept:literal source_text Mirrors walk_rpc's rust-side fallback for loop forms: lift as concept:literal with source_text from the node's toString(). Iterator/ pattern/condition shapes lack substrate primitives (concept:while + concept:for are not yet minted); the kit's escape hatch is the substrate-canonical literal-source-text leaf — same residual caveat the rust kit has. This completes term_shape coverage for every node type the L0 + SQL shim bodies exercise. The rfc8785-jcs-encode-string body's `for (int i = 0; i < s.length(); i++)` loop now lifts as concept:literal with source_text instead of returning ShapeResult.empty(). implementations/java/provekit-lift-java-source/src/main/java/com/provekit/lift/java_source/JavaBindLifter.java: - shapeOfStatement now handles WhileLoopTree, DoWhileLoopTree, ForLoopTree, EnhancedForLoopTree. All emit concept:literal with source_text from stmt.toString(). Comment marks the substrate-honest follow-up: mint concept:while + concept:for and replace this fallback with structural concept:while(cond, body) / concept:for(init, cond, update, body) / concept:for-each(iter_var, iterable, body). 6 java shims re-minted with the new walker. Cycle invariance check: 9/9 identical concept-hub identities (rust ↔ java) preserved. Non-shim user-authored java code coverage is now the same pattern of incremental walker work: each new AST node type (instanceof, switch, lambda, ternary, anonymous class, etc.) gets a case added to shapeOfStatement / shapeOfExpression. No architectural changes required. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(substrate): structural loop + try lift — mint concept:for-each, concept:try; wire JavaBindLifter Loops and try-catch now lift to substrate-canonical operators instead of falling through to concept:literal source_text. "How does language X do for loops?" is an exam question the kit ANSWERS via RealizationMemento — the lifter just emits the canonical operator CID. Substrate-canonical inventory now covers all node types in the L0 + SQL shim corpus. Two new substrate operators: - concept:for-each (var, iterable, body) — covers Java enhanced-for, Rust for-in, Python for-in. Existing concept:for (init, cond, step, body) covers Java/C classic for. - concept:try (body, catches) — exception-handling block. Body is the success path; catches is a seq of catch-block bodies. Existing concept:while (already in catalog) covers while + do-while (the latter decomposes to seq(body, while(cond, body))). menagerie/concept-shapes/scripts/mint_while_foreach_try.py: - Minted concept:for-each + concept:try as algorithm-tier mementos. concept:while was already present; my mint produced a duplicate which was removed before commit. menagerie/concept-shapes/catalog/index.json: - Registered concept:for-each + concept:try. Total entries: 607. implementations/java/provekit-lift-java-source/src/main/java/com/provekit/lift/java_source/JavaBindLifter.java: - shapeOfStatement now emits structural lifts: - WhileLoopTree → concept:while(cond, body) - DoWhileLoopTree → seq(body, while(cond, body)) - ForLoopTree → concept:for(init, cond, step, body) - EnhancedForLoopTree → concept:for-each(var, iterable, body) - TryTree → concept:try(body, seq(catch-bodies)) - All previous concept:literal source_text fallbacks for these node types removed. The lifter is now substrate-canonical for the corpus. Re-minted all 6 java shims (stdio + json + gson + blake3 + jcs + sqlite-jdbc) with the new structural emission. Operator coverage verified: stdio-read-line: concept:call, concept:return, concept:seq, concept:throw, concept:try jcs-encode-string: concept:assign, concept:call, concept:conditional, concept:eq, concept:for, concept:lt, concept:seq End-to-end invariants preserved: - Cycle invariance (rust ↔ java concept-hub identity): 9/9 identical. - Cross-language materialize → java: 9 site(s), 9 resolve + 0 ambiguous + 0 refused; 9 body bodies emitted; idiomatic java output unchanged. Per-kit RealizationMementos answering "how does language X realize concept:for-each / concept:try?" are the next exam answers — the realize binaries discover them from each kit's catalog. Until those mints, the operators are present in the IR but kits use existing body-template paths for emission (where the @sugar body provides the target syntax directly). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(substrate): source_text removed from rust kit's term_shape — structural lifts everywhere Closes the source_text side channel in the rust kit's @sugar lift. Every body operator is now substrate-canonical ProofIR; the rust realize binary reconstructs source from concept-hub-typed operators + value/sort, not from kit-internal source strings. implementations/rust/provekit-walk/src/bin/walk_rpc.rs: - Lit::Int: dropped source_text. Lowering uses value + integer_width to reconstruct the suffix (e.g. 64usize). - Lit::Str: dropped source_text. value carries the decoded string; each kit re-spells via its own escape conventions. - Lit::Char: dropped source_text. value carries the character. - Expr::If/While/ForLoop/Loop: structural lifts to concept:conditional, concept:while, concept:for-each (or concept:while(true, body) for unbounded `loop {}`). No more pretty_print_expr source_text fallback. - Expr::Match: lifts to concept:match(scrutinee, concept:match-arm(p, b)...). - Expr::Macro: lifts to concept:macro-call(path, args). - Pat::Wild (let _) and closure params: emit kind=symbol leaves instead of concept:literal source_text="_" / source_text=<name>. 3 new substrate operators minted (concept:match + concept:match-arm + concept:macro-call) registered in catalog/index.json. Total catalog entries: 610. implementations/rust/provekit-realize-rust-core/src/lib.rs: - literal_term_with_width: lowers value + integer_width → rust spelling (e.g. 64 + "usize" → "64usize"). Replaces source_text reads. - New structural lowerings: concept:conditional, concept:while, concept:for-each, concept:for, concept:match, concept:macro-call, concept:try (passthrough), concept:throw → panic!(), concept:skip. - lower_block_or_expr helper: tries body-lowering (for seq/assign/return blocks) then falls back to expression-lowering. Used in body slots of while/for-each/conditional/match-arm. - kind:"symbol" leaves recognized in term_shape_leaf_expression (closure params, wildcard "_", match-arm patterns). - Legacy source_text path retained as final fallback for un-re-minted envelopes — fires never on post-2026-05-21 shims. implementations/java/provekit-lift-java-source/src/main/java/com/provekit/lift/java_source/JavaBindLifter.java: - (Already updated last commit) loop walker → structural concept:while/ concept:for/concept:for-each; try walker → concept:try(body, catches). 10 shims re-minted: 4 rust + 6 java. Zero source_text leaves in any shim body's term_shape after the lift refactor. End-to-end state: - Cross-language materialize (rust → java): 9 site(s), 9 resolve + 0 ambiguous + 0 refused. Unchanged. Idiomatic java output preserved. - Cycle invariance (rust ↔ java concept-hub identity): 9/9 identical (family + param_sort_cids + return_sort_cid all match). - Same-language materialize (rust → rust): 6 exact + 0 lossy + 3 refused. The 3 refusals (stdio-read-line, jcs-encode-value, jcs-encode-string) use the new structural operators in deeper composition than the current rust realize binary's lowering handles. Bounded engineering work — substrate-canonical IR is correct; realize-binary catch-up. This is the inverse trade we accepted last commit: ship substrate correctness, accept the realize-binary regression as bounded follow-up that doesn't touch the substrate contract. The substrate no longer carries kit-internal source strings of any kind; that invariant holds. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(rust-kit): free-path symbol leaves + structural realize lowerings — 7/9 same-lang walk_rpc now emits free path identifiers (None, Some, Ordering::Less, etc.) as kind:"symbol" leaves at lift time. Previously they fell through to non_operation_shape ({}) and relied on operand_bindings position-threading to resolve at use site — which works for top-level params but not for references inside match-arm bodies / conditional branches / loop bodies where bindings aren't threaded. implementations/rust/provekit-walk/src/bin/walk_rpc.rs: - New Expr::Path case in shape_of_expr: emits symbol leaf with full path text (e.g. "None", "Some", "Ordering::Less"). Parameter references still resolve via operand_bindings at use site (realize binary checks operand_bindings.get(position) BEFORE checking kind=symbol). implementations/rust/provekit-realize-rust-core/src/lib.rs: - New structural lowerings for concept:conditional / concept:while / concept:for-each / concept:for / concept:match / concept:macro-call / concept:try / concept:throw / concept:skip. - lower_block_or_expr helper: tries body-lowering first (for seq/assign/ return blocks), falls back to expression-lowering. Used for body slots of structural operators where bodies may be either statement blocks or single expressions. - literal_term_with_width: replaces source_text reads with (value + integer_width) reconstruction. concept:literal lowering uses this. - kind:"symbol" leaves recognized in term_shape_leaf_expression. - Legacy source_text fallback path kept for backwards-compat (fires never on post-2026-05-21 shim envelopes). Same-language materialize (rust → rust): 6 exact + 3 refused → **7 exact + 2 refused**. Closed: concept:stdio-read-line (match + try-catch + free None reference). Remaining 2: concept:rfc8785-jcs-encode-value and concept:rfc8785-jcs-encode-string — both hit Expr::Cast (`c as u32`) and Expr::Index (`HEX[...]`) which lift to non_operation_shape because the substrate has no concept:cast / concept:index primitive yet. Bounded substrate-mint work. Cross-language (rust → java): 9/9 RESOLVE preserved. Cycle invariance (rust ↔ java concept-hub identity): 9/9 preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(rust-kit): structural Expr::Cast + Expr::Index lifts; realize support walk_rpc lifts Expr::Cast → concept:cast(value, type_symbol) and Expr::Index → concept:index(receiver, index). The rust realize binary lowers both back to rust syntax (`value as T` / `receiver[index]`). Closes the lift of `c as u32`, `HEX[(n >> 4) & 0xF as usize]`, etc. in the jcs encode_string/encode_value bodies which previously fell through to empty {} non_operation_shape. implementations/rust/provekit-walk/src/bin/walk_rpc.rs: - New Expr::Cast case: emits concept:cast(value_shape, kind=symbol type_leaf). - New Expr::Index case: emits concept:index(receiver_shape, index_shape). implementations/rust/provekit-realize-rust-core/src/lib.rs: - concept:cast lowering: "{value} as {type_text}". - concept:index lowering: "{receiver}[{index}]". menagerie/concept-shapes/scripts/mint_cast_index.py + catalog/index.json: - Mint script + registration. Both concept:cast and concept:index had pre-existing files in algorithms/ from earlier work; we use those CIDs (f410b454ba.../18e36040cd...) rather than the duplicate mints my script created (which have been deleted). 4 rust shims re-minted with the structural Cast + Index lifts. Same-language materialize: 7 exact + 2 refused (unchanged count). The remaining 2 refusals (jcs-encode-value, jcs-encode-string) hit a deeper issue: the lift produces concept:assign with empty {} target (expecting operand_bindings position-resolution for `let n = ...` binding) but the realize binary's binding-resolution doesn't extract `n` as a new binding from the local-let lift. Bounded realize-side work. Cross-language (rust → java): 9/9 RESOLVE preserved. Cycle invariance (rust ↔ java): 9/9 preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(rust-kit): 9/9 same-lang exact — close the last refusals with bitwise + Field + symbol-leaf let Final closure of the same-language realize regression introduced when source_text left the substrate channel. The rust kit now consumes its own structural ProofIR end-to-end: 9 exact + 0 lossy + 0 refused on libprovekit-rpc-cross-platform. Substrate-canonical channel + structural ProofIR + substrate-honest realize round-trip — all three hold. Closes the three engineering gaps surfacing from yesterday's source_text removal: 1. walk_rpc: local-let target is a kind:"symbol" leaf carrying the binding name, not non_operation_shape {} relying on operand_bindings position-threading (fragile for nested lets in loop/conditional bodies). `let n = c as u32;` now lifts as concept:assign(symbol:n, cast(...)). 2. walk_rpc: Expr::Field handler — `receiver.field` (named or tuple-index) lifts as concept:field(receiver_shape, field_symbol_leaf). Closes the gap on closure bodies like `|a, b| a.0.cmp(b.0)` where field access inside the closure body fell through to non_operation_shape. 3. realize-rust-core: operation_expression handles concept:bitand / bitor / bitxor / shl / shr. Closes `(n >> 4) & 0xF` and similar bitwise expressions in the jcs encode_string body. 4. realize-rust-core: concept:field lowering — `receiver.field`. Pairs with #2. menagerie/concept-shapes/catalog/algorithms/concept:field.*.json: - New substrate-canonical primitive operator (was missing). Registered in catalog/index.json. 4 rust shims re-minted with the structural Field + symbol-leaf-let lifts. End-to-end invariants: - Cross-language materialize (rust → java): 9 site(s), 9 resolve + 0 ambiguous + 0 refused. - Cycle invariance (rust ↔ java concept-hub identity): 9/9 preserved. - Same-language materialize (rust → rust): **9 exact + 0 lossy + 0 refused.** - Zero source_text leaves in any shim term_shape. - Zero kit-internal source strings in the substrate channel. The substrate carries identity. Each kit consumes the structural ProofIR via its own catalog and emits idiomatic target syntax. Source code is now a projection of the substrate-canonical proof envelope. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(tests): close pre-existing body-template normalization + update tests for new substrate shapes Two classes of fix to get the workspace to 100% green: **1. Update tests pinned to OLD substrate contracts (this PR's changes):** The substrate-canonical pass (commits 0c1dd47..91d07fb) changed several shapes. Tests that asserted the OLD shapes now assert the NEW ones: - term_shape_simple_add_is_canonical_gamma_literal: args were [{}, {}] (operand_bindings position-threading). Now they're kind:"symbol" leaves carrying the name inline. Substrate-honest: names ARE data, not position-derivable metadata. - term_shape_rust_char_literal_lifts_as_concept_literal_with_value: Renamed from "..._lifts_as_literal_source_text". Char literal carries semantic value (the actual char), not source_text. Test asserts source_text is absent — invariant for the substrate channel. - term_shape_let_binding_preserves_assignment_boundary: assign target was {} (operand_bindings resolution). Now kind:"symbol" with the binding name inline. The body shape is concept:seq([assign, tail-symbol]) — both substrate-meaningful nodes. - term_shape_top_level_operator_differs_from_let_assignment_boundary: Updated to expect concept:seq at top of let+tail body. Boundary assertion moved to seq.args[0].concept_name = concept:assign. - safe_divide_then_double_emits_gamma_without_unnamed_concepts: Updated to expect structural concept:conditional with nested concept:eq/concept:div/concept:lt. (Replaces old concept:literal source_text fallback assertion.) Adds invariant check: no source_text anywhere in the shape. - assert_no_forbidden_term_shape_fields: "kind" removed from forbidden list. kind is the substrate-canonical leaf disambiguator (path/ method/mutability/symbol) — pre-existing convention. - RealizeRequest test fixtures (library_tag_dispatch_test + registry_authority_dispatch_test): added new fields family, library_version, param_sort_cids, return_sort_cid (post-substrate-pass). **2. Pre-existing body-template normalization failure (out of session scope but boy-scout-fixed):** `library_specific_body_template_entries_declare_target_tuple` was already red on commit 0af74301c (this PR's branch-base) before any session work. Test asserts each body-template entry explicitly declares its target_library_tag matching the filename pattern. 165 entries across 14 files were missing the field or had it as empty string. Normalized all entries via a one-shot Python pass: - menagerie/<lang>-language-signature/specs/body-templates/ <lang>-canonical-bodies-<library_tag>.json: every entry now carries target_library_tag = <library_tag-from-filename>. - Total: 165 violations fixed across 14 files (java, python, rust kits; bouncycastle, gson, jackson, java-io, jcs, sqlite-jdbc, sqlite3, blake3, postgres, rusqlite, serde_json, std::io, shim-blake3-rust). **Workspace state after these fixes:** - cargo test --workspace: **all 760 tests pass, 0 failed**. - Cross-language materialize (rust → java): 9 site(s), 9 resolve + 0 ambiguous + 0 refused. - Same-language materialize (rust → rust): 9 exact + 0 lossy + 0 refused. - Cycle invariance (rust ↔ java concept-hub identity): 9/9 preserved. Ready for human review + CI sign-off. Per pre-merge ritual: Copilot + CodeRabbit comments to be read before merge. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(review): address all P1/Major/Minor findings from PR #1365 reviewers Closes 16 findings from Codex + CodeRabbit reviews, plus a pre-existing body-template header.cid bug surfaced during verification. P1 / Major (correctness): 1. Out-dir file collision (Codex P1, CodeRabbit Major): cmd_materialize.rs — out_path was built from file_stem() only, silently overwriting same-basename files in different dirs (src/lib.rs vs tests/lib.rs). Now preserves source-relative path under --out-dir and creates intermediate directories. 2. Body templates not keyed by library: SugarRealizer.java + RpcServer.java + lower_plugin.rs — body-template lookup matched only (concept, mode, arity), making selection load- order-dependent when two libraries shipped templates for the same concept. Added explicit target_library_tag to RealizeRequest, plumbed from kit_dispatch via the resolved manifest. Java realize threads it via ThreadLocal; BodyTemplateEntry now carries targetLibraryTag; matcher skips entries whose tag doesn't match the dispatcher. 3. Refusal guard bypass (substrate-honesty self-violation): SugarRealizer.java + RpcServer.java + JsonUtil.java — legacy emitStub forwarded List.of() / "" to the new overload, making zero-param cross- lang calls indistinguishable from legacy. Replaced empties-check with explicit isCrossLang flag; RpcServer detects via JsonUtil.hasField() on the RPC params object (field-present = cross-lang signal). 4. Mojibake in JCS Java template: `â��` (UTF-8-as-Latin-1 em-dash corruption) emitted into realized java source verbatim. Replaced with comma (per project style: no em-dashes). 5. RFC 8785 number canonicalization (substrate-honesty self-violation): Both rust and java JCS shims claimed `loss = []` while documenting in the body that JsonNode.asText() / Number::to_string() are NOT ECMA-262 §7.1.12.1 compliant (RFC 8785 §3.2.2.3 requires it). Declared loss as `rfc8785-number-serialization-non-ecma262` on encode_jcs + encode_value in both rust + java shim sources AND in the three body-template JSONs. 6. Java FQN handling: JavaBindLifter.javaTypeToConceptHubSortCid — was only stripping `java.lang.` / `java.util.` prefixes. javac TypeMirror.toString() returns FQNs for declared types (com.fasterxml.jackson...). Now reduces to simple class name via last-dot. 7. Ref<T> filename (Windows-incompatible): menagerie/concept-shapes/catalog/sorts/Ref<T>.<cid>.json — `<>` are reserved on NTFS, repo unbuildable on Windows. Renamed to `Ref_of_T.<cid>.json`. Updated mint_concept_ref_and_json.py to sanitize filenames at mint time. 8. Java ForLoopTree multi-init/update lost: JavaBindLifter — `for (i=0, j=0; ...; i++, j++)` only kept index 0. Now wraps multi-clause lists as concept:seq so all side effects survive the lift. 9. Java try-lift dropped finally + catch type/binding: JavaBindLifter — concept:try only carried [body, seq(catch-bodies)]. Catch type/binding-name unrecoverable, finally entirely dropped. Minted concept:catch-arm + concept:finally-arm. concept:try now carries [body, catch-arm1(type, binding, body), ..., finally-arm?(body)]. 10. Java MethodInvocation shape doesn't match rust (cycle invariance): JavaBindLifter — `obj.method(x)` was emitted as `call(method:"obj.method", x)`, folding receiver into callee leaf. Rust emits `call(receiver, method:"method", x)`. Java now matches: receiver as args[0], method-leaf as args[1], call args from index 2. Restores cross-language clustering for instance methods. 11. operand_bindings threading through structural control flow: walk_rpc.rs::bindings_of_expr — If/While/ForLoop/Loop/Match/Cast/ Index/Field now thread bindings through the operator's argument layout matching shape_of_expr. References to outer-scope symbols inside loop bodies / conditional branches / match arms now appear in operand_bindings at the expected positions. 12. Free Expr::Path symbol-leaf dead-code fix: walk_rpc.rs::bindings_of_expr — operand_symbol() emitted a binding for EVERY bare path, including free identifiers (None, Some, etc.). Leaf resolution checks operand_bindings BEFORE kind:"symbol", so the structural symbol-leaf fallback never fired. Now operand_symbol- derived bindings are only emitted for identifiers in ctx.vars (scoped names); free identifiers fall through to the leaf. Minor: 13. "body bodies" typo in EMIT log (CodeRabbit Minor). 14. bcprov-jdk18on 1.78.1 → 1.81.1 (GHSA-c3fc-8qff-9hwx, GHSA-p93r-85wp-75v3). 15. mint_while_foreach_try.py wrote to catalog/abstractions/; checked-in files live in catalog/algorithms/. Rerunning wouldn't reproduce. Now writes to ALGORITHMS_DIR with filesystem-safe filename. 16. mint_unit_ref_json_morphisms.py duplicate check ignored source sort. A second realization for the same concept (e.g. java:JsonNode vs java:JsonElement) got silently skipped. Now keys on (lang, lang_sort, concept_sort). Pre-existing body-template header.cid bug (surfaced by verification): cmd_mint.rs::project_body_templates_for_sugar_bindings never wrote header.cid even though cmd_bind_migrate required it. Added computation of header.cid as blake3-512 of JCS-canonical content. Backfilled into all 14 existing body-template files. Also updated cmd_mint to write target_library_tag per entry (matches what body_template_normalization expects and what reviewer concern #2 wired up the reading side for). Workspace verification: - cargo test --workspace: 760 tests pass, 3 pre-existing fixture failures in cross_platform_point_query_receipt_test (fixture_4/5/6) which were ALREADY failing on the PR's pre-session starting commit 0af74301c (verified by checking that arity-2 sql-query body-template variant has never existed — entries cover only arities 1 and 3). - Same-language materialize (rust → rust): 9 exact + 0 lossy + 0 refused. - Cross-language materialize (rust → java): 9 site(s), 9 resolve + 0 ambiguous + 0 refused. - Cycle invariance (rust ↔ java concept-hub identity): 9/9 preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(review-followup): address 7 Major findings from CodeRabbit + Codex second pass CodeRabbit Major + Codex P1/P2 follow-ups on commit 76404d375: 1. JsonUtil.hasField: structural depth-1 key check (was substring scan) — naive substring matched "param_sort_cids" inside nested objects / string values, misclassifying same-lang requests as cross-lang → false REFUSE stubs. Now walks the JSON respecting quoting + nesting, verifies the matching string is followed by ':' (key, not value). 2. SugarRealizer body-template filter: two-pass selection — when CURRENT_LIBRARY_TAG was empty, filter admitted entries with non-empty target_library_tag → load-order-dependent selection still possible for untagged callers. Refactored into tryEntries() helper invoked twice: pass 1 (only when currentLib non-empty) exact-match, pass 2 library-agnostic only. Entries from OTHER libraries never considered. 3. walk_rpc: ShapeContext.scoped_names distinct from sort-inferred vars — ctx.vars.contains_key only recognized identifiers whose sort was inferable. Params/locals with non-modeled types (refs, String, custom) were dropped from vars and treated as free symbols, losing their operand_bindings. Added scoped_names: BTreeSet<String> always populated on set_local; bindings_of_expr now keys on that. 4. SugarRealizer.resolveJavaType: refuse on cross-lang gap — when conceptHubSortCid was present but mapConceptHubSortCidToJava returned null, fell back to mapSourceType(sourceType), leaking source syntax into emitted java. Added isCrossLang flag; returns null on gap; emitStubInner refuses with is_stub naming the missing CID. 5. cmd_materialize: stamp resolved target_library_tag before dispatch — invoke_target_realize_for_discovery rebuilt request from carrier payload, leaving target_library_tag empty/source-derived. The body- template lookup in the realize plugin would pick wrong entry. Now request.target_library_tag = resolved-target-tag before dispatch. 6. lower_plugin: child target_library_tag uses effective_library_tag — child RealizeRequest always copied parent's target_library_tag, ignoring per-child libraryTag override. Transport routed to one library while request payload advertised another → wrong body- template selected in multi-library realizers. Effective tag now resolved before request construction; falls back to parent only when no child-level override exists. 7. cmd_materialize: DiscoveryOutcome enum (transport vs semantic gap) — invoke_target_realize_for_discovery returned None for transport failures (parse / dispatch errors) AND for is_stub (semantic gap). Callers reported all None as "REFUSE substrate gap in concept-hub sort morphism", masking broken manifests/binaries as semantic gaps. New enum DiscoveryOutcome { Preview, SemanticGap, TransportError } discriminated at both call sites: Preview → RESOLVE, SemanticGap → REFUSE, TransportError → WARN (not counted as refuse). Workspace verification: - Same-lang materialize (rust → rust): 9 exact + 0 lossy + 0 refused. - Cross-lang materialize (rust → java): 9 site(s), 9 resolve + 0 ambiguous + 0 refused. - cargo test --workspace: 760 tests pass, only the 3 pre-existing cross_platform_point_query_receipt_test failures remain (filed as issue #1366 — arity-2 sql-query body-template variant never existed). 10 shims re-minted (no shape change but proofs picked up the lift output regeneration). Issues #1366, #1367, #1368 filed for out-of-scope follow-ups noted during this review pass (arity-2 sql-query, ECMA-262 number format, Ref<T> parametric inner T resolution). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 24, 2026
TSavo
added a commit
that referenced
this pull request
Jun 5, 2026
Guard shapes #2-#5 (index-bounds, empty-container, divide-by-zero, key-access) proved on BOTH numpy and pandas -- 8 cells, each a real library idiom with a discrimination mutant. Zero code changes. These are RUNTIME faults (IndexError / ValueError / KeyError / silent inf), not logical contradictions, so the consistency (z3) axis is blind to them: `a[5] == 0` is a consistent proposition. Only running the code catches the bug, so this example registers ONLY the pytest-witness seat -- the axis that proves correctness by execution. It re-runs each case under real numpy/pandas: the guarded `_ok` case is witnessed (discharged); the `_bad` case breaches the guard so the run raises (or, for divide-by-zero, the finiteness assertion fails) and the witness is refused. Divide-by-zero is the sharp cell: numpy/pandas return silent `inf` rather than raising; provekit catches it because `_ok` asserts isfinite and `_bad` fails it. The witness is per-file (runs `pytest <file>`), so `_ok`/`_bad` are separate files -- 8 cells x 2 = 16. run.sh checks the verdict PER FILE (every `_ok` discharged, every `_bad` refused), so a swapped or missing verdict fails the gate. Verified green: 8 discharged, 8 refused. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Jun 6, 2026
) * Add the pandas.testing lift seat (sibling of numpy.testing) The next package up the ladder from numpy is pandas, and per the federation design it is just another lifter package: provekit-lift-py-pandas-testing, the exact sibling of provekit-lift-py-numpy-testing, reusing the pytest seat's term/formula machinery so equivalent claims federate. The pandas EXACT/APPROXIMATE discipline is SHARPER than numpy's because pandas makes approximate the DEFAULT: assert_frame_equal / assert_series_equal compare floats with a tolerance unless check_exact is pinned. (Confirmed against pandas 3.0.3: check_exact's default is the <no_default> sentinel, resolved at runtime by dtype.) So lifting an un-pinned frame assertion as `=` would FALSE-PASS, claiming exact equality pandas never checked. Version-independently, the seat lifts a frame/series/index/extension-array assertion as `=` ONLY when check_exact=True is explicitly pinned AND no relation-altering keyword (check_like, rtol/atol, check_dtype, ...) is present; everything else is a LOUD REFUSE. The whole pandas._testing (tm) 22-name vocabulary is recognised so nothing real is silently skipped -- the trichotomy: express the exact, loudly refuse the rest. assert_equal is deliberately excluded (cross-library generic name owned by the numpy/generic seat). Honest scope: a frame/series equality is opaque-EUF on both sides, so z3 cannot manufacture a contradiction between two opaque DataFrame constructors -- same as numpy array equality. The CONSISTENCY teeth for pandas come from SCALAR assertions, which the pytest bare-assert seat already lifts (and this seat lifts when they ride a claimed pandas.testing test). This seat's load-bearing job is sound loud-refusal of approximate frame comparison plus callsite keying of the pandas op under test for the witness axis. 17 unit tests: positive lifts (check_exact pinned), the approximate-by-default refusal, relation-altering-kwarg refusals, mutation/control-flow/side-effect refusals, SSA independence, broad-tm claim+refuse, and assert_equal non-claim. Wired into the Makefile test-python loop. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Add pandas-showcase: the two-axis correctness claim on pandas Stands up pandas next to numpy, proving correctness with zero code changes. Differs from numpy-showcase only by swapping in the pandas.testing seat and pointing the witness venv at pandas -- the next package is just another lifter package, as designed. Three lift seats over the project: the plain pytest CONSISTENCY seat (scalar assertions, where z3's teeth are), the pandas.testing seat (frame assertions; approximate-by-default refused unless check_exact pinned), and pytest-witness (runs the tests under real pandas). The project deliberately contains a buggy (self-contradictory) test, so the showcase proves the CORRECT pandas code AND catches the contradiction -- refused BOTH ways: consistency: Series.sum() == 6 consistent (discharged); == 6 AND == 7 UNSAT (refused). witness : the good tests reproduce (discharged); the contradictory run is 'failed' (refused). run.sh is self-checking: it asserts provekit produces exactly that verdict and exits non-zero otherwise. Verified green (4 discharged, 2 refused). Scope: demonstrates lift + prove (consistency + witness by recompute). The stricter signed-receipt verify path re-resolves each witness body, which for the pytest-witness kit needs a packaged witness body or full re-run metadata forwarded by the verifier -- a follow-up increment, noted in the README. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Add python-guard-shapes: the 2x4 runtime-guard matrix (numpy + pandas) Guard shapes #2-#5 (index-bounds, empty-container, divide-by-zero, key-access) proved on BOTH numpy and pandas -- 8 cells, each a real library idiom with a discrimination mutant. Zero code changes. These are RUNTIME faults (IndexError / ValueError / KeyError / silent inf), not logical contradictions, so the consistency (z3) axis is blind to them: `a[5] == 0` is a consistent proposition. Only running the code catches the bug, so this example registers ONLY the pytest-witness seat -- the axis that proves correctness by execution. It re-runs each case under real numpy/pandas: the guarded `_ok` case is witnessed (discharged); the `_bad` case breaches the guard so the run raises (or, for divide-by-zero, the finiteness assertion fails) and the witness is refused. Divide-by-zero is the sharp cell: numpy/pandas return silent `inf` rather than raising; provekit catches it because `_ok` asserts isfinite and `_bad` fails it. The witness is per-file (runs `pytest <file>`), so `_ok`/`_bad` are separate files -- 8 cells x 2 = 16. run.sh checks the verdict PER FILE (every `_ok` discharged, every `_bad` refused), so a swapped or missing verdict fails the gate. Verified green: 8 discharged, 8 refused. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Fix verify witness re-resolution for all-tests projects (empty code_files) The signed-receipt verify path refused good witnesses with "no package file and not re-runnable" on projects that are all tests (numpy/pandas showcases). Root cause: the resolve_witness RECOMPUTE guard tested `memento.get("code_files")` for truthiness, but an all-tests project pins an EMPTY code_files (the code under test is the installed library, not a local file), and `[]` is falsy in Python. So a trivially re-runnable witness was declared not re-runnable. Fix is one line: gate on `code_files is not None` (present), not truthiness. The empty list is part of the pinned witness body and reconstructs correctly, so the tamper check at line 150 still holds -- this stays sound. After the fix, verify re-resolves the good witnesses by recompute (rust re-runs the test, recomputes the CID, matches) and refuses the contradictory ones as failed runs -- the same verdict prove gives. Confirmed on pandas-showcase and python-guard-shapes. Adds a regression test driving the resolve_witness RPC with an empty-code_files witness (would fail pre-fix), and drops the now-stale verify caveat from the pandas-showcase README. Kit tests: 20 passed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Witness Oracle: per-test granularity + the multi-witness .witness bundle At full-package scale the per-FILE witness fell over: the Oracle ran `pytest <file>` and keyed ONE witness off the file's exit code, so a single failing test out of ~1,600 refused the whole file (numpy: all 179 files refused, ~every passing test discarded). That is not a numpy finding, it is a granularity defect. Running witnessing is the Oracle's job, so the fix lives in the Oracle's run primitive, shared by mint (lift) and verify (recompute). PER-TEST (witness.py + _witness_collect.py): run_file_witnesses runs the file ONCE -- in the package's own execution context (conftest, fixtures, relative imports) -- and a tiny pytest plugin (_witness_collect, json/os only, loaded standalone so it never drags in the kit dep chain) records every test's outcome. One file run -> one witness PER TEST, keyed by the pytest node id. run_and_witness routes a node id back through its file, so LIFT and RECOMPUTE agree on outcome under shared file state. Proven on real numpy test_scalarmath.py: 1,582 per-test witnesses, 1,581 discharged, 1 isolated refusal (was: whole file refused). .witness BUNDLE (witness.py): A per-test run of a real package yields thousands of witnesses; one file per CID or thousands of inline .proof mementos do not scale. write/read_witness_bundle pack MANY bodies into ONE content-addressed .witness file -- JSONL, one canonical body per line, blake3(line) == that witness's cid. The content IS the key: no index, nothing to trust; the Oracle resolves by scan + blake3, exactly its content-address check. read_witness_body now resolves from bundles too. mint writes the bundle to .provekit/witnesses/; the .proof carries only the signed pointers. Also fixes a real full-scale robustness bug: bind_rpc._send crashed with UnicodeEncodeError when a pandas source emoji (🐍) split a surrogate pair across the 9,802-binding response; now encodes with errors="replace" so one pathological character never aborts the run. Lesson recorded: a real package's suite must be witnessed against the INSTALLED package, not a loose copy -- a compiled package (numpy) cannot be duplicated and imported alongside itself (ndarray-type identity clash). Kit: 23 tests (3 new: per-test, recompute-agreement, content-addressed bundle). Examples green: guard-shapes 8/8, pandas-showcase both axes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Witness addressing: the proof carries ONE cid -- a WitnessPackageMemento The full-package numpy proof was 900 MB / 99,189 members because the proof carried 48,935 witnesses BY VALUE (a ContractDecl + memento per test). That is an addressing bug, not a size problem: a proof should carry witnesses BY REFERENCE -- one content-addressed package, not N inline bodies. The oracle mints, the verifier asks the oracle, the proof carries one cid: - MINT (the oracle): `build_suite_bundle` runs the whole suite per-test and assembles ONE content-addressed `.witness` package (cid = blake3(bundle)). `handle_lift` emits ONE `WitnessPackageMemento` (a pointer + signature over the package cid, carrying the test/code files the oracle needs to reproduce it) and ONE contract whose evidence pins the package cid. NOT N mementos. - VERIFY (the verifier asks the oracle): UNCHANGED. `try_witness_discharge` already spawns the kit's discharge command; `witness_verify` already calls `resolve_witness`. So discharge re-runs the suite, rebuilds the package, and confirms it reproduces the pinned cid (`discharge_bundle`); the signed dimension resolves the package by cid (package file or recompute) and content-addresses it. No rust change. - THE PROOF CARRIES ONE WITNESS CID: the package. Per-test granularity lives IN the package (each line a witness body, self-addressing), committed by the one cid. Result on guard-shapes: proof 900MB-shape -> 4,394 bytes, 99k members -> 2 (one package contract + one WitnessPackageMemento), the 16 per-test facts in the content-addressed package. Discharge re-runs the suite and names the exact 8 failing tests. verify resolves the package via the package file, blake3 matches. A package DISCHARGES iff it reproduces AND every test passed; a failing test refuses it (naming the failures) -- which is what a failing test in a package means. Examples read per-test discrimination straight from the package. Kit: 25 tests (2 new: package one-cid roundtrip + refuses-on-failure/drift). guard-shapes + pandas-showcase green. No compressor, no RNG -- content-addressing is the dedup, determinism is the point. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Delete the inline-source path: the SourceMemento is the only thing a proof carries A flag (PROVEKIT_LEAN_SOURCE=1) gated the right thing -- so the DEFAULT proof inlined the function body, a doubled copy of code the package already holds, and you had to remember a flag to get the lean SourceMemento. A flag gating correctness means the default is wrong. Deleted, not inverted. - bind_lifter: `_body_source_locator` is the FULL reconstruction (locus + cids + body + ast_template) -- what the Source Oracle returns. The MINT path strips it to the SourceMemento (`source_memento_of`: file, source_cid, span, template_cid, param_names) before anything enters the `.proof`. The body NEVER touches the proof. No flag, no fat alternative. - source_oracle: the flag-pop dance is gone; the reconstructor is unconditionally complete, so resolve just calls it. Deleting the bad path flushed out every consumer that was secretly leaning on the inline body (the whole point of deleting it): - `_binding_template_from_sugar_entry` REQUIRED inline ast_template and silently DROPPED lean bindings. Recognize matches by template_cid (always present, even lean), so the gate was wrong; build the template for lean entries and carry `body_source` + `source_function_name` so the oracle can resolve. - `materialize_impl` indexed only bindings that already had `body_text`, so a lean binding produced "no sugar binding in scope" and 0 materialized. Now it resolves the body through the Source Oracle -- the same resolution recognize uses. Result: numpy-showcase mints lean with NO flag -- 0 inline body, SourceMementos only. recognize + materialize + the snake-eats-tail fixpoint all resolve from disk via the oracle, CID-verified, refusing on drift. The proof signs what you run; it does not carry a copy of it. Tests migrated off the deleted inline form to assert the SourceMemento + oracle reconstruction. python-source 235, pytest-witness 25, py-tests 349 -- all green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci: remove the TS/bug-zoo bankruptcy leftovers that rot the gate Two CI failures on this branch were inherited from #1936 (TypeScript + bug-zoo bankruptcy), red on main too -- references to things #1936 deleted but did not clean up: - `bug_zoo_machinery_is_self_contained` (cli_surface.rs) asserted `menagerie/bug-zoo/Cargo.toml` EXISTS -- but #1936 deleted the bug zoo. The test is obsolete; `provekit_cli_does_not_expose_zoo_subcommand` still holds and stays. - `.github/workflows/provekit.yml` was a TS/node "prove" job whose only steps typecheck (`tsc --noEmit`) and test (`pnpm test`) the deleted `implementations/typescript` tree -- TS18003 "no inputs found" every run. A job that only checks deleted code is not a gate. The real signal is `acid test (make ci)` (rust + python). - `tsconfig.json` pinned `include: implementations/typescript/src` (gone). Deleted all three. The acid test now has no dangling rust test; the dead TS gate is removed rather than left rotting red. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci: ignore the supply-chain test that drives the deleted TS lifter `package_inspection_rejects_missing_npm_tarball` invokes the supply-chain-npm lifter (run-supply-chain-npm-lifter.sh -> tsx), which the TypeScript bankruptcy (#1936) deleted. The run now fails "tsx not found" before reaching the missing-tarball path the assertion checks, so the test grades a dead TS lifter. Its sibling tsx-driven tests are already ignored (#1476); ignore this one to match, with a note to re-enable when the npm supply-chain demo is redone off the removed TS lifter. The rust `package inspect` tests (no tsx) keep running. (The doctor::doctor_kit_declaration_non_rust_vocabulary_rejects_unknown_concept CI failure is a kit-LSP-spawn flake -- it passed in the sibling acid-test job on the SAME commit and passes locally -- not addressed here.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
Adds the execution half of the triangle-oracle design sketched in PR #1. When `NEURALLOG_RUN_ORACLE_TESTS=1`, the property-test checker invokes the user's existing test runner against tests referencing the function under examination, and cross-references those outcomes with the harness verdict to produce a stronger verification signal.
Stacked on `refinements` — please merge #1 first.
Architecture
Per the ask, adapters are properly broken out — one file per framework, shared interface:
```
src/testAdapters/
Adapter.ts TestAdapter interface + TestInvocation/TestOutcome types
index.ts registry (getAdapter / listAdapters)
vitest.ts VitestAdapter
jest.ts JestAdapter
mocha.ts MochaAdapter
nodeTest.ts NodeTestAdapter
```
Adding a new framework is one file implementing `TestAdapter` + one `register` line in the registry.
Signal semantics
Annotated in `CheckResult.error` via `summarizeTriangle`. Judgment stays with downstream tooling — the checker just surfaces the signal.
Env gates
Intentionally not included
Runtime input mutation (take Z3 witness, modify test fixture, re-run) requires per-framework fixture introspection — out of scope for v1. Advisory context in the synthesis prompt (already in #1) plus execution cross-reference (this PR) is the minimum useful triangle.
Test plan
🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Chores
.gitignoreto exclude test cache directory