Require evidence-bearing proof kernels in unsafe Rust V5

skills/unsafe-rust/SKILL.md

@@ -124,6 +124,57 @@ authoritative documentation is ambiguous or insufficient, identify the
 smallest missing proposition. Do not repair it with intuition. Report a
 documentation gap and suggest an upstream improvement when appropriate.
 
+## Close an Evidence-Bearing Proof Kernel
+
+Before certifying any conclusion, expose a minimal, reviewable kernel of this
+form:
+
+```text
+artifact facts
+  + applicable Rust/stdlib axioms, verified tool theorems,
+    or explicit TCB premises
+  + earlier proved lemmas or invariants
+  + explicit logic or mathematics
+  -> derived proposition
+  -> consumer, postcondition, or verdict
+```
+
+An artifact fact is only a literal property of the exact inspected source,
+expansion, generated output, or other artifact: for example, that a declaration,
+operator, type annotation, branch, tail expression, or attribute occurs at a
+location. Inspection alone does not establish what that construct means when
+compiled or executed. Branch selection, expression evaluation, function return,
+arithmetic behavior, type value domains, configuration selection, name access,
+typing/coherence, and caller-side unsafe obligations are semantic propositions;
+derive each from exact applicable authority or record the needed TCB premise.
+
+For every proof edge consumed by a certified conclusion, state the exact
+proposition and applicability, identify its premises and their sources, justify
+why they entail it, and identify its consumer. Quote the narrow text that
+entails each Rust axiom; a URL or topic label is not a proposition. Check
+direction explicitly: reject an unjustified converse, inverse, strengthened
+conclusion, or widened domain, and state any contrapositive step with its exact
+negation and domain. Canonical checked entries may be reused by identifier, but
+the local proof must show the proposition and inference being reused.
+
+Before treating a counterexample or caller path as a valid use, separately
+close its accessibility and selected-source path, well-typedness and coherence,
+every applicable caller and implementer contract owned outside the audited
+scope—including contracts imposed on witness-supplied code—and every
+corresponding compiler-enforced unsafe-context obligation needed to form the
+use. Do not assume an in-scope audited safety assertion merely because it
+appears on an unsafe impl, declaration, API boundary, or internal operation;
+that assertion may be the proposition an `UNSOUND` certificate later proves
+false. A declaration that looks safe is not, by inspection alone, proof that
+calling or implementing it carries no unsafe obligation.
+
+Do not issue `PROVED`, `UNSOUND`, `CONTRACT-BROKEN`, or an affirmative regional
+result until its required certificate closes. If a universal kernel remains
+incomplete, remove or qualify every dependent conclusion, record the smallest
+root gap and its dependent conclusions, search for an admissible indirect
+derivation, determine whether a separate existential certificate closes, and
+otherwise issue `UNPROVED`.
+
 ## Compose Proofs Locally and Literally
 
 - Identify the controlling contract independently of the existing safety
@@ -172,37 +223,37 @@ documentation gap and suggest an upstream improvement when appropriate.
    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,
+4. **State atomic obligations and kernels.** 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.
+   prove. Classify artifact facts, semantic premises, derived lemmas, and TCB
+   admissions; identify their exact sources and consumers.
 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.
+   relationship, and every claim conjunct through the evidence-bearing kernel
+   above. 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.
+   certificate, verify every semantic edge and implication direction, 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.
    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
 
-Read [proof-obligations.md](references/proof-obligations.md) before authoring or
-reviewing an unsafe contract, invariant, `SAFETY` comment, or local proof.
+Read [proof-obligations.md](references/proof-obligations.md) before authoring,
+reviewing, or auditing unsafe Rust and before certifying any proof, contract,
+invariant, `SAFETY` comment, or verdict.
 
 Keep each proof adjacent to the smallest cohesive unsafe operation or assertion.
-State the exact operation and its preconditions, cite checked facts and named
-invariants, show the derivation, and prove resulting postconditions and
-invariant state on every applicable exit.
+State the exact operation and its preconditions, cite checked artifact facts
+and proved lemmas or invariants, show the derivation, and prove resulting
+postconditions and invariant state on every applicable exit.
 
 When existing code can be validated only by reconstructing a material
 derivation absent from its safety comment, do not accept it silently. Include
@@ -269,7 +320,7 @@ persistent or full audit.
 |---|---|
 | **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. |
+| **UNSOUND** | There exists a proved valid in-scope use or execution—with accessibility/source selection, well-typedness/coherence, every applicable caller and implementer contract owned outside the audited scope (including contracts imposed on witness-supplied code), and every corresponding unsafe-context obligation needed to form the use satisfied—which reaches an executed operation or semantic event, an exact in-scope audited safety proposition (whether internal or attached to an impl, declaration, or API boundary) 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

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

@@ -80,9 +80,9 @@ and record every additional language-reachable surface in the table above.
 
 ## Obligation Ledger
 
-| Obligation ID | Source/API | Exact proposition | Required domain | Derivation, material premises, and their applicability | Covered domain/cases | Proof location | Reviewer | Status |
+| Obligation ID | Source/API | Exact goal and consumer | Required case/domain | Evidence-bearing kernel and component provenance | Covered domain/cases and relation certificates | Proof location | Certificate status / root blockers / finding | Reviewer verification |
 |---|---|---|---|---|---|---|---|---|
-| `<OBL-...>` | `<location>` | `<goal>` | `<required applicability>` | `<facts/invariants/TCB + domains>` | `<scope/partition>` | `<link>` | `<identity>` | `<status>` |
+| `<OBL-...>` | `<location>` | `<proposition + operation, lemma, postcondition, or verdict that consumes it>` | `<required applicability>` | `<artifact facts + semantic premises + derived lemmas + explicit inference; exact source and applicability for each>` | `<scope/partition + set/domain-transformation certificate IDs>` | `<link>` | `<exact status; root blocker IDs or none; finding link or none>` | `<reviewer identity + verification result/link>` |
 
 ## Theorem-Domain and Configuration Closure
 
