Revise unsafe Rust skill to V2 after V1 evaluation failures

skills/unsafe-rust/SKILL.md

@@ -48,6 +48,14 @@ deployment separately with their additional premises.
 - Attach an applicability domain to every claim and premise, whether stated
   locally or inherited from an identified project policy or canonical entry. A
   derivation proves only the cases covered by all premises it consumes.
+- Define or inherit a precise supported toolchain/configuration predicate
+  before consuming versioned premises or issuing a full verdict. If applicable
+  project sources conflict or materially underdetermine that predicate, obtain
+  an authorized resolution, prove an explicit conservative superset covering
+  every materially supported candidate predicate identified from those
+  sources, or leave the affected full-scope claim `UNPROVED`. Do not silently
+  select an MSRV, current toolchain, or convenient interpretation, and do not
+  assume that one earliest version represents the whole predicate.
 - Apply a guarantee documented for an older Rust release to a later stable
   release only when an exact applicable Rust backwards-compatibility
   commitment preserves that exact proposition throughout the later release's
@@ -92,6 +100,13 @@ documentation gap and suggest an upstream improvement when appropriate.
   entails the exact needed precondition.
 - Trace dataflow across calls and time rather than limiting review to lexical
   unsafe blocks. Account for every producer, transition, and consumer.
+- Do not promote a producer's preconditions into a universal invariant of its
+  output type. Any type- or abstraction-wide conclusion needs a complete
+  derivation independent of that invalid reversal—for example, applicable
+  authoritative premises, construction-and-preservation closure under an
+  enforced boundary, or an admissible explicit TCB premise. Local checks and
+  other applicable derivations may instead prove the proposition for the
+  particular consumed values or quantified subset.
 - For new code, place invariant-bearing representation in the smallest
   practical leaf module, keep safely accessible representation fields private
   to it, and treat safe code outside that module—including the rest of the same
@@ -100,9 +115,10 @@ documentation gap and suggest an upstream improvement when appropriate.
 ## Follow the Proof Workflow
 
 1. **Frame the claim.** Record the artifact identity, exact scope, valid uses or
-   executions, Rust and dependency versions, supported configuration set,
-   mandatory postconditions, TCB, exclusions, and whether design alternatives
-   are requested.
+   executions, Rust and dependency versions, the supported
+   toolchain/configuration predicate and its controlling sources, mandatory
+   postconditions, TCB, exclusions, unresolved support-policy conflicts, and
+   whether design alternatives are requested.
 2. **Inventory the surface.** Enumerate every in-scope safe and unsafe API
    surface, obligation site, invariant producer/transition/consumer, and
    generated or expanded artifact across the supported set.
@@ -113,11 +129,14 @@ documentation gap and suggest an upstream improvement when appropriate.
    explicit TCB entries. Unfold definitions and seek indirect multi-premise
    derivations; absence of one direct sentence is not itself a documentation
    gap. Justify every intermediate inference.
-5. **Close composition.** Ensure every literal contract clause and safe surface
-   has a disposition, every premise consumed by unsafe code has an admissible
-   source, and every supported configuration region is proved by an abstract
-   argument or exhaustive partition. Try to falsify the contract reading,
-   inference chain, and coverage before concluding `PROVED`.
+5. **Close composition.** Over the entire supported toolchain/configuration
+   predicate—by one parametric proof or an exhaustive partition as
+   appropriate—give every literal clause of each applicable controlling
+   contract and every safe surface a disposition. Ensure every consumed
+   premise has an admissible source. Try to falsify the contract reading, each
+   derivation, and coverage, including boundary and adversarial cases derived
+   from the clauses themselves rather than from any supposedly exhaustive
+   hazard list, before concluding `PROVED`.
 6. **Report exactly.** Keep unresolved obligations visible and state the
    smallest missing implication. Record proofs, TCB, coverage, findings,
    postcondition failures, documentation gaps, and residual scope without
@@ -164,8 +183,9 @@ requires an unenforced implementer behavior.
 
 Read
 [configurations-and-generated-code.md](references/configurations-and-generated-code.md)
