Revise the unsafe Rust skill after the V3 evaluation

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,17 +85,19 @@ 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.
 
 ## Use Only Applicable Premises
 
 - 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

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

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,31 +80,48 @@ 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 |
 |---|---|---|---|---|---|---|---|---|
 | `<OBL-...>` | `<location>` | `<goal>` | `<required applicability>` | `<facts/invariants/TCB + domains>` | `<scope/partition>` | `<link>` | `<identity>` | `<status>` |
 
 ## 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 |
+| Step ID | Controlling source expression or prior predicate | Derived predicate/inventory/partition | Relation to prove (write symbolically) | Required certificate: containments/witnesses/derivation | Status |
 |---|---|---|---|---|---|
-| `<DOMAIN-...>` | `<exact source + expression>` | `<symbolic result>` | `<derived = source / source ⊆ derived / derived ⊆ source / Required ⊆ union(cases)>` | `<derivation and source>` | `<proved / unresolved>` |
+| `<DOMAIN-...>` | `<exact source + expression>` | `<symbolic result>` | `<exact symbolic relation, e.g. derived = source or Required ⊆ union(cases)>` | `<derivation and source>` | `<proved / unresolved>` |
 
 - **Audit cutoff:** `<date/revision and effect on dynamic policies>`
 - **Exact `Required` predicate:** `<symbolic definition or link>`
+- **Configuration projection:** `<Required_cfg(configuration)>`
 - **Policy conflicts/authorized resolution:** `<conflicts, decision, or
   conservative audit domain without calling it the project promise>`
 - **Unresolved domain:** `<none or exact remainder/finding IDs>`
 
+### Build and Generation Pipeline
+
+`<Use this table for a materially nontrivial claim-relevant build, generation,
+expansion, linking, or artifact-selection pipeline. Otherwise record the simple
+selection facts in the obligation ledger.>`
+
+| Stage ID | Input/state region and predecessor | Ordered operation or transformation | Successful output/effect | Alternative exit and partial effects | Authority/TCB and applicability | Consumer |
+|---|---|---|---|---|---|---|
+| `<STAGE-...>` | `<exact cases in which reached>` | `<local source step or tool transition>` | `<exact consumed value/cardinality/identity/order, or universal output property>` | `<claim-relevant failure/rejection/other exit; later steps not reached>` | `<source proof + exact semantic premise>` | `<next stage/obligation>` |
+
+- **Freshness/invalidation:** `<input-change to rerun/cache/output identity
+  relation, or why irrelevant>`
+
 ### Covered Domain
 
 - **Discovered axes:** `<features, cfg, targets, architectures, OSes, SIMD,
   allocators, debug assertions, panic modes, generated output, and other actual
   axes>`
-- **Exact `Covered` predicate:** `<union valid case regions within each
-  obligation, then intersect across all claim-required obligations>`
+- **Configuration-fiber proof:** `<how every full Required case in each
+  Required_cfg fiber reaches its exact artifact/source or other in-scope build
+  outcome, with findings for any remainder>`
+- **Exact full-case `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
@@ -114,7 +131,7 @@ and record every additional language-reachable surface in the table above.
 - **Generated artifacts:** `<identity/proof>`
 - **Enforced exclusions:** `<how unsupported combinations cannot ship>`
 - **Sampled/tested configurations:** `<list and exact limited evidence provided>`
-- **Uncovered configurations:** `<none or finding IDs>`
+- **Uncovered full cases/configurations:** `<none or finding IDs>`
 
 ## 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

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.

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 `<scope>` over `<Required predicate>`, 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,