diff --git a/maintainers/unsafe-rust-skill-design.md b/maintainers/unsafe-rust-skill-design.md index 1ee88fb0a8..1f592c1d90 100644 --- a/maintainers/unsafe-rust-skill-design.md +++ b/maintainers/unsafe-rust-skill-design.md @@ -170,12 +170,20 @@ 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. +using a conservative audit domain requires containment. Claims that predicates +are strict subsets or incomparable additionally require the corresponding +nonmembership witnesses; preserving formulas is not itself a proof of their +relationship. 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`. +derivations. Let `Required` denote the exact full cases quantified by the +theorem—without losing relevant artifact, configuration, input, state, or +execution dimensions—and `Covered` the cases whose semantic obligations have +complete applicable proofs. An affirmative result requires +`Required ⊆ Covered`. A projection may organize a local argument but cannot +silently redefine claim-level coverage; the lemma must cover every required +case in each omitted-dimension fiber, parametrically or by proving the omitted +dimensions irrelevant, and must restore the full case before closure. 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 @@ -189,6 +197,23 @@ 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. +### Proof compression must be reversible + +Compact proofs and canonical entries are necessary for usable reports, but +compression may not hide a material inference. A reviewer must be able to start +at every certified conclusion and recover each intermediate proposition, +premise, applicability domain, source, and entailment step. A broad phrase such +as “cfg semantics,” a page-level citation, or a named TCB entry supplies only +the exact propositions the proof states and the source actually guarantees. + +The runtime package therefore uses the existing obligation ledger and proof +prose for a final reverse-trace pass. It does not require an explicit graph or a +second artifact. This is load-bearing because an audit can identify the right +code path and reach the right high-level verdict while still lacking one +semantic operator, numeric-domain fact, or stage transition needed to certify +that verdict. Such a result is not proof-grade merely because the omitted fact +is true or appears somewhere in an allowed document. + ### Producer contracts retain their quantifiers A precondition on one constructor, conversion, deserializer, FFI ingress, or @@ -250,7 +275,9 @@ 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. +the same false obligation or compute a maximal positive remainder unless that +regional theorem is requested. Any regional claim it does make must retain the +full relevant case dimensions and prove its stated boundary exactly. ### Configuration coverage is universal but need not be enumerative @@ -269,8 +296,19 @@ 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. +The claim-relevant mapping is not always an atomic function from one input to +one output. Generators and build scripts execute ordered, fallible operations, +may leave partial effects, may terminate before later selector handling, and +may be cached or rerun under a separate invalidation contract. Build tools then +interpret emitted directives or artifacts before the compiler selects source. +Collapsing this staged relation to its successful endpoint can make true but +unproved claims about rejection, reachability, or freshness. + +The runtime procedure therefore proves every stage, path, and exit that can +change the theorem domain, a consumed premise, the selected artifact/source, +reachability, or an in-scope postcondition. It still permits an exact-output +audit or a theorem about every supported output; the staged proof determines +when either result applies without requiring irrelevant build behavior. ### Soundness and promised behavior are separate obligations @@ -344,13 +382,15 @@ Nothing in the runtime package links to `maintainers/`. - [`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. + contains supported-domain recovery and transformation, staged build and + generation relations, configuration closure, 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. + contains scope, obligation-ledger, evidence reconciliation, finding, verdict, + and preservation rules. - `assets/` contains copyable audit artifacts, not additional hidden instructions. - Future evaluations belong outside the installable package. @@ -380,12 +420,12 @@ column records candidate semantic evaluation scenarios, not execution results. | 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 | +| D09 — Recover the full theorem domain losslessly and carry applicability through every derivation | A range, union, condition, input, or moving policy is contracted or projected away; a false set relationship or out-of-domain premise is then used to assert closure | Preserve the full case tuple and source predicates; use relation-appropriate containment/equality/witness certificates; 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 — nonlinear incomparable policies plus a configuration/input product and 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 | +| D14 — Prove the staged build/generation relation and shipped output | Endpoint mapping hides earlier failure, partial effects, stale reuse, or unsafe expansion | Follow every claim-relevant ordered operation and exit through emitted effects and tool interpretation; identify an exact output or prove the generator property | [Build and generation](../skills/unsafe-rust/references/configurations-and-generated-code.md#prove-build-and-generation-pipelines); [macros](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#audit-macros-and-hidden-apis) | EV14 — fallible ordered build directives plus caller-token-dependent proc-macro output | | 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 | @@ -394,6 +434,7 @@ column records candidate semantic evaluation scenarios, not execution results. | 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 | +| D23 — Require reversible derivation closure before verdict certification | The report reaches the right endpoint while silently omitting a semantic operator, numeric-domain fact, stage transition, applicability restriction, or citation inventory entry | Reverse-trace every conclusion through explicit material inferences and reconcile every semantic premise with its exact authority or TCB entry; reuse ordinary proof prose and the obligation ledger | [Proof workflow](../skills/unsafe-rust/SKILL.md#follow-the-proof-workflow); [reviewable derivations](../skills/unsafe-rust/references/proof-obligations.md#make-every-derivation-reviewable); [evidence reconciliation](../skills/unsafe-rust/references/audit-reporting.md#reconcile-derivations-and-evidence) | EV23 — locally correct proof with one unstated composite-predicate premise and one invoked-but-uncited integer-domain premise | ## Explicit Non-goals @@ -407,6 +448,8 @@ The runtime skill does not: complete; - require enumeration of every client program witnessing one already-identified false obligation; +- require a maximal positive-region characterization after a complete + existential refutation unless that separate regional theorem is in scope; - require an explicit safety-dependency graph; - require a second proof-record schema beyond ordinary contracts, invariants, obligation coverage, and audit artifacts; @@ -503,20 +546,24 @@ 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 +- lossless full-case theorem-domain recovery, including symbolic ranges, + unions, conditions, configuration/input products, relation-appropriate + witnesses, justified projections and enumerations, `Required ⊆ Covered`, + and multi-release premise applicability; +- authority checking, reverse-traceable derivations, premise-to-citation + reconciliation, 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; + configurations, and staged generated behavior with ordered fallible exits, + tool interpretation, partial effects, and freshness where applicable; - 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 +- reporting behavior that preserves exact scope, proves every relationship it + asserts, and exposes proof-artifact defects without imposing a separate + graph or exhaustive inventory of equivalent client witnesses; and - the abstraction-design firewall, minimum-capability modeling, consequential candidate comparison, compatibility/migration analysis, rejection of proposal laundering, and fresh audit of implemented changes. diff --git a/skills/unsafe-rust/SKILL.md b/skills/unsafe-rust/SKILL.md index 7c60a97623..89ae055778 100644 --- a/skills/unsafe-rust/SKILL.md +++ b/skills/unsafe-rust/SKILL.md @@ -40,11 +40,17 @@ 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. +Before proving the claim body or issuing a full verdict, derive the exact +domain quantified by the claim. Let a `case` retain every relevant dimension of +one valid use or execution: artifact, toolchain, configuration, input, state, +time, and any other dimension on which an obligation or premise can vary. Let +`Required(case)` denote the cases the claim requires and `Covered(case)` hold +exactly where every obligation the claim requires for that case has a complete +derivation from applicable premises. A local argument may project onto fewer +dimensions only when it proves the lemma for every required case in each +omitted-dimension fiber—parametrically or by proving those dimensions +irrelevant—and must restore the full case before claim-level closure. + 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. @@ -57,10 +63,15 @@ regions in which different obligations happened to be proved. 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`. +- Treat every asserted set relationship, normalization, enumeration, + partition, exclusion, and policy merge as a proof step. Prove the definition + of the exact relation asserted. For example, `A = B` needs `A ⊆ B` and + `B ⊆ A`; `A ⊊ B` needs `A ⊆ B` and a witness `w ∈ B \ A`; + incomparability needs witnesses `a ∈ A \ B` and `b ∈ B \ A`, with each + membership and nonmembership proved. Equivalent symbolic derivations are + acceptable, but required witnesses must remain explicit. Prove 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 @@ -74,7 +85,7 @@ regions in which different obligations happened to be proved. documentation applicable between samples. Apply -[configuration closure](references/configurations-and-generated-code.md#recover-the-required-supported-set) +[configuration recovery](references/configurations-and-generated-code.md#recover-the-required-supported-set) to derive supported compilation cases and prove every transformation of that predicate. @@ -82,9 +93,11 @@ predicate. - Bottom out Rust-language and standard-library facts in exact applicable text from versioned Rust Reference or standard-library documentation. -- Quote and link the smallest sufficient set of passages whose propositions, - together with justified inference steps, entail the fact. Open each citation - and verify its wording, qualifications, version, and scope. +- Quote and link the smallest sufficient set of passages whose explicitly + stated propositions, together with justified inference steps, entail the + fact. Open each citation and verify its wording, qualifications, version, and + scope. A page, allowlist entry, broad label such as “cfg semantics,” or nearby + cited clause does not supply a material proposition the proof never states. - 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. @@ -149,21 +162,31 @@ documentation gap and suggest an upstream improvement when appropriate. 1. **Frame the claim.** Record the artifact identity, exact scope, valid uses or 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 required domain. -4. **State every obligation.** Obtain each controlling contract, decompose it - literally, and state the exact proposition and applicability to prove. -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. -6. **Close and challenge.** Give every literal contract clause and safe surface - a disposition, establish domain closure, and try to falsify the domain +2. **Frame the full case domain.** Identify every relevant dimension and + preserve the controlling expressions, sources, candidate relationships, and + unresolved conflicts. State the proposed `Required` domain and how proof + cases will retain every dimension. +3. **Inventory surfaces and transformations.** Enumerate every in-scope safe + and unsafe API surface, obligation site, invariant + producer/transition/consumer, and each material stage and alternative exit + by which build or generation inputs can affect the theorem domain, a + consumed premise, shipped artifacts or selected source, reachability, or an + in-scope postcondition. +4. **State atomic obligations and premises.** Obtain each controlling contract, + decompose it literally, and state the exact proposition and applicability to + prove. Classify every material premise and identify its exact source. +5. **Construct the derivation.** Derive `Required`, every asserted domain + relationship, and every claim conjunct from checked local facts, named + invariants, applicable authoritative axioms, tool-derived theorems, or + explicit TCB entries. Unfold definitions and composite transformations; + preserve material operation order and alternative exits; seek indirect + multi-premise derivations; and justify every intermediate inference. +6. **Close, lint, and challenge.** Give every literal contract clause and safe + surface a disposition and establish domain closure. Reverse-trace each + conclusion used by a verdict or regional result through every material + inference to explicit, applicable premises; reconcile every Rust premise + with its checked quotation and link; and ensure no later-stage fact is + consumed on a path that exited earlier. Then 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. @@ -257,6 +280,13 @@ 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. +An existential certificate closes the universal verdict but does not excuse +omitting another in-scope surface, operation, contract clause, or mandatory +postcondition. Continue the inventory and give each independent obligation a +disposition. Do not claim that a proved or affected region is exact or maximal +unless its full case-domain equality is established; maximal positive remainder +characterization is required only when the audit scope requests it. + 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 diff --git a/skills/unsafe-rust/assets/tcb-audit-log-template.md b/skills/unsafe-rust/assets/tcb-audit-log-template.md index 0347294827..a79f3f880d 100644 --- a/skills/unsafe-rust/assets/tcb-audit-log-template.md +++ b/skills/unsafe-rust/assets/tcb-audit-log-template.md @@ -78,6 +78,9 @@ support.>` ## Review Attestation +- [ ] The audit's material semantic premises were reconciled against this + index; every Rust axiom or admitted proposition it consumes appears with + its exact source and applicability. - [ ] Every consumed entry has an exact proposition rather than a vague trust statement. - [ ] No entry merely assumes an in-scope conclusion or trusts code the declared 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 76d0678280..a3ef0c8619 100644 --- a/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md +++ b/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md @@ -67,7 +67,7 @@ and record every additional language-reachable surface in the table above. - [ ] safe trait methods and caller-provided implementations; - [ ] macros and macro-generated APIs; - [ ] reexports and configuration-specific APIs; -- [ ] language-reachable `#[doc(hidden)]` safe items. +- [ ] language-reachable `#[doc(hidden)]` safe items; - [ ] associated items, safe free functions/statics, callbacks, FFI entrypoints, blanket/default/auto-trait behavior, operators, and destruction whenever language-reachable or semantically relevant. @@ -80,7 +80,7 @@ and record every additional language-reachable surface in the table above. ## Obligation Ledger -| Obligation ID | Source/API | Exact proposition | Required domain | Premises and their applicability | Covered domain/cases | Proof location | Reviewer | Status | +| Obligation ID | Source/API | Exact proposition | Required domain | Derivation, material premises, and their applicability | Covered domain/cases | Proof location | Reviewer | Status | |---|---|---|---|---|---|---|---|---| | `` | `` | `` | `` | `` | `` | `` | `` | `` | @@ -88,23 +88,40 @@ and record every additional language-reachable surface in the table above. ### Required Domain Recovery -| Step ID | Controlling source expression or prior predicate | Derived predicate/inventory/partition | Relation to prove (write symbolically) | Equality/containment evidence | Status | +| Step ID | Controlling source expression or prior predicate | Derived predicate/inventory/partition | Relation to prove (write symbolically) | Required certificate: containments/witnesses/derivation | Status | |---|---|---|---|---|---| -| `` | `` | `` | `` | `` | `` | +| `` | `` | `` | `` | `` | `` | - **Audit cutoff:** `` - **Exact `Required` predicate:** `` +- **Configuration projection:** `` - **Policy conflicts/authorized resolution:** `` - **Unresolved domain:** `` +### Build and Generation Pipeline + +`` + +| Stage ID | Input/state region and predecessor | Ordered operation or transformation | Successful output/effect | Alternative exit and partial effects | Authority/TCB and applicability | Consumer | +|---|---|---|---|---|---|---| +| `` | `` | `` | `` | `` | `` | `` | + +- **Freshness/invalidation:** `` + ### Covered Domain - **Discovered axes:** `` -- **Exact `Covered` predicate:** `` +- **Configuration-fiber proof:** `` +- **Exact full-case `Covered` predicate:** `` - **Coverage proof:** `` - **Closure certificate:** `` - **Enforced exclusions:** `` - **Sampled/tested configurations:** `` -- **Uncovered configurations:** `` +- **Uncovered full cases/configurations:** `` ## TCB Summary @@ -211,15 +228,23 @@ explicitly excluded region. Explain enforcement of exclusions.>` ## Final Attestation - [ ] Every in-scope obligation has a status. -- [ ] Every controlling domain expression is preserved, and every normalization, - enumeration, partition, merge, or exclusion has its required equality or - containment proof. +- [ ] Every conclusion used by a verdict or regional result and every claimed + set relationship satisfies [Make every derivation + reviewable](../references/proof-obligations.md#make-every-derivation-reviewable). +- [ ] Every controlling domain expression is preserved, and every asserted set + relationship, normalization, enumeration, partition, merge, or exclusion + has the certificate required by its exact relation. +- [ ] Every materially relevant build/generation path records required order, + exits, and partial progress and proves each consumed tool-interpretation, + output, and freshness proposition; no later-stage fact is used on a path + that exited earlier. - [ ] 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 consumed citation and TCB entry was independently verified. +- [ ] Every material semantic premise appears in the authority/TCB inventory, + and every consumed citation and TCB entry was independently verified. - [ ] Every consumed TCB entry supporting `PROVED` has an accepted human disposition. - [ ] Every mandatory documented postcondition was reviewed in addition to UB diff --git a/skills/unsafe-rust/references/api-boundaries-and-evolution.md b/skills/unsafe-rust/references/api-boundaries-and-evolution.md index 1609e2dc8a..8a27c298f6 100644 --- a/skills/unsafe-rust/references/api-boundaries-and-evolution.md +++ b/skills/unsafe-rust/references/api-boundaries-and-evolution.md @@ -186,7 +186,7 @@ output depends on: - downstream code into which the macro expands. Inspect expansions to discover API and caller obligations. Then apply -[Audit generated and expanded code](configurations-and-generated-code.md#audit-generated-and-expanded-code) +[Prove build and generation pipelines](configurations-and-generated-code.md#prove-build-and-generation-pipelines) to prove closure over every supported accepted input, output, and configuration. Include generated public APIs in the same safe/unsafe surface audit as handwritten items. diff --git a/skills/unsafe-rust/references/audit-reporting.md b/skills/unsafe-rust/references/audit-reporting.md index c895a453de..309c3ae271 100644 --- a/skills/unsafe-rust/references/audit-reporting.md +++ b/skills/unsafe-rust/references/audit-reporting.md @@ -4,6 +4,7 @@ - [Freeze the audit claim](#freeze-the-audit-claim) - [Maintain an obligation ledger](#maintain-an-obligation-ledger) +- [Reconcile derivations and evidence](#reconcile-derivations-and-evidence) - [Aggregate verdicts](#aggregate-verdicts) - [Write actionable findings](#write-actionable-findings) - [Deliver a complete report](#deliver-a-complete-report) @@ -48,11 +49,17 @@ 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; +- the appropriate certificate for every asserted set relationship and domain + transformation consumed; - proof location; - reviewer verification; - status and finding link. +A row may cite a canonical subproof rather than repeat it, but neither a row nor +a proof name may hide a material inference. The record must let a reviewer +reverse-trace the obligation through every intermediate proposition to its +classified and applicable premises. + Include obligations created by: - unsafe operations and unsafe API calls; @@ -75,6 +82,17 @@ The ledger complements rather than replaces the proof workflow in follow changed propositions to every consumer; compiler-marked unsafe locations and textual diffs are only discovery starting points. +## Reconcile Derivations and Evidence + +Apply [Make every derivation +reviewable](proof-obligations.md#make-every-derivation-reviewable) before +certifying any verdict or regional result. In a persistent report, ensure the +obligation ledger and its canonical proofs expose that derivation, then +reconcile every material semantic premise they use with the report's authority +and TCB inventories. A valid fact found only by the reviewer may support a +reconstructed implementation proof, but record the deficient report or safety +comment rather than silently repairing its proof artifact. + ## Aggregate Verdicts Use the verdict definitions in `SKILL.md` for individual obligations and the @@ -95,6 +113,13 @@ 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`. +A completed existential refutation fixes its universal verdict but does not +erase independent obligations elsewhere in scope. Continue the surface and +site inventory. Report a positive or affected regional partition only at the +granularity and completeness actually proved; do not imply maximality unless +the task requests it and equality with the exact full-case region is +established. + Place qualifications in the theorem, not in vague prose. Use: > PROVED for `` over ``, relative to TCB @@ -172,10 +197,11 @@ A complete audit report contains: proofs/findings rather than duplicating them. Include material reconstructed proofs missing from the reviewed proof artifacts. 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. + expressions, full-case symbolic `Required`, its `Required_cfg` projection, + set-relationship and transformation certificates, audit cutoff, axes, staged + build/generation relation, configuration-fiber proofs, `Covered`, claim + closure, 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 192a19c973..5790ced732 100644 --- a/skills/unsafe-rust/references/configurations-and-generated-code.md +++ b/skills/unsafe-rust/references/configurations-and-generated-code.md @@ -5,7 +5,7 @@ - [Recover the required supported set](#recover-the-required-supported-set) - [Discover configuration axes](#discover-configuration-axes) - [Prove coverage of the recovered set](#prove-coverage-of-the-recovered-set) -- [Audit generated and expanded code](#audit-generated-and-expanded-code) +- [Prove build and generation pipelines](#prove-build-and-generation-pipelines) - [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) @@ -13,6 +13,13 @@ ## Recover the Required Supported Set +This reference helps recover the configuration projection of the full +`Required(case)` domain defined in `SKILL.md`. Define +`Required_cfg(configuration)` to hold when at least one full required case has +that configuration. This projection organizes support-policy and case proofs; +it does not replace inputs, states, executions, or other dimensions of +claim-level `Required` and `Covered`. + 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, @@ -38,28 +45,32 @@ 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, 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: +predicate, do not silently select the narrowest interpretation. Apply the +domain-recovery choices in `SKILL.md` to the full case domain: obtain an +authorized project decision, construct an explicit conservative `Required` +domain containing every materially supported candidate domain, or report +regional results and leave the combined claim `UNPROVED`. Then project that +chosen full domain to `Required_cfg`. Do not call a conservative audit domain a +newly inferred project promise. If a shippable configuration is exposed and no +applicable contract clearly excludes it, include its possible shippable full +cases in the unresolved conservative domain until project authority resolves +its status; successful compilation alone still does not define the support +promise. + +Every transformation from controlling expressions to the full `Required` +domain and its `Required_cfg` projection 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`; +- a conservative audit domain requires + `Candidate_i(case) ⊆ Required(case)` for every materially supported candidate + full-case domain; the projected containment follows but cannot substitute for + this full-case proof; - 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. +- a configuration partition used for proof requires `Required_cfg` to be + contained in the union of the proved configuration 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 @@ -69,13 +80,8 @@ 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 `Required` to a single MSRV. It may be finite, +rather than collapsing `Required_cfg` 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. A cutoff identifies when a dynamic predicate was recovered; it neither enumerates the toolchains before that date @@ -137,9 +143,12 @@ reference. ## Prove Coverage of the Recovered Set -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. +Every full required case must reach its exact audited artifact, selected source, +or other in-scope build outcome and satisfy the applicable semantic obligations. +A proved enforced exclusion may establish that a candidate combination has no +shippable full case; it does not cover any full case that remains in `Required`. +A CI matrix, sample of targets, or pairwise feature test establishes neither +domain recovery nor universal semantic coverage. Avoid Cartesian-product enumeration when an abstract proof is clearer. Valid coverage arguments include: @@ -148,7 +157,7 @@ coverage arguments include: - 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 - `Required`; + `Required_cfg`; - prove a generator emits only members of a finite audited family; - prove independent lemmas for axes, then prove their assumptions remain independent under composition; @@ -159,22 +168,77 @@ alone does not prove their combination; target facts can change layout, atomic availability, calling convention, or macro expansion on which another feature depends. -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 is `Covered`, that `Required ⊆ Covered`, and that their assumptions remain -true where regions interact. +Use `Required_cfg` only as an index into full-case proofs. Attach a +configuration-domain predicate to every obligation, premise, and coverage +lemma. For each required configuration, prove the relevant build, artifact, +source-selection, and semantic lemmas for every full required case in its +omitted-dimension fiber, parametrically or by an exhaustive partition. A unary +configuration lemma may assert one exact artifact or source only after proving +uniqueness or independence from the omitted dimensions. 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 `Required_cfg`, reattach every +other relevant case dimension, and prove their assumptions remain true where +regions interact. Use the resulting full-case lemmas in claim-level `Covered`; +do not substitute the configuration projection for it. 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. +conditional, or cross-axis full 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 contracts remain separate obligations. -## Audit Generated and Expanded Code +## Prove Build and Generation Pipelines + +Model claim-relevant build and generation machinery as a staged relation, not +merely an endpoint mapping: + +```text +policy and build inputs + -> ordered local operations, effects, and exits + -> emitted directives, metadata, source, or objects + -> build-tool/compiler interpretation + -> selected shipped artifact and source +``` + +Include an operation, exit, or effect when it can change the theorem domain, an +applicable or consumed premise, the selected or shipped artifact/source, +semantic reachability, or an in-scope postcondition. Group paths only after +proving them equivalent for every such proposition. Audit additional build +behavior when the requested theorem includes it. + +Derive the material stages from the artifact. For each stage, prove: + +- the exhaustive input/state partition on which it is reached; +- the order of operations whenever failure, partial progress, caching, or + invalidation can affect later stages; +- every claim-relevant fallible operation and alternative exit, including + which later operations are not reached and which earlier effects remain; +- a complete successful-output/effect relation sufficient for every downstream + proposition: exact value, cardinality, identity, or ordering when consumed or + asserted, otherwise a proved property covering every possible output; +- the distinction between local source behavior, build-tool or compiler + behavior, and any admitted environmental behavior; and +- that each output consumed by a later stage was actually established on that + path and within the premise's applicability. + +Classify outcomes according to the controlling contract. A policy rejection, +an infrastructure or tool failure, and successful production of an excluded or +supported artifact can all produce “no library was compiled” or another common +endpoint without being the same proof case. Do not say later selector, +generator, or compiler handling occurred on a path that exited earlier. + +Account for freshness when a changing input can reuse prior build state. Prove +the exact invalidation, rerun, cache-key, or identity relation consumed by the +claim rather than assuming the generator is re-executed with current inputs. + +When conditional source is selected, evaluate each material predicate from its +proved leaf options through every composite operator to the attribute or other +selection effect. Cite the applicable Rust semantics for those operators and +effects; a TCB entry mapping an external input to a leaf option does not also +supply Rust predicate semantics unless it explicitly says so. Treat generated code as shipped source. Capture enough information to reproduce or identify: @@ -207,9 +271,9 @@ unsafe code behind an invocation usable from safe context must be sound for every accepted safe invocation. Build scripts may emit `cfg` values, link directives, environment values, or -generated source. Include both their output and every supported path that can -produce different output. Include proc-macro and build dependencies in the TCB -or recursive audit as appropriate. +generated source. Prove their complete claim-relevant staged relation as above. +Include proc-macro and build dependencies in the TCB or recursive audit as +appropriate. ## Audit Targets, SIMD, and Concurrency @@ -310,26 +374,30 @@ 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 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. +A compilation or linker option belongs to `Required_cfg` 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: - every controlling support predicate and its exact source; -- the symbolic `Required` predicate, audit cutoff, and any unresolved policy +- the symbolic `Required_cfg` projection, its relationship to the full + `Required(case)` domain, the 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 asserted set relationship, normalization, enumeration, partition, + merge, or exclusion used to derive the full `Required` domain and its + `Required_cfg` projection, with its relation-appropriate certificate; - every discovered axis and its possible supported values/classes; -- the proof method and `Covered` predicate; -- the checked `Required ⊆ Covered` closure argument; +- the staged build/generation relation, including ordered effects, alternative + exits, tool interpretation, and freshness where applicable; +- the proof method for every required configuration fiber and its composition + into the full-case `Required ⊆ Covered` claim argument; - the obligation and premise applicability domains used by that proof; - generated artifact identities or generator theorem; - excluded combinations and their enforcement; @@ -338,6 +406,6 @@ For each audit, report: - remaining assumptions, unknowns, and unsupported tool features; - triggers requiring re-audit. -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. +Mark the audit `UNPROVED` if `Required_cfg` is not justified, a required +configuration fiber lacks a complete full-case argument, or any required full +case remains outside `Covered`. diff --git a/skills/unsafe-rust/references/proof-obligations.md b/skills/unsafe-rust/references/proof-obligations.md index b66660174c..815c02ccfa 100644 --- a/skills/unsafe-rust/references/proof-obligations.md +++ b/skills/unsafe-rust/references/proof-obligations.md @@ -5,6 +5,7 @@ - [Form the theorem](#form-the-theorem) - [Qualify applicability](#qualify-applicability) - [Separate kinds of premises](#separate-kinds-of-premises) +- [Make every derivation reviewable](#make-every-derivation-reviewable) - [Write safety documentation](#write-safety-documentation) - [Write local safety proofs](#write-local-safety-proofs) - [Carry invariants locally](#carry-invariants-locally) @@ -178,6 +179,51 @@ Likewise, distinguish: - obligations transferred to a returned pointer, reference, guard, token, or caller. +## Make Every Derivation Reviewable + +A proof may be compact, but it must be reversible by a reviewer. A premise, +intermediate proposition, or applicability restriction is material when +deleting it leaves the remaining explicit premises insufficient to entail a +certified conclusion; a countermodel may demonstrate that insufficiency. State +every such component. Justify each transition unless its entailment is directly +reviewable from the stated premises. Even a direct transition may not import an +unstated Rust, library, tool, environmental, or TCB premise. Omit only immediate +source syntax or purely logical rearrangement of already explicit premises. + +Do not hide a material component behind a name such as “layout rules,” “cfg +semantics,” “the build mapping,” or “the type guarantees it.” A citation verifies +only the proposition the proof extracts from it; an allowlisted page or another +clause on the same page does not silently fill an unstated premise. Unfold +composite behavior to the clauses actually used. When build or generation +stages are relevant, apply +[Prove build and generation pipelines](configurations-and-generated-code.md#prove-build-and-generation-pipelines). + +The ordinary proof prose or obligation ledger may carry this information. Do +not create a separate graph when the existing proof is already +reverse-traceable. Before certifying `PROVED`, `UNSOUND`, `CONTRACT-BROKEN`, or +any regional result: + +1. start at every conclusion used by the certificate and recover its full-case + applicability, every premise and intermediate proposition, and why they + entail the conclusion; +2. classify each premise as a checked source fact, mathematical step, named + invariant, Rust axiom, tool theorem, or TCB entry; check source facts and + invariants against their exact locations, dataflow, material operation order, + and alternative exits; +3. check material, non-immediate mathematical and logical steps by their + explicit derivations or witnesses; they need no Rust citation; +4. check every Rust semantic premise against its recorded exact versioned + quotation and link; +5. check every other semantic premise against its verified tool theorem or + accepted TCB entry; +6. ensure no projection, shorthand, page-level citation, or later-stage result + silently supplies a missing premise; and +7. trace forward through every relevant exit to prove the postconditions and + invariants consumed later. + +If a required component remains absent, remove every conclusion that depends on +it and apply the exact verdict certificate. + ## Write Safety Documentation Give every unsafe function, trait, impl, field, macro boundary, and other unsafe @@ -398,7 +444,10 @@ For each proof: 6. Verify every postcondition used downstream. 7. Search for circularity, vacuity, hidden trust, and stronger conclusions than the cited facts entail. -8. Record every missing implication so it cannot be forgotten, apply +8. Apply [Make every derivation reviewable](#make-every-derivation-reviewable) + to every conclusion used by a verdict or regional result and every claimed + set relationship. +9. Record every missing implication so it cannot be forgotten, apply [Search for indirect derivations](#search-for-indirect-derivations), and apply the verdict certificate in `SKILL.md`: report `UNPROVED` if a required implication remains absent and no existential refutation closes, or the @@ -406,10 +455,9 @@ For each proof: If validation requires a material derivation absent from the existing safety comment, include that reconstructed derivation—or the smallest missing -portion—in the review. A derivation is material when it supplies a necessary -logical bridge that is neither stated nor an immediate syntactic or -type-enforced fact visible at the proof site. Give its citations, -applicability, and relationship to the required preconditions and +portion—in the review. Apply the material-component definition in +[Make every derivation reviewable](#make-every-derivation-reviewable). Give its +citations, applicability, and relationship to the required preconditions and postconditions. Report the implementation result separately from the deficient proof artifact: