From 34363dbae2d578719eab7b5a140c4d8c24c81278 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Sat, 1 Aug 2026 00:52:21 +0000 Subject: [PATCH] Refine the V3 targeted confirmation before freezing Incorporate independent protocol review while the V3 confirmation remains a draft. Make V3 the absolute candidate under test and V2 a diagnostic comparator rather than allowing a relative improvement to satisfy the release decision. Clarify the atom rubrics, accepted proof forms, verdict certificates, authority requirements, condition-specific prompts, and frozen fixture expectations. Add coverage for exact set relations, symbolic configuration composition, ordered fallible construction, and the distinction between an unsoundness witness and an unnecessarily maximal characterization of every bad input. These are preregistration corrections, not interpretations of observed model behavior. No reports have been collected, no condition identities have been revealed, and the strict all-atoms and zero-hard-error gates remain unchanged. gherrit-pr-id: Gd5c25nyjtgu5tav2bs53xvoz525b6kpe --- .../fixtures/v3-targeted/c_conflict/TCB.md | 8 +- .../v3-targeted/k_regression/REQUEST.md | 11 +- .../v3-targeted/m_multirelease/EVIDENCE.md | 34 ++- .../v3-targeted/m_multirelease/REQUEST.md | 7 +- .../v3-targeted/m_multirelease/TCB.md | 31 ++- .../v3-targeted/q_quantifiers/EVIDENCE.md | 3 - .../fixtures/v3-targeted/q_quantifiers/TCB.md | 4 - .../v3-targeted/r_redesign/REQUEST.md | 5 +- .../fixtures/v3-targeted/s_symbolic/CI.md | 4 - .../v3-targeted/s_symbolic/SUPPORT.md | 6 +- .../fixtures/v3-targeted/s_symbolic/TCB.md | 2 +- .../fixtures/v3-targeted/x_cross/TCB.md | 17 +- .../fixtures/v3-targeted/x_cross/src/lib.rs | 7 +- .../v3-targeted-drafts/controls.md | 60 +++-- .../unsafe-rust/v3-targeted-drafts/domain.md | 255 ++++++++++++------ .../unsafe-rust/v3-targeted-drafts/verdict.md | 105 +++++--- evals/unsafe-rust/v3-targeted-plan.md | 58 ++-- 17 files changed, 382 insertions(+), 235 deletions(-) diff --git a/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/TCB.md index e3afde8f39..b059566e04 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/TCB.md +++ b/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. diff --git a/evals/unsafe-rust/fixtures/v3-targeted/k_regression/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/k_regression/REQUEST.md index df2459dab0..9383b3a5dd 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/k_regression/REQUEST.md +++ b/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. diff --git a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/EVIDENCE.md b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/EVIDENCE.md index 074f77a4cf..90e9567709 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/EVIDENCE.md +++ b/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::()` 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`. diff --git a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/REQUEST.md index 0626c1be25..8b5981839c 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/REQUEST.md +++ b/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. diff --git a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/TCB.md index 12594e7342..d82f1c3c00 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/TCB.md +++ b/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. diff --git a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/EVIDENCE.md b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/EVIDENCE.md index daedbff641..936041319e 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/EVIDENCE.md +++ b/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. diff --git a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/TCB.md index c10f2dc6ec..c5e89e85bb 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/TCB.md +++ b/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. diff --git a/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/REQUEST.md index c782b1b3c8..b002b0ef5b 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/REQUEST.md +++ b/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. diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/CI.md b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/CI.md index 8034ac7dc9..c1a59cb26d 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/CI.md +++ b/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. - diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/SUPPORT.md b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/SUPPORT.md index 416fa0dc7d..f0a2deb57d 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/SUPPORT.md +++ b/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. - diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/TCB.md index 6382bef673..f342ed39ca 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/TCB.md +++ b/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) diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/TCB.md index 19f2f96619..753ebaa759 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/TCB.md +++ b/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 diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/src/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/src/lib.rs index 3f31591c5b..233f32925a 100644 --- a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/src/lib.rs +++ b/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) } } } - diff --git a/evals/unsafe-rust/v3-targeted-drafts/controls.md b/evals/unsafe-rust/v3-targeted-drafts/controls.md index c50ce0dba9..2606f31bc9 100644 --- a/evals/unsafe-rust/v3-targeted-drafts/controls.md +++ b/evals/unsafe-rust/v3-targeted-drafts/controls.md @@ -7,8 +7,9 @@ ### Exact result -`Required` includes every safe downstream implementation of `Slot` and safe -instantiation of `increment`, not only the crate-owned `Tail`. A safe +Within the exact target/profile scope declared in `REQUEST.md`, `Required` +includes every safe downstream implementation of `Slot` and safe instantiation +of `increment`, not only the crate-owned `Tail`. A safe implementation can return 2. Calling `increment::(&mut [0, 0])` then executes `get_unchecked_mut(2)` on a length-2 slice. The Rust 1.82.0 contract requires an in-bounds index and says an out-of-bounds call is UB even if the @@ -33,17 +34,18 @@ audit after implementation. and proposals. - **R4:** Extract the exact minimum required behavior: wrapping increment of element 1 for the owned use, with no generic downstream implementation need. -- **R5:** Prefer a nongeneric safe specialization or an equally parsimonious - design that locally enforces the index and transfers no soundness obligation - to caller-controlled code. +- **R5:** Propose a nongeneric safe specialization that implements the required + wrapping increment of element 1 using checked indexing (or an exactly + behavior-equivalent safe operation), with no caller-controlled + implementation or index capability. - **R6:** Explain that removing the unpublished generic trait/API is an authorized contract delta with no promised downstream migration burden. - **R7:** Keep the redesign conditional and require implementation plus fresh audit; do not use it to narrow or alter the current `UNSOUND` result. -Equivalent safe formulations pass R5. Merely making the trait unsafe is a sound -candidate but does not pass the parsimony atom unless the report explains why -the unnecessary caller obligation is inferior to the safe specialization. +Merely making the trait unsafe does not pass R5: it preserves a caller +implementation capability that the supplied requirement expressly does not +need. ### Hard errors @@ -58,13 +60,17 @@ lets design intent narrow the current contract. `https://doc.rust-lang.org/1.82.0/std/primitive.slice.html#method.get_unchecked_mut` — the index must be in bounds; out-of-bounds calls are UB even if the resulting reference is unused. +- Rust 1.82.0 `u32::wrapping_add`: + `https://doc.rust-lang.org/1.82.0/std/primitive.u32.html#method.wrapping_add` + — wrapping modular addition supplies the requested update semantics. ## K — multi-issue regression ### Exact results -For `callback_index`, safe implementations of `Position` may return any -`usize`. For a one-byte slice, an implementation returning 1 gives valid safe +Within the exact target/profile scope declared in `REQUEST.md`, safe +implementations of `callback_index::Position` may return any `usize`. For a +one-byte slice, an implementation returning 1 gives valid safe calls to both `read` and `write`, each of which executes its respective out-of-bounds unchecked operation. Both safe surfaces are independently `UNSOUND`. @@ -92,17 +98,22 @@ consumers mean the unused `NAME` clause cannot be weakened from the published `callback_index::write`; do not stop after K1. - **K3:** For `local_proof::last`, reconstruct the nonempty -> `len > 0` -> `len - 1 < len` derivation, connect it to the exact unchecked-index contract, - report the implementation obligation proved, and separately report the - existing safety comment materially deficient with replacement proof content. -- **K4:** Prove both clauses of `High`'s unsafe-trait contract and prove `read` - sound relative to the complete valid-implementation contract. -- **K5:** Retain the `NAME` clause and explain that unknown public + and report the implementation obligation proved. +- **K4:** Separately report the existing `local_proof::last` safety comment + materially deficient and provide replacement proof content that identifies + the unchecked-index obligation and the K3 derivation. +- **K5:** Prove that `High` satisfies both clauses of its unsafe-trait contract: + `INDEX < 2` and the exact `NAME`/`INDEX` relation. +- **K6:** Prove `published_lane::read` sound for every valid implementation of + the complete `Lane` contract by consuming its `INDEX < 2` clause. +- **K7:** Retain the `NAME` clause and explain that unknown public implementers/consumers prevent weakening the published 1.x contract merely because the only visible consumer uses `INDEX`. -- **K6:** Propose a local bounds check or another design that couples and proves - the chosen position against the particular slice. Sealing may reduce the - implementation set but is not sufficient by itself. Keep every unimplemented - repair uncertified and leave both current findings unchanged. +- **K8:** Propose a repair that preserves callable read and write operations at + positions chosen by safe callers and locally couples and checks each chosen + position against the particular slice. Deleting or making the APIs + uncallable, or merely sealing or eliminating the caller-implementable trait, + does not meet that functional requirement. Score each atom independently. Compact shared reasoning may serve K1 and K2 only if it explicitly names both operations and shows that the witness reaches @@ -116,9 +127,10 @@ surface sound, rejects the correct `last` implementation because its comment is bad, explicitly calls the deficient comment adequate, relies on that comment as the proof, claims complete requested coverage while omitting the reconstruction, weakens the published trait contract from visible use alone, treats sealing -alone as a sufficient bounds proof, or certifies an unimplemented repair. A -mere omitted comment-quality disposition fails K3 but is not independently a -hard error. +alone as satisfying the stated functional repair, claims a callable +caller-position API is repaired without locally coupling the selected position +to the particular slice, or certifies an unimplemented repair. A mere omitted +comment-quality disposition fails K4 but is not independently a hard error. ### Authority @@ -130,6 +142,10 @@ hard error. `https://doc.rust-lang.org/1.82.0/std/primitive.slice.html#method.len` and `https://doc.rust-lang.org/1.82.0/std/primitive.slice.html#method.is_empty` +- Rust 1.82.0 Reference, arithmetic binary operators and integer overflow: + `https://doc.rust-lang.org/1.82.0/reference/expressions/operator-expr.html#arithmetic-and-logical-binary-operators` +- Rust 1.82.0 Reference, unsigned integer value domains: + `https://doc.rust-lang.org/1.82.0/reference/types/numeric.html#integer-types` - Rust 1.82.0 Reference, unsafe traits: `https://doc.rust-lang.org/1.82.0/reference/items/traits.html#unsafe-traits` - Rust 1.82.0 Reference, unsafe-trait proof obligations: diff --git a/evals/unsafe-rust/v3-targeted-drafts/domain.md b/evals/unsafe-rust/v3-targeted-drafts/domain.md index 957eee289c..2b93b8b8e7 100644 --- a/evals/unsafe-rust/v3-targeted-drafts/domain.md +++ b/evals/unsafe-rust/v3-targeted-drafts/domain.md @@ -23,6 +23,9 @@ The evaluator must independently confirm that every cited official page says what the report claims and applies to the claimed Rust version. A report does not pass merely by supplying a plausible-looking URL. +Throughout S, C, and X, `P` ranges over every Cargo profile supported by the +target and `D` over both states of debug assertions. + ## S — Symbolic Interval and Parametric Superset ### Intended theorem domain @@ -38,22 +41,27 @@ F_S = { telemetry-off, telemetry-on } O_S = { None } union { Some(b) | b is any u8 } ``` -Let `P` range over every Cargo profile accepted by the source and `D` over -both states of debug assertions. The exact requested case predicate is: +The exact requested case predicate is: ```text Required_S(r, t, f, p, d, o) iff r in R_S and t in T_S and f in F_S and p in P and d in D and o in O_S. ``` -This predicate is symbolic. It is not the four minor `.0` releases, the CI -matrix, or the Cargo minimum. In particular, `Required_S` contains Rust -1.85.1. Rust 1.84.1 is also an actual stable member, but a report may preserve -the exact symbolic predicate rather than enumerate released members. +This predicate is symbolic. It is not the CI matrix or the Cargo minimum. It +contains non-`.0` stable releases such as Rust 1.84.1 and 1.85.1, but a report +may preserve the exact symbolic predicate without enumerating any members. + +Define `Q_Option(r)` to mean that the two required `Option` propositions have +been established for release `r` by either of two admissible bases: + +1. the Rust 1.84.0 base authorities plus accepted entry + `COMPAT-OPTION-184-186` over its exact region; or +2. an exact finite partition that proves the released members of `R_S` are + `{1.84.0, 1.84.1, 1.85.0, 1.85.1, 1.86.0}` and verifies the two exact + versioned pages for every member. -Define `Q_Option(r)` to mean that the Rust 1.84.0 base authorities have been -verified and accepted entry `COMPAT-OPTION-184-186` applies those exact -propositions to `r`. The intended proof cases are: +The intended proof cases are: ```text Covered_S = { (r,t,f,p,d,o) | Q_Option(r), and t/f/p/d/o are otherwise arbitrary }. @@ -61,18 +69,18 @@ Covered_S = { (r,t,f,p,d,o) | Q_Option(r), and t/f/p/d/o are otherwise arbitrary The source derivation is parametric in `t`, `f`, `p`, and `d`; it need not and should not be expanded into their Cartesian product. Applicability still must -establish `R_S subset-of {r | Q_Option(r)}`. The accepted fixture-supplied TCB -entry does so after its base authority is verified. A merely report-authored -compatibility proposal, generic stability assertion, or endpoints alone does -not. +establish `R_S subset-of {r | Q_Option(r)}`. Either admissible basis above can +do so. A merely report-authored compatibility proposal, generic stability +assertion, endpoint sampling, or incomplete release partition cannot. ### Expected verdicts -- Safe-API soundness over `Required_S`: **PROVED relative to - `COMPAT-OPTION-184-186`**. +- Safe-API soundness over `Required_S`: **PROVED**, either from the exact + finite authoritative partition or relative to `COMPAT-OPTION-184-186`. - The documented `None -> 0` and `Some(b) -> b` behavior over `Required_S`: - **PROVED relative to `COMPAT-OPTION-184-186`**. -- Configuration closure: **PROVED relative to the same TCB**, because + **PROVED** on the same basis and with the TCB qualification whenever that + entry is consumed. +- Configuration closure: **PROVED** on the chosen basis, because `Required_S subset-of Covered_S`. The local proof is: `is_none()` returning true takes the `return 0` branch. If @@ -85,31 +93,42 @@ derivation. ### Atoms - **S1 — Lossless domain recovery:** States `R_S` as the closed symbolic - stable-release interval, keeps the three targets and both feature states, - and expressly recognizes Rust 1.85.1 as in scope. It does not substitute - Cargo's lower bound or CI's endpoint samples for the policy. -- **S2 — Premise applicability:** Verifies the exact Rust 1.84.0 base - propositions, applies only the fixture-supplied accepted - `COMPAT-OPTION-184-186` entry over its exact region, and keeps that TCB - qualification conspicuous. A report-authored premise does not pass. -- **S3 — Parametric local proof:** Gives the reachability/variant argument for - `unwrap_unchecked`, proves the documented result, and observes that the same - derivation covers a superset of all target/feature/profile combinations - without Cartesian enumeration. -- **S4 — Closure and verdict:** Establishes `Required_S subset-of Covered_S` - and reports both soundness and behavior `PROVED` over the exact policy domain - relative to the accepted entry. + stable-release predicate and keeps the three targets and both feature states. + It does not substitute Cargo's lower bound or CI's rows for the policy. Exact + symbolic notation passes without naming any particular patch release. +- **S2 — Premise applicability:** Uses one complete admissible evidence basis: + either verifies the 1.84.0 base, applies only fixture-supplied accepted entry + `COMPAT-OPTION-184-186`, and keeps that admission conspicuous; or proves the + exact five-member release partition and verifies both exact pages for every + member. A report-authored premise, partial partition, or mixed gap does not + pass. +- **S3 — Local safety proof:** Gives the reachability/variant argument that + reaching `unwrap_unchecked` implies the unchanged, still-owned value is + `Some`, thereby discharging the exact unsafe precondition. +- **S4 — Local behavioral proof:** Shows that `None` returns zero and `Some(b)` + returns `b`, using the applicable exact `Option` propositions. +- **S5 — Parametric configuration coverage:** Shows that the local derivation + is independent of target, feature, profile, and debug assertions and covers + their complete product without Cartesian enumeration. +- **S6 — Soundness closure and verdict:** Establishes + `Required_S subset-of Covered_S` for the soundness theorem and reports + soundness `PROVED` over the exact policy domain, conspicuously qualified by + `COMPAT-OPTION-184-186` if and only if that route was consumed. +- **S7 — Behavioral closure and verdict:** Establishes + `Required_S subset-of Covered_S` for the documented result theorem and + reports behavior `PROVED` over the exact policy domain, conspicuously + qualified by `COMPAT-OPTION-184-186` if and only if that route was consumed. ### Hard-error triggers A report commits a hard error if it: -- contracts the release interval to `.0` releases, CI samples, or the Cargo - minimum, including by omitting the expressly supported 1.85.1 case; +- claims full closure or an affirmative whole-domain result after contracting + the release predicate to `.0` releases, CI rows, or the Cargo minimum; - calls endpoints, a toolchain pin, or sparse documentation a proof of every interior release and then claims `PROVED`; - silently invents or accepts a report-authored compatibility premise, or hides - the accepted fixture TCB qualification; + the fixture TCB qualification after consuming that entry; - claims closure while leaving a `Required_S` region outside its proof; - finds `None` reachable at `unwrap_unchecked`; or - gives an unqualified `UNSOUND` or `CONTRACT-BROKEN` verdict for the shown @@ -185,10 +204,10 @@ Covered_C = { !f on X/A/W, or f on X/A } cross O_S cross P cross D. - Safe-API soundness and documented behavior over conservative union `U_C`: **PROVED relative to `BUILD-MAP-C`**. - The conclusion may state that either possible project promise is sound, - because both are subsets of the proved union. It must not relabel `U_C` as - the recovered exact project promise. + because both are subsets of the proved conservative domain. It must not + relabel that audit domain as the recovered exact project promise. - `turbo` plus wasm32: outside both policies and effectively rejected by the - active `compile_error!` configuration. + active `compile_error!` configuration, **PROVED relative to `BUILD-MAP-C`**. The non-`turbo` path uses the documented safe `unwrap_or`. The `turbo` path returns on `None`; reaching `unwrap_unchecked` therefore establishes `Some`, @@ -200,22 +219,27 @@ independent of target, `hardened`, profile, and debug assertions. - **C1 — Both nonlinear predicates:** Reproduces both policies without choosing precedence and identifies at least one Scarlet-only and one Indigo-only region. -- **C2 — Conservative domain:** Derives the exact minimal `U_C` formula, - including the conditional aarch64 clause, and distinguishes it from the - unresolved exact project promise. A transparent strict audit superset also - passes if the report states `U_C`, proves `U_C` is contained in that superset, - does not call it the project promise, and completely covers it. +- **C2 — Conservative domain:** Takes either rigorous route: derive the exact + minimal `U_C` formula, including its conditional aarch64 clause; or choose a + transparent audit superset `S` and prove separately that + `P_Scarlet subset-of S` and `P_Indigo subset-of S`. In either route, do not + call the chosen conservative domain the unresolved exact project promise. - **C3 — Enforced exclusion:** Recognizes that `turbo` wasm32 is excluded by both policies and that the `compile_error!` selected by the matching `cfg` makes the ordinary supported build interface reject it, using only the exact accepted `BUILD-MAP-C` mappings and applicable Rust semantics. -- **C4 — Parametric superset proof:** Proves both source branches and expresses - `Covered_C` as a target/configuration superset of `U_C`, without requiring a - Cartesian case inventory. -- **C5 — Closure and verdict:** Establishes containment of the chosen - conservative audit domain in complete source-proof coverage, reports source - soundness and behavior `PROVED` over at least `U_C` relative to the accepted - build TCB, and leaves only policy identity unresolved. +- **C4 — Soundness certificate:** Proves the safe non-`turbo` branch and the + `None`-return/reachable-`Some` argument for the unsafe `turbo` branch, + expresses the resulting `Covered` region parametrically, proves it contains + the chosen conservative audit domain, and reports soundness **PROVED relative + to `BUILD-MAP-C`** over that domain. +- **C5 — Behavioral certificate:** Proves both branches return zero for `None` + and the contained byte for `Some`, shows the same `Covered` region contains + the chosen conservative audit domain, and reports the documented behavior + **PROVED relative to `BUILD-MAP-C`** over that domain. +- **C6 — Policy status:** Reports the controlling exact project predicate + **UNRESOLVED** and does not relabel the chosen conservative audit domain as + that promise. ### Hard-error triggers @@ -223,15 +247,16 @@ A report commits a hard error if it: - silently selects Scarlet or Indigo, intersects them, or asserts that their union is the recovered exact project promise; -- contracts `U_C`, misstates it, or uses a larger domain without proving - containment and complete coverage; a conspicuously labeled justified strict - superset is not an error; +- claims that a chosen conservative audit domain contains both published + predicates, or claims closure over it, when the stated derivation does not; + merely declining closure is an atom failure, not a hard error; - treats `turbo` wasm32 as supported, or claims it is effectively rejected without accounting for the selected `compile_error!`; - treats Cargo's minimum, a hypothetical build sample, or a policy sentence as a Rust semantic axiom; - invents or widens a build-tool mapping beyond accepted `BUILD-MAP-C`; -- claims `PROVED` while leaving any part of `U_C` uncovered; or +- claims `PROVED` while leaving any part of the chosen conservative domain + uncovered; or - calls the shown source `UNSOUND` or `CONTRACT-BROKEN`. ## X — Simultaneous Feature, Target, and Allocator @@ -270,17 +295,18 @@ for either feature state. It is distinct from `Q_X`. The build script maps the accepted `FIXTURE_ALLOCATOR` value to exactly one `fixture_allocator` option; the Rust conditional-compilation rules then select -the corresponding source. For positive proof bookkeeping, the implementation -closes exactly these relevant call cases: +the corresponding source. For positive soundness bookkeeping, the +implementation closes exactly these call cases: ```text -Covered_X = { case in Required_X | not Q_X or value != 0 }. +Covered_X_sound = { case in Required_X | not Q_X or value != 0 }. ``` -Outside `Q_X`, safe `NonZeroU8::new(value).expect(...)` panics for zero and -returns a nonzero value otherwise. Inside `Q_X`, `new_unchecked(value)` meets -its precondition only for nonzero values. Consequently -`Required_X` is not a subset of `Covered_X`. +Outside `Q_X`, the explicit zero check panics for zero; after that check, +`new_unchecked(value)` meets its precondition. Inside `Q_X`, the unchecked +constructor is reached without that check and meets its precondition only for +nonzero values. Consequently `Required_X` is not a subset of +`Covered_X_sound`. ### Expected verdicts @@ -288,11 +314,13 @@ its precondition only for nonzero values. Consequently `BUILD-MAP-X`**. - Whole-domain postcondition “zero panics”: **UNPROVED**, not `CONTRACT-BROKEN`, from the known counterexample, because that execution - contains UB. -- Soundness and documented behavior outside `Q_X`, and for nonzero inputs - inside `Q_X`: **PROVED** with the version-matched contracts. + contains UB; the configuration classification is relative to `BUILD-MAP-X`. +- Soundness outside `Q_X`, and for nonzero inputs inside `Q_X`: **PROVED + relative to `BUILD-MAP-X`** with the version-matched contracts. +- The documented zero-input panic guarantee outside `Q_X`: **PROVED relative + to `BUILD-MAP-X`**. - The wasm32/arena pair: genuinely excluded and rejected; it is not the UB - witness. + witness. Effective rejection is **PROVED relative to `BUILD-MAP-X`**. The closing witness is the fully safe call `lane_id(0)` on Rust 1.85.1 for `aarch64-unknown-linux-gnu`, with `burst` enabled and the accepted `arena` @@ -306,20 +334,49 @@ the UB consequence. One supported witness closes `UNSOUND`. - **X1 — Complete cross-axis domain:** Recovers the target, feature, and allocator axes together; includes `Q_X`; and records only wasm32/arena as the policy exclusion. -- **X2 — Generated-configuration reachability:** Reads `build.rs` and - `BUILD.md`, follows accepted `arena` selection to - `fixture_allocator="arena"`, applies only the exact `BUILD-MAP-X` tool - mappings, and then applies all three `cfg` conjuncts. It does not audit only - handwritten library source in isolation or silently promote Cargo behavior - to a Rust axiom. -- **X3 — Existential UB certificate:** Gives the supported safe +- **X2 — Selector partition:** Recovers the complete environment-input + partition: omitted, Unicode `system`, Unicode `arena`, every other Unicode + value, and every non-Unicode value. +- **X3 — Accepted selector mapping:** Shows that omitted and explicit `system` + select `system`, while explicit `arena` selects `arena`, on build attempts + whose directive writes succeed. +- **X4 — Rejected selector behavior:** On attempts where the preceding + directive writes succeed, shows that every other Unicode value and every + non-Unicode value reaches a panic arm and, under `BUILD-MAP-X`, produces no + library compilation. It distinguishes that policy rejection from an earlier + infrastructure write failure, which also produces no compilation but never + reaches selector handling. +- **X5 — Allocator-cfg cardinality:** Shows that every successful accepted + selector path emits exactly one `fixture_allocator` cfg and that its value is + the value selected in X3. +- **X6 — Check-cfg directive:** After the preceding rerun write succeeds, shows + that the script attempts the check-cfg write before selector handling and + that, when this write succeeds, it registers exactly `system` and `arena` as + expected values without selecting either value. Failure of either write + follows the infrastructure no-compilation branch. +- **X7 — Rerun directive:** Shows that the script unconditionally attempts the + environment-change rerun write and that, when the write succeeds, + `BUILD-MAP-X` causes Cargo to rerun the script when `FIXTURE_ALLOCATOR` + changes. A failed write follows the infrastructure no-compilation branch. +- **X8 — Generated-configuration reachability:** Follows accepted `arena` + selection through `build.rs` to `fixture_allocator="arena"` and then applies + the feature, target, and allocator cfg conjuncts to reach `Q_X`. It does not + audit only handwritten library source in isolation. +- **X9 — Existential UB certificate:** Gives the supported safe `lane_id(0)` call in `Q_X`, reaches `new_unchecked(0)`, states the exact false nonzero proposition and applicable UB consequence, and reports `UNSOUND`. -- **X4 — Quantifier-sensitive behavior:** Calls the universal zero-input panic +- **X10 — Quantifier-sensitive behavior:** Calls the universal zero-input panic guarantee `UNPROVED`, not `CONTRACT-BROKEN`, because the known failing - execution has UB; separately proves the checked remainder. -- **X5 — Genuine exclusion:** Shows both that policy excludes wasm32/arena and + execution has UB. +- **X11 — Remainder soundness:** Proves soundness outside `Q_X` by following the + explicit zero guard and applying `new_unchecked` only after it establishes a + nonzero value, and proves nonzero inputs sound inside `Q_X`, relative to the + exact build mapping. +- **X12 — Regional panic theorem:** Proves that zero takes the explicit + `panic!` branch in every configuration outside `Q_X`, relative to the exact + build mapping. It asserts no undocumented nonzero return-value postcondition. +- **X13 — Genuine exclusion:** Shows both that policy excludes wasm32/arena and that the active `compile_error!` rejects that pair after allocator cfg generation under `BUILD-MAP-X`. It does not use this excluded pair as the witness or generalize the exclusion to aarch64/arena. @@ -328,8 +385,9 @@ the UB consequence. One supported witness closes `UNSOUND`. A report commits a hard error if it: -- omits any of feature, target, or allocator from the dangerous conjunction, - or treats the supported `Q_X` cell as excluded; +- omits feature, target, or allocator and then uses the contracted conjunction + to claim full-domain closure/soundness, or treats the supported `Q_X` cell as + excluded; - ignores build-script output and consequently declares the unsafe branch unreachable; - invents, hides, or widens a build-tool/target mapping beyond accepted @@ -362,6 +420,18 @@ Exact base pages: - `https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.is_none` - `https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.unwrap_unchecked` +The exact finite-partition alternative uses the same two propositions at every +released member of `R_S`: + +- `https://doc.rust-lang.org/1.84.1/std/option/enum.Option.html#method.is_none` +- `https://doc.rust-lang.org/1.84.1/std/option/enum.Option.html#method.unwrap_unchecked` +- `https://doc.rust-lang.org/1.85.0/std/option/enum.Option.html#method.is_none` +- `https://doc.rust-lang.org/1.85.0/std/option/enum.Option.html#method.unwrap_unchecked` +- `https://doc.rust-lang.org/1.85.1/std/option/enum.Option.html#method.is_none` +- `https://doc.rust-lang.org/1.85.1/std/option/enum.Option.html#method.unwrap_unchecked` +- `https://doc.rust-lang.org/1.86.0/std/option/enum.Option.html#method.is_none` +- `https://doc.rust-lang.org/1.86.0/std/option/enum.Option.html#method.unwrap_unchecked` + The official release inventory confirms the two patch releases, but is domain evidence rather than a substitute for a version-applicable semantic contract: @@ -411,17 +481,34 @@ For Rust 1.85.1: 1. `NonZero::new_unchecked(0)` has undefined behavior and its safety precondition requires a nonzero argument; -2. `NonZero::new(n)` creates `Some(nonzero)` exactly when `n` is nonzero; -3. `Option::expect` returns the `Some` value and panics on `None`; -4. conjunction and key/value configuration predicates select the stated - `#[cfg]` forms; and -5. `compile_error!` causes compilation to fail when selected. +2. primitive integer equality and `if` expression semantics make the explicit + zero branch execute exactly when `value == 0` and skip it otherwise; +3. `panic!` panics the current thread; +4. `env::var` distinguishes an omitted value, a Unicode value, and a + non-Unicode value as used by the build script; +5. block, match, string-view, pattern, and `println!` semantics establish the + local script's accepted-value mapping, rejection arms, unconditional rerun + directive, and single allocator-cfg emission; +6. conjunction, negation, and key/value configuration predicates select the + stated `#[cfg]` forms; and +7. `compile_error!` causes compilation to fail when selected. Exact pages: - `https://doc.rust-lang.org/1.85.1/std/num/struct.NonZero.html#method.new_unchecked` -- `https://doc.rust-lang.org/1.85.1/std/num/struct.NonZero.html#method.new` -- `https://doc.rust-lang.org/1.85.1/std/option/enum.Option.html#method.expect` +- `https://doc.rust-lang.org/1.85.1/reference/expressions/operator-expr.html#comparison-operators` +- `https://doc.rust-lang.org/1.85.1/reference/expressions/if-expr.html` +- `https://doc.rust-lang.org/1.85.1/std/macro.panic.html` +- `https://doc.rust-lang.org/1.85.1/std/env/fn.var.html` +- `https://doc.rust-lang.org/1.85.1/std/string/struct.String.html#method.as_str` +- `https://doc.rust-lang.org/1.85.1/std/primitive.str.html#impl-ToOwned-for-str` +- `https://doc.rust-lang.org/1.85.1/std/fmt/index.html#syntax` +- `https://doc.rust-lang.org/1.85.1/reference/expressions/block-expr.html` +- `https://doc.rust-lang.org/1.85.1/reference/expressions/match-expr.html` +- `https://doc.rust-lang.org/1.85.1/reference/patterns.html#literal-patterns` +- `https://doc.rust-lang.org/1.85.1/reference/patterns.html#or-patterns` +- `https://doc.rust-lang.org/1.85.1/reference/patterns.html#wildcard-pattern` +- `https://doc.rust-lang.org/1.85.1/std/macro.println.html` - `https://doc.rust-lang.org/1.85.1/reference/conditional-compilation.html#configuration-options` - `https://doc.rust-lang.org/1.85.1/reference/conditional-compilation.html#the-cfg-attribute` - `https://doc.rust-lang.org/1.85.1/std/macro.compile_error.html` @@ -432,7 +519,9 @@ exact identity, mappings, and region. Verify the cited Cargo contracts used to review that entry, but do not enlarge it: - `https://doc.rust-lang.org/1.85.1/cargo/reference/build-scripts.html#rustc-cfg` +- `https://doc.rust-lang.org/1.85.1/cargo/reference/build-scripts.html#rustc-check-cfg` - `https://doc.rust-lang.org/1.85.1/cargo/reference/build-scripts.html#rerun-if-env-changed` +- `https://doc.rust-lang.org/1.85.1/cargo/reference/build-scripts.html#life-cycle-of-a-build-script` - `https://doc.rust-lang.org/1.85.1/cargo/reference/features.html` No release blog, CI outcome, execution result, Miri result, prior report, or diff --git a/evals/unsafe-rust/v3-targeted-drafts/verdict.md b/evals/unsafe-rust/v3-targeted-drafts/verdict.md index 3334189123..462a52b776 100644 --- a/evals/unsafe-rust/v3-targeted-drafts/verdict.md +++ b/evals/unsafe-rust/v3-targeted-drafts/verdict.md @@ -59,13 +59,13 @@ dependency resolve times every ordinary profile. `UNSAFE-DEP` entry establishes that it honors its contract. The exact pin and caller-facing documentation establish the logical package coordinate and the propagated obligation, not authenticated implementation identity or - correctness. The smallest missing proposition is that the selected - `peer-unsafe-dep` 3.4.5 implementation satisfies the consumed safety/behavior - contract over this domain. + correctness. For the soundness claim actually requested here, the smallest + missing proposition is that every valid nonzero call to the selected + `peer-unsafe-dep` 3.4.5 implementation is free of UB over this exact domain. - **Q5 — No fabricated witness or silent trust:** Report `Q-delegate-sound` as **UNPROVED**, not `PROVED` and not `UNSOUND`. From the submitted packet, claim-level `Covered(Q-delegate-sound)` contains no case: - the dependency-correctness obligation is unresolved for all valid inputs. + the dependency-soundness obligation is unresolved for all valid inputs. There is also no proved execution of the unavailable body, so no UB witness may be invented. State that recursive source audit or an explicitly accepted exact `UNSAFE-DEP` entry would be required. @@ -126,10 +126,11 @@ let `I = {0, ..., 255}`. The claims are: executes no unsafe operation, returns normally, and returns `2` rather than the promised input value `1`. That complete execution is UB-free and proves `W-return` **CONTRACT-BROKEN**. -- **W4 — Cross-execution separation:** Do not transfer a conclusion between - the distinct executions. The input-zero UB witness cannot establish failure - of the panic promise, while the independent, defined input-one failure - remains usable and does not alter the soundness witness. + +Scoring guidance, not a separate atom: keep the three executions/theorems +independent. The input-zero UB witness cannot establish failure of the panic +promise, while the independent, defined input-one failure remains usable and +does not alter the soundness witness. ### W hard errors @@ -143,9 +144,7 @@ Any of these is a hard error: - claiming source observations remain guaranteed merely because they occur before the unsafe call; - falsely treating the independent input-one refutation as UB-containing, or - claiming complete behavioral coverage while omitting it; or -- replacing the three separate theorem results with one undifferentiated - verdict that loses a required conclusion. + claiming complete behavioral coverage while omitting it. ### W authorities to verify before freezing @@ -180,74 +179,90 @@ separately to soundness and the documented normal-return postcondition. ### Expected results and atoms -- **M1 — Exact domains:** Preserve all four finite release sets and the - target/profile/call products exactly. Do not treat the cutoff as adding or - removing releases. State release regions beside each claim rather than - issuing an unscoped crate-wide `PROVED`. -- **M2 — Parametric `acknowledge` proof:** Verify that accepted general entry +- **M1 — `acknowledge` domain:** Preserve exact finite set `V_ack` and its + target/profile product; every well-typed call is in `Calls_ack` because the + API adds no safety precondition. +- **M2 — `store_word` domains:** Preserve exact finite set `V_store` and its + target/profile/valid-call product separately for soundness and the documented + normal-return postcondition. +- **M3 — `copy_byte` domains:** Preserve exact finite set `V_copy` and its + target/profile/valid-call product separately for soundness and the documented + normal-return postcondition. +- **M4 — `load_word` domains:** Preserve exact finite set `V_load` and its + target/profile/valid-call product separately for soundness and the documented + normal-return postcondition. + +For M1–M4, do not let the cutoff add or remove releases and do not substitute +an unscoped crate-wide claim for the exact products. + +- **M5 — Parametric `acknowledge` proof:** Verify that accepted general entry `SEM-EMPTY-BLOCK-180-182` has exactly the required release, target, and profile scope. Independently inspect the local syntax and establish that the exact body is an empty block. For arbitrary `(v, target, profile, call) in Required(M-ack)`, combine only those premises: - the block executes no operation or event, yields unit, and the `unsafe fn` - marker itself adds no executed operation. Thus + `acknowledge` is zero-parameter and unit-returning, the valid call has defined + callee evaluation and returns `()`, and the `unsafe fn` marker changes only + its static caller obligation. Thus `Covered(M-ack) = Required(M-ack)` and source-level soundness is **PROVED parametrically relative to `SEM-EMPTY-BLOCK-180-182`**. Keep the admission conspicuous; the TCB entry is general semantics, not a target-specific assertion that the function is sound. -- **M3 — `store_word` soundness partition:** The 1.80.0 `ptr::write` authority +- **M6 — `store_word` soundness partition:** The 1.80.0 `ptr::write` authority applies exactly to the 1.80.0 case and the 1.81.0 authority to the 1.81.0 case. For each case, the documented caller contract entails the applicable page's alignment and write-validity preconditions. The identity `V_store = {1.80.0} union {1.81.0}` proves exhaustiveness. Therefore `Covered(M-store-sound) = Required(M-store-sound)` and soundness is **PROVED** by an exact finite partition. -- **M4 — `store_word` postcondition partition:** In each exact release case, +- **M7 — `store_word` postcondition partition:** In each exact release case, the applicable page says that `ptr::write(dst, value)` writes the supplied `value` to `dst` without reading or dropping the old value. The same finite partition covers every normal-return postcondition obligation, so `Covered(M-store-post) = Required(M-store-post)` and the documented postcondition is **PROVED**. -- **M5 — `copy_byte` soundness under the exact TCB:** Verify the Rust 1.80.0 - `copy_nonoverlapping` safety proposition, primitive `u8` size/alignment, and - `u8: Copy` base propositions. Then apply only accepted entry +- **M8 — `copy_byte` soundness under the exact TCB:** Verify the Rust 1.80.0 + `copy_nonoverlapping` safety proposition, primitive `u8` size, `u8: Copy`, + and exact `Copy` semantics base propositions. Then apply only accepted entry `COMPAT-COPY-180-182`, with its exact release set, `T = u8`, `count = 1`, target/profile domain, and consumer. The caller contract entails its source and destination validity, initialization, alignment, and nonoverlap clauses; - the admitted `u8` facts establish the one-byte specialization and avoid the - ownership hazard for non-`Copy` values. Thus + the admitted `u8` and `Copy` facts establish the one-byte specialization and + avoid the ownership hazard for non-`Copy` values. Thus `Covered(M-copy-sound) = Required(M-copy-sound)` and soundness is **PROVED relative to `COMPAT-COPY-180-182`**. -- **M6 — `copy_byte` postcondition under the exact TCB:** The accepted entry +- **M9 — `copy_byte` postcondition under the exact TCB:** The accepted entry preserves the base proposition that the call copies the source byte into the destination while leaving the source byte unchanged; `u8` has size one and - implements `Copy`. It covers every normal-return postcondition obligation, - so `Covered(M-copy-post) = Required(M-copy-post)` and the documented + implements `Copy` with the cited copy rather than move semantics. It covers + every normal-return postcondition obligation, so + `Covered(M-copy-post) = Required(M-copy-post)` and the documented postcondition is **PROVED relative to `COMPAT-COPY-180-182`**. -- **M7 — `load_word` soundness remainder:** In the 1.80.0 and 1.82.0 endpoint +- **M10 — `load_word` soundness remainder:** In the 1.80.0 and 1.82.0 endpoint cases, the exact `ptr::read` Safety sections plus exact-version `u32: Copy` - facts prove soundness from the caller contract, including safe retention of - the source value alongside the returned copy. Thus + and `Copy`-semantics facts prove soundness from the caller contract, + including safe retention of the source value alongside the returned copy. + Thus `Covered(M-load-sound) = {1.80.0, 1.82.0} times C_M times Calls_load`. The 1.80.1 and 1.81.0 regions and therefore the complete `V_load` soundness claim are **UNPROVED**. No UB witness is supplied, so `UNSOUND` does not follow. -- **M8 — `load_word` postcondition remainder:** In the same two endpoint +- **M11 — `load_word` postcondition remainder:** In the same two endpoint cases, the applicable `ptr::read` descriptions establish that the returned value is read from `src` while the source is left unchanged; the exact - `u32: Copy` facts discharge the ownership qualification. Therefore + `u32: Copy` and `Copy`-semantics facts discharge the ownership qualification. + Therefore `Covered(M-load-post) = {1.80.0, 1.82.0} times C_M times Calls_load`. The two interior regions and the complete postcondition claim are **UNPROVED**. No defined wrong-result witness is supplied, so `CONTRACT-BROKEN` does not follow. -- **M9 — Evidence discipline:** If the report actually relies on endpoint - sampling, the cutoff, an unstated stability guarantee, backward projection, - evidence for another operation, or a widened TCB entry to fill the - `ptr::read` interior, reject that basis explicitly. Identify the smallest - missing premise as a verified authority for the interior releases, an exact - applicable accepted compatibility entry, or another complete parametric - proof. Do not require a report that used none of the listed invalid bases to - recite all of them. + +Scoring guidance, not a separate atom: if a report actually relies on endpoint +sampling, the cutoff, an unstated stability guarantee, backward projection, +evidence for another operation, or a widened TCB entry to fill the `ptr::read` +interior, reject that basis explicitly. For an `UNPROVED` interior, require the +smallest missing premise: a verified authority for the interior releases, an +exact applicable accepted compatibility entry, or another complete parametric +proof. A report that uses none of the listed invalid bases need not recite them. ### M hard errors @@ -287,9 +302,12 @@ including all qualifications relevant to its exact release case: — copies `count * size_of::()` bytes; source/destination validity, alignment, and nonoverlap requirements; base case only. - `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. - `https://doc.rust-lang.org/1.80.0/std/primitive.u8.html#impl-Copy-for-u8` — `u8` implements `Copy` in the compatibility base case. +- `https://doc.rust-lang.org/1.80.0/std/marker/trait.Copy.html` + — exact copy rather than move semantics for `Copy` values in the base and + 1.80.0 endpoint cases. - `https://doc.rust-lang.org/1.80.0/std/ptr/fn.read.html` — reads without moving, leaves source unchanged, and requires read validity, alignment, and initialization for this non-ZST. @@ -299,6 +317,9 @@ including all qualifications relevant to its exact release case: — the same named propositions for the separate endpoint case. - `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. +- `https://doc.rust-lang.org/1.82.0/std/marker/trait.Copy.html` + — exact copy rather than move semantics for `Copy` values in the 1.82.0 + endpoint case. The `acknowledge` and compatibility results additionally consume the two exact accepted propositions in target file `TCB.md`; that file is not Rust authority diff --git a/evals/unsafe-rust/v3-targeted-plan.md b/evals/unsafe-rust/v3-targeted-plan.md index e50aa8bc5e..19972dcab9 100644 --- a/evals/unsafe-rust/v3-targeted-plan.md +++ b/evals/unsafe-rust/v3-targeted-plan.md @@ -8,13 +8,19 @@ ## Purpose -This confirmatory evaluation tests whether the V3 skill revision reliably -changes the specific proof behavior that prevented V2 from passing its strict -release gates, while preserving the abstraction-design and general-audit -behaviors that V2 already performed well. +This confirmatory evaluation tests whether V3 reliably exhibits the specific +proof capabilities implicated by V2's strict-gate failures, while preserving +the abstraction-design and general-audit capabilities that V2 already +exhibited. Its primary result is an absolute capability result for V3, not an +estimate of the causal effect of the revision. -It tests mechanisms, not release readiness. Passing this evaluation permits a -later broad release gate; it does not replace that gate. +The coherent V2 package is a diagnostic comparator. Lower V2 performance can +provide evidence consistent with targeted improvement; matched ceiling +performance shows replication of an existing capability and supplies no +evidence that V3 caused an improvement. + +It is a focused capability confirmation, not a release-readiness evaluation. +Passing it permits a later broad release gate; it does not replace that gate. ## Frozen candidate conditions @@ -22,7 +28,7 @@ The intended conditions are: | Condition | Package tree digest | `SKILL.md` digest | Role | |---|---|---|---| -| V3 | `668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf` | `0e23f7747cc63014bade7543efaf745e7e9a7e5d6dee2a48c602ef7a3eba091e` | treatment | +| V3 | `668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf` | `0e23f7747cc63014bade7543efaf745e7e9a7e5d6dee2a48c602ef7a3eba091e` | candidate | | V2 | `40b4171cc9daf7e51ba032aef52157a85a49c4c12cea8696deadb948e0867897` | `a0a75ef8a14497aa78b50b459981097ee99605c57fec95c637cf59aaa20fe766` | pre-change comparator | The comparison uses the coherent V2 package, not a synthetic deletion @@ -53,7 +59,8 @@ failure. Tests preservation of a symbolic stable-release interval, membership of a non-`.0` patch release, rejection of sampled CI/toolchains as an inventory, and -closure by a version-parametric proof over a justified superset. +closure by either an exact applicable release partition or a version-parametric +proof over a justified compatibility region. ### C — Conflicting policies, conservative union, and exclusions @@ -65,8 +72,10 @@ superset without Cartesian enumeration. ### X — Conditional feature/target/allocator cross-product Tests recovery of an easily missed simultaneous configuration, distinction -between a supported bad case and a genuinely enforced exclusion, and a complete -region-scoped UB certificate. +between a supported bad case and a genuinely enforced exclusion, complete +coverage of the build script's accepted/rejected selector interface and emitted +directives, a region-scoped UB certificate, UB-sensitive classification of the +documented panic theorem, and positive closure over the proved remainder. ### Q — Existential refutation versus incomplete universal proof @@ -114,14 +123,15 @@ into per-mode blind-scoring rubrics before collection. hard errors. - **H-release:** V3 passes every M atom in all five replicates with zero hard errors. -- **H-regression:** V3 passes every R and K atom in all five replicates, with +- **H-preservation:** V3 passes every R and K atom in all five replicates, with zero proposal laundering and zero hard errors. ## Primary gates The targeted confirmation passes only if all of the following hold: -1. Every V3 semantic atom passes 5/5. +1. Every frozen V3 atom passes 5/5, including domain, proof, verdict, + authority, design, compatibility, and review-process propositions. 2. V3 has zero hard errors. 3. V3 has zero proposal laundering. 4. V3 silently admits no TCB premise and uses no invalid or inapplicable @@ -131,14 +141,17 @@ The targeted confirmation passes only if all of the following hold: Failure of any primary gate fails the run. Do not average failures away, weaken an atom after seeing reports, or use V2 weakness to excuse a V3 error. -## Secondary comparison +## Diagnostic comparison After unblinding: - report V3 and V2 separately for every atom and mode; -- require that no V3 atom has fewer passes than its matched V2 atom; +- report whether any V3 atom has fewer passes than its matched V2 atom (the + absolute 5/5 V3 gate makes such a regression impossible in a passing run); - call V3 5/5 plus lower V2 performance evidence of targeted lift; - call matched 5/5 performance ceiling replication, not causal improvement; +- do not describe any comparison as causal proof: the conditions are coherent + package versions that differ in more than one isolated instruction; - do not pool heterogeneous modes into a headline score. ## Global hard errors @@ -175,7 +188,8 @@ Before collection, freeze and hash: - all target trees and opaque runtime copies; - the evaluated-agent prompt; - the oracle and per-mode scoring rubrics; -- exact official documentation URLs or a byte-identified mirror; +- one per-mode URL allowlist containing only exact official documentation URL + identities, or a byte-identified mirror manifest; - the randomized schedule and condition map; - output schema, word budgets, tool policy, and rerun policy. @@ -183,12 +197,13 @@ Each report agent must: - be fresh and receive no prior conversation (`fork_turns="none"`); - audit exactly one cell without helper agents; -- inspect only its opaque target, package, exact permitted official Rust/std - documentation, and empty output directory; +- inspect only its opaque target, package, per-mode URL allowlist, the exact + permitted official Rust/std pages (or frozen mirror bytes), and empty output + directory; - avoid building, testing, executing, or macro-expanding the target; - write one `report.md` and return the same report; -- stay within 1,800 words, except that K receives the same preregistered - 2,200-word cap in both conditions. +- stay within 1,800 words, except that X receives a 2,400-word cap and K a + 2,200-word cap, identical across conditions. Only genuine infrastructure failures may be rerun. Budget exhaustion, refusal, or semantic noncompletion is an incomplete/failed replicate, not infrastructure. @@ -212,6 +227,10 @@ The scorer must not infer a missing material premise from vague shorthand. The rubric must state in advance which compact formulations count, especially where one conceptual defect admits multiple independently scored witnesses. +The V2 and V3 agents for a mode receive the same allowlist. An allowlist may +identify URLs but must not summarize their propositions, expected use, verdict, +or relation to an atom. Its contents and digest are frozen before collection. + ## Oracle review Before the first report, two independent reviews must confirm: @@ -240,4 +259,3 @@ current zerocopy owning shards and integration, opaque holdouts, and matched V2 and no-skill subsets. It retains zero hard errors, zero proposal laundering, focused zero-miss recovery, no repaired-side recurrence, and artifact-integrity requirements. -