feat: buildc receipt verify arm for tool-call receipts - #36
Merged
Conversation
monte_carlo gains a two-arm DECLARED | EXECUTED status. Under the new
--mc-executed flag (opt-in; requires the full --mc-* declaration and
forces --columns to 3), the kernel prints a three-column row per
post-burn-in step, <invariant_scalar> <successes> <trials>, and receipt
verify RE-DERIVES the Wilson or normal-approx-95 interval from those
raw sufficient-statistic columns, entirely in verifier-owned code,
never from the kernel's own arithmetic.
The recompute runs twice. Stage A, over the sealed measurement series
before any re-run: a tampered-and-resealed interval is a pure data
contradiction, rejectable with no C compiler, so the self-test's
no-compiler property stays intact. Stage B, over the re-parsed re-run
series: a new failure class, MC_INTERVAL_DRIFT, for a receipt that
stays internally coherent while no longer describing the run it names.
Mutation-tested (Stage B skipped for EXECUTED receipts) to confirm it
is load-bearing, not redundant with Stage A.
The declared sample count becomes a WITNESSED denominator: the final
row's trials must equal monte_carlo.samples, the single biggest
honesty gain of the slice. Coherence is checked as a cumulative
Bernoulli count (integers below 2^53, trials incrementing by exactly
1, successes non-decreasing in {0, 1}, successes <= trials on every
row). Executable vocabulary v1: estimator proportion; interval methods
normal-approx-95 (refused at the boundary proportion, a zero-width
interval there overclaims precision) and wilson-95; clopper-pearson-95
is sealed-successes-only, not executable (needs a verified inverse
incomplete beta with no in-tree oracle), refused at emit and verify.
An EXECUTED block adds three not_claimed entries, present if and only
if the block is EXECUTED: sample_independence, interval_coverage,
estimator_semantics. EXECUTED hardens the interval arithmetic and the
denominator; it cannot and does not harden that the draws are
independent, that the named confidence level covers the true value, or
that the indicator counts what the author says it counts. This is
load-bearing honesty, not decoration: the receipt states in sealed
machine-readable form exactly which reading of an EXECUTED interval is
licensed.
Backward compatible: DECLARED receipts stay valid forever. The five
new fields are Option with skip_serializing_if; a DECLARED block's
serialized JSON carries exactly its original four keys, pinned by a
new test asserting the key set directly rather than assuming
skip_serializing_if behaves.
Shipped with: a new kernel pair, mc_pi_rejection_executed.bld and its
wrong-area negative fixture, same seed-42 stream as the DECLARED
sibling, calibration numbers measured by running the emitted receipt
(not invented): successes 1551 of 2000, estimate 0.7755, wilson-95
interval [0.7566951910008709, 0.7932485159471586]. The negative
fixture seals the slice's central lesson: the wrong-area factor only
scales the estimate, never the raw successes/trials counters, so the
interval executes and re-derives cleanly while the slack column still
blows the truth band. Corpus 27 -> 29. A tenth self-test case (nudge
the sealed interval_high on an EXECUTED block, reject through Stage A).
Nine new CLI tests covering the round trip and every emit-refusal path.
Docs (SCIENTIFIC-RECEIPT flags/schema/family/failure-classes/self-test/
corpus, CHANGELOG) and the plan/design docs in the writing-plans idiom.
Verified: full suite 1,644 passed / 0 failed (up from a 1,605 pre-slice
baseline measured at the start of final verification), exit codes
captured before any pipe; corpus 29/29, run twice for determinism;
self-test 10/10; cargo fmt --check clean. Every new gate
mutation-tested by literal inverse edit, never git checkout: sixteen
gates broken, observed red, restored, observed green, including one
mutation (a sign flip inside the Wilson formula's square root) that
only the hand-computed-value unit test catches, and one (the Stage B
skip) that proves Stage B is not redundant with Stage A.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…eline Pure count refresh, re-verified fresh on this branch rather than trusting slice-authoring-time numbers (the units slice merged to main after the executed-intervals slice was authored, so the rebased totals differ from both slices' own reports): cargo test 1683 passed, 0 failed, 11 ignored (lib 1004 with 1001 passed and 3 ignored, bin 179, cli 341, gpu 12, lexer 52, parser 98); buildc receipt corpus 29/29; verifier --self-test 10/10 on a freshly emitted executed-interval receipt; buildc corpus verify 8/8. The STATUS baseline enumeration also gains the wave's three newest members (executed intervals, drop flags, unit-annotated types) so the rise it explains matches what produced it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The review's one finding: MC_INTERVAL_CLOPPER_PEARSON_95 was used only in tests, tripping dead_code. The arm that refuses the method now formats its message through the constant, making it the single source of the name. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Design: docs/superpowers/specs/2026-07-29-model-boundary-receipts-design.md
Emission is harness-side (harness/model_shim.py's --receipt-dir flag, the
local-model / _wshim repo); this commit ships buildc's read side only.
- New docs/MODEL-RECEIPT.md: the buildlang-model-boundary-receipt/v0 schema
contract (field table, SHIM-WITNESSED vs DECLARED tags, the seal and
cross-language canonicalization contract). docs/SCIENTIFIC-RECEIPT.md
gains a pointer section; the scientific verifier's CAPABILITY_INADMISSIBLE
refusal of any Model-observing program is untouched.
- New compiler/src/model_receipt.rs: the fourth receipt verify arm (beside
gpu, scientific-runtime, and check), wired into both the plain and --json
`receipt verify` dispatch. Offline only (no re-run): seal recompute
(SEAL_MISMATCH), digest well-formedness (DIGEST_MALFORMED), and the three
named field-shape contracts (FIELD_CONTRACT_VIOLATION) -- no new failure
classes, the shared taxonomy is reused whole.
- compiler/src/main.rs: cmd_receipt_chain_build's member-schema gate widens
from a single-schema equality to a two-schema allowlist
(scientific-runtime + model-boundary-receipt). Chain verify needed zero
changes: pinned seals and subprocess re-verification already dispatch
through the new arm.
- compiler/tests/fixtures/model-receipt-golden.json: the byte-identical
golden fixture (echo-mode COMPLETED receipt) both repos pin, seal
6bb2a09c47f5eaa2e3208a5eadcd6d57d1faffa74a567e024e920571c3794035. The
no-floats schema is what makes serde_json::to_vec and Python's
json.dumps(..., separators=(",", ":"), ensure_ascii=False) agree
byte-for-byte.
- Tamper coverage (unit tests in model_receipt.rs, CLI tests in cli.rs
against the real buildc binary): a resealed field-shape violation, a seal
mismatch, and a propose/dispose chain (a model receipt beside a
Model-free disposer kernel's scientific receipt) that breaks with
CHAIN_LINK_UNVERIFIED when only the model member is tampered.
- The model receipt is not a corpus member and not a --self-test case (a
different artifact kind, not scientific evidence): corpus 29/29 and
self-test 10/10 stay unchanged, re-run and recorded. Full suite: 1,698
passed, 0 failed (+15 over the prior 1,683 baseline); cargo fmt clean.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…po byte pin The review's one Important: local-model pins the shared golden fixture eol=lf but buildlang had no .gitattributes at all, so a fresh Windows clone with autocrlf would smudge the fixture bytes. No current test breaks (verify recomputes seals from the parsed struct, proven empirically in review), but the cross-repo byte-identity provenance claim depends on the bytes, so both repos now pin it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adds the Rust verify/read side for flywheel.tool-call-receipt/v1, the schema emitted by local-model's ToolExecutor when receipt_dir is set. Mirrors model_receipt.rs in structure: struct declaration order is the canonical sealed order, seal recompute blanks seal.hex, verify checks SEAL_MISMATCH first then DIGEST_MALFORMED then FIELD_CONTRACT_VIOLATION. The golden fixture (tool-receipt-golden.json) is produced by the Python emit side and pinned with the same seal in both repos — the cross-language canonicalization contract. The Rust test golden_fixture_reseals_to_its_ pinned_seal hard-codes the pinned hex, proving serde_json::to_vec and Python json.dumps agree byte-for-byte. Dispatch: new schema arm in both receipt verify paths (json + non-json), chain allowlist widened to admit tool-call receipts beside scientific and model-boundary receipts. 6 Rust tests pass (including golden).
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
1 participant
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.
Rust verify/read side for flywheel.tool-call-receipt/v1. Mirrors model_receipt.rs: fixed-order seal, shared failure taxonomy, golden fixture pinned in both repos proving the cross-language canonicalization contract. Chain allowlist widened.