Collect the V3 targeted confirmation reports

evals/unsafe-rust/runs/2026-07-31-v3-targeted/collection/attempts/r001/1/attestation.json

@@ -0,0 +1,19 @@
+{
+  "agent_id": "/root/report_r001",
+  "api_state": "COMPLETED",
+  "attempt": 1,
+  "canonical_for_scoring": true,
+  "operational_scope_deviation": false,
+  "recorded_utc": "2026-08-01T03:26:35.837282Z",
+  "report_sha256": "4a8554d2840bc21e1a1da10ff8c50dc52fb362117b24e0d30e3359864a3db4b9",
+  "run_id": "r001",
+  "schema_version": 1,
+  "scope_evidence": "No known operational source-scope deviation.",
+  "semantic_noncompletion": false,
+  "source_isolation": "procedural",
+  "terminal_disposition": "COMPLETE",
+  "utf8": true,
+  "within_word_cap": true,
+  "word_cap": 1800,
+  "word_count": 766
+}

evals/unsafe-rust/runs/2026-07-31-v3-targeted/collection/attempts/r001/1/report.md

@@ -0,0 +1,104 @@
+# Focused source-only unsafe Rust review
+
+## Claim frame and results
+
+The audited source is `lib.rs` SHA-256
+`778d644359b84bc0e519ed7220bfcadfbba578e2c9fd4c474ce742c4b0021ceb`,
+together with the submitted manifest, dependency declaration, evidence policy,
+request, and TCB decision. The manifest selects edition 2021 and exactly
+`peer-unsafe-dep =3.4.5`. No dependency implementation, generated output,
+prior audit, or binary was supplied.
+
+Let **C** be: Rust compiler and standard library exactly 1.80.0; every target
+on which this source and that exact dependency resolve; and every ordinary
+debug or release profile. These are source-level Rust-abstract-semantics
+claims, not compiler-backend or binary claims.
+
+| Exported API | Exact valid uses | Soundness claim and strongest verdict |
+|---|---|---|
+| `pub fn force_unreachable()` | Every well-typed safe invocation; there is no caller safety precondition. | Every execution of every valid use in C is UB-free: **UNSOUND**, relative to TCB-R1. |
+| `pub unsafe fn delegated_nonzero(value: u8) -> u8` | Every invocation whose caller ensures `value != 0`; the contract states no ongoing or terminal obligation. | Every execution of every valid use in C is UB-free: **UNPROVED**, relative to TCB-R1. |
+
+Thus there is no combined `PROVED` result. The conjunction that both exports
+are sound is refuted by the first API, while the second API retains its own
+`UNPROVED` status.
+
+## API and boundary coverage
+
+The complete exported surface in `lib.rs` is the two public free functions
+above. There are no exported fields, constructors, types, traits, methods,
+statics, macros, reexports, hidden items, FFI declarations, or generated APIs.
+The relevant unsafe consumers are the call to
+`std::hint::unreachable_unchecked` and the call across the unsafe dependency
+boundary. `#![allow(dead_code)]` only changes linting.
+
+## Proof S1 — `force_unreachable`
+
+1. A direct safe call `force_unreachable()` is a well-typed valid use.
+2. On entry, the body has no branch, check, or earlier diverging operation. It
+   immediately evaluates `std::hint::unreachable_unchecked()`; therefore that
+   site is reached.
+3. Verified Rust 1.80.0 standard-library authority states: “Reaching this
+   function is Undefined Behavior.”
+   ([Safety section](https://doc.rust-lang.org/1.80.0/std/hint/fn.unreachable_unchecked.html#safety)).
+4. Consequently the valid safe invocation is a complete in-scope UB witness.
+
+The derivation is parametric over C: neither the source control flow nor the
+verified proposition has a target or ordinary-profile qualification. The
+existing comment, “This site is assumed to be unreachable,” is circular and
+false whenever the exported function is invoked; it proves no precondition.
+No comment-only repair can make this safe implementation sound. A resolution
+must remove the unchecked operation (for example, use a defined panic) or
+enforce an appropriate boundary; a safe API cannot impose a hidden
+unreachability obligation on callers.
+
+## Proof S2 — `delegated_nonzero`
+
+For an arbitrary valid call, let the input be `v: u8` with `v != 0`. The
+wrapper performs no mutation or conversion and passes that same `v` to
+`peer_unsafe_dep::duplicate_nonzero`. The submitted dependency contract's
+caller-side requirement is exactly `value != 0`. Thus the wrapper's documented
+precondition and unchanged dataflow completely discharge the local unsafe-call
+precondition, throughout C. The adjacent safety comment adequately identifies
+this local derivation.
+
+That does not prove the unsafe callee's provider obligation. The smallest
+missing soundness proposition is:
+
+> For exact `peer-unsafe-dep` 3.4.5, on every configuration in C, for every
+> `v: u8` with `v != 0`, every permitted execution of
+> `duplicate_nonzero(v)` is free from Rust undefined behavior.
+
+Neither declaration nor documentation proves that implementation theorem. The
+implementation is unavailable, and the human trust decision explicitly
+declines an `UNSAFE-DEP` admission. Exact pinning fixes identity but not
+correctness. Therefore the wrapper claim is `UNPROVED`; no valid UB witness was
+supplied, so `UNSOUND` is not justified.
+
+The wrapper itself does not explicitly promise result equality. The submitted
+dependency contract separately says it returns `value`; that provider
+postcondition is not consumed by S2, but its implementation status is also
+`UNPROVED`. Its smallest missing proposition is that every UB-free normal
+return for the same domain yields exactly `v`.
+
+## Configuration closure and TCB-R1
+
+There are no declared Cargo features or source `cfg` branches. Target and
+profile are the only stated axes. S1 is covered parametrically across them; the
+local part of S2 is likewise parametric, but the missing dependency proposition
+blocks all of C. No build, execution, test, expansion, or tool-derived evidence
+was used.
+
+TCB-R1 contains one accepted entry:
+
+- **AXIOM-UU-1:** for Rust/std 1.80.0 throughout C, reaching
+  `unreachable_unchecked` is UB. Identity and wording were independently
+  verified at the exact versioned page above. Consumers: S1. Re-audit on a
+  Rust version/domain or cited-contract change.
+
+There are no accepted implementation, compatibility, tool, or deployment
+entries. The proposed dependency-implementation proposition is deliberately
+unavailable/rejected and supports no proof. Re-audit S2 if dependency source is
+audited or the exact proposition is explicitly accepted; re-audit either claim
+on source, safety-contract, dependency identity, supported-domain, TCB, or Rust
+authority changes.

evals/unsafe-rust/runs/2026-07-31-v3-targeted/collection/attempts/r002/1/attestation.json

@@ -0,0 +1,19 @@
+{
+  "agent_id": "/root/report_r002",
+  "api_state": "COMPLETED",
+  "attempt": 1,
+  "canonical_for_scoring": true,
+  "operational_scope_deviation": false,
+  "recorded_utc": "2026-08-01T03:28:46.424312Z",
+  "report_sha256": "d91ac2821d69b57dd7bd98303059093769e6e2b6b99226936b2bf4edc90cdd32",
+  "run_id": "r002",
+  "schema_version": 1,
+  "scope_evidence": "No known operational source-scope deviation.",
+  "semantic_noncompletion": false,
+  "source_isolation": "procedural",
+  "terminal_disposition": "COMPLETE",
+  "utf8": true,
+  "within_word_cap": true,
+  "word_cap": 1800,
+  "word_count": 872
+}

evals/unsafe-rust/runs/2026-07-31-v3-targeted/collection/attempts/r002/1/report.md

@@ -0,0 +1,53 @@
+# Unsafe Rust Audit: `symbolic-domain-target` complete supplied snapshot
+
+## Claims and verdicts
+
+Let `D` be all tuples `(r,t,f,p,d)` where `r` is a released stable Rust toolchain and `1.84.0 <= r <= 1.86.0`; `t` is `x86_64-unknown-linux-gnu`, `aarch64-apple-darwin`, or `wasm32-unknown-unknown`; `f` is either state of `telemetry`; `p` is any Cargo profile; and `d` is either debug-assertion state.
+
+| Claim | Exact source-level theorem for every configuration in `D` and every well-typed safe call | Verdict |
+|---|---|---|
+| SOUND | `value_or_zero` executes without Rust undefined behavior | **PROVED relative to accepted TCB entry `COMPAT-OPTION-184-186`** |
+| RESULT | `None` returns `0`; `Some(v)` returns `v` | **PROVED relative to accepted TCB entry `COMPAT-OPTION-184-186`** |
+
+**Combined mandatory result: PROVED over exactly `D`, relative to `COMPAT-OPTION-184-186`.** This is an abstract Rust source theorem, not a compiler/backend or emitted-binary theorem.
+
+## Snapshot and scope
+
+The complete supplied package is edition 2021, `#![no_std]`, has no dependencies or build script, and contains one library source file. Relevant SHA-256 identities are: `src/lib.rs` `6a9db5bc51aa3c0fb1e966509de396cee5d451cb93f4295224d5772f22f838f8`; `Cargo.toml` `7e25c6b1489e215d6e4ecdc8b7beea11fc35237b3207fb01e836e6c7b4e818f6`; `SUPPORT.md` `45ee272e31a71fe28da355624691db55439d234c92ae8be5ce1af460aed4069c`; and `TCB.md` `db2ecc86f6e93d8e7ed6dd3df2c01cf0e5a80580a121341a5409f6888c2de413`. `REQUEST.md`, `CI.md`, and every supplied target file were reviewed. Audit cutoff: 2026-08-01. No code was generated, expanded, built, run, or tested; no prior audit was reused.
+
+## Domain recovery and configuration closure
+
+`SUPPORT.md` is explicit that its closed toolchain interval, including the upper cutoff, is the project commitment. Its predicate is crossed with the three enumerated targets, both feature states, every profile, and both debug-assertion states; this is exactly `D`, with no normalization to a finite release inventory. `Cargo.toml`'s `rust-version = "1.84"` is expressly only Cargo's minimum and is consistent with, but does not replace, that policy. `CI.md` lists samples only and supplies neither domain membership nor semantic proof.
+
+The source has no `cfg`, feature-conditioned item, profile-dependent check, arithmetic, target operation, dependency, macro, FFI, assembly, allocation, concurrency, or generated artifact. Its proof is therefore parametric in `t`, `f`, `p`, and `d`. Version coverage is parametric in `r` through the accepted TCB entry, rather than inferred from endpoints or sampled documentation.
+
+For every `c in D`, the proof below covers both valid `Option<u8>` variants. Hence each obligation's `Covered` predicate is `D`; their pointwise intersection is `D`, and `Required = D subseteq Covered = D`. No supported configuration is excluded or unresolved.
+
+## Boundary, invariant, and obligation ledger
+
+The only crate-defined language-reachable API is the safe free function `pub fn value_or_zero(Option<u8>) -> u8`. There are no public fields or types, crate constructors, traits/impls, methods, statics, macros, reexports, hidden items, callbacks, FFI entrypoints, or configuration-specific APIs. The sole unsafe surface is the internal call `value.unwrap_unchecked()`.
+
+The only invariant is transient `FALLTHROUGH-SOME`: from completion of the false `is_none` branch until the consuming unsafe call, the owned, immutable local `value` is `Some(v)`. It is established by the branch and `COMPAT-OPTION-184-186`; no assignment, alias-capable callback, or other operation intervenes.
+
+| Obligation | Required proposition | Derivation and status |
+|---|---|---|
+| O1 branch classification | `is_none` distinguishes `None` from `Some(v)` | The accepted entry preserves the exact classification throughout `D`. **PROVED** |
+| O2 unsafe precondition | the receiver of `unwrap_unchecked` is not `None` | Only fallthrough reaches the call; O1 and unchanged ownership establish `FALLTHROUGH-SOME`. **PROVED** |
+| O3 unsafe result | `unwrap_unchecked(Some(v))` returns `v` | The accepted entry preserves this base proposition throughout `D`. **PROVED** |
+| O4 documented result | `None -> 0`, `Some(v) -> v` | `None` returns before unsafe; `Some(v)` uses O2/O3. **PROVED** |
+
+The adjacent `SAFETY` comment identifies the dominating return, derives `Some`, and names the callee precondition; it is adequate. Full case proof: for `None`, O1 makes the condition true and the function returns `0` without reaching unsafe code. For `Some(v)`, O1 makes it false; the immutable value remains `Some(v)`; O2 permits the unsafe call and O3 returns `v`. These cases exhaust valid safe inputs, proving UB freedom and the complete documented behavior.
+
+## TCB audit log
+
+**Log identity:** supplied `TCB.md`, SHA-256 above. **Trust policy:** only its authorized, accepted proposition is admitted; no implementation, compiler, dependency, or environmental premise is added.
+
+`COMPAT-OPTION-184-186` is accepted by the authorized human reviewer. Its base authorities are the Rust 1.84.0 [`Option::is_none`](https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.is_none) and [`Option::unwrap_unchecked`](https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.unwrap_unchecked) pages. Verified relevant text states: “Returns true if the option is a None value”; “Returns the contained Some value”; and “Calling this method on None is undefined behavior.” The entry admits that the exact classification and `Some(v)` result/`None` UB propositions are preserved, without weakening, for every `r` and configuration in `D`. Consumers are O1–O4 only. It establishes neither interval membership nor Cargo/compiler/backend facts. Re-audit is required for any source, support interval, base proposition, feature/target scope, or human-disposition change. No rejected, pending, unused, or additional entries exist.
+
+## Evidence, findings, and residual scope
+
+No tool-derived evidence was used. **Findings: none.** Every required obligation is proved; there is no documentation gap, unresolved domain, or postcondition failure.
+
+Excluded from this source theorem are invalid values created by out-of-scope unsafe caller behavior, unsupported configurations, compiler/backend correctness, emitted binaries, and deployment properties. Re-audit on any source/API/documentation change, support/configuration expansion, material authoritative-document change, or change to `COMPAT-OPTION-184-186`.
+
+Final attestation: all safe and unsafe surfaces, target files, controlling domain expressions, mandatory postconditions, premise applicability, and TCB consumers have a disposition; `Required subseteq Covered` is established; the verdict does not rely on CI, tests, or absence of a counterexample.

evals/unsafe-rust/runs/2026-07-31-v3-targeted/collection/attempts/r003/1/attestation.json

@@ -0,0 +1,19 @@
+{
+  "agent_id": "/root/report_r003",
+  "api_state": "COMPLETED",
+  "attempt": 1,
+  "canonical_for_scoring": true,
+  "operational_scope_deviation": false,
+  "recorded_utc": "2026-08-01T03:28:56.151974Z",
+  "report_sha256": "52351c5c0755e56dc544a5814cc0bfaeb51f1cf6000e4db4a24ab2699e927812",
+  "run_id": "r003",
+  "schema_version": 1,
+  "scope_evidence": "No known operational source-scope deviation.",
+  "semantic_noncompletion": false,
+  "source_isolation": "procedural",
+  "terminal_disposition": "COMPLETE",
+  "utf8": true,
+  "within_word_cap": true,
+  "word_cap": 1800,
+  "word_count": 921
+}