feat(composition): pass typed results to exact checkers

[kaoru0822-kitauji]

Summary

This rebases the #1262 investigation onto latest practical main, b06974258ed4e987aaab41d19619f28f95be81d4, and replaces its startup-selected MCP tools with the smallest handoff fix that survives the architecture merged by #1256 and #1265.

• keep the public MCP surface fixed at exactly math.find and math.run
• expose the whole typed SmithNormalFormResult through the producer's existing output-port/value-reference mechanism
• let the separate exact checker declare a typed candidate input port and assemble its authoritative Pydantic request from payload.input plus that reference
• keep inline candidate requests supported and independently replay every referenced candidate
• fail closed on unknown ports, unknown or cross-runtime references, value-type mismatches, and inline/reference conflicts

The reference is a bounded runtime-local carrier, not evidence: it transfers no producer assurance and cannot authorize the checker or create a verification record by itself. Local and remote hosts use the same runtime adapter; no host-specific tool registration or mutable tool list was added.

Rebase and architectural decision

The old branch was based before #1256 and conflicted in the MCP tool surface, CLI, guidance, telemetry, and tool reference after rebasing onto #1265. Its three commits were intentionally dropped rather than conflict-resolved back into the tree.

#1256 established typed operations/ports/value references and the fixed two-tool search/execute surface. #1265 completed typed results to the wire, simplified verification composition, and made local/remote ownership explicit. Against that architecture, startup-fixed extra tools, local-only CLI flags, duplicated projected contracts, stale-binding telemetry, and a four-tool selection registry were no longer acceptable. This version reuses the merged typed composition primitives and adds no registry, codec, prepared handle, workflow state, or public MCP tool.

Trust boundary

matrix.normal_form.smith.compute@2 publishes output.value_refs.smith_form. matrix.normal_form.smith.verify@2 advertises a candidate: SmithNormalFormResult input port only because the producer exposes that exact whole-result type. The adapter resolves the reference, binds it to the candidate field, and performs the authoritative checker request parse once before independent Python-FLINT replay.

Focused coverage proves:

• the live MCP SDK still lists only math.find and math.run
• inspected producer/checker ports compose and create a bound verification record
• an attacker-created structurally valid but mathematically wrong Smith result is rejected with no record
• wrong-type, unknown, cross-runtime, unknown-port, and conflicting inline/reference inputs fail closed
• existing inline checker requests still work

Historical #1262 mechanism evidence

The original frozen manifest is preserved byte-for-byte at benchmarks/config/schema-bound-selection-v1.json (raw SHA-256 339e829dee7b1b3862ba6e102071e878d4939b944e140d415197a1dc0a9fccc3). These numbers remain useful evidence that host-visible capability schemas can help a weak model, but they do not validate the now-rejected extra-tool architecture.

Metric	Generic control	Old selected-tool treatment	Change
Contract satisfied	4/4	4/4	same
Verified cases	1	1	same
Correct abstentions	1	1	same
MCP calls	11	5	-54.5%
Tool/parameter errors	1/0	0/0	eliminated
Input tokens	279,433	150,477	-46.1%
Uncached input tokens	51,337	30,669	-40.3%
Output tokens	1,751	1,137	-35.1%
Model-visible MCP bytes	16,379	3,180	-80.6%
Elapsed seconds	173.76	127.12	-26.8%

Matched latest-main experiment

The new manifest is benchmarks/config/typed-checker-handoff-v1.json (raw SHA-256 25c7298bcbd34a3a99b648ed9b01b41d4e974eec98c867940ec09753c6d4719b). Control and treatment use the exact same four prompt bytes: scalar GCD, nested sparse polynomial GCD, Smith producer → checker, and a negative no-tool case. Both use Codex CLI 0.147.0, authenticated gpt-5.4-mini, low reasoning, direct MCP mode, fresh state, 337 capabilities, and policy digest sha256:805b4e007dfdb98641c2713d4b12be05bd5c5286c4f2a2d11db59be114de4cbc.

Metric	b0697425 control	Typed-ref treatment	Change
Contract satisfied	4/4	4/4	same
Verified cases	1	1	same
Correct abstentions	1	1	same
MCP calls	9	10	+11.1%
Tool/parameter errors	0/0	1/0	+1 tool error
Input tokens	230,494	243,947	+5.8%
Uncached input tokens	39,518	33,643	-14.9%
Output tokens	1,668	1,873	+12.3%
Model-visible MCP bytes	10,288	8,737	-15.1%
Elapsed seconds	141.14	168.37	+19.3%

The treatment trace carried the producer result as inputs.candidate.value_ref without repeating candidate in the payload and independently produced the requested exact-replay verification record. The control used the same producer and checker but retranscribed the whole candidate inline. Both were 4/4. Treatment reduced the typed-handoff bytes and uncached input, but one unrelated first producer call used an invalid bare matrix before retrying; this made aggregate calls, total tokens, and elapsed time worse. The result is retained rather than rerolled for favorable metrics.

Evidence hygiene: a preliminary treatment on the historical prompt was not counted because the model chose inline retranscription. Another treatment revealed ambiguous guidance by sending both a reference and an inline candidate; the fail-closed conflict led to the explicit generic instruction to omit port-bound fields from payload, after which the accepted treatment used the intended carrier. Source-mixed checker and loopback-proxy attempts were also excluded; both failure modes failed visibly. Final runs use checkout-local locked environments plus explicit loopback proxy bypass, and both reports record zero command failures.

