From df5c1ef21f398f13e28bcda6a268c51b4acc4a0f Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Sat, 1 Aug 2026 00:12:56 +0000 Subject: [PATCH] Revise unsafe Rust skill to V2 after V1 evaluation failures 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 --- skills/unsafe-rust/SKILL.md | 54 ++++++++++++++----- .../unsafe-code-audit-report-template.md | 6 ++- .../api-boundaries-and-evolution.md | 9 ++-- .../unsafe-rust/references/audit-reporting.md | 21 ++++++-- .../configurations-and-generated-code.md | 48 ++++++++++++++--- .../references/proof-obligations.md | 45 ++++++++++++++-- 6 files changed, 149 insertions(+), 34 deletions(-) diff --git a/skills/unsafe-rust/SKILL.md b/skills/unsafe-rust/SKILL.md index 543a42bc7f..370782667b 100644 --- a/skills/unsafe-rust/SKILL.md +++ b/skills/unsafe-rust/SKILL.md @@ -48,6 +48,14 @@ deployment separately with their additional premises. - Attach an applicability domain to every claim and premise, whether stated locally or inherited from an identified project policy or canonical entry. A derivation proves only the cases covered by all premises it consumes. +- Define or inherit a precise supported toolchain/configuration predicate + before consuming versioned premises or issuing a full verdict. If applicable + project sources conflict or materially underdetermine that predicate, obtain + an authorized resolution, prove an explicit conservative superset covering + every materially supported candidate predicate identified from those + sources, or leave the affected full-scope claim `UNPROVED`. Do not silently + select an MSRV, current toolchain, or convenient interpretation, and do not + assume that one earliest version represents the whole predicate. - Apply a guarantee documented for an older Rust release to a later stable release only when an exact applicable Rust backwards-compatibility commitment preserves that exact proposition throughout the later release's @@ -92,6 +100,13 @@ documentation gap and suggest an upstream improvement when appropriate. entails the exact needed precondition. - Trace dataflow across calls and time rather than limiting review to lexical unsafe blocks. Account for every producer, transition, and consumer. +- Do not promote a producer's preconditions into a universal invariant of its + output type. Any type- or abstraction-wide conclusion needs a complete + derivation independent of that invalid reversal—for example, applicable + authoritative premises, construction-and-preservation closure under an + enforced boundary, or an admissible explicit TCB premise. Local checks and + other applicable derivations may instead prove the proposition for the + particular consumed values or quantified subset. - For new code, place invariant-bearing representation in the smallest practical leaf module, keep safely accessible representation fields private to it, and treat safe code outside that module—including the rest of the same @@ -100,9 +115,10 @@ documentation gap and suggest an upstream improvement when appropriate. ## Follow the Proof Workflow 1. **Frame the claim.** Record the artifact identity, exact scope, valid uses or - executions, Rust and dependency versions, supported configuration set, - mandatory postconditions, TCB, exclusions, and whether design alternatives - are requested. + executions, Rust and dependency versions, the supported + toolchain/configuration predicate and its controlling sources, mandatory + postconditions, TCB, exclusions, unresolved support-policy conflicts, and + whether design alternatives are requested. 2. **Inventory the surface.** Enumerate every in-scope safe and unsafe API surface, obligation site, invariant producer/transition/consumer, and generated or expanded artifact across the supported set. @@ -113,11 +129,14 @@ documentation gap and suggest an upstream improvement when appropriate. explicit TCB entries. Unfold definitions and seek indirect multi-premise derivations; absence of one direct sentence is not itself a documentation gap. Justify every intermediate inference. -5. **Close composition.** Ensure every literal contract clause and safe surface - has a disposition, every premise consumed by unsafe code has an admissible - source, and every supported configuration region is proved by an abstract - argument or exhaustive partition. Try to falsify the contract reading, - inference chain, and coverage before concluding `PROVED`. +5. **Close composition.** Over the entire supported toolchain/configuration + predicate—by one parametric proof or an exhaustive partition as + appropriate—give every literal clause of each applicable controlling + contract and every safe surface a disposition. Ensure every consumed + premise has an admissible source. Try to falsify the contract reading, each + derivation, and coverage, including boundary and adversarial cases derived + from the clauses themselves rather than from any supposedly exhaustive + hazard list, before concluding `PROVED`. 6. **Report exactly.** Keep unresolved obligations visible and state the smallest missing implication. Record proofs, TCB, coverage, findings, postcondition failures, documentation gaps, and residual scope without @@ -164,8 +183,9 @@ requires an unenforced implementer behavior. Read [configurations-and-generated-code.md](references/configurations-and-generated-code.md) -for every full audit and whenever conditional compilation, targets, generated -code, FFI, assembly, SIMD, allocators, linking, or build tooling is relevant. +for every full audit and whenever supported-toolchain policy, conditional +compilation, targets, generated code, FFI, assembly, SIMD, allocators, linking, +or build tooling is relevant. Every supported combination of compilation options that can ship downstream must be sound. Use parametric proofs or exhaustive partitions when literal enumeration would explode; do not substitute a tested sample. @@ -204,8 +224,18 @@ persistent or full audit. circular, or unverifiable. - **UNSOUND:** A valid use or in-scope execution is proved to reach undefined behavior. -- **CONTRACT-BROKEN:** A documented postcondition is proved false even though - undefined behavior need not occur. +- **CONTRACT-BROKEN:** It is proved that there exists a valid in-scope + execution which, considered as a whole, contains no undefined behavior and + falsifies a documented postcondition. + +Classify a witness using the execution as a whole, not observations from a +prefix of an execution that later reaches undefined behavior. An +undefined-behavior-containing execution can witness `UNSOUND` but cannot +establish the existential claim required for `CONTRACT-BROKEN`. If it is the +only behavioral evidence, report soundness as `UNSOUND` and the postcondition +as `UNPROVED`. An independent UB-free witness or equivalent existence proof +may establish `CONTRACT-BROKEN`; separate proofs may therefore establish both +verdicts. Apply verdicts separately to soundness, documented postconditions, and conditional application claims. State exact scope, applicability, and TCB diff --git a/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md b/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md index 29e2b10723..387ce2f7a6 100644 --- a/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md +++ b/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md @@ -17,6 +17,8 @@ do not present it as unconditional Rust soundness>` - **Scope:** `` - **Supported configuration predicate:** `` +- **Support-policy sources/conflicts:** `` - **TCB log:** `` - **Skill revision:** `` - **Qualification:** `` none>` - **Defect:** `` - **Authority/TCB involved:** `` -- **Counterexample:** `` +- **Defined postcondition refutation:** `` - **Affected producers/consumers:** `` - **Required resolution:** ` PROVED for `` under ``, relative to TCB @@ -109,7 +117,8 @@ Each finding should contain: derivation; - smallest missing, false, circular, or unsupported implication; - authoritative contract or TCB entry involved; -- whether a valid UB counterexample or postcondition counterexample is known; +- whether a valid UB witness or a separate UB-free postcondition refutation or + equivalent existence proof is known; - affected callers, producers, consumers, generated output, and configurations; - minimal acceptable resolution; - compatibility and re-audit consequences. @@ -156,8 +165,10 @@ A complete audit report contains: 5. **Obligation coverage:** Proof sites and status summary; link to detailed proofs/findings rather than duplicating them. Include material reconstructed proofs missing from the reviewed proof artifacts. -6. **Configuration closure:** Supported-set definition, axes, abstract or - enumerative coverage proof, generated artifacts, and enforced exclusions. +6. **Configuration closure:** Supported-set definition, controlling policy + sources and conflicts, audit cutoff, authorized resolution or conservative + superset, axes, abstract or enumerative coverage proof, generated artifacts, + and enforced exclusions. 7. **TCB audit log:** Every authoritative or admitted proposition and reviewer disposition. 8. **Tool-derived evidence:** Exact theorem, artifact/model scope, bounds, diff --git a/skills/unsafe-rust/references/configurations-and-generated-code.md b/skills/unsafe-rust/references/configurations-and-generated-code.md index aad7a9a89a..f436c53db5 100644 --- a/skills/unsafe-rust/references/configurations-and-generated-code.md +++ b/skills/unsafe-rust/references/configurations-and-generated-code.md @@ -14,20 +14,52 @@ ## Define the Supported Set Write a precise predicate `Supported(configuration)` before claiming full -soundness. Derive it from published package metadata, documentation, target -policy, feature declarations, build tooling, compiler support, downstream -integration agreements, and the artifacts that can actually be shipped. - -Include every compilation option combination that downstream users are allowed -to produce, not merely CI jobs or maintainer-preferred builds. If a compilable -combination is exposed without a clear exclusion, conservatively treat it as -supported until the project owner establishes otherwise. +soundness. Fix the exact source or packaged artifact and audit cutoff. Let the +predicate range over every relevant toolchain component, host/target fact, and +build option rather than reducing it to a `rustc` version string. + +Classify support evidence before using it: + +- applicable package metadata, published policy, release documentation, + feature/target policy, and authorized downstream agreements may define the + project's support contract; +- manifest checks, build scripts, `compile_error!`, wrappers, packaging rules, + and distribution controls may admit or enforce configurations; and +- CI jobs, lockfiles, successful builds, `rust-toolchain.toml`, and maintainer + defaults observe or select particular configurations but do not by themselves + define or prove downstream support. + +Resolve inherited fields in the exact workspace and inspect the effective +packaged metadata when it can differ. Interpret every mechanism through its +applicable contract; do not hard-code a universal precedence among metadata, +documentation, and agreements. A documented exclusion may delimit a support +promise, but if soundness depends on preventing that configuration from +shipping, require effective rejection before claiming closure. + +If applicable support declarations conflict or materially underdetermine the +predicate, do not silently select the narrowest interpretation. Obtain an +authorized project decision, prove an explicit conservative superset covering +every materially supported candidate predicate identified from the controlling +sources, or report regional results and leave the full claim `UNPROVED`. Do not +call that conservative audit domain a newly inferred project promise. If a +shippable configuration is exposed and no applicable contract clearly excludes +it, include it in the unresolved conservative candidate domain until project +authority resolves its status; successful compilation alone still does not +define the support promise. + +Preserve conditional and nonlinear structure across every discovered axis +rather than collapsing the predicate to a single MSRV. It may be finite, +nonlinear, or moving and need not have a globally earliest toolchain. Resolve +dynamic policies at the audit cutoff; cover later members only through an +applicable parametric theorem or re-audit trigger. Record: - source revision and workspace/package selection; - Rust toolchain range, edition, standard-library identity, and relevant compiler flags; +- controlling support-policy sources, conflicts, authorized resolutions, and + the audit cutoff; - target triples, target specifications, CPUs, features, ABIs, data layouts, and linkers; - Cargo features, dependency feature unification, optional dependencies, and diff --git a/skills/unsafe-rust/references/proof-obligations.md b/skills/unsafe-rust/references/proof-obligations.md index 017aeb6320..8880ec3ca9 100644 --- a/skills/unsafe-rust/references/proof-obligations.md +++ b/skills/unsafe-rust/references/proof-obligations.md @@ -52,7 +52,9 @@ execution exhibits undefined behavior, make no claim that observations elsewhere—or notionally “before” that event—remain guaranteed. An unexecuted bad path does not by itself make a different execution undefined, but soundness of a safe API still quantifies over every valid use and execution, so one reachable -valid counterexample refutes it. +valid counterexample refutes it. Such a UB-containing execution cannot also +establish a defined behavioral observation; apply the exact witness rule in +`SKILL.md`. ## Qualify Applicability @@ -76,6 +78,10 @@ exactly identified project support policy, invariant definition, axiom entry, or TCB entry. The local proof must still make the inheritance and relevant case clear enough to review. +Derive the required predicate under +[Define the supported set](configurations-and-generated-code.md#define-the-supported-set), +then carry it through every premise and case lemma below. + A documented Rust guarantee from version `R` may support a later stable version only when an exact Rust backwards-compatibility commitment preserves that exact semantic proposition throughout the later version's relevant edition, target, @@ -125,6 +131,33 @@ these classes, the proof is incomplete. Distinguish the validity of a value of type `T` from a stronger library invariant attached to its role in an abstraction. Prove both when needed. + +Never promote one producer's admission contract into an invariant of its output +type. A constructor, conversion, deserializer, FFI ingress, mutation, or other +producer precondition applies at that invocation. It supports a fact about that +particular result only through a proved postcondition or dataflow relation; it +does not prove that every valid value came through that producer or that later +transitions preserve the property. + +To rely on `I` as an invariant of every value in a stated set, provide a +complete derivation over that set without reversing the producer implication. +Such a derivation may, for example, use: + +1. applicable authoritative premises that entail `I` for every value in the + set; +2. an enforced abstraction boundary plus a complete proof that every in-scope + ingress and producer establishes `I` and every transition preserves it; +3. another applicable derivation, including a verified tool theorem, that + entails the exact quantified proposition; or +4. the exact universal proposition as an admissible accepted TCB premise under + the TCB rules. + +This enumeration does not replace the entailment requirement or exclude other +valid proof forms. A consumer may instead establish `I` for its particular +values or quantified subset from local checks, proved producer and transition +history, and other applicable premises. If neither derivation closes, leave +the consuming obligation `UNPROVED`. + Likewise, distinguish: - permission to perform an operation; @@ -331,8 +364,9 @@ For each proof: 1. Reconstruct the required preconditions from the callee or language/library contract rather than trusting the comment's summary. 2. Open every citation and verify its exact proposition, version, and scope. -3. Check each claimed local fact against the actual dataflow and all alternative - paths. +3. Check each claimed local fact—including its quantifier, producer/transition + history, and applicability domain—against the actual dataflow and all + alternative paths. 4. Expand every named invariant and ensure it is established initially and preserved by every permitted transition. 5. Check quantifiers, arithmetic boundaries, zero-sized and empty cases, @@ -358,8 +392,9 @@ proof artifact: - If the reconstruction succeeds, the implementation obligation may be proved, but report the inadequate comment and provide proposed replacement wording. - If the reconstruction fails, leave the obligation unproved. -- If it yields a valid UB or postcondition counterexample, report `UNSOUND` or - `CONTRACT-BROKEN` as applicable. +- If it yields a valid execution containing UB, report `UNSOUND`. If it proves + that a valid UB-free execution falsifies a postcondition, report + `CONTRACT-BROKEN`. Do not use the UB-containing execution itself for both. When changes are authorized, update the adjacent proof rather than leaving the reconstructed reasoning only in the review. A canonical checked proof or named