Correct the V5 diagnostic oracle after independent review - #3602
Open
joshlf wants to merge 20 commits into
Open
Conversation
Introduce a proof-oriented unsafe Rust authoring and audit skill. Treat safety documentation as an English-language theorem and each SAFETY comment as its proof, with every material premise grounded in exact versioned Rust Reference or standard-library text or recorded conspicuously in the TCB. Require obligation-first review, local invariant composition, adversarial caller reasoning, explicit dependency trust, complete safe-API and configuration surfaces, documented postconditions, and proof-grade audit artifacts. Include the conditional abstraction-design workflow, module-boundary discipline, API-evolution and SemVer analysis, generated-code coverage, TCB and report templates, and a source catalog and evaluation plan. Preserve the paired exploratory smoke test that preceded this V1 snapshot. Ten fresh source-only agents reviewed synthetic vulnerable/fixed code, a historical zerocopy defect/fix pair, and current zerocopy. The treatment retained complete known-defect recall and improved authority, configuration, surface, TCB, and report closure, while the current-code challenge exposed missed version applicability, literal contract clauses, and indirect derivations. The exact predecessor skill archive and several raw pilot artifacts were not retained. Record its digest and results without claiming a byte-exact predecessor-to-V1 diff. The pilot used procedural rather than hardened isolation, one replicate per cell, and cannot establish release readiness. gherrit-pr-id: G6f4nmapfoz5ur4camwh2yhyazexc2lct
Replay the predecessor pilot targets against the frozen V1 package and run a 54-report treatment/core-ablation study over nine abstraction-design modes. Preserve the fixtures, frozen packages, manifests, raw reports, blind scores, adjudications, and limitations needed to interpret both exploratory studies. The legacy replay recovered every known synthetic and historical defect and accepted every fixed control without a hard error. It improved historical version applicability, literal HasField contract discovery, and exposure of reconstructed proofs, while still missing an admissible indirect Copy and UnsafeCell derivation on the current-source challenge. The abstraction-design workflow produced the clearest measured improvement. No treatment report certified an unimplemented proposal, while 16 of 27 core-ablation reports did; treatment matched or exceeded every adjudicated mode and elicited parsimonious designs such as checked construction, real sealing, safe slice splitting, and receiver-bound lifetimes. The preregistered gates nevertheless failed. Four treatment reports used executions containing UB as defined behavioral counterexamples. Two of three treatment reports incorrectly proved a Rust-1.70 empty-slice pointer loop after promoting constructor or slice admission facts into a universal invariant; the third treatment report correctly falsified the evaluator's original oracle. These failures motivate V2's whole-execution verdict, exact-domain, boundary-case, and producer-quantifier rules. The results remain exploratory: isolation was procedural, model identity and sampling seed were unavailable, and the legacy replay was neither byte-identical to the pilot nor a statistical release evaluation. gherrit-pr-id: G3y45zv35fuuyeejc26bftqdd33lqz2oh
Translate the V1 evaluation failures into general proof rules rather than adding fixture-specific hazard trivia. Require CONTRACT-BROKEN to have a valid UB-free falsifying execution. An execution that contains UB may prove UNSOUND, but it cannot establish a defined observation before or after the UB; without a separate UB-free witness, the corresponding behavioral promise remains UNPROVED. Require an explicit supported toolchain and configuration predicate, preserve conflicting controlling policy sources, distinguish a conservative audit domain from the project's unresolved support promise, and reject an earliest version, CI sample, or convenient policy interpretation as proof of the whole domain. Forbid promotion of one constructor, conversion, deserializer, or other producer's precondition into a universal invariant of its output type. Require an authoritative universal premise, enforced construction-and-preservation closure, a verified theorem or explicit TCB premise, or a derivation specific to the values actually consumed. Strengthen literal-clause closure, full supported-domain composition, and boundary and adversarial falsification before PROVED. Update the report template and proof, configuration, API, and reporting references to carry the same rules. gherrit-pr-id: Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz
Run a preregistered 150-report forward evaluation: ten modes, three frozen conditions, and five fresh replicates per cell, with two blind scorers per mode and adjudication before unblinding. V2 versus V1 is the primary comparison; the V1 core ablation is only a historical bridge. V2 passes every whole-execution, exact Rust-1.79/1.80 boundary, producer-quantifier, ticket, configuration, and published-contract atom. It produces no proposal laundering and retains strong reconstructed-proof behavior. The release gate still fails with 16 atom misses and five hard errors. Four of five V2 reports contract an inclusive stable-release interval by omitting Rust 1.80.1, then assert exhaustive closure. Another report assembles every fact needed for a valid empty-slice UB witness but dilutes the conclusion to UNPROVED by continuing to seek a universal positive lemma. Sparse-version interval claims cause two more misses; one omitted alias route exposes an oracle-granularity issue rather than a clear skill defect. The evidence shows that recovering the quantified domain must itself be a proof obligation and that verdicts need explicit logical certificates. It motivates V3's Required/Covered model, domain-transformation obligations, multi-release proof bases, and existential UB certificate. Preserve the failed gate unchanged. Differences between coherent conditions are mixed, modes are heterogeneous, five replicates are an engineering screen, and procedural isolation and unavailable model/seed identity preclude a broad causal or population-level claim. gherrit-pr-id: Gthyz3viupsc7cxzrbqaql6qitqmx2ews
Respond holistically to the concentrated V2 failures. Define Required as the exact cases quantified by a claim and Covered as the cases whose obligations have complete applicable derivations. Preserve ranges, unions, exclusions, and conditional policies symbolically; make every normalization, enumeration, partition, merge, and exclusion a checked proof step; and require Required to be contained in Covered before issuing PROVED. Require every multi-release affirmative claim to use a parametric proof, an exhaustive applicable partition, or an exact proposition-preserving compatibility premise. Endpoints, sparse samples, CI, stability badges, and an audit cutoff do not establish an interval. Replace informal verdict selection with quantifier-sensitive certificates. UNPROVED records an incomplete universal derivation. UNSOUND requires a valid in-scope use, reachability, a false exact safety proposition, and an applicable UB consequence; once all four links close, do not demand a universal positive lemma. CONTRACT-BROKEN continues to require a UB-free falsifying execution. Update audit and TCB templates to retain domain transformations, coverage containment, version bases, and complete verdict certificates. Add the maintainer rationale and traceability document so later changes preserve this proof model without leaking design history into the runtime instructions. gherrit-pr-id: Gcbutfa3xssppp2tjpxo2fjo6kguufo6t
Add an evaluator-only draft for comparing the coherent V3 package with V2 over eight focused modes and five fresh replicates per condition. Exercise symbolic intervals with patch releases, nonlinear conflicting policies, feature/target/allocator cross-products, complete existential UB certificates versus incomplete universal proofs, whole-execution behavioral reasoning, valid multi-release positive proof forms, abstraction-redesign firewalls, and multi-issue regression coverage. Draft strict candidate gates: every V3 atom must pass 5/5, with zero hard errors, proposal laundering, silent TCB or authority defects, semantic noncompletion, and scope or budget defects. Keep the coherent V2 package only as a diagnostic comparator and preserve per-mode results rather than pooling heterogeneous tasks. This commit contains only the candidate package snapshot, fixtures, plan, and evaluator drafts. It records no evaluation result and authorizes no report collection until the protocol and artifacts are independently reviewed and frozen. gherrit-pr-id: Gq7dw6cdl4up4hg4zvgvdkpqs6pdhsb2u
Incorporate independent protocol review while the V3 confirmation remains a draft. Make V3 the absolute candidate under test and V2 a diagnostic comparator rather than allowing a relative improvement to satisfy the release decision. Clarify the atom rubrics, accepted proof forms, verdict certificates, authority requirements, condition-specific prompts, and frozen fixture expectations. Add coverage for exact set relations, symbolic configuration composition, ordered fallible construction, and the distinction between an unsoundness witness and an unnecessarily maximal characterization of every bad input. These are preregistration corrections, not interpretations of observed model behavior. No reports have been collected, no condition identities have been revealed, and the strict all-atoms and zero-hard-error gates remain unchanged. gherrit-pr-id: Gd5c25nyjtgu5tav2bs53xvoz525b6kpe
Freeze a blind 80-report evaluation of V3 against V2: eight modes, two conditions, and five fresh replicates per cell. Seal condition maps, prompts, fixtures, frozen skill packages, rubrics, allowed authority, expected atoms, and report and scoring schemas before generation begins. Retain mode-level analysis for symbolic release domains, nonlinear policy composition, configuration products, existential unsoundness certificates, whole-execution behavioral claims, positive multi-version proofs, abstraction-design firewalls, and regression breadth. Require candidate V3 to pass every required atom in every replicate and produce zero hard errors, TCB or authority defects, proposal laundering, semantic noncompletion, and scope or budget failures. Add an append-only event ledger and explicit attempt lifecycle so generation, validation, retries, blind scoring, adjudication, and unblinding remain auditable. Record the independent package and protocol reviews. At freeze time the report count is zero, so later results cannot have influenced the question or success criteria. gherrit-pr-id: G5k3oylk4nmllritz5hdpiksvqbp24ffs
Generate and preserve all 80 canonical reports under the frozen blind protocol, without inspecting the hidden condition map or changing prompts, fixtures, skill packages, rubrics, or gates. Retain raw attempts and validation records so operational failures are distinguishable from semantic outcomes. Three interrupted orchestration attempts, r033 through r035, are recorded and replaced according to the preregistered retry rules; their existence does not alter the canonical sample or scoring criteria. This phase establishes only that the preregistered corpus was collected. It performs no semantic comparison, blind scoring, adjudication, unblinding, or release conclusion. gherrit-pr-id: Gxgsta5jm3iasu652ow7bfbefe3c2r6nb
Complete independent blind scoring, adjudication, condition unblinding, and the preregistered result for all 80 reports. Preserve score packets, ledgers, adjudications, integrity checks, event history, and the machine-readable result needed to reproduce the decision. V3 earns 272 of 300 required atoms, and every atom reaches 5/5 in S, Q, W, M, R, and K: symbolic release coverage, quantifier-sensitive existential certificates, whole-execution behavior, positive multi-version proofs, abstraction-redesign firewalling, and regression breadth. K nevertheless has one authority-inventory defect, so it does not pass the complete zero-defect gate. In C, C1 reaches 1/5 and C3 through C5 reach 3/5; in X, X4, X6, and X7 reach 0/5 and X11 reaches 2/5. Two C reports contain hard TCB or authority defects. The aggregate identifies a narrower failure class but does not diagnose it: agents often reach a plausible conclusion without a complete, reversible derivation of the quantified case set or construction relation. Because the all-atoms, hard-error, and authority gates fail, V3 is not accepted despite its high pooled atom count and strong performance in other modes. gherrit-pr-id: G3rihw6xuj2lcqvojuxabx73mkjzsgdd5
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
Rework the proof model around lossless representations and locally checkable certificates, following the V3 gate failure and qualitative diagnosis. Require an explicit case domain for each quantified claim and describe how inputs map to obligation fibers. For equality, containment, disjointness, and incomparability claims, require the exact direction-specific certificate and the separating witnesses the relation demands. Treat feature, target, allocator, toolchain, and policy expressions as semantic sets whose operators must be justified before their denotations may be composed. Model ordered and fallible construction as a staged relation rather than an endpoint summary. Require transformations to retain enough information to reverse or independently check the derivation, and reject prose such as by inspection or all cases when the case mapping is not shown. Scope counterexamples to the verdict actually requested: one complete existential unsoundness witness closes UNSOUND, while exhaustive characterization is a separate deliverable. Preserve the V3 strengths: whole-execution UB reasoning, exact supported-domain coverage, producer quantifiers, verdict certificates, reconstructed-proof reporting, module-local invariant discipline, and the conditional abstraction-design workflow. Do not add fixture names or hazard lists to the agent-facing skill. gherrit-pr-id: Gavvgvuiorzpz3yzrmmlq5zb5inu3nazb
Freeze a 50-report blind evaluation of V4 against V3: five focused modes, two conditions, and five fresh replicates per cell. The modes test proof-kernel completeness, Boolean configuration semantics, length and arithmetic reasoning, quantifier-sensitive verdicts, and abstraction redesign. Seal the condition map, prompts, fixtures, frozen skill packages, authority allowlists, atom rubrics, canonical output schema, scoring packets, retry rules, and preregistered gates before collection. Require V4 to pass every required atom in every replicate, with zero hard errors, TCB or authority defects, proposal laundering, semantic noncompletion, scope failures, or budget failures. Treat V3 only as a diagnostic comparator. Retain exact package digests, reviewer records, validation tools, and an append-only event protocol so collection, scoring, and unblinding can be distinguished. No candidate reports exist at freeze time. gherrit-pr-id: Gpt2gxvx72macbs3xnoxkx7o3k5mtekib
Generate and preserve the complete 50-report canonical corpus under the frozen blind protocol. Keep condition identities sealed and leave the packages, prompts, fixtures, rubrics, authority sets, and release gates unchanged. Record 54 total attempts. Four infrastructure failures are retried under the preregistered rules; every canonical report validates and remains within its output cap. Preserve the raw reports, attempt metadata, validator output, and collection integrity records so later scoring can distinguish model behavior from orchestration behavior. This commit closes report collection only. It contains no scoring result, unblinding, semantic interpretation, or revision to the skill. gherrit-pr-id: Gowcssqoviioleh66rgjls4bafqwd4l5n
Complete blind scoring, adjudication, aggregation, condition unblinding, and the official preregistered V4 decision. Preserve the scoring ledger, packets, events, integrity checks, machine-readable summaries, and unblinding artifacts. V4 improves proof-kernel coverage to 135 of 135 atoms from V3's 124 of 135 and Boolean-configuration reasoning to 25 of 75 from 8 of 75. Quantifier-sensitive verdict reasoning remains 25 of 25, abstraction redesign improves to 27 of 35 from 23 of 35, and length and arithmetic reasoning regresses to 40 of 55 from 46 of 55. Across all modes, V4 produces no proposal laundering, scope or budget defect, semantic noncompletion, or confirmed novel finding. The absolute gate still fails. V4 does not pass every required atom, and hard errors plus TCB or authority defects remain. The dominant pattern is not a bad high-level verdict but an incomplete semantic bridge: visible source syntax is treated as if it directly established execution semantics, types, arithmetic, control flow, or caller obligations. The official outcome is therefore failure, irrespective of comparative gains. Detailed root-cause interpretation belongs to the following analysis phase. gherrit-pr-id: G4gcidwygjqjb3gwg5fcikcvz4chrkvix
Trace V4's scored misses to missing semantic premises while preserving the official failed result. The reports commonly identify the right risk and even the right witness, but close the proof with an uncited reading of syntax. In Boolean-configuration reports, a missing premise for implicit return or the end of main fans out into nine uncovered atoms; one official scoring path also accepted an equivalent omission and is recorded as an evaluator false pass. In length reports, agents use field types, usize subtraction, overflow behavior, or the fact that a true branch skips its else branch without authority that entails those exact propositions. In redesign reports, agents produce a sound witness and useful API but omit the premise that an ordinary safe function call imposes no unsafe caller obligation. The recurring defect is a proof kernel with an unstated root, not lack of a longer construct checklist. It motivates V5's distinction between artifact facts and semantic propositions, proposition-level provenance and consumer tracking, implication-direction checks, valid-use certificates, root-blocker fan-out, and mandatory disclosure of proofs reconstructed during review. Also harden later evaluations: score direct decisions separately from dependency fan-out, include metamorphic holdouts that vary syntax while preserving semantics, canonicalize retry and output handling, materialize gates mechanically, and define a finite terminal confirmation sequence rather than an open-ended search for ever more fixtures. gherrit-pr-id: Gquwn2yzvxejg4lkqiqoaaowxzxbmj62x
Revise the runtime skill around the root cause of the V4 failures: agents must not silently promote visible Rust syntax or artifact text into the semantic proposition needed by an unsafe-code proof. Require every load-bearing premise to state its exact proposition, provenance, applicability domain, and downstream consumer. Distinguish directly observed artifact facts from claims about Rust execution, typing, arithmetic, control flow, library behavior, or caller obligations; the latter must follow from applicable authoritative text, an explicit admitted TCB premise, or a checked derivation. Verify that cited text entails the proposition in the direction the proof uses it rather than merely mentioning related concepts. Add a valid-use certificate that identifies why the counterexample or proof case is admitted at each safe API boundary. Track root blockers separately from the atoms that depend on them so one missing semantic bridge cannot be hidden by many repeated conclusions. When an auditor must reconstruct a proof that the code comment does not contain, require the report to expose that reconstructed proof for maintainer review instead of silently accepting the site. Keep the existing exact-domain, set-relation, staged-construction, whole-execution, verdict-certificate, local-invariant, and abstraction-design discipline. Express the new requirements as a compact evidence-bearing proof kernel, not as a list of syntax forms or evaluated fixtures. gherrit-pr-id: Gj24u57i5qq6wbmrnwypu7cy7dupt2mt3
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
Add an explicitly unsealed V5 evaluation design that can be reviewed before any semantic agent sees a fixture. The draft defines eight modes, three conditions, five replicates per cell, 109 theorem atoms, closed defect rules, 31 controls, fixture manifests, authority material, and exact schemas for the planned collection and scoring pipeline. Add seven new fixture trees, reuse the V4 predicate fixture by declaration, and preserve the current V5 runtime skill as a content-addressed frozen package. The package bytes are intentionally exact, including existing Markdown hard line breaks. Add deterministic schedule generation, atom and gate composition, scorer and consistency data structures, attempt leasing/finalization primitives, word counting, projection contracts, and synthetic self-tests. Keep the run conspicuously DRAFT/UNSEALED: twenty-five blocking integration hooks and a constant static-integrity failure prevent the scaffolding from producing a favorable diagnostic result or being mistaken for release evidence. No reports, scores, adjudications, condition maps, seeds, lock, or results are included. This commit preserves the pre-integration design as a reviewable baseline; the next phase must repair and implement the promotion/runtime path before any evaluation launches. gherrit-pr-id: Ghh32fbkyuqkrndyfjzwwarkb4dmfosug
The earlier focused evaluations showed that the next diagnostic suite had to distinguish local premise closure from fan-out, valid-use unsoundness from contract breakage, and claimed authority from authority that actually proves the consumed proposition. Independent review of the V5 draft then found that its semantic materials did not yet meet that standard. Split F into an unavailable evidence root, separate safety and wrapping-result theorems, three dependent consumers, an independent unsound local case, and a checked control. Add authority-reconciliation controls for F and R, a positive Q branch control, and neutralize Q fixture identifiers. Correct Q’s central semantic mistake: Rust 1.83 says constructing a non-UTF-8 str is not immediate UB. The oracle now classifies the safe API as unsound through the authoritative invalid-str invariant escape and downstream-UB consequence, forbids claims of immediate or time-local UB, and requires an exact later witness before claiming a particular UB execution. Add the exact coercion, unsizing, lifetime, and API-signature authority needed by that proof. Make the review surface auditable rather than aspirational. Recompute the live V4 P fixture with historical BYTE_TREE_V1, bind every frozen lineage input, require exact file and named-item inventories, reject unlisted public APIs and exports, enforce strict JSON in all semantic validators, and synchronize propositions, quotations, locators, verification, allowlists, and the agent-visible projection. gherrit-pr-id: Guzo775xby4g7ptvtc325vbwh3zf5wxhv Validation: two independent semantic reviews; 115 atoms; 35 controls with complete coverage; 8 DRAFT fixture manifests; 69 authority entries; 137 Rust-only projected records; all 31 pinned Rust 1.83 pages and 86 quotations revalidated; strict-JSON, surface-mutation, locator-mutation, and live-P-tree negative tests passed. These materials remain DRAFT pending static integration and do not constitute a frozen evaluation.
This was referenced Aug 29, 2026
This was referenced Aug 29, 2026
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Ghh32fbkyuqkrndyfjzwwarkb4dmfosug #3602 +/- ##
==================================================================
Coverage 91.85% 91.85%
==================================================================
Files 20 20
Lines 6093 6093
==================================================================
Hits 5597 5597
Misses 496 496 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 76bccfa577
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| "neutral_label": "fixture-dogwood", | ||
| "source_digest": "INTEGRATION_BOUND_SOURCE_TREE_SHA256", | ||
| "exact_prompt_set_sha256": "INTEGRATION_BOUND_EXACT_PROMPT_SET_SHA256", | ||
| "reused_fixture_binding": { |
There was a problem hiding this comment.
When P.json is validated against schemas/fixture-manifest.schema.json, this new property is rejected because that schema sets top-level additionalProperties to false but neither declares nor conditionally requires reused_fixture_binding. The custom Python validator accepts the field, leaving the manifest and its repository schema contradictory and blocking schema-based static integration; update the fixture schema with the binding's structure and P-only applicability.
Useful? React with 👍 / 👎.
joshlf
force-pushed
the
Ghh32fbkyuqkrndyfjzwwarkb4dmfosug
branch
from
August 29, 2026 11:11
091e9d6 to
953089a
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The earlier focused evaluations showed that the next diagnostic suite had to distinguish local premise closure from fan-out, valid-use unsoundness from contract breakage, and claimed authority from authority that actually proves the consumed proposition. Independent review of the V5 draft then found that its semantic materials did not yet meet that standard.
Split F into an unavailable evidence root, separate safety and wrapping-result theorems, three dependent consumers, an independent unsound local case, and a checked control. Add authority-reconciliation controls for F and R, a positive Q branch control, and neutralize Q fixture identifiers.
Correct Q’s central semantic mistake: Rust 1.83 says constructing a non-UTF-8 str is not immediate UB. The oracle now classifies the safe API as unsound through the authoritative invalid-str invariant escape and downstream-UB consequence, forbids claims of immediate or time-local UB, and requires an exact later witness before claiming a particular UB execution. Add the exact coercion, unsizing, lifetime, and API-signature authority needed by that proof.
Make the review surface auditable rather than aspirational. Recompute the live V4 P fixture with historical BYTE_TREE_V1, bind every frozen lineage input, require exact file and named-item inventories, reject unlisted public APIs and exports, enforce strict JSON in all semantic validators, and synchronize propositions, quotations, locators, verification, allowlists, and the agent-visible projection.
Validation: two independent semantic reviews; 115 atoms; 35 controls with complete coverage; 8 DRAFT fixture manifests; 69 authority entries; 137 Rust-only projected records; all 31 pinned Rust 1.83 pages and 86 quotations revalidated; strict-JSON, surface-mutation, locator-mutation, and live-P-tree negative tests passed. These materials remain DRAFT pending static integration and do not constitute a frozen evaluation.