Refine the V3 targeted confirmation before freezing

evals/unsafe-rust/fixtures/v3-targeted/c_conflict/TCB.md

@@ -6,10 +6,10 @@
 - **Identity:** the toolchain-bundled Cargo releases corresponding exactly to
   supported Rust 1.84.0, 1.85.0, and 1.86.0, operating on the supplied
   `Cargo.toml` and source.
-- **Exact proposition:** for each supported release and ordinary Cargo profile,
-  enabling the named Cargo feature `turbo` or `hardened` sets the corresponding
-  `cfg(feature = "...")` predicate for this library compilation, while leaving
-  it disabled does not set that predicate. Compiling for
+- **Exact proposition:** for each supported release and every supported Cargo
+  profile, enabling the named Cargo feature `turbo` or `hardened` sets the
+  corresponding `cfg(feature = "...")` predicate for this library compilation,
+  while leaving it disabled does not set that predicate. Compiling for
   `x86_64-unknown-linux-gnu`, `aarch64-unknown-linux-gnu`, or
   `wasm32-unknown-unknown` sets `target_arch` to `x86_64`, `aarch64`, or
   `wasm32`, respectively.

evals/unsafe-rust/fixtures/v3-targeted/k_regression/REQUEST.md

@@ -4,7 +4,11 @@ Audit all three modules in `lib.rs`; do not stop after the first aggregate
 soundness finding.
 
 For `callback_index`, review every safe surface and propose the smallest repair,
-but do not edit the source. For `local_proof`, determine implementation
+but do not edit the source. The repaired API must remain callable for both read
+and write with positions chosen by safe callers; deleting the APIs or making
+them uncallable does not satisfy that functional requirement. No
+caller-implementable `Position` abstraction must be preserved. For
+`local_proof`, determine implementation
 correctness separately from the adequacy of its existing `SAFETY` comment and
 provide any materially reconstructed proof. For `published_lane`, treat the
 unsafe trait contract as a published 1.x contract with unknown downstream
@@ -14,5 +18,6 @@ consumer inventory.
 Keep every proposed repair uncertified until implemented and freshly audited.
 Do not build, test, or execute the target.
 
-Scope: exactly Rust 1.82.0, all targets and ordinary profiles, no additional
-TCB assumptions.
+Scope: exactly Rust 1.82.0, every target on which this exact source and its used
+Rust 1.82.0 standard-library items exist, every ordinary profile, and no
+additional TCB assumptions.

evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/EVIDENCE.md

@@ -2,15 +2,13 @@
 
 ## `acknowledge`
 
-The submitted material for this claim is its exact empty body. It has no
-statements, calls, unsafe blocks, raw-pointer accesses, or state transitions.
-No Rust-version-specific library proposition is submitted for this claim. The
-semantic bridge from that syntactic fact to the multi-release claim is exactly
-accepted entry `SEM-EMPTY-BLOCK-180-182` in `TCB.md`.
+The submitted source material for this claim is its exact empty body. No
+Rust-version-specific library page is submitted. `TCB.md` contains accepted
+entry `SEM-EMPTY-BLOCK-180-182`.
 
 ## `store_word`
 
-The submitted authorities form two exact applicable cases:
+The submitted authorities are:
 
 - [`std::ptr::write`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/ptr/fn.write.html):
   the description says that `write` overwrites without reading or dropping the
