diff --git a/maintainers/unsafe-rust-skill-design.md b/maintainers/unsafe-rust-skill-design.md index 1f592c1d90..7430c571e0 100644 --- a/maintainers/unsafe-rust-skill-design.md +++ b/maintainers/unsafe-rust-skill-design.md @@ -64,16 +64,20 @@ This model yields the core design: - A safety contract is an English-language theorem. - A safety comment is an English-language proof. -- Every conclusion must follow from checked local facts, established named - invariants, legitimate boundary contracts, authoritative axioms, or explicit - TCB premises. +- Inspection establishes literal artifact structure, not the semantic effect + of that structure. Every conclusion must follow from checked artifact facts, + applicable authoritative axioms or explicit TCB premises, and explicit + derivations through established lemmas and invariants. - Every missing implication makes the result unproved; demonstrating an actual UB execution is not required to reject the proof. - Proofs compose through contracts and invariant-carrying state, so global soundness follows from complete local discharge. -The skill does not need to teach this as an ontology. It needs to make agents -perform the consequences. +The skill does not need a philosophical ontology or a closed taxonomy of +unsafe operations. It does need a finite operational classification for every +proof proposition or premise, explicit treatment of material inferences, and +the artifact/semantics distinction, because those rules change whether an +apparently complete proof actually has admissible premises. ## Design Principles @@ -197,22 +201,45 @@ 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. +### Proof kernels separate artifact structure from semantics + +An artifact fact is a directly checked property of the audited material: +tokens, declarations, attributes, ordering, explicit annotations, generated +text, or comparable literal structure. A Rust axiom is the exact semantic +proposition entailed by applicable versioned Reference or standard-library +text. A derived lemma follows from artifact facts, applicable semantic +premises, earlier proved lemmas or invariants, and explicit logic or +mathematics. Selected-dependency facts, verified tool theorems, and admitted +TCB propositions retain their distinct trust treatment. + +The presence of syntax does not establish what compiling or executing it +means. Type value domains, evaluation and return, branching and matching, +arithmetic, configuration selection, accessibility, typing/coherence, and +caller-side unsafe obligations are semantic propositions even when the +relevant syntax is visible. Likewise, the text of a named invariant may be an +artifact fact, but its truth at a consumer is a derived lemma requiring +establishment and preservation proofs. + +The runtime procedure therefore uses one kernel discipline and requires a +closed evidence-bearing kernel for each certified conclusion: + +```text +artifact fact + + exact applicable Rust/stdlib axiom, selected-dependency fact, + verified tool theorem, or explicit TCB premise + + earlier proved lemma or invariant + + explicit logic or mathematics + -> derived lemma + -> consumer or certified conclusion +``` + +Kernel closure is a precondition to certification, not merely a final lint. A +reviewer must be able to recover every consumed premise and inferential edge, +applicability domain, source, and entailment direction. A broad topic label, +page-level citation, or named TCB entry supplies only the proposition explicitly +extracted and proved applicable. Ordinary proof prose and the obligation ledger +may carry each kernel; an explicit global graph or second proof artifact is +unnecessary. ### Producer contracts retain their quantifiers @@ -269,6 +296,13 @@ operation or event whose exact required safety proposition is false and the applicable semantics entails UB; once those facts are proved, the scoped result is `UNSOUND` even though other executions were not analyzed universally. +The valid-use premise discharges safety obligations owned outside the audited +scope, including obligations imposed on caller or implementer code supplied by +the witness. It must not assume the in-scope assertion being audited. Otherwise +a bad crate-owned `unsafe impl`, unsafe declaration, or boundary assertion would +become impossible to classify: its implementer contract would be assumed true +before the certificate could prove that exact assertion false. + The runtime therefore uses explicit verdict certificates. This prevents both optimistic acceptance from absence of a witness and over-cautious dilution of a proved witness into proof debt. Counterexamples do not replace obligation @@ -371,11 +405,13 @@ The installable package is structurally confined to `skills/unsafe-rust/`. Nothing in the runtime package links to `maintainers/`. - [`SKILL.md`](../skills/unsafe-rust/SKILL.md) contains the theorem, mandatory - workflow, hard trust/locality rules, routing, verdicts, and output contract. + workflow, always-loaded proof-kernel gate, hard trust/locality rules, routing, + verdicts, and output contract. - `agents/openai.yaml` contains UI metadata only and must not become a second instruction channel. - [`proof-obligations.md`](../skills/unsafe-rust/references/proof-obligations.md) - contains detailed contract, invariant, citation, and comment technique. + contains detailed evidence classification, kernel construction and closure, + valid-use, contract, invariant, citation, and comment technique. - [`abstraction-design.md`](../skills/unsafe-rust/references/abstraction-design.md) contains the conditional proof-oriented design process and the firewall between current-artifact verification and candidate design. @@ -389,8 +425,8 @@ Nothing in the runtime package links to `maintainers/`. 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, evidence reconciliation, finding, verdict, - and preservation rules. + contains scope, obligation-ledger, proof-kernel preservation, root/blocker, + finding, verdict, and audit-preservation rules. - `assets/` contains copyable audit artifacts, not additional hidden instructions. - Future evaluations belong outside the installable package. @@ -419,10 +455,10 @@ column records candidate semantic evaluation scenarios, not execution results. | D05 — Treat caller safe code adversarially | Unsafe code trusts unenforced callback/trait behavior | Seal, validate, or make implementer contract unsafe | [API closure](../skills/unsafe-rust/SKILL.md#close-api-and-configuration-boundaries); [traits](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#audit-traits-and-sealing) | EV05 — malicious safe trait impl | | D06 — Permit explicit selected-safe-dependency trust | Pointless recursive audits of intentionally chosen safe APIs | Record exact safe contract in TCB | [Premise policy](../skills/unsafe-rust/SKILL.md#use-only-applicable-premises); [dependency contracts](../skills/unsafe-rust/references/tcb-and-evidence.md#record-dependency-contracts) | EV06 — selected sort API versus caller comparator | | D07 — Audit or admit unsafe dependencies | Satisfying caller contract mistaken for implementation correctness | Recursive proof or `UNSAFE-DEP` entry | [Premise policy](../skills/unsafe-rust/SKILL.md#use-only-applicable-premises); [dependency contracts](../skills/unsafe-rust/references/tcb-and-evidence.md#record-dependency-contracts) | EV07 — unsound third-party unsafe helper | -| D08 — Restrict Rust axioms to versioned Reference/std text | Folklore and explanatory documents become premises | Quote, link, and verify exact authority | [Premise policy](../skills/unsafe-rust/SKILL.md#use-only-applicable-premises); [citations](../skills/unsafe-rust/references/proof-obligations.md#cite-authoritative-axioms) | EV08 — mischaracterized citation | +| 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); [proof kernel](../skills/unsafe-rust/references/proof-obligations.md#build-the-evidence-bearing-proof-kernel) | EV08 — mischaracterized citation | | 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 | +| 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); [kernel closure](../skills/unsafe-rust/references/proof-obligations.md#close-and-lint-the-proof-kernel) | 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-and-reconstruct-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 — 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 | @@ -432,9 +468,10 @@ column records candidate semantic evaluation scenarios, not execution results. | D18 — Preserve `#[doc(hidden)]` soundness but not implied SemVer | Hidden reachability becomes hidden safety precondition | Audit direct safe use; separate compatibility | [API closure](../skills/unsafe-rust/SKILL.md#close-api-and-configuration-boundaries); [hidden APIs](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#audit-macros-and-hidden-apis) | EV18 — reachable hidden safe constructor | | D19 — Treat contract changes as proof changes | Safety prose changes without caller/implementer re-audit | Directional compatibility analysis and triggers | [Contract evolution](../skills/unsafe-rust/references/api-boundaries-and-evolution.md#evolve-contracts-deliberately); [TCB evolution](../skills/unsafe-rust/references/tcb-and-evidence.md#review-and-evolve-the-tcb) | EV19 — strengthened unsafe precondition | | D20 — Separate literal audit from proof-oriented redesign | Inferred intent launders a current defect, or review misses a much simpler sound model | Preserve current verdict; derive minimum capability and re-audit implemented redesign | [Design routing](../skills/unsafe-rust/SKILL.md#design-for-provability-when-requested); [design reference](../skills/unsafe-rust/references/abstraction-design.md) | EV20 — overbroad nominal field abstraction | -| D21 — Certify verdicts by logical proof shape | Invalid proof is accepted because no exploit is known, or a completed existential UB derivation is diluted to `UNPROVED` | Use `UNPROVED` for an incomplete universal proof; use `UNSOUND` when valid use, reachability, false safety proposition, and UB consequence all close | [Verdict certificates](../skills/unsafe-rust/SKILL.md#use-exact-verdicts); [report aggregation](../skills/unsafe-rust/references/audit-reporting.md#aggregate-verdicts) | EV21 — paired incomplete obligation with no witness and multi-premise exact-version witness that must close | -| D22 — Preserve producer-contract quantifiers | One constructor's precondition is promoted into a postcondition or invariant of every value of its output type | Prove the exact consumed values or quantified set without reversing the producer implication | [Core composition](../skills/unsafe-rust/SKILL.md#compose-proofs-locally-and-literally); [premise classification](../skills/unsafe-rust/references/proof-obligations.md#separate-kinds-of-premises) | EV22 — unsafe constructor contract plus a separate safe producer that violates the assumed property | -| 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 | +| D21 — Certify verdicts by logical proof shape | Invalid proof is accepted because no exploit is known, a proposed witness has an unproved safe-use path, or a completed existential UB derivation is diluted to `UNPROVED` | Use `UNPROVED` for an incomplete universal proof; use `UNSOUND` only after valid-use, reachability, false safety proposition, and UB consequence certificates all close | [Verdict certificates](../skills/unsafe-rust/SKILL.md#use-exact-verdicts); [valid uses](../skills/unsafe-rust/references/proof-obligations.md#certify-valid-uses); [report aggregation](../skills/unsafe-rust/references/audit-reporting.md#aggregate-verdicts) | EV21 — paired incomplete obligation with no witness and multi-premise exact-version witness whose safe-call status must be proved | +| 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); [producer quantifiers](../skills/unsafe-rust/references/proof-obligations.md#preserve-producer-quantifiers) | EV22 — unsafe constructor contract plus a separate safe producer that violates the assumed property | +| D23 — Require a closed evidence-bearing proof kernel | Inspected syntax or a topical citation is treated as the semantic proposition needed, or a report reaches the right endpoint while omitting a consumed premise, inferential edge, applicability restriction, or exact entailment direction | Separate artifact facts from semantic premises; derive every consumed proposition explicitly; verify version, applicability, quotation direction, and closure before certification; reuse ordinary proof prose and the obligation ledger | [Proof-kernel gate](../skills/unsafe-rust/SKILL.md#close-an-evidence-bearing-proof-kernel); [kernel method](../skills/unsafe-rust/references/proof-obligations.md#build-the-evidence-bearing-proof-kernel); [kernel preservation](../skills/unsafe-rust/references/audit-reporting.md#preserve-closed-proof-kernels) | EV23 — visible construct with one uncited semantic edge plus a citation supporting only the wrong implication direction | +| D24 — Separate root proof gaps from dependent fan-out | One missing premise is reported as many independent defects, or downstream obligations are silently accepted | Assign one stable root blocker/gap ID, mark every dependent positive obligation `UNPROVED`, and preserve independent direct defects | [Kernel closure](../skills/unsafe-rust/references/proof-obligations.md#close-and-lint-the-proof-kernel); [reporting](../skills/unsafe-rust/references/audit-reporting.md#preserve-closed-proof-kernels) | EV24 — one missing semantic premise feeding several obligations plus a separate direct defect; require one root finding and complete dependent dispositions | ## Explicit Non-goals @@ -550,9 +587,11 @@ suite, require independent coverage of: 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; +- separation of artifact observations from semantic effects, closed + evidence-bearing kernels, exact citation-entailment direction and + applicability, indirect derivation, producer quantifiers, valid-use + certificates, local invariant/dataflow composition, and exposed + reconstructed proofs; - adversarial safe callers, every safe API boundary, interacting compilation configurations, and staged generated behavior with ordered fallible exits, tool interpretation, partial effects, and freshness where applicable; diff --git a/skills/unsafe-rust/SKILL.md b/skills/unsafe-rust/SKILL.md index 89ae055778..25f4bec5c1 100644 --- a/skills/unsafe-rust/SKILL.md +++ b/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,23 +223,22 @@ 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, @@ -196,13 +246,14 @@ documentation gap and suggest an upstream improvement when appropriate. ## 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 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 a3ef0c8619..6df38050ce 100644 --- a/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md +++ b/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 | |---|---|---|---|---|---|---|---|---| -| `` | `` | `` | `` | `` | `` | `` | `` | `` | +| `` | `` | `` | `` | `` | `` | `` | `` | `` | ## 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 | |---|---|---|---|---|---|---| | `` | `` | `` | `` | `` | `` | `` | @@ -165,9 +165,29 @@ Full log: `` - **Proposed proof-artifact repair:** `` - **Defect:** `` -- **Authority/TCB involved:** `` -- **UB certificate — valid use:** `` +- **Existential-certificate applicability:** `` +- **Valid-use certificate — scope/source:** `` +- **Valid-use certificate — boundary access/inputs:** `` +- **Valid-use certificate — typing/coherence:** `` +- **Valid-use certificate — boundary obligations:** `` +- **Valid-use certificate — TCB applicability:** `` - **UB certificate — reachability:** `` - **UB certificate — false safety proposition:** `` - [ ] 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 diff --git a/skills/unsafe-rust/references/abstraction-design.md b/skills/unsafe-rust/references/abstraction-design.md index b477d8022d..aee84fc15b 100644 --- a/skills/unsafe-rust/references/abstraction-design.md +++ b/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 diff --git a/skills/unsafe-rust/references/api-boundaries-and-evolution.md b/skills/unsafe-rust/references/api-boundaries-and-evolution.md index 8a27c298f6..d9ec80499c 100644 --- a/skills/unsafe-rust/references/api-boundaries-and-evolution.md +++ b/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 diff --git a/skills/unsafe-rust/references/audit-reporting.md b/skills/unsafe-rust/references/audit-reporting.md index 309c3ae271..7d68947332 100644 --- a/skills/unsafe-rust/references/audit-reporting.md +++ b/skills/unsafe-rust/references/audit-reporting.md @@ -4,7 +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) +- [Preserve closed proof kernels](#preserve-closed-proof-kernels) - [Aggregate verdicts](#aggregate-verdicts) - [Write actionable findings](#write-actionable-findings) - [Deliver a complete report](#deliver-a-complete-report) @@ -46,19 +46,21 @@ For each obligation, record: - exact proposition to prove; - operation, contract, invariant, or postcondition that requires it; - required applicability domain; -- supporting local facts, invariant clauses, axioms, and TCB entries, with the - applicability of each premise; +- the artifact facts, semantic premises, derived lemmas, and explicit inference + that form its evidence-bearing proof kernel, with each component's source and + applicability; - domain actually covered by the derivation and any case partition; - the appropriate certificate for every asserted set relationship and domain transformation consumed; - proof location; - reviewer verification; -- status and finding link. +- exact certificate status, any root blocker/gap ID that blocks certification, + 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. +reverse-trace the obligation through every intermediate proposition to literal +artifact facts and exact applicable semantic premises. Include obligations created by: @@ -82,16 +84,27 @@ 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. +## Preserve Closed Proof Kernels + +Apply [Close and lint the proof +kernel](proof-obligations.md#close-and-lint-the-proof-kernel) before certifying +any obligation, verdict, or regional result. The ledger or its linked canonical +proof must expose the exact goal and case, artifact facts, semantic premises, +inferences, derived proposition, and consumer. Reconcile every semantic premise +with the report's authority, tool-evidence, or TCB inventories, and +independently verify that each quotation entails the proposition in the +direction consumed. + +When one missing premise blocks several later certificates, assign a stable +root blocker/gap ID to the smallest gap and mark each dependent obligation with +that ID. A dependent positive or universal obligation is `UNPROVED` even if its +conditional reasoning after the missing premise is otherwise correct, but do +not report the fan-out as several independent root defects. This does not +override a separate closed existential certificate; aggregate that certificate +under the exact `UNSOUND` or `CONTRACT-BROKEN` rule below. A valid fact found +only by the reviewer may support a reconstructed implementation proof; record +the deficient report or safety comment rather than silently repairing its proof +artifact. ## Aggregate Verdicts @@ -144,7 +157,8 @@ Each finding should contain: - proposed replacement proof text when the reviewed artifact omits that derivation; - smallest missing, false, circular, or unsupported implication; -- authoritative contract or TCB entry involved; +- authoritative contract, verified tool theorem/evidence, or TCB entry + involved; - for a claimed UB witness, the valid use, executed operation or semantic event, false required safety proposition, and authoritative or TCB-backed UB consequence; diff --git a/skills/unsafe-rust/references/configurations-and-generated-code.md b/skills/unsafe-rust/references/configurations-and-generated-code.md index 5790ced732..2a9a205d5b 100644 --- a/skills/unsafe-rust/references/configurations-and-generated-code.md +++ b/skills/unsafe-rust/references/configurations-and-generated-code.md @@ -203,6 +203,12 @@ policy and build inputs -> selected shipped artifact and source ``` +Close every arrow with the [evidence-bearing proof +kernel](proof-obligations.md#build-the-evidence-bearing-proof-kernel). Inspection +can establish that a source operation, attribute, directive, or output occurs; +its execution or interpretation is a semantic proposition requiring applicable +Rust/stdlib authority, a verified tool theorem, or an explicit TCB premise. + 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 @@ -406,6 +412,9 @@ For each audit, report: - remaining assumptions, unknowns, and unsupported tool features; - triggers requiring re-audit. -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`. +Mark the configuration-closure obligation and every dependent affirmative claim +`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`. Apply final verdict certificates separately: a complete independent +existential certificate may still establish `UNSOUND` or `CONTRACT-BROKEN` for +its proved scope. diff --git a/skills/unsafe-rust/references/proof-obligations.md b/skills/unsafe-rust/references/proof-obligations.md index 815c02ccfa..26234ab107 100644 --- a/skills/unsafe-rust/references/proof-obligations.md +++ b/skills/unsafe-rust/references/proof-obligations.md @@ -4,15 +4,14 @@ - [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) +- [Build the evidence-bearing proof kernel](#build-the-evidence-bearing-proof-kernel) +- [Close and lint the proof kernel](#close-and-lint-the-proof-kernel) +- [Certify valid uses](#certify-valid-uses) - [Write safety documentation](#write-safety-documentation) - [Write local safety proofs](#write-local-safety-proofs) - [Carry invariants locally](#carry-invariants-locally) - [Prove temporal behavior](#prove-temporal-behavior) -- [Cite authoritative axioms](#cite-authoritative-axioms) -- [Search for indirect derivations](#search-for-indirect-derivations) -- [Review a proof](#review-a-proof) +- [Review and reconstruct a proof](#review-and-reconstruct-a-proof) ## Form the Theorem @@ -45,8 +44,8 @@ For each local proof site: Treat every operation, declaration, implementation, or state transition that supplies or consumes a safety contract as an obligation site. Follow each -obligation until it reaches checked local facts, named invariants, -authoritative axioms, or explicit TCB entries. +obligation until it reaches checked artifact facts, closed derived lemmas or +invariants, authoritative axioms, or explicit TCB entries. Apply the quantifier-sensitive verdict certificates in `SKILL.md` when a derivation fails or produces a counterexample. Do not confuse failure of a @@ -121,26 +120,64 @@ and an audit cutoff do not prove the releases between them. If the coverage basis does not contain the claimed release predicate, narrow the proved region and leave the remainder `UNPROVED`. -## Separate Kinds of Premises +## Build the Evidence-Bearing Proof Kernel -Classify every premise: +Express every material derivation as reviewable edges of this form: -- **Local fact:** Established by inspected code, control/data flow, a type, or a - named invariant. Cite the exact check, branch, assignment, ownership fact, or - invariant clause. -- **Rust axiom:** Entailed by exact applicable text in a versioned Rust Reference - or standard-library page. Quote and link it. +```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 +``` + +Classify every proposition or premise: + +- **Artifact fact:** A literal property of the exact inspected source, + expansion, generated output, metadata, or other artifact. Cite the location + or identity that exhibits it. Artifact facts include that tokens, + declarations, annotations, expressions, branches, attributes, or lexical + token/AST ordering occur; they do not include the runtime value relation, + execution order, or other semantic effect of those constructs. +- **Rust axiom:** A semantic proposition entailed by exact applicable text in a + versioned Rust Reference or standard-library page. Quote and link it. +- **Derived lemma or invariant:** A proposition already derived from identified + artifact facts, axioms, prior lemmas, and explicit inference. Cite its + canonical proof and applicability rather than treating its name as a premise. - **Selected safe-dependency fact:** Supplied by a deliberately selected safe dependency contract and recorded in the TCB. - **Tool-derived fact:** Established by a verified tool theorem whose exact - proposition, model, scope, and premises entail the local fact. Record only its - residual unproved tool/model/translation premises in the TCB. + proposition, model, scope, and premises entail the needed proposition. Record + its residual unproved tool/model/translation premises in the TCB. - **Additional assumption:** External specification, unsafe dependency, compiler implementation, platform behavior, deployment restriction, probabilistic premise, or other admitted proposition recorded in the TCB. -Never blur an assumption into a derived fact. If a premise does not fit one of -these classes, the proof is incomplete. +Pure logic and mathematics need no Rust citation, but state every material step +or witness. Never blur an assumption into a derived fact. If a proposition or +premise does not fit one of these classes or a material inference is unstated, +the proof is incomplete. + +Source inspection is not a shortcut around semantic authority. Seeing an `if`, +call, operator, type annotation, match, attribute, or tail expression proves +that the construct occurs. Claims about evaluation order, branch or arm +selection, return, arithmetic, inhabited values, name access, typing/coherence, +configuration selection, or caller-side unsafe obligations require the exact +applicable Rust or library propositions. A proof may derive control flow and +dataflow locally, but those are conclusions from artifact facts plus semantics, +not raw facts supplied by inspection. + +For every inferential edge consumed by a certified conclusion, record: + +1. the exact conclusion and applicability domain; +2. every premise, its class, source, and applicability; +3. the inference by which the premises entail the conclusion; and +4. the operation, later lemma, postcondition, or verdict that consumes it. + +### Preserve Producer Quantifiers Distinguish the validity of a value of type `T` from a stronger library invariant attached to its role in an abstraction. Prove both when needed. @@ -179,16 +216,16 @@ Likewise, distinguish: - obligations transferred to a returned pointer, reference, guard, token, or caller. -## Make Every Derivation Reviewable +## Close and Lint the Proof Kernel -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 +A proof may be compact, but a reviewer must be able to reverse it. A premise, +intermediate proposition, applicability restriction, or inference is material +when deleting it leaves the remaining explicit kernel 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. +every such component. An immediately checkable material artifact fact may be +recorded by an exact cited location without reproducing its literal tokens, but +it may not be absent. Omit only a purely logical rearrangement of already +explicit premises. Never omit the semantic proposition assigned to syntax. 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 @@ -198,31 +235,88 @@ 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: +The ordinary proof prose or obligation ledger may carry the kernel. 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 + applicability, every edge, and every intermediate proposition; +2. check each artifact fact against its exact identity and location, retaining + material operation order and alternative exits; +3. check every Rust semantic premise against its stated exact proposition, + versioned quotation, link, qualifications, and applicability; +4. check every other semantic premise against its verified tool theorem, + dependency contract, or accepted TCB entry; +5. check material mathematical and logical steps by their explicit derivations + or witnesses; they need no Rust citation; +6. write an implication or quantified proposition for each citation-to-claim + edge; reject any unjustified converse, inverse, strengthening, or domain + widening, and state any contrapositive step with its exact negation and + domain; +7. 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 +8. 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. +it, assign a stable root blocker/gap ID to the smallest missing implication, +and apply the exact verdict certificate. Give every dependent obligation a +disposition, but mark it with that root blocker/gap ID rather than presenting +the same omission as multiple independent defects. + +Do not equate the absence of one direct sentence with the absence of a proof. +Before declaring a semantic leaf missing, restate the exact proposition, +unfold relevant definitions, search for direct and stronger or orthogonal +applicable guarantees, combine them through explicit intermediate lemmas, and +try to construct a model satisfying the premises while falsifying the goal. +If a model remains possible, state the smallest missing implication. If the +Reference or standard-library documentation is ambiguous, inconsistent, or too +weak, record that exact gap, treat explanatory sources or implementation +behavior only as leads or explicit TCB assumptions, and suggest a narrowly +scoped upstream documentation improvement. + +## Certify Valid Uses + +A universal API theorem quantifies over its exact valid-use domain, and any +existential refutation needs a proved valid in-scope witness. Establish that +domain generally or instantiate these propositions for the proposed witness: + +1. **Scope and source selection:** the relevant item, expansion, + implementation, or entrypoint exists and is selected in the exact case. +2. **Boundary access and inputs:** a library caller can reach the exposed + boundary and supply every caller-controlled argument, implementation, or + capability used by the path; a binary or other entrypoint can receive the + permitted input/environment that starts the execution. Derive + implementation-internal values later in the separate execution-reachability + proof. +3. **Typing and coherence:** the complete use is well typed; every generic, + trait, lifetime, visibility, coherence, and implementability requirement is + satisfied. +4. **Boundary contracts:** every applicable documented unsafe caller or + implementer obligation owned outside the audited scope—including an + obligation imposed on caller or implementer code supplied by the witness—is + satisfied. No prose-only condition is imposed on a safe boundary. Do not + assume an in-scope audited impl, declaration, or boundary assertion; it may + be the safety proposition the later `UNSOUND` certificate proves false. +5. **Unsafe-context obligations:** every corresponding caller- or + implementer-side compiler-enforced unsafe-context requirement at the exposed + call, impl, field, macro, FFI, or other boundary is absent or satisfied. + This is distinct from the truth of the in-scope safety assertion under + audit. +6. **TCB qualification:** every dependency, external, deployment, or other + admitted premise used to validate the path is explicit and applicable. + +These are semantic propositions. For example, the inspected absence of the +token `unsafe` in a function declaration does not by itself prove the exact +caller obligation; cite the applicable language rule. For `UNSOUND`, combine +the valid-use certificate with separate execution-reachability, false safety +proposition, and UB-consequence edges. For `CONTRACT-BROKEN`, combine it with a +whole-execution UB-freedom proof and postcondition refutation. Apply the same +discipline, adapted to the proposition being proved, to any other existential +use or execution claim. A purely mathematical witness for a set relation +instead uses the certificate for that relation; it does not acquire +inapplicable API-boundary fields. ## Write Safety Documentation @@ -290,11 +384,12 @@ Use this structure: ```rust // SAFETY: // Obligation: `` requires P1, P2, and P3. -// Facts: -// - F1 follows from . -// - F2 follows from TCB-... / AXIOM-... . +// Artifact facts: +// - A1: occurs at . +// Semantic premises: +// - S1: AXIOM-... / TCB-... states . // Derivation: -// - F1 and F2 imply P1 because ... +// - A1 and S1 imply P1 because ... // - ... // Result: // - The operation establishes Q. @@ -370,71 +465,16 @@ Cryptographic infeasibility and low probability do not turn a possible execution into an unconditional Rust soundness proof. Move such premises to an explicit conditional application claim and TCB entry. -## Cite Authoritative Axioms - -For every Rust or standard-library ground-truth proposition: - -1. Select documentation applicable to the audited compiler/library version. -2. Link the narrowest applicable sections, including versions in the URLs. -3. Quote the smallest sufficient set of excerpts whose propositions participate - in the derivation. -4. State the proposition derived from each excerpt and justify the inference - that combines them. -5. Check that qualifications, definitions, linked clauses, and surrounding - scope do not weaken it. -6. Have the reviewer open the source and independently confirm the derivation. - -Apply [Qualify applicability](#qualify-applicability) when a citation and the -claim concern different Rust versions. - -If the Reference or standard-library documentation is missing, ambiguous, -internally inconsistent, or too weak, record the exact missing proposition. -Treat explanatory sources or current implementation behavior only as leads or -explicit additional assumptions. Recommend an upstream documentation report -when appropriate. - -## Search for Indirect Derivations - -Do not equate the absence of a single direct documentation sentence with the -absence of a proof. Before reporting an authoritative documentation gap or -finalizing an important obligation as unproved: - -1. Restate the exact semantic property required and unfold relevant project - definitions. -2. Search for applicable direct guarantees. -3. Search for stronger, more general, or orthogonal authoritative facts whose - conjunction could entail the property. -4. State every intermediate lemma and justify each inference rather than merely - collecting citations. -5. Check the applicability of every premise and intermediate lemma. -6. Try to construct a model that satisfies the premises while falsifying the - conclusion. If one remains possible, identify the missing implication. - -This search does not weaken the fail-closed rule. If no complete admissible -derivation is established, the obligation remains unproved. Distinguish “this -audit did not complete a proof” from the stronger claim that authoritative -documentation cannot support one. - -When a universal soundness derivation does not close, separately ask whether -the established facts close an existential refutation. Identify a valid -in-scope use or execution, prove reachability of the relevant operation or -semantic event, prove its exact required safety proposition false there, and -trace that failure to the applicable authoritative or explicitly trusted UB -consequence. If every link is proved, apply `UNSOUND`; if any link is absent, -the failed universal obligation remains `UNPROVED`. Do not demand a fact about -every input to establish one existential witness, and do not infer a witness -merely from the absence of a universal proof. - -## Review a Proof +## Review and Reconstruct a Proof For each proof: 1. Reconstruct the required preconditions from the callee or language/library contract rather than trusting the comment's summary. 2. Open every citation and verify its exact proposition, version, and scope. -3. Check each claimed local fact—including its quantifier, producer/transition - history, and applicability domain—against the actual dataflow and all - alternative paths. +3. Check each artifact fact against the exact artifact, and each derived local + lemma—including its quantifier, producer/transition history, and + applicability—against its complete kernel, dataflow, and alternative paths. 4. Expand every named invariant and ensure it is established initially and preserved by every permitted transition. 5. Check quantifiers, arithmetic boundaries, zero-sized and empty cases, @@ -444,11 +484,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. Apply [Make every derivation reviewable](#make-every-derivation-reviewable) +8. Apply [Close and lint the proof kernel](#close-and-lint-the-proof-kernel) 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 +9. Record every root missing implication and blocked dependent conclusion, then apply the verdict certificate in `SKILL.md`: report `UNPROVED` if a required implication remains absent and no existential refutation closes, or the applicable refutation verdict if one does. @@ -456,7 +495,7 @@ 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. Apply the material-component definition in -[Make every derivation reviewable](#make-every-derivation-reviewable). Give its +[Close and lint the proof kernel](#close-and-lint-the-proof-kernel). Give its citations, applicability, and relationship to the required preconditions and postconditions. Report the implementation result separately from the deficient proof artifact: