Revise unsafe Rust skill around domain and verdict certificates

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:
 

skills/unsafe-rust/assets/tcb-audit-log-template.md

@@ -8,7 +8,8 @@
 - **Source snapshot:** `<repository + revision/digest>`
 - **Generated artifacts:** `<identities/digests>`
 - **Rust/toolchain scope:** `<versions>`
-- **Supported configuration predicate:** `<definition or link>`
+- **Supported configuration predicate:** `<certified domain ID/link in audit
+  report>`
 - **Theorem(s) supported:** `<exact soundness, postcondition, binary, or
   application claims>`
 - **Owner/reviewer:** `<names or roles>`
@@ -36,8 +37,8 @@ support.>`
 - **Disposition:** `<accepted / rejected / pending / superseded>`
 - **Exact proposition:** `<the smallest proposition accepted without further
   in-scope proof>`
-- **Quantification and scope:** `<inputs, executions, versions, targets,
-  configurations, APIs, and time interval>`
+- **Quantification and scope:** `<inputs, executions, exact release/version
+  regions, targets, configurations, APIs, and time interval>`
 - **Exact identity:** `<document URL + version, package + version/source,
   revision/digest, binary, model, tool, agreement, or environment>`
 - **Source/contract:** `<narrow link, document section, agreement, audit, or
@@ -88,6 +89,9 @@ support.>`
       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.

skills/unsafe-rust/assets/unsafe-code-audit-report-template.md

@@ -2,27 +2,18 @@
 
 ## Claims and Verdicts
 
-- **Soundness claim:** `<exact source-level or binary-level absence-of-UB theorem>`
-- **Soundness verdict:** `<PROVED / UNPROVED / UNSOUND; split by scope or
-  configuration when needed>`
-- **Documented-postcondition claim:** `<exact contracts in scope>`
-- **Documented-postcondition verdict:** `<PROVED / UNPROVED /
-  CONTRACT-BROKEN; split by contract, scope, or configuration when needed>`
+| Claim ID | Exact theorem | Required-domain ID | Verdict | Certificate/proof/finding | TCB and qualification |
+|---|---|---|---|---|---|
+| `<CLAIM-SOUND-...>` | `<source- or binary-level absence-of-UB theorem>` | `<DOMAIN-...>` | `<PROVED / UNPROVED / UNSOUND>` | `<closure proof or finding IDs>` | `<TCB + assumptions>` |
+| `<CLAIM-POST-...>` | `<documented postcondition>` | `<DOMAIN-...>` | `<PROVED / UNPROVED / CONTRACT-BROKEN>` | `<closure proof or finding IDs>` | `<TCB + assumptions>` |
+| `<CLAIM-APP-...>` | `<conditional deployment/security/probabilistic theorem, or omit>` | `<DOMAIN-...>` | `<exact qualified result>` | `<proof/finding IDs>` | `<explicit conditional TCB>` |
+
 - **Combined mandatory result:** `<PROVED only if every in-scope soundness and
   mandatory documented-postcondition obligation is proved; otherwise list all
   applicable component verdicts and finding IDs>`
-- **Conditional application claim:** `<deployment/security/probabilistic theorem,
-  or none>`
-- **Conditional application result:** `<exact qualified result and finding IDs;
-  do not present it as unconditional Rust soundness>`
 - **Scope:** `<APIs/modules/packages/binaries>`
-- **Supported configuration predicate:** `<exact definition or link>`
-- **Support-policy sources/conflicts:** `<controlling sources, ambiguity,
-  authorized resolution or conservative audit superset, and audit cutoff>`
 - **TCB log:** `<ID/revision/link>`
 - **Skill revision:** `<unsafe-rust revision>`
-- **Qualification:** `<exact conditional assumptions; “none beyond stated TCB”
-  if appropriate>`
 
 ## Audited Snapshot
 
@@ -93,14 +84,33 @@ and record every additional language-reachable surface in the table above.
 |---|---|---|---|---|---|---|---|---|
 | `<OBL-...>` | `<location>` | `<goal>` | `<required applicability>` | `<facts/invariants/TCB + domains>` | `<scope/partition>` | `<link>` | `<identity>` | `<status>` |
 
-## 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 |
+|---|---|---|---|---|---|
+| `<DOMAIN-...>` | `<exact source + expression>` | `<symbolic result>` | `<derived = source / source ⊆ derived / derived ⊆ source / Required ⊆ union(cases)>` | `<derivation and source>` | `<proved / unresolved>` |
+
+- **Audit cutoff:** `<date/revision and effect on dynamic policies>`
+- **Exact `Required` predicate:** `<symbolic definition or link>`
+- **Policy conflicts/authorized resolution:** `<conflicts, decision, or
+  conservative audit domain without calling it the project promise>`
+- **Unresolved domain:** `<none or exact remainder/finding IDs>`
+
+### Covered Domain
 
-- **Supported set:** `<formal/operational definition>`
 - **Discovered axes:** `<features, cfg, targets, architectures, OSes, SIMD,
   allocators, debug assertions, panic modes, generated output, and other actual
   axes>`
-- **Coverage proof:** `<parametric argument, exhaustive partition, finite
-  enumeration, generator proof, or combination>`
+- **Exact `Covered` predicate:** `<union valid case regions within each
+  obligation, then intersect across all claim-required obligations>`
+- **Coverage proof:** `<parametric argument, justified exhaustive partition,
+  justified finite enumeration, generator proof, or combination>`
+- **Closure certificate:** `<proof of Required ⊆ aggregate Covered, or finding
+  ID>`
+- **Version-spanning premise basis:** `<parametric proof, exhaustive applicable
+  cases, exact compatibility entry, or unresolved>`
 - **Generated artifacts:** `<identity/proof>`
 - **Enforced exclusions:** `<how unsupported combinations cannot ship>`
 - **Sampled/tested configurations:** `<list and exact limited evidence provided>`
@@ -139,7 +149,14 @@ Full log: `<link/ID>`
   none>`
 - **Defect:** `<smallest missing, false, circular, or unsupported implication>`
 - **Authority/TCB involved:** `<citations/IDs>`
-- **UB witness:** `<valid in-scope execution reaching UB, or “not established”>`
+- **UB certificate — valid use:** `<why the use/execution is valid and in scope,
+  or “not established”>`
+- **UB certificate — reachability:** `<executed operation or semantic event,
+  or “not established”>`
+- **UB certificate — false safety proposition:** `<exact required clause and
+  derivation of its falsity, or “not established”>`
+- **UB certificate — consequence:** `<applicable authority/TCB derivation to
+  UB, or “not established”>`
 - **Defined postcondition refutation:** `<valid UB-free witness or equivalent
   proof that an in-scope UB-free execution falsifies the postcondition, or “not
   established”>`
@@ -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.

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,