From 36cbde8c27b64a895caebb6b35364058fb8e609f Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Sat, 1 Aug 2026 00:13:31 +0000 Subject: [PATCH] Revise unsafe Rust skill around domain and verdict certificates 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 --- maintainers/unsafe-rust-skill-design.md | 557 ++++++++++++++++++ skills/unsafe-rust/SKILL.md | 120 ++-- .../assets/tcb-audit-log-template.md | 10 +- .../unsafe-code-audit-report-template.md | 65 +- .../api-boundaries-and-evolution.md | 9 +- .../unsafe-rust/references/audit-reporting.md | 39 +- .../configurations-and-generated-code.md | 101 +++- .../references/proof-obligations.md | 54 +- .../references/tcb-and-evidence.md | 5 +- 9 files changed, 821 insertions(+), 139 deletions(-) create mode 100644 maintainers/unsafe-rust-skill-design.md diff --git a/maintainers/unsafe-rust-skill-design.md b/maintainers/unsafe-rust-skill-design.md new file mode 100644 index 0000000000..1ee88fb0a8 --- /dev/null +++ b/maintainers/unsafe-rust-skill-design.md @@ -0,0 +1,557 @@ +# Design of the Unsafe Rust Authoring and Audit Skill + +> **Status and audience** +> +> This document governs maintenance of the `unsafe-rust` skill. It is not part +> of the installable skill package, is not loaded during ordinary skill use, and +> must never serve as a premise in an unsafe-code proof. Human maintainers—and +> agents specifically tasked with maintaining the skill—should read it before +> changing agent-facing instructions. +> +> The installed skill revision governs an agent's operational procedure. Exact +> Rust Reference and standard-library documentation, together with explicit TCB +> entries, govern proof premises. This document governs how maintainers evolve +> that procedure. A conflict between this document and the installed skill is a +> maintenance defect, not a hidden runtime instruction. + +## Purpose + +The skill exists to make unsafe Rust authoring and review produce proof-grade +results. It succeeds when an agent: + +- finds every in-scope soundness obligation and every mandatory postcondition + obligation; +- discharges each obligation from verified facts and conspicuous trust; +- detects incomplete, circular, or overbroad reasoning; +- covers every supported shippable configuration; +- distinguishes proof from counterexample-finding evidence; +- reports the exact theorem established without optimism. + +The design optimizes for correct behavior, not encyclopedic coverage or +pedagogical completeness. Agent context is finite. Material belongs in the +runtime package only when it predictably changes authoring, review, or verdict +behavior. + +## Three Separate Layers + +The system deliberately separates: + +1. **Proof authority.** Versioned Rust Reference and standard-library text + supplies Rust axioms. Explicit TCB entries supply admitted non-axiomatic + premises. +2. **Operational procedure.** `skills/unsafe-rust/SKILL.md` and its conditional + references tell an agent what to do. +3. **Maintenance rationale.** This document explains why that procedure has its + present shape and how proposed changes are judged. + +The maintainer document may cite RFCs, research, tools, community practice, and +incidents to explain design choices. Such material does not become a Rust proof +authority merely because maintainers found it persuasive. + +## Governing Model + +Unsafe Rust authoring and audit is obligation discharge. + +The default result sought is source-level Rust soundness under documented Rust +abstract semantics for an exact source snapshot, for every valid use and every +supported compilation configuration, relative to explicit trust. The mandatory +behavioral extension covers every documented postcondition of an unsafe API in +scope and every documented guarantee consumed by an in-scope soundness proof. +Other safe-API robustness, binary, deployment, security, or probabilistic claims +are separate, explicitly scoped theorems with separate premises. + +This model yields the core design: + +- A safety contract is an English-language theorem. +- A safety comment is an English-language proof. +- Every conclusion must follow from checked local facts, established named + invariants, legitimate boundary contracts, authoritative axioms, or explicit + TCB premises. +- Every missing implication makes the result unproved; demonstrating an actual + UB execution is not required to reject the proof. +- Proofs compose through contracts and invariant-carrying state, so global + soundness follows from complete local discharge. + +The skill does not need to teach this as an ontology. It needs to make agents +perform the consequences. + +## Design Principles + +### Obligation-first, not taxonomy-first + +Closed lists of “core unsafe operations” are fragile, invite category debates, +and can cause auditors to miss declarations, generated behavior, invariant +transitions, or future language features. The skill instead asks what exact +precondition or postcondition each proof site supplies or consumes and follows +that proposition through the dataflow. + +Terminology is retained only when it changes behavior. Distinguishing a contract +boundary from an operation that can exhibit UB can explain composition, but an +auditor need not adopt that philosophy if every obligation is still discharged. + +### Local composition, not informal global reasoning + +Nonlocal state is unavoidable; nonlocal informal proof is not. Every shared fact +must be reified as a named invariant or contract that producers establish and +consumers can invoke locally. A function contract about the whole program state +is an acceptable degenerate invariant. + +An explicit dependency graph can help some humans, but requiring one does not +improve correctness when complete location-by-location proofs already record +every producer, consumer, and transition. The runtime procedure requires +coverage, not a particular visualization. + +### Module boundaries are the preferred ownership boundary + +Rust crate-relative visibility is mechanically convenient but enlarges the +region in which a safe edit can invalidate an invariant without an unsafe marker. +For new code, the skill therefore treats code outside the smallest owning module +as foreign and recommends private representation fields. This is stricter than +ordinary same-crate trust and is intended to reduce human proof scope. + +Existing code with broader visibility remains auditable by computing the real +access region. The skill warns rather than fabricating privacy. + +Compiler-enforced unsafe fields are different. They deliberately create a +field-level unsafe boundary analogous to an unsafe function and may have broad +visibility. The skill must still require complete operation contracts and proof +of implicit safe behavior such as destruction. Because the feature's semantics +can evolve, runtime wording remains conditional on the exact audited Rust +version and authoritative documentation. + +The initial design follows the explicit analogy and destructor caveat in +[RFC 3458](https://rust-lang.github.io/rfcs/3458-unsafe-fields.html), while +treating the RFC as advisory and the +[language tracking issue](https://github.com/rust-lang/rust/issues/132922) as a +trigger to revisit the runtime wording when authoritative specification and +stabilization change. + +### Safe caller code is adversarial; selected dependencies are deliberate trust + +Unsafe code cannot rely on arbitrary caller-provided safe callbacks, values, or +safe trait implementations behaving according to prose. Such behavior is not +enforced by the caller accepting an unsafe obligation. + +A project may intentionally trust a selected safe dependency to behave as +documented. That is an explicit opt-in relationship, so the skill permits it +only when the TCB records the exact dependency and contract. Contract channels +include SemVer ranges, exact pins, maintained forks, out-of-band agreements, and +consumer-specific promises. + +Unsafe dependency implementations receive no silent extension of this +exception. They must be recursively audited or explicitly admitted. + +### Authority and trust must be visible + +The project chose a deliberately narrow Rust authority policy: exact Reference +and standard-library text. Explanatory material remains useful for discovery but +cannot silently repair missing authoritative semantics. + +Versioned, narrowly scoped quotations prevent an agent from relying on memory, +search snippets, or wording that changed with Rust. Reviewers must verify that +citations actually entail the attributed fact. When they do not, the correct +result is a documentation gap or TCB admission, not confident paraphrase. + +A TCB audit log makes all remaining trust reviewable. It must not make a theorem +vacuous by admitting the very in-scope implementation or conclusion that the +audit purports to prove. + +### Applicability travels with every premise + +A true proposition outside its domain is not a premise for the case being +proved. Source identity, Rust version, target, configuration, input/state +domain, and execution interval therefore belong to the proof, not merely to +report metadata. + +The required theorem domain must itself be recovered without loss before its +body can be proved. Support declarations, build admission or enforcement, and +observations such as CI have different roles. The auditor preserves controlling +ranges, unions, exclusions, and conditions symbolically; resolves material +ambiguity through project authority or an explicit conservative audit domain; +and treats every normalization, enumeration, partition, or exclusion as a +proof-bearing transformation. Replacing a source predicate requires equality; +using a conservative audit domain requires containment. + +Recovering the required domain and proving coverage of it are distinct +derivations. Let `Required` denote the exact cases quantified by the theorem and +`Covered` the union of cases whose semantic obligations have complete +applicable proofs. An affirmative result requires `Required ⊆ Covered`. +Exhaustive enumeration is one possible proof technique, not the model: symbolic +and parametric proofs are preferable when exact membership is large, dynamic, +or unnecessary. Samples and endpoints can falsify coverage but cannot establish +an interval or inventory. + +This is also why versioned citations alone are insufficient. Reusing an older +Rust guarantee on a later stable release requires an exact +proposition-preserving backwards-compatibility premise; an item's stability +badge is not a blanket promise about every sentence later attached to its +documentation. A cutoff bounds when the theorem was evaluated but supplies no +semantic continuity. Each case lemma's premise applicability must survive +composition across the whole claimed release and configuration region. + +### Producer contracts retain their quantifiers + +A precondition on one constructor, conversion, deserializer, FFI ingress, or +other producer is a proposition about that invocation. Treating it as a +universal fact about the output type replaces an implication about one +invocation with an unproved universally quantified conclusion. + +The runtime procedure requires a complete derivation for the exact quantified +set without reversing the producer implication. Authoritative premises, a +closed and enforced abstraction proof, a verified tool theorem, or an +admissible explicit TCB entry can contribute such a derivation. A consumer may +instead establish the fact for the values it consumes from local checks and +proved producer/transition history. This is a general dataflow rule rather than +a constructor-specific hazard list. + +### Literal verification precedes design + +An auditor must verify the artifact against its controlling contract as written. +Names, tests, implementation shape, comments, history, and known consumers can +help infer design intent, but inferred intent cannot narrow a public contract or +discharge a current proof obligation. + +Design advice is nevertheless valuable when modification is authorized. A +proof-oriented redesign can extract the minimum capability consumers need, +separate accidentally coupled properties, and replace unsupported assumptions +with validation, types, privacy, or smaller contracts. The runtime package keeps +this as a conditional design process within the same skill because it shares +the authority, contract, TCB, and re-audit rules. It maintains a verdict +firewall: the current artifact is judged literally, a proposal receives only a +conditional proof plan, and an implemented redesign is a new artifact requiring +a fresh audit. + +### Reconstructed proofs must improve the proof artifact + +Fail-closed review does not mean giving up when no single citation states the +desired conclusion. Agents should seek admissible indirect derivations from +multiple clauses, definitions, local facts, and named invariants before +finalizing an obligation as unproved. + +If that work reconstructs a material derivation omitted from the existing +safety comment, silently accepting the code wastes the audit's most useful +result. The runtime procedure therefore requires exposing the reconstruction +and separately classifying implementation correctness and proof-documentation +quality. This does not permit retroactively adding a caller obligation or a +provider guarantee to the controlling contract. + +### Verdicts close according to their quantifiers + +Fail-closed reasoning has two different outcomes. A universal soundness proof +with a missing implication is `UNPROVED` even when no exploit is known. An +existential refutation is complete only when a valid in-scope use reaches an +operation or event whose exact required safety proposition is false and the +applicable semantics entails UB; once those facts are proved, the scoped result +is `UNSOUND` even though other executions were not analyzed universally. + +The runtime therefore uses explicit verdict certificates. This prevents both +optimistic acceptance from absence of a witness and over-cautious dilution of a +proved witness into proof debt. Counterexamples do not replace obligation +coverage: one witness fixes the aggregate soundness verdict, while a +comprehensive audit still gives every independently in-scope obligation and +surface a disposition. It need not enumerate every client program exhibiting +the same false obligation. + +### Configuration coverage is universal but need not be enumerative + +Every supported combination that can ship downstream must be sound. Features, +targets, SIMD, allocators, assertions, generators, and build/link inputs interact, +so testing a matrix is insufficient. + +Requiring literal enumeration would create combinatorial busywork. The skill +accepts parametric proofs, exhaustive partitions, generator proofs, and other +valid universal arguments. It requires the theorem, not one audit technique. + +### Generated behavior is behavior + +Macros, proc macros, build scripts, generated bindings, and linker/build outputs +can create public APIs and unsafe operations whose properties depend on caller +tokens, configuration, hygiene, or the destination crate. Auditing only a +generator's handwritten implementation can miss the actual shipped theorem. + +The runtime procedure therefore includes generated artifacts and permits either +an exact-output audit or a proof about every supported output. + +### Soundness and promised behavior are separate obligations + +There is no settled universal definition of API robustness broad enough for this +skill to impose. There is, however, a load-bearing minimum: satisfying an unsafe +API's documented safety preconditions obligates the implementation both to +avoid UB and to establish that API's documented postconditions. Any documented +guarantee consumed by a soundness proof is likewise a mandatory proof +obligation. + +The skill reports postcondition failures separately because they can exist +without UB and can also invalidate downstream unsafe proofs. The witness rules +must respect time-traveling UB: an execution that ever exhibits UB has no +defined observation before or after it. Such an execution can refute soundness, +but cannot itself prove that a documented postcondition is false. A +`CONTRACT-BROKEN` finding therefore requires proof that a valid UB-free +execution falsifies the postcondition; when the only behavioral witness +contains UB, soundness is `UNSOUND` and the postcondition remains `UNPROVED`. +Independent proofs may establish both findings. + +### Evidence is judged by its theorem, not its tool category + +Blanket statements about testing or static analysis are inaccurate. A sampled +run may find only counterexamples; a sound over-approximation, exhaustive model +checker, or deductive verifier may prove a universal fact within its model. + +The runtime rule therefore asks what exact proposition a result establishes, +over what domain, under what assumptions, with what remaining TCB. This rule is +both more rigorous and less likely to bitrot than a named-tool hierarchy. + +The contrast between [Miri's explicitly execution-specific +guarantee](https://github.com/rust-lang/miri/#readme) and proof-oriented tools +such as [Kani](https://model-checking.github.io/kani/) helped expose why the +category label is not the load-bearing distinction. Their documentation informs +skill design but is not a Rust semantic axiom. + +### Probabilistic and deployment claims remain conditional + +A negligible-probability path to UB still refutes unconditional Rust soundness. +Cryptographic assumptions and deployment restrictions can support useful binary +or application theorems, so the skill permits them as conspicuous TCB entries +and requires qualified verdicts. They may not become hidden preconditions of a +safe library API. + +### Compatibility follows propositions, not signatures + +Safety preconditions and documented postconditions are contracts consumed by +proofs. Strengthening a caller obligation or weakening a provider guarantee can +break existing code even when types do not change. Trait contracts have +implementer and consumer directions that must be analyzed separately. + +SemVer, exact pins, forks, and out-of-band agreements govern which changes are +permitted or expected; none independently proves a semantic fact. Audits record +their skill, TCB, source, and contract revisions so later changes can identify +affected proofs. + +## Artifact Architecture + +The installable package is structurally confined to `skills/unsafe-rust/`. +Nothing in the runtime package links to `maintainers/`. + +- [`SKILL.md`](../skills/unsafe-rust/SKILL.md) contains the theorem, mandatory + workflow, hard trust/locality rules, routing, verdicts, and output contract. +- `agents/openai.yaml` contains UI metadata only and must not become a second + instruction channel. +- [`proof-obligations.md`](../skills/unsafe-rust/references/proof-obligations.md) + contains detailed contract, invariant, citation, and comment technique. +- [`abstraction-design.md`](../skills/unsafe-rust/references/abstraction-design.md) + contains the conditional proof-oriented design process and the firewall + between current-artifact verification and candidate design. +- [`api-boundaries-and-evolution.md`](../skills/unsafe-rust/references/api-boundaries-and-evolution.md) + contains module/API/trait/macro/dependency/robustness/evolution guidance. +- [`configurations-and-generated-code.md`](../skills/unsafe-rust/references/configurations-and-generated-code.md) + contains supported-domain recovery and transformation, configuration-closure, + code-generation, target, FFI, assembly, allocator, and linking guidance. +- [`tcb-and-evidence.md`](../skills/unsafe-rust/references/tcb-and-evidence.md) + contains trust categories, dependency relationships, conditional claims, and + tool-evidence evaluation. +- [`audit-reporting.md`](../skills/unsafe-rust/references/audit-reporting.md) + contains scope, obligation-ledger, finding, verdict, and preservation rules. +- `assets/` contains copyable audit artifacts, not additional hidden + instructions. +- Future evaluations belong outside the installable package. + +Use this sentence-level inclusion test: + +> Every agent-facing sentence must set a required result, require an action or +> verification, define a term needed by such a requirement, route to +> conditionally needed material, or provide the smallest example necessary to +> disambiguate one of those things. + +Anything else belongs here or nowhere. Prefer removing redundant explanation to +adding “do not worry about this” qualifications. + +## Resolved Design Decisions and Traceability + +This table records stable rationale, not conversational history. The final +column records candidate semantic evaluation scenarios, not execution results. + +| ID and decision | Failure prevented | Agent-facing consequence | Runtime location | Evaluation requirement | +|---|---|---|---|---| +| D01 — Require exact proof obligations rather than a primitive-operation taxonomy | Missing future, generated, declaration, or state-transition obligations | Follow every consumed contract to premises | [Core composition](../skills/unsafe-rust/SKILL.md#compose-proofs-locally-and-literally); [proof reference](../skills/unsafe-rust/references/proof-obligations.md) | EV01 — omitted non-syntactic invariant consumer | +| D02 — Reify nonlocal facts in named local invariants | Hand-waved global state and circular proofs | Establish/preserve/consume at local boundaries | [Core composition](../skills/unsafe-rust/SKILL.md#compose-proofs-locally-and-literally); [invariant mechanics](../skills/unsafe-rust/references/proof-obligations.md#carry-invariants-locally) | EV02 — delayed field consumer across calls | +| D03 — Prefer smallest-module ownership | Safe same-crate mutation silently invalidates invariants | Private fields; outside module untrusted | [Core composition](../skills/unsafe-rust/SKILL.md#compose-proofs-locally-and-literally); [module privacy](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#use-module-privacy) | EV03 — `pub(super)` invariant mutation | +| D04 — Permit compiler-enforced public unsafe fields | Treating an explicit unsafe API as hidden safe access | Document and prove every operation plus implicit behavior | [Unsafe fields](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#handle-unsafe-fields) | EV04 — public unsafe field with drop caveat | +| D05 — Treat caller safe code adversarially | Unsafe code trusts unenforced callback/trait behavior | Seal, validate, or make implementer contract unsafe | [API closure](../skills/unsafe-rust/SKILL.md#close-api-and-configuration-boundaries); [traits](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#audit-traits-and-sealing) | EV05 — malicious safe trait impl | +| D06 — Permit explicit selected-safe-dependency trust | Pointless recursive audits of intentionally chosen safe APIs | Record exact safe contract in TCB | [Premise policy](../skills/unsafe-rust/SKILL.md#use-only-applicable-premises); [dependency contracts](../skills/unsafe-rust/references/tcb-and-evidence.md#record-dependency-contracts) | EV06 — selected sort API versus caller comparator | +| D07 — Audit or admit unsafe dependencies | Satisfying caller contract mistaken for implementation correctness | Recursive proof or `UNSAFE-DEP` entry | [Premise policy](../skills/unsafe-rust/SKILL.md#use-only-applicable-premises); [dependency contracts](../skills/unsafe-rust/references/tcb-and-evidence.md#record-dependency-contracts) | EV07 — unsound third-party unsafe helper | +| D08 — Restrict Rust axioms to versioned Reference/std text | Folklore and explanatory documents become premises | Quote, link, and verify exact authority | [Premise policy](../skills/unsafe-rust/SKILL.md#use-only-applicable-premises); [citations](../skills/unsafe-rust/references/proof-obligations.md#cite-authoritative-axioms) | EV08 — mischaracterized citation | +| D09 — Recover the theorem domain losslessly and carry applicability through every derivation | A range, union, condition, or moving policy is contracted during normalization; a sampled or out-of-domain premise is then used to assert closure | Preserve source predicates; prove equality/containment for every transformation; require `Required ⊆ Covered`; certify every multi-version premise region | [Domain recovery](../skills/unsafe-rust/SKILL.md#recover-the-required-domain); [applicability](../skills/unsafe-rust/references/proof-obligations.md#qualify-applicability); [supported set](../skills/unsafe-rust/references/configurations-and-generated-code.md#recover-the-required-supported-set) | EV09 — symbolic interval/union with an easily omitted interior or conditional member, plus sparse version evidence | +| D10 — Require indirect-derivation search before final failure | Valid multi-clause proofs are rejected because no single sentence states the conclusion | Unfold definitions, combine exact premises, and identify the smallest remaining gap | [Proof workflow](../skills/unsafe-rust/SKILL.md#follow-the-proof-workflow); [indirect derivations](../skills/unsafe-rust/references/proof-obligations.md#search-for-indirect-derivations) | EV10 — validity derived from orthogonal std guarantees | +| D11 — Expose material reconstructed proofs | Reviewer silently accepts code whose safety comment omits the actual argument | Report reconstructed proof and proof-artifact defect separately | [Proof-grade documentation](../skills/unsafe-rust/SKILL.md#write-and-review-proof-grade-documentation); [proof review](../skills/unsafe-rust/references/proof-obligations.md#review-a-proof) | EV11 — sound operation with hand-waving comment | +| D12 — Include every safe API surface | Public field, trait, constructor, hidden item, or macro bypasses invariant | Apply explicit surface checklist | [API closure](../skills/unsafe-rust/SKILL.md#close-api-and-configuration-boundaries); [surface inventory](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#enumerate-every-surface) | EV12 — macro-generated safe constructor | +| D13 — Cover every supported configuration abstractly or concretely | Tested matrix misses shippable combination | Recover the required set and prove closure abstractly or by justified exhaustive cases | [API/configuration closure](../skills/unsafe-rust/SKILL.md#close-api-and-configuration-boundaries); [configuration reference](../skills/unsafe-rust/references/configurations-and-generated-code.md) | EV13 — feature/target interaction | +| D14 — Audit output as well as generators | Generator source appears safe while expansion is not | Capture exact output or prove generator property | [Generated code](../skills/unsafe-rust/references/configurations-and-generated-code.md#audit-generated-and-expanded-code); [macros](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#audit-macros-and-hidden-apis) | EV14 — caller-token-dependent proc macro | +| D15 — Prove mandatory documented postconditions over defined executions | UB freedom masks broken guarantees, or an observation from a UB-containing execution is treated as defined | Prove unsafe-API and soundness-consumed guarantees; require proof of a valid UB-free falsifying execution for `CONTRACT-BROKEN`; trace consumers | [Exact claim](../skills/unsafe-rust/SKILL.md#establish-the-exact-claim); [verdicts](../skills/unsafe-rust/SKILL.md#use-exact-verdicts); [documented behavior](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#prove-documented-behavior) | EV15 — UB-only apparent behavior failure plus an independent UB-free contract failure | +| D16 — Judge tools by exact theorem | Both false confidence in clean runs and false rejection of formal proof | Check scope/model/bounds/TCB | [Evidence policy](../skills/unsafe-rust/SKILL.md#evaluate-trust-and-evidence); [tool theorem](../skills/unsafe-rust/references/tcb-and-evidence.md#judge-tools-by-their-theorem) | EV16 — bounded result versus completeness proof | +| D17 — Make deployment/crypto assumptions conditional | Negligible or restricted UB mislabeled unconditional soundness | Explicit TCB and qualified theorem | [External/deployment assumptions](../skills/unsafe-rust/references/tcb-and-evidence.md#record-external-and-deployment-assumptions); [report aggregation](../skills/unsafe-rust/references/audit-reporting.md#aggregate-verdicts) | EV17 — signature-gated bad path | +| D18 — Preserve `#[doc(hidden)]` soundness but not implied SemVer | Hidden reachability becomes hidden safety precondition | Audit direct safe use; separate compatibility | [API closure](../skills/unsafe-rust/SKILL.md#close-api-and-configuration-boundaries); [hidden APIs](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#audit-macros-and-hidden-apis) | EV18 — reachable hidden safe constructor | +| D19 — Treat contract changes as proof changes | Safety prose changes without caller/implementer re-audit | Directional compatibility analysis and triggers | [Contract evolution](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#evolve-contracts-deliberately); [TCB evolution](../skills/unsafe-rust/references/tcb-and-evidence.md#review-and-evolve-the-tcb) | EV19 — strengthened unsafe precondition | +| D20 — Separate literal audit from proof-oriented redesign | Inferred intent launders a current defect, or review misses a much simpler sound model | Preserve current verdict; derive minimum capability and re-audit implemented redesign | [Design routing](../skills/unsafe-rust/SKILL.md#design-for-provability-when-requested); [design reference](../skills/unsafe-rust/references/abstraction-design.md) | EV20 — overbroad nominal field abstraction | +| D21 — Certify verdicts by logical proof shape | Invalid proof is accepted because no exploit is known, or a completed existential UB derivation is diluted to `UNPROVED` | Use `UNPROVED` for an incomplete universal proof; use `UNSOUND` when valid use, reachability, false safety proposition, and UB consequence all close | [Verdict certificates](../skills/unsafe-rust/SKILL.md#use-exact-verdicts); [report aggregation](../skills/unsafe-rust/references/audit-reporting.md#aggregate-verdicts) | EV21 — paired incomplete obligation with no witness and multi-premise exact-version witness that must close | +| D22 — Preserve producer-contract quantifiers | One constructor's precondition is promoted into a postcondition or invariant of every value of its output type | Prove the exact consumed values or quantified set without reversing the producer implication | [Core composition](../skills/unsafe-rust/SKILL.md#compose-proofs-locally-and-literally); [premise classification](../skills/unsafe-rust/references/proof-obligations.md#separate-kinds-of-premises) | EV22 — unsafe constructor contract plus a separate safe producer that violates the assumed property | + +## Explicit Non-goals + +The runtime skill does not: + +- teach ordinary Rust syntax or ownership fundamentals; +- reproduce the Rust Reference or standard-library documentation; +- claim an exhaustive list of UB, unsafe operations, hazards, configuration + axes, or proof obligations; +- require finite enumeration when a symbolic or parametric domain proof is + complete; +- require enumeration of every client program witnessing one already-identified + false obligation; +- require an explicit safety-dependency graph; +- require a second proof-record schema beyond ordinary contracts, invariants, + obligation coverage, and audit artifacts; +- impose a proof-state machine or engagement-mode matrix in addition to the one + proof workflow; +- split proof-oriented redesign into a separate skill with a duplicate + authority or verdict model; +- prescribe a fixed number of redesign candidates or an arbitrary scoring + formula; +- standardize undocumented API robustness; +- decide project support or SemVer policy without evidence; +- turn advisory sources, current implementation behavior, or this document into + Rust axioms; +- equate all static analysis with bug finding or all formal tools with proof; +- preserve tentative terminology, resolved debate, or historical hedging in + agent-facing prose; +- certify a compiler-generated binary when only source semantics were proved; +- use inferred intent or a proposed redesign as evidence for the current + artifact. + +Rejected alternatives belong here only when recording the decision prevents a +plausible regression. This document is not a transcript or a repository for +every idea considered. + +## Change-Acceptance Protocol + +Every behavior-changing proposal must answer: + +1. What concrete omission, false acceptance, false rejection, or recurring + author/reviewer error does it prevent? +2. What observable agent behavior must change? +3. What authoritative basis, incident, proof principle, or explicit project + policy supports it? +4. Does it belong in always-loaded instructions, a conditional reference, a + deterministic tool/template, an evaluation, this document, or nowhere? +5. Is existing text already sufficient? +6. What runtime context/token cost does it add? +7. What semantic evaluation would demonstrate the improvement without leaking + the intended answer? +8. Does it alter theorem scope, authority, trust, verdict meaning, compatibility, + or previously issued audit judgments? +9. What material can be simplified or removed once the change exists? + +Classify the change: + +- **Editorial:** No intended change in agent behavior or accepted proofs. +- **Operational:** Changes authoring, review, coverage, artifact, or verdict + behavior. +- **Foundational:** Changes the primary theorem, authority model, trust policy, + scope, or status meanings. + +Operational changes must update traceability and semantic evaluations. +Foundational changes must amend this document in the same change and identify +how existing audits should be interpreted. Editorial changes should not smuggle +in new obligations. + +## Evolution and Compatibility of the Skill + +Every persistent audit should identify the skill revision used. A later, +stricter procedure can reveal that an earlier proof was incomplete; it does not +retroactively make the old report complete or silently change its stated +theorem. + +Treat these as behaviorally significant skill changes: + +- accepting or rejecting a new kind of proof premise; +- changing Reference/std authority policy; +- changing selected dependency or unsafe dependency trust; +- expanding or narrowing valid-use or configuration quantification; +- changing the meaning or precedence of verdicts; +- changing required postcondition/robustness scope; +- changing persistent audit artifacts in a way that drops information. + +When authoritative Rust documentation evolves, update routing or examples only +after checking exact support ranges and compatibility promises. Avoid embedding +semantic fact lists in the skill; that is the main defense against bitrot. + +When a relevant unstable feature stabilizes, replace conditional wording only +after authoritative documentation exists for the supported Rust range. Do not +derive a stable rule solely from an accepted RFC or implementation. + +## Validation Strategy + +Validate behavior with semantic fixtures, not snapshots of preferred wording. +Use fresh agents with only the skill, task, and raw artifact under review. Do +not leak the expected bug or intended conclusion. + +The evaluator-only [source catalog](../evals/unsafe-rust/source-catalog.md) and +[testing plan](../evals/unsafe-rust/testing-plan.md) define corpus provenance, +oracle isolation, fresh-agent execution, scoring, and release gates. They are +maintenance artifacts and must not be linked from the installable skill. + +Give every operational decision in the traceability table a semantic fixture or +an explicit reason why another fixture exercises the same behavior. Across the +suite, require independent coverage of: + +- lossless theorem-domain recovery, including symbolic ranges, unions, + conditions, justified enumerations, `Required ⊆ Covered`, and + multi-release premise applicability; +- authority checking, indirect derivation, producer quantifiers, local + invariant/dataflow composition, and exposed reconstructed proofs; +- adversarial safe callers, every safe API boundary, interacting compilation + configurations, and generated behavior; +- exact TCB/dependency relationships and both limited and genuinely universal + tool evidence; +- all verdict certificates, including incomplete proofs without invented + witnesses, completed multi-premise UB witnesses, whole-execution + postcondition reasoning, and conditional deployment/probabilistic claims; +- reporting behavior that preserves exact scope and proof-artifact defects + without imposing an unnecessary graph or witness inventory; and +- the abstraction-design firewall, minimum-capability modeling, consequential + candidate comparison, compatibility/migration analysis, rejection of + proposal laundering, and fresh audit of implemented changes. + +Every real audit incident should be considered for a regression fixture. Static +artifact review is not behavioral validation; run evaluations only in an +explicitly scoped validation phase. + +## Anti-drift Controls + +Maintain these controls as the project grows: + +- Keep the installable package allowlisted or structurally isolated from + `maintainers/`. +- Reject runtime-package links into maintainer material. +- Check one-way traceability links from this document to stable runtime headings. +- Require operational changes to update traceability and evaluations, or state + why no existing behavior changes. +- Periodically perform a subtractive review: remove each agent-facing paragraph + hypothetically and retain it only if correct behavior becomes worse. +- Review the skill when supported Rust ranges change, relevant features + stabilize, authoritative documentation changes materially, or an incident + exposes a gap. +- Use short decision records for major reversals, including the evidence and + conditions that would reverse the decision again. Do not duplicate Git history + in a generic changelog. +- Keep templates structural. Do not let them become a second source of + operational rules that diverges from the references. + +## Known Documentation Sensitivities + +Some topics, especially evolving unsafe-field, aliasing/provenance, FFI, +target-feature, and compiler/linker behavior, may lack authoritative text strong +enough for a requested proof. The runtime response must be `UNPROVED` or +conditional on an explicit TCB entry, plus a narrowly stated documentation gap. + +This section records why the skill remains authority-driven and conditional; it +must not grow into an alternative semantic specification. diff --git a/skills/unsafe-rust/SKILL.md b/skills/unsafe-rust/SKILL.md index 370782667b..7c60a97623 100644 --- a/skills/unsafe-rust/SKILL.md +++ b/skills/unsafe-rust/SKILL.md @@ -38,6 +38,46 @@ Prove source-level Rust soundness first. State claims about a particular compiler backend, binary, platform, security property, probability, or deployment separately with their additional premises. +## Recover the Required Domain + +Before consuming premises or issuing a full verdict, derive the exact domain +quantified by the claim. Let `Required(case)` denote the valid uses, inputs, +states, executions, Rust/toolchain versions, and configurations that the claim +requires. Let `Covered(case)` hold exactly where every obligation the claim +requires for that case has a complete derivation from applicable premises. +Within one obligation, valid case lemmas may be unioned. Across distinct +obligations, claim-level coverage is their pointwise conjunction—not a union of +regions in which different obligations happened to be proved. + +- Preserve the controlling domain expressions symbolically, including ranges, + unions, exclusions, quantifiers, and conditional or moving policies. Record + their exact sources and audit cutoff. +- If applicable project sources conflict or materially underdetermine support, + obtain an authorized resolution, derive an explicit conservative audit + domain containing every materially supported candidate predicate, or leave + the affected combined claim `UNPROVED`. Do not call a conservative audit + domain the resolved project promise. +- Treat every normalization, enumeration, partition, exclusion, and policy + merge as a proof step. Prove equality before replacing one domain expression + with another, the required containment before using a conservative superset, + and `Required ⊆ Covered` before concluding `PROVED`. +- A finite inventory requires evidence both that every listed member belongs + and that no required member is omitted. Endpoints, one representative per + apparent category, CI jobs, lockfiles, and other samples do not prove an + interval or set inventory. +- Prefer a parametric proof over the symbolic predicate when enumeration would + be large or its exact membership is unavailable. Otherwise report proved + regions and the unresolved remainder; do not turn it into an implicit + exclusion. +- An audit cutoff limits the temporal scope of a claim. It does not establish + semantic continuity, enumerate releases before the cutoff, or make sampled + documentation applicable between samples. + +Apply +[configuration closure](references/configurations-and-generated-code.md#recover-the-required-supported-set) +to derive supported compilation cases and prove every transformation of that +predicate. + ## Use Only Applicable Premises - Bottom out Rust-language and standard-library facts in exact applicable text @@ -48,14 +88,6 @@ 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 @@ -115,36 +147,29 @@ 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, 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 + executions, mandatory postconditions, TCB, exclusions, and whether design + alternatives are requested. +2. **Recover the domain.** Preserve the controlling expressions, derive + `Required`, justify every transformation or conservative enlargement, and + state how eventual proof cases will establish `Required ⊆ Covered`. +3. **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. -3. **State every obligation.** Obtain each controlling contract, decompose it + generated or expanded artifact across the required domain. +4. **State every obligation.** Obtain each controlling contract, decompose it literally, and state the exact proposition and applicability to prove. -4. **Construct the derivation.** Derive every conjunct from checked local facts, +5. **Construct the derivation.** Derive every conjunct from checked local facts, named invariants, applicable authoritative axioms, tool-derived theorems, or 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.** 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 - optimism. - -Do not require a concrete UB counterexample to reject an incomplete proof. A -missing, ambiguous, circular, or inapplicable derivation is sufficient for -`UNPROVED`. +6. **Close and challenge.** Give every literal contract clause and safe surface + a disposition, establish domain closure, and try to falsify the domain + recovery, contract reading, derivations, and coverage with boundary and + adversarial cases derived from the actual clauses. +7. **Certify and report.** Apply the quantifier-sensitive certificates below. + Keep every unresolved obligation visible and state the smallest missing + implication. Record proofs, TCB, coverage, findings, postcondition failures, + documentation gaps, and residual scope without optimism. ## Write and Review Proof-Grade Documentation @@ -217,16 +242,20 @@ new artifact and audit them anew. Read [audit-reporting.md](references/audit-reporting.md) before delivering a persistent or full audit. -- **PROVED:** Every obligation for the exact named claim is discharged over its - complete applicability, relative to the stated TCB. -- **UNPROVED:** At least one required derivation, premise, applicability or - coverage argument, postcondition proof, or citation is missing, ambiguous, - circular, or unverifiable. -- **UNSOUND:** A valid use or in-scope execution is proved to reach undefined - behavior. -- **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. +| Verdict | Required certificate | +|---|---| +| **PROVED** | Every obligation for the exact named claim has a checked derivation over its complete applicability, `Required ⊆ Covered`, and every premise is proved from admissible sources or appears as an accepted entry in the stated TCB. | +| **UNPROVED** | A required derivation, premise, applicability or domain-closure argument, postcondition proof, or citation remains missing, ambiguous, circular, or unverifiable, and no applicable existential refutation below is complete. | +| **UNSOUND** | There exists a proved valid in-scope use or execution which reaches an executed operation or semantic event, its exact required safety proposition is false there, and applicable authoritative semantics—possibly together with an explicit TCB premise about the implementation—entails undefined behavior. | +| **CONTRACT-BROKEN** | There exists a proved valid in-scope execution which, considered as a whole, contains no undefined behavior and falsifies a documented postcondition. | + +Failure to prove a universal obligation is enough for `UNPROVED`; do not invent +a counterexample. Conversely, once all parts of an existential UB certificate +are proved, report the scoped soundness claim `UNSOUND`; do not continue to +demand a universal positive lemma and dilute the result to `UNPROVED`. A +violation of user-authored safety prose is not by itself a runtime UB event: +trace the certificate through applicable contracts to the exact authoritative +or explicitly trusted UB consequence. Classify a witness using the execution as a whole, not observations from a prefix of an execution that later reaches undefined behavior. An @@ -239,8 +268,11 @@ verdicts. Apply verdicts separately to soundness, documented postconditions, and conditional application claims. State exact scope, applicability, and TCB -beside every verdict. Never substitute “looks sound,” “probably sound,” or test -success. +beside every verdict. For every affirmative claim spanning multiple Rust +releases, identify a parametric proof, an exhaustive applicable partition, or +an exact proposition-preserving compatibility premise whose covered domain +contains the claimed release set. Never substitute endpoints, sparse samples, +an audit cutoff, “looks sound,” “probably sound,” or test success. For a persistent audit, complete: diff --git a/skills/unsafe-rust/assets/tcb-audit-log-template.md b/skills/unsafe-rust/assets/tcb-audit-log-template.md index 7cfad4e866..0347294827 100644 --- a/skills/unsafe-rust/assets/tcb-audit-log-template.md +++ b/skills/unsafe-rust/assets/tcb-audit-log-template.md @@ -8,7 +8,8 @@ - **Source snapshot:** `` - **Generated artifacts:** `` - **Rust/toolchain scope:** `` -- **Supported configuration predicate:** `` +- **Supported configuration predicate:** `` - **Theorem(s) supported:** `` - **Owner/reviewer:** `` @@ -36,8 +37,8 @@ support.>` - **Disposition:** `` - **Exact proposition:** `` -- **Quantification and scope:** `` +- **Quantification and scope:** `` - **Exact identity:** `` - **Source/contract:** `` proposition has an audit, additional contract, or explicit admission. - [ ] Every third-party unsafe implementation is recursively audited or explicitly admitted. +- [ ] Every version-spanning compatibility entry states the exact proposition + preserved and its exact release/configuration region; pins, stability + badges, and sampled documentation are not used as interval coverage. - [ ] Tool-derived facts state their exact theorem and residual TCB. - [ ] External, deployment, and probabilistic assumptions qualify the verdict conspicuously. 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 387ce2f7a6..76d0678280 100644 --- a/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md +++ b/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md @@ -2,27 +2,18 @@ ## Claims and Verdicts -- **Soundness claim:** `` -- **Soundness verdict:** `` -- **Documented-postcondition claim:** `` -- **Documented-postcondition verdict:** `` +| Claim ID | Exact theorem | Required-domain ID | Verdict | Certificate/proof/finding | TCB and qualification | +|---|---|---|---|---|---| +| `` | `` | `` | `` | `` | `` | +| `` | `` | `` | `` | `` | `` | +| `` | `` | `` | `` | `` | `` | + - **Combined mandatory result:** `` -- **Conditional application claim:** `` -- **Conditional application result:** `` - **Scope:** `` -- **Supported configuration predicate:** `` -- **Support-policy sources/conflicts:** `` - **TCB log:** `` - **Skill revision:** `` -- **Qualification:** `` ## Audited Snapshot @@ -93,14 +84,33 @@ and record every additional language-reachable surface in the table above. |---|---|---|---|---|---|---|---|---| | `` | `` | `` | `` | `` | `` | `` | `` | `` | -## Configuration Closure +## Theorem-Domain and Configuration Closure + +### Required Domain Recovery + +| Step ID | Controlling source expression or prior predicate | Derived predicate/inventory/partition | Relation to prove (write symbolically) | Equality/containment evidence | Status | +|---|---|---|---|---|---| +| `` | `` | `` | `` | `` | `` | + +- **Audit cutoff:** `` +- **Exact `Required` predicate:** `` +- **Policy conflicts/authorized resolution:** `` +- **Unresolved domain:** `` + +### Covered Domain -- **Supported set:** `` - **Discovered axes:** `` -- **Coverage proof:** `` +- **Exact `Covered` predicate:** `` +- **Coverage proof:** `` +- **Closure certificate:** `` +- **Version-spanning premise basis:** `` - **Generated artifacts:** `` - **Enforced exclusions:** `` - **Sampled/tested configurations:** `` @@ -139,7 +149,14 @@ Full log: `` none>` - **Defect:** `` - **Authority/TCB involved:** `` -- **UB witness:** `` +- **UB certificate — valid use:** `` +- **UB certificate — reachability:** `` +- **UB certificate — false safety proposition:** `` +- **UB certificate — consequence:** `` - **Defined postcondition refutation:** `` @@ -194,10 +211,14 @@ explicitly excluded region. Explain enforcement of exclusions.>` ## Final Attestation - [ ] Every in-scope obligation has a status. -- [ ] Every `PROVED` obligation has a complete checked derivation. +- [ ] Every controlling domain expression is preserved, and every normalization, + enumeration, partition, merge, or exclusion has its required equality or + containment proof. +- [ ] Every verdict has the certificate required by `SKILL.md`, including + `Required ⊆ Covered` for `PROVED` and every existential link for + `UNSOUND` or `CONTRACT-BROKEN`. - [ ] Every material derivation reconstructed during review is exposed with its applicability, and deficient proof artifacts are reported separately. -- [ ] Every supported configuration is covered by proof. - [ ] Every consumed citation and TCB entry was independently verified. - [ ] Every consumed TCB entry supporting `PROVED` has an accepted human disposition. diff --git a/skills/unsafe-rust/references/api-boundaries-and-evolution.md b/skills/unsafe-rust/references/api-boundaries-and-evolution.md index 6df8fb05b9..1609e2dc8a 100644 --- a/skills/unsafe-rust/references/api-boundaries-and-evolution.md +++ b/skills/unsafe-rust/references/api-boundaries-and-evolution.md @@ -226,12 +226,9 @@ At minimum, an unsafe API implementation is responsible for both: 2. establishing every documented postcondition when its safety preconditions and other documented conditions are met. -Evaluate postconditions independently under the verdict rule in `SKILL.md`. A -UB-containing execution cannot itself prove the required UB-free behavioral -refutation: report soundness as `UNSOUND` and leave that postcondition -`UNPROVED` unless an independent UB-free witness or equivalent proof resolves -it. Determine whether a proved broken guarantee can make downstream unsafe -consumers unsound. +Evaluate postconditions independently under the verdict certificates in +`SKILL.md`, then determine whether a proved broken guarantee can make downstream +unsafe consumers unsound. Do not invent a universal standard for undocumented robustness. State the exact behavioral claim being reviewed: panic freedom, determinism, resource bounds, diff --git a/skills/unsafe-rust/references/audit-reporting.md b/skills/unsafe-rust/references/audit-reporting.md index 69ff28f2d8..c895a453de 100644 --- a/skills/unsafe-rust/references/audit-reporting.md +++ b/skills/unsafe-rust/references/audit-reporting.md @@ -15,9 +15,9 @@ Before reviewing proofs, record: - exact repository, source revision/digest, workspace packages, generated artifacts, and relevant uncommitted changes; -- supported toolchain/configuration predicate, its controlling policy sources, - conflicts or gaps, audit cutoff, authorized resolution or conservative audit - domain, and enforced exclusions; +- controlling support expressions, conflicts or gaps, audit cutoff, authorized + resolution or conservative audit domain, the exact symbolic `Required` + predicate, every transformation used to derive it, and enforced exclusions; - dependency resolution and relevant source identities; - API, module, binary, or whole-project scope; - soundness theorem and documented postconditions in scope; @@ -48,6 +48,7 @@ For each obligation, record: - supporting local facts, invariant clauses, axioms, and TCB entries, with the applicability of each premise; - domain actually covered by the derivation and any case partition; +- the equality or containment proof for every domain transformation consumed; - proof location; - reviewer verification; - status and finding link. @@ -85,16 +86,18 @@ be `UNSOUND` while a different configuration remains `UNPROVED`. Issue `PROVED` for the combined default claim only when every in-scope soundness and documented-postcondition obligation is proved. -Classify a witness using the execution as a whole. A valid execution that ever -exhibits UB can establish `UNSOUND` but cannot itself establish the UB-free -existence claim required for `CONTRACT-BROKEN`. If it is the only behavioral -evidence, report that postcondition as `UNPROVED`. An independent UB-free -witness or equivalent existence proof may establish `CONTRACT-BROKEN`; -separate proofs may establish both verdicts. +Certify each result with the proof shape required by `SKILL.md`. For `PROVED`, +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 +link from valid use through reachability and a false safety proposition to the +applicable UB consequence. For `CONTRACT-BROKEN`, certify that the falsifying +execution is UB-free as a whole. Otherwise state the smallest gap and use +`UNPROVED`. Place qualifications in the theorem, not in vague prose. Use: -> PROVED for `` under ``, relative to TCB +> PROVED for `` over ``, relative to TCB > ``. For a deployment, external, or cryptographic premise, name the exact entry and @@ -117,8 +120,11 @@ Each finding should contain: derivation; - smallest missing, false, circular, or unsupported implication; - authoritative contract or TCB entry involved; -- whether a valid UB witness or a separate UB-free postcondition refutation or - equivalent existence proof is known; +- for a claimed UB witness, the valid use, executed operation or semantic event, + false required safety proposition, and authoritative or TCB-backed UB + consequence; +- whether 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. @@ -165,10 +171,11 @@ 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, controlling policy - sources and conflicts, audit cutoff, authorized resolution or conservative - superset, axes, abstract or enumerative coverage proof, generated artifacts, - and enforced exclusions. +6. **Theorem-domain and configuration closure:** Controlling policy + expressions, symbolic `Required`, transformation/equivalence or containment + proofs, audit cutoff, axes, `Covered`, `Required ⊆ Covered`, premise-version + applicability, generated artifacts, enforced exclusions, and unresolved + remainder. 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 f436c53db5..192a19c973 100644 --- a/skills/unsafe-rust/references/configurations-and-generated-code.md +++ b/skills/unsafe-rust/references/configurations-and-generated-code.md @@ -2,21 +2,22 @@ ## Contents -- [Define the supported set](#define-the-supported-set) +- [Recover the required supported set](#recover-the-required-supported-set) - [Discover configuration axes](#discover-configuration-axes) -- [Prove every supported combination](#prove-every-supported-combination) +- [Prove coverage of the recovered set](#prove-coverage-of-the-recovered-set) - [Audit generated and expanded code](#audit-generated-and-expanded-code) - [Audit targets, SIMD, and concurrency](#audit-targets-simd-and-concurrency) - [Audit allocators, panic modes, and assertions](#audit-allocators-panic-modes-and-assertions) - [Audit FFI, assembly, linking, and global symbols](#audit-ffi-assembly-linking-and-global-symbols) - [Record configuration coverage](#record-configuration-coverage) -## Define the Supported Set +## Recover the Required Supported Set -Write a precise predicate `Supported(configuration)` before claiming full -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. +Preserve each controlling support expression as a precise symbolic predicate +before claiming full soundness. Fix the exact source or packaged artifact and +audit cutoff. Let each 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: @@ -38,20 +39,47 @@ 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 +authorized project decision, derive an explicit conservative audit predicate +containing every materially supported candidate predicate identified from the +controlling sources, or report regional results and leave the full claim +`UNPROVED`. Call the resulting predicate `Required(configuration)`. Do not call +a conservative `Required` predicate 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. +Every transformation from controlling expressions to `Required` is a proof +obligation. Record the transformation and the relation it must establish: + +- an exact normalization requires equality in both directions; +- a conservative audit domain requires every materially supported candidate + predicate to be contained in `Required`; +- an exclusion requires an applicable support contract and, when soundness + depends on preventing shipment, effective enforcement; and +- a case partition used for proof requires `Required` to be contained in the + union of the proved case predicates. Cases need not be disjoint unless the + proof relies on uniqueness. + +Do not replace a range or conditional predicate with a finite inventory until +both membership and completeness are established from applicable evidence. A +list of endpoints, sampled toolchains, one apparent representative per minor +series, or successfully observed releases is not an inventory proof. When +exact membership is unavailable or large, retain the symbolic predicate and +prove it parametrically; if neither parametric proof nor justified exhaustive +partition closes, leave the remainder `UNPROVED`. + +Let `Covered(configuration)` be the union of configuration regions for which +all applicable semantic obligations and premises are proved. Full configuration +closure requires a checked containment proof `Required ⊆ Covered`. Coverage of +an incorrectly contracted restatement does not establish this relation. + Preserve conditional and nonlinear structure across every discovered axis -rather than collapsing the predicate to a single MSRV. It may be finite, +rather than collapsing `Required` 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. +dynamic policies at the audit cutoff. A cutoff identifies when a dynamic +predicate was recovered; it neither enumerates the toolchains before that date +nor supplies semantic continuity between sampled versions. Record: @@ -107,10 +135,11 @@ Discover the actual axes from the audited project and authoritative toolchain contracts. Add newly discovered axes to the audit and report gaps in this reference. -## Prove Every Supported Combination +## Prove Coverage of the Recovered Set -Every supported combination must be sound. A CI matrix, sample of targets, or -pairwise feature test does not establish this universal claim. +Every case in `Required` must be sound. A CI matrix, sample of targets, or +pairwise feature test does not establish either the required domain or this +universal semantic claim. Avoid Cartesian-product enumeration when an abstract proof is clearer. Valid coverage arguments include: @@ -118,8 +147,8 @@ coverage arguments include: - prove one implementation is parametric over an axis; - partition configurations into equivalence classes and prove the partition is exhaustive and each class representative shares the relevant semantics; -- prove mutually exclusive `cfg` predicates form a total partition over the - supported set; +- prove mutually exclusive `cfg` predicates form a total partition over + `Required`; - prove a generator emits only members of a finite audited family; - prove independent lemmas for axes, then prove their assumptions remain independent under composition; @@ -134,8 +163,12 @@ Attach a configuration-domain predicate to every obligation, premise, and coverage lemma. A premise proved for one target, toolchain, feature set, or generated artifact cannot discharge another case merely because the source looks similar. If separate lemmas cover separate regions, prove that their -union contains the entire supported set and that their assumptions remain true -where regions interact. +union is `Covered`, that `Required ⊆ Covered`, and that their assumptions remain +true where regions interact. + +Before accepting closure, try to exhibit a required boundary, interior, +conditional, or cross-axis case absent from `Covered`. This is a falsification +check, not a substitute for the containment proof. Do not infer semantic coverage from successful compilation. Compilation may establish syntax, typing, and selected compiler-enforced conditions; unsafe @@ -277,19 +310,26 @@ Audit whole-program/link obligations when relevant, including: - linker flags or custom target settings that alter assumptions used by source proofs. -A compilation or linker option that still emits a binary belongs to the -supported configuration set if users may ship it. Do not label a flag itself -“Rust undefined behavior” without authoritative text. Instead, trace any -resulting execution to the exact violated Rust or external contract, or state -that the artifact lies outside the proved source-level claim. +A compilation or linker option belongs to `Required` only when the controlling +support predicate includes it; the technical ability to emit or ship a binary +does not itself define project support. For an included option that emits a +binary, do not label the flag itself “Rust undefined behavior” without +authoritative text. Trace any resulting execution to the exact violated Rust or +external contract, or state that the artifact lies outside the proved +source-level claim. ## Record Configuration Coverage For each audit, report: -- the formal or operational definition of the supported set; +- every controlling support predicate and its exact source; +- the symbolic `Required` predicate, audit cutoff, and any unresolved policy + ambiguity; +- every normalization, enumeration, partition, merge, or exclusion used to + derive `Required`, with its equality or containment proof; - every discovered axis and its possible supported values/classes; -- the proof method establishing coverage; +- the proof method and `Covered` predicate; +- the checked `Required ⊆ Covered` closure argument; - the obligation and premise applicability domains used by that proof; - generated artifact identities or generator theorem; - excluded combinations and their enforcement; @@ -298,5 +338,6 @@ For each audit, report: - remaining assumptions, unknowns, and unsupported tool features; - triggers requiring re-audit. -Mark the audit `UNPROVED` if a shippable supported combination is neither -individually audited nor covered by a valid universal argument. +Mark the audit `UNPROVED` if `Required` is not justified or if a required +shippable combination is neither individually audited nor covered by a valid +universal argument. diff --git a/skills/unsafe-rust/references/proof-obligations.md b/skills/unsafe-rust/references/proof-obligations.md index 8880ec3ca9..b66660174c 100644 --- a/skills/unsafe-rust/references/proof-obligations.md +++ b/skills/unsafe-rust/references/proof-obligations.md @@ -47,14 +47,9 @@ supplies or consumes a safety contract as an obligation site. Follow each obligation until it reaches checked local facts, named invariants, authoritative axioms, or explicit TCB entries. -Undefined behavior is a property of an entire execution. If any event in an -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. Such a UB-containing execution cannot also -establish a defined behavioral observation; apply the exact witness rule in -`SKILL.md`. +Apply the quantifier-sensitive verdict certificates in `SKILL.md` when a +derivation fails or produces a counterexample. Do not confuse failure of a +universal proof with proof of an existential refutation. ## Qualify Applicability @@ -78,9 +73,12 @@ 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. +Derive the required toolchain/configuration projection and every transformation +of that projection under +[Recover the required supported set](configurations-and-generated-code.md#recover-the-required-supported-set), +then carry it through every premise and case lemma below. The domain covered by +a derivation is the intersection of the applicability domains of every premise +it consumes; the union of valid case lemmas must contain the required domain. A documented Rust guarantee from version `R` may support a later stable version only when an exact Rust backwards-compatibility commitment preserves that exact @@ -108,6 +106,20 @@ state an audit cutoff and later-release re-audit trigger. A compatibility premise about abstract semantics does not prove correctness of future compiler binaries. +Before issuing any affirmative result spanning multiple Rust releases, record +the exact required release predicate and one coverage basis: + +- an applicable parametric derivation over the whole predicate; +- an exhaustive partition with applicable premises for every class or member; + or +- an exact proposition-preserving backwards-compatibility premise whose domain + covers every later release claimed. + +Endpoint documentation, sparse version samples, an earliest supported release, +and an audit cutoff do not prove the releases between them. If the coverage +basis does not contain the claimed release predicate, narrow the proved region +and leave the remainder `UNPROVED`. + ## Separate Kinds of Premises Classify every premise: @@ -357,6 +369,16 @@ derivation is established, the obligation remains unproved. Distinguish “this audit did not complete a proof” from the stronger claim that authoritative documentation cannot support one. +When a universal soundness derivation does not close, separately ask whether +the established facts close an existential refutation. Identify a valid +in-scope use or execution, prove reachability of the relevant operation or +semantic event, prove its exact required safety proposition false there, and +trace that failure to the applicable authoritative or explicitly trusted UB +consequence. If every link is proved, apply `UNSOUND`; if any link is absent, +the failed universal obligation remains `UNPROVED`. Do not demand a fact about +every input to establish one existential witness, and do not infer a witness +merely from the absence of a universal proof. + ## Review a Proof For each proof: @@ -378,7 +400,9 @@ For each proof: the cited facts entail. 8. Record every missing implication so it cannot be forgotten, apply [Search for indirect derivations](#search-for-indirect-derivations), and - report `UNPROVED` if a required implication remains absent. + apply the verdict certificate in `SKILL.md`: report `UNPROVED` if a required + implication remains absent and no existential refutation closes, or the + applicable refutation verdict if one does. If validation requires a material derivation absent from the existing safety comment, include that reconstructed derivation—or the smallest missing @@ -391,10 +415,8 @@ 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 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. +- If the reconstruction fails, leave the obligation unproved unless it instead + closes one of the existential certificates in `SKILL.md`. When changes are authorized, update the adjacent proof rather than leaving the reconstructed reasoning only in the review. A canonical checked proof or named diff --git a/skills/unsafe-rust/references/tcb-and-evidence.md b/skills/unsafe-rust/references/tcb-and-evidence.md index 8e1be81aa4..ba5efcff73 100644 --- a/skills/unsafe-rust/references/tcb-and-evidence.md +++ b/skills/unsafe-rust/references/tcb-and-evidence.md @@ -192,8 +192,9 @@ is not unconditional Rust soundness. Classify evidence by what the exact result proves: -- A concrete failing execution can refute a universal claim when the execution - is in scope and valid. +- A concrete execution refutes only a claim whose applicable verdict certificate + it satisfies. A valid in-scope execution with a complete UB certificate can + refute soundness; a postcondition refutation must be UB-free as a whole. - A clean sampled test, fuzzing run, sanitizer run, interpreter execution, or stress run usually establishes only that the explored executions did not trigger the modeled failure.