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