ci: cut the nightly deep verification to about an hour

.github/workflows/deep-verification.yml

@@ -21,11 +21,11 @@ jobs:
       matrix:
         include:
           - target: x86_64-pc-windows-msvc
-            cases: "100000"
-          - target: i686-pc-windows-msvc
             cases: "20000"
+          - target: i686-pc-windows-msvc
+            cases: "5000"
     runs-on: windows-latest
-    timeout-minutes: 180
+    timeout-minutes: 45
     env:
       CARGO_BUILD_TARGET: ${{ matrix.target }}
       WINDOWS_SPAWN_STRESS_CASES: ${{ matrix.cases }}
@@ -43,12 +43,12 @@ jobs:
       - run: cargo test --locked --test windows_spawn spawn_cleanup_stress -- --ignored --exact
 
   random:
-    name: Random command lines and environments at fifty times their size
+    name: Random command lines and environments at ten times their size
     runs-on: windows-latest
-    timeout-minutes: 300
+    timeout-minutes: 60
     env:
       RUSTFLAGS: --cfg windows_spawn_vectors
-      WINDOWS_SPAWN_RANDOM_SCALE: "50"
+      WINDOWS_SPAWN_RANDOM_SCALE: "10"
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
@@ -66,7 +66,7 @@ jobs:
       matrix:
         target: [command-line, environment-block]
     runs-on: ubuntu-latest
-    timeout-minutes: 330
+    timeout-minutes: 30
     env:
       FUZZ_TARGET: ${{ matrix.target }}
     steps:
@@ -84,7 +84,7 @@ jobs:
           tool: cargo-fuzz@0.13.2
       - run: >-
           cargo +nightly-2026-10-13 fuzz run "$FUZZ_TARGET" --target x86_64-unknown-linux-gnu
-          -- -max_total_time=18000 -max_len=16384
+          -- -max_total_time=900 -max_len=16384
       - if: failure()
         uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9  # v7.0.2
         with:

CONTRIBUTING.md

@@ -60,7 +60,7 @@ cargo +nightly fuzz run command-line -- -max_total_time=600 -max_len=16384
 cargo +nightly fuzz run environment-block -- -max_total_time=600 -max_len=16384
 ```
 
-`WINDOWS_SPAWN_RANDOM_SCALE` multiplies the number of random command lines and environments, which the nightly workflow raises to fifty times.
+`WINDOWS_SPAWN_RANDOM_SCALE` multiplies the number of random command lines and environments, which the nightly workflow raises to ten times.
 
 ## Expectations
 

docs/adr/0013-repository-laws-are-enforced-mechanically.md

@@ -35,5 +35,7 @@ Rustc lints are limited to those Rust 1.75 recognizes.
 ## Consequences
 
 - Changing a law changes the lint table, `clippy.toml`, or the gate, with its tests.
-- Pointer-integer and `DWORD` width conversions keep `as` behind registered exceptions in `sys`, because Rust 1.75 has no `From` form for them.
+- Reading a handle's value keeps `as` behind a registered exception in `sys`, because Rust 1.75 has no pointer `addr`.
+  A value becomes a handle through a byte offset from null.
+  A `DWORD` width converts through its bytes in `domain::conversion_rules`, where Kani proves each conversion for every input.
 - When the MSRV reaches Rust 1.81, `#[expect(…, reason = …)]` replaces the registry.

docs/adr/0017-long-careful-and-fuzzed-runs.md

@@ -13,16 +13,16 @@ PR #14 ran a stress test, `cargo careful`, an ARM64 smoke test, Miri, AddressSan
 - An ignored test, `spawn_cleanup_stress`, spawns children in thirteen modes.
   The modes cover both commits, a dropped suspended child, collected output, written input, a killed tree, transferred handles, a Job, an alternate parent, and two failed spawns.
   It requires the process's handle count to end where it started, after a warm-up that runs each mode twice.