-for every full audit and whenever conditional compilation, targets, generated
-code, FFI, assembly, SIMD, allocators, linking, or build tooling is relevant.
+for every full audit and whenever supported-toolchain policy, conditional
+compilation, targets, generated code, FFI, assembly, SIMD, allocators, linking,
+or build tooling is relevant.
 Every supported combination of compilation options that can ship downstream
 must be sound. Use parametric proofs or exhaustive partitions when literal
 enumeration would explode; do not substitute a tested sample.
@@ -204,8 +224,18 @@ persistent or full audit.
   circular, or unverifiable.
 - **UNSOUND:** A valid use or in-scope execution is proved to reach undefined
   behavior.
-- **CONTRACT-BROKEN:** A documented postcondition is proved false even though
-  undefined behavior need not occur.
+- **CONTRACT-BROKEN:** It is proved that there exists a valid in-scope
+  execution which, considered as a whole, contains no undefined behavior and
+  falsifies a documented postcondition.
+
+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
+establish the existential claim required for `CONTRACT-BROKEN`. If it is the
+only behavioral evidence, report soundness as `UNSOUND` and the postcondition
+as `UNPROVED`. An independent UB-free witness or equivalent existence proof
+may establish `CONTRACT-BROKEN`; separate proofs may therefore establish both
+verdicts.
 
 Apply verdicts separately to soundness, documented postconditions, and
 conditional application claims. State exact scope, applicability, and TCB

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

@@ -17,6 +17,8 @@
   do not present it as unconditional Rust soundness>`
 - **Scope:** `<APIs/modules/packages/binaries>`
 - **Supported configuration predicate:** `<exact definition or link>`
+- **Support-policy sources/conflicts:** `<controlling sources, ambiguity,
+  authorized resolution or conservative audit superset, and audit cutoff>`
 - **TCB log:** `<ID/revision/link>`
 - **Skill revision:** `<unsafe-rust revision>`
 - **Qualification:** `<exact conditional assumptions; “none beyond stated TCB”
