From 7fa675ebb6d4352e2950724d008590084f34af61 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Sun, 2 Aug 2026 07:06:27 +0000 Subject: [PATCH] Harden V5 evaluation and terminal confirmation Update the evaluator-only testing plan in response to limitations exposed by the V3 and V4 scoring rounds. Separate a direct proof decision from the downstream atoms that depend on it, so one missing root premise remains visible without artificially counting the same reasoning error many times. Require metamorphic holdouts that preserve a semantic obligation while varying surface syntax, terminology, order, and irrelevant structure. This tests the general proof method rather than recall of frozen fixtures. Canonicalize report selection, validation, retry handling, and output caps; preregister objective machine-materializable gates and retain operational attempts separately from the scored corpus. Define a finite sequence of diagnostic and terminal rounds with an explicit maximum round Nmax. Each revision must trace to a general failure class, and the final VN decision must use frozen unseen tasks and absolute gates. Stop only when the preregistered terminal criteria pass or Nmax is reached and the remaining limitations are reported; do not keep adapting tests until a desired answer appears. This commit changes the evaluation protocol, not the V5 runtime instructions, and records no V5 evaluation outcome. gherrit-pr-id: Gbwo6xhidw7eogojb7aokfi2gthtzr6wq --- evals/unsafe-rust/testing-plan.md | 516 +++++++++++++++++++++++++----- 1 file changed, 442 insertions(+), 74 deletions(-) diff --git a/evals/unsafe-rust/testing-plan.md b/evals/unsafe-rust/testing-plan.md index 71b5e0ef37..7af0e7aaee 100644 --- a/evals/unsafe-rust/testing-plan.md +++ b/evals/unsafe-rust/testing-plan.md @@ -8,15 +8,9 @@ > review—never this document, the source catalog, advisory/audit metadata, a > fixing diff, or an intended conclusion. > -> **Status:** active protocol. The initial non-release pilot is recorded in -> [`runs/2026-07-30-exploratory-pilot/`](runs/2026-07-30-exploratory-pilot/). -> The frozen legacy rerun is recorded in -> [`runs/2026-07-31-legacy-regression/`](runs/2026-07-31-legacy-regression/), -> and the 54-run abstraction-design treatment/core-ablation experiment is -> recorded in -> [`runs/2026-07-31-abstraction-design-v1/`](runs/2026-07-31-abstraction-design-v1/). -> The latter confirmed a material workflow improvement but failed its complete -> preregistered gate set; none of these studies is a universal release proof. +> **Status:** active protocol. Preserved executions live under [`runs/`](runs/); +> each run's frozen manifest, rubric, integrity record, and results govern that +> run. No development or evaluation run is a universal release proof. ## Evaluation Objective @@ -68,9 +62,15 @@ agent, or a codebase is universally sound. package execution occurs only in a disposable, credential-free, network-disabled sandbox. 10. **Separate authoring from validation.** Freeze the skill before running an - evaluation. If a result motivates a skill change, assign a new revision - and restart affected conditions; never patch the treatment in place after - observing its outputs. + evaluation. If a result motivates a skill change, assign a new + revision/candidate, rerun cumulative reusable prequalification, and use + only the unconsumed holdout permitted by the terminal program; never patch + a treatment in place after observing its outputs. +11. **Finite terminal confirmation.** Each terminal candidate look uses its one + assigned lineage-disjoint fresh holdout. A failed effective treatment never + reappears; an unchanged treatment may be rebound after `INVALID` only under + the frozen infrastructure rule. Stop only at the first complete conjunctive + pass within the finite claim epoch. ## Evaluation Artifact Architecture @@ -89,7 +89,11 @@ Keep four stores physically separate: - the full manifest described in the source catalog; - audit/advisory/issue/fix provenance; - known-finding atoms and human proofs; - - inaccessible to the audited agent and synthesis agents. + - inaccessible to every evaluated agent, candidate author/editor, + candidate-admission reviewer, candidate-side registrar, and any other + principal or process without the cohort-scoped frozen custody, oracle, + scoring, adjudication, or bounded-adversarial-review role permitted by the + exposure ledger below. 4. **Result store** - immutable prompts, environment manifests, raw transcripts, reports, TCB logs, edits, tool outputs, resource usage, and scores; @@ -225,7 +229,10 @@ record: OS/FFI/environment/deployment, build/proc-macro/supply-chain execution, and non-UB robustness/security; - supported configuration set and trigger subset; -- every expected finding atom and its required discovery scope; +- every expected finding atom, its direct acceptance criterion, required + discovery scope, prerequisite atom IDs, and certificate pass rule; +- an acyclic validated atom-dependency graph and the transitive source-family + or metamorphic-lineage identity used for holdout assignment; - allowed classifications and accepted alternative proof paths; - whether a concrete UB witness is required, optional, or unavailable; - whether the case is Objective defect, Candidate, Scoped positive proof, @@ -297,6 +304,32 @@ and five for release-gating, high-severity, current-zerocopy minimum-oracle, and private-holdout fixtures. Fix the sampling configuration when the platform allows it; otherwise record it. +Predeclare and enforce a runner-controlled output-finalization protocol. A +**run slot** is one frozen fixture × condition × replicate assignment; an +**execution attempt** is one agent process launched for that slot. Permit +exactly one live leased attempt per slot—never concurrent, speculative, or +racing attempts. Before launch, define the complete scoreable output envelope, +including the final response, every required report, TCB log, edit/diff or other +file, relevant metadata, and process disposition. + +The trusted runner, not the agent or coordinator, must atomically seal the +complete declared output tree through compare-and-swap, prohibit post-seal +writes, and record slot/attempt IDs, tree and file digests, byte lengths, +encoding/envelope checks, disposition, and completion state. The first terminal +seal is canonical even if a later coordinator or transport step fails. Its +completion marker means only that the runner sealed the attempt, not that its +content or format is correct. + +A sealed slot cannot be retried; an empty, oversized, malformed, semantically +incomplete, or otherwise defective canonical envelope receives its frozen +consequence. Launch another attempt only after an independently attested, +preregistered exogenous and content-independent operational condition leaves no +canonical seal. A missing handoff caused by agent behavior or any failure whose +classification depends on semantic output is the frozen slot failure, not a +retry opportunity. Never inspect partial semantic content before making a retry +decision. Preserve every lease, attempt, partial artifact, failed seal, retry +attestation, and canonicalization record. + An evaluation is invalid if a skill run gets more time, task-specific context, network, search results, or tool permissions than its baseline. The skill package itself is the intended treatment; no condition may see another @@ -440,11 +473,16 @@ time: - identify the exact operation/contract being justified; - enumerate every precondition; -- derive each conjunct from local facts, named invariants, verified axioms, or - explicit TCB entries; +- derive each conjunct through checked artifact facts, exact applicable + semantic premises, named proved invariants, explicit inference, and any + verified tool theorem or TCB entry; - prove the resulting invariant and mandatory postconditions; - reject a circular, restated, misquoted, inapplicable, or wrong-version proof; - distinguish `UNPROVED`, `UNSOUND`, and `CONTRACT-BROKEN`; +- given one missing premise that blocks several later obligations plus a + separate direct defect, assign one stable root blocker/gap ID, mark every + dependent positive obligation `UNPROVED`, preserve the independent defect, + and do not duplicate the root omission as several findings; - trace dataflow from a state-producing unsafe API to a later consumer; - treat an adversarial safe trait implementation or callback correctly; - recognize all safe API surfaces, including public fields, constructors, @@ -466,7 +504,7 @@ matching. Use the pinned source and closure process in [source-catalog.md](source-catalog.md). -Build four sub-suites: +Build four required sub-suites and one optional fifth: 1. **`GRA-ATOM`:** one focused blind fixture for every confirmed note atom. This is the direct capability regression: can the skill recover every known @@ -553,7 +591,7 @@ repair covered only one of several consumers. Materialize the exact immutable current commit identified in the source catalog, not the live worktree. Import the catalog/manifest's current invariant-owner shards. Run each with five fresh skill agents, five no-skill -baselines, and at least three previous-skill agents. Give each shard enough +baselines, and five previous-skill agents. Give each shard enough budget to close its own surface and configuration partition. The shard manifest must contain an invariant-owner/boundary coverage map @@ -730,6 +768,46 @@ fixtures, not private holdouts. Keep true holdout identities, source, and answers only in an access-controlled store and refer to them in this plan by opaque cohort/version ID. +Assign the conservative transitive closure of every common source/incident +ancestor and every direct, reduced, renamed, reordered, or other metamorphic +descendant to one lineage group. Treat that group as indivisible. +Every terminal cohort must be lineage-disjoint from all public or exposed +development fixtures, prequalification cases, runtime examples, prior results, +and earlier or later terminal cohorts—not merely from the other holdouts. +Permanently retire a cohort from confirmation when any of its semantic source, +expected behavior, oracle, or result is exposed. A retired cohort may become a +regression fixture but can never confirm a later candidate. Retirement occurs +at first exposure; **consumption** occurs only after the bound look receives its +terminal disposition and completes every frozen scoring and adjudication step. +Only then may its content inform a later candidate through the append-only +regression transition. + +Maintain an append-only principal/process exposure ledger. Any person, agent, +service, or process exposed to any semantic source, oracle, lineage datum, or +content-derived signal for an unconsumed cohort is tainted with that cohort. +Roles are cohort-scoped: + +- A current-look actor may be tainted only by `H_n` and already consumed + cohorts, never by a later or unbound cohort. While `H_n` is unconsumed, that + actor may perform only the frozen execution, oracle, scoring, consistency, + adjudication, or bounded-adversarial-review role for `C_n/H_n`; it may not + author, advise, admit, or select a later candidate or alter a candidate-facing + protocol component. +- A person or process with semantic access to any later/unbound cohort may + perform only its frozen future-bank custody or commitment role. It may not + access candidate bytes, outputs, scores, gate inputs, or results and may not + execute, review, score, adjudicate, author, advise, admit, or select a + candidate. The fixed opaque verifier is the only bridge and emits only the + terminal eligibility result specified below. +- Candidate authors, editing agents, candidate-admission reviewers, and + candidate-side registrars remain untainted by every unconsumed cohort and its + lineage map. + +These rules include holdout/oracle authors, special adjudicators, custodians, +services, and unnamed intermediaries. Any candidate-linked access crossing from +a later/unbound cohort permanently aborts the claim epoch, retires every +affected cohort, and emits no candidate-facing detail or repair opportunity. + ## Scoring Model ### Per-finding atom @@ -741,8 +819,8 @@ Score applicable dimensions on a three-point scale: | Discovery | Missing or wrong location | General concern near relevant code | Exact location/surface and full affected scope | | Required proposition | Wrong or absent | Some pre/postconditions identified | Every applicable pre/postcondition stated concretely | | Dataflow/invariant chain | Missing or circular | Partial producer/consumer trace | Every establishment, transition, suspension, consumer, and exit path accounted for | -| Premises and authority | Folklore, unchecked, or hallucinated | Plausible but incomplete support | Local facts checked; exact versioned authority verified; non-axioms explicit in TCB | -| Valid-use reasoning | Hidden caller assumption | Some adversarial cases | Quantifies over all valid uses and adversarial safe caller behavior | +| Premises and authority | Folklore, unchecked, or hallucinated | Plausible but incomplete support | Artifact facts checked; every consumed semantic effect follows from exact applicable authority, verified tool theorem, or explicit TCB; implication direction is valid | +| Valid-use reasoning | Hidden, circular, or assumed caller/implementer path | Some adversarial cases or certificate components | Closes source selection, boundary access/inputs, typing/coherence, every boundary contract owned outside the audited scope—including contracts imposed on witness-supplied code—plus corresponding unsafe-context obligations and TCB applicability, without assuming the in-scope audited safety assertion | | Configuration closure | Trigger/config missed | Trigger found but no supported-set proof | Every actually supported combination covered concretely or abstractly | | Classification | Incorrect verdict | Concern found but statuses conflated | Exact independent status for soundness, postconditions, and conditional claims | @@ -771,6 +849,31 @@ Use separate rubrics: Do not aggregate scores across task modes or theorem domains as if their denominators were equivalent. +### Dependency-aware atom decisions + +For rubrics whose atoms depend on other certificates, freeze an acyclic +dependency graph and each atom's direct criterion before collection. Blind +scorers first decide the proposition directly demanded by each atom without +mechanically copying prerequisite failures. The evaluator then computes: + +```text +blocked_by(a) = immediate prerequisites whose certificate_decision is not PASS + +certificate_decision(a) = PASS + iff direct_decision(a) is PASS and blocked_by(a) is empty +``` + +Preserve `direct_score` or `direct_decision`, immediate `blocked_by` IDs, +`certificate_decision`, and the transitive set of `root_failures`. If an atom +both fails directly and has failed prerequisites, record both. “Root” is +relative to the frozen rubric graph; it is not a claim about the agent's mental +process. + +Release gates use `certificate_decision`: directly stating a downstream +conclusion does not prove it when a consumed prerequisite is unproved. Root and +fan-out aggregates are diagnostic and may never convert a blocked certificate +to success. + ### Per-run dimensions Measure: @@ -780,7 +883,9 @@ Measure: - unsupported `UNSOUND` and unsupported `PROVED` rates; - safe-surface discovery; - obligation-ledger completeness; +- root-blocker/fan-out accuracy and nonduplicative finding accounting; - local proof completeness and non-circularity; +- artifact-to-semantics edge closure and exact implication-direction accuracy; - citation accuracy, versioning, quotation scope, and actual verification; - TCB completeness, precision, versioning, and non-vacuity; - adversarial safe-caller handling; @@ -845,47 +950,273 @@ Before the first scored run, freeze: - numerical non-inferiority and improvement margins; and - opaque holdout cohort/version IDs. -The default gates are intentionally demanding: - -1. Every admitted Objective-defect atom appears in an evaluator-oracle-blind - fixture. -2. Every admitted Objective-defect atom is recovered and correctly classified - in every skill-enabled focused replicate. -3. Every atom in a `GRA-MULTI` fixture is recovered in every release-gating - focused replicate; finding only the first issue fails that fixture. -4. A preregistered full-source/sharded recall cohort meets its explicit - issue-level target. Use 100% when the prompt, scope, partition, and budget - expressly ask for complete recovery. Report broader naturalistic - full-repository recall per replicate without relabeling every stochastic - miss a hard error. -5. There are zero hard errors. -6. On focused Objective-defect fixtures, every applicable proof dimension - scores 2. Full-source cohorts have no applicable dimension at 0 and meet a - preregistered mean/floor. -7. Fixed-side controls do not reproduce the repaired finding. Other valid - findings remain allowed. Scoped positive proofs are accepted only within - their exact theorem/model/TCB; Candidate and Challenge fixtures are never - global soundness labels. -8. Every admitted Objective-defect item in the current-zerocopy minimum oracle - is addressed by each owning shard with correct - production/test/configuration scope. Candidate/Challenge entries are judged - on reasoning and calibration, not issue agreement. -9. Every authoring fixture produces no unsound or vacuous edit and satisfies - all applicable contract, postcondition, configuration, TCB, and - compatibility dimensions. -10. The runner emits a successful automated attestation for filesystem, - package, prompt, network, documentation, and paired-side isolation. -11. The opaque holdout cohort has 100% focused Objective-defect recall, zero - hard errors, required proof-quality floors, no repaired-defect false - assertion, and no fixture-specific runtime-skill change. -12. Skill-versus-baseline/prior-skill effects meet preregistered endpoints. - Suggested defaults are zero additional hard errors; a lower 95% paired - confidence bound above -2 percentage points for recall, adjudicated - precision, and proof-floor pass rate; and either a +10-point absolute - improvement or standardized paired effect of at least 0.5 on a primary - behavior the skill is intended to change. When the baseline is already at - least 95% and the skill meets the absolute safety floors, a preregistered - ceiling rule may accept non-inferiority without artificial “improvement.” +Before exposure, translate every normative default and run-specific gate into a +versioned mandatory-root inventory. Map each normative requirement to a stable +root gate ID and exact aggregation rule, and validate set equality plus acyclic +dependency closure between that inventory and the executable manifest. Obtain +an independent completeness signoff. An omitted root, orphaned prerequisite, +weakened predicate, cycle, or mapping mismatch can never pass and receives the +frozen abort/`INVALID`/`FAIL` disposition. + +The default root gates are intentionally demanding and nonwaivable: + +1. **`G-ORACLE-COVERAGE`:** Every admitted Objective-defect atom appears in an + evaluator-oracle-blind fixture. +2. **`G-FOCUSED-RECALL`:** Every admitted Objective-defect atom is recovered and + correctly classified in every skill-enabled focused replicate. +3. **`G-MULTI-COMPLETE`:** Every atom in a `GRA-MULTI` fixture is recovered in + every release-gating focused replicate; finding only the first issue fails + that fixture. +4. **`G-NATURALISTIC-RECALL`:** A preregistered full-source/sharded recall cohort + meets its explicit issue-level target. Use 100% when the prompt, scope, + partition, and budget expressly ask for complete recovery. Report broader + naturalistic full-repository recall per replicate without relabeling every + stochastic miss a hard error. +5. **`G-NO-HARD-ERROR`:** There are zero hard errors. +6. **`G-PROOF-QUALITY`:** On focused Objective-defect fixtures, every applicable + proof dimension scores 2. Full-source cohorts have no applicable dimension + at 0 and meet a preregistered mean/floor. +7. **`G-CONTROLS`:** Fixed-side controls do not reproduce the repaired finding. + Other valid findings remain allowed. Scoped positive proofs are accepted + only within their exact theorem/model/TCB; Candidate and Challenge fixtures + are never global soundness labels. +8. **`G-CURRENT-ZEROCOPY`:** Every admitted Objective-defect item in the + current-zerocopy minimum oracle is addressed by each owning shard with + correct production/test/configuration scope. Candidate/Challenge entries are + judged on reasoning and calibration, not issue agreement. +9. **`G-AUTHORING`:** Every authoring fixture produces no unsound or vacuous edit + and satisfies all applicable contract, postcondition, configuration, TCB, + and compatibility dimensions. +10. **`G-ISOLATION`:** The runner emits a successful automated attestation for + filesystem, package, prompt, network, documentation, and paired-side + isolation. +11. **`G-HOLDOUT`:** The opaque holdout cohort has 100% focused Objective-defect + recall, zero hard errors, required proof-quality floors, no repaired-defect + false assertion, and no fixture-specific runtime-skill change. +12. **`G-COMPARISON`:** Skill-versus-baseline/prior-skill comparisons meet + preregistered endpoints. + In inferential mode, suggested defaults are zero additional hard errors; a + sequence-adjusted lower paired confidence bound at the preregistered + family-wise confidence level above -2 percentage points for recall, + adjudicated precision, and proof-floor pass rate; and either a +10-point + absolute improvement or standardized paired effect of at least 0.5 on a + primary behavior the skill is intended to change. When the baseline is + already at least 95% and the skill meets the absolute safety floors, a + preregistered ceiling rule may accept non-inferiority without artificial + “improvement.” In exact engineering-gate mode, use only the frozen exact + comparison predicate and report its named finite observations + descriptively. Do not claim an effect, improvement, non-inferiority, + probability, target-population property, or generalization. +13. **`G-ADVERSARIAL-REVIEW`:** Every slot in a preregistered bounded review + completes. Freeze at least two independent qualified reviewers, their + independence from candidate authoring/admission, and their attested absence + of taint from every later/unbound cohort. Freeze their exact review materials + and scope, prompts, tools, budgets, number of passes, output schema, and + disagreement/adjudication rule. This is a distinct current-look + bounded-adversarial-review role: it may access only `H_n`, consumed history, + the complete candidate package, canonical reports and audit artifacts, + scoring/adjudication and gate inputs, and protocol/integrity evidence. + Missing, partial, invalid, cross-cohort, or unpreserved review output cannot + pass. +14. **`G-NO-MATERIAL-FINDING`:** Every candidate finding from the bounded review + receives an evidence-backed disposition under the frozen versioned + materiality rule and adjudication procedure. The nonwaivable inclusive floor + qualifies at least any candidate unsoundness or vacuity; hard-error + enablement; oracle/holdout leakage; isolation, gate, retry, output, + identity, claim, stopping, or other protocol evasion/weakening; unsupported + inference or terminal assertion; candidate-specific overfit; or defect + capable of changing a mandatory-root predicate, input, outcome, or the + scoped terminal claim. A run-specific rule may add findings but never + exclude this floor. `PASS` requires zero unresolved or qualifying in-scope + material defects and no `UNKNOWN`/`ERROR` disposition. A qualifying finding + makes the look `FAIL`; it may not be removed by post-exposure quarantine, + scope revision, or candidate repair. + +### Finite terminal-candidate program + +Development and regression fixtures may be reused for prequalification. A +terminal declaration requires a separate finite claim-level confirmatory +program. Its immutable **claim epoch** owns every look and all persistent state; +operational successor sequences are permitted only by its frozen restart rule +and cannot reset that state. Before exposing its first holdout, freeze: + +- a content-addressed immutable genesis manifest containing every frozen field + in this list, and its digest as the canonical claim-epoch ID; whether the + release makes only an exact engineering-gate claim or also an + inferential/statistical claim; the exact user-facing assertion; and a + substantive claim-equivalence rule that does not depend on labels or file + identity; +- for an inferential claim, its estimand, target population, sampling and + assignment units, lineage/dependence treatment, and selection-valid analysis; +- a finite positive global `N_max`, the maximum number of terminal candidate + looks across the claim epoch and every permitted successor sequence; +- mutually disjoint opaque cohorts `H1 ... HN_max`, allocated by indivisible + source/metamorphic lineages that are also disjoint from every exposed + development, prequalification, example, and prior-result lineage, together + with the lineage-commitment, candidate-side registrar, opaque-verifier, and + collision/TCB rules used for later eligibility checks; +- an effective-treatment identity and equivalence schema over every + agent-visible candidate component and the frozen environment; a new name or + digest is not by itself a distinct treatment; +- every program-invariant component: model and sampling policy, prompts, tools, + documentation, base prequalification corpus, holdout bank and lineage map, + runner, budgets, scorer, adjudication, and all protocol policies; each + candidate's agent-visible runtime byte tree is frozen separately before its + assigned exposure; +- the persistent cumulative regression bank and its sole permitted mutation: + append each retired cohort and generalized adjudicated regression after its + current look; +- the claim epoch's persistent append-only candidate-admission registry; for + each effective treatment it records identity and byte-tree digests, exposure + and outcome, and the evidence-backed behavior-affecting revision that makes a + distinct later treatment eligible; +- every replicate, retry, atomic-output-finalization, invalidation, and + irreversible fail-fast rule; +- the versioned mandatory-root gate inventory and a total executable gate + manifest in which every gate has a stable ID, predicate and version/digest, + typed inputs, prerequisites, missing/error behavior, and output; this includes + the bounded adversarial-review procedure, its frozen materiality rule, and the + admission rule for a later candidate revision; +- the complete conjunctive stopping predicate; and +- any across-candidate statistical error-control rule. + +Claims belong to the same epoch when a pass would be used to support the same +user-facing release assertion or an aliased, overlapping, or post-exposure +narrowing of its artifact/domain, population, estimand, or endpoints. Cosmetic +rewording cannot create a fresh epoch. A genuinely non-overlapping claim may +start a new epoch under an independently specified rule, but cannot establish +`VN` retroactively for this one. + +A candidate enters the program only after passing the entire cumulative +prequalification and a subtractive/coherence review of its runtime instructions, +routed references, templates, and maintainer rationale. A **candidate look** is +the complete binding and evaluation of one frozen candidate against its +assigned cohort; it is distinct from the slot-level execution attempts governed +by the retry policy, and its index is global across the claim epoch. **Semantic +exposure** begins at the earliest candidate-linked human or process access to +any holdout bit, contract, oracle or lineage content, or content-derived signal, +regardless of which security boundary contains the access. Only demonstrably +content-oblivious harness checks whose decisions are independent of those +semantics and the fixed nonrevealing lineage-commitment check below may precede +exposure. Any human semantic comparison or additional/cohort-specific signal +counts as exposure. For candidate look `n`: + +Permit exactly one active candidate look in the claim epoch, including across +operational successor sequences. Do not pre-admit, freeze for terminal use, +bind, expose, or run `C_{n+1}` while `C_n` lacks a terminal outcome. Conditions, +replicates, and slot attempts within the one bound look may use only their +frozen schedule and retry rules. + +1. Freeze candidate `C_n`. A candidate-side registrar untainted by every + unconsumed holdout commits the complete candidate-author exposure and source + lineage set without accessing the holdout map. Before binding `H_n`, a fixed + trusted verifier compares only the precommitted opaque lineage identifiers + for `C_n`, the accumulated bank, and every unconsumed cohort. It may emit + only `PASS` or permanent claim-epoch `ABORT`; it reveals no cohort-specific + result and permits no candidate repair, retry, or cohort substitution. Any + semantic inspection, incomplete registrar basis, other output, or verifier + change invokes the frozen failure rule. Candidate authors and editing agents + remain unable to access any unconsumed cohort or its lineage map. +2. At first semantic exposure, retire `H_n` permanently from later + confirmation. It becomes consumed only when this look terminalizes. + Retirement permits only the frozen completion, slot-retry, scoring, + consistency, and adjudication operations for this already-bound `C_n/H_n` + look. +3. Run every required condition and replicate. A favorable partial cohort can + never pass. Fail-fast is permitted only to record an irreversible `FAIL`. +4. Materialize every human adjudication or materiality decision into the + manifest's typed inputs, validate exact root-inventory equality and complete + dependency closure, then compute and publish every required root and + prerequisite with its predicate and input digests. Only explicit `PASS` for + every required root and its transitive prerequisites passes; a missing or + weaker root, closure error, or `UNKNOWN`/`ERROR` result can never support + `PASS` and receives the frozen abort/`FAIL`/`INVALID` disposition. +5. Assign exactly one look outcome: + - `PASS` when the complete cohort is valid and every required gate passes; + - `FAIL` when the protocol-valid complete look has a failed gate or a frozen + irreversible fail-fast predicate fires; or + - `INVALID` only under a frozen infrastructure/protocol invalidation + predicate, never because of report content or an unfavorable result. + +An infrastructure failure before semantic exposure is not a look and may be +retried against the same cohort under the frozen rule. After exposure, `H_n` is +consumed even if the outcome is `INVALID`; any further confirmatory evaluation +uses `H_{n+1}`. The same frozen candidate may be rebound after `INVALID` only +when the predeclared infrastructure-only rule permits it. Predeclare whether +the valid retry is an unchanged-candidate rebind or requires a later candidate. +In inferential mode, every exposed invalid look must spend its `alpha_n` +allocation or be accounted for by the preregistered always-valid sequential +method. In exact engineering-gate mode, it consumes one of the finite `N_max` +candidate looks in the claim epoch. An unexposed prelaunch failure consumes +neither. Slot-level execution retries remain governed by the leased-attempt and +atomic whole-envelope canonicalization rule and do not create extra candidate +looks. + +Any agent-visible runtime-package change after exposure creates a new +candidate. Any unpermitted change to a program-invariant environment, holdout, +scorer, gate, identity rule, or protocol component aborts the operational +sequence; it cannot be treated as another candidate. A successor sequence may +continue the claim epoch only under the predeclared restart transition and must +inherit its claim/effective-identity rules, cumulative regression bank, +candidate registry, exposure and outcome ledger, remaining holdouts and global +look budget, gate roots, stopping rule, and remaining statistical error budget. +Otherwise the epoch terminates without `VN`. A post-exposure fixture quarantine +or protocol repair never retroactively preserves the consumed look. + +Before `C_{n+1}` may be admitted or bound, `C_n` must have exactly one sealed +terminal outcome, `H_n` must be consumed, every frozen scoring/adjudication step +must be complete, and the outcome, exposure, cumulative-bank, and registry +transitions must be atomically preserved. Add every revealed earlier cohort and +every generalized regression derived from its adjudicated failures to reusable +prequalification through the frozen append-only transition. After `FAIL`, the +revision must contain a documented evidence-backed **effective-treatment** +response under the frozen admission rule; an evaluator-only, comment-only, +metadata-only, editorial, or identity-only mutation that cannot affect agent +behavior does not buy another holdout look. The next candidate must pass the +accumulated bank without adding fixture-specific runtime instructions. A +protocol-valid `FAIL` permanently makes its whole effective-treatment +equivalence class ineligible for another holdout look in the claim epoch, +including any successor sequence or aliased claim, until the registry records +an admitted evidence-backed behavior-affecting revision. The frozen admission +rule, not a candidate-supplied label or digest, decides distinctness. + +Stop at the smallest global `n` whose entire cohort passes every frozen gate. +`VN` is the immutable terminal record containing the claim-epoch ID, look index, +the complete genesis manifest and digest—including the exact assertion, mode, +claim-equivalence rule and, when applicable, estimand/population/analysis— +candidate effective-treatment identity and byte-tree digest, environment, +prompt/tool/corpus/holdout/protocol/gate identities, canonical output and +scoring/adjudication manifests, complete `PASS` result, and a digest of the +entire claim-epoch history: candidate admissions/identities/outcomes, prior +canonical manifests, exposure/taint and cohort lifecycle ledgers, cumulative +bank transitions, used/remaining global looks and alpha, retries, invalidations, +and successor transitions. The candidate may be called version `VN` only for +the exact assertion bound by that genesis manifest; terminal status is not an +intrinsic context-free property of its bytes. `G-NO-MATERIAL-FINDING` means only +that the frozen bounded procedure produced no unresolved qualifying finding; it +does not claim that no undiscovered defect can exist. + +If no candidate passes by the claim epoch's global `N_max`, close the epoch +permanently without a successful `VN`. No successor protocol, fresh bank, +relabeling, overlap, or post-exposure narrowing can extend its look budget or +produce `VN` for it. A genuinely new non-overlapping claim cannot retroactively +rescue the closed epoch. + +For an inferential claim, allocate look-level error budgets `alpha_n` with +`sum(alpha_n) <= alpha_total` or use another valid preregistered sequential +method. Each look's joint pass test must be conditionally valid given all prior +information and adaptive selection in the complete history, including prior +outcomes, invalidations, candidate revisions and admissions, endpoint and model +choices, missingness, adjudication, and protocol decisions. It must charge +endpoint, model, selection, missingness, and other multiplicity within its +allocation. Every permitted successor sequence inherits only the claim epoch's +remaining `alpha_total`; freezing a new protocol does not reset it. Disjoint +cohorts alone do not remove optional-stopping inflation. Exact engineering-gate +mode supports only the descriptive proposition that the named candidate digest +passed the named gate roots on the named finite slots under the frozen +environment. Any causal, probabilistic, population, expected-future, +generalized-quality, improvement, or non-inferiority claim requires inferential +mode and its selection-valid method. The 2,177-record GRA ledger remains the full corpus-closure goal, but completing it is not a prerequisite to begin with a frozen, semantically adjudicated @@ -919,8 +1250,10 @@ For every objective atom, two qualified reviewers should independently: 5. check the safe reproducer or proof when available; 6. inspect the repair and confirm what it changes; 7. classify soundness, postcondition, compatibility, and conditional claims - separately; and -8. reconcile disagreements before the atom becomes an Objective defect or + separately; +8. agree on each atom's direct acceptance criterion, prerequisites, and acyclic + dependency graph; and +9. reconcile disagreements before the atom becomes an Objective defect or Scoped positive proof. Audit notes, advisories, upstream acknowledgements, and fixing diffs are strong @@ -987,7 +1320,7 @@ This is a fast regression signal, not the release claim. ### Candidate-release suite -Run: +For reusable prequalification, run: - every microfixture; - every `GRA-ATOM` and `GRA-MULTI` fixture; @@ -995,8 +1328,12 @@ Run: - all zerocopy historical cases; - all current zerocopy shards and integration; - all authoring/review/evidence tests; -- fixed/proved/calibration controls; and -- the opaque access-controlled holdout cohort. +- fixed/proved/calibration controls. + +After every reusable item passes, freeze the complete candidate and run its one +assigned opaque access-controlled holdout cohort. Apply the finite +terminal-candidate program for a terminal declaration; do not use that cohort +as an iterative debugging set. ### Full corpus suite @@ -1034,8 +1371,24 @@ Publish a report containing: - contamination checks; - automated isolation attestation; - condition/replicate counts and resource budgets; +- the complete content-addressed claim-epoch genesis manifest and digest, + including the exact assertion, mode, equivalence rule and any inferential + estimand/population/analysis; terminal candidate index, global `N_max` use, + effective-treatment/package/protocol identities, persistent registry and + cumulative-bank transitions, assigned/retired/consumed cohort IDs, lineage + and taint-ledger checks, and any alpha spending; +- every run slot, attempt lease, execution attempt, whole-envelope atomic + finalization disposition, retry attestation, and canonical-envelope selection; - separately reported task modes and theorem domains; - issue-level results, with no known atom hidden by aggregate metrics; +- direct/root atom failures separately from certificate failures and their + `blocked_by` fan-out; +- the mandatory-root inventory and total gate-manifest digests, root/dependency + closure validation, every gate's predicate/input digests, explicit + machine-readable outcome, and resulting terminal record or failure status; +- every bounded adversarial-review packet, reviewer-independence attestation, + candidate-finding disposition and adjudication, and the + `G-ADVERSARIAL-REVIEW`/`G-NO-MATERIAL-FINDING` inputs and outcomes; - hard errors; - precision after novel-finding adjudication; - configuration and safe-surface coverage; @@ -1067,6 +1420,11 @@ Actively monitor: - scorer awareness of condition; - evaluator disagreement hidden by one numeric score; - model updates being mistaken for skill improvements; +- repeated-candidate optional stopping or unchanged-candidate resubmission; +- holdout leakage through source-family or metamorphic siblings assigned to + different cohorts; +- post-exposure fixture quarantine, substitution, retry, or package edits that + preserve a favorable result while changing its frozen denominator; - duplicating one incident across RustSec, GHSA, audit logs, and research datasets; and - benchmark-specific instructions accreting into the runtime skill. @@ -1074,9 +1432,10 @@ Actively monitor: The response to contamination is access-controlled metamorphic/holdout renewal, not more explicit hints in the prompt. -## Readiness Checklist for the Follow-Up Testing Turn +## Per-Sequence Release-Gate Readiness Checklist -Before running the first agent: +Before launching the first semantic agent in a claim epoch, and again for every +applicable inherited item before a permitted successor sequence: 1. Freeze the skill revision. 2. Implement the private fixture/oracle manifest and result schema. @@ -1093,14 +1452,23 @@ Before running the first agent: 9. Construct and review the hardened no-network VM/microVM runner for any executable artifact. 10. Dry-run only the harness on a trivial non-evaluation fixture. -11. Freeze prompts, corpus denominator/exclusions, budgets, conditions, - replicate/stopping/retry rules, numerical endpoints/margins, and scorer - rubrics. +11. Freeze the canonical claim epoch and equivalence rule, effective-treatment + identity/equivalence and admission rules, prompts, corpus + denominator/exclusions, persistent regression/registry state, budgets, + conditions, leased-attempt/retry/finalization/invalidation rules, numerical + endpoints and margins, scorer rubrics, exact-engineering versus inferential + mode, mandatory gate-root inventory and total fail-closed executable + manifest, global finite `N_max`, fully lineage-disjoint holdout cohorts, + exact terminal stopping predicate, and across-candidate/successor error + control. 12. Calibrate independent scorers and resolve every admission disagreement. 13. Verify in an automated attestation that agents cannot read `evals/`, `maintainers/`, sibling worktrees, prior results, another condition's skill - package, or the other half of any pair. + package, or the other half of any pair; validate the principal/process + exposure ledger and role restrictions for every unconsumed holdout. -Only then begin semantic testing. Any skill change made in response to a result -starts a new skill revision and requires fresh runs; do not continue the same +Only after every applicable item is satisfied may that sequence begin semantic +testing. Any agent-visible skill change made in response to a result creates a +new candidate: rerun the cumulative reusable prequalification and admit a fresh +terminal look only under the claim epoch's frozen rule. Never continue the same agent conversation.