Draft targeted confirmation for unsafe Rust V3

evals/unsafe-rust/fixtures/v3-targeted/c_conflict/Cargo.toml

@@ -0,0 +1,13 @@
+[package]
+name = "conflicting-domain-target"
+version = "0.1.0"
+edition = "2021"
+rust-version = "1.84"
+
+[features]
+default = []
+turbo = []
+hardened = []
+
+[lib]
+path = "src/lib.rs"

evals/unsafe-rust/fixtures/v3-targeted/c_conflict/POLICY-INDIGO.md

@@ -0,0 +1,25 @@
+# Published support policy: Indigo
+
+For this snapshot, let:
+
+- `V = {1.84.0, 1.85.0, 1.86.0}`;
+- `X = x86_64-unknown-linux-gnu`;
+- `A = aarch64-unknown-linux-gnu`;
+- `W = wasm32-unknown-unknown`;
+- `f` mean that `turbo` is enabled; and
+- `h` mean that `hardened` is enabled.
+
+Both Boolean states of each feature are meaningful. A configuration
+`(v, t, f, h)` is supported by Indigo exactly when `v` is in `V`, `t` is in
+`{X, A, W}`, and this predicate is true:
+
+```text
+!f
+or (f and t = X and (h or v >= 1.86.0))
+or (f and t = A and !h and v >= 1.85.0)
+```
+
+Thus `turbo` on `W` is expressly unsupported. All Cargo profiles and both
+states of debug assertions are supported for every configuration selected by
+the predicate.
+

evals/unsafe-rust/fixtures/v3-targeted/c_conflict/POLICY-SCARLET.md

@@ -0,0 +1,25 @@
+# Published support policy: Scarlet
+
+For this snapshot, let:
+
+- `V = {1.84.0, 1.85.0, 1.86.0}`;
+- `X = x86_64-unknown-linux-gnu`;
+- `A = aarch64-unknown-linux-gnu`;
+- `W = wasm32-unknown-unknown`;
+- `f` mean that `turbo` is enabled; and
+- `h` mean that `hardened` is enabled.
+
+Both Boolean states of each feature are meaningful. A configuration
+`(v, t, f, h)` is supported by Scarlet exactly when `v` is in `V`, `t` is in
+`{X, A, W}`, and this predicate is true:
+
+```text
+!f
+or (f and t = X and (!h or v >= 1.85.0))
+or (f and t = A and h)
+```
+
+Thus `turbo` on `W` is expressly unsupported. All Cargo profiles and both
+states of debug assertions are supported for every configuration selected by
+the predicate.
+

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

@@ -0,0 +1,13 @@
+# Conflicting-policy source review
+
+`POLICY-SCARLET.md` and `POLICY-INDIGO.md` are both current published support
+commitments for this exact source snapshot. No precedence, supersession, or
+conflict-resolution rule has been authorized.
+
+Perform a source-only unsafe-code audit and state the strongest conclusion that
+can be justified without selecting a new support policy. Account for the
+effective configuration rejection in the source. `TCB.md` is an accepted human
+trust decision; apply it only to its exact build-tool mappings and keep it
+conspicuous. Use version-matched Rust Reference and standard-library
+documentation for material Rust propositions. Do not modify, build, run, or
+test the target.

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

@@ -0,0 +1,24 @@
+# Accepted build-tool premise
+
+## BUILD-MAP-C
+
+- **Disposition:** accepted by the authorized human reviewer for this target.
+- **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
+  `x86_64-unknown-linux-gnu`, `aarch64-unknown-linux-gnu`, or
+  `wasm32-unknown-unknown` sets `target_arch` to `x86_64`, `aarch64`, or
+  `wasm32`, respectively.
+- **Consumers:** only configuration reachability and effective-rejection proofs
+  for this target.
+- **Excluded propositions:** no Rust semantic fact, source-branch correctness,
+  compatibility outside the three exact releases, or backend/binary correctness
+  is admitted.
+- **Re-audit trigger:** any change to Cargo/toolchain identity, feature names,
+  target set, manifest, source cfgs, or human disposition.
+
+No other build-tool or implementation premise is accepted.

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

@@ -0,0 +1,22 @@
+#![no_std]
+
+#[cfg(all(feature = "turbo", target_arch = "wasm32"))]
+compile_error!("the turbo feature is not supported on wasm32");
+
+/// Returns the contained byte, or zero when `value` is `None`.
+#[cfg(not(feature = "turbo"))]
+pub fn value_or_zero(value: Option<u8>) -> u8 {
+    value.unwrap_or(0)
+}
+
+/// Returns the contained byte, or zero when `value` is `None`.
+#[cfg(feature = "turbo")]
+pub fn value_or_zero(value: Option<u8>) -> u8 {
+    if value.is_none() {
+        return 0;
+    }
+
+    // SAFETY: The `None` case returned above, so this value is `Some`.
+    unsafe { value.unwrap_unchecked() }
+}
+

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

@@ -0,0 +1,18 @@
+# Focused multi-issue review
+
+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
+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
+implementations and consumers; repository-visible use is not an exhaustive
+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.

evals/unsafe-rust/fixtures/v3-targeted/k_regression/lib.rs