@@ -105,7 +105,7 @@ and record every additional language-reachable surface in the table above.
 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 ID | Input/state region and predecessor | Ordered operation or transformation | Successful output/effect | Alternative exit and partial effects | Authority/tool/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>` |
 
@@ -165,9 +165,29 @@ Full log: `<link/ID>`
 - **Proposed proof-artifact repair:** `<replacement comment/canonical proof, or
   none>`
 - **Defect:** `<smallest missing, false, circular, or unsupported implication>`
-- **Authority/TCB involved:** `<citations/IDs>`
-- **UB certificate — valid use:** `<why the use/execution is valid and in scope,
+- **Authority/tool/TCB involved:** `<citations/IDs>`
+- **Existential-certificate applicability:** `<required for a finding that
+  asserts a use/execution witness; otherwise “not applicable” for every
+  valid-use and UB field below>`
+- **Valid-use certificate — scope/source:** `<why the exact artifact, configuration,
+  input, state, and execution are in scope and the relevant source is selected,
   or “not established”>`
+- **Valid-use certificate — boundary access/inputs:** `<how a library caller can reach
+  the exposed boundary and supply every caller-controlled argument, impl, or
+  capability, or how the permitted binary/entrypoint input starts the
+  execution; “not established” if absent>`
+- **Valid-use certificate — typing/coherence:** `<why the complete use is well typed,
+  coherent, and implementable, or “not established”>`
+- **Valid-use certificate — boundary obligations:** `<why every applicable
+  caller or implementer contract owned outside the audited scope—including
+  contracts imposed on witness-supplied code—and every corresponding
+  compiler-enforced unsafe-context requirement needed to form the use is absent
+  or satisfied; identify rather than assume any in-scope audited impl,
+  declaration, boundary, or internal safety assertion tested below; or “not
+  established/not applicable”>`
+- **Valid-use certificate — TCB applicability:** `<dependency, external, deployment,
+  or other admitted premises used to validate the path, or “none/not
+  established”>`
 - **UB certificate — reachability:** `<executed operation or semantic event,
   or “not established”>`
 - **UB certificate — false safety proposition:** `<exact required clause and
@@ -229,8 +249,14 @@ explicitly excluded region. Explain enforcement of exclusions.>`
 
 - [ ] Every in-scope obligation has a status.
 - [ ] 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).
+      set relationship satisfies [Close and lint the proof
+      kernel](../references/proof-obligations.md#close-and-lint-the-proof-kernel).
+- [ ] Artifact observations are not used as semantic propositions; every
+      consumed semantic edge has exact applicable authority, a verified tool
+      theorem, or an accepted TCB entry.
+- [ ] Every citation's extracted proposition and the conclusion that consumes
+      it were checked in implication form for direction, qualifications, and
+      domain.
 - [ ] 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.
@@ -241,10 +267,19 @@ explicitly excluded region. Explain enforcement of exclusions.>`
 - [ ] Every verdict has the certificate required by `SKILL.md`, including
       `Required ⊆ Covered` for `PROVED` and every existential link for
       `UNSOUND` or `CONTRACT-BROKEN`.
+- [ ] Every existential use or execution witness has a closed valid-use
+      certificate covering source selection, boundary access/inputs,
+      typing/coherence, boundary contracts owned outside the audited scope
+      (including contracts imposed on witness-supplied code), corresponding
+      unsafe-context requirements, and TCB applicability without assuming an
+      in-scope audited safety assertion; a `CONTRACT-BROKEN` witness additionally
+      proves whole-execution UB-freedom. Mathematical witnesses use the
+      certificate for their exact relation instead.
 - [ ] Every material derivation reconstructed during review is exposed with its
       applicability, and deficient proof artifacts are reported separately.
-- [ ] Every material semantic premise appears in the authority/TCB inventory,
-      and every consumed citation and TCB entry was independently verified.
+- [ ] Every material semantic premise appears in the authority, tool-evidence,
+      or TCB inventory, and every consumed citation, tool theorem, 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/abstraction-design.md

@@ -51,9 +51,9 @@ Record the constraints that the abstraction must satisfy:
 Use each source only for the proposition it actually establishes. User
 requirements can determine desired behavior. Current contracts determine
 current obligations. Call sites, tests, names, comments, history, and
-implementation structure may suggest intent or establish local source facts,
-but an inference about intent is not a Rust semantic premise and does not prove
-implementation correctness.
+implementation structure may suggest intent or establish literal artifact
+facts, but an inference about intent is not a Rust semantic premise and does
+not prove implementation correctness.
 
 Known internal consumers do not exhaust the consumers of a public API. Treat
 the published contract as a required constraint unless an applicable contract

skills/unsafe-rust/references/api-boundaries-and-evolution.md

@@ -46,6 +46,13 @@ code preserves soundness. For each unsafe surface, prove that its complete
 documented contract is sufficient and that its implementation establishes all
 documented postconditions for every valid use.
 
+When a universal proof or counterexample depends on a caller path through one
+of these surfaces, apply [Certify valid
+uses](proof-obligations.md#certify-valid-uses). Source visibility or a
+safe-looking declaration does not by itself prove access, well-typedness,
+coherence, or the absence of a caller- or implementer-side compiler-enforced
+unsafe-context requirement needed to form the use.
+
 Determine the controlling contract from the actual published or otherwise
 applicable normative text. Examples, rationale, tests, names, existing safety
 comments, and inferred design intent may aid discovery but may not narrow or