Harden V5 staged runtime and recovery - #3607
Open
joshlf wants to merge 21 commits into
Open
Conversation
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. |
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
Freeze the V1 skill package and replay the synthetic, historical, and current-source targets from the exploratory predecessor pilot. Preserve the manifests, raw reports, scores, and limitations needed to compare the replay with the earlier procedural run. The replay recovers every known synthetic and historical defect and accepts every fixed control. It improves version applicability, literal contract discovery, and exposure of reconstructed proofs, while still missing an admissible indirect Copy and UnsafeCell derivation on the current-source challenge. Treat this as legacy confirmation rather than release evidence: the replay is not byte-identical to the pilot, uses one replicate per target, and retains the pilot's procedural-isolation and unavailable model-identity limitations. gherrit-pr-id: Gup6qexxvahgx6uken5vngpapqsaio22h
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 reproduce the comparison. No treatment report certifies an unimplemented proposal, while 16 of 27 core-ablation reports do. Treatment matches or exceeds every adjudicated mode and produces parsimonious designs such as checked construction, real sealing, safe slice splitting, and receiver-bound lifetimes. The preregistered gates nevertheless fail. Four treatment reports use executions containing UB as behavioral counterexamples, and two incorrectly prove a Rust-1.70 empty-slice pointer loop by promoting producer facts into a universal invariant. These failures motivate V2's whole-execution verdict, exact-domain, boundary-case, and producer-quantifier rules. The study remains exploratory: isolation is procedural, model identity and sampling seed are unavailable, modes are heterogeneous, and one replicate per cell cannot establish release readiness. 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
Freeze a blind 80-report evaluation of V3 against V2 after independent review and preregistration refinement: 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. Exercise 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 V3 to pass every required atom in every replicate with zero hard errors, 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. At freeze time the report count is zero, so later results cannot have influenced the protocol 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 DRAFT/UNSEALED eight-mode, three-condition, five-replicate-per-cell diagnostic design. After independent review, correct and validate the 115-atom, 35-control oracle, including F's unavailable-root and fan-out separation and Q's invalid-str invariant escape and later-UB semantics. Bind exact fixture surfaces, frozen skill packages, V4 lineage, authority propositions and quotations, deterministic schedules, schemas, projection contracts, and strict-JSON semantic validators. Preserve synthetic self-tests for schedule generation, atom and gate composition, attempt lifecycles, projection, scoring, consistency, and aggregation data structures. Keep the design conspicuously non-executable as release evidence: blocking integration hooks and a static-integrity failure prevent promotion, and no reports, scores, adjudications, condition maps, seeds, lock, or result are recorded. gherrit-pr-id: Ghh32fbkyuqkrndyfjzwwarkb4dmfosug
The first V5 draft described the intended diagnostic study but could not safely execute it. Review found that READY promotion was impossible, several CLI routes had stale arities, padded report IDs disagreed with their validators, host-specific paths destroyed prompt equality, evaluator packets named only digests rather than readable evidence, materiality had no runnable lifecycle, and DRAFT/READY schemas and runtime-state rules contradicted one another. Replace that draft boundary with an authenticated prepare-snapshot, private-review, and finalize lifecycle. The production lock now binds the trusted source declaration, both skill packages, every target, the harness programs, the staged word counter, 120 report prompts/plans/launches, 43 evaluator assignments, hook-specific review contracts and receipts, empty pre-lock runtime state, and a separately custodied external commitment. Synthetic paths carry an authenticated test-only kind and cannot mint production artifacts. Adversarial review exposed further trust failures: executing an unverified candidate verifier, source-copy TOCTOU, ambiguous line-oriented manifests, arbitrary review claims and evaluator launches, stale receipts, unreviewed runtime state, irrelevant schema leakage, optional or crash-unsafe external commitments, and a coherent attack that rebound an F report to target E and a V5 condition to the V4 package. Use injective framed commitments, trusted in-process regeneration, exact artifact/check/evidence inventories, private review copies, atomic no-replace publication, explicit custody-bound recovery, and exact target/condition/package joins to close those failures. Preserve each attack as a negative self-test. Complete the execution protocol around those locked inputs: readable content-addressed packets, two independent consistency reviews, conditional adjudication, materiality review and ledger reconstruction, exact projection and control joins, deterministic aggregate rebuilding, production state authentication, canonical path checks, leases and seals with crash recovery, and fail-closed bound gate evaluation. Unbound caller data cannot make D-STATIC pass. Validation covers prepare, integration, protocol, and draft-verification self-tests; hostile temporary paths; all CLI help surfaces; all JSON parsing and schemas; adversarial provenance, packet, lease, gate, commitment, and assignment mutations; whitespace; and cache hygiene. This remains diagnostic infrastructure: G-ISOLATION and G-OUTPUT-FINALIZATION deliberately remain FAIL, so the commit cannot support a release or terminal-VN claim. gherrit-pr-id: Ghchu3g3fkri2ofhgm5addjto4rfkyvyi
Replace the caller-supplied semantic overlay with an immutable lifecycle of three source reviews and eight snapshot reviews. Require disjoint reviewer identities and bind exact source trees, report materials, authority evidence, work products, receipts, captures, external commitment, and static lock. Carry the same descriptor-captured evidence through aggregation instead of reopening paths or consuming legacy summaries. Correct DRAFT/READY status versions and excluded authority kinds, derive aggregate and gate inputs from the authenticated receipt inventory, and execute only captured trusted word-count bytes. Close receipt, candidate-path, word-counter, and lock-reopen races with no-follow captures, stable inode checks, immutable publication, and exact commitment joins. Document uninterrupted private custody as a TCB premise and exercise the complete mechanical 3+8 review lifecycle plus adversarial replacement, identity, provenance, and aggregation mutations. This remains diagnostic infrastructure. It records no genuine semantic reports or evaluation result, and reviewer honesty, custody, trusted runtime semantics, and collision resistance remain explicit premises. gherrit-pr-id: Gwmskgf6pp5ufbufusyjegs357wjllvtq
Replace the monolithic mutable runtime with a coordinator-claimed six-stage immutable aggregation prefix. Derive each evaluator frontier and input packet only from the committed predecessor stage, bind every manifest to the static lock, coordinator, predecessor, and cumulative envelopes, and rederive the chain during bound-gate evaluation. Make attempt sealing bounded and crash-recoverable with exact external workspaces, seal-time input verification, injective pathname capture, hard payload, entry, and path budgets, immutable terminal claims, and no-replace object and pointer publication. Publish authenticated terminal ERROR records when a phase cannot safely derive its successor while allowing usable report-format failures to reach their frozen gate consequence. Update schemas, policies, integration contracts, and adversarial self-tests for the 154-to-163-attempt, six-stage production lifecycle. gherrit-pr-id: Gfkyot5qmode4aiscnrbgzyffxebq4z56
joshlf
force-pushed
the
Gfkyot5qmode4aiscnrbgzyffxebq4z56
branch
from
August 29, 2026 11:11
2964a8d to
38e88de
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
1 participant
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.
No description provided.