Revise unsafe Rust skill around domain and verdict certificates - #3524
Revise unsafe Rust skill around domain and verdict certificates#3524joshlf wants to merge 1 commit into
Conversation
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
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gthyz3viupsc7cxzrbqaql6qitqmx2ews #3524 +/- ##
==================================================================
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: 36cbde8c27
ℹ️ 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".
| identify the exact `Required` domain, union valid case lemmas within each | ||
| obligation, intersect coverage across all claim-required obligations, and prove | ||
| `Required ⊆ Covered` for that aggregate predicate. For `UNSOUND`, record every |
There was a problem hiding this comment.
When obligations apply to mutually exclusive cases—for example, one obligation under cfg(feature = "fast") and another under its negation—unioning each obligation's proved regions and then intersecting them yields an empty Covered domain even though every required case is proved. Each per-obligation predicate must first include cases where that obligation is inapplicable (equivalently, applicable => proved) before the intersection; otherwise valid configuration-partitioned audits are incorrectly reported as UNPROVED.
Useful? React with 👍 / 👎.
2 participants
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.
Latest Update: v2 — Compare vs v1
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gcbutfa3xssppp2tjpxo2fjo6kguufo6t && git checkout -b pr-Gcbutfa3xssppp2tjpxo2fjo6kguufo6t FETCH_HEADCheckout
git fetch origin refs/heads/Gcbutfa3xssppp2tjpxo2fjo6kguufo6t && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gcbutfa3xssppp2tjpxo2fjo6kguufo6t && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.