@@ -0,0 +1,53 @@
+#![allow(dead_code)]
+
+pub mod callback_index {
+    pub trait Position {
+        fn position(&self) -> usize;
+    }
+
+    pub fn read<P: Position>(bytes: &[u8], position: &P) -> u8 {
+        unsafe { *bytes.get_unchecked(position.position()) }
+    }
+
+    pub fn write<P: Position>(bytes: &mut [u8], position: &P, value: u8) {
+        unsafe { *bytes.get_unchecked_mut(position.position()) = value }
+    }
+}
+
+pub mod local_proof {
+    pub fn last(bytes: &[u8]) -> Option<u8> {
+        if bytes.is_empty() {
+            None
+        } else {
+            let index = bytes.len() - 1;
+            // SAFETY: This is the fast path.
+            Some(unsafe { *bytes.get_unchecked(index) })
+        }
+    }
+}
+
+pub mod published_lane {
+    pub struct Word(pub [u32; 2]);
+
+    /// Identifies one of the two lanes in `Word`.
+    ///
+    /// # Safety
+    ///
+    /// `INDEX` must be less than 2. `NAME` must be `"low"` when `INDEX == 0`
+    /// and `"high"` when `INDEX == 1`.
+    pub unsafe trait Lane {
+        const INDEX: usize;
+        const NAME: &'static str;
+    }
+
+    pub struct High;
+
+    unsafe impl Lane for High {
+        const INDEX: usize = 1;
+        const NAME: &'static str = "high";
+    }
+
+    pub fn read<L: Lane>(word: &Word) -> u32 {
+        unsafe { *word.0.get_unchecked(L::INDEX) }
+    }
+}

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

@@ -0,0 +1,62 @@
+# Submitted evidence and applicability
+
+## `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`.
+
+## `store_word`
+
+The submitted authorities form two exact applicable cases:
+
+- [`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
+  old value, and its Safety section requires `dst` to be valid for writes and
+  properly aligned.
+- [`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:
+
+- [`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
+  not permit overlap. Its Safety section requires the source and destination
+  regions to be valid for the corresponding read and write, both pointers to
+  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: Copy`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/primitive.u8.html#impl-Copy-for-u8):
+  `u8` implements `Copy`.
+
+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.
+
+## `load_word`
+
+Only the two endpoint authorities are supplied:
+
+- [`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
+  unchanged. Its Safety section requires a non-ZST source to be valid for
+  reads, properly aligned, and properly initialized.
+- [`std::ptr::read`, Rust 1.82.0](https://doc.rust-lang.org/1.82.0/std/ptr/fn.read.html):
+  the same description and Safety propositions are supplied for the 1.82.0
+  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.
+- [`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.
+
+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.

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

@@ -0,0 +1,20 @@
+# Multi-release source-only review
+
+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.
+
+The authority entries and their claim-specific applicability are exactly those
+in `EVIDENCE.md`. The only non-authoritative admitted premises are the two
+accepted, narrowly scoped entries in `TCB.md`. Do not transfer an entry between
+different operations merely because their contracts or implementations look
+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.

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

@@ -0,0 +1,14 @@
+# Exact supported domains
+
+The audit cutoff is 2026-07-31. All listed releases, every target on which the
+item exists, and every ordinary debug or release profile are supported.
+
+The exact release predicates are:
+
+- `acknowledge`: `V_ack = {1.80.0, 1.80.1, 1.81.0, 1.82.0}`.
+- `store_word`: `V_store = {1.80.0, 1.81.0}`.
+- `copy_byte`: `V_copy = {1.80.0, 1.80.1, 1.81.0, 1.82.0}`.
+- `load_word`: `V_load = {1.80.0, 1.80.1, 1.81.0, 1.82.0}`.
+
+These are explicit finite sets, not notation for every release in a numeric
+interval. No other Rust release is in `Required` for this target.

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

@@ -0,0 +1,50 @@
+# Accepted TCB entries
+
+## SEM-EMPTY-BLOCK-180-182
+
+- **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.
+- **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.
+- **Exclusions:** this entry does not assert that `acknowledge` is sound, does
+  not describe any nonempty body, and establishes nothing about any pointer
+  operation or other API.
+- **Re-audit trigger:** any change to `V_ack`, the body of `acknowledge`, its
+  signature, its documented contract, or the human disposition.
+
+## COMPAT-COPY-180-182
+
+- **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`.
+- **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:
+  (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.
+- **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.
+- **Re-audit trigger:** any change to `V_copy`, the base proposition, the exact
+  source call, its type/count, or the human disposition.
+
+There is no entry other than `SEM-EMPTY-BLOCK-180-182` and
+`COMPAT-COPY-180-182`.

evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/lib.rs

@@ -0,0 +1,37 @@
+#![allow(dead_code)]
+
+/// Has no additional safety requirements.
+pub unsafe fn acknowledge() {}
+
+/// Stores `value` at `dst` without reading or dropping the old `u16`.
+///
+/// # Safety
+///
+/// `dst` must be properly aligned and valid for writes of one `u16`.
+pub unsafe fn store_word(dst: *mut u16, value: u16) {
+    // SAFETY: The caller guarantees exactly the preconditions of `ptr::write`.
+    unsafe { std::ptr::write(dst, value) }
+}
+
+/// Copies the byte at `src` to `dst` and preserves the source byte.
+///
+/// # Safety
+///
+/// `src` must be properly aligned, valid for reads of one `u8`, and point to an
+/// initialized `u8`; `dst` must be properly aligned and valid for writes of one
+/// `u8`; and the two one-byte regions must not overlap.
+pub unsafe fn copy_byte(src: *const u8, dst: *mut u8) {
+    // SAFETY: The caller guarantees every precondition for a one-element copy.
+    unsafe { std::ptr::copy_nonoverlapping(src, dst, 1) }
+}
+
+/// Reads and returns the initialized `u32` at `src` without changing it.
+///
+/// # Safety
+///
+/// `src` must be properly aligned, valid for reads of one `u32`, and point to
+/// a properly initialized `u32`.
+pub unsafe fn load_word(src: *const u32) -> u32 {
+    // SAFETY: The caller guarantees exactly the preconditions of `ptr::read`.
+    unsafe { std::ptr::read(src) }
+}

evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "quantifier-target"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+peer-unsafe-dep = "=3.4.5"