@@ -137,7 +139,9 @@ Full log: `<link/ID>`
   none>`
 - **Defect:** `<smallest missing, false, circular, or unsupported implication>`
 - **Authority/TCB involved:** `<citations/IDs>`
-- **Counterexample:** `<valid UB/postcondition witness, or “not required/not
+- **UB witness:** `<valid in-scope execution reaching UB, or “not established”>`
+- **Defined postcondition refutation:** `<valid UB-free witness or equivalent
+  proof that an in-scope UB-free execution falsifies the postcondition, or “not
   established”>`
 - **Affected producers/consumers:** `<IDs/locations>`
 - **Required resolution:** `<minimum proof, contract, implementation, privacy,

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

@@ -226,9 +226,12 @@ At minimum, an unsafe API implementation is responsible for both:
 2. establishing every documented postcondition when its safety preconditions
    and other documented conditions are met.
 
-Do not label a postcondition failure “sound” and stop. Report it separately as
-`CONTRACT-BROKEN`, while also determining whether downstream unsafe code can
-turn the broken guarantee into unsoundness.
+Evaluate postconditions independently under the verdict rule in `SKILL.md`. A
+UB-containing execution cannot itself prove the required UB-free behavioral
+refutation: report soundness as `UNSOUND` and leave that postcondition
+`UNPROVED` unless an independent UB-free witness or equivalent proof resolves
+it. Determine whether a proved broken guarantee can make downstream unsafe
+consumers unsound.
 
 Do not invent a universal standard for undocumented robustness. State the exact
 behavioral claim being reviewed: panic freedom, determinism, resource bounds,

skills/unsafe-rust/references/audit-reporting.md

@@ -15,9 +15,10 @@ Before reviewing proofs, record:
 
 - exact repository, source revision/digest, workspace packages, generated
   artifacts, and relevant uncommitted changes;
-- Rust/compiler/standard-library versions and supported range;
+- supported toolchain/configuration predicate, its controlling policy sources,
+  conflicts or gaps, audit cutoff, authorized resolution or conservative audit
+  domain, and enforced exclusions;
 - dependency resolution and relevant source identities;
-- supported configurations and exclusions;
 - API, module, binary, or whole-project scope;
 - soundness theorem and documented postconditions in scope;
 - TCB log identity/revision;
@@ -84,6 +85,13 @@ be `UNSOUND` while a different configuration remains `UNPROVED`. Issue `PROVED`
 for the combined default claim only when every in-scope soundness and
 documented-postcondition obligation is proved.
 
+Classify a witness using the execution as a whole. A valid execution that ever
+exhibits UB can establish `UNSOUND` but cannot itself establish the UB-free
+existence claim required for `CONTRACT-BROKEN`. If it is the only behavioral
+evidence, report that postcondition as `UNPROVED`. An independent UB-free
+witness or equivalent existence proof may establish `CONTRACT-BROKEN`;
+separate proofs may establish both verdicts.
+
 Place qualifications in the theorem, not in vague prose. Use:
 
 > PROVED for `<scope>` under `<supported-set predicate>`, relative to TCB
@@ -109,7 +117,8 @@ Each finding should contain:
   derivation;
 - smallest missing, false, circular, or unsupported implication;
 - authoritative contract or TCB entry involved;
-- whether a valid UB counterexample or postcondition counterexample is known;
+- whether a valid UB witness or a separate UB-free postcondition refutation or
+  equivalent existence proof is known;
 - affected callers, producers, consumers, generated output, and configurations;
 - minimal acceptable resolution;
 - compatibility and re-audit consequences.
@@ -156,8 +165,10 @@ A complete audit report contains:
 5. **Obligation coverage:** Proof sites and status summary; link to detailed
    proofs/findings rather than duplicating them. Include material reconstructed
    proofs missing from the reviewed proof artifacts.
-6. **Configuration closure:** Supported-set definition, axes, abstract or
-   enumerative coverage proof, generated artifacts, and enforced exclusions.
+6. **Configuration closure:** Supported-set definition, controlling policy
+   sources and conflicts, audit cutoff, authorized resolution or conservative
+   superset, axes, abstract or enumerative coverage proof, generated artifacts,
+   and enforced exclusions.
 7. **TCB audit log:** Every authoritative or admitted proposition and reviewer
    disposition.
 8. **Tool-derived evidence:** Exact theorem, artifact/model scope, bounds,

skills/unsafe-rust/references/configurations-and-generated-code.md

@@ -14,20 +14,52 @@
 ## Define the Supported Set
 
 Write a precise predicate `Supported(configuration)` before claiming full
-soundness. Derive it from published package metadata, documentation, target
-policy, feature declarations, build tooling, compiler support, downstream
-integration agreements, and the artifacts that can actually be shipped.
-
-Include every compilation option combination that downstream users are allowed
-to produce, not merely CI jobs or maintainer-preferred builds. If a compilable
-combination is exposed without a clear exclusion, conservatively treat it as
-supported until the project owner establishes otherwise.
+soundness. Fix the exact source or packaged artifact and audit cutoff. Let the
+predicate range over every relevant toolchain component, host/target fact, and
+build option rather than reducing it to a `rustc` version string.
+
+Classify support evidence before using it:
+
+- applicable package metadata, published policy, release documentation,
+  feature/target policy, and authorized downstream agreements may define the
+  project's support contract;
+- manifest checks, build scripts, `compile_error!`, wrappers, packaging rules,
+  and distribution controls may admit or enforce configurations; and
+- CI jobs, lockfiles, successful builds, `rust-toolchain.toml`, and maintainer
+  defaults observe or select particular configurations but do not by themselves
+  define or prove downstream support.
+
+Resolve inherited fields in the exact workspace and inspect the effective
+packaged metadata when it can differ. Interpret every mechanism through its
+applicable contract; do not hard-code a universal precedence among metadata,
+documentation, and agreements. A documented exclusion may delimit a support
+promise, but if soundness depends on preventing that configuration from
+shipping, require effective rejection before claiming closure.
+
+If applicable support declarations conflict or materially underdetermine the
+predicate, do not silently select the narrowest interpretation. Obtain an
+authorized project decision, prove an explicit conservative superset covering
+every materially supported candidate predicate identified from the controlling
+sources, or report regional results and leave the full claim `UNPROVED`. Do not
+call that conservative audit domain a newly inferred project promise. If a
+shippable configuration is exposed and no applicable contract clearly excludes
+it, include it in the unresolved conservative candidate domain until project
+authority resolves its status; successful compilation alone still does not
+define the support promise.
+
+Preserve conditional and nonlinear structure across every discovered axis
+rather than collapsing the predicate to a single MSRV. It may be finite,
+nonlinear, or moving and need not have a globally earliest toolchain. Resolve
+dynamic policies at the audit cutoff; cover later members only through an
+applicable parametric theorem or re-audit trigger.
 
 Record:
 
 - source revision and workspace/package selection;
 - Rust toolchain range, edition, standard-library identity, and relevant compiler
   flags;
+- controlling support-policy sources, conflicts, authorized resolutions, and
+  the audit cutoff;
 - target triples, target specifications, CPUs, features, ABIs, data layouts, and
   linkers;
 - Cargo features, dependency feature unification, optional dependencies, and

skills/unsafe-rust/references/proof-obligations.md

@@ -52,7 +52,9 @@ execution exhibits undefined behavior, make no claim that observations
 elsewhere—or notionally “before” that event—remain guaranteed. An unexecuted bad
 path does not by itself make a different execution undefined, but soundness of a
 safe API still quantifies over every valid use and execution, so one reachable
-valid counterexample refutes it.
+valid counterexample refutes it. Such a UB-containing execution cannot also
+establish a defined behavioral observation; apply the exact witness rule in
+`SKILL.md`.
 
 ## Qualify Applicability
 
@@ -76,6 +78,10 @@ exactly identified project support policy, invariant definition, axiom entry,
 or TCB entry. The local proof must still make the inheritance and relevant case
 clear enough to review.
 
+Derive the required predicate under
+[Define the supported set](configurations-and-generated-code.md#define-the-supported-set),
+then carry it through every premise and case lemma below.
+
 A documented Rust guarantee from version `R` may support a later stable version
 only when an exact Rust backwards-compatibility commitment preserves that exact
 semantic proposition throughout the later version's relevant edition, target,
@@ -125,6 +131,33 @@ these classes, the proof is incomplete.
 
 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.
+
+Never promote one producer's admission contract into an invariant of its output
+type. A constructor, conversion, deserializer, FFI ingress, mutation, or other
+producer precondition applies at that invocation. It supports a fact about that
+particular result only through a proved postcondition or dataflow relation; it
+does not prove that every valid value came through that producer or that later
+transitions preserve the property.
+
+To rely on `I` as an invariant of every value in a stated set, provide a
+complete derivation over that set without reversing the producer implication.
+Such a derivation may, for example, use:
+
+1. applicable authoritative premises that entail `I` for every value in the
+   set;
+2. an enforced abstraction boundary plus a complete proof that every in-scope
+   ingress and producer establishes `I` and every transition preserves it;
+3. another applicable derivation, including a verified tool theorem, that
+   entails the exact quantified proposition; or
+4. the exact universal proposition as an admissible accepted TCB premise under
+   the TCB rules.
+
+This enumeration does not replace the entailment requirement or exclude other
+valid proof forms. A consumer may instead establish `I` for its particular
+values or quantified subset from local checks, proved producer and transition
+history, and other applicable premises. If neither derivation closes, leave
+the consuming obligation `UNPROVED`.
+
 Likewise, distinguish:
 
 - permission to perform an operation;
@@ -331,8 +364,9 @@ 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 against the actual dataflow and all alternative
-   paths.
+3. Check each claimed local fact—including its quantifier, producer/transition
+   history, and applicability domain—against the actual dataflow and all
+   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,
@@ -358,8 +392,9 @@ proof artifact:
 - If the reconstruction succeeds, the implementation obligation may be proved,
   but report the inadequate comment and provide proposed replacement wording.
 - If the reconstruction fails, leave the obligation unproved.
-- If it yields a valid UB or postcondition counterexample, report `UNSOUND` or
-  `CONTRACT-BROKEN` as applicable.
+- If it yields a valid execution containing UB, report `UNSOUND`. If it proves
+  that a valid UB-free execution falsifies a postcondition, report
+  `CONTRACT-BROKEN`. Do not use the UB-containing execution itself for both.
 
 When changes are authorized, update the adjacent proof rather than leaving the
 reconstructed reasoning only in the review. A canonical checked proof or named