From 478ac50069c35aadffccec08a28ef1a5f33ea6e8 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Sat, 1 Aug 2026 10:34:57 +0000 Subject: [PATCH] Analyze the V3 targeted confirmation failures Perform a post-result qualitative analysis without changing the official V3 decision. Trace each miss back to the proof structure that produced it rather than adding a checklist of fixture-specific mistakes. The configuration failures omit the semantics of combinators such as all and not, then assert closure of the resulting product or complement. The exact-domain failures compress an ordered, fallible build into an endpoint mapping and therefore cannot reconstruct which intermediate states are reachable. Several reports state that two sets are incomparable without giving both separating witnesses. One otherwise-correct report omits authority for the usize domain. Another seeks a maximal bad-input remainder even though one complete existential witness is sufficient for UNSOUND. These observations explain why Required/Covered and verdict certificates were necessary but not sufficient: the representation still allowed lossy summaries to masquerade as exact derivations. They motivate V4's explicit case domains and fibers, set-relation certificates, staged construction relations, reversible transformations, and demand-driven counterexample scope. Keep these as general proof obligations rather than embedding the evaluated fixtures in the runtime skill. gherrit-pr-id: Glzlcl663nbggljjqi64x7gs3yyw5b7ys --- .../qualitative-findings.md | 310 ++++++++++++++++++ 1 file changed, 310 insertions(+) create mode 100644 evals/unsafe-rust/runs/2026-07-31-v3-targeted/qualitative-findings.md diff --git a/evals/unsafe-rust/runs/2026-07-31-v3-targeted/qualitative-findings.md b/evals/unsafe-rust/runs/2026-07-31-v3-targeted/qualitative-findings.md new file mode 100644 index 0000000000..a0ddf7899b --- /dev/null +++ b/evals/unsafe-rust/runs/2026-07-31-v3-targeted/qualitative-findings.md @@ -0,0 +1,310 @@ +# V3 Targeted Confirmation: Qualitative Findings + +## Status + +The preregistered V3 gate failed. This run is preserved as evidence about the +frozen V3 package, not rewritten into a passing result. + +The run collected all 80 planned reports, obtained all 16 blind scores, used +blind adjudication for the four modes with scorer disagreement, and produced +the frozen aggregate in [results/aggregate.json](results/aggregate.json). Three +first report attempts were lost to orchestration interruption and were +preserved as `ORCHESTRATOR_TOOL_FAILURE`; their second attempts completed. No +canonical report had an operational scope deviation, semantic noncompletion, +or word-budget defect. + +The candidate passed 272 of 300 atom decisions. That aggregate number is only +descriptive: modes are heterogeneous, and the preregistered rule required every +V3 atom to pass in all five replicates. The exact result is in +[results/summary.md](results/summary.md): + +- every atom passed 5/5 in `S`, `Q`, `W`, `M`, `R`, and `K`; +- `C1` passed 1/5 and `C3`–`C5` passed 3/5; +- `X4`, `X6`, and `X7` passed 0/5, while `X11` passed 2/5; +- two `C` reports contained hard errors and TCB/authority defects; and +- one `K` report had a TCB/authority-accounting defect without a hard error. + +The frozen V3 package is byte-identical to the current `skills/unsafe-rust` +package at the time of this analysis. V2 is a coherent diagnostic comparator, +not a causal ablation. Exact hosted model-build and sampling-seed metadata were +unavailable, and host isolation was procedural. + +## What V3 Demonstrated Reliably + +The six modes outside `C` and `X` produced 205/205 V3 atom passes across 30 +reports. Twenty-nine of those reports had no scored defect. This is strong +fixture-specific evidence that the model-plus-skill can perform: + +- symbolic support-domain and multi-release coverage; +- correct separation of incomplete universal proofs from complete existential + UB certificates; +- whole-execution reasoning for postconditions in the presence of UB; +- exact-version and admitted compatibility-premise reasoning; +- current-artifact verdicts separated from abstraction redesign; and +- continued review after finding one unsound surface, including reconstructed + local proofs and literal unsafe-trait contracts. + +V2 also reached the ceiling on those atoms, so this is replication rather than +evidence that V3 caused an improvement. Five reports per cell are an engineering +screen, not a population estimate or release-readiness claim. + +## Failure Analysis + +### C1: predicate relationships need an explicit proof + +All five V3 reports reproduced both nonlinear policy predicates and passed the +conservative-domain atom. Only one explicitly pinned a Scarlet-only case and +an Indigo-only case, so `C1` passed 1/5. + +The code and domain reasoning were not generally lost. The missed proposition +was the asserted relationship between the two predicates. Reproducing both +formulas and correctly normalizing their union does not itself expose a proof +that neither predicate contains the other. For proof-grade reporting, a claim +of incomparability needs a separating witness for each failed containment +direction, just as equality needs both containments. + +There is also an evaluation-alignment issue. The user request asked for the +strongest conclusion without choosing a policy but did not expressly request +separating witnesses. The hidden rubric used “identifies a region” as a strict +reporting requirement. Future tasks should either request the relationship +certificate explicitly or define when a symbolic derivation is sufficient. + +### C3–C5: one omitted proof edge cascaded into several failures + +V3 reports `r046` and `r010` correctly derived the conservative union and +correctly proved the local `unwrap_or` and guarded `unwrap_unchecked` bodies. +They cited the `cfg` attribute's include/remove behavior and `compile_error!`, +but did not state and narrowly cite the applicable Rust semantics of `all` and +`not`. `BUILD-MAP-C` expressly supplied only Cargo feature/target leaf mappings +and no Rust semantics. + +Both reports nevertheless asserted exact body selection, effective rejection, +`Required ⊆ Covered`, and full `PROVED` verdicts. Strict adjudication therefore +failed `C3`–`C5`, applied `G11`, `CH2`, and `CH6`, and marked a TCB/authority +defect. This is one missing semantic bridge per report, not three independent +unsafe-code reasoning defects. + +The current skill already requires every material premise and inference to be +explicit, applicable, and authoritative. Three V3 reports and all five V2 +reports supplied the missing semantics. The result is best classified as a +stochastic adherence failure that exposes insufficient reliability of the +final closure check, not absence of the underlying rule and not evidence that +V3 caused a regression. + +One additional V3 `C` report twice attributed `unwrap_unchecked` to source line +22 when it was on line 20. That factual error was preserved as a novel finding +but did not enter the preregistered defective-report count. + +### X4, X6, and X7: the build pipeline was compressed into a mapping + +Every report recovered the external selector partition, accepted selector to +allocator-cfg mapping, simultaneous target/feature/allocator UB cell, genuine +wasm/arena exclusion, and final source reachability. None of the five V3 +reports proved the complete ordered and fallible build-script relation required +by `X4`, `X6`, and `X7`. + +The source first attempts the rerun directive, then the check-cfg directive, +then reads and classifies the environment input, and finally emits a selected +cfg. Either earlier output write can fail before selector handling. A complete +proof therefore distinguishes at least: + +1. failure of the first write; +2. first-write success followed by failure of the second; +3. both writes succeeding followed by selector rejection; and +4. all prerequisite writes and selector handling succeeding, with exactly the + resulting directives and Cargo effects. + +Reports generally summarized this as “invalid selectors panic; stdout failure +produces no compilation; BUILD-MAP-X supplies rerun/check-cfg/cfg behavior.” +That proves important endpoints but not the staged relation, exact ordering, +or the proposition that an earlier failure preempts later handling. + +This exposes a runtime architecture gap. The configuration reference tells the +agent to audit build scripts and every path producing different output, but it +does not operationalize a build as an ordered, fallible transducer from inputs +through effects and exits to compiler-selected source. The correction should +be that general model, not Cargo- or fixture-specific directive trivia. + +The evaluation also overbundled some requirements. `X4` combined selector +policy rejection with an infrastructure prefix path and produced five scorer +disagreements. `X6` and `X7` made exact directive bookkeeping primary atoms even +though the task did not separately name those theorems. Such details are valid +audit obligations when they affect configuration freshness or reachability, +but future fixtures should make that semantic dependency explicit. + +### X11: a useful regional theorem, but not required to close `UNSOUND` + +Two V3 reports proved the exact positive region: + +```text +(Required \ Q_X) × every u8 + ∪ Q_X × {1..=255}. +``` + +The other three proved every input outside `Q_X` and supplied the zero-input UB +witness inside `Q_X`, but did not separately prove the nonzero inputs there. + +This result reveals a wording inconsistency worth fixing: the core skill defines +`case` across configurations, inputs, states, and executions, while the +configuration reference sometimes speaks only of `Covered(configuration)`. +Coverage must retain every dimension relevant to the claim. + +It does not follow that every audit which closes `UNSOUND` must compute a +maximal positive remainder. One valid existential certificate refutes the +universal soundness claim, while comprehensive review still requires a +disposition for every independent surface and obligation. `X11` demanded an +additional regional theorem that was useful but not explicitly requested. +Future scoring should require maximal or exact regional classification only +when the task asks for it; any regional theorem actually asserted must of +course retain the full case tuple and be proved exactly. + +The V2/V3 comparison for `X11` is additionally unreliable. Both scorers passed +V2 report `F` by claiming it affirmatively proved nonzero inputs in `Q_X`, but +the report only identified zero as the failing case—the same proof shape that +adjudication rejected in comparable reports. Because both scorers made the +same error, the cell never reached adjudication. The reported V2 4/5 therefore +is not calibrated consistently with V3 2/5. + +### K: correct proof, incomplete citation inventory + +V3 report `r016` passed all eight `K` atoms and had no hard error. It correctly +derived false `is_empty` ⇒ `len > 0` ⇒ representable `len - 1 < len`, but +cited only the arithmetic-operator rules while asserting that its listed +authorities were complete. It omitted the available version-matched authority +for the unsigned `usize` domain. + +Adjudication correctly kept the implementation proof and all atoms: the report +had invoked the right proposition, and the permitted authority verified it. +It nevertheless retained the TCB/authority-accounting defect because the +report itself did not cite or inventory that consumed proposition. This is a +narrow provenance failure, not bad unsafe-Rust reasoning. Like the `C` cascade, +it supports a final premise-to-citation reconciliation pass rather than a new +integer-specific rule. + +### V2 R: the recorded scope defect is a scorer false positive + +Both scorers marked V2 report `r011` for prohibited package inspection because +it disclosed the evaluated skill digest. The report prompt expressly required +the agent to read the supplied package, and the V2 report template required the +skill revision. The disclosed digest matched that permitted package. This was +not sibling or condition-map inspection. + +Agreement prevented adjudication, so the aggregate preserves the flag. It +should be treated as an evaluation defect and does not affect the V3 gate. +Future rubrics must define scope flags precisely, state that permitted package +identity may be reported, and independently review every positive global +defect flag even when two scorers agree. + +## Holistic V4 Direction + +The runtime package should not accumulate `cfg(all)`, `println!`, `usize`, or +fixture-specific checklist bullets. It should make the existing proof model +harder to compress incorrectly. + +The coherent revision should have one reusable certificate discipline: + +1. Preserve one full `Case` domain through policy, build/configuration, API + input/state, and execution reasoning. References may project it for local + discussion but must not redefine claim coverage at a coarser granularity. +2. For every claimed relationship or proof edge, state the exact proposition, + applicability, derivation or witness, premise source, and consumer. This may + live in ordinary proof prose or the existing obligation ledger; no explicit + dependency graph or second record schema is required. +3. Prove predicate relationships according to the relation asserted: both + containments for equality, containment plus a separating witness for strict + containment, and a witness in each set difference for incomparability. +4. Model build and generation machinery as a staged relation from inputs, + through ordered and fallible local operations and emitted effects, through + build-tool interpretation, to compiler-selected artifacts and source. Cover + alternative exits and partial progress before consuming later-stage facts. +5. Before any affirmative certificate, reverse-trace every conclusion to + explicit local facts, mathematical steps, authoritative Rust propositions, + tool theorems, or accepted TCB entries. Reconcile every material Rust leaf + with the exact quotation/link and applicability recorded in the report. +6. Preserve the existing quantifier-sensitive verdict rules. `UNSOUND` closes + existentially; it neither excuses auditing other surfaces nor creates an + unnecessary requirement to maximize every positive remainder. + +This is a refinement and consolidation of the obligation/domain workflow, not +a new ontology. Existing duplicated uses of `Covered(configuration)` and broad +“cfg/build mapping” shorthand should be replaced where the full-case and staged +relation make them unnecessary. + +The report template should instantiate the same model with an optional staged +configuration table and a stronger final proof-edge/premise attestation. The +maintainer rationale should record why these requirements are load-bearing and +why no explicit proof graph or fixture taxonomy is imposed. + +## Evaluation Corrections and Next Sequence + +Before the next run: + +- fix adjudication packet identity so read-only hardening cannot conflict with + permission-sensitive target identity checks; +- define global defect flags precisely and adjudicate every positive flag; +- add a cross-report consistency review for atoms with heterogeneous decisions + or other reason to suspect equivalent proof shapes were treated differently; +- split unrelated atom clauses or expressly request the combined theorem; +- require separating witnesses when predicate incomparability is scored; and +- require an exact regional map only when the task asks for one. + +Then: + +1. revise the runtime skill and maintainer rationale coherently and preserve it + as V4; +2. run focused confirmation on predicate relationships, proof-edge authority, + staged build/configuration behavior, and full-case applicability, with + unchanged verdict and redesign controls; +3. if that passes, run the broader fresh-agent release suite; and +4. only after all skill/meta revisions and evaluation rounds are complete, + write the deferred terse process report, split between design/brainstorming + and empirical evaluation/iteration. + +The separately requested audit of zerocopy's uses of `#[doc(hidden)]` also +remains deferred until the skill is final. + +## Evidence Index + +The principal preserved evidence for the conclusions above is: + +- aggregate counts, defects, and failed cells: + [results/aggregate.json](results/aggregate.json) and + [results/summary.md](results/summary.md); +- condition and report identity: + [sealed/condition-map.tsv](sealed/condition-map.tsv), + [sealed/blind-map.tsv](sealed/blind-map.tsv), and + [sealed/launch-schedule.tsv](sealed/launch-schedule.tsv); +- `C` requirements and final decisions: + [freeze/rubrics/C.md](freeze/rubrics/C.md), + [scoring/final/C.json](scoring/final/C.json), and + [scoring/adjudications/C.json](scoring/adjudications/C.json); +- the two defective `C` reports: + [r046](collection/attempts/r046/1/report.md) and + [r010](collection/attempts/r010/1/report.md), compared with the passing V3 + reports [r077](collection/attempts/r077/1/report.md), + [r023](collection/attempts/r023/1/report.md), and + [r062](collection/attempts/r062/1/report.md); +- `X` requirements and final decisions: + [freeze/rubrics/X.md](freeze/rubrics/X.md), + [scoring/final/X.json](scoring/final/X.json), and + [scoring/adjudications/X.json](scoring/adjudications/X.json); +- the V3 `X` reports: + [r066](collection/attempts/r066/1/report.md), + [r018](collection/attempts/r018/1/report.md), + [r015](collection/attempts/r015/1/report.md), + [r034](collection/attempts/r034/2/report.md), and + [r064](collection/attempts/r064/1/report.md); +- the build pipeline being scored: + [build.rs](../../fixtures/v3-targeted/x_cross/build.rs), + [TCB.md](../../fixtures/v3-targeted/x_cross/TCB.md), and + [src/lib.rs](../../fixtures/v3-targeted/x_cross/src/lib.rs); +- the `K` authority-accounting decision: + [r016](collection/attempts/r016/1/report.md), + [scoring/final/K.json](scoring/final/K.json), and + [scoring/adjudications/K.json](scoring/adjudications/K.json); and +- the V2 `R` scope false positive: + [r011](collection/attempts/r011/1/report.md), + [scoring/final/R.json](scoring/final/R.json), the permitted-package wording + in [freeze/prompts/report.md](freeze/prompts/report.md), and the V2 report + template under the frozen package identified by + [sealed/condition-map.tsv](sealed/condition-map.tsv).