Remaining #1031 scope

This fixes the highest-risk producer/checker retranscription slice exposed by #941 without claiming to close #1031.

Still open: the host-visible first call to math.run.payload remains generic for scalar and nested operations. Exact inspection returns the authoritative schema as data, and runtime Pydantic validation remains fail closed, but ordinary MCP host schema machinery still cannot constrain that first capability-specific payload. The fixed two-tool architecture intentionally rejects dynamic selected tools, bounded execution unions, and generic prepared handles; a complete #1031 solution therefore still needs a host-compatible design that preserves those constraints.

Now solved for declared typed composition: once a producer exposes a compatible whole-result output port and a consumer declares the matching input port, the model can carry the value without reconstructing its schema or wrapper. This PR enables that path for the Smith producer/checker pair; broader exact-checker coverage remains future domain-owned work.

Validation

Final head: 218441c99b30690f7879e91f473e00cc4f0ffbc6. The matched reports bind control to b06974258ed4e987aaab41d19619f28f95be81d4 and treatment to that final head.

• make test-domain TESTS=tests/domain/matrix/test_inline_exact_verification.py: 8 passed
• make test-mcp TESTS=tests/boundary/mcp/test_mcp_checker_value_references.py: 1 passed
• make test-composition TESTS=tests/composition/portfolio/test_portfolio_assembler.py: passed
• make test-plan BASE=origin/main: selected the full affected boundary
• make check-changed BASE=origin/main: 11/11 commands passed; 2,768 Python tests passed with three expected Lean skips, and 58 npm tests passed
• make check-static: Ruff/format, complexity, deptry, vulture, mypy (446 files), test architecture (411 files), six import contracts, test-plan projection, runtime inventory, product architecture (1,666 files), and package build passed

[morluto]

Architecture review against current main after #1256 and #1265: superseded as a product mechanism; preserve the experiment/evidence separately.

The evaluation is useful: the bounded direct schemas reduced calls, visible bytes, and parameter mistakes in this frozen suite. But the implementation now contradicts an explicit product boundary rather than filling an accidental gap. Current docs/reference/tools.md says Jacobian exposes exactly math.find and math.run, and explicitly accepts that the generic executor does not expose selected payloads as separate host-level tools. #1256 also removed alternate execution surfaces/prepared-handle-style machinery, and #1265 kept the public MCP surface exactly two tools while splitting local vs remote host ownership.

This PR changes that contract to “two by default” and adds 1–4 startup-selected operation tools. Even though bounded and protocol-compliant, that creates a second agent-facing execution surface whose schema, naming, registration, stale-contract checks, telemetry, docs, and local-only semantics all have to coexist with math.run. The new architecture is intentionally paying the generic-envelope cost to keep one execution model.

Recommendation: do not rebase this implementation for merge. If we want to retain the result, restack the benchmark/report as research evidence against #1031/#1218 and close this PR as superseded by the fixed two-tool architecture. A future reversal should be an explicit product-model decision with evidence that outweighs the permanent second surface, not an incremental exception.

[morluto]

Post-cutover disposition: retain; this is the acceptable replacement architecture

I re-reviewed the rewritten branch against #1256/#1265 and the current open backlog.

The old startup-selected MCP-tool design is gone. The surviving implementation now fits the intended ownership model:

• public MCP remains exactly math.find + math.run;
• the producer exposes an existing typed output port;
• the checker declares the matching typed candidate port;
• the runtime-local value reference is only a carrier, not evidence or checker authorization;
• authoritative Pydantic parsing and independent replay still occur at the checker boundary;
• inline candidates remain supported and wrong/cross-runtime/conflicting references fail closed.

The Smith slice is appropriately narrow and gives the materialized/inline checker backlog a reusable current pattern without introducing a registry, workflow, relationship graph, prepared handle, or alternate host surface. The matched evaluation is mixed, but product correctness does not depend on a behavioral-win claim.

Current head 218441c is mergeable and CI, Benchmarks, and Container Image are green. Rebase onto the latest one-commit-newer main only if GitHub requires it; do not redesign again.

Disposition: retain and land after normal review.

[morluto]

#1298 is the intended current-main replacement and now explicitly credits @kaoru0822-kitauji for the original work here. I’m leaving #1262 open for now because #1298 states that it supersedes this PR once green, and its current CI run still has a failing required CI workflow. Once #1298 is green, this older branch can be closed.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 8504c1db36

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Preserve canonical validation for typed checker requests

When any exact checker receives an inline payload, this marker makes _normalize_request bypass validate_payload, while _validated_inline_payloads calls coercive Pydantic directly and never canonicalizes or bounds the assembled request. For example, the Smith checker accepts candidate.rank: "2", normalizes it to an integer, and can return VERIFIED even though the advertised schema requires an integer; the canonical 10 MiB, nesting-depth, and float restrictions are also skipped. Canonicalize and bound the assembled payload after resolving the reference and before model_validate, as InstalledOperationAdapter does.

Useful? React with 👍 / 👎.