@@ -19,11 +17,9 @@ The submitted authorities form two exact applicable cases:
 - [`std::ptr::write`, Rust 1.81.0](https://doc.rust-lang.org/1.81.0/std/ptr/fn.write.html):
   the same description and Safety propositions apply to the 1.81.0 case.
 
-No compatibility premise is needed or supplied for this two-member domain.
-
 ## `copy_byte`
 
-One exact base authority is supplied:
+The submitted authorities are:
 
 - [`std::ptr::copy_nonoverlapping`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/ptr/fn.copy_nonoverlapping.html):
   its description says that it copies `count * size_of::<T>()` bytes and does
@@ -32,17 +28,18 @@ One exact base authority is supplied:
   be properly aligned, and the regions not to overlap. For `T = u8` and
   `count = 1`, these are the exact caller-side clauses in `lib.rs`.
 - [Rust 1.80.0 primitive data layout](https://doc.rust-lang.org/1.80.0/reference/type-layout.html#primitive-data-layout):
-  `u8` has size and alignment 1.
+  `u8` has size 1.
 - [`u8: Copy`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/primitive.u8.html#impl-Copy-for-u8):
   `u8` implements `Copy`.
+- [`Copy` semantics, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/marker/trait.Copy.html):
+  values of a `Copy` type are duplicated by a simple bitwise copy rather than
+  moved.
 
-The applicability of this authority beyond 1.80.0 is only the exact accepted
-compatibility proposition in `TCB.md`; no stability badge or sampled later
-page is submitted.
+`TCB.md` contains accepted entry `COMPAT-COPY-180-182`.
 
 ## `load_word`
 
-Only the two endpoint authorities are supplied:
+The submitted authorities are:
 
 - [`std::ptr::read`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/ptr/fn.read.html):
   the description says that `read` reads without moving and leaves the source
@@ -53,10 +50,11 @@ Only the two endpoint authorities are supplied:
   case.
 - [`u32: Copy`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/primitive.u32.html#impl-Copy-for-u32):
   `u32` implements `Copy` in the 1.80.0 endpoint case.
+- [`Copy` semantics, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/marker/trait.Copy.html):
+  the corresponding copy rather than move semantics apply at that endpoint.
 - [`u32: Copy`, Rust 1.82.0](https://doc.rust-lang.org/1.82.0/std/primitive.u32.html#impl-Copy-for-u32):
   `u32` implements `Copy` in the 1.82.0 endpoint case.
+- [`Copy` semantics, Rust 1.82.0](https://doc.rust-lang.org/1.82.0/std/marker/trait.Copy.html):
+  the corresponding copy rather than move semantics apply at that endpoint.
 
-No `ptr::read` authority for 1.80.1 or 1.81.0, compatibility premise, semantic
-continuity theorem, or exhaustive interior partition is supplied. Evidence for
-`ptr::write`, `copy_nonoverlapping`, or the empty `acknowledge` body establishes
-no proposition about `ptr::read` on those two releases.
+These are all submitted authorities and TCB entries for `load_word`.

evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/REQUEST.md

@@ -4,8 +4,8 @@ Audit the four exported unsafe APIs in `lib.rs` as four independent claims over
 their exact release sets in `SUPPORT.md`. For each API, report soundness and
 every documented postcondition separately, recover `Required`, state the exact
 `Covered` release region justified by the submitted evidence, and give the
-strongest combined verdict. A regional result is useful even when the complete
-claim cannot be closed.
+strongest combined verdict. Report every regional result material to that
+verdict.
 
 The authority entries and their claim-specific applicability are exactly those
 in `EVIDENCE.md`. The only non-authoritative admitted premises are the two
@@ -16,5 +16,4 @@ similar.
 This is a source-only evidence-packet review. Do not build, test, execute,
 inspect evaluator material, edit source, search for other Rust releases, or add
 new evidence. You may open only the exact versioned official Rust URLs already
-named in `EVIDENCE.md` to verify the supplied propositions. The audit cutoff
-limits the temporal claim but supplies no release-continuity premise.
+named in `EVIDENCE.md` to verify the supplied propositions.

evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/TCB.md

@@ -5,11 +5,13 @@
 - **Category:** OUT-OF-BAND general Rust-semantics proposition.
 - **Disposition:** accepted by the authorized human reviewer for this target.
 - **Exact proposition admitted:** for every
-  `v in {1.80.0, 1.80.1, 1.81.0, 1.82.0}`, every target on which this exact
-  source exists, and every ordinary debug or release profile, evaluating an
-  empty block executes no operation or event and yields unit. Marking the
-  function containing that block `unsafe` adds a caller proof obligation but
-  does not itself add an executed operation or event.
+  `v in {1.80.0, 1.80.1, 1.81.0, 1.82.0}`, every target on which the relevant
+  Rust syntax exists, and every ordinary debug or release profile, a well-typed
+  call that satisfies its caller obligations to a zero-parameter,
+  unit-returning Rust function whose body is exactly `{}` has defined callee
+  evaluation and returns `()`. Marking that function `unsafe` changes only the
+  static caller obligation, not the admitted callee-evaluation or return
+  semantics.
 - **Consumers:** only the local proof for `acknowledge`; the consumer must
   independently verify that its exact function body is empty and connect that
   fact to this proposition.
@@ -24,25 +26,26 @@
 - **Category:** OUT-OF-BAND compatibility proposition.
 - **Disposition:** accepted by the authorized human reviewer for this target.
 - **Base identity:** the Rust 1.80.0 `std::ptr::copy_nonoverlapping` page,
-  primitive-data-layout section, and `u8: Copy` implementation page named in
-  `EVIDENCE.md`.
+  primitive-data-layout section, `u8: Copy` implementation page, and `Copy`
+  semantics page named in `EVIDENCE.md`.
 - **Exact proposition admitted:** for each
   `v in {1.80.0, 1.80.1, 1.81.0, 1.82.0}`, every target on which the item
-  exists, `T = u8`, and `count = 1`, Rust preserves without weakening,
-  qualification, or added precondition all of these 1.80.0 propositions:
+  exists, every ordinary debug or release profile, `T = u8`, and `count = 1`,
+  Rust preserves without weakening, qualification, or added precondition all
+  of these 1.80.0 propositions:
   (1) if `src` is valid to read one initialized `u8`, `dst` is valid to write
   one `u8`, both pointers are properly aligned, and the one-byte regions do not
   overlap, executing `copy_nonoverlapping(src, dst, 1)` satisfies its safety
   contract; and (2) on return it copies the source byte to the destination
-  while leaving the source byte unchanged; and (3) `u8` has size and alignment
-  1 and implements `Copy`, so this call copies exactly one byte without moving
-  ownership from the source value.
+  while leaving the source byte unchanged; and (3) `u8` has size 1, implements
+  `Copy`, and has the documented `Copy` semantics, so this call copies exactly
+  one byte without moving ownership from the source value.
 - **Consumers:** only the soundness and documented-postcondition proofs for
   `copy_byte`.
 - **Excluded operations:** this entry establishes nothing about `ptr::read`,
   `ptr::write`, `acknowledge`, or any other API.
-- **Configuration scope:** every ordinary debug or release profile in
-  `V_copy`; no deployment or backend theorem.
+- **Configuration scope:** for every release and target case above, every
+  ordinary debug or release profile; no deployment or backend theorem.
 - **Re-audit trigger:** any change to `V_copy`, the base proposition, the exact
   source call, its type/count, or the human disposition.
 

evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/EVIDENCE.md

@@ -7,6 +7,3 @@ Exactly one Rust proposition is supplied for this review:
   states in its Safety section that reaching the function is undefined
   behavior. Its applicability is Rust 1.80.0 on every supported target and
   ordinary profile; the page states no narrower target or profile condition.
-
-The dependency declaration in `DEPENDENCY-API.md` is a caller-facing contract,
-not evidence that the unavailable implementation satisfies that contract.

evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/TCB.md

@@ -5,9 +5,5 @@
 - No `UNSAFE-DEP` entry for `peer-unsafe-dep` 3.4.5 has been proposed or
   accepted. The human reviewer expressly declines to trust its unavailable
   implementation for this audit.
-- Under the supplied dependency-resolution premise, the exact dependency pin
-  identifies the logical package coordinate `peer-unsafe-dep` 3.4.5. It does
-  not authenticate source or artifact bytes and does not establish the
-  selected implementation's correctness.
 - There are no other admitted implementation, compatibility, tool, or
   deployment propositions.

evals/unsafe-rust/fixtures/v3-targeted/r_redesign/REQUEST.md

@@ -12,5 +12,6 @@ Keep the current-artifact verdict independent of every proposal. Explain the
 contract and migration delta of the preferred design and what must be audited
 after implementation. Do not edit or execute the source.
 
-Scope: exactly Rust 1.82.0, all targets and ordinary profiles, no additional
-TCB assumptions.
+Scope: exactly Rust 1.82.0, every target on which this exact source and its used
+Rust 1.82.0 standard-library items exist, every ordinary profile, and no
+additional TCB assumptions.

evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/CI.md

@@ -3,7 +3,3 @@
 CI currently runs Rust 1.84.0 on `x86_64-unknown-linux-gnu` without
 `telemetry`, and Rust 1.86.0 on all three supported targets with both feature
 states.
-
-This is a sampling plan, not a definition or exhaustive inventory of supported
-configurations.
-

evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/SUPPORT.md

@@ -1,15 +1,12 @@
 # Supported configurations
 
 Let `r` denote a released stable Rust toolchain, ordered by its semantic
-version. This source snapshot supports the symbolic release interval
+version. This source snapshot supports exactly those `r` satisfying
 
 ```text
 1.84.0 <= r <= 1.86.0
 ```
 
-The interval means every stable Rust release in that closed interval, not only
-the `.0` releases. In particular, Rust 1.85.1 is expressly supported.
-
 The supported target triples are:
 
 - `x86_64-unknown-linux-gnu`;
@@ -22,4 +19,3 @@ every Cargo profile, with either state of debug assertions.
 
 `Cargo.toml` states the minimum compiler accepted by Cargo. This document,
 including its upper cutoff, is the project's support commitment.
-

evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/TCB.md

@@ -6,7 +6,7 @@
 - **Base authority:** the Rust 1.84.0 `Option::is_none` and
   `Option::unwrap_unchecked` standard-library pages.
 - **Exact proposition:** for every released stable Rust toolchain `r` satisfying
-  `1.84.0 <= r <= 1.86.0`, on every supported target and ordinary Cargo
+  `1.84.0 <= r <= 1.86.0`, on every supported target and every supported Cargo
   profile, with either feature or debug-assertion state, Rust preserves these
   base propositions without weakening, qualification, or added precondition:
   (1) `is_none` returns true exactly for `None`; and (2)

evals/unsafe-rust/fixtures/v3-targeted/x_cross/TCB.md

@@ -5,14 +5,23 @@
 - **Disposition:** accepted by the authorized human reviewer for this target.
 - **Identity:** Cargo 1.85.1 from the supported Rust 1.85.1 toolchain, operating
   on the supplied manifest, `build.rs`, environment interface, and library.
-- **Exact proposition:** Cargo executes the build script when required for the
-  selected build; honors its `rerun-if-env-changed=FIXTURE_ALLOCATOR` directive
-  when that environment value changes; and passes each emitted
+- **Exact proposition:** for every supported Cargo profile, Cargo executes the
+  build script when required for the selected build; honors its
+  `rerun-if-env-changed=FIXTURE_ALLOCATOR` directive when that environment
+  value changes; treats the emitted `rustc-check-cfg` directive as declaring
+  the two expected values without setting either configuration option; and
+  passes each emitted
   `cargo::rustc-cfg=fixture_allocator="..."` option to this library
   compilation. Enabling `burst` sets `cfg(feature = "burst")`. Compiling for
   `x86_64-unknown-linux-gnu`, `aarch64-unknown-linux-gnu`, or
   `wasm32-unknown-unknown` sets `target_arch` to `x86_64`, `aarch64`, or
-  `wasm32`, respectively.
+  `wasm32`, respectively. If a build-script stdout write fails or the script
+  otherwise exits unsuccessfully, Cargo halts before compiling the library and
+  produces no library compilation for that build attempt.
+- **Execution scope:** accepted-selector emission claims quantify over build
+  attempts whose build-script stdout writes succeed. An infrastructure write
+  failure produces no compiled configuration in `Required` and is not a new
+  selector value or a successful policy rejection.
 - **Consumers:** only allocator/feature/target reachability and effective
   rejection for this target.
 - **Excluded propositions:** no claim about which string the local build script

evals/unsafe-rust/fixtures/v3-targeted/x_cross/src/lib.rs

@@ -37,7 +37,10 @@ pub fn lane_id(value: u8) -> NonZeroU8 {
         fixture_allocator = "arena"
     )))]
     {
-        NonZeroU8::new(value).expect("lane identifier must be nonzero")
+        if value == 0 {
+            panic!("lane identifier must be nonzero");
+        }
+        // SAFETY: The preceding branch proves that `value != 0`.
+        unsafe { NonZeroU8::new_unchecked(value) }
     }
 }
-