Freeze the V4 focused confirmation protocol

evals/unsafe-rust/fixtures/v4-focused/b_build/BUILD.md

@@ -0,0 +1,34 @@
+# Ordered allocator-selection build interface
+
+Supported builds use Cargo 1.85.1 and this crate's `build.rs`. The raw value of
+`FIXTURE_ALLOCATOR` has this complete partition:
+
+- an omitted variable and the Unicode value `system` are accepted and select
+  the `system` allocator;
+- the Unicode value `arena` is accepted and selects the `arena` allocator;
+- the Unicode value `arena-stop` is a deliberately rejected freshness canary;
+  the script writes the `arena` allocator directive and then panics;
+- every other Unicode value is rejected before an allocator directive is
+  attempted; and
+- every non-Unicode value is rejected before an allocator directive is
+  attempted.
+
+The script first attempts to write
+`cargo::rerun-if-env-changed=FIXTURE_ALLOCATOR`. It then reads and classifies
+the environment value. Each accepted path attempts exactly one
+`cargo::rustc-cfg=fixture_allocator="..."` write and returns successfully if
+that write succeeds. The `arena-stop` path attempts that same `arena` write and
+then panics. A failure of any stdout write makes that `println!` panic at that
+point; any earlier successfully written directive lines are therefore a
+partial output prefix of an unsuccessful script execution.
+
+The freshness guarantee is part of the supported build interface. In
+particular, after a successful `arena` build in a Cargo target directory,
+changing `FIXTURE_ALLOCATOR` to `arena-stop` must rerun the script and reject
+the current build. A previously compiled `arena` library is not a result of
+that current rejected build.
+
+Only a successful script execution for an accepted selector supplies an
+allocator configuration to a library compilation. Manually invoking `rustc`,
+inventing configuration options, or overriding the build script is outside the
+theorem.

evals/unsafe-rust/fixtures/v4-focused/b_build/Cargo.toml

@@ -0,0 +1,13 @@
+[package]
+name = "ordered-build-target"
+version = "0.1.0"
+edition = "2021"
+rust-version = "1.85.1"
+build = "build.rs"
+
+[features]
+default = []
+burst = []
+
+[lib]
+path = "src/lib.rs"

evals/unsafe-rust/fixtures/v4-focused/b_build/REQUEST.md

@@ -0,0 +1,35 @@
+# Ordered build-to-source unsafe-code audit
+
+Perform a source-only unsafe-code audit of the complete supplied crate,
+including its build script, build and support policies, generated configuration
+options, selected library source, public safe API, and documented panic
+postcondition.
+
+Recover the complete supported theorem domain. Then give the complete
+claim-relevant build relation in execution order, not merely its endpoint
+mapping. Account for every raw `FIXTURE_ALLOCATOR` class, every successful
+path, every explicit rejection, every stdout-write failure point, and every
+material partial emitted prefix and exit. Follow each emitted directive through
+its exact Cargo interpretation to the configuration options and library source
+that are selected, or prove why no current library compilation is produced.
+
+Audit the rerun/freshness sequence explicitly, including reuse of one Cargo
+target directory while changing `FIXTURE_ALLOCATOR` from `arena` to
+`arena-stop`. Separately prove or reject the project's target/allocator
+exclusion.
+
+Report the strongest soundness and documented-postcondition verdicts. The
+report must also state and prove the **exact maximal sound region over the full
+supported configuration product and every `u8` API input**, rather than giving
+only one counterexample or a non-maximal positive remainder. Symbolic formulas
+and parametric proofs are welcome; Cartesian enumeration is not required.
+
+`TCB.md` is an accepted human trust decision for only the exact Cargo,
+freshness, process-status, feature, and target-cfg propositions it names. Keep
+every consumed part explicit and do not widen it. Verify every material Rust
+proposition against narrowly scoped, version-matched Rust Reference or
+standard-library documentation: cite its exact URL and quote the relied-upon
+text. Cargo documentation may be used to review the accepted Cargo premise but
+is not a Rust semantic axiom.
+
+Do not modify, build, run, or test the target.

evals/unsafe-rust/fixtures/v4-focused/b_build/SUPPORT.md

