Collect all V4 focused audit reports

evals/unsafe-rust/runs/2026-08-01-v4-focused/collection/attempts/r001/1/attestation.json

@@ -0,0 +1,19 @@
+{
+  "agent_id": "/root/v4_report_r001",
+  "api_state": "COMPLETED",
+  "attempt": 1,
+  "canonical_for_scoring": true,
+  "operational_scope_deviation": false,
+  "recorded_utc": "2026-08-01T18:07:30.630418Z",
+  "report_sha256": "6a1aad4f07b372199c6b991e19332f67e30230c93e695d407ce30d97d0fc5df4",
+  "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": 910
+}

evals/unsafe-rust/runs/2026-08-01-v4-focused/collection/attempts/r001/1/report.md

@@ -0,0 +1,131 @@
+# Focused source-only unsafe Rust review
+
+## Claim frame and domain
+
+Snapshot: the submitted `Cargo.toml`, `lib.rs`, `DEPENDENCY-API.md`,
+`EVIDENCE.md`, and `TCB.md`. Scope is the two exported functions and their two
+unsafe calls. There are no exported fields, types, traits, implementations,
+macros, statics, callbacks, FFI surfaces, conditional items, or generated
+artifacts in the packet. No prior audit, dependency implementation, expansion,
+binary, or tool result is reused.
+
+Let `T` be exactly the targets on which this source and the resolved
+`peer-unsafe-dep` 3.4.5 compile, and let `P = {ordinary debug, ordinary
+release}`. The controlling request and manifest give
+
+`C = { (Rust 1.80.0, edition 2021, target t, profile p,
+peer-unsafe-dep =3.4.5) | t in T, p in P }`.
+
+This is retained symbolically: no finite target inventory is asserted.
+`Required_cfg = C`. There are no source `cfg`s or features to partition. The
+manifest's exact version requirement and the submitted resolution statement
+establish the dependency version selected; they establish no proposition about
+its body. The target predicate and profiles come verbatim from `REQUEST.md`, so
+normalization to `C` holds in both directions by definition. The audit cutoff
+is 2026-08-01; the supplied policy is static.
+
+For `force_unreachable`, `Required_F` contains every `c in C` and every
+well-typed safe invocation and permitted execution of the function. There is
+no caller safety precondition. For `delegated_nonzero`, `Required_D` contains
+every `c in C`, every `v: u8` with `v != 0`, and every permitted execution of
+an unsafe invocation whose documented obligation is satisfied. No ongoing or
+terminal caller obligation is documented.
+
+## Authority and trust boundary (`TCB-PACKET-1`)
+
+`AXIOM-UU-180` is accepted exactly as directed by `TCB.md`. The checked Rust
+1.80.0 standard-library Safety section says: “Reaching this function is
+Undefined Behavior.” It states no target or profile qualification, so the
+packet applies it throughout `C`.
+[Versioned source](https://doc.rust-lang.org/1.80.0/std/hint/fn.unreachable_unchecked.html#safety).
+
+No `UNSAFE-DEP` proposition for `peer-unsafe-dep` 3.4.5 is accepted; the human
+trust decision expressly declines it. No other implementation, compatibility,
+tool, environment, or deployment proposition is admitted. The submitted peer
+documentation is the caller/provider contract, not evidence that its
+unavailable unsafe implementation fulfills that contract.
+
+## Claim F — `force_unreachable`
+
+**Soundness verdict: UNSOUND over all of `Required_F`, relative to
+`TCB-PACKET-1`.**
+
+Existential UB certificate (indeed parametric in every `c in C`):
+
+1. **Valid use.** `force_unreachable` is a public safe function with no
+   arguments or stated precondition, so a safe call `force_unreachable()` is a
+   valid in-scope use.
+2. **Reachability.** Once invoked, its body has no check or alternative exit;
+   `lib.rs:6` evaluates `std::hint::unreachable_unchecked()`.
+3. **False required safety proposition.** The call site is therefore reached.
+   The operation requires that it not be reached.
+4. **UB consequence.** `AXIOM-UU-180` directly classifies reaching the function
+   as undefined behavior.
+
+These facts do not vary with target or profile, and the axiom covers all of
+`C`; thus each required configuration has the witness. The line 5 safety
+comment merely assumes the proposition disproved by ordinary invocation. It
+is not a proof and cannot be repaired with stronger prose: the implementation
+must remove the call (for example, use defined panic/divergence) or remove the
+safe callable behavior.
+
+The descriptive sentence at line 3 supplies no separate defined-behavior
+postcondition. Because the witness execution contains UB, it cannot establish
+`CONTRACT-BROKEN`.
+
+## Claim D — `delegated_nonzero`
+
+**Soundness verdict: UNPROVED over `Required_D`, relative to
+`TCB-PACKET-1`.**
+
+The complete local call-site derivation is:
+
+1. A valid wrapper use supplies `v != 0` by `lib.rs:13`.
+2. Line 17 passes that same `u8` value, without a transition, to
+   `duplicate_nonzero`.
+3. The submitted peer safety contract requires exactly `value != 0`.
+   Therefore the wrapper discharges the peer's caller-side precondition for
+   every `v` in `1..=255` and every `c in C`. The local safety comment is
+   correct for that obligation.
+4. Soundness additionally requires the exact peer implementation to be free
+   of UB for every such valid call. Neither the caller precondition nor the
+   declaration proves provider correctness.
+
+The smallest missing proposition is:
+
+`DEP-SOUND`: for every `c in C` and `v: u8` with `v != 0`, every permitted
+execution of `peer-unsafe-dep` 3.4.5's exact `duplicate_nonzero(v)`
+implementation is free of Rust undefined behavior.
+
+The dependency body/generated output is absent, no assertion about its
+executions is supplied, and `TCB.md` rejects admission of this proposition.
+Consequently the implementation obligation's covered domain is not shown to
+contain `Required_D`; `Required_D subseteq Covered_D` cannot be certified.
+There is also no valid execution showing that `DEP-SOUND` is false, so the
+stronger `UNSOUND` certificate is unavailable.
+
+The peer contract additionally promises to return `value`. That provider
+postcondition is likewise unverified for the unavailable implementation. The
+wrapper documents delegation but no explicit equality postcondition of its
+own. No UB-free postcondition counterexample is supplied, so
+`CONTRACT-BROKEN` is not established.
+
+Minimum resolution: submit and recursively audit the exact dependency
+implementation and any generated output over `C`, or obtain human acceptance
+of a precise `UNSAFE-DEP` entry covering `DEP-SOUND` (and the return guarantee
+if it is consumed). An exact version pin alone is insufficient.
+
+## Obligation closure
+
+| ID | Obligation | Status |
+|---|---|---|
+| F-CALL | `unreachable_unchecked` is not reached | False; complete UB certificate above |
+| D-PRE | argument passed to peer is nonzero | Proved for all `Required_D` |
+| D-IMPL | valid peer call is UB-free | Unproved: `DEP-SOUND` missing |
+| D-RET | peer valid call returns its input | Unproved provider guarantee; not an explicit wrapper postcondition |
+
+Combined result: `force_unreachable` is **UNSOUND**; `delegated_nonzero` is
+**UNPROVED**. There is no tool-derived evidence and no binary/backend theorem.
+Re-audit on any source or contract change, support-domain change, Rust or cited
+documentation change, dependency identity/body/generated-output change, or
+new TCB disposition.

evals/unsafe-rust/runs/2026-08-01-v4-focused/collection/attempts/r002/1/attestation.json

@@ -0,0 +1,19 @@
+{
+  "agent_id": "/root/v4_report_r002",
+  "api_state": "COMPLETED",
+  "attempt": 1,
+  "canonical_for_scoring": true,
+  "operational_scope_deviation": false,
+  "recorded_utc": "2026-08-01T18:11:26.122348Z",
+  "report_sha256": "2f12ab5921c09f2eaf84d142758c151a33e35e8868fb9d7e0ddb3e1b15667c50",
+  "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": 907
+}

evals/unsafe-rust/runs/2026-08-01-v4-focused/collection/attempts/r002/1/report.md

@@ -0,0 +1,57 @@
+# Focused unsafe-Rust source review
+
+## Claim, snapshot, and domain
+
+The audited artifact is the submitted `lib.rs` for `quantifier-target` 0.1.0, edition 2021, together with `Cargo.toml`, `DEPENDENCY-API.md`, `EVIDENCE.md`, and `TCB.md`. The manifest pins `peer-unsafe-dep = "=3.4.5"`. No dependency implementation, generated output, binary, prior audit, or tool-derived result was supplied or inspected.
+
+Let
+
+`D = {(t,p) | Rust/stdlib = 1.80.0, this source and peer-unsafe-dep 3.4.5 resolve on target t, and p is an ordinary debug or ordinary release profile}`.
+
+This is the controlling `Required` predicate from `REQUEST.md`; it is retained symbolically rather than replaced by an unproved target inventory. There are no `cfg`, feature, generated-source, target, or profile branches in `lib.rs`. Thus its two function bodies are identical throughout `D`. The exact dependency implementation may vary only within the resolution already quantified by `D`; its absence matters to Claim 2. Audit cutoff: this submitted source/evidence snapshot on 2026-08-01.
+
+The complete exported surface is the safe free function `force_unreachable` and unsafe free function `delegated_nonzero`. There are no exported fields, constructors, types, traits/impls, statics, macros, hidden items, callbacks, FFI declarations, or owned representation invariants in the submitted source.
+
+## Verdicts
+
+| Claim | Valid-use domain | Compilation domain | Verdict |
+|---|---|---|---|
+| C1: every permitted execution of `force_unreachable()` is free of Rust UB | Every well-typed safe invocation; there is no caller safety precondition | `D` | **UNSOUND**, on every member of `D` |
+| C2: every permitted execution of `delegated_nonzero(value)` is free of Rust UB | Unsafe invocations with a valid `u8` value satisfying the complete documented obligation `value != 0`, i.e. `value in 1..=255`; no ongoing or terminal obligation is documented | `D` | **UNPROVED** |
+
+## C1 proof and UB certificate
+
+`lib.rs:4` exposes `force_unreachable` as safe. Therefore a safe caller may directly invoke it, and that invocation is a valid in-scope use. Its body has no branch, check, argument, callback, or earlier operation: control reaches the call to `std::hint::unreachable_unchecked()` at `lib.rs:6`.
+
+Accepted TCB entry **AXIOM-UU-180** is the verified Rust 1.80.0 standard-library Safety statement: “Reaching this function is Undefined Behavior.” ([exact versioned page](https://doc.rust-lang.org/1.80.0/std/hint/fn.unreachable_unchecked.html#safety)). The submitted evidence and accepted trust decision give this proposition every-target/ordinary-profile applicability, hence all of `D`.
+
+Thus, for each `(t,p) in D`: (1) a direct safe call is valid; (2) source control flow necessarily executes the unsafe operation; (3) its required proposition, that the call site is unreachable, is false because the invocation reached it; and (4) AXIOM-UU-180 entails UB. This is a complete existential refutation for each configuration, stronger than merely failing a universal proof. The `SAFETY` comment “assumed to be unreachable” supplies no premise and is contradicted by the public safe entry path.
+
+Minimum repair: remove the unchecked operation (for example, use a defined panic path) or establish an actually enforced control-flow invariant before it. Documentation alone cannot impose a hidden precondition on this safe API.
+
+## C2 derivation and smallest gap
+
+For every valid C2 call, `value != 0` holds by the exported unsafe contract at `lib.rs:11-14`. The wrapper passes that same, unchanged `value` to `peer_unsafe_dep::duplicate_nonzero` at `lib.rs:17`. The submitted exact 3.4.5 dependency declaration requires precisely `value != 0`. Therefore the local caller-side safety obligation for the dependency call is proved throughout `D`; the adjacent `SAFETY` comment accurately states this part.
+
+That is not a proof of the unsafe dependency provider. A third-party unsafe call additionally requires the exact implementation to uphold its contract for every valid call. `DEPENDENCY-API.md` expressly says its implementation and generated output are absent and supplies no assertion about its body. `TCB.md` expressly declines any `UNSAFE-DEP` admission for 3.4.5. An exact pin establishes identity, not undocumented implementation correctness.
+
+The smallest missing soundness proposition is:
+
+> For every `(t,p) in D` and every `v in 1..=255`, every permitted execution of the exact resolved `peer-unsafe-dep` 3.4.5 implementation of `duplicate_nonzero(v)` is free of Rust undefined behavior.
+
+Neither source proof nor an accepted TCB entry entails it. No valid UB witness against that implementation is supplied, so **UNSOUND** is not justified; failure of the universal derivation yields **UNPROVED**. Resolution requires either a recursive audit of the exact dependency implementation/generated artifact over `D`, or explicit human acceptance of that precise `UNSAFE-DEP` proposition.
+
+The wrapper documents no result-equals-input postcondition; it only syntactically forwards the callee result. The dependency documentation separately says it returns `value`. That dependency postcondition is also **UNPROVED** for the same missing implementation evidence, though it is not needed to prove the wrapper’s caller-side precondition.
+
+## Obligation and trust closure
+
+| Obligation | Premises/coverage | Status |
+|---|---|---|
+| O1: safe C1 callers reach no UB | local unconditional call + AXIOM-UU-180, all `D` | Refuted; C1 UNSOUND |
+| O2: C2 establishes callee precondition | exported `value != 0` contract + unchanged argument, all `D` | PROVED |
+| O3: exact unsafe dependency honors its safety contract | implementation proof or accepted `UNSAFE-DEP` required; neither supplied | UNPROVED; blocks C2 |
+| O4: dependency honors “Returns value” | same missing provider evidence | UNPROVED |
+
+TCB revision is the supplied `TCB.md`: AXIOM-UU-180 is accepted; unsafe-dependency, implementation, compatibility, tool, and deployment premises are absent. No testing evidence contributes. Aggregate coverage is all `D` for the C1 refutation and O2, but O3 covers no established region, so `Required subseteq Covered` cannot be certified for C2.
+
+Re-audit is required if either function or its documentation changes; the supported Rust/target/profile predicate changes; the Rust authority changes; the dependency identity, contract, features, implementation, or generated output becomes available or changes; or the TCB trust decision changes.

evals/unsafe-rust/runs/2026-08-01-v4-focused/collection/attempts/r003/1/attestation.json

@@ -0,0 +1,19 @@
+{
+  "agent_id": "/root/v4_report_r003",
+  "api_state": "COMPLETED",
+  "attempt": 1,
+  "canonical_for_scoring": true,
+  "operational_scope_deviation": false,
+  "recorded_utc": "2026-08-01T18:11:46.889438Z",
+  "report_sha256": "c8399a0504c893f30a809f39b7426472335f151709ffe5a6960a9cb87f83e9e2",
+  "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": 896
+}