-  `WINDOWS_SPAWN_STRESS_CASES` sets the number of spawns: 1300 on every PR on x64 and i686, and 100000 on x64 and 20000 on i686 every night.
+  `WINDOWS_SPAWN_STRESS_CASES` sets the number of spawns: 1300 on every PR on x64 and i686, and 20000 on x64 and 5000 on i686 every night.
 - CI runs the Windows tests under `cargo careful`, whose standard library checks the preconditions of the unsafe operations in `sys`, such as those of `slice::from_raw_parts`.
 - CI runs `cargo xtask test` on a Windows 11 ARM64 runner.
 - A `fuzz` crate compiles the encoder and the block builder from `src/domain`, and requires the parser models to read back what they wrote.
   The parser models and the block scan compile under `cfg(fuzzing)` for it.
-  Each target runs for ten minutes on every PR, and for five hours every night.
+  Each target runs for ten minutes on every PR, and for fifteen minutes every night.
   The fuzz crate is its own workspace, outside the package, the MSRV, and the workspace lints, and the repository gate checks its targets.
 - Miri and AddressSanitizer run the platform-neutral decisions on Linux.
   Those decisions hold no unsafe code, so these runs guard against a change that brings some in, at the cost of minutes.
-- `WINDOWS_SPAWN_RANDOM_SCALE` multiplies the random command lines and environments, which keep their seeds, and the nightly workflow runs them at fifty times their size.
+- `WINDOWS_SPAWN_RANDOM_SCALE` multiplies the random command lines and environments, which keep their seeds, and the nightly workflow runs them at ten times their size.
 
 Rejected:
 
@@ -34,6 +34,6 @@ Rejected:
 ## Consequences
 
 - CI gains six jobs, and `required` waits for each of them.
-- A leak in every spawn fails a PR, and a rarer leak fails the nightly run, whose 100000 spawns let it add up.
+- A leak in every spawn fails a PR, and a rarer leak fails the nightly run, whose 20000 spawns let it add up.
 - A failed fuzz run uploads the input that failed.
-- The nightly workflow runs on its schedule or on demand, and it gates no PR.
+- The nightly workflow runs on its schedule or on demand, spends about an hour of runner time, and gates no PR.

proofs/README.md

@@ -6,7 +6,7 @@ Each layer runs a pinned tool, accepts only the complete expected result, and ru
 
 | Layer | Tool | What it proves | How it reaches the code |
 | --- | --- | --- | --- |
-| `kani` | Kani 0.68.0 | The decision cores in `src/domain` and the mitigation layout, for every input within each harness's bounds | It runs the crate's own functions |
+| `kani` | Kani 0.68.0 | The decision cores and `DWORD` conversions in `src/domain` and the mitigation layout, for every input within each harness's bounds | It runs the crate's own functions |
 | `lean` | Lean 4.35.0 | Both C runtime parsers read back every command line the encoder writes, for arguments of every length | Vectors from the proved model, which the Rust tests and the Windows parsers check |
 | `verus` | Verus 0.2026.10.04 | The encoder writes what the Lean model writes, for every argument | A copy that must equal the crate's functions token for token |
 | `tla` | `TLC` 1.7.4 | `Child::wait_with_output` returns with every byte, and each of two plausible mistakes deadlocks or never returns | A model of the protocol |

src/domain/conversion_rules.rs