@@ -0,0 +1,23 @@
+# Supported configurations
+
+This snapshot supports Rust 1.85.1 on these target triples:
+
+- `x86_64-unknown-linux-gnu`;
+- `aarch64-unknown-linux-gnu`; and
+- `wasm32-unknown-unknown`.
+
+Both states of the `burst` feature and both allocator models (`system` and
+`arena`, selected as specified in `BUILD.md`) are supported, with exactly one
+exclusion: `arena` is unsupported on `wasm32-unknown-unknown`, regardless of
+the `burst` feature. The source must reject that excluded target/allocator
+pair.
+
+Every other combination of the listed target, feature state, and allocator is
+supported in every Cargo profile, with either state of debug assertions.
+
+An allocator model is selected only by an accepted raw environment value from
+`BUILD.md`. The rejected `arena-stop`, other-Unicode, and non-Unicode classes
+are build-interface rejection cases, not additional allocator models or
+supported library configurations. A build rejected by a build-script failure
+or by the required wasm32/arena source error must not supply a current library
+artifact to downstream users.

evals/unsafe-rust/fixtures/v4-focused/b_build/TCB.md

@@ -0,0 +1,47 @@
+# Accepted build-tool premise
+
+## BUILD-MAP-ORDERED
+
+- **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:** for every supported Cargo profile, Cargo executes this
+  build script when required for the selected build. A successfully written
+  `cargo::rerun-if-env-changed=FIXTURE_ALLOCATOR` line records that a later
+  change in the raw value (including present-to-present changes) makes the
+  prior selection stale and causes the script to run again before Cargo can
+  select a library for the current build. Cargo interprets a successfully
+  written `cargo::rustc-cfg=fixture_allocator="VALUE"` line from a build script
+  that subsequently exits successfully by passing that exact key/value
+  configuration option to this library compilation. Such a current library
+  compilation receives exactly the `fixture_allocator` directives emitted by
+  that successful current script execution and no retained selector from an
+  earlier execution. Cargo does not compile the library when the build-script
+  process exits unsuccessfully, even if stdout already contains one or more
+  complete directive lines. It does not present a library from an earlier
+  successful selector value as the result of the current stale, unsuccessful
+  build. An uncaught panic of this exact build script's main thread is an
+  unsuccessful process exit.
+
+  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.
+- **Execution scope:** successful-selector emission claims quantify over build
+  attempts whose applicable stdout writes succeed and whose script returns
+  successfully. An execution ending in a write failure or explicit panic
+  produces no library compilation for that current build; any emitted prefix
+  does not create a compiled configuration. Such an execution is not an
+  accepted selector success, and an incidental write failure is not a new raw
+  selector class.
+- **Consumers:** only ordered build-output interpretation, freshness,
+  allocator/feature/target reachability, selected source, and effective
+  rejection for this target.
+- **Excluded propositions:** no claim about which string the local build script
+  emits or in which order, source correctness, Rust abstract semantics, a
+  backend, or a binary is admitted.
+- **Re-audit trigger:** any change to Cargo/toolchain identity, manifest,
+  `build.rs`, environment interface, target set, source cfgs, or human
+  disposition.
+
+No other build-tool or implementation premise is accepted.

evals/unsafe-rust/fixtures/v4-focused/b_build/build.rs

@@ -0,0 +1,27 @@
+use std::env;
+
+fn main() {
+    println!("cargo::rerun-if-env-changed=FIXTURE_ALLOCATOR");
+
+    match env::var("FIXTURE_ALLOCATOR") {
+        Err(env::VarError::NotPresent) => {
+            println!("cargo::rustc-cfg=fixture_allocator=\"system\"");
+        }
+        Ok(value) => match value.as_str() {
+            "system" => {
+                println!("cargo::rustc-cfg=fixture_allocator=\"system\"");
+            }
+            "arena" => {
+                println!("cargo::rustc-cfg=fixture_allocator=\"arena\"");
+            }
+            "arena-stop" => {
+                println!("cargo::rustc-cfg=fixture_allocator=\"arena\"");
+                panic!("arena-stop rejects this build after allocator emission");
+            }
+            _ => panic!("unsupported FIXTURE_ALLOCATOR value"),
+        },
+        Err(env::VarError::NotUnicode(_)) => {
+            panic!("FIXTURE_ALLOCATOR must be valid Unicode");
+        }
+    }
+}

evals/unsafe-rust/fixtures/v4-focused/b_build/src/lib.rs

