Bind V5 aggregation to authenticated reviews - #3605
Open
joshlf wants to merge 23 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.
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
Dry-running the executable V5 lifecycle exposed a remaining trust gap: static integration still began with a caller-supplied reviewed semantic overlay, while production had no public evidence-bearing path for authoring the review receipts that supposedly authorized it. The fixture contract also bound a source digest and prompt summary rather than the complete prompt, input-plan, and launch material actually consumed by each mode. Adversarial review found related failures at those boundaries. Exact-quotation matching erased meaningful whitespace and did not confine excerpts to their cited rustdoc fragments. Several anchors and excerpts were stale, and the V4 lineage record overstated a frozen page-byte manifest as review of current V5 propositions. READY evaluator inputs could retain DRAFT schema prose. Review receipts admitted opaque PASS claims, synthetic receipts could be made production-shaped by renaming actors, and reviewer identities could be reused across phases or at runtime. The executable lifecycle also had concrete integrity and availability bugs: report targets and condition packages could be coherently rebound; production leases initially called an undefined helper; persisted peer leases were not universally checked; receipt metadata, validation, copying, and identity extraction reopened mutable paths; finalization could bless a coherently swapped bundle after publication; and the hardened receipt predicate made genuine production finalization reject its own prematurely-writable stage. Add an explicit reviewed-source boundary before snapshot construction. prepare-source-review now derives an immutable candidate from the 38 DRAFT semantic templates, trusted declaration, eight exact target trees, requested values and seeds, and complete trusted reviewer-tool inventory. Two independent oracle reviews and one coherence review operate on disjoint verified private copies. Their contracts bind the concrete procedure and receipt schema, reviewer runtime, exact artifact and coverage sets, theorem inputs, and itemized reviewer-authored work products. Trusted builders validate and no-replace publish canonical read-only receipts, and finalize-reviewed-inputs preserves those exact bytes. Carry the same discipline through snapshot review and execution. Snapshot contracts bind their procedure, schema, tool/runtime identity, acceptance requirements, complete coverage, and work product. Require three distinct source reviewers and eight distinct snapshot reviewers, disjoint across both sets. Permanently exclude all eleven identities from runtime roles, and enforce the canonical actor grammar against every persisted lease during acquisition, sealing, state verification, and aggregate reconstruction. Capture every production receipt once through an O_NOFOLLOW/O_CLOEXEC/O_NONBLOCK descriptor, verify canonical 0444 regular-file bytes and stable inode metadata, and use only that capture for validation, copying, hashes, and reviewer identity. Parse the lock-authenticated framed manifest strictly and bind source receipt captures to their exact path, kind, size, mode, and SHA-256 records. Return the lock and reviewer exclusion set from one coherent verification operation so protocol callers never reopen receipts. Derive and recheck the external commitment from the verified private finalization stage before no-replace publication. Verify the published path, require it to reproduce that exact identity, and only then publish the separately custodied commitment. Verify a copied review candidate while its receipts remain read-only before opening the private stage for finalization. Make fixture identity exact across lifecycle phases. Replace ambiguous source and prompt fields with BYTE_TREE_V1 source bindings and a V5_MODE_REPORT_MATERIAL_SET_V1 digest over all fifteen prompt, input-plan, and launch records per mode. Leave the report-material binding explicitly unresolved during source review, derive it after snapshot construction, and byte-check the DRAFT-to-candidate-to-READY transitions. Deterministically promote schema lifecycle comments and reject stale DRAFT or UNSEALED prose in evaluator-mounted schemas. Correct the authority oracle at the same boundary. Scope quotation checks to real rustdoc fragments and single semantic elements while preserving word boundaries and punctuation. Repair function, block, match, call, array, method-call, textual, enum-variant, invalid-value, and associated-constant anchors; correct the get_unchecked, unwrap_unchecked, and NonZero excerpts; and add missing cfg-option, cfg-removal, and equality premises. Narrow reused V4 provenance to page bytes bound by its frozen manifest rather than claiming that V4 reviewed current V5 content. Bind 130 locator records and 146 URL edges with the exact-quotation evidence digest, and regenerate the 142-record neutral projection and per-mode allowlists. Expand regression coverage for quotation and lineage drift, forged fixture and report-material bindings, stale schema markers, incomplete work products, missing evidence and receipts, special receipt entries, synthetic-to-production promotion, duplicate or overlapping reviewers, pathname/inode substitution, late identity rereads, poisoned runtime leases, and coherent post-publication bundle replacement. Exercise a complete mechanically production-shaped 3+8 review, finalization, external commitment, and verification lifecycle. This proves the public mechanics are live; it does not claim that human reviewers honestly performed the generated test reviews. Validation passes for preparation, integration, and protocol DRAFT checks and self-tests; the full mechanical production and synthetic lifecycles; all four semantic validators; 115 atoms and 35 controls with complete coverage; eight fixture manifests; 69 authority entries; 83 strict JSON files; 52 schema declarations; all CLI help surfaces; AST and unresolved-global checks; and cache/diff cleanliness. Independent authority review verified 130 locator records and 146 URL edges over 58 pinned official pages. A final independent adversarial replay found no remaining issue at any severity. This remains diagnostic infrastructure. No genuine independent production review receipts, semantic reports, scores, or evaluation result are recorded here. G-ISOLATION and G-OUTPUT-FINALIZATION remain fixed FAIL and release eligibility remains false. Reviewer authentication and honesty, private-copy custody, trusted Python and filesystem semantics, external-commitment custody, and SHA-256 collision resistance remain explicit TCB premises. Review basis: HEAD eeb84a8d58158678c1c5c6a57713fe38321938f4; integrate.py 8a6e267b3b92fae1bbc7b87c57e549fa34ad81910340b744d5b4a99b69479ab3; protocol.py 0daab7a161e11aa0f7d18f0865f7e5ffbfd1a0acd645f73aaa799a33da8ab4c0; 34-file fingerprint 87a1158ad80d1d9458cb9b9e06777806efe97128e7ddfb1c8caf7151a64bb351. gherrit-pr-id: Gwmskgf6pp5ufbufusyjegs357wjllvtq
The first genuine production snapshot-review pass invalidated the V5 candidate before any report or evaluator was exposed. H-VALIDATE-AGGREGATION-RULE-INVENTORY found that integration promoted root-inventory and gate-manifest versions to the READY literal while protocol validators still required the DRAFT literal, and that aggregate derivation consumed nonexistent legacy freeze/reviews summaries rather than the authenticated source-review receipts. H-BUILD-VALIDATE-REPORT-AUTHORITY-PROJECTIONS separately found that the verification ledger omitted TCB_BOUNDARY even though the Rust-only packet correctly excluded those propositions. Make DRAFT and READY gate/root status-version pairs exact in code and schemas. Retain the descriptor-captured three source and eight snapshot review receipts in one canonical authenticated-evidence result, carry the exact eleven reviewer exclusions with it, and consume those records directly for oracle/coherence decisions, digests, and materiality scope without reopening receipt paths. Remove the legacy review-summary dependency and the duplicate static-verifier call. Bump the changed aggregate/rules semantics to v2. Derive the authority excluded-kind inventory from every current non-RUST proposition, require the verification ledger to equal it exactly, reject duplicate proposition IDs and ledger drift, and add missing/stale/duplicate/novel-kind mutations. Document the same-capture evidence boundary. gherrit-pr-id: Ge64gipf6sorrrdfcfdn53nwmf5wjhtsu Validation: prepare/integrate/protocol draft checks and self-tests; the full mechanical production plus synthetic integration lifecycle; all four semantic validators; strict parsing of 83 JSON files; AST/duplicate-literal checks over eight Python files; all 48 CLI help surfaces; schema/instance review; and three independent read-only cross-reviews. A subsequent adversarial review of this checkpoint identified runtime-construction and candidate-path race work for the next iteration.
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 @@
## Gwmskgf6pp5ufbufusyjegs357wjllvtq #3605 +/- ##
====================================================================
Coverage ? 91.85%
====================================================================
Files ? 20
Lines ? 6093
Branches ? 0
====================================================================
Hits ? 5597
Misses ? 496
Partials ? 0 ☔ 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: 81f0cdbe1f
ℹ️ 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".
Comment on lines
+4387
to
+4389
| rederived = _derive_aggregate_context_from_verified( | ||
| root, static_lock, reviewer_ids, review_evidence | ||
| ) |
There was a problem hiding this comment.
When the candidate directory's parent is writable or otherwise attacker-replaceable, it can be renamed and replaced after load_verified_static_bundle_with_review_evidence() returns. This call then reopens root by pathname throughout _derive_aggregate_context_from_verified, while the returned static_lock is unused and the retained review evidence is not rebound to those newly read files, so a replacement tree can supply its own static contracts, runtime aggregate, and lock while inheriting PASS review evidence from the authenticated tree. The previous derive_aggregate_context(root, external_commitment_path) call performed another external-commitment-backed static verification here; either retain a stable directory handle/capture for subsequent reads or reverify the pathname before using it.
Useful? React with 👍 / 👎.
joshlf
force-pushed
the
Gwmskgf6pp5ufbufusyjegs357wjllvtq
branch
from
August 29, 2026 11:11
b1e88b3 to
c3d2551
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 first genuine production snapshot-review pass invalidated the V5 candidate before any report or evaluator was exposed. H-VALIDATE-AGGREGATION-RULE-INVENTORY found that integration promoted root-inventory and gate-manifest versions to the READY literal while protocol validators still required the DRAFT literal, and that aggregate derivation consumed nonexistent legacy freeze/reviews summaries rather than the authenticated source-review receipts. H-BUILD-VALIDATE-REPORT-AUTHORITY-PROJECTIONS separately found that the verification ledger omitted TCB_BOUNDARY even though the Rust-only packet correctly excluded those propositions.
Make DRAFT and READY gate/root status-version pairs exact in code and schemas. Retain the descriptor-captured three source and eight snapshot review receipts in one canonical authenticated-evidence result, carry the exact eleven reviewer exclusions with it, and consume those records directly for oracle/coherence decisions, digests, and materiality scope without reopening receipt paths. Remove the legacy review-summary dependency and the duplicate static-verifier call. Bump the changed aggregate/rules semantics to v2.
Derive the authority excluded-kind inventory from every current non-RUST proposition, require the verification ledger to equal it exactly, reject duplicate proposition IDs and ledger drift, and add missing/stale/duplicate/novel-kind mutations. Document the same-capture evidence boundary.
Validation: prepare/integrate/protocol draft checks and self-tests; the full mechanical production plus synthetic integration lifecycle; all four semantic validators; strict parsing of 83 JSON files; AST/duplicate-literal checks over eight Python files; all 48 CLI help surfaces; schema/instance review; and three independent read-only cross-reviews. A subsequent adversarial review of this checkpoint identified runtime-construction and candidate-path race work for the next iteration.