@@ -0,0 +1,99 @@
+//! Conversions between Win32 widths and Rust integers that `From` does not offer, written without `as`.
+//!
+//! A `DWORD` widens to a `usize`, and a compile-time size narrows to a `DWORD`, through their little-endian bytes.
+
+use std::mem::size_of;
+
+const _: () = assert!(
+    size_of::<usize>() >= size_of::<u32>(),
+    "a usize holds every DWORD"
+);
+
+/// Widens a `DWORD` through its bytes, which the low bytes of a `usize` hold.
+pub(crate) fn widen(value: u32) -> usize {
+    let mut bytes = [0_u8; size_of::<usize>()];
+    for (slot, byte) in bytes.iter_mut().zip(value.to_le_bytes()) {
+        *slot = byte;
+    }
+    usize::from_le_bytes(bytes)
+}
+
+/// Returns true if `value` fits a `DWORD`.
+///
+/// A shift by 32 bits finds the high bits of a 64-bit `usize`, and a 32-bit `usize` has none.
+const fn fits_dword(value: usize) -> bool {
+    match value.checked_shr(u32::BITS) {
+        Some(high) => high == 0,
+        None => true,
+    }
+}
+
+/// Converts a compile-time size to a Win32 `DWORD`; a size that does not fit fails constant evaluation.
+pub(crate) const fn dword_const(value: usize) -> u32 {
+    assert!(fits_dword(value), "size does not fit a DWORD");
+    let [first, second, third, fourth, ..] = value.to_le_bytes();
+    u32::from_le_bytes([first, second, third, fourth])
+}
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    #[kani::proof]
+    fn every_dword_widens_to_its_value() {
+        let value: u32 = kani::any();
+        assert_eq!(widen(value) as u64, u64::from(value));
+        kani::cover!(value == u32::MAX);
+    }
+
+    #[kani::proof]
+    fn a_size_fits_a_dword_exactly_up_to_its_maximum() {
+        let value: usize = kani::any();
+        assert_eq!(fits_dword(value), value <= u32::MAX as usize);
+        kani::cover!(value == u32::MAX as usize);
+        kani::cover!(value == u32::MAX as usize + 1);
+    }
+
+    #[kani::proof]
+    fn every_size_within_a_dword_narrows_to_its_value() {
+        let value: usize = kani::any();
+        kani::assume(value <= u32::MAX as usize);
+        assert_eq!(u64::from(dword_const(value)), value as u64);
+        kani::cover!(value == u32::MAX as usize);
+    }
+
+    #[kani::proof]
+    fn negative_control_bytes_in_big_endian_order() {
+        let value: u32 = kani::any();
+        let mut bytes = [0_u8; size_of::<usize>()];
+        for (slot, byte) in bytes.iter_mut().zip(value.to_be_bytes()) {
+            *slot = byte;
+        }
+        assert!(
+            usize::from_le_bytes(bytes) as u64 == u64::from(value),
+            "NEGATIVE_CONVERSION_CONTROL"
+        );
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn conversions_keep_their_values() {
+        assert_eq!(widen(0), 0);
+        assert_eq!(widen(0x0102_0304), 0x0102_0304);
+        assert_eq!(widen(u32::MAX), 0xFFFF_FFFF);
+        assert_eq!(dword_const(0), 0);
+        assert_eq!(dword_const(0x0102_0304), 0x0102_0304);
+        assert_eq!(dword_const(widen(u32::MAX)), u32::MAX);
+    }
+
+    #[test]
+    #[cfg(target_pointer_width = "64")]
+    #[should_panic(expected = "size does not fit a DWORD")]
+    fn a_size_past_a_dword_panics() {
+        dword_const(widen(u32::MAX) + 1);
+    }
+}

src/domain/mod.rs

@@ -4,6 +4,7 @@
 
 pub(crate) mod attribute_rules;
 pub(crate) mod command_line_rules;
+pub(crate) mod conversion_rules;
 pub(crate) mod creation_flag_rules;
 pub(crate) mod environment_rules;
 pub(crate) mod plan_rules;

src/sys.rs

@@ -47,6 +47,7 @@ use windows_sys::Win32::System::Threading::{
 };
 
 use crate::domain::attribute_rules::{self, SizeFault};
+use crate::domain::conversion_rules::{dword_const, widen};
 use crate::domain::creation_flag_rules::{creation_word, ConsoleFlag, PriorityFlag};
 use crate::domain::environment_rules;
 use crate::handles::BorrowedPseudoConsole;
@@ -1355,29 +1356,18 @@ fn is_valid_handle(handle: HANDLE) -> bool {
 }
 
 /// Returns a handle's numeric value, as a child sees it in an argument or the environment.
+///
+/// Rust 1.75 has no `addr` for pointers, so reading the value takes `as`.
 #[allow(clippy::as_conversions)]
 pub(crate) fn handle_value(handle: HANDLE) -> isize {
     handle as isize
 }
 
 /// Returns the handle a numeric value names.
