diff --git a/CHANGELOG.md b/CHANGELOG.md index 36e2ee53..302fe4da 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,32 @@ tracked in `STATUS.md`, `README.md`, and ## Unreleased +- **Executed Monte Carlo intervals with a witnessed denominator**: `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 + (` `), and `receipt verify` + RE-DERIVES the Wilson or normal-approx-95 interval from those raw + sufficient-statistic columns, entirely in verifier-owned code, at two + stages: Stage A over the sealed series before any re-run (a + tampered-and-resealed interval is a pure data contradiction, rejectable + with no C compiler), and Stage B over the 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). The declared sample count + becomes a WITNESSED denominator: the final row's `trials` must equal + `monte_carlo.samples`. 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`). An EXECUTED block adds + three `not_claimed` entries -- `sample_independence`, `interval_coverage`, + `estimator_semantics` -- present if and only if the block is EXECUTED: + EXECUTED hardens the interval arithmetic and the denominator, never the + estimator's semantics or independence. Backward compatible: `DECLARED` + receipts stay valid forever, the five new fields are `Option` with + `skip_serializing_if`, and a receipt sealed before this slice re-serializes + to its exact bytes (pinned by test). New kernel pair + `examples/mc_pi_rejection_executed.bld` / + `examples/mc_pi_rejection_executed_broken.bld`; corpus 29/29; self-test + 10/10; full suite 1,644 passed, 0 failed. - **Split-frontier drop flags (memory pillar increment 5, opt-in)**: behind the same `BUILDLANG_EXPERIMENTAL_FREE` flag (default off, flag-off output byte-identical, verified mechanically), the C backend now reclaims heap diff --git a/README.md b/README.md index 5487e103..2fb18367 100644 --- a/README.md +++ b/README.md @@ -257,8 +257,8 @@ output, and the receipt tooling are the verified core; SPIR-V, LLVM IR, WASM, Rust, x86-64, ARM64, GPU dispatch, and `#[linear]` types are labeled experimental and stay that way until their evidence says otherwise. The release-shaped baseline (2026-07-29, local `cargo test` from `compiler/`): -1605 tests passing, 0 failing (11 ignored), with `buildc receipt corpus` -27/27 and `buildc corpus verify` 8/8. Ground-truth release evidence lives in +1683 tests passing, 0 failing (11 ignored), with `buildc receipt corpus` +29/29 and `buildc corpus verify` 8/8. Ground-truth release evidence lives in [STATUS.md](STATUS.md); [CHANGELOG.md](CHANGELOG.md) tracks changes. ## Documentation and ecosystem diff --git a/STATUS.md b/STATUS.md index 76d013f8..101045df 100644 --- a/STATUS.md +++ b/STATUS.md @@ -57,9 +57,9 @@ Last audited: 2026-07-01 (wind-down point); broader status audit remains 2026-06 > receipt per computation mode (deterministic, exact-probabilistic, seeded > stochastic, Monte Carlo, budgeted heuristic, plus the cross-backend bonus) > into one ordered, tamper-evident bundle via `receipt chain`. Current -> baseline: 1605 tests passing, 0 failing, 11 ignored; the example corpus -> (`examples/scientific-corpus.json`) is 27/27; the verifier `--self-test` is -> 9/9. +> baseline: 1683 tests passing, 0 failing, 11 ignored; the example corpus +> (`examples/scientific-corpus.json`) is 29/29; the verifier `--self-test` is +> 10/10. ## Identity The Effects Language -- algebraic effects as a first-class feature. @@ -80,7 +80,7 @@ The Effects Language -- algebraic effects as a first-class feature. - **Macro expansion**: Builtin macros, pattern matching, hygiene. Unit tests present. - **Interprocedural Lifetime Analysis** (Phase 1): Lifetime parameters flow through `FnTy` (function types), enabling precise borrow tracking at call sites. Functions like `fn pick<'a, 'b>(x: &'a i32, y: &'b i32) -> &'a i32` correctly propagate only the `'a`-linked borrow. Return lifetime mismatches (returning `'b` where `'a` expected) are rejected with clear errors. 8 new unit tests, 3 integration test programs. - **Current CI-shaped cargo baseline (2026-07-02, invariant family complete)**: lib 940, bin 140, cli 309, lexer 52, parser 88 (0 failed; 3 lib + 8 doc-test ignored) via `cargo test` from `compiler/`; `cargo fmt --check` clean; corpus 8/8. The rise from the `939/81/301` wind-down baseline is Phases A/B/C/D1-D3 of the Telos master-plan mandate: the receipt export bridge, the capability-witnessed receipt fields, and the seven-member invariant family (conservation, bounded, energy-identity, relation, conserved-band, non-negative) with their paired kernels and multi-column capture. (Prior 2026-06-23 baseline was 1002 passed / 0 failed / 11 ignored under a different aggregation.) -- **Current CI-shaped cargo baseline (2026-07-29, five-modes wave complete)**: lib 968 (965 passed, 3 ignored), bin 158, cli 330, gpu 12, lexer 52, parser 88 -- 1605 passed, 0 failed, 11 ignored total, via `cargo test` from `compiler/`; `cargo fmt --check` clean; `buildc receipt corpus examples/scientific-corpus.json` 27/27; verifier `--self-test` 9/9; `buildc corpus verify` (the 8-program semantic corpus, a separate C-backend regression check) stays 8/8. The rise from the 2026-07-02 `940/140/309/52/88` baseline above is the five-modes wave (2026-07-28 to 2026-07-29): the `Random` capability with witnessed-seed receipts, Monte Carlo estimator receipts, budgeted-search receipts, the `Model` capability's propose/dispose refusal, cross-backend relation receipts through the Rust backend (the invariant family's eighth member), and wall-clock metering (`runtime_state.wall_seconds`, the receipt's first EXECUTED budget fact). Detail: `docs/FIVE-MODES-TOUR.md`. +- **Current CI-shaped cargo baseline (2026-07-29, five-modes wave complete)**: lib 1004 (1001 passed, 3 ignored), bin 179, cli 341, gpu 12, lexer 52, parser 98 -- 1683 passed, 0 failed, 11 ignored total, via `cargo test` from `compiler/`; `cargo fmt --check` clean; `buildc receipt corpus examples/scientific-corpus.json` 29/29; verifier `--self-test` 10/10; `buildc corpus verify` (the 8-program semantic corpus, a separate C-backend regression check) stays 8/8. The rise from the 2026-07-02 `940/140/309/52/88` baseline above is the five-modes wave (2026-07-28 to 2026-07-29): the `Random` capability with witnessed-seed receipts, Monte Carlo estimator receipts, budgeted-search receipts, the `Model` capability's propose/dispose refusal, cross-backend relation receipts through the Rust backend (the invariant family's eighth member), wall-clock metering (`runtime_state.wall_seconds`, the receipt's first EXECUTED budget fact), executed Monte Carlo intervals with a witnessed denominator (the `monte_carlo` block's EXECUTED status), split-frontier drop flags (memory pillar increment 5, opt-in), and unit-annotated numeric types (checker slice one, experimental). Detail: `docs/FIVE-MODES-TOUR.md`. - **Linear types `#[linear]` (2026-07-01, experimental — best-effort LINT, not a proven-sound checker):** opt-in no-cloning. A `#[linear]` struct/enum value is tracked as a resource that should be moved/consumed at most once -- the shared foundation for quantum qubit no-cloning, on-chain no-double-spend, and fin-sec resource-handle safety. Now enforced by **two layers**: the conservative AST gate (sound-over-complete name tracking + containment rule) AND a new **MIR affine/borrow checker** (`codegen/analysis/linear.rs`, built on the reusable `codegen::analysis` dataflow substrate) that runs post-lowering and closes the classes the name tracker cannot follow -- move-out-of-shared-borrow (incl. laundered through aggregates/returns and higher-order fn-pointers), field-extract from an owned linear aggregate, generic deref-and-return, and struct/enum record-pattern-through-`&`. Verified by repeated empirical adversarial sweeps (`buildc check` on constructed clones, confirmed with `buildc run`). **Not yet fully sound (do NOT claim a soundness guarantee):** known residual = `&mut`-match payload move + un-enumerated advanced corners; a complete affine checker is a deliberate multi-brick effort (cf. Rust's borrow checker). Honest scope: `docs/LINEAR-TYPES.md`. Ordinary types are unaffected (copy-like reuse preserved). - **Multiple dispatch (2026-07-01, static):** Julia-style — multiple functions may share one name, and a call selects the method by the tuple of ALL argument types (not just the receiver), resolved statically via one shared resolver (`types/dispatch.rs`) used by both the checker and codegen. Specificity: exact > coercion/concrete > generic; ambiguity and no-match are ERRORS (never a silent pick). Generic and concrete defs of a name compose (concrete wins when it matches, else the generic monomorphizes). Backward-compatible: only overloaded (2+ def) names are mangled, so single-def names and `extern "C"` FFI are byte-identical (verified by a 22/22 differential C sweep). Deferred: operator overloading on both operands (still left-operand-only), and dynamic runtime-type dispatch (no runtime type descriptors yet). Details: `docs/MULTIPLE-DISPATCH.md`. - **Math syntax (2026-07-01, Pillar B):** four additive, backward-compatible features (each verified by a differential C sweep showing existing programs unchanged). (1) **Broadcasting operators `.+ .- .* ./`** over fixed-size `Array` (the type of an array literal `[..]`), including scalar broadcast in both directions; length agreement is a COMPILE-TIME check carried in the `Array` type (no runtime dimension check), and codegen desugars each operator into an unrolled array of per-element SCALAR MIR ops, so the broadcast ops never reach any backend. (2) **`linalg` stdlib module** (`stdlib/linalg.bld`): free functions `vec_add/sub/mul/div`, `vec_scale`, `vec_scalar_add`, `vec_dot`, `vec_sum`, `vec_norm` over the dynamic `Vec`, no compiler/runtime change. (3) **`**` power** wired to the pre-existing `BinOp::Pow` (right-associative, `-2 ** 2 == -4`; prefix `**x` stays double-deref, so no pointer code changes). (4) **Unicode operator aliases** `× · ∙ -> *`, `÷ -> /`, `− -> -`. Honest scope: this is elementwise broadcasting over FIXED-SIZE arrays plus a 1-D vector library over DYNAMIC `Vec` (two distinct surfaces: operators work on array literals, the library on `Vec`; a `Vec` cannot yet use `.+`), NOT Julia-parity linear algebra. Deferred: dynamic-`Vec` broadcasting operators, a true 2-D `Matrix{T}` with linear algebra (no N-D MIR type exists), `f32` element parity, and broadcast comparisons/`.^`. Details: `docs/MATH-SYNTAX.md`. @@ -179,4 +179,4 @@ package API completion. LSP readiness is tracked separately through the checked `buildlang-lsp-dispatch-receipt/v0` artifact and still excludes end-to-end VS Code extension verification. -BuildLang has a **working compiler core** (lexer -> parser -> type checker -> MIR -> C backend -> executable) with a current local baseline (2026-07-29) of 1605 tests passed, 0 failed (11 ignored) via `cargo test --quiet` from `compiler/` (per-target splits live in the dated baseline entries above). It can compile and run real programs with variables, functions, control flow, pattern matching, recursion, and algebraic effects. C, LLVM, x86-64, ARM64, WASM, SPIR-V, HLSL, GLSL, and Rust are accessible from the CLI via `buildc build --target `, but with different maturity levels. The C backend is production-verified and now has a semantic-corpus C execution receipt matching the current 8-program corpus; `buildc run` uses per-run temp build directories so concurrent C receipt probes avoid shared temp C/PDB collisions; `buildc corpus verify` validates the semantic corpus manifest, C/Rust receipts, and real C-backend stdout, accepts explicit corpus roots, and can refresh the C receipt for copied corpus fixtures after C stdout passes. The same corpus path now carries a `buildlang-substrate-receipt/v0` aggregation receipt that checks source-set size, backend maturity, memory gaps, representation fallback policy, and evidence commands without promoting experimental backends. Its representation surface is now backed by a checked `buildlang-mir-representation-receipt/v0` artifact that recomputes per-program MIR operation families, symbols, memory-surface flags, and control-flow summaries during `buildc corpus verify`. The same verification path now also checks a `buildlang-memory-layout-receipt/v0` artifact that binds the corpus memory surface to manifest tags, MIR-derived memory flags, ownership/layout classification, digest evidence, and explicit known gaps without claiming byte-level ABI layout or full borrow proof. `buildc receipt verify` re-checks saved source-bound check receipts against current source inputs, policy/profile digests, replayed effect/accountability surfaces, optional required built-in profile identity, and optional required policy digest, with optional JSON verification reports for CI; check policies now validate referenced effect names against built-in capabilities and the checked source graph so misspelled gates fail instead of silently weakening enforcement, can require `allowed_effects` to be authoritative even when empty, can require explicit direct/propagated provenance allowlists, can constrain direct capability boundaries to exact ambient helper/macro/FFI sources, can classify compile-time ambient macros such as `include_str!` and `env!` under `FileSystem`/`Environment`, can scan macro argument token trees with `SourceId` provenance so `println!(read_file(...))` requires both `Console` and `FileSystem` in entry sources and external module files and unknown extern calls/statics surface as `Foreign`, can classify known effectful `build_*` C runtime helper aliases declared in extern blocks under their real domain capability instead of generic `Foreign`, can preserve qualified ambient helper paths such as `io::read_file` in diagnostics, receipts, and scaffolded source allowlists, can reject effectful callbacks passed into pure `fn(...)` boundaries instead of erasing effect rows, and can preserve delayed or propagated capability evidence across callbacks, closures, aggregates, async awaits, branches, loops, casts, refs/derefs, pipes, assignments, selected aggregate fields, returned functions, and exact source allowlists. The built-in `strict-accountability` policy profile packages required effect inventory, digest, provenance, source, and coverage requirements into a named adoption gate for teams that want no ambient IO without exact allowlists, and `buildc policy scaffold` can turn observed receipt evidence into an exact strict policy skeleton for review while preserving pure receipts against later effect drift. `buildc doctor` reports local toolchain, stdlib, registry, optional backend tools, and backend maturity for adoption diagnostics; tested quickstart examples cover first-run CPU execution, mutable control flow, algebraic effects, and HLSL shader output; the Rust backend is subset-validated with `rustc --emit=metadata` and has a narrower generated-executable stdout smoke layer over the same semantic corpus plus manifest contract/receipt consistency/metadata guards; LLVM can optionally link with clang; native/WASM backends output assembly/binary for external toolchain linking. Formatter and package-manager entry points (`buildc fmt`, `buildc pkg`) are wired into the CLI, but the package manager has no live registry. `buildc lsp` starts the current stdio server loop, dispatches the checked raw LSP receipt sequence through structural JSON-RPC parsing, emits compiler-backed diagnostics, and returns receipt-verified semantic tokens v0 plus opened-document workspace symbols; full compiler-backed semantic token indexing, global workspace-symbol indexing, and end-to-end VS Code extension verification remain open. The self-hosted compiler and standard library (244,085 lines of `.bld` code) represent an ambitious long-term vision but cannot be compiled or executed today. +BuildLang has a **working compiler core** (lexer -> parser -> type checker -> MIR -> C backend -> executable) with a current local baseline (2026-07-29) of 1683 tests passed, 0 failed (11 ignored) via `cargo test --quiet` from `compiler/` (per-target splits live in the dated baseline entries above). It can compile and run real programs with variables, functions, control flow, pattern matching, recursion, and algebraic effects. C, LLVM, x86-64, ARM64, WASM, SPIR-V, HLSL, GLSL, and Rust are accessible from the CLI via `buildc build --target `, but with different maturity levels. The C backend is production-verified and now has a semantic-corpus C execution receipt matching the current 8-program corpus; `buildc run` uses per-run temp build directories so concurrent C receipt probes avoid shared temp C/PDB collisions; `buildc corpus verify` validates the semantic corpus manifest, C/Rust receipts, and real C-backend stdout, accepts explicit corpus roots, and can refresh the C receipt for copied corpus fixtures after C stdout passes. The same corpus path now carries a `buildlang-substrate-receipt/v0` aggregation receipt that checks source-set size, backend maturity, memory gaps, representation fallback policy, and evidence commands without promoting experimental backends. Its representation surface is now backed by a checked `buildlang-mir-representation-receipt/v0` artifact that recomputes per-program MIR operation families, symbols, memory-surface flags, and control-flow summaries during `buildc corpus verify`. The same verification path now also checks a `buildlang-memory-layout-receipt/v0` artifact that binds the corpus memory surface to manifest tags, MIR-derived memory flags, ownership/layout classification, digest evidence, and explicit known gaps without claiming byte-level ABI layout or full borrow proof. `buildc receipt verify` re-checks saved source-bound check receipts against current source inputs, policy/profile digests, replayed effect/accountability surfaces, optional required built-in profile identity, and optional required policy digest, with optional JSON verification reports for CI; check policies now validate referenced effect names against built-in capabilities and the checked source graph so misspelled gates fail instead of silently weakening enforcement, can require `allowed_effects` to be authoritative even when empty, can require explicit direct/propagated provenance allowlists, can constrain direct capability boundaries to exact ambient helper/macro/FFI sources, can classify compile-time ambient macros such as `include_str!` and `env!` under `FileSystem`/`Environment`, can scan macro argument token trees with `SourceId` provenance so `println!(read_file(...))` requires both `Console` and `FileSystem` in entry sources and external module files and unknown extern calls/statics surface as `Foreign`, can classify known effectful `build_*` C runtime helper aliases declared in extern blocks under their real domain capability instead of generic `Foreign`, can preserve qualified ambient helper paths such as `io::read_file` in diagnostics, receipts, and scaffolded source allowlists, can reject effectful callbacks passed into pure `fn(...)` boundaries instead of erasing effect rows, and can preserve delayed or propagated capability evidence across callbacks, closures, aggregates, async awaits, branches, loops, casts, refs/derefs, pipes, assignments, selected aggregate fields, returned functions, and exact source allowlists. The built-in `strict-accountability` policy profile packages required effect inventory, digest, provenance, source, and coverage requirements into a named adoption gate for teams that want no ambient IO without exact allowlists, and `buildc policy scaffold` can turn observed receipt evidence into an exact strict policy skeleton for review while preserving pure receipts against later effect drift. `buildc doctor` reports local toolchain, stdlib, registry, optional backend tools, and backend maturity for adoption diagnostics; tested quickstart examples cover first-run CPU execution, mutable control flow, algebraic effects, and HLSL shader output; the Rust backend is subset-validated with `rustc --emit=metadata` and has a narrower generated-executable stdout smoke layer over the same semantic corpus plus manifest contract/receipt consistency/metadata guards; LLVM can optionally link with clang; native/WASM backends output assembly/binary for external toolchain linking. Formatter and package-manager entry points (`buildc fmt`, `buildc pkg`) are wired into the CLI, but the package manager has no live registry. `buildc lsp` starts the current stdio server loop, dispatches the checked raw LSP receipt sequence through structural JSON-RPC parsing, emits compiler-backed diagnostics, and returns receipt-verified semantic tokens v0 plus opened-document workspace symbols; full compiler-backed semantic token indexing, global workspace-symbol indexing, and end-to-end VS Code extension verification remain open. The self-hosted compiler and standard library (244,085 lines of `.bld` code) represent an ambitious long-term vision but cannot be compiled or executed today. diff --git a/compiler/src/main.rs b/compiler/src/main.rs index c2a83c1c..a430afae 100644 --- a/compiler/src/main.rs +++ b/compiler/src/main.rs @@ -49,13 +49,14 @@ use scientific_runtime::{ }; use scientific_runtime::{ build_scientific_runtime_receipt, build_self_test_cases, column_count_matches_invariant, - crucible_measurement_from_report, evaluate_scientific_runtime_receipt, parse_numeric_series, - verify_scientific_runtime_receipt, RederivedFacts, RerunObservation, ScientificBudget, - ScientificCrossBackend, ScientificDigest, ScientificEffectPolicy, ScientificMonteCarlo, - ScientificReceiptInputs, ScientificRuntimeReceipt, ScientificToolchain, SecondaryObservation, - BOUNDED_INVARIANT, CONSERVATION_INVARIANT, CONSERVED_BAND_INVARIANT, CROSS_BACKEND_INVARIANT, - CRUCIBLE_MEASUREMENT_EXPORT_SCHEMA, ENERGY_IDENTITY_INVARIANT, ENERGY_MONOTONE_INVARIANT, - NON_NEGATIVE_INVARIANT, RELATION_INVARIANT, SCIENTIFIC_RUNTIME_SCHEMA, + compute_mc_executed, crucible_measurement_from_report, evaluate_scientific_runtime_receipt, + parse_numeric_series, verify_scientific_runtime_receipt, RederivedFacts, RerunObservation, + ScientificBudget, ScientificCrossBackend, ScientificDigest, ScientificEffectPolicy, + ScientificMonteCarlo, ScientificReceiptInputs, ScientificRuntimeReceipt, ScientificToolchain, + SecondaryObservation, BOUNDED_INVARIANT, CONSERVATION_INVARIANT, CONSERVED_BAND_INVARIANT, + CROSS_BACKEND_INVARIANT, CRUCIBLE_MEASUREMENT_EXPORT_SCHEMA, ENERGY_IDENTITY_INVARIANT, + ENERGY_MONOTONE_INVARIANT, MC_EXECUTED_ESTIMATOR_PROPORTION, NON_NEGATIVE_INVARIANT, + RELATION_INVARIANT, SCIENTIFIC_RUNTIME_SCHEMA, }; use symbol_graph::{verify_symbol_graph_receipt, SymbolGraphReceipt, SYMBOL_GRAPH_RECEIPT}; @@ -271,6 +272,15 @@ enum Commands { #[arg(long, value_name = "METHOD")] mc_interval: Option, + /// Declare the Monte Carlo run EXECUTED: the verifier re-derives the + /// interval from raw sufficient-statistic columns the kernel prints + /// (successes/trials counters beside the invariant scalar) instead of + /// trusting the declaration. Requires all three --mc-* flags together; + /// forces --columns to 3 (an unset default is silently upgraded, any + /// other explicit value is refused, the --cross-backend idiom). + #[arg(long)] + mc_executed: bool, + /// Declare the run a budgeted search: the step ceiling. Both /// --budget-* flags declare together or not at all. A budgeted /// receipt carries NOT_PROVES_OPTIMALITY and refuses free text @@ -673,6 +683,7 @@ fn main() -> ExitCode { mc_estimator, mc_samples, mc_interval, + mc_executed, budget_steps, budget_consumed, budget_wall_seconds, @@ -686,7 +697,11 @@ fn main() -> ExitCode { "--seed is not supported with --gpu (the GPU cross-check has no Random capability)" ); Err(1) - } else if mc_estimator.is_some() || mc_samples.is_some() || mc_interval.is_some() { + } else if mc_estimator.is_some() + || mc_samples.is_some() + || mc_interval.is_some() + || mc_executed + { eprintln!( "--mc-* flags are not supported with --gpu (the GPU cross-check has no Random capability)" ); @@ -723,6 +738,7 @@ fn main() -> ExitCode { mc_estimator.as_deref(), mc_samples, mc_interval.as_deref(), + mc_executed, budget_steps, budget_consumed, budget_wall_seconds, @@ -2079,6 +2095,9 @@ fn cmd_receipt_corpus(manifest_path: &Path) -> Result<(), i32> { if let Some(interval) = &member.mc_interval { emit.args(["--mc-interval", interval]); } + if member.mc_executed { + emit.arg("--mc-executed"); + } if let Some(steps) = member.budget_steps { emit.args(["--budget-steps", &steps.to_string()]); } @@ -7483,6 +7502,7 @@ fn cmd_run( mc_estimator: Option<&str>, mc_samples: Option, mc_interval: Option<&str>, + mc_executed: bool, budget_steps: Option, budget_consumed: Option, budget_wall_seconds: Option, @@ -7516,11 +7536,20 @@ fn cmd_run( ); return Err(1); } + // Only the DECLARED shape can be built here: whether the block + // is EXECUTED-and-coherent is unknown until the real series + // exists. The finalization below (after capture) upgrades this + // to EXECUTED when --mc-executed was passed, fail closed. Some(ScientificMonteCarlo { estimator: estimator.to_string(), samples, interval_method: interval_method.to_string(), status: "DECLARED".to_string(), + estimate: None, + interval_low: None, + interval_high: None, + n_effective: None, + successes: None, }) } _ => { @@ -7530,6 +7559,25 @@ fn cmd_run( return Err(1); } }; + // --mc-executed requires the full declaration (all three --mc-* flags), + // and its estimator must be in the v1 executable vocabulary (`proportion`); + // DECLARED blocks may still use free text. The interval-method vocabulary + // check is NOT duplicated here: it is fail-closed inside + // `compute_mc_executed`, called once real data exists, below. + if mc_executed && mc_flag_count < 3 { + eprintln!( + "Error: --mc-executed requires the full Monte Carlo declaration (--mc-estimator, --mc-samples, --mc-interval)" + ); + return Err(1); + } + if let Some(estimator) = mc_estimator { + if mc_executed && estimator != MC_EXECUTED_ESTIMATOR_PROPORTION { + eprintln!( + "Error: --mc-executed requires --mc-estimator proportion (v1 executable vocabulary); DECLARED blocks may still use free text" + ); + return Err(1); + } + } // The budgeted-search declaration is all-or-nothing, exactly like the MC // declaration: a result without its budget ceiling hides whether it // stopped at the limit, so neither flag alone is accepted. Deterministic @@ -7642,10 +7690,14 @@ fn cmd_run( // `--invariant cross-backend` defines its own column structure (2: the C // anchor and the secondary lane), so an unset `--columns` (the CLI - // default, 1) is silently upgraded; anything else is left for the - // existing column-count gate below to refuse. + // default, 1) is silently upgraded; `--mc-executed` similarly forces 3 + // (the invariant scalar plus the witnessed successes/trials counters); + // anything else is left for the existing column-count gate below to + // refuse. let columns = if invariant_name == CROSS_BACKEND_INVARIANT && columns == 1 { 2 + } else if mc_executed && columns == 1 { + 3 } else { columns }; @@ -7655,7 +7707,9 @@ fn cmd_run( // so the two can never drift: the `relation` invariant reads across columns // and needs at least two; every single-scalar invariant reads one value per // step and rejects a multi-column request rather than silently ignoring it. - if emit_receipt.is_some() && !column_count_matches_invariant(invariant_name, columns) { + if emit_receipt.is_some() + && !column_count_matches_invariant(invariant_name, columns, mc_executed) + { if invariant_name == RELATION_INVARIANT { eprintln!( "--invariant relation needs --columns >= 2 (each row must hold the columns to compare)" @@ -7664,6 +7718,10 @@ fn cmd_run( eprintln!( "--invariant cross-backend needs --columns 2 (the C anchor and the secondary lane); the invariant defines its own column structure" ); + } else if mc_executed { + eprintln!( + "--mc-executed needs --columns 3 (the invariant scalar plus the witnessed successes/trials counters); the invariant defines its own column structure" + ); } else { eprintln!( "--columns {columns} is only valid with --invariant relation; the single-scalar invariants read one value per step" @@ -7740,6 +7798,9 @@ fn cmd_run( ); return Err(1); } + // This transitively refuses --cross-backend --mc-executed too: + // --mc-executed requires mc_flag_count == 3 (checked above), which + // this arm already refuses whenever any mc flag is present. if mc_flag_count > 0 { eprintln!( "--cross-backend does not support --mc-* (Monte Carlo requires the Random capability, which --cross-backend already refuses)" @@ -7929,6 +7990,33 @@ fn cmd_run( (primary_series, columns, None) }; + // --mc-executed finalization: the early `monte_carlo` block could only + // build the DECLARED shape (whether it is EXECUTED-and-coherent was + // unknown until the real series existed). Recompute now, fail closed: + // an incoherent EXECUTED block never reaches + // `build_scientific_runtime_receipt` (never gets sealed). + let monte_carlo = if mc_executed { + let mc = monte_carlo.expect("mc_executed implies mc_flag_count == 3, checked above"); + let computed = compute_mc_executed(&series, column_count, mc.samples, &mc.interval_method) + .map_err(|reason| { + eprintln!( + "Error: --mc-executed refuses to seal an incoherent EXECUTED block: {reason}" + ); + 1i32 + })?; + Some(ScientificMonteCarlo { + status: "EXECUTED".to_string(), + estimate: Some(computed.estimate), + interval_low: Some(computed.interval_low), + interval_high: Some(computed.interval_high), + n_effective: Some(computed.n_effective), + successes: Some(computed.successes), + ..mc + }) + } else { + monte_carlo + }; + let os = std::env::consts::OS.to_string(); let mut flags = vec![format!("invariant={invariant}"), format!("metric={metric}")]; if negative_fixture { diff --git a/compiler/src/scientific_runtime.rs b/compiler/src/scientific_runtime.rs index e1b6a758..2e24876b 100644 --- a/compiler/src/scientific_runtime.rs +++ b/compiler/src/scientific_runtime.rs @@ -140,6 +140,49 @@ pub const CROSS_BACKEND_INVARIANT: &str = "cross_backend_columns_agree"; /// tolerance it is absolute: cross-backend kernels must emit O(1) values. pub const CROSS_BACKEND_TOLERANCE: f64 = 1e-5; +/// Executed Monte Carlo estimator vocabulary, v1: the mean of Bernoulli +/// indicators. DECLARED blocks keep free text forever (the shipped corpus +/// uses `mean`); this vocabulary gates EXECUTED blocks only. +pub const MC_EXECUTED_ESTIMATOR_PROPORTION: &str = "proportion"; + +/// Executed interval method: normal approximation. Degenerate at a boundary +/// proportion (successes == 0 or successes == trials): refused at emit and +/// at verify, pointing at `wilson-95`. +pub const MC_INTERVAL_NORMAL_APPROX_95: &str = "normal-approx-95"; + +/// Executed interval method: Wilson score. Well-defined at the boundary +/// proportions, asymmetric by construction. +pub const MC_INTERVAL_WILSON_95: &str = "wilson-95"; + +/// NOT executable in v1 (needs an inverse incomplete beta with no in-tree +/// oracle). Named here only so refusal messages can point at it by +/// constant rather than a bare string; never accepted by +/// `compute_mc_executed`. +pub const MC_INTERVAL_CLOPPER_PEARSON_95: &str = "clopper-pearson-95"; + +/// z for a two-sided 95% normal/Wilson interval: the double nearest the +/// 0.975 standard-normal quantile. Shared by both executable methods. +pub const MC_INTERVAL_Z_95: f64 = 1.959963984540054; + +/// Absolute float tolerance for the emit/verify interval recompute +/// (`estimate`, `interval_low`, `interval_high`, both stages). The +/// arithmetic runs on identical integer inputs through one fixed Rust +/// implementation at emit and verify, so agreement should be exact in +/// practice; this is headroom against a future compiler reassociating +/// verifier-side float ops, not load-bearing looseness. Values are O(1) +/// proportions, so absolute is safe. +pub const MC_RECOMPUTE_TOLERANCE: f64 = 1e-12; + +/// The three `not_claimed` entries an EXECUTED monte_carlo block adds, +/// present iff `status == "EXECUTED"` (the `NOT_PROVES_OPTIMALITY`/ +/// `optimality` pairing idiom). EXECUTED hardens the interval arithmetic +/// and the denominator; it cannot and does not claim these. +pub const MC_EXECUTED_NOT_CLAIMED: &[&str] = &[ + "sample_independence", + "interval_coverage", + "estimator_semantics", +]; + /// Provenance reference to the Telos pass-0009 research probe (reference only; /// never matched byte-wise, per the determinism decision in the design). pub const RESEARCH_SOURCE_HASH: &str = @@ -277,7 +320,11 @@ pub struct ScientificNumericalMethod { /// the estimator's denominator, id, and interval method were stated up /// front, and that the run they describe re-derives exactly under the sealed /// seed. The weaker the mode's promise, the more the receipt must carry. -#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +/// +/// No longer `Eq` (only `PartialEq`): the five EXECUTED fields below add +/// `f64`, which has no total order (`Eq` cannot be derived over it), the +/// same `ScientificBudget` precedent (its wall fields dropped `Eq` first). +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] pub struct ScientificMonteCarlo { /// The estimator's id (e.g. `mean`), author-declared, non-empty. pub estimator: String, @@ -288,8 +335,27 @@ pub struct ScientificMonteCarlo { /// claim is the interval, never the point, so a result whose interval /// method is undeclared is refused. pub interval_method: String, - /// `DECLARED` (v0): the facts were stated, not independently executed. + /// `DECLARED` | `EXECUTED`. DECLARED (v0): the facts were stated, not + /// independently executed. EXECUTED: the verifier RE-DERIVES the interval + /// from raw sufficient-statistic columns the kernel prints, at two + /// stages (see `compute_mc_executed`). pub status: String, + /// p_hat = successes_final / trials_final. Present IFF `status == + /// "EXECUTED"`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub estimate: Option, + /// Lower bound by the named method. Present IFF `status == "EXECUTED"`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub interval_low: Option, + /// Upper bound by the named method. Present IFF `status == "EXECUTED"`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub interval_high: Option, + /// trials_final; MUST equal `samples`, the witnessed denominator. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub n_effective: Option, + /// successes_final. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub successes: Option, } /// The budgeted-search admission block: a heuristic result without its @@ -902,21 +968,28 @@ pub fn is_known_invariant(name: &str) -> bool { } /// The column-count contract for an invariant: the `relation` invariant reads -/// ACROSS a row's columns and needs at least two; every single-scalar invariant -/// reads one value per step and requires exactly one column. Emit enforces this -/// before compiling; verify RE-CHECKS it (FIELD_CONTRACT_VIOLATION) so a -/// resealed receipt cannot present a column structure the invariant's contract -/// forbids, keeping the structural contract symmetric across emit and verify -/// like every other sealed field. -pub fn column_count_matches_invariant(name: &str, column_count: usize) -> bool { +/// ACROSS a row's columns and needs at least two; an EXECUTED monte_carlo +/// receipt requires exactly 3 columns (the invariant scalar plus the +/// witnessed successes/trials counters) paired with a single-scalar invariant +/// name, never with `relation`/`cross-backend` (their columns already mean +/// something else); every other single-scalar invariant requires exactly 1. +/// Emit enforces this before compiling; verify RE-CHECKS it +/// (FIELD_CONTRACT_VIOLATION) so a resealed receipt cannot present a column +/// structure the invariant's contract forbids, keeping the structural +/// contract symmetric across emit and verify like every other sealed field. +pub fn column_count_matches_invariant(name: &str, column_count: usize, mc_executed: bool) -> bool { if name == RELATION_INVARIANT { - column_count >= 2 + !mc_executed && column_count >= 2 } else if name == CROSS_BACKEND_INVARIANT { // The cross-backend row is exactly two columns (the C anchor and the // secondary lane): unlike the open-ended relation family member, the // invariant itself defines the column structure, so no other count - // is expressible. - column_count == 2 + // is expressible. Never paired with an EXECUTED mc block: the + // columns already mean something else, and cross-backend refuses + // Random anyway, which mc requires. + !mc_executed && column_count == 2 + } else if mc_executed { + column_count == 3 } else { column_count == 1 } @@ -1057,6 +1130,27 @@ pub fn evaluate_measurement( effective_len: rows, } } + _ if column_count == 3 => { + // An EXECUTED monte_carlo receipt: column 0 is the declared + // single-scalar invariant, columns 1-2 are the witnessed + // successes/trials counters `compute_mc_executed` checks + // separately. De-interleave and evaluate the invariant over + // column 0 only; rows are the effective observation count, + // mirroring the relation arm above. Ragged (not a multiple of + // 3) yields zero rows, same "cannot witness" treatment + // `relation_columns_agree` gives a ragged relation series. + let ragged = series.is_empty() || series.len() % 3 != 0; + let col0: Vec = if ragged { + Vec::new() + } else { + series.iter().step_by(3).copied().collect() + }; + let rows = col0.len(); + MeasurementVerdict { + observed: evaluate_invariant(name, &col0, tol), + effective_len: rows, + } + } _ => MeasurementVerdict { observed: evaluate_invariant(name, series, tol), effective_len: series.len(), @@ -1064,6 +1158,141 @@ pub fn evaluate_measurement( } } +/// The recomputed EXECUTED monte_carlo fields, owned by the caller to +/// compare against the sealed ones (emit: seal them; verify: compare). +#[derive(Clone, Debug, PartialEq)] +pub struct McExecutedComputed { + pub estimate: f64, + pub interval_low: f64, + pub interval_high: f64, + pub n_effective: u64, + pub successes: u64, +} + +/// Recompute the EXECUTED monte_carlo fields from a captured three-column +/// series (` ` per row), the +/// declared denominator, and the named interval method. PURE and +/// unit-tested; called from emit (fail closed before sealing), verify +/// Stage A (over the sealed series, before any re-run), and verify Stage B +/// (over the re-run series). Never trusts anything but the raw columns. +/// +/// Coherence checks, in order (Decision 1, design doc): every successes/ +/// trials value is integer-valued (`fract() == 0`) and below 2^53; trials +/// increments by exactly 1 across consecutive rows (the first row's +/// absolute value is free, the burn-in edge); successes is non-decreasing +/// with increments in {0, 1}; successes <= trials on every row; the final +/// row's trials equals `samples` (the witnessed-denominator equality). +/// `interval_method` must be one of the two executable methods +/// (`MC_INTERVAL_NORMAL_APPROX_95`, `MC_INTERVAL_WILSON_95`); any other +/// name (including `clopper-pearson-95`) is refused here, the single +/// source of truth for the executable vocabulary. `normal-approx-95` is +/// additionally refused at a boundary proportion (successes_final == 0 or +/// == trials_final): a zero-width interval there overclaims precision; +/// the message points at `wilson-95`. +pub fn compute_mc_executed( + series: &[f64], + column_count: usize, + samples: u64, + interval_method: &str, +) -> Result { + const MAX_EXACT_INTEGER: f64 = 9007199254740992.0; // 2^53 + + if column_count != 3 { + return Err(format!( + "column_count {column_count} is not 3: an EXECUTED monte_carlo receipt requires exactly three columns per row" + )); + } + if series.is_empty() || series.len() % 3 != 0 { + return Err(format!( + "series length {} is not a positive multiple of 3: ragged rows cannot witness a Bernoulli count", + series.len() + )); + } + let rows = series.len() / 3; + + let mut prev_trials: Option = None; + let mut prev_successes: Option = None; + for k in 0..rows { + let successes_k = series[k * 3 + 1]; + let trials_k = series[k * 3 + 2]; + for (label, value) in [("successes", successes_k), ("trials", trials_k)] { + if value.fract() != 0.0 || !value.is_finite() || value.abs() >= MAX_EXACT_INTEGER { + return Err(format!( + "row {k}: {label} = {value} is not an exact non-negative integer below 2^53" + )); + } + } + if let Some(prev) = prev_trials { + if trials_k != prev + 1.0 { + return Err(format!( + "row {k}: trials {trials_k} does not follow row {}'s trials {prev} by exactly 1", + k - 1 + )); + } + } + if let Some(prev) = prev_successes { + let delta = successes_k - prev; + if delta != 0.0 && delta != 1.0 { + return Err(format!( + "row {k}: successes {successes_k} does not follow row {}'s successes {prev} by 0 or 1", + k - 1 + )); + } + } + if successes_k > trials_k { + return Err(format!( + "row {k}: successes {successes_k} exceeds trials {trials_k}" + )); + } + prev_trials = Some(trials_k); + prev_successes = Some(successes_k); + } + + let trials_final = prev_trials.expect("rows > 0, checked above") as u64; + let successes_final = prev_successes.expect("rows > 0, checked above") as u64; + if trials_final != samples { + return Err(format!( + "witnessed final trials {trials_final} does not equal the declared samples {samples}: the denominator is not witnessed" + )); + } + + let n = trials_final as f64; + let p_hat = successes_final as f64 / n; + let z = MC_INTERVAL_Z_95; + + let (interval_low, interval_high) = match interval_method { + MC_INTERVAL_NORMAL_APPROX_95 => { + if successes_final == 0 || successes_final == trials_final { + return Err(format!( + "normal-approx-95 is degenerate at the boundary proportion (successes = {successes_final} of {trials_final}); use wilson-95" + )); + } + let half_width = z * (p_hat * (1.0 - p_hat) / n).sqrt(); + (p_hat - half_width, p_hat + half_width) + } + MC_INTERVAL_WILSON_95 => { + let z2 = z * z; + let denom = 1.0 + z2 / n; + let center = (p_hat + z2 / (2.0 * n)) / denom; + let margin = (z / denom) * (p_hat * (1.0 - p_hat) / n + z2 / (4.0 * n * n)).sqrt(); + (center - margin, center + margin) + } + other => { + return Err(format!( + "interval_method `{other}` is not in the EXECUTED executable vocabulary (v1: normal-approx-95, wilson-95); `{MC_INTERVAL_CLOPPER_PEARSON_95}` needs a verified inverse incomplete beta and is not executable" + )); + } + }; + + Ok(McExecutedComputed { + estimate: p_hat, + interval_low, + interval_high, + n_effective: trials_final, + successes: successes_final, + }) +} + /// Inputs threaded from `cmd_run` into the receipt builder. pub struct ScientificReceiptInputs<'a> { pub source_path: &'a Path, @@ -1216,6 +1445,15 @@ pub fn build_scientific_runtime_receipt( labels.push("NOT_PROVES_OPTIMALITY".to_string()); not_claimed.push("optimality".to_string()); } + // The EXECUTED monte_carlo boundary: hardening the interval arithmetic + // and the denominator cannot and does not harden sample independence, + // interval coverage, or the estimator's semantics. Sealed machine- + // readably (the NOT_PROVES_OPTIMALITY/optimality pairing idiom). + if let Some(mc) = &monte_carlo { + if mc.status == "EXECUTED" { + not_claimed.extend(MC_EXECUTED_NOT_CLAIMED.iter().map(|s| s.to_string())); + } + } // The typed-effect system doing receipt work: witnessed absences and the // determinism statement derive from the observed capability union. @@ -1573,6 +1811,51 @@ pub fn build_self_test_cases( }); } + // 10. FIELD_CONTRACT_VIOLATION (MC executed interval does not recompute): + // nudge the sealed interval_high on an EXECUTED monte_carlo block (the + // receipt's own block if it already carries one -- e.g. a receipt + // emitted from mc_pi_rejection_executed.bld -- else a syntactically + // valid one is added, mirroring case 9's cross_backend fallback). + // Either way the tamper reaches Stage A's FIELD_CONTRACT_VIOLATION arm: + // whichever stage-A gate fires first (seed pairing, field presence, or + // the interval-mismatch check this case targets) on an arbitrary + // pristine input, the reported class is FIELD_CONTRACT_VIOLATION + // either way, the same robustness case 7's zero-denominator tamper + // already relies on. + { + let mut v = receipt_json.clone(); + match v.get_mut("monte_carlo") { + Some(mc) + if !mc.is_null() + && mc.get("status").and_then(|s| s.as_str()) == Some("EXECUTED") => + { + let bumped = mc["interval_high"].as_f64().unwrap_or(0.5) + 0.25; + mc["interval_high"] = serde_json::Value::from(bumped); + } + _ => { + v["monte_carlo"] = serde_json::json!({ + "estimator": "proportion", + "samples": 4u64, + "interval_method": "wilson-95", + "status": "EXECUTED", + "estimate": 0.5, + "interval_low": 0.15, + "interval_high": 0.85, + "n_effective": 4u64, + "successes": 2u64, + }); + } + } + let v = reseal_json(&v)?; + cases.push(SelfTestCase { + label: "EXECUTED monte_carlo interval_high nudged against its Stage A recompute" + .to_string(), + tampered: v, + expected_class: "FIELD_CONTRACT_VIOLATION".to_string(), + resealed: true, + }); + } + Ok(cases) } @@ -1688,6 +1971,13 @@ pub struct ScientificCorpusMember { pub mc_samples: Option, #[serde(default, skip_serializing_if = "Option::is_none")] pub mc_interval: Option, + /// Whether to emit under `--mc-executed`, passed through by the runner. + /// No `skip_serializing_if` (the `negative_fixture` precedent): this + /// manifest is hand-authored input, never re-serialized from the + /// struct, so byte-stability does not apply here the way it does to a + /// sealed receipt. + #[serde(default)] + pub mc_executed: bool, /// The member's budgeted-search declaration (`--budget-steps` / /// `--budget-consumed`), passed through by the runner. The same /// all-or-nothing contract applies: a partial declaration is refused at @@ -2159,14 +2449,23 @@ pub fn evaluate_scientific_runtime_receipt( } // Re-check the column-count contract emit enforced (relation needs >= 2 - // columns, every single-scalar invariant needs exactly 1), so a resealed - // receipt cannot present a column structure the invariant forbids. The - // field is inert for the single-scalar invariants' verdict, but leaving the - // contract unenforced at verify would let emit and verify disagree on what - // a well-formed receipt is. - if !column_count_matches_invariant(&receipt.invariant.name, receipt.measurement.column_count) { + // columns, an EXECUTED monte_carlo receipt needs exactly 3, every other + // single-scalar invariant needs exactly 1), so a resealed receipt cannot + // present a column structure the invariant forbids. The field is inert + // for the single-scalar invariants' verdict, but leaving the contract + // unenforced at verify would let emit and verify disagree on what a + // well-formed receipt is. + let mc_executed_for_columns = receipt + .monte_carlo + .as_ref() + .is_some_and(|mc| mc.status == "EXECUTED"); + if !column_count_matches_invariant( + &receipt.invariant.name, + receipt.measurement.column_count, + mc_executed_for_columns, + ) { eprintln!( - "Error: column_count {} violates the contract for invariant `{}` (relation requires >= 2, every single-scalar invariant requires exactly 1)", + "Error: column_count {} violates the contract for invariant `{}` (relation requires >= 2, an EXECUTED monte_carlo receipt requires exactly 3, every other single-scalar invariant requires exactly 1)", receipt.measurement.column_count, receipt.invariant.name ); return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); @@ -2319,7 +2618,11 @@ pub fn evaluate_scientific_runtime_receipt( // its SHAPE is not negotiable: it rides only on a seeded Random program // (an MC claim over a stream that cannot re-derive is unpriceable), its // denominator is non-zero, its estimator and interval method are named, - // and its status is the one thing v0 can honestly say (DECLARED). + // and its status is one of the two things v0 can honestly say (DECLARED + // or EXECUTED). Stage A (this block): re-derived over the SEALED series, + // before any re-run, so a tampered-and-resealed interval is a pure data + // contradiction. Stage B (after the re-run, below) re-derives the same + // fields over the re-run series. if let Some(mc) = &receipt.monte_carlo { if !rederived_uses_random || receipt.seed_value.is_none() { eprintln!( @@ -2339,12 +2642,90 @@ pub fn evaluate_scientific_runtime_receipt( ); return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); } - if mc.status != "DECLARED" { - eprintln!( - "Error: monte_carlo.status `{}` is not expressible: v0 declares the facts, it does not execute them (the only valid status is DECLARED)", - mc.status - ); - return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + let executed_fields_present = mc.estimate.is_some() + || mc.interval_low.is_some() + || mc.interval_high.is_some() + || mc.n_effective.is_some() + || mc.successes.is_some(); + match mc.status.as_str() { + "DECLARED" => { + if executed_fields_present { + eprintln!( + "Error: monte_carlo.status is DECLARED but an executed field is present: a DECLARED block never carries estimate/interval_low/interval_high/n_effective/successes" + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + } + "EXECUTED" => { + let ( + Some(estimate), + Some(interval_low), + Some(interval_high), + Some(n_effective), + Some(successes), + ) = ( + mc.estimate, + mc.interval_low, + mc.interval_high, + mc.n_effective, + mc.successes, + ) + else { + eprintln!( + "Error: monte_carlo.status is EXECUTED but not all five executed fields (estimate, interval_low, interval_high, n_effective, successes) are present" + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + }; + if mc.estimator != MC_EXECUTED_ESTIMATOR_PROPORTION { + eprintln!( + "Error: EXECUTED monte_carlo estimator `{}` is not in the executable vocabulary (v1: proportion)", + mc.estimator + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + let computed = compute_mc_executed( + &receipt.measurement.observed_values, + receipt.measurement.column_count, + mc.samples, + &mc.interval_method, + ) + .map_err(|reason| { + eprintln!( + "Error: EXECUTED monte_carlo Stage A (sealed series, no re-run) recompute failed: {reason}" + ); + verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1) + })?; + if computed.n_effective != n_effective || n_effective != mc.samples { + eprintln!( + "Error: sealed n_effective {n_effective} does not match the Stage A witnessed denominator {} (declared samples {})", + computed.n_effective, mc.samples + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + if computed.successes != successes { + eprintln!( + "Error: sealed successes {successes} does not match the Stage A recompute {}", + computed.successes + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + if (computed.estimate - estimate).abs() > MC_RECOMPUTE_TOLERANCE + || (computed.interval_low - interval_low).abs() > MC_RECOMPUTE_TOLERANCE + || (computed.interval_high - interval_high).abs() > MC_RECOMPUTE_TOLERANCE + { + eprintln!( + "Error: sealed EXECUTED interval fields do not match the Stage A recompute over the sealed series (estimate {estimate} vs {}, low {interval_low} vs {}, high {interval_high} vs {})", + computed.estimate, computed.interval_low, computed.interval_high + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + } + other => { + eprintln!( + "Error: monte_carlo.status `{other}` is not expressible (only DECLARED or EXECUTED)" + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } } } // The budgeted-search admission contracts. Deterministic: unlike @@ -2506,6 +2887,27 @@ pub fn evaluate_scientific_runtime_receipt( ); return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); } + // The EXECUTED monte_carlo not_claimed triad: sample_independence, + // interval_coverage, and estimator_semantics must pair exactly (all + // three or none) with an EXECUTED monte_carlo block. + let mc_executed = receipt + .monte_carlo + .as_ref() + .is_some_and(|mc| mc.status == "EXECUTED"); + let has_all_mc_not_claimed = MC_EXECUTED_NOT_CLAIMED + .iter() + .all(|c| receipt.not_claimed.iter().any(|x| x == c)); + let has_any_mc_not_claimed = MC_EXECUTED_NOT_CLAIMED + .iter() + .any(|c| receipt.not_claimed.iter().any(|x| x == c)); + if mc_executed != has_all_mc_not_claimed || (has_any_mc_not_claimed && !has_all_mc_not_claimed) + { + eprintln!( + "Error: not_claimed `sample_independence`/`interval_coverage`/`estimator_semantics` present={} but monte_carlo EXECUTED={}: the boundary entries must pair exactly (all three or none) with an EXECUTED block", + has_any_mc_not_claimed, mc_executed + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } // The claim-language rule: a budgeted search reports its incumbent, // never optimality, so the free text may not contradict // NOT_PROVES_OPTIMALITY. @@ -2738,6 +3140,42 @@ pub fn evaluate_scientific_runtime_receipt( return Err(verify_failure_class(json, "MEASUREMENT_COUNT_DRIFT", 1)); } + // Stage B: an EXECUTED monte_carlo block's sealed fields must ALSO + // re-derive over the RE-RUN series (not just the sealed one, Stage A + // above). Stage A alone would let a receipt stay internally coherent + // while no longer describing the run it names; Stage B catches that. + if let Some(mc) = &receipt.monte_carlo { + if mc.status == "EXECUTED" { + // Stage A already required all five fields present; unwrap is safe. + let estimate = mc.estimate.expect("Stage A validated presence"); + let interval_low = mc.interval_low.expect("Stage A validated presence"); + let interval_high = mc.interval_high.expect("Stage A validated presence"); + let computed = compute_mc_executed( + &verdict_series, + receipt.measurement.column_count, + mc.samples, + &mc.interval_method, + ) + .map_err(|reason| { + eprintln!( + "Error: EXECUTED monte_carlo Stage B (re-run series) recompute failed: {reason}" + ); + verify_failure_class(json, "MC_INTERVAL_DRIFT", 1) + })?; + if computed.n_effective != mc.samples + || computed.successes != mc.successes.expect("Stage A validated presence") + || (computed.estimate - estimate).abs() > MC_RECOMPUTE_TOLERANCE + || (computed.interval_low - interval_low).abs() > MC_RECOMPUTE_TOLERANCE + || (computed.interval_high - interval_high).abs() > MC_RECOMPUTE_TOLERANCE + { + eprintln!( + "Error: EXECUTED monte_carlo interval drift: sealed fields do not match the Stage B recompute over the re-run series" + ); + return Err(verify_failure_class(json, "MC_INTERVAL_DRIFT", 1)); + } + } + } + // (4) Recompute the verdict and compare against the stored one. let recomputed = recompute_verdict( &receipt.invariant.name, @@ -3175,6 +3613,10 @@ fn digest_is_well_formed(digest: &ScientificDigest) -> bool { /// - `MEASUREMENT_COUNT_DRIFT`, `INVARIANT_STATUS_DRIFT`, /// `VIOLATION_COUNT_DRIFT`, `RECEIPT_STATUS_DRIFT`: the re-run disagrees with /// the stored verdict facts. +/// - `MC_INTERVAL_DRIFT`: an EXECUTED monte_carlo receipt's sealed interval +/// fields do not match the Stage B recompute over the re-run series +/// (Stage A already passed over the sealed series; this catches a +/// receipt that stopped describing the run it names). /// - `SEAL_MISMATCH`: the stored receipt body does not re-seal. /// - `INVARIANT_NOT_HELD` (exit 3): the receipt is FAITHFUL but records /// FAIL_UNEXPECTED / UNVERIFIABLE (emitted at the verdict tail, not here). @@ -3461,6 +3903,7 @@ mod tests { "FIELD_CONTRACT_VIOLATION", "FIELD_CONTRACT_VIOLATION", "FIELD_CONTRACT_VIOLATION", + "FIELD_CONTRACT_VIOLATION", ] ); @@ -4222,6 +4665,201 @@ mod tests { assert_eq!(mono.effective_len, 4); } + #[test] + fn evaluate_measurement_deinterleaves_column_zero_for_three_columns() { + // Columns 1-2 would fail non_negative (negative values), but column 0 + // (the invariant scalar) is all non-negative, so the verdict must + // read column 0 only, ignoring the witnessed counters beside it. + let series = [ + 1.0, -5.0, -5.0, // row 0: invariant 1.0, successes -5, trials -5 + 2.0, -6.0, -6.0, // row 1 + ]; + let verdict = + evaluate_measurement(NON_NEGATIVE_INVARIANT, &series, NON_NEGATIVE_TOLERANCE, 3); + assert_eq!(verdict.effective_len, 2, "row count, not token count"); + assert_eq!( + verdict.observed.violation_count, 0, + "column 0 alone is non-negative; columns 1-2 must be ignored by the invariant check" + ); + } + + #[test] + fn evaluate_measurement_three_column_ragged_series_cannot_witness() { + // A series length not a multiple of 3 cannot form complete rows, + // mirroring the existing ragged-relation test. + let verdict = evaluate_measurement( + NON_NEGATIVE_INVARIANT, + &[1.0, 2.0, 3.0, 4.0], + NON_NEGATIVE_TOLERANCE, + 3, + ); + assert_eq!(verdict.effective_len, 0); + } + + #[test] + fn column_count_matches_invariant_refuses_mc_executed_with_relation() { + // An EXECUTED mc block can never pair with relation/cross-backend: + // their columns already mean something else. + assert!(!column_count_matches_invariant(RELATION_INVARIANT, 3, true)); + assert!(!column_count_matches_invariant( + CROSS_BACKEND_INVARIANT, + 3, + true + )); + assert!(column_count_matches_invariant(RELATION_INVARIANT, 3, false)); + assert!(column_count_matches_invariant( + NON_NEGATIVE_INVARIANT, + 3, + true + )); + assert!(!column_count_matches_invariant( + NON_NEGATIVE_INVARIANT, + 3, + false + )); + } + + #[test] + fn compute_mc_executed_recovers_a_coherent_wilson_series() { + // successes 1,1,2,2; trials 10,11,12,13 (each an increment of exactly + // 1); the invariant scalar column is arbitrary (0.0 throughout). + let series = [ + 0.0, 1.0, 10.0, // + 0.0, 1.0, 11.0, // + 0.0, 2.0, 12.0, // + 0.0, 2.0, 13.0, // + ]; + let result = compute_mc_executed(&series, 3, 13, MC_INTERVAL_WILSON_95); + let computed = result.expect("a coherent series must compute"); + assert_eq!(computed.n_effective, 13); + assert_eq!(computed.successes, 2); + assert!((computed.estimate - 2.0 / 13.0).abs() < 1e-12); + assert!(computed.interval_low < computed.estimate); + assert!(computed.estimate < computed.interval_high); + } + + #[test] + fn compute_mc_executed_rejects_before_any_rerun_on_bad_trials_step() { + // trials jumps by 2 between row 0 and row 1 (10 -> 12): a pure data + // contradiction the function catches with no re-run machinery at all + // (the function takes no compile/run inputs). + let series = [0.0, 1.0, 10.0, 0.0, 1.0, 12.0]; + let err = compute_mc_executed(&series, 3, 12, MC_INTERVAL_WILSON_95) + .expect_err("a trials step of 2 must be rejected"); + assert!(err.contains("row 1"), "error must name the row: {err}"); + assert!(err.contains("trials"), "error must name the field: {err}"); + } + + #[test] + fn compute_mc_executed_rejects_successes_decrease() { + let series = [0.0, 2.0, 10.0, 0.0, 1.0, 11.0]; + let err = compute_mc_executed(&series, 3, 11, MC_INTERVAL_WILSON_95) + .expect_err("a successes decrease must be rejected"); + assert!(err.contains("row 1"), "error must name the row: {err}"); + assert!( + err.contains("successes"), + "error must name the field: {err}" + ); + } + + #[test] + fn compute_mc_executed_rejects_successes_exceeding_trials() { + let series = [0.0, 5.0, 4.0]; + let err = compute_mc_executed(&series, 3, 4, MC_INTERVAL_WILSON_95) + .expect_err("successes exceeding trials must be rejected"); + assert!(err.contains("exceeds"), "error must name the reason: {err}"); + } + + #[test] + fn compute_mc_executed_rejects_non_integer_column() { + let series = [0.0, 1.5, 10.0]; + let err = compute_mc_executed(&series, 3, 10, MC_INTERVAL_WILSON_95) + .expect_err("a non-integer successes value must be rejected"); + assert!( + err.contains("integer"), + "error must name the integrality reason: {err}" + ); + } + + #[test] + fn compute_mc_executed_witnessed_denominator_must_equal_samples() { + // A coherent series whose final trials is 2000, but samples declares + // 1999: the denominator is not witnessed. + let series = [0.0, 1000.0, 2000.0]; + let err = compute_mc_executed(&series, 3, 1999, MC_INTERVAL_WILSON_95) + .expect_err("a witnessed/declared denominator mismatch must be rejected"); + assert!( + err.contains("2000"), + "error must name the witnessed trials: {err}" + ); + assert!( + err.contains("1999"), + "error must name the declared samples: {err}" + ); + } + + #[test] + fn compute_mc_executed_rejects_ragged_series() { + let series = [0.0, 1.0, 10.0, 0.0]; + let err = compute_mc_executed(&series, 3, 10, MC_INTERVAL_WILSON_95) + .expect_err("a series length not a multiple of 3 must be rejected"); + assert!(err.contains("ragged"), "error must name the reason: {err}"); + } + + #[test] + fn compute_mc_executed_normal_approx_degenerate_at_zero_successes() { + let series = [0.0, 0.0, 10.0]; + let err = compute_mc_executed(&series, 3, 10, MC_INTERVAL_NORMAL_APPROX_95) + .expect_err("zero successes must be rejected for normal-approx-95"); + assert!( + err.contains("wilson-95"), + "error must point at the alternative: {err}" + ); + } + + #[test] + fn compute_mc_executed_normal_approx_degenerate_at_all_successes() { + let series = [0.0, 10.0, 10.0]; + let err = compute_mc_executed(&series, 3, 10, MC_INTERVAL_NORMAL_APPROX_95) + .expect_err("all-successes must be rejected for normal-approx-95"); + assert!( + err.contains("wilson-95"), + "error must point at the alternative: {err}" + ); + } + + #[test] + fn compute_mc_executed_rejects_clopper_pearson() { + let series = [0.0, 5.0, 10.0]; + let err = compute_mc_executed(&series, 3, 10, MC_INTERVAL_CLOPPER_PEARSON_95) + .expect_err("clopper-pearson-95 is not executable in v1"); + assert!( + err.contains("inverse incomplete beta"), + "error must name the reason: {err}" + ); + } + + #[test] + fn compute_mc_executed_wilson_matches_hand_computed_value() { + // successes = 3, trials = 10: p_hat = 0.3, z = 1.959963984540054. + // Hand-computed (independent transcription of the Wilson formula): + // z2 = 3.84145...; denom = 1 + z2/n; center = (p + z2/(2n)) / denom; + // margin = (z/denom) * sqrt(p*(1-p)/n + z2/(4n^2)). + let series = [0.0, 3.0, 10.0]; + let computed = compute_mc_executed(&series, 3, 10, MC_INTERVAL_WILSON_95) + .expect("a coherent series must compute"); + let z = MC_INTERVAL_Z_95; + let z2 = z * z; + let n = 10.0f64; + let p = 0.3f64; + let denom = 1.0 + z2 / n; + let center = (p + z2 / (2.0 * n)) / denom; + let margin = (z / denom) * (p * (1.0 - p) / n + z2 / (4.0 * n * n)).sqrt(); + assert!((computed.interval_low - (center - margin)).abs() < 1e-9); + assert!((computed.interval_high - (center + margin)).abs() < 1e-9); + assert!((computed.estimate - 0.3).abs() < 1e-12); + } + #[test] fn verify_round_trips_a_relation_receipt() { let path = Path::new("k.bld"); @@ -5718,6 +6356,11 @@ mod tests { samples: 2000, interval_method: "normal-approx-95".to_string(), status: "DECLARED".to_string(), + estimate: None, + interval_low: None, + interval_high: None, + n_effective: None, + successes: None, } } fn run( @@ -5764,6 +6407,25 @@ mod tests { Ok(()), "a complete MC declaration on a seeded Random run must verify" ); + // BACKWARD COMPATIBILITY PIN: a DECLARED block's serialized JSON + // carries EXACTLY the four original keys, none of the five new + // EXECUTED fields (`skip_serializing_if = "Option::is_none"` + // working as intended). A receipt sealed before this slice, when + // re-parsed and re-serialized today, produces this exact shape, so + // its bytes and seal are unchanged. + let mc_keys: std::collections::BTreeSet<&str> = value["monte_carlo"] + .as_object() + .expect("monte_carlo is an object") + .keys() + .map(|k| k.as_str()) + .collect(); + assert_eq!( + mc_keys, + ["estimator", "samples", "interval_method", "status"] + .into_iter() + .collect::>(), + "a DECLARED monte_carlo block must serialize with exactly its original four keys" + ); // A zero denominator is unpriceable. let mut bad = mc(); @@ -5776,11 +6438,20 @@ mod tests { bad.interval_method = " ".to_string(); assert_eq!(run(&seeded_mc(bad), random_policy()), Err(1)); - // A status v0 cannot honestly say is refused. + // EXECUTED is now expressible, but this literal (via mc(), which + // sets none of the five executed fields) must still fail: EXECUTED + // with no executed fields present is FIELD_CONTRACT_VIOLATION (the + // field-presence gate), not an unknown status. let mut bad = mc(); bad.status = "EXECUTED".to_string(); assert_eq!(run(&seeded_mc(bad), random_policy()), Err(1)); + // A THIRD status string is refused as unknown: the two-arm + // vocabulary (DECLARED | EXECUTED) itself stays gated. + let mut bad = mc(); + bad.status = "SIMULATED".to_string(); + assert_eq!(run(&seeded_mc(bad), random_policy()), Err(1)); + // An MC block on a program with no Random capability (and no seed) is // refused at the pairing gate. let unpaired = build_scientific_runtime_receipt(ScientificReceiptInputs { @@ -5797,6 +6468,387 @@ mod tests { assert!(value.get("monte_carlo").is_none()); } + /// The effect-policy fixture for the EXECUTED monte_carlo tests: Random + /// paired with a sealed seed. + fn mc_executed_random_policy() -> ScientificEffectPolicy { + ScientificEffectPolicy { + facts_digest: hex_digest('9'), + observed_capabilities: vec!["Console".to_string(), "Random".to_string()], + reads_stdin: false, + } + } + + /// A coherent 3-column EXECUTED monte_carlo receipt fixture: series is + /// ` ` per row, successes + /// 1,1,2,2 over trials 1,2,3,4 (samples = 4), wilson-95. The executed + /// fields are computed by `compute_mc_executed` itself so the fixture is + /// self-consistent by construction. + fn coherent_executed_mc_receipt(path: &Path) -> ScientificRuntimeReceipt { + let series = vec![ + 0.0, 1.0, 1.0, // + 0.0, 1.0, 2.0, // + 0.0, 2.0, 3.0, // + 0.0, 2.0, 4.0, // + ]; + let computed = compute_mc_executed(&series, 3, 4, MC_INTERVAL_WILSON_95) + .expect("fixture series must be coherent"); + let mc = ScientificMonteCarlo { + estimator: MC_EXECUTED_ESTIMATOR_PROPORTION.to_string(), + samples: 4, + interval_method: MC_INTERVAL_WILSON_95.to_string(), + status: "EXECUTED".to_string(), + estimate: Some(computed.estimate), + interval_low: Some(computed.interval_low), + interval_high: Some(computed.interval_high), + n_effective: Some(computed.n_effective), + successes: Some(computed.successes), + }; + build_scientific_runtime_receipt(ScientificReceiptInputs { + effect_policy: mc_executed_random_policy(), + seed_value: Some(42), + monte_carlo: Some(mc), + column_count: 3, + ..base_inputs_for(NON_NEGATIVE_INVARIANT, path, series, true, false) + }) + } + + /// An ALL-FAILURE variant (successes = 0 on every row) of the coherent + /// EXECUTED fixture, under wilson-95 (which, unlike normal-approx-95, + /// has no boundary refusal at successes = 0). This exists specifically + /// to isolate the "all five executed fields present" gate from the + /// Stage A recompute-mismatch gate: since `u64::default() == 0` equals + /// the REAL successes value here, a missing `successes` field defaults + /// to exactly the correct number, so ONLY the presence gate (not the + /// recompute comparison) can catch it -- the field-presence-guard + /// mutation test below relies on this. + fn coherent_executed_mc_receipt_all_failures(path: &Path) -> ScientificRuntimeReceipt { + let series = vec![ + 0.0, 0.0, 1.0, // + 0.0, 0.0, 2.0, // + 0.0, 0.0, 3.0, // + 0.0, 0.0, 4.0, // + ]; + let computed = compute_mc_executed(&series, 3, 4, MC_INTERVAL_WILSON_95) + .expect("an all-failure series is coherent under wilson-95"); + assert_eq!(computed.successes, 0, "fixture precondition"); + let mc = ScientificMonteCarlo { + estimator: MC_EXECUTED_ESTIMATOR_PROPORTION.to_string(), + samples: 4, + interval_method: MC_INTERVAL_WILSON_95.to_string(), + status: "EXECUTED".to_string(), + estimate: Some(computed.estimate), + interval_low: Some(computed.interval_low), + interval_high: Some(computed.interval_high), + n_effective: Some(computed.n_effective), + successes: Some(computed.successes), + }; + build_scientific_runtime_receipt(ScientificReceiptInputs { + effect_policy: mc_executed_random_policy(), + seed_value: Some(42), + monte_carlo: Some(mc), + column_count: 3, + ..base_inputs_for(NON_NEGATIVE_INVARIANT, path, series, true, false) + }) + } + + #[test] + fn verify_round_trips_a_coherent_executed_monte_carlo_receipt() { + // The positive control for every negative test below: a faithful + // EXECUTED receipt must verify (both stages pass on an untampered, + // faithfully re-run receipt). + let path = Path::new("k.bld"); + let receipt = coherent_executed_mc_receipt(path); + let value = serde_json::to_value(&receipt).expect("to_value"); + assert_eq!(value["monte_carlo"]["status"], "EXECUTED"); + assert_eq!(value["monte_carlo"]["n_effective"], 4); + assert_eq!(value["monte_carlo"]["successes"], 2); + assert!(receipt + .not_claimed + .iter() + .any(|c| c == "sample_independence")); + assert!(receipt.not_claimed.iter().any(|c| c == "interval_coverage")); + assert!(receipt + .not_claimed + .iter() + .any(|c| c == "estimator_semantics")); + let src = receipt.source_digest.clone(); + let graph = receipt.input_graph_digest.clone(); + let series = receipt.measurement.observed_values.clone(); + let result = verify_scientific_runtime_receipt( + &value, + None, + true, + &receipt.compiler_version, + &receipt.language_version, + Some(&test_toolchain()), + move |_| { + Ok(RederivedFacts { + source_digest: src, + input_graph_digest: graph, + effect_policy: mc_executed_random_policy(), + }) + }, + move |_, _, _, _| Ok(rerun(series)), + ); + assert_eq!(result, Ok(()), "a faithful EXECUTED receipt must verify"); + } + + #[test] + fn verify_stage_a_rejects_tampered_executed_interval_before_any_rerun() { + // Tamper interval_high directly on the sealed JSON (bypassing + // `seal_receipt`, so the seal would be stale) then re-seal via the + // same `reseal_json` path the self-test uses. A rerun_series closure + // that panics if called proves the rejection fires BEFORE any + // re-run: this is the "Stage-A-rejects-before-rerun" property test. + let path = Path::new("k.bld"); + let receipt = coherent_executed_mc_receipt(path); + let value = serde_json::to_value(&receipt).expect("to_value"); + let mut tampered = value.clone(); + let bumped = tampered["monte_carlo"]["interval_high"] + .as_f64() + .expect("interval_high must be present") + + 0.25; + tampered["monte_carlo"]["interval_high"] = serde_json::Value::from(bumped); + let tampered = reseal_json(&tampered).expect("reseal must succeed"); + let src = receipt.source_digest.clone(); + let graph = receipt.input_graph_digest.clone(); + let result = verify_scientific_runtime_receipt( + &tampered, + None, + true, + &receipt.compiler_version, + &receipt.language_version, + Some(&test_toolchain()), + move |_| { + Ok(RederivedFacts { + source_digest: src, + input_graph_digest: graph, + effect_policy: mc_executed_random_policy(), + }) + }, + |_, _, _, _| panic!("Stage A must reject a tampered interval before any re-run"), + ); + assert_eq!(result, Err(1)); + } + + #[test] + fn verify_stage_b_reports_mc_interval_drift_on_a_changed_rerun() { + // The SEALED series is untampered (Stage A passes cleanly), but the + // RE-RUN returns a DIFFERENT coherent series (one more successful + // draw): a receipt that stayed internally coherent while no longer + // describing the run it names. Only Stage B catches this. + let path = Path::new("k.bld"); + let receipt = coherent_executed_mc_receipt(path); + let value = serde_json::to_value(&receipt).expect("to_value"); + let src = receipt.source_digest.clone(); + let graph = receipt.input_graph_digest.clone(); + let drifted_series = vec![ + 0.0, 1.0, 1.0, // + 0.0, 2.0, 2.0, // one more success than the sealed series + 0.0, 3.0, 3.0, // + 0.0, 3.0, 4.0, // + ]; + let report = evaluate_scientific_runtime_receipt( + &value, + None, + true, + &receipt.compiler_version, + &receipt.language_version, + Some(&test_toolchain()), + move |_| { + Ok(RederivedFacts { + source_digest: src, + input_graph_digest: graph, + effect_policy: mc_executed_random_policy(), + }) + }, + move |_, _, _, _| Ok(rerun(drifted_series)), + ); + assert!(report.is_err(), "a Stage B interval drift must fail verify"); + } + + #[test] + fn verify_refuses_declared_block_carrying_an_executed_field() { + let path = Path::new("k.bld"); + let mut mc = ScientificMonteCarlo { + estimator: "mean".to_string(), + samples: 2000, + interval_method: "normal-approx-95".to_string(), + status: "DECLARED".to_string(), + estimate: None, + interval_low: None, + interval_high: None, + n_effective: None, + successes: None, + }; + mc.estimate = Some(0.5); // an executed field on a DECLARED block + let receipt = build_scientific_runtime_receipt(ScientificReceiptInputs { + effect_policy: mc_executed_random_policy(), + seed_value: Some(42), + monte_carlo: Some(mc), + ..base_inputs(path, vec![4.0, 3.0, 2.0], true, false) + }); + let value = serde_json::to_value(&receipt).expect("to_value"); + let src = receipt.source_digest.clone(); + let graph = receipt.input_graph_digest.clone(); + let result = verify_scientific_runtime_receipt( + &value, + None, + true, + &receipt.compiler_version, + &receipt.language_version, + Some(&test_toolchain()), + move |_| { + Ok(RederivedFacts { + source_digest: src, + input_graph_digest: graph, + effect_policy: mc_executed_random_policy(), + }) + }, + |_, _, _, _| { + panic!("a DECLARED-with-executed-field block must reject before any re-run") + }, + ); + assert_eq!(result, Err(1)); + } + + #[test] + fn verify_refuses_executed_block_missing_an_executed_field() { + let path = Path::new("k.bld"); + // The all-failure fixture: real successes = 0 EQUALS + // `u64::default()`, so a missing `successes` field would slip past + // the Stage A recompute-mismatch comparison undetected -- ONLY the + // "all five fields present" gate can catch it here, which is the + // point (an ordinary nonzero fixture would be caught downstream + // regardless of whether this specific gate runs, which would make + // the test insensitive to this gate's removal). + let receipt = coherent_executed_mc_receipt_all_failures(path); + let mut value = serde_json::to_value(&receipt).expect("to_value"); + value["monte_carlo"] + .as_object_mut() + .unwrap() + .remove("successes"); + let value = reseal_json(&value).expect("reseal must succeed"); + let src = receipt.source_digest.clone(); + let graph = receipt.input_graph_digest.clone(); + let result = verify_scientific_runtime_receipt( + &value, + None, + true, + &receipt.compiler_version, + &receipt.language_version, + Some(&test_toolchain()), + move |_| { + Ok(RederivedFacts { + source_digest: src, + input_graph_digest: graph, + effect_policy: mc_executed_random_policy(), + }) + }, + |_, _, _, _| panic!("EXECUTED with a missing field must reject before any re-run"), + ); + assert_eq!(result, Err(1)); + } + + #[test] + fn verify_refuses_executed_estimator_outside_vocabulary() { + let path = Path::new("k.bld"); + let receipt = coherent_executed_mc_receipt(path); + let mut value = serde_json::to_value(&receipt).expect("to_value"); + value["monte_carlo"]["estimator"] = serde_json::Value::from("mean"); + let value = reseal_json(&value).expect("reseal must succeed"); + let src = receipt.source_digest.clone(); + let graph = receipt.input_graph_digest.clone(); + let result = verify_scientific_runtime_receipt( + &value, + None, + true, + &receipt.compiler_version, + &receipt.language_version, + Some(&test_toolchain()), + move |_| { + Ok(RederivedFacts { + source_digest: src, + input_graph_digest: graph, + effect_policy: mc_executed_random_policy(), + }) + }, + |_, _, _, _| panic!("an out-of-vocabulary estimator must reject before any re-run"), + ); + assert_eq!(result, Err(1)); + } + + #[test] + fn verify_not_claimed_triad_biconditional() { + let path = Path::new("k.bld"); + + fn check(receipt: &ScientificRuntimeReceipt, value: serde_json::Value) -> Result<(), i32> { + let src = receipt.source_digest.clone(); + let graph = receipt.input_graph_digest.clone(); + verify_scientific_runtime_receipt( + &value, + None, + true, + &receipt.compiler_version, + &receipt.language_version, + Some(&test_toolchain()), + move |_| { + Ok(RederivedFacts { + source_digest: src, + input_graph_digest: graph, + effect_policy: mc_executed_random_policy(), + }) + }, + |_, _, _, _| panic!("a not_claimed triad mismatch must reject before any re-run"), + ) + } + + // EXECUTED with the triad ABSENT is refused. + let receipt = coherent_executed_mc_receipt(path); + let mut value = serde_json::to_value(&receipt).expect("to_value"); + value["not_claimed"] = serde_json::Value::Array( + receipt + .not_claimed + .iter() + .filter(|c| !MC_EXECUTED_NOT_CLAIMED.contains(&c.as_str())) + .map(|c| serde_json::Value::from(c.clone())) + .collect(), + ); + let value = reseal_json(&value).expect("reseal must succeed"); + assert_eq!(check(&receipt, value), Err(1)); + + // DECLARED with the triad PRESENT is refused. + let plain = + build_scientific_runtime_receipt(base_inputs(path, vec![4.0, 3.0, 2.0], true, false)); + let mut value = serde_json::to_value(&plain).expect("to_value"); + let mut not_claimed: Vec = value["not_claimed"] + .as_array() + .unwrap() + .iter() + .cloned() + .collect(); + for c in MC_EXECUTED_NOT_CLAIMED { + not_claimed.push(serde_json::Value::from(*c)); + } + value["not_claimed"] = serde_json::Value::Array(not_claimed); + let value = reseal_json(&value).expect("reseal must succeed"); + assert_eq!(check(&plain, value), Err(1)); + + // EXECUTED with only two of three present is refused. + let receipt = coherent_executed_mc_receipt(path); + let mut value = serde_json::to_value(&receipt).expect("to_value"); + value["not_claimed"] = serde_json::Value::Array( + receipt + .not_claimed + .iter() + .filter(|c| c.as_str() != "interval_coverage") + .map(|c| serde_json::Value::from(c.clone())) + .collect(), + ); + let value = reseal_json(&value).expect("reseal must succeed"); + assert_eq!(check(&receipt, value), Err(1)); + } + #[test] fn verify_enforces_the_budget_admission_contracts() { fn budget() -> ScientificBudget { diff --git a/compiler/tests/cli.rs b/compiler/tests/cli.rs index 108f0141..4ec7456c 100644 --- a/compiler/tests/cli.rs +++ b/compiler/tests/cli.rs @@ -15116,6 +15116,548 @@ fn monte_carlo_declaration_round_trips_and_pins_the_admission_contract() { let _ = fs::remove_dir_all(&dir); } +#[test] +fn mc_pi_rejection_executed_round_trip_and_negative_fixture() { + if !c_backend_ready() { + eprintln!( + "skipping mc_pi_rejection_executed_round_trip_and_negative_fixture: C backend not ready" + ); + return; + } + let dir = + std::env::temp_dir().join(format!("buildlang_sci_mc_executed_{}", std::process::id())); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create mc-executed fixture dir"); + + let mc_executed_flags = [ + "--mc-executed", + "--mc-estimator", + "proportion", + "--mc-samples", + "2000", + "--mc-interval", + "wilson-95", + ]; + + // POSITIVE: the executed pi kernel PASSes, the block is sealed EXECUTED + // with a re-deriving interval and a witnessed denominator, and the + // receipt verifies (both Stage A and Stage B). + let pass_receipt = dir.join("mcpi_executed.json"); + let emit_pass = buildc() + .arg("run") + .arg(repo_example("mc_pi_rejection_executed.bld")) + .args(["--emit-receipt"]) + .arg(&pass_receipt) + .args([ + "--invariant", + "non-negative", + "--metric", + "slack", + "--problem", + "mc-pi-rejection-executed", + "--seed", + "42", + ]) + .args(mc_executed_flags) + .output() + .expect("emit mc-executed PASS receipt"); + assert!( + emit_pass.status.success(), + "emitting the mc-executed PASS receipt should succeed\nstderr:\n{}", + String::from_utf8_lossy(&emit_pass.stderr) + ); + let pass: serde_json::Value = + serde_json::from_slice(&fs::read(&pass_receipt).expect("read PASS receipt")).unwrap(); + assert_eq!(pass["receipt_status"], "PASS"); + assert_eq!(pass["monte_carlo"]["status"], "EXECUTED"); + assert_eq!(pass["monte_carlo"]["n_effective"], 2000); + let successes = pass["monte_carlo"]["successes"] + .as_u64() + .expect("successes must be present"); + assert!(successes <= 2000); + let estimate = pass["monte_carlo"]["estimate"].as_f64().unwrap(); + let low = pass["monte_carlo"]["interval_low"].as_f64().unwrap(); + let high = pass["monte_carlo"]["interval_high"].as_f64().unwrap(); + assert!( + low < estimate && estimate < high, + "interval_low < estimate < interval_high must hold: {low} < {estimate} < {high}" + ); + let verify_pass = buildc() + .args(["receipt", "verify"]) + .arg(&pass_receipt) + .output() + .expect("verify mc-executed PASS receipt"); + assert!( + verify_pass.status.success(), + "the mc-executed PASS receipt must verify\nstderr:\n{}", + String::from_utf8_lossy(&verify_pass.stderr) + ); + + // NEGATIVE fixture: the wrong-area estimator still executes and + // re-derives a coherent interval (the raw successes/trials counters are + // untouched by the wrong-area factor), while the slack column blows the + // truth band and FAILs as declared. The interval claim and the + // truth-band claim fail independently. + let fail_receipt = dir.join("mcpi_executed_broken.json"); + let emit_fail = buildc() + .arg("run") + .arg(repo_example("mc_pi_rejection_executed_broken.bld")) + .args(["--emit-receipt"]) + .arg(&fail_receipt) + .args([ + "--invariant", + "non-negative", + "--negative-fixture", + "--metric", + "slack", + "--problem", + "mc-pi-rejection-executed", + "--seed", + "42", + ]) + .args(mc_executed_flags) + .output() + .expect("emit mc-executed negative fixture"); + assert!( + emit_fail.status.success(), + "emitting the mc-executed negative fixture should succeed\nstderr:\n{}", + String::from_utf8_lossy(&emit_fail.stderr) + ); + let fail: serde_json::Value = + serde_json::from_slice(&fs::read(&fail_receipt).expect("read FAIL receipt")).unwrap(); + assert_eq!(fail["receipt_status"], "FAIL_EXPECTED"); + assert_eq!( + fail["monte_carlo"]["status"], "EXECUTED", + "the wrong-area estimator still yields a coherent, re-deriving EXECUTED interval" + ); + let verify_fail = buildc() + .args(["receipt", "verify"]) + .arg(&fail_receipt) + .output() + .expect("verify mc-executed negative fixture"); + assert!( + verify_fail.status.success(), + "a faithfully reproduced FAIL_EXPECTED must verify (exit 0)\nstderr:\n{}", + String::from_utf8_lossy(&verify_fail.stderr) + ); + + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn mc_executed_without_full_declaration_is_refused() { + if !c_backend_ready() { + eprintln!("skipping mc_executed_without_full_declaration_is_refused: C backend not ready"); + return; + } + let dir = std::env::temp_dir().join(format!( + "buildlang_sci_mc_executed_refuse_partial_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + let refused = buildc() + .arg("run") + .arg(repo_example("mc_pi_rejection_executed.bld")) + .args(["--emit-receipt"]) + .arg(dir.join("partial.json")) + .args([ + "--invariant", + "non-negative", + "--seed", + "42", + "--mc-executed", + ]) + .output() + .expect("run --mc-executed with no other mc flags"); + assert!( + !refused.status.success(), + "--mc-executed alone must be refused" + ); + assert!( + String::from_utf8_lossy(&refused.stderr) + .contains("requires the full Monte Carlo declaration"), + "the refusal must name the all-or-nothing contract\nstderr:\n{}", + String::from_utf8_lossy(&refused.stderr) + ); + + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn mc_executed_clopper_pearson_is_refused() { + if !c_backend_ready() { + eprintln!("skipping mc_executed_clopper_pearson_is_refused: C backend not ready"); + return; + } + let dir = std::env::temp_dir().join(format!( + "buildlang_sci_mc_executed_refuse_clopper_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + let refused = buildc() + .arg("run") + .arg(repo_example("mc_pi_rejection_executed.bld")) + .args(["--emit-receipt"]) + .arg(dir.join("clopper.json")) + .args(["--invariant", "non-negative", "--seed", "42"]) + .args([ + "--mc-executed", + "--mc-estimator", + "proportion", + "--mc-samples", + "2000", + "--mc-interval", + "clopper-pearson-95", + ]) + .output() + .expect("run --mc-executed with clopper-pearson-95"); + assert!( + !refused.status.success(), + "clopper-pearson-95 must be refused (not executable in v1)" + ); + let stderr = String::from_utf8_lossy(&refused.stderr); + assert!( + stderr.contains("not in the EXECUTED executable vocabulary") + || stderr.contains("inverse incomplete beta"), + "the refusal must name the unexecutable method\nstderr:\n{}", + stderr + ); + + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn mc_executed_declared_samples_mismatching_witnessed_trials_is_refused() { + if !c_backend_ready() { + eprintln!( + "skipping mc_executed_declared_samples_mismatching_witnessed_trials_is_refused: C backend not ready" + ); + return; + } + let dir = std::env::temp_dir().join(format!( + "buildlang_sci_mc_executed_refuse_denominator_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + // A tiny kernel that prints exactly 5 post-burn rows (trials_final = 5), + // declared under --mc-samples 2000: the witnessed denominator does not + // equal the declared one. + let src = "fn main() ~ Console + Random {\n\ + let n: i32 = 5;\n\ + let mut inside: i32 = 0;\n\ + let mut k: i32 = 0;\n\ + while k < n {\n\ + let x: f64 = random_f64();\n\ + if x < 0.5 { inside = inside + 1; }\n\ + k = k + 1;\n\ + println!(\"{} {} {}\", 1.0, inside, k);\n\ + }\n\ + }\n"; + let path = dir.join("mc_five_rows.bld"); + fs::write(&path, src).expect("write mc_five_rows.bld"); + + let refused = buildc() + .arg("run") + .arg(&path) + .args(["--emit-receipt"]) + .arg(dir.join("mismatch.json")) + .args(["--invariant", "non-negative", "--seed", "42"]) + .args([ + "--mc-executed", + "--mc-estimator", + "proportion", + "--mc-samples", + "2000", + "--mc-interval", + "wilson-95", + ]) + .output() + .expect("run --mc-executed on a kernel with fewer draws than declared"); + assert!( + !refused.status.success(), + "a witnessed/declared denominator mismatch must be refused" + ); + assert!( + String::from_utf8_lossy(&refused.stderr).contains("does not equal the declared samples"), + "the refusal must name the denominator mismatch\nstderr:\n{}", + String::from_utf8_lossy(&refused.stderr) + ); + + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn mc_executed_incoherent_successes_jump_is_refused() { + if !c_backend_ready() { + eprintln!("skipping mc_executed_incoherent_successes_jump_is_refused: C backend not ready"); + return; + } + let dir = std::env::temp_dir().join(format!( + "buildlang_sci_mc_executed_refuse_jump_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + // A tiny kernel whose "successes" column jumps by 2 between row 0 (k=1, + // successes=0) and row 1 (k=2, successes=2): never exceeds trials at any + // row, but is not a coherent cumulative Bernoulli count (a delta of 2 + // is neither 0 nor 1). + let src = "fn main() ~ Console + Random {\n\ + let mut k: i32 = 0;\n\ + while k < 3 {\n\ + let x: f64 = random_f64();\n\ + let _unused: f64 = x;\n\ + k = k + 1;\n\ + let mut succ: i32 = 0;\n\ + if k >= 2 { succ = k; }\n\ + println!(\"{} {} {}\", 1.0, succ, k);\n\ + }\n\ + }\n"; + let path = dir.join("mc_jump.bld"); + fs::write(&path, src).expect("write mc_jump.bld"); + + let refused = buildc() + .arg("run") + .arg(&path) + .args(["--emit-receipt"]) + .arg(dir.join("jump.json")) + .args(["--invariant", "non-negative", "--seed", "42"]) + .args([ + "--mc-executed", + "--mc-estimator", + "proportion", + "--mc-samples", + "3", + "--mc-interval", + "wilson-95", + ]) + .output() + .expect("run --mc-executed on a kernel with an incoherent successes jump"); + assert!( + !refused.status.success(), + "a successes column jumping by 2 must be refused" + ); + let stderr = String::from_utf8_lossy(&refused.stderr); + assert!( + stderr.contains("does not follow") && stderr.contains("by 0 or 1"), + "the refusal must name the incoherent jump\nstderr:\n{}", + stderr + ); + + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn mc_executed_explicit_columns_other_than_three_is_refused() { + if !c_backend_ready() { + eprintln!( + "skipping mc_executed_explicit_columns_other_than_three_is_refused: C backend not ready" + ); + return; + } + let dir = std::env::temp_dir().join(format!( + "buildlang_sci_mc_executed_refuse_columns_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + let refused = buildc() + .arg("run") + .arg(repo_example("mc_pi_rejection_executed.bld")) + .args(["--emit-receipt"]) + .arg(dir.join("columns.json")) + .args([ + "--invariant", + "non-negative", + "--seed", + "42", + "--columns", + "2", + ]) + .args([ + "--mc-executed", + "--mc-estimator", + "proportion", + "--mc-samples", + "2000", + "--mc-interval", + "wilson-95", + ]) + .output() + .expect("run --mc-executed with an explicit --columns 2"); + assert!( + !refused.status.success(), + "an explicit --columns other than 3 must be refused under --mc-executed" + ); + assert!( + String::from_utf8_lossy(&refused.stderr).contains("needs --columns 3"), + "the refusal must name the required column count\nstderr:\n{}", + String::from_utf8_lossy(&refused.stderr) + ); + + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn mc_executed_normal_approx_degenerate_boundary_is_refused() { + if !c_backend_ready() { + eprintln!( + "skipping mc_executed_normal_approx_degenerate_boundary_is_refused: C backend not ready" + ); + return; + } + let dir = std::env::temp_dir().join(format!( + "buildlang_sci_mc_executed_refuse_degenerate_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + // A tiny kernel whose counter never fails a single draw: successes == + // trials on every row, so the final proportion sits at the 1.0 boundary. + let src = "fn main() ~ Console + Random {\n\ + let n: i32 = 5;\n\ + let mut k: i32 = 0;\n\ + while k < n {\n\ + let x: f64 = random_f64();\n\ + let _unused: f64 = x;\n\ + k = k + 1;\n\ + println!(\"{} {} {}\", 1.0, k, k);\n\ + }\n\ + }\n"; + let path = dir.join("mc_always_succeeds.bld"); + fs::write(&path, src).expect("write mc_always_succeeds.bld"); + + let refused = buildc() + .arg("run") + .arg(&path) + .args(["--emit-receipt"]) + .arg(dir.join("degenerate.json")) + .args(["--invariant", "non-negative", "--seed", "42"]) + .args([ + "--mc-executed", + "--mc-estimator", + "proportion", + "--mc-samples", + "5", + "--mc-interval", + "normal-approx-95", + ]) + .output() + .expect("run --mc-executed on a boundary-proportion kernel with normal-approx-95"); + assert!( + !refused.status.success(), + "a boundary proportion under normal-approx-95 must be refused" + ); + let stderr = String::from_utf8_lossy(&refused.stderr); + assert!( + stderr.contains("degenerate") && stderr.contains("wilson-95"), + "the refusal must name the degeneracy and point at wilson-95\nstderr:\n{}", + stderr + ); + + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn mc_executed_refused_with_gpu() { + // No `c_backend_ready()` gate needed: this refusal fires on CLI shape + // before any GPU device probe or receipt work (mirroring the existing + // --gpu/--budget-wall-seconds composition test). + let dir = std::env::temp_dir().join(format!( + "buildlang_sci_mc_executed_refuse_gpu_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + let refused = buildc() + .arg("run") + .arg(repo_example("decay_cross_backend.bld")) + .args([ + "--gpu", + "--mc-executed", + "--mc-estimator", + "proportion", + "--mc-samples", + "2000", + "--mc-interval", + "wilson-95", + ]) + .output() + .expect("run --gpu --mc-executed together"); + assert!( + !refused.status.success(), + "--gpu combined with --mc-executed must be refused" + ); + assert!( + String::from_utf8_lossy(&refused.stderr) + .contains("--mc-* flags are not supported with --gpu"), + "the refusal must name the gpu/mc composition\nstderr:\n{}", + String::from_utf8_lossy(&refused.stderr) + ); + + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn mc_executed_refused_with_cross_backend() { + if !c_backend_ready() { + eprintln!("skipping mc_executed_refused_with_cross_backend: C backend not ready"); + return; + } + let dir = std::env::temp_dir().join(format!( + "buildlang_sci_mc_executed_refuse_cross_backend_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + let refused = buildc() + .arg("run") + .arg(repo_example("decay_cross_backend.bld")) + .args(["--emit-receipt"]) + .arg(dir.join("cb_mc_executed.json")) + .args(["--cross-backend", "rust", "--invariant", "cross-backend"]) + .args([ + "--mc-executed", + "--mc-estimator", + "proportion", + "--mc-samples", + "2000", + "--mc-interval", + "wilson-95", + ]) + .output() + .expect("run --cross-backend --mc-executed together"); + assert!( + !refused.status.success(), + "--cross-backend combined with --mc-executed must be refused" + ); + // The column-count gate is the FIRST refusal to fire here (Task 3's + // `column_count_matches_invariant` update makes the cross-backend arm + // require `!mc_executed`, so it refuses for ANY --columns value once + // mc_executed is true), ahead of the later `mc_flag_count > 0` check + // inside the `--cross-backend` block. Both gates independently cover + // this composition; the column gate simply wins the race. + assert!( + String::from_utf8_lossy(&refused.stderr) + .contains("--invariant cross-backend needs --columns 2"), + "the refusal must name the cross-backend column contract\nstderr:\n{}", + String::from_utf8_lossy(&refused.stderr) + ); + + let _ = fs::remove_dir_all(&dir); +} + #[test] fn budget_declaration_round_trips_and_pins_the_admission_contract() { if !c_backend_ready() { @@ -15875,8 +16417,8 @@ fn receipt_verify_self_test_proves_the_verifier_can_fail() { ); let stdout = String::from_utf8_lossy(&self_test.stdout); assert!( - stdout.contains("9/9 tampers rejected with the expected failure_class"), - "self-test should report all nine tampers rejected\nstdout:\n{}", + stdout.contains("10/10 tampers rejected with the expected failure_class"), + "self-test should report all ten tampers rejected\nstdout:\n{}", stdout ); // The taxonomy arms actually exercised must appear in the report. @@ -16064,8 +16606,8 @@ fn receipt_corpus_asserts_declared_classifications() { assert_eq!(shipped["schema"], "buildlang-scientific-receipt-corpus/v0"); assert_eq!( shipped["members"].as_array().unwrap().len(), - 27, - "the shipped corpus should cover all thirteen kernel pairs plus the cross-backend singleton" + 29, + "the shipped corpus should cover all fourteen kernel pairs plus the cross-backend singleton" ); // A small correct manifest: the command emits, verifies, and confirms each diff --git a/docs/SCIENTIFIC-RECEIPT.md b/docs/SCIENTIFIC-RECEIPT.md index c3003990..75ea8f05 100644 --- a/docs/SCIENTIFIC-RECEIPT.md +++ b/docs/SCIENTIFIC-RECEIPT.md @@ -103,6 +103,17 @@ Flags on the `run` subcommand (all additive; absent `--emit-receipt`, none of th zero sample count is refused as an unpriceable denominator, and the declaration requires a `Random`-observing program with a seed (an MC claim over a stream that cannot re-derive is worthless as evidence). +- `--mc-executed` upgrades the declaration to EXECUTED: the verifier RE-DERIVES the interval + from raw sufficient-statistic columns the kernel prints (successes/trials counters beside + the invariant scalar) instead of trusting it. Requires all three `--mc-*` flags together + (`--mc-executed` alone is refused), and `--mc-estimator` must be `proportion` (v1's only + executable estimator; DECLARED blocks may still use free text). `--columns` is forced to 3 + (an unset default of 1 is silently upgraded, any other explicit value is refused, the + `--cross-backend` idiom). Fail-closed at emit: an incoherent EXECUTED block (a bad + successes/trials stream, a witnessed denominator that disagrees with `--mc-samples`, an + unexecutable `--mc-interval`, or a degenerate boundary proportion under + `normal-approx-95`) is refused before the receipt is sealed, never sealed as if it were + coherent. - `--budget-steps `, `--budget-consumed ` declare the run a budgeted search and seal the step ceiling, the consumption, and a DERIVED `exhausted` flag as the receipt's `budget` block. Both declare together or not at all (a result without its budget ceiling @@ -215,15 +226,51 @@ The receipt is a single JSON object. Its layers, outermost meaning first: - `numerical_method`: `{ description?, status }`, author-DECLARED via `--method` (buildc cannot derive scheme semantics from source and does not pretend to); an inconsistent status/description pair is rejected (`FIELD_CONTRACT_VIOLATION`). -- `monte_carlo` (optional): `{ estimator, samples, interval_method, status }`, the MC - admission block from the `--mc-*` flags. Author-declared like `numerical_method`, but - with hard shape contracts verify re-checks (`FIELD_CONTRACT_VIOLATION`): it rides only - on a seeded `Random` run, `samples` is non-zero, `estimator` and `interval_method` are - non-empty, and `status` is `DECLARED` (v0 states the facts, it does not execute them). +- `monte_carlo` (optional): `{ estimator, samples, interval_method, status, estimate?, + interval_low?, interval_high?, n_effective?, successes? }`, the MC admission block from + the `--mc-*` flags. Author-declared, with hard shape contracts verify re-checks + (`FIELD_CONTRACT_VIOLATION`): it rides only on a seeded `Random` run, `samples` is + non-zero, `estimator` and `interval_method` are non-empty, and `status` is one of two + values. + - `DECLARED` (v0's original shape): the facts were stated, not independently executed; + the five `estimate`/`interval_low`/`interval_high`/`n_effective`/`successes` fields are + absent, and their presence on a DECLARED block is refused. `estimator`/`interval_method` + stay free text forever (the shipped corpus uses `mean`/`normal-approx-95`). + - `EXECUTED` (`--mc-executed`): the verifier RE-DERIVES the interval from raw + sufficient-statistic columns the kernel prints (a three-column series, + ` ` per row), never from the kernel's own + arithmetic, at TWO stages: Stage A over the SEALED `measurement.observed_values` before + any re-run (so a tampered-and-resealed interval is a pure data contradiction, rejectable + with no C compiler), and Stage B over the re-parsed re-run series (`MC_INTERVAL_DRIFT` + on disagreement, since a Stage-A-clean receipt that no longer describes the run it names + is a different kind of dishonesty than a tampered field). All five executed fields must + be present, and are refused when absent. The executable estimator vocabulary (v1) is + `proportion` only (the mean of Bernoulli indicators); the executable interval-method + vocabulary is `normal-approx-95` and `wilson-95` (`normal-approx-95` additionally + refused at the boundary proportion, successes = 0 or successes = trials, since a + zero-width interval there overclaims precision; the message points at `wilson-95`). + `clopper-pearson-95` is sealed-successes-only, not executable in v1 (it needs a verified + inverse incomplete beta with no in-tree oracle), and is refused at both emit and verify. + The aggregate columns must be structurally coherent as a cumulative Bernoulli count + (every value an exact integer below 2^53, `trials` incrementing by exactly 1 across + consecutive rows after the free first-row value, `successes` non-decreasing with + increments in `{0, 1}`, `successes <= trials` on every row), and the final row's + `trials` MUST equal the declared `samples`: the witnessed-denominator equality, the + single biggest honesty gain of the EXECUTED shape. Float fields are compared within a + pinned absolute tolerance (`1e-12`) in both stages. An EXECUTED block additionally adds + three `not_claimed` entries -- `sample_independence`, `interval_coverage`, + `estimator_semantics` -- present if and only if `status == "EXECUTED"` (the + `NOT_PROVES_OPTIMALITY`/`optimality` pairing idiom): EXECUTED hardens the interval + arithmetic and the denominator, but 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 the admission rule for the weakest-promise mode: deterministic work needs only a hash, but an MC number without its denominator, seed, and interval method is - unpriceable, so the receipt refuses to exist without them. v0 claims REPRODUCIBILITY - and declaration discipline, never correctness of the interval. + unpriceable, so the receipt refuses to exist without them. DECLARED claims + REPRODUCIBILITY and declaration discipline, never correctness of the interval; EXECUTED + hardens the interval arithmetic and the witnessed denominator, never the estimator's + semantics or independence. - `budget` (optional): `{ steps_limit, steps_consumed, exhausted, status, wall_seconds_limit?, wall_exceeded? }`, the budgeted-search admission block from the `--budget-*` flags. Author-declared like `monte_carlo`, but with hard shape contracts verify re-checks @@ -324,6 +371,17 @@ a receipt cannot weaken its own check. | `non-negative` | `non_negative` | `s[k] < -tol` (dropped below zero) | `1e-9` | | `cross-backend` (`--cross-backend `, `--columns` forced to 2) | `cross_backend_columns_agree` | the C-anchor and secondary-lane columns of a row differ by more than `tol` (the same evaluator as `relation`) | `1e-5` | +An EXECUTED `monte_carlo` receipt (`--mc-executed`, `--columns` forced to 3) takes any +single-scalar invariant name above (never `relation`/`cross-backend`: their columns already +mean something else, and `column_count_matches_invariant` refuses the pairing). The row is +` `; `evaluate_measurement` DE-INTERLEAVES it, +evaluating the named invariant over column 0 only, with columns 1-2 left for +`compute_mc_executed`'s separate coherence and interval re-derivation. The effective +observation count for the "at least two points" verdict rule is the ROW count, mirroring +how `relation` counts rows rather than raw tokens. A ragged three-column series (length not +a multiple of 3) yields zero rows, the same "cannot witness" treatment a ragged `relation` +series gets. + The `conservation` and `bounded` references are both `s[0]` (the initial value), not the mean, so a re-run that reproduces a different-length prefix cannot shift the reference. The checks are genuinely distinct: `conservation` fences BOTH sides of `s[0]`, `bounded` fences only the @@ -601,7 +659,7 @@ fixtures and CI pin the *specific* failure instead of accepting "anything failed | `DIGEST_MALFORMED` | a sealed digest field is not a real sha256 (64 hex chars); an absent hash cannot masquerade as witnessed provenance | 1 | | `ORACLE_KIND_UNSUPPORTED`, `ORACLE_STATUS_UNSUPPORTED`, `ORACLE_BINDING_MISMATCH`, `INVARIANT_UNSUPPORTED` | the oracle/invariant block names a kind, status, or criterion this verifier does not implement; binding is pinned to the implementation, never to another sealed field | 1 | | `FENCE_STATUS_UNEXPECTED` | a telemetry/lineage fence was edited to claim availability v0 does not produce | 1 | -| `FIELD_CONTRACT_VIOLATION` | a sealed field claims something the program cannot express (a `seed_value` when nothing observes `Random`, a Random-using program with no sealed seed, a `monte_carlo` block without a seeded Random run or with a zero/nameless denominator, estimator, or interval method, a `budget` block with a zero ceiling, consumption above its ceiling, a hand-set `exhausted`, or a non-`DECLARED` status, a `budget.wall_seconds_limit` that is non-positive or non-finite, present without a sealed `runtime_state.wall_seconds`, or paired with a `wall_exceeded` that disagrees with the SEALED `wall_seconds > wall_seconds_limit` comparison, a `wall_exceeded` present without `wall_seconds_limit`, a `cross_backend` block present without the `cross_backend_columns_agree` invariant or that invariant without the block (the biconditional), a non-`rust` `cross_backend.secondary_target`, a non-`EXECUTED` `cross_backend.status`, a `cross_backend` block whose RE-DERIVED capabilities include `Random` (the Rust lane has no seeded PRNG, so the streams could not agree; this transitively excludes a `monte_carlo` block riding along too, since MC requires `Random`), or a `NOT_PROVES_OPTIMALITY`/`optimality` pairing or claim-language mismatch), is internally inconsistent (DECLARED method, no description), or resealed a non-canonical `invariant.tolerance` | 1 | +| `FIELD_CONTRACT_VIOLATION` | a sealed field claims something the program cannot express (a `seed_value` when nothing observes `Random`, a Random-using program with no sealed seed, a `monte_carlo` block without a seeded Random run or with a zero/nameless denominator, estimator, or interval method, a status outside `DECLARED`/`EXECUTED`, a `budget` block with a zero ceiling, consumption above its ceiling, a hand-set `exhausted`, or a non-`DECLARED` status, a `budget.wall_seconds_limit` that is non-positive or non-finite, present without a sealed `runtime_state.wall_seconds`, or paired with a `wall_exceeded` that disagrees with the SEALED `wall_seconds > wall_seconds_limit` comparison, a `wall_exceeded` present without `wall_seconds_limit`, a `cross_backend` block present without the `cross_backend_columns_agree` invariant or that invariant without the block (the biconditional), a non-`rust` `cross_backend.secondary_target`, a non-`EXECUTED` `cross_backend.status`, a `cross_backend` block whose RE-DERIVED capabilities include `Random` (the Rust lane has no seeded PRNG, so the streams could not agree; this transitively excludes a `monte_carlo` block riding along too, since MC requires `Random`), or a `NOT_PROVES_OPTIMALITY`/`optimality` pairing or claim-language mismatch), is internally inconsistent (DECLARED method, no description), or resealed a non-canonical `invariant.tolerance`. The EXECUTED `monte_carlo` sub-cases: an executed field (`estimate`/`interval_low`/`interval_high`/`n_effective`/`successes`) present on a DECLARED block, or one of the five ABSENT on an EXECUTED block; an EXECUTED `estimator`/`interval_method` outside the v1 executable vocabulary (`proportion`; `normal-approx-95`, `wilson-95`); a `column_count` other than 3 on an EXECUTED block; an incoherent aggregate successes/trials stream (non-integer, a trials step other than +1, a successes step outside `{0, 1}`, `successes > trials`); a witnessed final `trials` that disagrees with the declared `samples` (the denominator is not witnessed); the Stage A recompute (over the sealed series) disagreeing with the sealed `estimate`/`interval_low`/`interval_high`/`n_effective`/`successes`; and the `sample_independence`/`interval_coverage`/`estimator_semantics` `not_claimed` triad biconditional | 1 | | `EFFECT_POLICY_DRIFT` | the sealed effect/capability facts, or the witnessed fields derived from them, do not re-derive from the source | 1 | | `CAPABILITY_INADMISSIBLE` | the RE-DERIVED capabilities include `Model`: a scientific receipt cannot witness a model-mediated run (models propose, oracles dispose) | 1 | | `TOOL_UNAVAILABLE` | no C compiler available for the re-run | 4 | @@ -610,6 +668,7 @@ fixtures and CI pin the *specific* failure instead of accepting "anything failed | `RERUN_EXIT_MISMATCH` | the re-run's process exit code differs from the sealed one (covers a crashing re-run) | 1 | | `SOURCE_DIGEST_MISMATCH`, `INPUT_GRAPH_DIGEST_MISMATCH` | the source changed since sealing | 1 | | `MEASUREMENT_COUNT_DRIFT`, `INVARIANT_STATUS_DRIFT`, `VIOLATION_COUNT_DRIFT`, `RECEIPT_STATUS_DRIFT` | the re-run disagrees with a stored verdict fact | 1 | +| `MC_INTERVAL_DRIFT` | an EXECUTED `monte_carlo` receipt's sealed interval fields do not match the Stage B recompute over the re-run series (Stage A already passed over the sealed series; this catches a receipt that stopped describing the run it names) | 1 | | `SEAL_MISMATCH` | the stored receipt body does not re-seal | 1 | | `INVARIANT_NOT_HELD` | faithful receipt, but the recorded verdict is `FAIL_UNEXPECTED` or `UNVERIFIABLE` | 3 | @@ -633,24 +692,29 @@ Given a valid scientific-runtime receipt, it tampers several distinct sealed fie that each tamper is rejected by the real verify path with its expected `failure_class`. Cases that keep the body well-formed are re-sealed (so the tamper passes the integrity gate and reaches the specific contract check under test); the seal-mismatch case is deliberately left unsealed. -The current nine cases exercise five separate arms of the taxonomy: `COMPILER_MISMATCH` +The current ten cases exercise five separate arms of the taxonomy: `COMPILER_MISMATCH` (foreign compiler tag), `SEAL_MISMATCH` (a witnessed value edited without re-sealing), -`MALFORMED` (a required field removed), `FIELD_CONTRACT_VIOLATION` (five times, through +`MALFORMED` (a required field removed), `FIELD_CONTRACT_VIOLATION` (six times, through different gates: a sealed tolerance loosened then re-sealed, the sealed `seed_value` flipped against the program's capabilities then re-sealed, a `monte_carlo` block given a zero sample denominator then re-sealed, a `budget` block given a `steps_consumed` above -`steps_limit` then re-sealed, and the sealed `cross_backend` block swapped against the +`steps_limit` then re-sealed, the sealed `cross_backend` block swapped against the invariant name -- removed if present, added with a syntactically valid shape if absent -- -then re-sealed), and `INVARIANT_UNSUPPORTED` (an unknown invariant name, -re-sealed). Every case is rejected before any program re-run, so `--self-test` needs no C -compiler (and no rustc): the seed-pairing, MC, budget, and cross-backend cases are rejected at -the source re-derivation stage or the field-contract gate, so they (alone) need the receipt's -source file readable, exactly as `buildc check` would. It exits 0 only if every tamper produced -its expected class, and prints `self-test: N/N tampers rejected with the expected -failure_class`. There is no tenth case for the wall-metering fields: a tampered -`wall_exceeded` or `wall_seconds_limit` is rejected through the exact same -`FIELD_CONTRACT_VIOLATION` arm the budget case (case 8) already exercises, so a tenth case -would prove nothing the ninth does not already prove. +then re-sealed, and case 10: an EXECUTED `monte_carlo` block's sealed `interval_high` +nudged against its Stage A recompute -- the receipt's own block if it already carries one +(e.g. a receipt emitted from `mc_pi_rejection_executed.bld`), else a syntactically valid +one is added, mirroring case 9's `cross_backend` fallback -- then re-sealed), and +`INVARIANT_UNSUPPORTED` (an unknown invariant name, re-sealed). Every case is rejected +before any program re-run, so `--self-test` needs no C compiler (and no rustc): the +seed-pairing, MC, budget, cross-backend, and EXECUTED-interval cases are rejected at the +source re-derivation stage or the field-contract gate (Stage A, in the EXECUTED case), +so they (alone) need the receipt's source file readable, exactly as `buildc check` would. +It exits 0 only if every tamper produced its expected class, and prints `self-test: N/N +tampers rejected with the expected failure_class`. Case 10 is robust to WHICHEVER Stage A +gate fires first (seed pairing, field presence, or the interval-mismatch check it targets) +on an arbitrary pristine input: every pre-re-run EXECUTED violation this slice adds +reports `FIELD_CONTRACT_VIOLATION`, the same class case 7's zero-denominator tamper +already relies on regardless of which specific MC gate fires first. ### Chaining receipts (`receipt chain`) @@ -680,14 +744,15 @@ probabilistic-exact, stochastic, Monte Carlo, heuristic, plus the cross-backend The example kernels come in positive/negative pairs, each declared to PASS or to FAIL_EXPECTED under a named invariant. `examples/scientific-corpus.json` records that ground truth for all -thirteen pairs plus the cross-backend singleton (a member whose kernel draws from +fourteen pairs plus the cross-backend singleton (a member whose kernel draws from `random_f64()` also declares its `seed`, which the runner passes as `--seed`, an MC member -declares `mc_estimator` / `mc_samples` / `mc_interval`, passed through the same way, a budgeted -member declares `budget_steps` / `budget_consumed`, passed through as `--budget-steps` / -`--budget-consumed`, and the cross-backend member declares `cross_backend`, passed through as -`--cross-backend`; a Random member with no declared seed, or a partial MC or budget -declaration, fails the corpus loudly, because emit refuses it), and one command checks reality -against it: +declares `mc_estimator` / `mc_samples` / `mc_interval`, passed through the same way, an +EXECUTED MC member additionally declares `mc_executed: true`, passed through as +`--mc-executed`, a budgeted member declares `budget_steps` / `budget_consumed`, passed +through as `--budget-steps` / `--budget-consumed`, and the cross-backend member declares +`cross_backend`, passed through as `--cross-backend`; a Random member with no declared seed, +or a partial MC or budget declaration, fails the corpus loudly, because emit refuses it), +and one command checks reality against it: ``` buildc receipt corpus examples/scientific-corpus.json diff --git a/docs/superpowers/plans/2026-07-29-mc-executed-intervals.md b/docs/superpowers/plans/2026-07-29-mc-executed-intervals.md new file mode 100644 index 00000000..688e37ae --- /dev/null +++ b/docs/superpowers/plans/2026-07-29-mc-executed-intervals.md @@ -0,0 +1,973 @@ +# w1: Monte Carlo EXECUTED interval discipline (implementation plan, DRAFT) + +> **For agentic workers:** REQUIRED SUB-SKILL: superpowers:subagent-driven-development +> (recommended) or superpowers:executing-plans, task-by-task. + +**Scope verdict (read first).** This is ONE commit, comparable in shape to the prior +scientific-runtime slices (slice 2, `docs/superpowers/plans/2026-07-28-mc-estimator-receipts.md`, +commit `9430439`, which added the DECLARED `monte_carlo` block this slice extends): one +schema extension (five `Option` fields plus a two-arm status), one shared pure recompute +function called from three sites (emit, verify stage A, verify stage B), one new CLI flag, +one new kernel pair, one new corpus pair, one new self-test case, and the matching docs. +No prerequisite is missing: the DECLARED `monte_carlo` block, the multi-column capture +machinery (`column_count`, `relation_columns_agree`, `evaluate_measurement`), and the +EXECUTED-status precedent (`cross_backend`) all already ship. + +**Goal.** Upgrade `monte_carlo` from a DECLARED-only admission block to a two-arm +`DECLARED | EXECUTED` block where an EXECUTED receipt seals a Wilson or normal-approx-95 +interval the verifier RE-DERIVES from raw sufficient-statistic columns the kernel prints +(cumulative `successes`/`trials` counters beside the existing invariant scalar), never +from the kernel's own arithmetic. Mechanism: the kernel prints exactly three columns per +post-burn-in row, ` `; a new shared function +`compute_mc_executed` de-interleaves them, checks structural coherence as a cumulative +Bernoulli count, and recomputes the interval, entirely in verifier-owned code. Emit calls +it once (fail closed: an incoherent EXECUTED block is never sealed). Verify calls it +TWICE: Stage A over the sealed `measurement.observed_values` (no re-run, so a +tampered-and-resealed interval is a pure data contradiction, rejectable before any program +re-run, keeping the self-test's no-compiler property intact), and Stage B over the +re-parsed re-run series (a new failure class, `MC_INTERVAL_DRIFT`, since a Stage-A-clean +receipt that no longer describes the run it names is a different kind of dishonesty than a +tampered field). What EXECUTED can never claim — sample independence, interval coverage, +estimator semantics — is sealed as three new `not_claimed` entries, present iff the block +is EXECUTED, mirroring the `NOT_PROVES_OPTIMALITY`/`optimality` pairing idiom the budget +block already uses. + +**Source of truth.** `.superpowers/sdd/w1-mc-executed-design-DRAFT.md`. This plan +implements it exactly; every deviation below is either a design line-anchor correction +(verified by reading the current file) or a decision the design explicitly left open, +marked inline with one sentence of rationale. No other deviation is authorized. + +**Controller-pinned counts (override the design doc's numbers).** Corpus 27 -> 29 +(thirteen pairs plus the cross-backend singleton, plus this slice's new pair). Self-test +9 -> 10. Every count in this plan uses these. + +## Global constraints + +- ONE commit on branch `feat/mc-executed-intervals`. The stack base (which commit or + branch it is created from) is decided by the controller at dispatch time, not by this + plan: do not assume the HEAD current when this plan was drafted (`0fc3406`, branch + `feat/units-in-types`, being actively edited by a concurrent agent on + `compiler/src/types/infer.rs`) is the base merely because it was HEAD at draft time. Do + not push. +- Backward compatibility is absolute: every scientific-runtime receipt sealed before this + slice parses and re-serializes to its EXACT bytes and seal. The five new + `ScientificMonteCarlo` fields are `Option` with + `#[serde(default, skip_serializing_if = "Option::is_none")]`, the `ScientificBudget` + precedent (`compiler/src/scientific_runtime.rs:306-309`). `ScientificMonteCarlo` loses + `Eq` (gains `f64` fields), same precedent. Schema stays `v0`. +- `--mc-executed` is opt-in; the DECLARED emission path (all 27 existing corpus members) + is byte-for-byte untouched. +- Every new gate is mutation-tested: break it, observe the specific test go red, restore + it, observe green. Task 9 enumerates every gate this slice adds. +- No em-dashes in any prose or code comment this commit adds (repo-wide voice rule). +- Exit codes are captured before any pipe in every verification command run for this + slice (the pipes-swallow-exit-codes trap); never `| tail` or `| grep` a gate command + without capturing `$?`/`%ERRORLEVEL%` first. +- `cargo fmt --check` clean. +- `buildc corpus verify examples/scientific-corpus.json` reports `29/29`. +- `buildc receipt verify .json --self-test` reports `10/10`. +- Full `cargo test` from `compiler/` reports 0 failed (baseline before this slice: confirm + the count by running it once at the start of Task 11; do not assume a stale number). + +## Task 1: schema extension (`compiler/src/scientific_runtime.rs`) + +- [ ] Extend `ScientificMonteCarlo` (currently lines 280-293: `estimator`, `samples`, + `interval_method`, `status`) with five `Option` fields, dropping `Eq` from the derive: + + ```rust + #[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] + pub struct ScientificMonteCarlo { + pub estimator: String, + pub samples: u64, + pub interval_method: String, + /// `DECLARED` | `EXECUTED`. + pub status: String, + /// p_hat = successes_final / trials_final. Present IFF `status == "EXECUTED"`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub estimate: Option, + /// Lower bound by the named method. Present IFF `status == "EXECUTED"`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub interval_low: Option, + /// Upper bound by the named method. Present IFF `status == "EXECUTED"`. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub interval_high: Option, + /// trials_final; MUST equal `samples`, the witnessed denominator. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub n_effective: Option, + /// successes_final. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub successes: Option, + } + ``` + +- [ ] Add the pinned vocabulary and tolerance constants, beside the other family + constants near the top of the file (after `CROSS_BACKEND_TOLERANCE`, line ~141): + + ```rust + /// Executed Monte Carlo estimator vocabulary, v1: the mean of Bernoulli + /// indicators. DECLARED blocks keep free text forever (the shipped corpus + /// uses `mean`); this vocabulary gates EXECUTED blocks only. + pub const MC_EXECUTED_ESTIMATOR_PROPORTION: &str = "proportion"; + + /// Executed interval method: normal approximation. Degenerate at a boundary + /// proportion (successes == 0 or successes == trials): refused at emit and + /// at verify, pointing at `wilson-95`. + pub const MC_INTERVAL_NORMAL_APPROX_95: &str = "normal-approx-95"; + + /// Executed interval method: Wilson score. Well-defined at the boundary + /// proportions, asymmetric by construction. + pub const MC_INTERVAL_WILSON_95: &str = "wilson-95"; + + /// NOT executable in v1 (needs an inverse incomplete beta with no in-tree + /// oracle). Named here only so refusal messages can point at it by + /// constant rather than a bare string; never accepted by + /// `compute_mc_executed`. + pub const MC_INTERVAL_CLOPPER_PEARSON_95: &str = "clopper-pearson-95"; + + /// z for a two-sided 95% normal/Wilson interval: the double nearest the + /// 0.975 standard-normal quantile. Shared by both executable methods. + pub const MC_INTERVAL_Z_95: f64 = 1.959963984540054; + + /// Absolute float tolerance for the emit/verify interval recompute + /// (`estimate`, `interval_low`, `interval_high`, both stages). The + /// arithmetic runs on identical integer inputs through one fixed Rust + /// implementation at emit and verify, so agreement should be exact in + /// practice; this is headroom against a future compiler reassociating + /// verifier-side float ops, not load-bearing looseness. Values are O(1) + /// proportions, so absolute is safe. + pub const MC_RECOMPUTE_TOLERANCE: f64 = 1e-12; + + /// The three `not_claimed` entries an EXECUTED monte_carlo block adds, + /// present iff `status == "EXECUTED"` (the `NOT_PROVES_OPTIMALITY`/ + /// `optimality` pairing idiom). EXECUTED hardens the interval arithmetic + /// and the denominator; it cannot and does not claim these. + pub const MC_EXECUTED_NOT_CLAIMED: &[&str] = + &["sample_independence", "interval_coverage", "estimator_semantics"]; + ``` + +- [ ] Fix the existing test helper `mc()` inside + `verify_enforces_the_monte_carlo_admission_contracts` (currently lines 5715-5722): add + the five new fields as `None` so the struct literal compiles. +- [ ] Update the same test's `bad.status = "EXECUTED".to_string()` case (currently lines + 5780-5782, comment "A status v0 cannot honestly say is refused"): EXECUTED is now + expressible, so this specific literal (via `mc()`, which sets none of the five executed + fields) must still fail, but for a DIFFERENT reason: EXECUTED with no executed fields + present is `FIELD_CONTRACT_VIOLATION` (Task 4's field-presence gate), not an unknown + status. Reword the comment; the assertion (`Err(1)`) is unchanged. Add a sibling case + in the same test for `status` set to a third string (e.g. `"SIMULATED"`), which must + still be refused as an unknown status, so the two-arm vocabulary itself stays gated. + +## Task 2: `compute_mc_executed` (shared pure recompute, `scientific_runtime.rs`) + +This is the single function emit and both verify stages call, so all three can never +disagree on the math. Insert after `evaluate_measurement` (current lines 1041-1065). + +- [ ] Result type: + + ```rust + /// The recomputed EXECUTED monte_carlo fields, owned by the caller to + /// compare against the sealed ones (emit: seal them; verify: compare). + #[derive(Clone, Debug, PartialEq)] + pub struct McExecutedComputed { + pub estimate: f64, + pub interval_low: f64, + pub interval_high: f64, + pub n_effective: u64, + pub successes: u64, + } + ``` + +- [ ] The function: + + ```rust + /// Recompute the EXECUTED monte_carlo fields from a captured three-column + /// series (` ` per row), the + /// declared denominator, and the named interval method. PURE and + /// unit-tested; called from emit (fail closed before sealing), verify + /// Stage A (over the sealed series, before any re-run), and verify Stage B + /// (over the re-run series). Never trusts anything but the raw columns. + /// + /// Coherence checks, in order (Decision 1, design doc): every successes/ + /// trials value is integer-valued (`fract() == 0`) and below 2^53; trials + /// increments by exactly 1 across consecutive rows (the first row's + /// absolute value is free, the burn-in edge); successes is non-decreasing + /// with increments in {0, 1}; successes <= trials on every row; the final + /// row's trials equals `samples` (the witnessed-denominator equality). + /// `interval_method` must be one of the two executable methods + /// (`MC_INTERVAL_NORMAL_APPROX_95`, `MC_INTERVAL_WILSON_95`); any other + /// name (including `clopper-pearson-95`) is refused here, the single + /// source of truth for the executable vocabulary. `normal-approx-95` is + /// additionally refused at a boundary proportion (successes_final == 0 or + /// == trials_final): a zero-width interval there overclaims precision; + /// the message points at `wilson-95`. + pub fn compute_mc_executed( + series: &[f64], + column_count: usize, + samples: u64, + interval_method: &str, + ) -> Result { + const MAX_EXACT_INTEGER: f64 = 9007199254740992.0; // 2^53 + + if column_count != 3 { + return Err(format!( + "column_count {column_count} is not 3: an EXECUTED monte_carlo receipt requires exactly three columns per row" + )); + } + if series.is_empty() || series.len() % 3 != 0 { + return Err(format!( + "series length {} is not a positive multiple of 3: ragged rows cannot witness a Bernoulli count", + series.len() + )); + } + let rows = series.len() / 3; + + let mut prev_trials: Option = None; + let mut prev_successes: Option = None; + for k in 0..rows { + let successes_k = series[k * 3 + 1]; + let trials_k = series[k * 3 + 2]; + for (label, value) in [("successes", successes_k), ("trials", trials_k)] { + if value.fract() != 0.0 || !value.is_finite() || value.abs() >= MAX_EXACT_INTEGER { + return Err(format!( + "row {k}: {label} = {value} is not an exact non-negative integer below 2^53" + )); + } + } + if let Some(prev) = prev_trials { + if trials_k != prev + 1.0 { + return Err(format!( + "row {k}: trials {trials_k} does not follow row {}'s trials {prev} by exactly 1", + k - 1 + )); + } + } + if let Some(prev) = prev_successes { + let delta = successes_k - prev; + if delta != 0.0 && delta != 1.0 { + return Err(format!( + "row {k}: successes {successes_k} does not follow row {}'s successes {prev} by 0 or 1", + k - 1 + )); + } + } + if successes_k > trials_k { + return Err(format!( + "row {k}: successes {successes_k} exceeds trials {trials_k}" + )); + } + prev_trials = Some(trials_k); + prev_successes = Some(successes_k); + } + + let trials_final = prev_trials.expect("rows > 0, checked above") as u64; + let successes_final = prev_successes.expect("rows > 0, checked above") as u64; + if trials_final != samples { + return Err(format!( + "witnessed final trials {trials_final} does not equal the declared samples {samples}: the denominator is not witnessed" + )); + } + + let n = trials_final as f64; + let p_hat = successes_final as f64 / n; + let z = MC_INTERVAL_Z_95; + + let (interval_low, interval_high) = match interval_method { + MC_INTERVAL_NORMAL_APPROX_95 => { + if successes_final == 0 || successes_final == trials_final { + return Err(format!( + "normal-approx-95 is degenerate at the boundary proportion (successes = {successes_final} of {trials_final}); use wilson-95" + )); + } + let half_width = z * (p_hat * (1.0 - p_hat) / n).sqrt(); + (p_hat - half_width, p_hat + half_width) + } + MC_INTERVAL_WILSON_95 => { + let z2 = z * z; + let denom = 1.0 + z2 / n; + let center = (p_hat + z2 / (2.0 * n)) / denom; + let margin = + (z / denom) * (p_hat * (1.0 - p_hat) / n + z2 / (4.0 * n * n)).sqrt(); + (center - margin, center + margin) + } + other => { + return Err(format!( + "interval_method `{other}` is not in the EXECUTED executable vocabulary (v1: normal-approx-95, wilson-95); clopper-pearson-95 needs a verified inverse incomplete beta and is not executable" + )); + } + }; + + Ok(McExecutedComputed { + estimate: p_hat, + interval_low, + interval_high, + n_effective: trials_final, + successes: successes_final, + }) + } + ``` + +- [ ] Unit tests, `#[cfg(test)] mod tests` in the same file: + - `compute_mc_executed_recovers_a_coherent_wilson_series`: a hand-built 4-row series + (e.g. successes `1,1,2,2`, trials `10,11,12,13`), `samples = 13`, `wilson-95`; assert + `Ok` with `n_effective == 13`, `successes == 2`, and `estimate == 2.0/13.0`. + - `compute_mc_executed_rejects_before_any_rerun_on_bad_trials_step`: trials jumping by 2 + between two rows; assert `Err` whose message names the offending row and field + (**this is the "Stage-A-rejects-before-rerun" property test**: it proves the + coherence check fires on pure data, with no re-run machinery involved at all, since + the function takes no compile/run inputs). + - `compute_mc_executed_rejects_successes_decrease`. + - `compute_mc_executed_rejects_successes_exceeding_trials`. + - `compute_mc_executed_rejects_non_integer_column`. + - `compute_mc_executed_witnessed_denominator_must_equal_samples`: coherent series whose + final trials is 2000 but `samples = 1999`; assert `Err` naming both numbers (**the + witnessed-denominator equality test** named in the task). + - `compute_mc_executed_rejects_ragged_series`: `series.len()` not a multiple of 3. + - `compute_mc_executed_normal_approx_degenerate_at_zero_successes` and + `..._at_all_successes`: both boundary refusals, message points at `wilson-95`. + - `compute_mc_executed_rejects_clopper_pearson`: message names the inverse-incomplete- + beta reason. + - `compute_mc_executed_wilson_matches_hand_computed_value`: one series where + `interval_low`/`interval_high` are checked against a value computed independently + (by hand or a second formula transcription) to `1e-9`, catching a transcription bug + in the Wilson formula itself (the unit test that would fail if the code above has a + sign or parenthesization error). + +## Task 3: `column_count_matches_invariant` and `evaluate_measurement` + +**Decision (design left the exact signature open):** thread a `mc_executed: bool` +parameter through `column_count_matches_invariant`. Without it, the function cannot tell +"3 columns, single-scalar invariant" apart for an EXECUTED mc receipt versus a receipt +that just set `--columns 3` on an ordinary single-scalar invariant, and the two must be +treated differently (the former valid, the latter refused, exactly as `column_count == 2` +already is for every invariant except `cross-backend`). Rationale: this is the minimal +change that keeps the contract PRECISE (an EXECUTED mc receipt requires exactly 3 columns +paired with a single-scalar invariant; `relation`/`cross-backend` explicitly refuse +`mc_executed == true`, since their columns mean something else) rather than loosening +`column_count == 1` to `column_count in {1, 3}` for every single-scalar invariant +regardless of whether an MC block backs it. + +- [ ] `column_count_matches_invariant` (currently lines 904-923), new signature and body: + + ```rust + pub fn column_count_matches_invariant(name: &str, column_count: usize, mc_executed: bool) -> bool { + if name == RELATION_INVARIANT { + !mc_executed && column_count >= 2 + } else if name == CROSS_BACKEND_INVARIANT { + !mc_executed && column_count == 2 + } else if mc_executed { + column_count == 3 + } else { + column_count == 1 + } + } + ``` + + Update the doc comment: "the `relation` invariant reads across a row's columns...; an + EXECUTED monte_carlo receipt requires exactly 3 columns (the invariant scalar plus the + witnessed successes/trials counters) paired with a single-scalar invariant name, never + with `relation`/`cross-backend` (their columns already mean something else); every other + single-scalar invariant requires exactly 1." +- [ ] Update both call sites for the new parameter: + - `main.rs` emit gate (currently line 7658): pass the emit-time `mc_executed` bool + (from the new `--mc-executed` flag, Task 5). + - `scientific_runtime.rs` verify gate (currently line 2167): pass + `receipt.monte_carlo.as_ref().is_some_and(|mc| mc.status == "EXECUTED")`. +- [ ] `evaluate_measurement` (currently lines 1041-1065): add the mirror arm the design + names, between the existing `RELATION_INVARIANT | CROSS_BACKEND_INVARIANT` arm and the + final catch-all: + + ```rust + pub fn evaluate_measurement( + name: &str, + series: &[f64], + tol: f64, + column_count: usize, + ) -> MeasurementVerdict { + match name { + RELATION_INVARIANT | CROSS_BACKEND_INVARIANT => { + // unchanged + let (observed, rows) = relation_columns_agree(series, tol, column_count); + MeasurementVerdict { observed, effective_len: rows } + } + _ if column_count == 3 => { + // An EXECUTED monte_carlo receipt: column 0 is the declared + // single-scalar invariant, columns 1-2 are the witnessed + // successes/trials counters `compute_mc_executed` checks + // separately. De-interleave and evaluate the invariant over + // column 0 only; rows are the effective observation count, + // mirroring the relation arm above. Ragged (not a multiple of + // 3) yields zero rows, same "cannot witness" treatment + // `relation_columns_agree` gives a ragged relation series. + let ragged = series.is_empty() || series.len() % 3 != 0; + let col0: Vec = if ragged { + Vec::new() + } else { + series.iter().step_by(3).copied().collect() + }; + let rows = col0.len(); + MeasurementVerdict { + observed: evaluate_invariant(name, &col0, tol), + effective_len: rows, + } + } + _ => MeasurementVerdict { + observed: evaluate_invariant(name, series, tol), + effective_len: series.len(), + }, + } + } + ``` + + This arm is reached only for names other than `relation`/`cross-backend` (the first arm + already claimed those unconditionally), so a genuine 3-column `relation` request is + unaffected. `column_count_matches_invariant` (above) is the ONLY gate that ties + `column_count == 3` to `mc_executed`; `evaluate_measurement` trusts that gate already + ran, consistent with how it already trusts `column_count_matches_invariant` for the + relation arm. +- [ ] Unit tests: `evaluate_measurement_deinterleaves_column_zero_for_three_columns` + (a 3-column series where columns 1-2 would fail `non_negative` but column 0 passes; + assert the verdict reads column 0 only) and + `evaluate_measurement_three_column_ragged_series_cannot_witness` (mirrors the existing + ragged-relation test). + +## Task 4: verify wiring (`scientific_runtime.rs`, `evaluate_scientific_runtime_receipt`) + +**Stage A** extends the existing MC admission block (currently lines 2323-2349, all +before the re-run at line 2586, so this stays pre-re-run and needs no C compiler): + +- [ ] Replace the block with a two-arm version: + + ```rust + if let Some(mc) = &receipt.monte_carlo { + if !rederived_uses_random || receipt.seed_value.is_none() { + eprintln!( + "Error: the receipt carries a monte_carlo block but the program is not a seeded Random run (an MC estimate needs the Random capability and a sealed seed to re-derive)" + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + if mc.samples == 0 { + eprintln!("Error: monte_carlo.samples is 0: an MC claim without its denominator is unpriceable"); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + if mc.estimator.trim().is_empty() || mc.interval_method.trim().is_empty() { + eprintln!("Error: monte_carlo declares an empty estimator or interval_method: the claim is the interval, never the point, so both must be named"); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + let executed_fields_present = mc.estimate.is_some() + || mc.interval_low.is_some() + || mc.interval_high.is_some() + || mc.n_effective.is_some() + || mc.successes.is_some(); + match mc.status.as_str() { + "DECLARED" => { + if executed_fields_present { + eprintln!("Error: monte_carlo.status is DECLARED but an executed field is present: a DECLARED block never carries estimate/interval_low/interval_high/n_effective/successes"); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + } + "EXECUTED" => { + let (Some(estimate), Some(interval_low), Some(interval_high), Some(n_effective), Some(successes)) = + (mc.estimate, mc.interval_low, mc.interval_high, mc.n_effective, mc.successes) + else { + eprintln!("Error: monte_carlo.status is EXECUTED but not all five executed fields (estimate, interval_low, interval_high, n_effective, successes) are present"); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + }; + if mc.estimator != MC_EXECUTED_ESTIMATOR_PROPORTION { + eprintln!("Error: EXECUTED monte_carlo estimator `{}` is not in the executable vocabulary (v1: proportion)", mc.estimator); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + let computed = compute_mc_executed( + &receipt.measurement.observed_values, + receipt.measurement.column_count, + mc.samples, + &mc.interval_method, + ) + .map_err(|reason| { + eprintln!("Error: EXECUTED monte_carlo Stage A (sealed series, no re-run) recompute failed: {reason}"); + verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1) + })?; + if computed.n_effective != n_effective || n_effective != mc.samples { + eprintln!("Error: sealed n_effective {n_effective} does not match the Stage A witnessed denominator {} (declared samples {})", computed.n_effective, mc.samples); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + if computed.successes != successes { + eprintln!("Error: sealed successes {successes} does not match the Stage A recompute {}", computed.successes); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + if (computed.estimate - estimate).abs() > MC_RECOMPUTE_TOLERANCE + || (computed.interval_low - interval_low).abs() > MC_RECOMPUTE_TOLERANCE + || (computed.interval_high - interval_high).abs() > MC_RECOMPUTE_TOLERANCE + { + eprintln!("Error: sealed EXECUTED interval fields do not match the Stage A recompute over the sealed series (estimate {estimate} vs {}, low {interval_low} vs {}, high {interval_high} vs {})", computed.estimate, computed.interval_low, computed.interval_high); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + } + other => { + eprintln!("Error: monte_carlo.status `{other}` is not expressible (only DECLARED or EXECUTED)"); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + } + } + ``` + +- [ ] `not_claimed` biconditional, placed beside the existing `NOT_PROVES_OPTIMALITY`/ + `optimality` checks (currently lines 2491-2508): + + ```rust + let mc_executed = receipt.monte_carlo.as_ref().is_some_and(|mc| mc.status == "EXECUTED"); + let has_all_mc_not_claimed = MC_EXECUTED_NOT_CLAIMED + .iter() + .all(|c| receipt.not_claimed.iter().any(|x| x == c)); + let has_any_mc_not_claimed = MC_EXECUTED_NOT_CLAIMED + .iter() + .any(|c| receipt.not_claimed.iter().any(|x| x == c)); + if mc_executed != has_all_mc_not_claimed || (has_any_mc_not_claimed && !has_all_mc_not_claimed) { + eprintln!( + "Error: not_claimed `sample_independence`/`interval_coverage`/`estimator_semantics` present={} but monte_carlo EXECUTED={}: the boundary entries must pair exactly (all three or none) with an EXECUTED block", + has_any_mc_not_claimed, mc_executed + ); + return Err(verify_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + ``` + +**Stage B**, placed immediately after the existing `MEASUREMENT_COUNT_DRIFT` check +(currently lines 2732-2739) and before the `recompute_verdict` call, using the same +`verdict_series` the rest of post-re-run verify already uses: + +- [ ] Insert: + + ```rust + if let Some(mc) = &receipt.monte_carlo { + if mc.status == "EXECUTED" { + // Stage A already required all five fields present; unwrap is safe. + let estimate = mc.estimate.expect("Stage A validated presence"); + let interval_low = mc.interval_low.expect("Stage A validated presence"); + let interval_high = mc.interval_high.expect("Stage A validated presence"); + let computed = compute_mc_executed( + &verdict_series, + receipt.measurement.column_count, + mc.samples, + &mc.interval_method, + ) + .map_err(|reason| { + eprintln!("Error: EXECUTED monte_carlo Stage B (re-run series) recompute failed: {reason}"); + verify_failure_class(json, "MC_INTERVAL_DRIFT", 1) + })?; + if computed.n_effective != mc.samples + || computed.successes != mc.successes.expect("Stage A validated presence") + || (computed.estimate - estimate).abs() > MC_RECOMPUTE_TOLERANCE + || (computed.interval_low - interval_low).abs() > MC_RECOMPUTE_TOLERANCE + || (computed.interval_high - interval_high).abs() > MC_RECOMPUTE_TOLERANCE + { + eprintln!("Error: EXECUTED monte_carlo interval drift: sealed fields do not match the Stage B recompute over the re-run series"); + return Err(verify_failure_class(json, "MC_INTERVAL_DRIFT", 1)); + } + } + } + ``` + +- [ ] Add `MC_INTERVAL_DRIFT` to the `verify_failure_class` doc comment (currently around + lines 3175-3177, beside `MEASUREMENT_COUNT_DRIFT`): "`MC_INTERVAL_DRIFT`: an EXECUTED + monte_carlo receipt's sealed interval fields do not match the Stage B recompute over the + re-run series (Stage A already passed over the sealed series; this catches a receipt + that stopped describing the run it names)." +- [ ] Unit tests in `scientific_runtime.rs`'s `#[cfg(test)] mod tests`, extending + `verify_enforces_the_monte_carlo_admission_contracts` or a new sibling test: + - `verify_stage_a_rejects_tampered_executed_interval_before_any_rerun`: build a receipt + with a coherent EXECUTED block, tamper `interval_high` directly on the + `ScientificRuntimeReceipt` (bypassing `seal_receipt` so the seal is stale is wrong; + instead mutate then re-seal via the same path the self-test's `reseal_json` uses), + pass a `rerun_series` closure that `panic!`s if called (the existing idiom at line + 5697), assert `Err(1)` with the panic never firing (the direct proof that Stage A + rejects before Task 8's self-test case exercises it through the CLI). + - `verify_stage_b_reports_mc_interval_drift_on_a_changed_rerun`: a coherent EXECUTED + receipt whose `rerun_series` closure returns a DIFFERENT coherent series (e.g. one + more successful draw), assert `Err(1)` and that the printed `failure_class` is + `MC_INTERVAL_DRIFT` (use the `--json` path, matching the existing test idiom that + reads `failure_class` from the JSON report). + - `verify_refuses_declared_block_carrying_an_executed_field`. + - `verify_refuses_executed_block_missing_an_executed_field`. + - `verify_refuses_executed_estimator_outside_vocabulary`. + - `verify_not_claimed_triad_biconditional`: EXECUTED block with the triad ABSENT is + refused; DECLARED block with the triad PRESENT is refused; EXECUTED with only two of + three present is refused. + +## Task 5: emit wiring (`compiler/src/main.rs`) + +- [ ] New CLI flag, `Commands::Run`, immediately after `mc_interval` (currently line 272) + and before `budget_steps` (currently line 274): + + ```rust + /// Declare the Monte Carlo run EXECUTED: the verifier re-derives the + /// interval from raw sufficient-statistic columns the kernel prints + /// (successes/trials counters beside the invariant scalar) instead of + /// trusting the declaration. Requires all three --mc-* flags together; + /// forces --columns to 3 (an unset default is silently upgraded, any + /// other explicit value is refused, the --cross-backend idiom). + #[arg(long)] + mc_executed: bool, + ``` + +- [ ] Thread `mc_executed` through the `main()` dispatch match arm (currently lines + 662-730): add to the `Commands::Run { .. }` destructure, add to the `--gpu` refusal + condition (currently lines 689-693: `else if mc_estimator.is_some() || mc_samples.is_some() || mc_interval.is_some()`, add `|| mc_executed` since a bare `--gpu --mc-executed` with no other mc flags + bypasses `cmd_run` entirely via `cmd_run_gpu` and would otherwise never hit the + all-or-nothing gate inside `cmd_run`), and pass it as a new positional argument to + `cmd_run(...)` after `mc_interval.as_deref()`. +- [ ] `cmd_run` signature (currently lines 7471-7490): add `mc_executed: bool` after + `mc_interval: Option<&str>`. +- [ ] Extend the MC declaration gate (currently lines 7504-7532) with the mc_executed + pairing and vocabulary checks, still CLI-shape-only (before compiling): + + ```rust + if mc_executed && mc_flag_count < 3 { + eprintln!("Error: --mc-executed requires the full Monte Carlo declaration (--mc-estimator, --mc-samples, --mc-interval)"); + return Err(1); + } + if let Some(estimator) = mc_estimator { + if mc_executed && estimator != MC_EXECUTED_ESTIMATOR_PROPORTION { + eprintln!("Error: --mc-executed requires --mc-estimator proportion (v1 executable vocabulary); DECLARED blocks may still use free text"); + return Err(1); + } + } + ``` + + (The interval-method vocabulary check is NOT duplicated here: it is fail-closed inside + `compute_mc_executed`, called once real data exists, below.) +- [ ] Columns auto-upgrade (currently lines 7643-7651): add the mc_executed branch beside + the existing cross-backend one: + + ```rust + let columns = if invariant_name == CROSS_BACKEND_INVARIANT && columns == 1 { + 2 + } else if mc_executed && columns == 1 { + 3 + } else { + columns + }; + ``` + +- [ ] Column-structure gate call (currently line 7658): pass `mc_executed` as the new + third argument to `column_count_matches_invariant`; add a branch to the error-message + `if`/`else if` chain (currently lines 7659-7671) for `mc_executed`: `"--mc-executed + needs --columns 3 (the invariant scalar plus the witnessed successes/trials counters); + the invariant defines its own column structure"`. +- [ ] `--cross-backend` composition (currently lines 7743-7748, `if mc_flag_count > 0`): + this already transitively refuses `--cross-backend --mc-executed` whenever the three + declaration flags are present (which `--mc-executed` now requires); no code change + needed here, but add a one-line comment noting the transitive coverage so a future + reader does not think it is missing. +- [ ] **Defer EXECUTED finalization until after capture.** The early `monte_carlo` + construction (currently lines 7504-7532) can only build the DECLARED shape (status is + unknown to be EXECUTED-and-coherent until the real series exists). Change: the early + block always builds a `status: "DECLARED".to_string()` block as today (all five new + fields `None`), stored in `monte_carlo`. After the run is captured and `series`/ + `column_count` are finalized (currently lines 7889-7930, the same place + `cross_backend_block` is finalized), if `mc_executed` is true, recompute the final + block: + + ```rust + let monte_carlo = if mc_executed { + let mc = monte_carlo.expect("mc_executed implies mc_flag_count == 3, checked above"); + let computed = compute_mc_executed(&series, column_count, mc.samples, &mc.interval_method) + .map_err(|reason| { + eprintln!("Error: --mc-executed refuses to seal an incoherent EXECUTED block: {reason}"); + 1i32 + })?; + Some(ScientificMonteCarlo { + status: "EXECUTED".to_string(), + estimate: Some(computed.estimate), + interval_low: Some(computed.interval_low), + interval_high: Some(computed.interval_high), + n_effective: Some(computed.n_effective), + successes: Some(computed.successes), + ..mc + }) + } else { + monte_carlo + }; + ``` + + Place this right after the `series`/`column_count`/`cross_backend_block` tuple + (currently ending line 7930) and before `ScientificReceiptInputs` is built (currently + line 7938), so it fires BEFORE sealing (fail closed: an incoherent EXECUTED block never + reaches `build_scientific_runtime_receipt`). +- [ ] `not_claimed` additions at emit, `scientific_runtime.rs`, + `build_scientific_runtime_receipt` (currently lines 1214-1218, after the existing + budget/`optimality` push, before `witnessed_fields_from_capabilities`): + + ```rust + if let Some(mc) = &monte_carlo { + if mc.status == "EXECUTED" { + not_claimed.extend(MC_EXECUTED_NOT_CLAIMED.iter().map(|s| s.to_string())); + } + } + ``` + +## Task 6: kernel, negative fixture, corpus (27 -> 29) + +- [ ] `examples/mc_pi_rejection_executed.bld`: copy `examples/mc_pi_rejection.bld`'s + algorithm exactly (same `n = 2000`, `burn = 200`, `band = 0.3`, same seed-42 stream, + same `4.0 * inside / k` estimate and slack computation, since a re-derivation on the + SAME PRNG stream needs no new calibration), and print three columns per post-burn-in + row instead of one: + + ``` + println!("{} {} {}", band - err, inside, k); + ``` + + Header comment: reuse the existing kernel's calibration prose verbatim (band 0.3 vs + measured worst error 0.2094 under seed 42), add one sentence pointing at the DECLARED + sibling, and add the EXECUTED-specific facts that can only be known by running the + emitted kernel: `successes_final` (= `inside` at k = 2000), `trials_final` (= 2000, by + construction), and the `wilson-95` `interval_low`/`interval_high` for seed 42. **These + three numbers are not invented here** (this plan is read-only, no build/run performed + under it): the implementer runs `buildc run examples/mc_pi_rejection_executed.bld + --emit-receipt - --seed 42 --mc-executed --mc-estimator proportion --mc-samples 2000 + --mc-interval wilson-95 --invariant non-negative --metric slack --problem + mc-pi-rejection-executed`, reads `monte_carlo.successes`/`interval_low`/`interval_high` + from the printed receipt, and transcribes them into the header comment, exactly the + discipline the shipped kernel's own header used for its `0.2094` figure. +- [ ] `examples/mc_pi_rejection_executed_broken.bld`: copy + `examples/mc_pi_rejection_broken.bld` (the wrong-area 3.0-factor estimator) and add the + same two extra columns (`inside`, `k`), UNCHANGED by the wrong-area factor (which only + scales the printed `est`/slack, not the `inside` counter). Header comment: the existing + broken kernel's prose plus one sentence stating the central lesson: the proportion + columns are untouched, so the interval executes and re-derives cleanly (a coherent, + witnessed EXECUTED block) while the slack column still blows the truth band + (`FAIL_EXPECTED`), proving the two claims (interval arithmetic, estimator truth) fail + independently. +- [ ] `ScientificCorpusMember` (`main.rs`, currently lines 1663-1705): add + `#[serde(default)] pub mc_executed: bool` after `mc_interval` (the `negative_fixture` + precedent: no `skip_serializing_if`, since this manifest is hand-authored input, never + re-serialized from the struct, so byte-stability does not apply here the way it does to + a sealed receipt). +- [ ] `cmd_receipt_corpus` (currently around lines 2073-2081, beside the `mc_interval` + passthrough): `if member.mc_executed { emit.arg("--mc-executed"); }`. +- [ ] `examples/scientific-corpus.json`: insert two new members immediately after the + existing `mc_pi_rejection`/`mc_pi_rejection_broken` pair (currently lines 26-27), + keeping the file's pairing-adjacency convention. **Decision (design left the exact + manifest shape open):** do not set an explicit `"columns"` key; rely on the same + auto-upgrade-from-default-1 convention the `cross-backend` singleton member already + relies on (it carries no `"columns"` key either), rather than introducing a new, + inconsistent style for this pair. + + ```json + {"source": "examples/mc_pi_rejection_executed.bld", "invariant": "non-negative", "seed": 42, "mc_estimator": "proportion", "mc_samples": 2000, "mc_interval": "wilson-95", "mc_executed": true, "expected_status": "PASS"}, + {"source": "examples/mc_pi_rejection_executed_broken.bld", "invariant": "non-negative", "negative_fixture": true, "seed": 42, "mc_estimator": "proportion", "mc_samples": 2000, "mc_interval": "wilson-95", "mc_executed": true, "expected_status": "FAIL_EXPECTED"}, + ``` + + Corpus count: 27 -> 29. + +## Task 7: self-test case 10 (9 -> 10) + +**Decision (design left the exact tamper shape open):** do NOT synthesize a fully +self-contained coherent EXECUTED receipt state (rewriting `invariant.name`, +`measurement.observed_values`, `column_count`, `observed`, `receipt_status`, etc. to keep +everything cross-referentially consistent). Reuse cases 7-9's existing "mutate the +existing block if present, else add a syntactically valid one" idiom instead. Rationale, +verified by reading the verify code path (Task 4): EVERY pre-re-run EXECUTED violation +this slice adds reports `FIELD_CONTRACT_VIOLATION`, the SAME class case 7 already relies +on when its zero-denominator MC tamper is checked against a receipt whose underlying +kernel (e.g. `funnel_probe.bld`, the fixture the shipped self-test CLI test already uses) +does not even observe `Random` — case 7 passes today regardless of WHICH specific MC gate +fires first, because `--self-test` only asserts the `failure_class` string, never the +specific message. Case 10 gets the same robustness for free: whichever stage-A gate fires +first (seed pairing, field presence, or the interval-mismatch check this case targets) on +an arbitrary pristine input, the reported class is `FIELD_CONTRACT_VIOLATION` either way. + +- [ ] Add to `build_self_test_cases` (`scientific_runtime.rs`, after case 9, currently + ending line 1574): + + ```rust + // 10. FIELD_CONTRACT_VIOLATION (MC executed interval does not recompute): + // nudge the sealed interval_high on an EXECUTED monte_carlo block (the + // receipt's own block if it already carries one -- e.g. a receipt + // emitted from mc_pi_rejection_executed.bld -- else a syntactically + // valid one is added, mirroring case 9's cross_backend fallback). + // Either way the tamper reaches Stage A's FIELD_CONTRACT_VIOLATION arm: + // see the design note above for why this is robust to whichever + // receipt self-test is run against. + { + let mut v = receipt_json.clone(); + match v.get_mut("monte_carlo") { + Some(mc) if !mc.is_null() && mc.get("status").and_then(|s| s.as_str()) == Some("EXECUTED") => { + let bumped = mc["interval_high"].as_f64().unwrap_or(0.5) + 0.25; + mc["interval_high"] = serde_json::Value::from(bumped); + } + _ => { + v["monte_carlo"] = serde_json::json!({ + "estimator": "proportion", + "samples": 4u64, + "interval_method": "wilson-95", + "status": "EXECUTED", + "estimate": 0.5, + "interval_low": 0.15, + "interval_high": 0.85, + "n_effective": 4u64, + "successes": 2u64, + }); + } + } + let v = reseal_json(&v)?; + cases.push(SelfTestCase { + label: "EXECUTED monte_carlo interval_high nudged against its Stage A recompute".to_string(), + tampered: v, + expected_class: "FIELD_CONTRACT_VIOLATION".to_string(), + resealed: true, + }); + } + ``` + +- [ ] Update `self_test_cases_cover_distinct_failure_classes_and_seal_states` (currently + line ~3439-3444 area) to expect 10 cases. +- [ ] Update `compiler/tests/cli.rs`'s + `receipt_verify_self_test_proves_the_verifier_can_fail` (currently lines 15833-15897): + the `stdout.contains("9/9 tampers rejected...")` assertion (line 15878) becomes + `"10/10 tampers rejected with the expected failure_class"`. + +## Task 8: CLI tests (`compiler/tests/cli.rs`) + +Model on the existing `mc_pi_rejection` round-trip block (currently lines 14940-15080+, +the `mc_flags` helper it builds from). + +- [ ] Round-trip test `mc_pi_rejection_executed_round_trip_and_negative_fixture`: emit and + verify the PASS receipt from `mc_pi_rejection_executed.bld` under + `--mc-executed --mc-estimator proportion --mc-samples 2000 --mc-interval wilson-95`, + assert `receipt_status == "PASS"`, `monte_carlo.status == "EXECUTED"`, + `monte_carlo.n_effective == 2000`, `monte_carlo.successes` present and + `<= 2000`, `monte_carlo.interval_low < monte_carlo.estimate < monte_carlo.interval_high`; + emit and verify the FAIL_EXPECTED receipt from `mc_pi_rejection_executed_broken.bld` + with `--negative-fixture`, assert `receipt_status == "FAIL_EXPECTED"` AND + `monte_carlo.status == "EXECUTED"` with a re-deriving interval (the central lesson: the + interval claim and the truth-band claim fail independently). +- [ ] Six emit-refusal tests, each asserting non-zero exit and a specific stderr + substring: + 1. `mc_executed_without_full_declaration_is_refused`: `--mc-executed` alone (no + `--mc-estimator`/`--mc-samples`/`--mc-interval`); expect "requires the full Monte + Carlo declaration". + 2. `mc_executed_clopper_pearson_is_refused`: `--mc-interval clopper-pearson-95`; expect + "not in the EXECUTED executable vocabulary" / "inverse incomplete beta". + 3. `mc_executed_declared_samples_mismatching_witnessed_trials_is_refused`: use a + modified copy of the executed kernel (or a `--` trailing arg that changes its loop + bound, if the kernel supports one; otherwise add a tiny new fixture kernel that + prints exactly 999 rows) declared with `--mc-samples 2000`; expect "does not equal the + declared samples". + 4. `mc_executed_incoherent_successes_jump_is_refused`: a tiny purpose-built fixture + kernel that prints a successes column jumping by 2 in one step; expect "does not + follow" / "by 0 or 1". + 5. `mc_executed_explicit_columns_other_than_three_is_refused`: `--mc-executed --columns + 2`; expect "needs --columns 3". + 6. `mc_executed_normal_approx_degenerate_boundary_is_refused`: a tiny purpose-built + fixture kernel whose counter never fails a single draw (successes == trials always, + e.g. printing `x*x+y*y < 2.0` which is always true in the unit square) with + `--mc-interval normal-approx-95`; expect "degenerate" / "wilson-95". + Fixture kernels for cases 3, 4, 6 are new, minimal `.bld` files under + `examples/` or `compiler/tests/programs/` (implementer's choice of directory, + matching whichever the existing tiny CLI-test-only fixtures already use in this file); + they are NOT corpus members (the design explicitly scopes these as "cli.rs, not + corpus"). +- [ ] `--gpu`/`--mc-executed` and `--cross-backend`/`--mc-executed` composition refusal + tests (mirroring the existing `--gpu`/`--mc-*` and `--cross-backend`/`--mc-*` tests + already in this file; grep for them and add the `--mc-executed` sibling case beside + each). + +## Task 9: mutation checks (every new gate; break, observe red, restore, observe green) + +- [ ] `compute_mc_executed`: remove the `trials_k != prev + 1.0` check -> + `compute_mc_executed_rejects_before_any_rerun_on_bad_trials_step` red; restore, green. +- [ ] `compute_mc_executed`: remove the successes-delta-in-{0,1} check -> + `compute_mc_executed_rejects_successes_decrease` red; restore, green. +- [ ] `compute_mc_executed`: remove the `successes_k > trials_k` check -> + `compute_mc_executed_rejects_successes_exceeding_trials` red; restore, green. +- [ ] `compute_mc_executed`: remove the `trials_final != samples` check -> + `compute_mc_executed_witnessed_denominator_must_equal_samples` red; restore, green. +- [ ] `compute_mc_executed`: remove the normal-approx boundary guard -> + `compute_mc_executed_normal_approx_degenerate_at_zero_successes` red; restore, green. +- [ ] `compute_mc_executed`: flip a sign in the Wilson `margin` computation -> + `compute_mc_executed_wilson_matches_hand_computed_value` red; restore, green (this is + the mutation that would NOT be caught by any coherence test, only the hand-computed + value test, so it is worth calling out explicitly in the commit body). +- [ ] `column_count_matches_invariant`: remove the `!mc_executed &&` guard on the + `RELATION_INVARIANT` arm -> a new test asserting `column_count_matches_invariant(RELATION_INVARIANT, 3, true) == false` goes red; restore, green. +- [ ] `evaluate_measurement`: remove the ragged-series guard in the new arm -> + `evaluate_measurement_three_column_ragged_series_cannot_witness` red; restore, green. +- [ ] Verify Stage A: remove the `executed_fields_present` DECLARED-biconditional check -> + `verify_refuses_declared_block_carrying_an_executed_field` red; restore, green. +- [ ] Verify Stage A: remove the all-five-fields-present destructure guard (replace with + an unconditional unwrap-or-default) -> `verify_refuses_executed_block_missing_an_executed_field` red; restore, green. +- [ ] Verify Stage A: remove the estimator vocabulary check -> + `verify_refuses_executed_estimator_outside_vocabulary` red; restore, green. +- [ ] Verify Stage A: loosen the `MC_RECOMPUTE_TOLERANCE` comparison to always pass -> + `verify_stage_a_rejects_tampered_executed_interval_before_any_rerun` red; restore, + green. +- [ ] Verify Stage B: skip the Stage B block entirely when `mc.status == "EXECUTED"` -> + `verify_stage_b_reports_mc_interval_drift_on_a_changed_rerun` red; restore, green (this + is the mutation that proves Stage B is load-bearing and not redundant with Stage A: a + receipt whose sealed series was never tampered, only its RE-RUN diverges, passes Stage A + cleanly and must be caught here). +- [ ] Verify: remove the `not_claimed` triad biconditional -> `verify_not_claimed_triad_biconditional` red; restore, green. +- [ ] Emit: remove the fail-closed `compute_mc_executed` call before sealing (seal + unconditionally) -> the CLI refusal tests (Task 8, cases 3, 4, 6) go red (an incoherent + block gets sealed instead of refused); restore, green. +- [ ] Self-test case 10: temporarily delete the case from `build_self_test_cases` -> + `self_test_cases_cover_distinct_failure_classes_and_seal_states` (expects 10) red; + restore, green. + +## Task 10: docs deltas (same commit) + +- [ ] `docs/SCIENTIFIC-RECEIPT.md`, section 1 (flags, currently lines 98-103 for the + existing `--mc-*` bullets): add a `--mc-executed` bullet describing the boolean flag, + the all-or-nothing requirement, the columns auto-upgrade, and the fail-closed emit + refusal. +- [ ] Section 2 (schema, currently lines 218-226, the `monte_carlo` block description): + rewrite to describe the two-arm `status`, the five new `Option` fields present iff + EXECUTED, the estimator/interval-method executable vocabulary (`proportion`; + `normal-approx-95`, `wilson-95`; `clopper-pearson-95` sealed-successes-only, not + executable), the witnessed-denominator equality, and the DECLARED-vs-EXECUTED + biconditional on the five fields (mirroring the existing `wall_exceeded`-without- + `wall_seconds_limit` idiom prose already in this section for `budget`). +- [ ] Section 3 (invariant family, currently the `column_count` discussion around line + 316+): add one paragraph on the EXECUTED 3-column shape and the `evaluate_measurement` + de-interleave-to-column-0 behavior. +- [ ] Failure classes table (currently lines 587-614): add `MC_INTERVAL_DRIFT` as its own + row, exit 1, "an EXECUTED monte_carlo receipt's sealed interval fields do not match the + Stage B recompute over the re-run series." Extend the `FIELD_CONTRACT_VIOLATION` row's + parenthetical (currently one long sentence) with the new EXECUTED sub-cases (missing + executed fields, executed fields on a DECLARED block, estimator/interval_method outside + the executable vocabulary, incoherent aggregate columns, a witnessed denominator that + disagrees with the declared `samples`, the Stage A interval mismatch, the `not_claimed` + triad biconditional). +- [ ] Self-test section (currently lines 622-653): "nine cases" -> "ten cases"; add case + 10's description in the enumerated list; update the "There is no tenth case" closing + paragraph (currently lines 650-653, about wall-metering) since there NOW IS a tenth + case for a different reason. Rewrite that paragraph to describe case 10 instead (it no + longer needs to argue why a tenth case is unnecessary). +- [ ] Corpus section (currently lines 679-711): "thirteen pairs plus the cross-backend + singleton" -> "fourteen pairs plus the cross-backend singleton"; document the new + `mc_executed` manifest field and its `--mc-executed` passthrough beside the existing + `mc_estimator`/`mc_samples`/`mc_interval` prose (currently lines 684-686). +- [ ] `CHANGELOG.md` `## Unreleased` (currently starting line 11): one new bullet at the + TOP of the list (the file's newest-first convention, confirmed by the split-frontier + entry currently occupying that position), same register as the existing entries + (feature name in bold, honest scope, concrete numbers once Task 11 produces them: corpus + 29/29, self-test 10/10, full-suite pass count). Content: the two-stage recompute, the + witnessed denominator, the `not_claimed` additions, and the explicit statement that + EXECUTED hardens interval arithmetic and the denominator, never the estimator's + semantics or independence. + +## Task 11: final verification gate + +- [ ] `cargo fmt --check --manifest-path compiler/Cargo.toml`: clean. +- [ ] `buildc corpus verify examples/scientific-corpus.json`: `29/29`. Capture the exit + code directly (no pipe) before printing/inspecting output. +- [ ] `buildc receipt verify .json + --self-test`: `10/10`. Capture the exit code directly before inspecting output. +- [ ] Full `cargo test --manifest-path compiler/Cargo.toml`: 0 failed. Record the exact + passed/ignored counts (do not assume the pre-slice baseline is unchanged; report the + new numbers). +- [ ] Re-run `buildc corpus verify` a second time to confirm determinism (two consecutive + clean runs), matching the discipline the split-frontier increment applied to its own + gates. +- [ ] Only after all of the above are green: fill in CHANGELOG's numbers (Task 10) and + commit. One commit, on `feat/mc-executed-intervals`, not pushed, per Global Constraints. diff --git a/docs/superpowers/specs/2026-07-29-mc-executed-intervals-design.md b/docs/superpowers/specs/2026-07-29-mc-executed-intervals-design.md new file mode 100644 index 00000000..5442c633 --- /dev/null +++ b/docs/superpowers/specs/2026-07-29-mc-executed-intervals-design.md @@ -0,0 +1,347 @@ +# w1: Monte Carlo EXECUTED interval discipline (design) + +> Design document, not a plan. Internal register. Grounded 2026-07-29 against +> branch `feat/drop-flags` (HEAD b57abb1), the slice 2 commit 9430439, the +> slice 2 plan (`docs/superpowers/plans/2026-07-28-mc-estimator-receipts.md`), +> `compiler/src/scientific_runtime.rs`, `docs/SCIENTIFIC-RECEIPT.md` sections +> 1-3 and 6, and the five-modes brief +> (`git show docs/epistemic-os-vision:docs/superpowers/specs/2026-07-28-five-modes-one-environment.md`). +> All file:line references below verified today (high confidence). + +## 0. The answer up front + +EXECUTED intervals are achievable without the verifier trusting an +unverifiable kernel claim, but only for the ARITHMETIC layer of the claim. +The verifier can honestly compute the interval itself if the kernel prints +the estimator's raw sufficient statistic as extra columns of the captured +series: cumulative `successes` and `trials` counters beside the existing +invariant scalar. Those are pre-arithmetic facts the verifier can check for +structural coherence and re-derive exactly under the sealed seed, and the +interval over them is a fixed computation the verifier owns end to end. + +What can NEVER be executed is the SEMANTIC layer: that the indicator counts +what the author says it counts, that the draws behave as independent samples, +and that the named confidence level covers the true value. Those stay +declared, and the design seals them as does-not-prove facts (new `not_claimed` +entries) rather than pretending the upgrade removed them. This is the +honest-refusal clause resolved as a partial refusal: EXECUTED hardens the +interval arithmetic and the denominator; it does not, and cannot, harden the +indicator's meaning. The design says so in the receipt itself. + +## 1. What ships today (the gap, precisely) + +- The `monte_carlo` block seals `{estimator, samples, interval_method, + status: "DECLARED"}` (scientific_runtime.rs:281-293). Verify re-checks only + SHAPE: seeded Random pairing, non-zero samples, non-empty names, status + exactly `DECLARED` (scientific_runtime.rs:2318-2349). Nothing checks that + `samples: 2000` has anything to do with what the program did, and nothing + computes any interval anywhere. v0 claims reproducibility and declaration + discipline, never interval correctness, and its docs say so. +- The shipped kernel `examples/mc_pi_rejection.bld` prints ONE column: the + slack `band - |estimate_k - pi|` post burn-in, checked by `non_negative`. + The estimate series is destroyed at the print site: from slack alone the + verifier can recover `|estimate - pi|` but not the estimate, the successes + count, or the denominator. The obstacle in the tasking is real. +- The machinery that already solves the shape of this problem: + - Multi-column capture: the series is row-major with a sealed + `column_count`; the relation invariant de-interleaves and computes its + check verifier-side from raw columns, on the stated argument that a + kernel printing raw columns cannot conceal a disagreement by computing + the check itself (scientific_runtime.rs:113-119, 982-1027). + - The EXECUTED precedent: `cross_backend.status == "EXECUTED"` means the + block witnesses a run that actually happened and verify re-executes it + rather than trusting the declaration (scientific_runtime.rs:337-361, + docs/SCIENTIFIC-RECEIPT.md section 2). Status vocabulary per block, with + verify pinning the one honest value, is the established idiom. + - The column-count contract is symmetric across emit and verify + (scientific_runtime.rs:904-923), and `evaluate_measurement` is the single + dispatch both go through (1041-1059). +- The five-modes brief names the flywheel statistics module as the reference + design: declared MDE, "no effect" vs "no power" made distinguishable. The + language-level translation: a receipt that seals a witnessed denominator + and a computed width lets a consumer price a wide interval as absence of + power rather than absence of signal. That distinguishability, not interval + truth, is what this upgrade buys. + +## 2. Decision 1: the data path + +Chosen: **(d), a refinement of (a): cumulative sufficient-statistic columns.** +The kernel prints, per post-burn-in step, one row of exactly three columns: + +``` + +``` + +Column 0 feeds the declared invariant unchanged (the slack under +`non_negative` for the pi kernel). Columns 1 and 2 are the estimator's +running sufficient statistic as raw cumulative counters, integer-valued. +The verifier, on an EXECUTED receipt: + +1. De-interleaves by the sealed `column_count == 3`. +2. Checks structural coherence of the aggregate columns: every value + integer-valued (`fract() == 0`) and below 2^53; `trials` increments by + exactly 1 across consecutive rows (the first row's absolute value is + free: it is the burn-in edge); `successes` non-decreasing with increments + in {0, 1}; `successes <= trials` on every row. +3. Takes the final row as the full-sample statistic and requires + `trials_final == monte_carlo.samples`. The declared denominator becomes a + WITNESSED one: this is the single biggest honesty gain of the slice, and + it costs one equality check. +4. Computes `p_hat = successes_final / trials_final` and the interval by the + named method, entirely in verifier-owned code, and compares against the + sealed executed fields (tolerances in Decision 3). + +The recompute runs TWICE, in two stages: + +- **Stage A, no re-run:** over the SEALED `measurement.observed_values`. The + sealed executed fields must be the named method applied to the sealed + series. This makes a tampered-and-resealed interval a pure data + contradiction, rejectable before any program re-run, which keeps the + self-test's no-compiler property intact (docs/SCIENTIFIC-RECEIPT.md, + self-test section: every case rejected before any re-run). +- **Stage B, after the re-run:** the same computation over the re-parsed + re-run series. Verify never compares raw floats series-to-series today + (only count and verdict), so without stage B a receipt could stay + internally coherent while no longer describing the run it names. + +### The candidates killed, with reasons + +**(a) as stated (a running-estimate column beside the slack):** the running +estimate `4 * inside / k` is a DERIVED float. The verifier either trusts the +kernel's arithmetic (the exact trust EXECUTED is supposed to remove) or +reverse-engineers the transform (kernel semantics buildc cannot parse). Raw +counters are the pre-arithmetic facts; the relation invariant's argument, +moved one level down: print what you aggregated, not what you computed from +it. The refinement keeps (a)'s capture mechanism and replaces its payload. + +**(b) a second `--mc-metric` series convention:** the receipt's honesty rests +on ONE stdout stream, ONE measurement block, ONE raw-stdout digest, ONE +sealed extraction policy. A second series needs a stream-splitting protocol +(prefix tags or a second channel), a second digest, and a second count rule: +a parallel copy of machinery that column de-interleaving already provides, +plus a new seam for the two streams to disagree across. Interleaved columns +also keep the aggregates row-aligned with the invariant series for free. +Killed as duplication with new failure modes and no added honesty. + +**(c) verifier re-runs a REFERENCE estimator from the sealed seed:** buildc +cannot parse kernel semantics, so a reference estimator is a SECOND program +whose equivalence to the kernel is precisely the unverifiable claim. The PRNG +consumption pattern (draw order, draws per iteration, burn-in) is +kernel-specific, so a mismatch is a false alarm and a match is unearned +confidence, and the mechanism blesses exactly one kernel shape forever. This +is the declared trust re-introduced at one remove, wearing an EXECUTED +badge, which is worse than DECLARED because it lies about its category. +Killed on principle, not on cost. + +### Machinery deltas the chosen path requires + +- `column_count_matches_invariant` (scientific_runtime.rs:911-923) gains an + arm: an EXECUTED mc receipt requires `column_count == 3` paired with a + single-scalar invariant. `relation` and `cross-backend` are refused with an + EXECUTED mc block (`cross_backend` is already transitively excluded, since + it refuses Random and mc requires it, scientific_runtime.rs:2442-2448). +- `evaluate_measurement` (scientific_runtime.rs:1041-1059) gains the mirror + of the relation arm: for an EXECUTED mc receipt a single-scalar invariant + evaluates over de-interleaved column 0, and `effective_len` is the ROW + count. `measurement.count` stays the total token count, exactly as + `relation` handles it, so token drift stays independently caught. +- New emit flag `--mc-executed` (boolean): requires all three `--mc-*` + declaration flags; forces `--columns` to 3 in the cross-backend idiom + (unset default silently upgraded, any other value refused); refused with + `--gpu` and `--cross-backend` (both already refuse the mc flags). + +## 3. Decision 2: what EXECUTED claims, and refuses to claim + +An EXECUTED `monte_carlo` block claims, and verify re-derives, exactly: + +1. The sealed interval is the named method applied to the captured aggregate + columns (stage A), and the same computation over a fresh re-run under the + sealed seed re-derives it (stage B). +2. The denominator is witnessed: `samples == n_effective == trials_final`, + re-derived from the seeded stream. +3. The aggregate stream is structurally coherent as a cumulative Bernoulli + count (the checks in Decision 1). + +It refuses to claim, sealed machine-readably as `not_claimed` additions +(present IFF the block is EXECUTED, the `NOT_PROVES_OPTIMALITY` pairing +idiom) plus does-not-prove prose in the docs: + +- `sample_independence`: the PRNG is a deterministic recurrence; independence + is a modeling assumption about it, not a checkable fact. +- `interval_coverage`: the 95% is a property of the method under assumptions + the receipt cannot check. EXECUTED does not claim the true value lies in + the interval, for ANY value of "true". +- `estimator_semantics`: the verifier witnesses that a coherent counter was + aggregated and the arithmetic over it; it cannot witness that the indicator + measures quarter-circle membership rather than anything else, nor that any + author-side transform (pi = 4p) is the right one. The truth-band slack in + column 0 keeps carrying that check for known-answer kernels, as a separate, + honestly-labeled claim. + +Estimator unbiasedness needs no new entry: it is subsumed by +`estimator_semantics` and the existing physical-law boundary. The oracle +block does NOT change: the interval is an admission-block fact whose +"verdict" is re-derivation, not pass/fail; promoting it to an oracle kind +(`executed_interval`) was considered and killed because it would conflate the +receipt's verdict criterion (the invariant) with a computation that has no +pass/fail semantics of its own. + +## 4. Decision 3: v1 method set and numeric discipline + +Executed vocabulary, pinned (an EXECUTED block must name one of these; the +verifier owns the arithmetic): + +- `normal-approx-95`: `p_hat +/- z * sqrt(p_hat * (1 - p_hat) / n)`, with z + pinned as a named const `1.959963984540054` (the double nearest the 0.975 + normal quantile) beside the family tolerances. Degenerate guard: refused at + emit when `successes == 0` or `successes == trials` (a zero-width interval + at the boundary overclaims; the error message points at `wilson-95`). +- `wilson-95`: the Wilson score interval, same pinned z. Well-defined at the + boundary proportions, asymmetric by construction. +- `clopper-pearson-95`: NOT executable in v1. Exact binomial bounds need an + inverse incomplete beta, which is its own numerics-correctness burden with + no in-tree oracle. A method the verifier cannot execute cannot ride on an + EXECUTED block: refused at emit and at verify. The raw `successes` count IS + sealed, so v2 can add it with no schema or kernel change. DECLARED blocks + keep free-text method names forever (their claim never included execution). + +Executed estimator vocabulary v1: `proportion` only (the mean of Bernoulli +indicators). DECLARED blocks keep free text (the shipped corpus uses `mean`, +untouched). + +Sealed executed fields, present IFF `status == "EXECUTED"`: + +``` +estimate f64 p_hat = successes_final / trials_final +interval_low f64 lower bound by the named method +interval_high f64 upper bound by the named method +n_effective u64 trials_final (must equal samples) +successes u64 successes_final +``` + +Named deviation from the tasking sketch (`{estimate, half_width, +n_effective}`): Wilson's interval is not centered on `p_hat`, so a lone +half_width either loses the center or forces a dishonestly symmetric +reading. Low/high bounds are method-agnostic; half_width is derivable for +the symmetric method by anyone who wants it. + +Numeric discipline: + +- Integers exact: `n_effective`, `successes`, and the integrality checks on + the columns are exact comparisons. The aggregates re-derive exactly under + the sealed seed: the PRNG is integer arithmetic over u64 state, and for the + reference kernel the indicator path (`x*x + y*y < 1.0`) uses only IEEE + correctly-rounded ops with no libm calls, so the counter stream is + bit-stable across platforms (moderate confidence for the general claim; + high for this kernel class). Kernel-author discipline, documented not + enforced: aggregate columns must be libm-free integer counters, or stage B + will fail loudly on the platform where the stream differs, which is the + correct outcome. +- Floats within a pinned absolute `1e-12` (`MC_RECOMPUTE_TOLERANCE`), applied + to `estimate`, `interval_low`, `interval_high` in both stages. The interval + arithmetic runs on identical integer inputs through one fixed Rust + implementation at emit and verify, so agreement should be exact in + practice; the tolerance is headroom against a future compiler reassociating + verifier-side float ops, in the family's verdict-robustness style, not a + load-bearing looseness. Values are O(1) proportions, so absolute is safe. + +## 5. Decision 4: backward compatibility and the verify contracts + +- **DECLARED receipts stay valid forever.** The status gate at + scientific_runtime.rs:2342-2348 becomes a two-arm vocabulary + (`DECLARED | EXECUTED`); every contract added by this slice fires only on + `EXECUTED`. The five executed fields are `Option` + + `#[serde(default, skip_serializing_if = "Option::is_none")]`, so every + receipt sealed before this slice parses and re-serializes to its exact + bytes and seal. `ScientificMonteCarlo` loses `Eq` (f64 fields), the + `ScientificBudget` precedent (scientific_runtime.rs:306-309). +- Schema stays `v0`: additive optional fields within v0 is the shipped + precedent (wall metering added `wall_seconds_limit`/`wall_exceeded` the + same way). +- **EXECUTED is opt-in** via `--mc-executed`; the DECLARED emission path is + byte-for-byte untouched, existing corpus members re-emit unchanged. +- Verify contracts, by status: + - DECLARED: exactly today's four checks (seeded-Random pairing, non-zero + samples, non-empty names, status vocabulary), PLUS: any executed field + present on a DECLARED block is refused (the biconditional, the + `wall_exceeded`-without-`wall_seconds_limit` idiom). + - EXECUTED: the DECLARED shape checks, then: all five executed fields + present; estimator in the executable vocabulary; interval_method in the + executable vocabulary; `column_count == 3` with a single-scalar + invariant; aggregate coherence over the sealed series; stage A recompute; + `n_effective == samples`; then after the re-run, stage B recompute and + coherence over the re-derived series. +- Failure classes, additive within v0 (the table has grown slice by slice): + every pre-re-run EXECUTED violation is `FIELD_CONTRACT_VIOLATION` (a sealed + field claims something the sealed data contradicts, the existing meaning); + stage B disagreement is one new class, `MC_INTERVAL_DRIFT`, exit 1, sitting + in the drift family beside `MEASUREMENT_COUNT_DRIFT`. Old receipts can + never produce the new class. + +## 6. Decision 5: kernel migration, corpus, fixtures + +- **`examples/mc_pi_rejection.bld` stays exactly as it is**, as the DECLARED + exemplar. It is the backward-compat witness: rewriting it would orphan the + DECLARED path's corpus coverage and falsify the claim that DECLARED + receipts remain first-class. Its header gains one sentence pointing at the + executed sibling. +- **New `examples/mc_pi_rejection_executed.bld`:** the same rejection kernel + printing three-column rows `slack inside k` post burn-in, emitted with + `--seed 42 --mc-executed --mc-estimator proportion --mc-samples 2000 + --mc-interval wilson-95 --invariant non-negative`. Header comment records + the executed numbers for seed 42 (measured at implementation time, not + invented here) the way the DECLARED kernel records its 0.2094 calibration. +- **New negative fixture `examples/mc_pi_rejection_executed_broken.bld`:** + the wrong-area estimator (factor 3.0) with the SAME counter columns. The + proportion columns are untouched, so the interval executes and re-derives + cleanly while the slack column blows the truth band: `FAIL_EXPECTED`. This + seals the slice's central lesson into the corpus: an executed interval is + not a truth claim, and the two claims fail independently. +- Corpus 24 -> 26, both new members with full mc + executed passthrough + fields (`mc_executed: true` added to the corpus schema). +- **Emit-refusal tests (cli.rs, not corpus):** `--mc-executed` without the + three declaration flags; with `clopper-pearson-95` (the unexecutable + method, one of the two tasked negatives); declared samples that do not + equal the witnessed final trials (kernel draws 1000, declares 2000); + incoherent aggregates (a successes column that jumps by 2); an explicit + `--columns` other than 3; degenerate `normal-approx-95` at a boundary + proportion. Emit computes the same checks as verify stage A, fail closed: + an incoherent EXECUTED block never gets sealed in the first place. +- **Self-test case 10** (the other tasked negative, the sealed interval that + does not recompute): nudge sealed `interval_high`, reseal, expect + `FIELD_CONTRACT_VIOLATION` via stage A. Pre-re-run by construction, so the + self-test keeps needing no C compiler. A resealed unexecutable method name + is rejected through the same stage and is covered by a verify unit test + rather than an eleventh case (one case per gate FAMILY, the shipped + self-test philosophy). + +## 7. The riskiest decision, named + +The fixed positional column convention plus the coherence checks as the +entire provenance story. A deliberately adversarial kernel can print a +synthetic counter stream that satisfies every coherence check while being +unrelated to its actual draws: EXECUTED hardens the arithmetic and the +denominator, not the indicator's provenance. The design's defense is not +mechanical but declarative, and that is the bet: the `estimator_semantics` / +`sample_independence` / `interval_coverage` entries in `not_claimed`, and the +does-not-prove prose, must carry the boundary. If a consumer reads EXECUTED +as "the interval is true," no achievable mechanism would have saved them; the +receipt at least states, in sealed machine-readable form, exactly which +reading is licensed. Second risk, smaller: the cross-platform exactness bet +on integer counters, mitigated by the integrality checks and the loud stage B +failure on the platform where it breaks. + +## 8. Deferred, tracked + +- `clopper-pearson-95` execution (needs a verified inverse incomplete beta; + the sealed `successes` already carries the input it will need). +- A declared affine transform field (`scale`, e.g. 4.0 for pi) so the + executed fields could be stated in the headline quantity's units. Killed + for v1 to keep the sealed-knob count minimal: the truth band already + witnesses the pi-level claim, and a declared scale on an executed number + blurs the status boundary this slice exists to sharpen. +- Non-Bernoulli estimators (a mean over a continuous column needs sealed + moments and loses the integer-exactness argument; a different design, not + a vocabulary entry). +- Multiple mc estimates per receipt (one block per receipt is the v0 shape; + chains already compose receipts). diff --git a/examples/mc_pi_rejection_executed.bld b/examples/mc_pi_rejection_executed.bld new file mode 100644 index 00000000..3c18145e --- /dev/null +++ b/examples/mc_pi_rejection_executed.bld @@ -0,0 +1,58 @@ +// Monte Carlo kernel: pi by rejection sampling, EXECUTED interval sibling of +// mc_pi_rejection.bld. Same algorithm, same seed-42 stream (n = 2000, burn = +// 200, band = 0.3, the same `4.0 * inside / k` estimate and slack +// computation), so a re-derivation on the SAME PRNG stream needs no new +// calibration: the measured worst error after burn-in under seed 42 is +// 0.2094, so the band clears it by ~1.4x (see mc_pi_rejection.bld for the +// full calibration story). +// +// The difference: each post-burn-in row prints THREE columns instead of one, +// `slack inside k`, so the verifier can re-derive the Monte Carlo interval +// itself from the raw sufficient-statistic columns (cumulative successes and +// trials) instead of trusting a declared one. Column 0 (slack) feeds the +// `non-negative` invariant unchanged; columns 1-2 (`inside`, `k`) are the +// witnessed successes/trials counters `compute_mc_executed` checks for +// structural coherence and re-derives the wilson-95 interval from, at two +// stages (Stage A over the sealed series before any re-run, Stage B over the +// re-run series). +// +// Emitted with `--seed 42 --mc-executed --mc-estimator proportion +// --mc-samples 2000 --mc-interval wilson-95 --invariant non-negative` +// (`--columns` auto-upgrades to 3). Measured at implementation time by +// running the emitted receipt (not invented here, the same discipline the +// DECLARED kernel's header used for its 0.2094 figure): under seed 42, +// successes_final = 1551 of trials_final = 2000, estimate = 0.7755, +// wilson-95 interval_low = 0.7566951910008709, interval_high = +// 0.7932485159471586. +// +// EXECUTED hardens the interval arithmetic and the witnessed denominator; it +// does not, and cannot, harden sample independence, interval coverage, or +// the estimator's semantics (sealed as `not_claimed` entries). Companion +// negative fixture: mc_pi_rejection_executed_broken.bld. + +fn main() ~ Console + Random { + let n: i32 = 2000; + let burn: i32 = 200; + let band: f64 = 0.3; + let mut inside: i32 = 0; + let mut k: i32 = 0; + while k < n { + let x: f64 = random_f64(); + let y: f64 = random_f64(); + if x * x + y * y < 1.0 { + inside = inside + 1; + } + k = k + 1; + if k >= burn { + let est: f64 = 4.0 * (inside as f64) / (k as f64); + let mut err: f64 = est - 3.14159265358979323846; + if err < 0.0 { + err = 0.0 - err; + } + // Slack against the calibrated truth band (column 0), plus the + // witnessed successes/trials counters (columns 1-2) the + // verifier re-derives the executed interval from. + println!("{} {} {}", band - err, inside, k); + } + } +} diff --git a/examples/mc_pi_rejection_executed_broken.bld b/examples/mc_pi_rejection_executed_broken.bld new file mode 100644 index 00000000..f88baa95 --- /dev/null +++ b/examples/mc_pi_rejection_executed_broken.bld @@ -0,0 +1,43 @@ +// Negative fixture for mc_pi_rejection_executed.bld: the same sampler under +// the same WRONG-AREA estimator as mc_pi_rejection_broken.bld (factor 3.0 +// instead of 4.0), with the same three-column EXECUTED capture +// (`slack inside k`). +// +// The central lesson this fixture seals into the corpus: the wrong-area +// factor only scales the printed estimate/slack (column 0), never the raw +// `inside`/`k` counters (columns 1-2). So the EXECUTED interval still +// executes and re-derives CLEANLY (a coherent, witnessed denominator and a +// correctly re-derived wilson-95 interval), while the slack column still +// blows through the truth band and the `non-negative` invariant FAILs as +// declared (FAIL_EXPECTED). The interval claim and the estimator-truth claim +// fail INDEPENDENTLY: an executed interval is not a truth claim about the +// quantity it estimates, only about the arithmetic and the denominator. +// +// The sealed seed makes the failure exactly re-derivable. + +fn main() ~ Console + Random { + let n: i32 = 2000; + let burn: i32 = 200; + let band: f64 = 0.3; + let mut inside: i32 = 0; + let mut k: i32 = 0; + while k < n { + let x: f64 = random_f64(); + let y: f64 = random_f64(); + if x * x + y * y < 1.0 { + inside = inside + 1; + } + k = k + 1; + if k >= burn { + // Wrong area factor: 3.0 instead of 4.0. Untouched: the raw + // inside/k counters below, so the executed interval still + // re-derives cleanly even as the slack claim fails. + let est: f64 = 3.0 * (inside as f64) / (k as f64); + let mut err: f64 = est - 3.14159265358979323846; + if err < 0.0 { + err = 0.0 - err; + } + println!("{} {} {}", band - err, inside, k); + } + } +} diff --git a/examples/scientific-corpus.json b/examples/scientific-corpus.json index 9e7052de..a5fb7c2c 100644 --- a/examples/scientific-corpus.json +++ b/examples/scientific-corpus.json @@ -25,6 +25,8 @@ {"source": "examples/random_walk_bound_broken.bld", "invariant": "non-negative", "negative_fixture": true, "seed": 42, "expected_status": "FAIL_EXPECTED"}, {"source": "examples/mc_pi_rejection.bld", "invariant": "non-negative", "seed": 42, "mc_estimator": "mean", "mc_samples": 2000, "mc_interval": "normal-approx-95", "expected_status": "PASS"}, {"source": "examples/mc_pi_rejection_broken.bld", "invariant": "non-negative", "negative_fixture": true, "seed": 42, "mc_estimator": "mean", "mc_samples": 2000, "mc_interval": "normal-approx-95", "expected_status": "FAIL_EXPECTED"}, + {"source": "examples/mc_pi_rejection_executed.bld", "invariant": "non-negative", "seed": 42, "mc_estimator": "proportion", "mc_samples": 2000, "mc_interval": "wilson-95", "mc_executed": true, "expected_status": "PASS"}, + {"source": "examples/mc_pi_rejection_executed_broken.bld", "invariant": "non-negative", "negative_fixture": true, "seed": 42, "mc_estimator": "proportion", "mc_samples": 2000, "mc_interval": "wilson-95", "mc_executed": true, "expected_status": "FAIL_EXPECTED"}, {"source": "examples/greedy_change_budget.bld", "invariant": "non-negative", "budget_steps": 60000, "budget_consumed": 495, "expected_status": "PASS"}, {"source": "examples/greedy_change_budget_broken.bld", "invariant": "non-negative", "negative_fixture": true, "budget_steps": 60000, "budget_consumed": 495, "expected_status": "FAIL_EXPECTED"}, {"source": "examples/decay_cross_backend.bld", "invariant": "cross-backend", "cross_backend": "rust", "expected_status": "PASS"}