diff --git a/.github/workflows/deep-verification.yml b/.github/workflows/deep-verification.yml index f2a12bc..cbea857 100644 --- a/.github/workflows/deep-verification.yml +++ b/.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: diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b184df9..9bbdd20 100644 --- a/CONTRIBUTING.md +++ b/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 diff --git a/docs/adr/0013-repository-laws-are-enforced-mechanically.md b/docs/adr/0013-repository-laws-are-enforced-mechanically.md index a49cd3d..385121a 100644 --- a/docs/adr/0013-repository-laws-are-enforced-mechanically.md +++ b/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. diff --git a/docs/adr/0017-long-careful-and-fuzzed-runs.md b/docs/adr/0017-long-careful-and-fuzzed-runs.md index 73c4ca6..d0845a6 100644 --- a/docs/adr/0017-long-careful-and-fuzzed-runs.md +++ b/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. diff --git a/proofs/README.md b/proofs/README.md index fd0e248..184d592 100644 --- a/proofs/README.md +++ b/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 | diff --git a/src/domain/conversion_rules.rs b/src/domain/conversion_rules.rs new file mode 100644 index 0000000..b63fbc2 --- /dev/null +++ b/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::() >= size_of::(), + "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::()]; + 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::()]; + 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); + } +} diff --git a/src/domain/mod.rs b/src/domain/mod.rs index 0f02334..218d404 100644 --- a/src/domain/mod.rs +++ b/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; diff --git a/src/sys.rs b/src/sys.rs index c4a84eb..fd52ad8 100644 --- a/src/sys.rs +++ b/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::().wrapping_byte_offset(value) } /// Returns true if `error` carries the Win32 error `code`. diff --git a/tests/lifecycle/mod.rs b/tests/lifecycle/mod.rs index 0635ee4..939cb74 100644 --- a/tests/lifecycle/mod.rs +++ b/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) -> 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. diff --git a/tests/support/mod.rs b/tests/support/mod.rs index 045436c..53b3f94 100644 --- a/tests/support/mod.rs +++ b/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( 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); 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 { .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")); diff --git a/tests/windows_spawn.rs b/tests/windows_spawn.rs index c1f5c51..2a3641d 100644 --- a/tests/windows_spawn.rs +++ b/tests/windows_spawn.rs @@ -1,9 +1,7 @@ -#![cfg_attr(not(windows), allow(missing_docs))] -#![cfg(windows)] -#![allow(clippy::as_conversions, clippy::expect_used, clippy::unwrap_in_result)] - //! End-to-end Windows process creation tests. +#![cfg(windows)] + #[cfg(windows_spawn_vectors)] mod lifecycle; mod support; @@ -12,7 +10,7 @@ use std::fs::{self, File}; use std::io::{self, Read, Write}; use std::mem::size_of_val; use std::os::windows::fs::OpenOptionsExt; -use std::os::windows::io::{AsHandle, AsRawHandle, FromRawHandle, OwnedHandle, RawHandle}; +use std::os::windows::io::{AsHandle, AsRawHandle, FromRawHandle, OwnedHandle}; use std::path::Path; use std::sync::mpsc; use std::thread; @@ -60,8 +58,7 @@ fn attached_to_test_pseudoconsole() -> bool { }; let mut information = CONSOLE_SCREEN_BUFFER_INFO::default(); // SAFETY: `output` is an open console handle and `information` is writable. - let queried = - unsafe { GetConsoleScreenBufferInfo(output.as_raw_handle() as HANDLE, &mut information) }; + let queried = unsafe { GetConsoleScreenBufferInfo(output.as_raw_handle(), &mut information) }; queried != 0 && information.dwSize.X == PCON_SIZE.X && information.dwSize.Y == PCON_SIZE.Y } @@ -597,8 +594,8 @@ impl TestPseudoConsole { // SAFETY: CreatePipe succeeded and returned two distinct handles. Ok(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), ) }) } @@ -610,8 +607,8 @@ impl TestPseudoConsole { let result = unsafe { CreatePseudoConsole( PCON_SIZE, - input_reader.as_raw_handle() as HANDLE, - output_writer.as_raw_handle() as HANDLE, + input_reader.as_raw_handle(), + output_writer.as_raw_handle(), 0, &mut value, ) @@ -647,7 +644,7 @@ impl TestPseudoConsole { let writer = self .input_writer .as_ref() - .expect("a live pseudoconsole retains its input writer"); + .ok_or_else(|| io::Error::other("the pseudoconsole's input writer is closed"))?; let mut written = 0_u32; let length = u32::try_from(input.len()) .map_err(|error| io::Error::new(io::ErrorKind::InvalidInput, error))?; @@ -955,29 +952,49 @@ fn capability_wrappers_and_all_option_builders_are_exercised() -> io::Result<()> Ok(()) } +/// The radix of the `{:p}` text of a handle. +const HEXADECIMAL: u32 = 16; + +/// The error of an excluded-handle probe value that doesn't parse. +fn malformed_probe(value: &str, what: &str, cause: impl std::fmt::Display) -> io::Error { + io::Error::new( + io::ErrorKind::InvalidData, + format!("the probe's {what} in {value:?} is malformed: {cause}"), + ) +} + +/// The fields of the excluded-handle probe: the handle as the `{:p}` text of its value, then the file's volume and index. +fn probe_fields(value: &str) -> io::Result<(HANDLE, u32, u64)> { + let [handle_text, volume, index] = value.split(':').collect::>()[..] else { + return Err(malformed_probe( + value, + "field count", + "it needs three fields", + )); + }; + let digits = handle_text + .strip_prefix("0x") + .ok_or_else(|| malformed_probe(value, "handle", "it lacks the 0x prefix"))?; + let address = usize::from_str_radix(digits, HEXADECIMAL) + .map_err(|error| malformed_probe(value, "handle", error))?; + let null: HANDLE = std::ptr::null_mut(); + Ok(( + null.wrapping_byte_add(address), + volume + .parse() + .map_err(|error| malformed_probe(value, "volume", error))?, + index + .parse() + .map_err(|error| malformed_probe(value, "file index", error))?, + )) +} + #[test] fn handle_list_excludes_an_unlisted_inheritable_handle() -> io::Result<()> { const PROBE: &str = "WINDOWS_SPAWN_EXCLUDED_HANDLE_PROBE"; if let Some(value) = std::env::var_os(PROBE) { - let value = value.to_string_lossy(); - let mut fields = value.split(':'); - let handle = fields - .next() - .expect("probe handle is present") - .parse::() - .expect("probe handle must be an integer"); - let volume = fields - .next() - .expect("probe volume is present") - .parse::() - .expect("probe volume must be an integer"); - let index = fields - .next() - .expect("probe file index is present") - .parse::() - .expect("probe file index must be an integer"); - assert!(fields.next().is_none(), "probe has exactly three fields"); - if let Ok(identity) = file_identity(handle as HANDLE) { + let (handle, volume, index) = probe_fields(&value.to_string_lossy())?; + if let Ok(identity) = file_identity(handle) { assert_ne!( identity, (volume, index), @@ -992,9 +1009,9 @@ fn handle_list_excludes_an_unlisted_inheritable_handle() -> io::Result<()> { let listed_file = File::open("NUL")?; let excluded_file = File::create(&excluded_path)?; let excluded = inheritable_duplicate(&excluded_file)?; - let excluded_value = excluded.as_handle().as_raw_handle() as isize; - let (excluded_volume, excluded_index) = file_identity(excluded.as_handle().as_raw_handle())?; - let probe = format!("{excluded_value}:{excluded_volume}:{excluded_index}"); + let excluded_raw = excluded.as_handle().as_raw_handle(); + let (excluded_volume, excluded_index) = file_identity(excluded_raw)?; + let probe = format!("{excluded_raw:p}:{excluded_volume}:{excluded_index}"); let mut command = Command::new(std::env::current_exe()?); command diff --git a/xtask/src/gates.rs b/xtask/src/gates.rs index 5ffea55..19ebd01 100644 --- a/xtask/src/gates.rs +++ b/xtask/src/gates.rs @@ -24,14 +24,8 @@ const EXCEPTIONS: &[Exception] = &[ Exception { file: "src/sys.rs", lint: "clippy::as_conversions", - count: 4, - reason: "handle values and Win32 widths convert where Rust 1.75 has no From form", - }, - Exception { - file: "src/sys.rs", - lint: "clippy::cast_possible_truncation", count: 1, - reason: "dword_const is evaluated in constants, where an oversized value fails the build", + reason: "handle_value reads a handle's value, and Rust 1.75 has no pointer addr", }, Exception { file: "tests/support/mod.rs", @@ -39,30 +33,6 @@ const EXCEPTIONS: &[Exception] = &[ count: 1, reason: "a probe reports by exit code", }, - Exception { - file: "tests/windows_spawn.rs", - lint: "missing_docs", - count: 1, - reason: "the test crate is empty off Windows", - }, - Exception { - file: "tests/windows_spawn.rs", - lint: "clippy::as_conversions", - count: 1, - reason: "tests call Win32 directly with handle values", - }, - Exception { - file: "tests/windows_spawn.rs", - lint: "clippy::expect_used", - count: 1, - reason: "tests assert by panicking", - }, - Exception { - file: "tests/windows_spawn.rs", - lint: "clippy::unwrap_in_result", - count: 1, - reason: "tests assert by panicking", - }, ]; /// Identifiers that measure or wait on time (ADR 0010). diff --git a/xtask/src/proofs/kani.rs b/xtask/src/proofs/kani.rs index 96573ea..4a3188b 100644 --- a/xtask/src/proofs/kani.rs +++ b/xtask/src/proofs/kani.rs @@ -55,6 +55,18 @@ pub(crate) const KANI_PROOFS: &[Proof] = &[ name: "domain::command_line_rules::proofs::plain_arguments_stay_verbatim", covers: 2, }, + Proof { + name: "domain::conversion_rules::proofs::every_dword_widens_to_its_value", + covers: 1, + }, + Proof { + name: "domain::conversion_rules::proofs::a_size_fits_a_dword_exactly_up_to_its_maximum", + covers: 2, + }, + Proof { + name: "domain::conversion_rules::proofs::every_size_within_a_dword_narrows_to_its_value", + covers: 1, + }, Proof { name: "domain::creation_flag_rules::proofs::the_word_holds_the_policy_one_console_one_priority_and_the_internal_flags", covers: 2, @@ -99,6 +111,10 @@ pub(crate) const KANI_CONTROLS: &[Control] = &[ name: "domain::command_line_rules::proofs::negative_control_unescaped_closing_quote", marker: "NEGATIVE_COMMAND_LINE_CONTROL", }, + Control { + name: "domain::conversion_rules::proofs::negative_control_bytes_in_big_endian_order", + marker: "NEGATIVE_CONVERSION_CONTROL", + }, Control { name: "domain::creation_flag_rules::proofs::negative_control_a_spawn_that_runs_at_once", marker: "NEGATIVE_CREATION_FLAG_CONTROL",