-#[allow(clippy::as_conversions)]
+///
+/// A handle is an opaque value that no code dereferences, so the pointer carries no provenance, as `ptr::without_provenance_mut` would make it.
 pub(crate) const fn handle_from_value(value: isize) -> HANDLE {
-    value as HANDLE
-}
-
-/// Converts a compile-time size to a Win32 `DWORD`; a size that does not fit fails constant evaluation.
-#[allow(clippy::as_conversions, clippy::cast_possible_truncation)]
-const fn dword_const(value: usize) -> u32 {
-    let wide = value as u64;
-    assert!(wide <= u32::MAX as u64, "size does not fit a DWORD");
-    wide as u32
-}
-
-/// Widens a `DWORD`; `usize` has at least 32 bits on every Windows target.
-#[allow(clippy::as_conversions)]
-const fn widen(value: u32) -> usize {
-    value as usize
+    ptr::null_mut::<c_void>().wrapping_byte_offset(value)
 }
 
 /// Returns true if `error` carries the Win32 error `code`.

tests/lifecycle/mod.rs

@@ -248,8 +248,9 @@ fn differs(what: &str, expected: impl Display, actual: impl Display) -> io::Erro
     ))
 }
 
+/// A probe's exit as the model names it; an exit without a code, which Windows never reports, matches no row.
 fn status_of(code: Option<i32>) -> String {
-    format!("Status {}", code.expect("a probe exits with a code"))
+    code.map_or_else(|| "Status none".to_owned(), |code| format!("Status {code}"))
 }
 
 /// Replays every trace of `table` and returns the first disagreement.

tests/support/mod.rs

@@ -47,8 +47,8 @@ pub(crate) fn pipe() -> io::Result<(File, File)> {
     // SAFETY: CreatePipe succeeded, so both handles are new and distinct.
     let (read, write) = unsafe {
         (
-            OwnedHandle::from_raw_handle(read as RawHandle),
-            OwnedHandle::from_raw_handle(write as RawHandle),
+            OwnedHandle::from_raw_handle(read),
+            OwnedHandle::from_raw_handle(write),
         )
     };
     Ok((File::from(read), File::from(write)))
@@ -76,7 +76,7 @@ pub(crate) fn local_duplicate<T: AsHandle>(
         return Err(io::Error::last_os_error());
     }
     // SAFETY: DuplicateHandle returned a new, uniquely owned handle.
-    Ok(unsafe { OwnedHandle::from_raw_handle(duplicate as RawHandle) })
+    Ok(unsafe { OwnedHandle::from_raw_handle(duplicate) })
 }
 
 /// The test's end of a probe's gate pipe.
@@ -87,7 +87,10 @@ pub(crate) struct Gate(Option<File>);
 impl Gate {
     /// Makes one probe exit with `code`.
     pub(crate) fn open_with(&mut self, code: u8) -> io::Result<()> {
-        let mut writer = self.0.take().expect("the gate is still closed");
+        let mut writer = self
+            .0
+            .take()
+            .ok_or_else(|| io::Error::other("the gate is already open"))?;
         writer.write_all(&[code])
     }
 
@@ -268,9 +271,10 @@ fn adopt_pipe(variable: &str) -> io::Result<File> {
         .map_err(|error| io::Error::new(io::ErrorKind::NotFound, error))?
         .parse()
         .map_err(|error| io::Error::new(io::ErrorKind::InvalidData, error))?;
+    let raw: RawHandle = ptr::null_mut();
     // SAFETY: the parent listed this inheritable handle in PROC_THREAD_ATTRIBUTE_HANDLE_LIST and published its value only in `variable`.
     // This process adopts it exactly once.
-    let handle = unsafe { OwnedHandle::from_raw_handle(value as RawHandle) };
+    let handle = unsafe { OwnedHandle::from_raw_handle(raw.wrapping_byte_offset(value)) };
     // SAFETY: the owned handle is valid for the query.
     if unsafe { GetFileType(handle.as_raw_handle()) } != FILE_TYPE_PIPE {
         return Err(io::Error::new(io::ErrorKind::InvalidData, "not a pipe"));