Draft targeted confirmation for unsafe Rust V3 - #3525
Open
joshlf wants to merge 6 commits into
Open
Conversation
This was referenced Aug 3, 2026
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gcbutfa3xssppp2tjpxo2fjo6kguufo6t #3525 +/- ##
==================================================================
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: 96ab342dfd
ℹ️ 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".
| edition = "2021" | ||
|
|
||
| [dependencies] | ||
| peer-unsafe-dep = "=3.4.5" |
There was a problem hiding this comment.
lib.rs into the quantifier crate
The fixture's only Rust source is the top-level lib.rs, but this manifest neither provides src/lib.rs nor declares [lib] path = "lib.rs". Cargo therefore rejects the supplied manifest with “no targets specified,” so the dependency-resolution and compilation domain required by REQUEST.md and the Q oracle cannot exist as written, invalidating this evaluation mode before it tests the intended quantifier behavior.
Useful? React with 👍 / 👎.
Comment on lines
+44
to
+45
| - **Configuration scope:** every ordinary debug or release profile in | ||
| `V_copy`; no deployment or backend theorem. |
There was a problem hiding this comment.
The configuration scope places ordinary profiles “in V_copy,” but V_copy is defined in SUPPORT.md as a set of Rust releases, not profiles. Because this fixture expressly prohibits widening the TCB and M5/M6 require exact release/profile applicability, an evaluated agent cannot literally derive coverage for every required profile from this entry. State the scope as every release in V_copy crossed with every ordinary debug or release profile.
Useful? React with 👍 / 👎.
Comment on lines
+49
to
+50
| This predicate is symbolic. It is not the four minor `.0` releases, the CI | ||
| matrix, or the Cargo minimum. In particular, `Required_S` contains Rust |
There was a problem hiding this comment.
.0 release count
The closed interval from 1.84.0 through 1.86.0 contains three minor .0 releases—1.84.0, 1.85.0, and 1.86.0—not four. Because this mode explicitly scores lossless release-domain recovery and treats incorrect contraction as a hard error, the erroneous count makes the oracle internally inconsistent and can lead scorers to penalize an otherwise exact report.
Useful? React with 👍 / 👎.
Comment on lines
+420
to
+423
| Exact pages: | ||
|
|
||
| - `https://doc.rust-lang.org/1.85.1/std/num/struct.NonZero.html#method.new_unchecked` | ||
| - `https://doc.rust-lang.org/1.85.1/std/num/struct.NonZero.html#method.new` |
There was a problem hiding this comment.
The X witness requires proving that a supported FIXTURE_ALLOCATOR=arena selection is visible to build.rs, that std::env::var returns that value, and therefore that the script emits the arena cfg. BUILD-MAP-X accepts only execution, rebuild, and forwarding of already-emitted cfgs and expressly excludes which string the script emits, while this authority list contains neither the std::env::var contract nor an environment-inheritance premise. Under the package's own proof rules, X2/X3 therefore cannot close from the frozen authorities; add the exact environment/std authorities or an appropriately scoped accepted premise.
Useful? React with 👍 / 👎.
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
joshlf
force-pushed
the
Gq7dw6cdl4up4hg4zvgvdkpqs6pdhsb2u
branch
from
August 29, 2026 10:42
96ab342 to
5c16b4d
Compare
joshlf
force-pushed
the
Gcbutfa3xssppp2tjpxo2fjo6kguufo6t
branch
4 times, most recently
from
September 2, 2026 20:45
9401243 to
5d3022d
Compare
joshlf
force-pushed
the
Gcbutfa3xssppp2tjpxo2fjo6kguufo6t
branch
5 times, most recently
from
September 3, 2026 01:00
53958dd to
c37eb34
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.
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.
Latest Update: v4 — Compare vs v3
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gq7dw6cdl4up4hg4zvgvdkpqs6pdhsb2u && git checkout -b pr-Gq7dw6cdl4up4hg4zvgvdkpqs6pdhsb2u FETCH_HEADCheckout
git fetch origin refs/heads/Gq7dw6cdl4up4hg4zvgvdkpqs6pdhsb2u && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gq7dw6cdl4up4hg4zvgvdkpqs6pdhsb2u && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.