@@ -0,0 +1,34 @@
+use std::num::NonZeroU8;
+
+#[cfg(all(target_arch = "wasm32", fixture_allocator = "arena"))]
+compile_error!("the arena allocator is unsupported on wasm32");
+
+/// Constructs a lane identifier.
+///
+/// # Panics
+///
+/// Panics when `value` is zero.
+pub fn lane_id(value: u8) -> NonZeroU8 {
+    #[cfg(all(
+        feature = "burst",
+        target_arch = "aarch64",
+        fixture_allocator = "arena"
+    ))]
+    {
+        // SAFETY: Burst-mode lane identifiers are never zero.
+        return unsafe { NonZeroU8::new_unchecked(value) };
+    }
+
+    #[cfg(not(all(
+        feature = "burst",
+        target_arch = "aarch64",
+        fixture_allocator = "arena"
+    )))]
+    {
+        if value == 0 {
+            panic!("lane identifier must be nonzero");
+        }
+        // SAFETY: The preceding branch proves that `value != 0`.
+        unsafe { NonZeroU8::new_unchecked(value) }
+    }
+}

evals/unsafe-rust/fixtures/v4-focused/l_proof/REQUEST.md

@@ -0,0 +1,21 @@
+# Local proof-artifact review
+
+Audit `last` in `lib.rs` without editing it. Determine the implementation's
+soundness separately from the adequacy of the existing `SAFETY` comment. If
+you must reconstruct any material part of the proof to reach your verdict,
+show that reconstruction and provide replacement comment text which would
+make the proof locally reviewable.
+
+Inventory every Rust semantic or standard-library premise materially consumed
+by your proof. For each such premise, give a narrowly scoped, version-matched
+authoritative citation, quote the exact prose which supplies it, and state the
+exact proposition you verified there.
+Reconcile that inventory against the premises used in the derivation; do not
+list citations which the proof does not consume, or silently consume Rust
+facts which the inventory does not establish.
+
+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.
+
+Do not build, test, or execute the target.

evals/unsafe-rust/fixtures/v4-focused/l_proof/lib.rs

@@ -0,0 +1,11 @@
+#![allow(dead_code)]
+
+pub fn last(bytes: &[u8]) -> Option<&u8> {
+    if bytes.is_empty() {
+        None
+    } else {
+        let index = bytes.len() - 1;
+        // SAFETY: The returned reference cannot outlive `bytes`.
+        Some(unsafe { bytes.get_unchecked(index) })
+    }
+}

evals/unsafe-rust/fixtures/v4-focused/p_predicates/Cargo.toml

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

evals/unsafe-rust/fixtures/v4-focused/p_predicates/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/v4-focused/p_predicates/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/v4-focused/p_predicates/REQUEST.md

@@ -0,0 +1,37 @@
+# Focused predicate and full-case source review
+
+`POLICY-SCARLET.md` and `POLICY-INDIGO.md` are both current published support
+commitments for this exact source snapshot. No precedence, supersession,
+intersection, union, or other conflict-resolution rule has been authorized.
+
+Perform a source-only unsafe-code audit and state the strongest conclusions
+that the supplied evidence justifies. Your report must do all of the following:
+
+1. Reproduce the exact Scarlet and Indigo configuration predicates separately.
+   Determine their exact equality/containment relationship, giving one concrete
+   separating configuration in each direction if neither contains the other.
+2. Use a full audit case
+   `(version, target, turbo, hardened, profile, debug_assertions, input)`, where
+   `input` ranges over every valid `Option<u8>`. Define the full-case domain
+   induced by each policy.
+3. Select and state a conservative full-case audit domain which contains both
+   policy-induced full-case domains. Prove each containment separately. Do not
+   describe the selected audit domain as the crate's exact support promise:
+   the identity of that promise remains a separate question governed only by
+   the two supplied policy documents and their lack of a precedence rule.
+4. Account for both policy-level exclusion and source-level effective rejection
+   of every `turbo`/`wasm32` case.
+5. Prove or refute the local safety obligation at the unsafe operation and the
+   documented `value_or_zero` postcondition on each selected source branch.
+6. State `Required(case)` and the applicable soundness and behavioral
+   `Covered(case)` predicates without projecting away the configuration or
+   input dimensions. Give the set-containment argument needed for each
+   whole-domain conclusion. A symbolic argument over dimensions which are
+   genuinely irrelevant is preferred to enumerating their values.
+
+`TCB.md` records an accepted human trust decision. Apply it only to its exact
+build-tool mappings and consumers, and keep every conclusion which depends on
+it conspicuously qualified. For each material Rust semantic premise, cite the
+applicable exact-version Rust Reference or standard-library page and quote the
+prose which supplies that premise. Do not modify, build, run, or test the
+target.

evals/unsafe-rust/fixtures/v4-focused/p_predicates/TCB.md

@@ -0,0 +1,24 @@
+# Accepted build-tool premise
+
+## BUILD-MAP-POLICY
+
+- **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 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.
+- **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.