From 301b6e0848234964331037c68cd57b4a57cd4f80 Mon Sep 17 00:00:00 2001 From: Zain Dana Harper <17142659+HarperZ9@users.noreply.github.com> Date: Wed, 29 Jul 2026 11:48:27 -0700 Subject: [PATCH 1/3] feat: 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, never from the kernel's own arithmetic. The recompute runs twice. Stage A, over the sealed measurement series before any re-run: a tampered-and-resealed interval is a pure data contradiction, rejectable with no C compiler, so the self-test's no-compiler property stays intact. Stage B, over the re-parsed re-run series: a new failure class, MC_INTERVAL_DRIFT, for a receipt that stays internally coherent while no longer describing the run it names. Mutation-tested (Stage B skipped for EXECUTED receipts) to confirm it is load-bearing, not redundant with Stage A. The declared sample count becomes a WITNESSED denominator: the final row's trials must equal monte_carlo.samples, the single biggest honesty gain of the slice. Coherence is checked as a cumulative Bernoulli count (integers below 2^53, trials incrementing by exactly 1, successes non-decreasing in {0, 1}, successes <= trials on every row). Executable vocabulary v1: estimator proportion; interval methods normal-approx-95 (refused at the boundary proportion, a zero-width interval there overclaims precision) and wilson-95; clopper-pearson-95 is sealed-successes-only, not executable (needs a verified inverse incomplete beta with no in-tree oracle), refused at emit and verify. An EXECUTED block adds three not_claimed entries, present if and only if the block is EXECUTED: sample_independence, interval_coverage, estimator_semantics. EXECUTED hardens the interval arithmetic and the denominator; it cannot and does not harden that the draws are independent, that the named confidence level covers the true value, or that the indicator counts what the author says it counts. This is load-bearing honesty, not decoration: the receipt states in sealed machine-readable form exactly which reading of an EXECUTED interval is licensed. Backward compatible: DECLARED receipts stay valid forever. The five new fields are Option with skip_serializing_if; a DECLARED block's serialized JSON carries exactly its original four keys, pinned by a new test asserting the key set directly rather than assuming skip_serializing_if behaves. Shipped with: a new kernel pair, mc_pi_rejection_executed.bld and its wrong-area negative fixture, same seed-42 stream as the DECLARED sibling, calibration numbers measured by running the emitted receipt (not invented): successes 1551 of 2000, estimate 0.7755, wilson-95 interval [0.7566951910008709, 0.7932485159471586]. The negative fixture seals the slice's central lesson: the wrong-area factor only scales the estimate, never the raw successes/trials counters, so the interval executes and re-derives cleanly while the slack column still blows the truth band. Corpus 27 -> 29. A tenth self-test case (nudge the sealed interval_high on an EXECUTED block, reject through Stage A). Nine new CLI tests covering the round trip and every emit-refusal path. Docs (SCIENTIFIC-RECEIPT flags/schema/family/failure-classes/self-test/ corpus, CHANGELOG) and the plan/design docs in the writing-plans idiom. Verified: full suite 1,644 passed / 0 failed (up from a 1,605 pre-slice baseline measured at the start of final verification), exit codes captured before any pipe; corpus 29/29, run twice for determinism; self-test 10/10; cargo fmt --check clean. Every new gate mutation-tested by literal inverse edit, never git checkout: sixteen gates broken, observed red, restored, observed green, including one mutation (a sign flip inside the Wilson formula's square root) that only the hand-computed-value unit test catches, and one (the Stage B skip) that proves Stage B is not redundant with Stage A. Co-Authored-By: Claude Fable 5 --- CHANGELOG.md | 26 + compiler/src/main.rs | 110 +- compiler/src/scientific_runtime.rs | 1106 ++++++++++++++++- compiler/tests/cli.rs | 550 +++++++- docs/SCIENTIFIC-RECEIPT.md | 121 +- .../plans/2026-07-29-mc-executed-intervals.md | 973 +++++++++++++++ ...2026-07-29-mc-executed-intervals-design.md | 347 ++++++ examples/mc_pi_rejection_executed.bld | 58 + examples/mc_pi_rejection_executed_broken.bld | 43 + examples/scientific-corpus.json | 2 + 10 files changed, 3266 insertions(+), 70 deletions(-) create mode 100644 docs/superpowers/plans/2026-07-29-mc-executed-intervals.md create mode 100644 docs/superpowers/specs/2026-07-29-mc-executed-intervals-design.md create mode 100644 examples/mc_pi_rejection_executed.bld create mode 100644 examples/mc_pi_rejection_executed_broken.bld 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/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..c87e4a7b 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); 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"} From cbec98c7f82ea4f746c4b103552333401f6687bf Mon Sep 17 00:00:00 2001 From: Zain Dana Harper <17142659+HarperZ9@users.noreply.github.com> Date: Wed, 29 Jul 2026 11:53:01 -0700 Subject: [PATCH 2/3] docs: refresh README and STATUS counts to the measured post-slice baseline Pure count refresh, re-verified fresh on this branch rather than trusting slice-authoring-time numbers (the units slice merged to main after the executed-intervals slice was authored, so the rebased totals differ from both slices' own reports): cargo test 1683 passed, 0 failed, 11 ignored (lib 1004 with 1001 passed and 3 ignored, bin 179, cli 341, gpu 12, lexer 52, parser 98); buildc receipt corpus 29/29; verifier --self-test 10/10 on a freshly emitted executed-interval receipt; buildc corpus verify 8/8. The STATUS baseline enumeration also gains the wave's three newest members (executed intervals, drop flags, unit-annotated types) so the rise it explains matches what produced it. Co-Authored-By: Claude Fable 5 --- README.md | 4 ++-- STATUS.md | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) 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. From 68c54013342472dc43397b6e154182e3b9e103a4 Mon Sep 17 00:00:00 2001 From: Zain Dana Harper <17142659+HarperZ9@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:15:00 -0700 Subject: [PATCH 3/3] fix: name the clopper-pearson refusal through its constant The review's one finding: MC_INTERVAL_CLOPPER_PEARSON_95 was used only in tests, tripping dead_code. The arm that refuses the method now formats its message through the constant, making it the single source of the name. Co-Authored-By: Claude Fable 5 --- compiler/src/scientific_runtime.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/scientific_runtime.rs b/compiler/src/scientific_runtime.rs index c87e4a7b..2e24876b 100644 --- a/compiler/src/scientific_runtime.rs +++ b/compiler/src/scientific_runtime.rs @@ -1279,7 +1279,7 @@ pub fn compute_mc_executed( } 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" + "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" )); } };