feat: executed Monte Carlo intervals with a witnessed denominator - #34
Open
HarperZ9 wants to merge 3 commits into
Open
feat: executed Monte Carlo intervals with a witnessed denominator#34HarperZ9 wants to merge 3 commits into
HarperZ9 wants to merge 3 commits into
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>
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.
The monte_carlo block's EXECUTED upgrade: the kernel prints sufficient-statistic columns (slack, successes, trials), and the VERIFIER computes the interval by the named method (normal-approx-95 with a boundary-proportion refusal, wilson-95 with its genuine asymmetry sealed as interval_low/high; clopper-pearson-95 honestly refused as unexecutable). Two-stage recompute: Stage A over the SEALED series refuses a tampered-and-resealed interval before any re-run (review live-probed it: 410 microseconds, rerun closure provably never fired); Stage B re-derives over the re-run stream (drift class MC_INTERVAL_DRIFT). Coherence rules make the counters mechanically provenance-checkable (integers below 2^53, trials stepping by one, successes non-decreasing in {0,1}), and the declared denominator becomes WITNESSED via trials_final == samples. Sealed does-not-prove additions: sample_independence, interval_coverage, estimator_semantics. DECLARED receipts stay valid forever and byte-identical (pinned). Ships the executed pi kernel pair (corpus 29/29), self-test case 10, and a fresh-verified count refresh of README/STATUS (suite 1683/0: lib 1001+3i, bin 179, cli 341, gpu 12, lexer 52, parser 98). Review PASS/PASS with every load-bearing commitment verified live; the single Minor is fixed in the tail commit.
(generated with Claude Code, https://claude.com/claude-code)