Module formal 

Kani

79 passed, 0 failed.

algebra::lazy_map::verification

Harness	Harness assertions	Result
proof_clamp_add_composition	[Success] For every i64 key and two ordered clamp intervals with arbitrary i64 biases whose sum fits i64, composition agrees with sequential saturating actions [Success] attempt to add with overflow [Success] attempt to negate with overflow [Success] attempt to shift left with overflow [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 22.989 s Cover: 4/4 reached
proof_clamp_add_constructors	[Success] For all i64 keys and update values, chmin, chmax and add construct the corresponding clamp or saturating addition [Success] The identity clamp/add action preserves every i64 key	Success 0.874 s Cover: 2/2 reached
proof_max_update	[Success] For all nonempty i64 extrema aggregates and optional assignments, updating after merging equals merging after updating [Success] For every i64 aggregate and pair of optional assignments, composition applies them in order and the last present assignment wins [Success] For every i64 extremum aggregate, the identity update preserves its value [Success] For every i64 key and optional assignment, updating its singleton aggregate agrees with updating the key	Success 0.658 s Cover: 2/2 reached
proof_min_update	[Success] For all nonempty i64 extrema aggregates and optional assignments, updating after merging equals merging after updating [Success] For every i64 aggregate and pair of optional assignments, composition applies them in order and the last present assignment wins [Success] For every i64 extremum aggregate, the identity update preserves its value [Success] For every i64 key and optional assignment, updating its singleton aggregate agrees with updating the key	Success 0.649 s Cover: 2/2 reached

algebra::operations::logical_linear_operation_impl::verification

Harness	Harness assertions	Result
proof_composition	[Success] Composition applies a then b for all u64 masks, XOR terms and inputs	Success 0.196 s Cover: 1/1 reached
proof_laws	[Success] Associativity for all u64 operations [Success] Left identity for all u64 operations [Success] Right identity for all u64 operations	Success 0.189 s
proof_power	[Success] For all u64 operations and exponents, power 0 is identity; positive powers preserve constant/identity bits and toggle negated bits exactly when the exponent is odd [Success] attempt to shift left with overflow	Success 14.475 s Cover: 3/3 reached

algorithm::binary_search::verification

Harness	Harness assertions	Result
proof_f32_midpoint	[Success] For all f32 bit patterns, midpoint search stops only at identical or adjacent total-order representations; negative and positive zero are adjacent [Success] For every pair of f32 bit patterns, including infinities and NaNs, a midpoint strictly reduces the interval in Rust total_cmp order [Success] attempt to shift left with overflow [Success] attempt to subtract with overflow	Success 1.405 s Cover: 3/3 reached
proof_f64_midpoint	[Success] For all f64 bit patterns, midpoint search stops only at identical or adjacent total-order representations; negative and positive zero are adjacent [Success] For every pair of f64 bit patterns, including infinities and NaNs, a midpoint strictly reduces the interval in Rust total_cmp order [Success] attempt to shift left with overflow [Success] attempt to subtract with overflow	Success 4.183 s Cover: 3/3 reached
proof_signed_midpoint	[Success] For all i128 endpoints in either order, a midpoint strictly reduces the search interval [Success] For all i128 endpoints, search stops only at equal or adjacent values	Success 4.188 s Cover: 2/2 reached
proof_unsigned_midpoint	[Success] For all u128 endpoints in either order, a midpoint strictly reduces the search interval [Success] For all u128 endpoints, search stops only at equal or adjacent values	Success 1.462 s Cover: 2/2 reached

algorithm::bitdp::verification

Harness	Harness assertions	Result
proof_combination_start	[Success] For every 0 <= k <= n < 64, u64 combination enumeration starts with a valid k-bit selection among n bits [Success] The first u64 combination is the smallest integer with the requested number of selected bits [Success] attempt to shift left with overflow	Success 0.483 s Cover: 2/2 reached
proof_combination_step	[Success] Every next u64 combination on at most 63 bits increases and preserves the number of selected bits [Success] For every u64 combination state on 0 through 63 bits, the iterator yields the current combination [Success] The next u64 combination is the smallest larger value with the same popcount, so it skips none [Success] attempt to shift left with overflow [Success] attempt to subtract with overflow [Success] u64 combination enumeration ends exactly when no larger combination remains and stays exhausted	Success 89.674 s Cover: 4/4 reached
proof_subset_step	[Success] Each u64 subset step chooses the greatest smaller submask, so it skips none [Success] Each u64 subset step strictly decreases while remaining a submask [Success] For every u64 mask and current submask, the iterator yields that submask [Success] For every u64 mask, subset enumeration starts with the entire mask [Success] attempt to shift left with overflow [Success] u64 subset enumeration ends exactly after zero and stays exhausted	Success 0.340 s Cover: 2/2 reached

algorithm::dyadic_ranges::verification

Harness	Harness assertions	Result
proof_dyadic_step	[Success] Empty and reversed u64 intervals produce no dyadic ranges and stay exhausted [Success] For all nonempty u64 intervals, the first dyadic range starts at the left endpoint, is aligned, has power-of-two length and fits within the interval [Success] For all u64 intervals, dyadic iteration advances without gaps and stops only at the right endpoint [Success] For all u64 intervals, the emitted dyadic range has the largest aligned power-of-two length that fits at the current left endpoint [Success] attempt to add with overflow [Success] attempt to multiply with overflow [Success] attempt to subtract with overflow	Success 3.297 s Cover: 2/2 reached

algorithm::quotient_index::verification

Harness	Harness assertions	Result
proof_quotient_constructors_u64_max	[Success] On 64-bit targets, for every numerator from (2^32-1)^2 through usize::MAX, the actual ceiling constructor stores square root 2^32-1 and its exact ceiling quotient; all three pivot values and both square-interval endpoints are covered [Success] On 64-bit targets, for every numerator from (2^32-1)^2 through usize::MAX, the actual floor constructor stores square root 2^32-1 and its exact floor quotient; all three pivot values and both square-interval endpoints are covered [Success] attempt to add with overflow [Success] attempt to multiply with overflow [Success] attempt to subtract with overflow	Success 11.938 s Cover: 5/5 reached

algorithm::sort::verification

Harness	Harness assertions	Result
proof_merge_sort	[Success] For four arbitrary u8 values and every possible u8 value, merge sort preserves its multiplicity [Success] For four arbitrary u8 values, merge sort returns values in ascending order [Success] index out of bounds: the length is less than or equal to the given index	Success 11.067 s Cover: 2/2 reached
proof_signed_radix_key	[Success] For every pair of i128 values, the sixteen radix bytes preserve signed numeric ordering and equality [Success] attempt to multiply with overflow [Success] attempt to shift left with overflow	Success 0.870 s Cover: 2/2 reached

algorithm::ternary_search::verification

Harness	Harness assertions	Result
proof_f32_key	[Success] For every f32 bit pattern, ternary-search keys round-trip and preserve total_cmp order, including NaN payloads, infinities, and signed zeros	Success 0.157 s Cover: 2/2 reached
proof_f64_key	[Success] For every f64 bit pattern, ternary-search keys round-trip and preserve total_cmp order, including NaN payloads, infinities, and signed zeros	Success 0.227 s Cover: 2/2 reached
proof_signed_key	[Success] For all i128 values, ternary-search keys round-trip exactly and preserve signed order over the full domain	Success 0.336 s Cover: 1/1 reached

data_structure::allocator::verification

Harness	Harness assertions	Result
proof_pool_reuse	[Success] Deallocating either of two owned u8 values across a pool growth returns that value [Success] Reusing either slot writes the new owned value and preserves the other live pointer and value [Success] The next allocation reuses the removed slot, whether it belongs to the current or an older chunk [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 11.744 s Cover: 2/2 reached
proof_pool_zero_sized_drop	[Success] After any removal subset of four zero-sized values and one further allocation, pool destruction drops exactly all five values [Success] Allocating or reusing an over-aligned zero-sized value preserves its 64-byte alignment [Success] For four aligned zero-sized pool values, deallocating any subset drops exactly those values [Success] attempt to calculate the remainder with a divisor of zero [Success] attempt to shift right with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 21.038 s Cover: 2/2 reached

data_structure::binary_indexed_tree::verification

Harness	Harness assertions	Result
proof_group_range_order	[Success] For any sequence of four permutations of three labels and every valid range, Fenwick range cancellation preserves noncommutative composition order, including empty ranges [Success] index out of bounds: the length is less than or equal to the given index	Success 55.896 s Cover: 2/2 reached
proof_prefix_order	[Success] For all four u8 bitwise affine maps and every valid prefix, Fenwick construction and accumulation preserve left-to-right noncommutative order [Success] For all four u8 bitwise affine maps and every valid prefix, updating an empty Fenwick tree in ascending index order preserves noncommutative composition	Success 9.455 s Cover: 2/2 reached

data_structure::binary_trie::verification

Harness	Harness assertions	Result
proof_range_bounds	[Success] Binary-trie range normalization preserves membership for every u64 key, including included, excluded, unbounded, reversed, and empty ranges [Success] For every binary-trie key width from 0 through 64 and all valid u64 bounds, a normalized nonempty range stays within the key universe [Success] attempt to shift left with overflow	Success 2.537 s Cover: 2/2 reached

data_structure::bit_vector::verification

Harness	Harness assertions	Result
proof_scalar_select	[Success] For every nonzero u64 word and valid rank, exactly rank set bits precede the scalar selection [Success] For every nonzero u64 word and valid zero-based rank, scalar select returns the position of a set bit [Success] attempt to shift left with overflow [Success] attempt to shift right with overflow [Success] attempt to subtract with overflow	Success 20.764 s Cover: 3/3 reached

data_structure::bitset::verification

Harness	Harness assertions	Result
proof_parse_binary_scalar	[Success] For every 64-byte input, scalar binary parsing accepts exactly ASCII zeroes and ones [Success] For every valid 64-byte binary input and every bit index, scalar parsing stores that character at the corresponding bit in a zero-initialized word [Success] attempt to shift left with overflow [Success] attempt to shift right with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 13.516 s Cover: 3/3 reached

data_structure::compressed_binary_indexed_tree::verification

Harness	Harness assertions	Result
proof_ordered_updates	[Success] For all four u8 bitwise affine maps inserted at diagonal coordinates 0 through 3, compressed Fenwick prefix queries preserve noncommutative insertion order in both dimensions [Success] index out of bounds: the length is less than or equal to the given index	Success 89.498 s Cover: 2/2 reached

data_structure::dary_heap::verification

Harness	Harness assertions	Result
proof_u128_block	[Success] For every nonempty partially filled four-lane u128 block, scalar maximum selection chooses an occupied lane even when all real values equal the zero padding [Success] Scalar u128 maximum selection returns the first maximum over the full 128-bit domain [Success] Split high and low u64 storage preserves every u128 value and leaves padding zero [Success] index out of bounds: the length is less than or equal to the given index	Success 8.659 s Cover: 2/2 reached

data_structure::dual_segment_tree::verification

Harness	Harness assertions	Result
proof_updates_four	[Success] For every array of 4 u8 bitwise affine maps, two arbitrary range updates with an intervening point assignment preserve action order at every point and input [Success] index out of bounds: the length is less than or equal to the given index	Success 33.205 s Cover: 3/3 reached
proof_updates_three	[Success] For every array of 3 u8 bitwise affine maps, two arbitrary range updates with an intervening point assignment preserve action order at every point and input [Success] index out of bounds: the length is less than or equal to the given index	Success 29.732 s Cover: 3/3 reached

data_structure::radix_heap::verification

Harness	Harness assertions	Result
proof_buckets_u32	[Success] For all monotone u32 keys, the radix bucket index is in bounds and bucket zero contains exactly the last removed key [Success] For all u32 keys not below last, every key in an earlier radix bucket is smaller than every key in a later bucket [Success] For all u32 keys, choosing the minimum of a nonzero bucket as the new last moves every member to a strictly earlier bucket [Success] attempt to shift left with overflow [Success] attempt to subtract with overflow	Success 0.155 s Cover: 2/2 reached
proof_buckets_u64	[Success] For all monotone u64 keys, the radix bucket index is in bounds and bucket zero contains exactly the last removed key [Success] For all u64 keys not below last, every key in an earlier radix bucket is smaller than every key in a later bucket [Success] For all u64 keys, choosing the minimum of a nonzero bucket as the new last moves every member to a strictly earlier bucket [Success] attempt to shift left with overflow [Success] attempt to subtract with overflow	Success 0.604 s Cover: 2/2 reached

data_structure::segment_tree::verification

Harness	Harness assertions	Result
proof_fold_four	[Success] For all 4 u8 bitwise affine maps, every set/update/clear and every valid range, SegmentTree folds in left-to-right composition order, including empty ranges [Success] index out of bounds: the length is less than or equal to the given index	Success 26.704 s Cover: 3/3 reached
proof_fold_three	[Success] For all 3 u8 bitwise affine maps, every set/update/clear and every valid range, SegmentTree folds in left-to-right composition order, including empty ranges [Success] index out of bounds: the length is less than or equal to the given index	Success 18.511 s Cover: 3/3 reached
proof_partition_five	[Success] For every 5-element i8 array and every nonnegative i16 limit, partition_point_acc returns the maximal interval whose running sums from the search endpoint stay within the limit; signed values make the prefix-maximum monoid noncommutative [Success] attempt to add with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 44.232 s Cover: 3/3 reached
proof_rpartition_five	[Success] For every 5-element i8 array and every nonnegative i16 limit, rpartition_point_acc returns the maximal interval whose running sums from the search endpoint stay within the limit; signed values make the prefix-maximum monoid noncommutative [Success] attempt to add with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 76.770 s Cover: 3/3 reached

data_structure::sliding_window_aggregation::verification

Harness	Harness assertions	Result
proof_deque_back_four	[Success] After an endpoint removal and insertion from a 4-element deque, length, endpoints and noncommutative aggregate match the logical order [Success] Both removal directions return None on an empty DequeAggregation [Success] For all 4 u8 bitwise affine maps inserted with push_front, pop_back rebalances and returns the opposite endpoint [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 18.578 s Cover: 2/2 reached
proof_deque_back_three	[Success] After an endpoint removal and insertion from a 3-element deque, length, endpoints and noncommutative aggregate match the logical order [Success] Both removal directions return None on an empty DequeAggregation [Success] For all 3 u8 bitwise affine maps inserted with push_front, pop_back rebalances and returns the opposite endpoint [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 16.103 s Cover: 2/2 reached
proof_deque_front_four	[Success] After an endpoint removal and insertion from a 4-element deque, length, endpoints and noncommutative aggregate match the logical order [Success] Both removal directions return None on an empty DequeAggregation [Success] For all 4 u8 bitwise affine maps inserted with push_back, pop_front rebalances and returns the opposite endpoint [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 11.602 s Cover: 2/2 reached
proof_deque_front_three	[Success] After an endpoint removal and insertion from a 3-element deque, length, endpoints and noncommutative aggregate match the logical order [Success] Both removal directions return None on an empty DequeAggregation [Success] For all 3 u8 bitwise affine maps inserted with push_back, pop_front rebalances and returns the opposite endpoint [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 16.385 s Cover: 2/2 reached

data_structure::sparse_set::verification

Harness	Harness assertions	Result
proof_fixed_set	[Success] After insertion or removal in the four-key domain, every sparse-set membership query agrees with the mathematical set [Success] After insertion or removal in the four-key domain, sparse-set iteration and length equal the mathematical set [Success] After insertion or removal in the four-key domain, sparse-set iteration contains valid keys without duplicates [Success] For every ordered set of keys 0 through 3, fixed SparseSet<u8> insertion reports whether the key was absent [Success] For every ordered set of keys 0 through 3, fixed SparseSet<u8> removal reports whether the key was present [Success] index out of bounds: the length is less than or equal to the given index	Success 41.002 s Cover: 2/2 reached
proof_growing_set	[Success] A growing SparseSet<u8> accepts every first key from 0 through 3 starting at zero capacity [Success] After every two-key insertion sequence on keys 0 through 3, growing sparse-set membership is exactly the inserted set [Success] After one insertion into a growing sparse set, holes and keys beyond the allocated index are absent [Success] For all two-key insertion sequences on keys 0 through 3, a growing sparse set suppresses duplicates and tracks the exact size [Success] Removing the first key after two insertions preserves exactly the distinct second key in a growing sparse set [Success] attempt to add with overflow	Success 14.036 s Cover: 3/3 reached

data_structure::trie::verification

Harness	Harness assertions	Result
proof_failure_binary_00_10	No harness assertions	Success 8.546 s Cover: 2/2 reached
proof_failure_binary_00_11	No harness assertions	Success 10.262 s Cover: 2/2 reached
proof_failure_binary_01_10	No harness assertions	Success 12.697 s Cover: 2/2 reached
proof_failure_binary_01_11	No harness assertions	Success 9.129 s Cover: 2/2 reached
proof_failure_composition_order	[Success] For the trie of 01 and 10 and every assignment of bool-to-bool functions, failure aggregation composes the node with its suffix ancestors in decreasing suffix-length order; this monoid is noncommutative [Success] index out of bounds: the length is less than or equal to the given index	Success 11.767 s Cover: 1/1 reached
proof_failure_root_alphabets	No harness assertions	Success 7.586 s
proof_failure_unary_chain	[Success] Every unary transition advances to the next depth or stays at the longest stored prefix [Success] For the unary trie of depths zero through four and arbitrary u8 labels, each aggregated label contains exactly all prefix labels through its depth, including the full chain of proper suffixes [Success] attempt to add with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 3.930 s

data_structure::vec_map::verification

Harness	Harness assertions	Result
proof_fixed_operations	[Success] Complete draining yields exactly the logical map and leaves every key vacant [Success] Constructing any map on keys 0 through 3 preserves its occupied and vacant slots [Success] Drain yields each occupied key once [Success] Insertion returns exactly the previous value [Success] Removal returns exactly the previous value [Success] The entry initializer runs exactly once for a vacant key and never for an occupied key [Success] With fixed storage, every insert, remove, entry insertion, or entry modification from any map on keys 0 through 3 preserves all u64 values [Success] index out of bounds: the length is less than or equal to the given index	Success 77.943 s Cover: 3/3 reached

math::bit_matrix::verification

Harness	Harness assertions	Result
proof_next_column	[Success] For every three-row 128-column bit matrix and every row suffix and column interval, pivot scanning returns the first column containing a one, or the interval end if none exists [Success] attempt to shift left with overflow [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 33.466 s Cover: 3/3 reached

math::floor_sum::verification

Harness	Harness assertions	Result
proof_floor_sum_u64_boundary	[Success] For every u64 length n and intercept b, floor_sum(n, 1, b, u64::MAX) counts exactly the terms reaching the modulus, even when n + b exceeds u64::MAX [Success] attempt to subtract with overflow	Success 1.685 s Cover: 2/2 reached

math::prime_factors::verification

Harness	Harness assertions	Result
proof_modular_subtraction	[Success] For every positive u64 modulus and pair of reduced residues, Montgomery subtraction returns their canonical modular difference, including borrowing at u64::MAX [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.312 s Cover: 3/3 reached

num::discrete_steps::verification

Harness	Harness assertions	Result
proof_i32_u64_steps	[Success] For all i32 endpoints, steps_between returns their nonnegative distance iff it fits u64 [Success] For every i32 value and u64 distance, backward_checked returns the exact difference iff representable [Success] For every i32 value and u64 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.687 s Cover: 3/3 reached
proof_i64_u32_steps	[Success] For all i64 endpoints, steps_between returns their nonnegative distance iff it fits u32 [Success] For every i64 value and u32 distance, backward_checked returns the exact difference iff representable [Success] For every i64 value and u32 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.533 s Cover: 3/3 reached
proof_i64_u64_steps	[Success] For all i64 endpoints, steps_between returns their nonnegative distance iff it fits u64 [Success] For every i64 value and u64 distance, backward_checked returns the exact difference iff representable [Success] For every i64 value and u64 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.952 s Cover: 3/3 reached
proof_inclusive_range	[Success] An i64 range whose inclusive endpoints cannot be represented contains no i64 value [Success] For all included, excluded or unbounded i64 endpoints, checked inclusive normalization preserves membership of every i64 value	Success 0.953 s Cover: 3/3 reached
proof_isize_u16_steps	[Success] For all isize endpoints, steps_between returns their nonnegative distance iff it fits u16 [Success] For every isize value and u16 distance, backward_checked returns the exact difference iff representable [Success] For every isize value and u16 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.816 s Cover: 3/3 reached
proof_isize_u32_steps	[Success] For all isize endpoints, steps_between returns their nonnegative distance iff it fits u32 [Success] For every isize value and u32 distance, backward_checked returns the exact difference iff representable [Success] For every isize value and u32 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.607 s Cover: 3/3 reached
proof_u32_u64_steps	[Success] For all u32 endpoints, steps_between returns their nonnegative distance iff it fits u64 [Success] For every u32 value and u64 distance, backward_checked returns the exact difference iff representable [Success] For every u32 value and u64 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.494 s Cover: 3/3 reached
proof_u64_u32_steps	[Success] For all u64 endpoints, steps_between returns their nonnegative distance iff it fits u32 [Success] For every u64 value and u32 distance, backward_checked returns the exact difference iff representable [Success] For every u64 value and u32 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.770 s Cover: 3/3 reached
proof_u64_u64_steps	[Success] For all u64 endpoints, steps_between returns their nonnegative distance iff it fits u64 [Success] For every u64 value and u64 distance, backward_checked returns the exact difference iff representable [Success] For every u64 value and u64 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.593 s Cover: 3/3 reached
proof_usize_u16_steps	[Success] For all usize endpoints, steps_between returns their nonnegative distance iff it fits u16 [Success] For every usize value and u16 distance, backward_checked returns the exact difference iff representable [Success] For every usize value and u16 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.585 s Cover: 3/3 reached
proof_usize_u32_steps	[Success] For all usize endpoints, steps_between returns their nonnegative distance iff it fits u32 [Success] For every usize value and u32 distance, backward_checked returns the exact difference iff representable [Success] For every usize value and u32 distance, forward_checked returns the exact sum iff representable [Success] attempt to add with overflow [Success] attempt to subtract with overflow	Success 0.767 s Cover: 3/3 reached

num::dyadic::verification

Harness	Harness assertions	Result
proof_i16_normalization	[Success] For every i16 numerator and u32 exponent, dyadic normalization divides out exactly the largest permitted power of two, preserving the value and reducing zero to 0/1 [Success] attempt to shift right with overflow [Success] attempt to subtract with overflow	Success 1.757 s Cover: 4/4 reached
proof_i32_normalization	[Success] For every i32 numerator and u32 exponent, dyadic normalization divides out exactly the largest permitted power of two, preserving the value and reducing zero to 0/1 [Success] attempt to shift right with overflow [Success] attempt to subtract with overflow	Success 15.910 s Cover: 4/4 reached
proof_i8_normalization	[Success] For every i8 numerator and u32 exponent, dyadic normalization divides out exactly the largest permitted power of two, preserving the value and reducing zero to 0/1 [Success] attempt to shift right with overflow [Success] attempt to subtract with overflow	Success 0.896 s Cover: 4/4 reached

num::integer::verification

Harness	Harness assertions	Result
proof_u128_mod_add_sub	[Success] For all reduced u128 operands and any nonzero modulus, mod_add returns the unique reduced sum, including machine overflow [Success] For all reduced u128 operands and any nonzero modulus, mod_sub returns the unique reduced difference, including machine underflow [Success] For every reduced u128 operand and any nonzero modulus, mod_neg returns its reduced additive inverse	Success 7.384 s Cover: 4/4 reached
proof_u16_mod_add_sub	[Success] For all reduced u16 operands and any nonzero modulus, mod_add returns the unique reduced sum, including machine overflow [Success] For all reduced u16 operands and any nonzero modulus, mod_sub returns the unique reduced difference, including machine underflow [Success] For every reduced u16 operand and any nonzero modulus, mod_neg returns its reduced additive inverse	Success 0.987 s Cover: 4/4 reached
proof_u32_mod_add_sub	[Success] For all reduced u32 operands and any nonzero modulus, mod_add returns the unique reduced sum, including machine overflow [Success] For all reduced u32 operands and any nonzero modulus, mod_sub returns the unique reduced difference, including machine underflow [Success] For every reduced u32 operand and any nonzero modulus, mod_neg returns its reduced additive inverse	Success 1.477 s Cover: 4/4 reached
proof_u64_mod_add_sub	[Success] For all reduced u64 operands and any nonzero modulus, mod_add returns the unique reduced sum, including machine overflow [Success] For all reduced u64 operands and any nonzero modulus, mod_sub returns the unique reduced difference, including machine underflow [Success] For every reduced u64 operand and any nonzero modulus, mod_neg returns its reduced additive inverse	Success 2.864 s Cover: 4/4 reached
proof_u8_mod_add_sub	[Success] For all reduced u8 operands and any nonzero modulus, mod_add returns the unique reduced sum, including machine overflow [Success] For all reduced u8 operands and any nonzero modulus, mod_sub returns the unique reduced difference, including machine underflow [Success] For every reduced u8 operand and any nonzero modulus, mod_neg returns its reduced additive inverse	Success 0.673 s Cover: 4/4 reached
proof_usize_mod_add_sub	[Success] For all reduced usize operands and any nonzero modulus, mod_add returns the unique reduced sum, including machine overflow [Success] For all reduced usize operands and any nonzero modulus, mod_sub returns the unique reduced difference, including machine underflow [Success] For every reduced usize operand and any nonzero modulus, mod_neg returns its reduced additive inverse	Success 2.940 s Cover: 4/4 reached

tools::fastio::verification

Harness	Harness assertions	Result
proof_i16_input	[Success] For every valid i16 decimal token of one through 5 digits, with any ASCII whitespace delimiter and initialized padding, the little-endian SWAR parser returns its value, including leading zeros and every byte alignment [Success] Parsing a i16 consumes exactly its optional minus sign, digits and one delimiter [Success] attempt to add with overflow [Success] attempt to multiply with overflow [Success] attempt to negate with overflow [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 6.838 s Cover: 3/3 reached
proof_i8_input	[Success] For every valid i8 decimal token of one through 3 digits, with any ASCII whitespace delimiter and initialized padding, the little-endian SWAR parser returns its value, including leading zeros and every byte alignment [Success] Parsing a i8 consumes exactly its optional minus sign, digits and one delimiter [Success] attempt to add with overflow [Success] attempt to multiply with overflow [Success] attempt to negate with overflow [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index	Success 3.190 s Cover: 3/3 reached
proof_u16_input	[Success] For every valid u16 decimal token of one through 5 digits, with any ASCII whitespace delimiter and initialized padding, the little-endian SWAR parser returns its value, including leading zeros and every byte alignment [Success] Parsing a u16 consumes exactly its optional minus sign, digits and one delimiter [Success] attempt to add with overflow [Success] attempt to multiply with overflow [Unreachable] attempt to negate with overflow [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index [Unreachable] index out of bounds: the length is less than or equal to the given index	Success 3.821 s Cover: 3/3 reached
proof_u8_input	[Success] For every valid u8 decimal token of one through 3 digits, with any ASCII whitespace delimiter and initialized padding, the little-endian SWAR parser returns its value, including leading zeros and every byte alignment [Success] Parsing a u8 consumes exactly its optional minus sign, digits and one delimiter [Success] attempt to add with overflow [Success] attempt to multiply with overflow [Unreachable] attempt to negate with overflow [Success] attempt to subtract with overflow [Success] index out of bounds: the length is less than or equal to the given index [Unreachable] index out of bounds: the length is less than or equal to the given index	Success 2.459 s Cover: 3/3 reached

Verus

PASS — 280 checks verified, 0 errors.

algorithm::cartesian_tree

Function	Properties checked	Result
CartesianTree::append_minimum	No labeled property; see source	PASS SMT: 10.862 ms
CartesianTree::clone	No labeled property; see source	PASS SMT: 0.076 ms
CartesianTree::new	For every input length and any PartialOrd comparison outcomes, CartesianTree::new creates reciprocal parent/child links; the root alone has the absent-parent marker and every child is on the correct side of its parent For every nonempty input length and any PartialOrd comparison outcomes, CartesianTree::new constructs valid subtree intervals: the root spans the full input and each node’s children split its interval around its own index For every nonempty input whose stable comparison model defines a total preorder on its values, every constructed Cartesian subtree is rooted at the leftmost minimum of its interval Under the same total-preorder assumption, every subtree interval is maximal for its leftmost minimum: a preceding boundary value is no greater than the root, and a following boundary value is strictly smaller than the root	PASS SMT: 6979.895 ms
CartesianTree::preserved_right_path	No labeled property; see source	PASS SMT: 53.957 ms
CartesianTree::spine_prefix	No labeled property; see source	PASS SMT: 22.903 ms
CartesianTree::subtree_ranges_unique	No labeled property; see source	PASS SMT: 23.932 ms
CartesianTree::unique_ranges	For every nonempty Cartesian tree with valid subtree intervals, its root and child links determine exactly one interval for every node; this uniqueness needs no assumptions about the input ordering	PASS SMT: 9.084 ms
CartesianTree::with_ranges	On normal return, with_ranges has invoked its callback exactly once per node with that node’s subtree interval, for every nonempty tree whose children split those intervals and whose callback precondition holds for every reported interval	PASS SMT: 1246.801 ms

algorithm::cartesian_tree::verification

Function	Properties checked	Result
constructed_ranges	For every nonempty input, the actual CartesianTree constructor establishes the subtree-interval precondition needed to traverse every node with with_ranges	PASS SMT: 4.277 ms
integer_minima	For every nonempty i64 input, the ordering precondition holds and the actual constructor produces maximal intervals for each node’s leftmost minimum, including repeated and extreme values	PASS SMT: 11.657 ms
key_minima	For arbitrary i64 keys with unconstrained payloads, constructing a Cartesian tree chooses the leftmost minimum key as the root and establishes the subtree-minimum guarantees without inspecting payloads	PASS SMT: 12.007 ms
singleton_ranges	The subtree-interval precondition is inhabited: a singleton Cartesian tree satisfies it and can be traversed with a callback whose precondition checks the reported interval	PASS SMT: 29.269 ms
validated_ranges	A callback that requires its node to lie in a nonempty subtree interval can be passed to with_ranges for every tree with valid subtree intervals	PASS SMT: 7.038 ms

algorithm::quotient_index

Function	Properties checked	Result
FloorQuotientIndex::contains_key	No labeled property; see source	PASS SMT: 8.873 ms
FloorQuotientIndex::contains_value	For every positive usize numerator and every usize value, contains_value recognizes exactly the values n/k for keys 1 through n, including usize::MAX	PASS SMT: 18.445 ms
FloorQuotientIndex::index_bounds	No labeled property; see source	PASS SMT: 19.787 ms
FloorQuotientIndex::index_order	No labeled property; see source	PASS SMT: 18.696 ms
FloorQuotientIndex::index_to_key	No labeled property; see source	PASS SMT: 6.211 ms
FloorQuotientIndex::index_to_key_unchecked	No labeled property; see source	PASS SMT: 62.323 ms
FloorQuotientIndex::index_to_value	No labeled property; see source	PASS SMT: 5.880 ms
FloorQuotientIndex::index_to_value_unchecked	No labeled property; see source	PASS SMT: 17.753 ms
FloorQuotientIndex::index_value_properties	No labeled property; see source	PASS SMT: 18.540 ms
FloorQuotientIndex::key_to_index	No labeled property; see source	PASS SMT: 5.649 ms
FloorQuotientIndex::key_to_index_unchecked	No labeled property; see source	PASS SMT: 30.019 ms
FloorQuotientIndex::key_to_value	No labeled property; see source	PASS SMT: 5.148 ms
FloorQuotientIndex::key_to_value_unchecked	No labeled property; see source	PASS SMT: 5.002 ms
FloorQuotientIndex::key_values	No labeled property; see source	PASS SMT: 38.674 ms
FloorQuotientIndex::len	No labeled property; see source	PASS SMT: 12.486 ms
FloorQuotientIndex::value_to_index	No labeled property; see source	PASS SMT: 3.891 ms
FloorQuotientIndex::value_to_index_unchecked	No labeled property; see source	PASS SMT: 13.351 ms
FloorQuotientIndex::value_to_key	No labeled property; see source	PASS SMT: 8.533 ms
FloorQuotientIndex::value_to_key_unchecked	For every present floor quotient below usize::MAX, value_to_key_unchecked returns a nonempty interval containing exactly all keys producing that quotient The maximum usize quotient occurs only for numerator usize::MAX and key 1	PASS SMT: 27.183 ms
FloorQuotientIndex::values	No labeled property; see source	PASS SMT: 23.487 ms

algorithm::quotient_index::verification

Function	Properties checked	Result
collect_quotients	Collecting key_values returns one nonempty exact key interval per quotient, in the same order and with the same length as values Collecting values for any valid floor quotient index returns exactly all distinct floor(n/k) values for 1 <= k <= n, in strictly increasing order	PASS SMT: 25.643 ms
floor_membership	A positive floor quotient is present exactly when its key interval contains an integer, with zero, out-of-range values and usize::MAX handled explicitly	PASS SMT: 6.646 ms
floor_reciprocal	No labeled property; see source	PASS SMT: 9.233 ms
floor_split	No labeled property; see source	PASS SMT: 56.199 ms
index_round_trip	For every positive usize numerator, its integer square root and every valid index, index-to-value and value-to-index round trip exactly, and index-to-key returns the same complete interval as value-to-key For every valid key, both checked and unchecked key-to-index produce the same index, and mapping that index to a value yields exactly the key’s floor quotient The indexed quotient values are strictly increasing, so no two valid indices represent the same floor quotient	PASS SMT: 31.439 ms
key_round_trip	For every positive usize numerator and valid key, the safe quotient APIs recognize the key and its quotient and return exactly the interval of keys producing that quotient, including the original key	PASS SMT: 3.080 ms
quotient_at_least	No labeled property; see source	PASS SMT: 19.447 ms
quotient_interval	For positive integers n, v and k, n/k equals v exactly when n/(v+1) < k <= n/v	PASS SMT: 43.306 ms
small_floor_quotient	No labeled property; see source	PASS SMT: 5.915 ms

data_structure::counter

Function	Properties checked	Result
BTreeCounter::clear	No labeled property; see source	PASS SMT: 3.720 ms
BTreeCounter::clone	No labeled property; see source	PASS SMT: 0.371 ms
BTreeCounter::default	No labeled property; see source	PASS SMT: 3.272 ms
BTreeCounter::get	No labeled property; see source	PASS SMT: 7.189 ms
BTreeCounter::is_empty	No labeled property; see source	PASS SMT: 3.896 ms
BTreeCounter::iter	No labeled property; see source	PASS SMT: 5.164 ms
BTreeCounter::keys	No labeled property; see source	PASS SMT: 4.655 ms
BTreeCounter::len	No labeled property; see source	PASS SMT: 4.146 ms
BTreeCounter::new	No labeled property; see source	PASS SMT: 0.422 ms
BTreeCounter::remove	No labeled property; see source	PASS SMT: 4.795 ms
BTreeCounter::remove_count	No labeled property; see source	PASS SMT: 11.320 ms
BTreeCounter::values	No labeled property; see source	PASS SMT: 6.214 ms

data_structure::counter::verification

Function	Properties checked	Result
removal_conserves_counts	BTreeCounter::remove_count saturates at the stored count, returns exactly the removed multiplicity, removes an exhausted key including a stored zero, and preserves all other keys; any two removals conserve initial = removed + remaining without an overflow precondition. The standard lawful key-order model is required. Insertion, range, Clone, Extend, and FromIterator are not verified	PASS SMT: 22.634 ms

data_structure::range_ap_add

Function	Properties checked	Result
RangeArithmeticProgressionAdd::build_inplace	For any length and i64 second differences whose first and second prefix sums fit i64, build_inplace produces exactly those double prefix sums	PASS SMT: 201.372 ms
RangeArithmeticProgressionAdd::clone	No labeled property; see source	PASS SMT: 0.097 ms
RangeArithmeticProgressionAdd::new	No labeled property; see source	PASS SMT: 8.417 ms
RangeArithmeticProgressionAdd::update	For any buffer length, update adds a + (i - l)d exactly at positions in [l, l + k), including empty and clipped intervals, provided indices, coefficient expressions, and intermediate i64 buffer additions fit	PASS SMT: 1126.643 ms
RangeArithmeticProgressionAdd::update_isize	For arbitrary buffer lengths and signed starts, update_isize clips an arithmetic progression at both array boundaries without changing its values, under the index and intermediate i64 arithmetic preconditions	PASS SMT: 64.438 ms
double_prefix_sum	No labeled property; see source	PASS SMT: 0.423 ms
double_prefix_sum_after_add	Adding delta at index j changes a double prefix sum ending at e by (e - j) times delta when j is before e, and otherwise leaves it unchanged	PASS SMT: 27.165 ms
double_prefix_sum_matches	When first prefix sums fit i64, summing their stored values agrees with the mathematical double prefix sum	PASS SMT: 11.738 ms
prefix_sum	No labeled property; see source	PASS SMT: 0.630 ms
prefix_sum_after_add	Adding a representable delta at one buffer index changes a prefix sum exactly when that index belongs to the prefix	PASS SMT: 11.168 ms

graph::grid

Function	Properties checked	Result
GridDirection::clone	No labeled property; see source	PASS SMT: 0.072 ms
GridDirection::dxdy	No labeled property; see source	PASS SMT: 1.652 ms
GridDirection::ndxdy	No labeled property; see source	PASS SMT: 3.912 ms
GridVertices::clone	No labeled property; see source	PASS SMT: 0.133 ms
GridVertices::next	No labeled property; see source	PASS SMT: 268.313 ms

graph::grid::verification

Function	Properties checked	Result
direction_components	All eight grid directions have the stated unit offsets, and ndxdy scales both components by every nonnegative distance representable as isize, including zero	PASS SMT: 18.327 ms
first_vertex	A grid with either dimension zero yields no vertices; every nonempty grid starts at coordinate (0, 0)	PASS SMT: 49.652 ms
row_major_coordinates	For arbitrary grid dimensions, the vertex iterator has exactly height times width elements in row-major order, and every valid coordinate occurs at its flattened index; the model does not require the cell count to fit usize	PASS SMT: 12.425 ms
row_major_index	Every position in the arbitrary-length row-major vertex sequence yields an in-range coordinate whose flattened index is that position, so the enumeration contains no extra or duplicate vertices	PASS SMT: 25.647 ms

math::gcd

Function	Properties checked	Result
coefficient_step	An extended-Euclidean step preserves opposite coefficient signs and the weighted absolute-value invariant, bounding both the product and updated coefficient by that invariant	PASS SMT: 179.867 ms
extgcd	For every i64 input pair excluding i64::MIN, iterative extended GCD terminates without integer overflow and returns a signed gcd with exact Bezout coefficients; its magnitude divides both inputs and the result is zero exactly for (0, 0)	PASS SMT: 347.651 ms
extgcd_recurse	For every i64 input pair excluding i64::MIN, recursive extended GCD terminates and satisfies the exact integer Bezout identity without overflowing its i64 coefficients, including negative inputs The absolute value of the nonzero returned gcd divides both inputs; together with the Bezout identity this characterizes their greatest common divisor	PASS SMT: 345.422 ms
factor_twos	For any nonzero u64 and any shift up to its trailing-zero count, right shift divides out exactly 2^shift and leaves a positive value	PASS SMT: 194.014 ms
gcd_loop	For all u64 inputs and every positive integer d, d divides the result exactly when d divides both inputs For all u64 inputs, Euclidean GCD returns zero exactly for (0, 0)	PASS SMT: 28.112 ms
halve_common	Halving the even member of an odd/even pair preserves every positive common divisor, including after a shared positive scaling	PASS SMT: 83.970 ms
modinv	For every 0 < a < m < 2^63 with coprime a and m, iterative modular inversion returns a multiplicative inverse in [0, m) without overflowing i64 intermediates	PASS SMT: 95.831 ms
modinv_extgcd_binary	For every odd modulus 1 < p < 2^63 and coprime input 0 < a < p, binary modular inversion terminates without overflow and returns the inverse in [0, p)	PASS SMT: 610.555 ms
modular_halving	For a positive odd modulus, adding it to an odd coefficient before halving preserves the modular representation of an even value and keeps the coefficient in [0, modulus], or [0, modulus) when it started there	PASS SMT: 86.545 ms
modular_subtraction	No labeled property; see source	PASS SMT: 30.576 ms
signed_coefficient_step	A signed extended-Euclidean step preserves the weighted absolute-value invariant and bounds the coefficient update by it for either sign of each non-minimum i64 operand	PASS SMT: 78.031 ms
signed_division	For signed i64 operands excluding i64::MIN and a nonzero divisor, Rust’s truncating quotient and remainder preserve a = q*b + r and have the unsigned quotient and remainder as their magnitudes	PASS SMT: 72.812 ms
strip_twos_common	Removing any number of trailing zero bits from the even member of an odd/even pair preserves common divisibility, including after a shared positive scaling	PASS SMT: 191.572 ms

math::gcd::verification

Function	Properties checked	Result
extended_gcd_matches_euclidean	For all nonnegative i64 inputs, recursive extended GCD and Euclidean GCD return the same greatest common divisor	PASS SMT: 46.291 ms
inverse_boundaries	For every modulus 2 <= m < 2^63, the inverse of 1 exists and is 1 For every modulus 2 <= m < 2^63, the inverse of m - 1 exists and is m - 1	PASS SMT: 21.224 ms

math::prime_factors

Function	Properties checked	Result
MontgomeryReduction64::new	For every odd u64 modulus, six Newton iterations with wrapping arithmetic compute its exact multiplicative inverse modulo 2^64	PASS SMT: 54.974 ms

math::prime_factors::verification

Function	Properties checked	Result
inverse_precision	The six Newton steps double inverse precision from 1 bit to 64 bits without requiring a modulus larger than 2^64	PASS SMT: 20.281 ms
inverse_refinement	A wrapping Newton step squares the inverse-error divisor whenever its square divides 2^64	PASS SMT: 1539.851 ms

string::knuth_morris_pratt

Function	Properties checked	Result
KnuthMorrisPratt::clone	No labeled property; see source	PASS SMT: 0.126 ms
KnuthMorrisPratt::new	For any pattern with lawful Eq and length below usize::MAX, each KMP table entry is the longest proper prefix matching the corresponding prefix’s suffix KMP preprocessing uses at most 3n Eq calls for a pattern of length n, excluding comparison internals and allocation	PASS SMT: 292.296 ms
extend_border	A prefix match extends by one exactly when the next pattern and text elements compare equal	PASS SMT: 12.011 ms
nested_borders	Inside a matched suffix of length j, a shorter length k matches exactly when it is a border of the pattern prefix of length j	PASS SMT: 6.857 ms

string::suffix_array

Function	Properties checked	Result
SuffixArray::clone	No labeled property; see source	PASS SMT: 0.096 ms
SuffixArray::index	No labeled property; see source	PASS SMT: 5.250 ms
SuffixArray::into_inner	No labeled property; see source	PASS SMT: 4.726 ms
SuffixArray::lcp_array	No labeled property; see source	PASS SMT: 7.712 ms
SuffixArray::lcp_array_with_rank	Given a permutation of all suffix starts sorted lexicographically under keys consistent with text equality, LCP construction returns the exact longest common prefix of every adjacent suffix pair and the exact inverse rank permutation, for arbitrary text lengths including zero LCP construction makes at most 2n equality comparisons for text length n; the bound excludes the internal cost of equality and allocation, and termination assumes these called operations terminate	PASS SMT: 376.582 ms

string::suffix_array::verification

Function	Properties checked	Result
constant_order	No labeled property; see source	PASS SMT: 6.189 ms
constant_text	For every constant byte string, including the empty string, a concrete descending suffix permutation satisfies the LCP precondition and the actual LCP method returns [0, 1, …, n - 1] with inverse ranks n - position	PASS SMT: 144.531 ms
empty_suffix_first	No labeled property; see source	PASS SMT: 8.425 ms
lex_asymmetric	No labeled property; see source	PASS SMT: 5.576 ms
lex_less	No labeled property; see source	PASS SMT: 4.538 ms
matched_symmetric	No labeled property; see source	PASS SMT: 4.149 ms
prefix_interval	No labeled property; see source	PASS SMT: 14.917 ms
shift_lower_bound	No labeled property; see source	PASS SMT: 53.261 ms

string::z_algorithm

Function	Properties checked	Result
Zarray::clone	No labeled property; see source	PASS SMT: 0.114 ms
Zarray::index	No labeled property; see source	PASS SMT: 5.899 ms
Zarray::new	At most 2n - 2 Eq calls for any nonempty input of length n For any nonempty input s with lawful Eq, z[i] is the longest common prefix length of s and s[i..] The Z-array has the same length as the input	PASS SMT: 117.481 ms
carry_match	Shifting an overlapping prefix match by k preserves n - k matching elements	PASS SMT: 7.822 ms
copy_match	The known Z-box also matches at the copied prefix’s mismatch boundary The m matching prefix elements transfer to the shifted position i + k	PASS SMT: 11.360 ms

string::z_algorithm::verification

Function	Properties checked	Result
Classified::eq	No labeled property; see source	PASS SMT: 4.260 ms
bytes	Zarray::new is called with a lawful, stable Eq matching its specification Zarray::new is called with nonempty input	PASS SMT: 5.451 ms
classified	Class-based equality satisfies the Eq specification and equivalence laws Zarray::new is called with a lawful, stable Eq matching its specification Zarray::new is called with nonempty input	PASS SMT: 3.709 ms
distinct_payloads	The two example values are structurally distinct The two example values compare equal via Eq despite different payloads	PASS SMT: 2.564 ms
indexed_bytes	For every nonempty byte sequence and every valid index, constructing and indexing a Z-array returns the exact longest common prefix with that suffix Zarray::new is called with a lawful, stable Eq matching its specification Zarray::new is called with nonempty input	PASS SMT: 6.540 ms

tools::coding

Function	Properties checked	Result
BitReader::new	No labeled property; see source	PASS SMT: 8.720 ms
BitReader::read_bit	No labeled property; see source	PASS SMT: 65.286 ms
BitReader::read_u8	No labeled property; see source	PASS SMT: 58.482 ms
BitWriter::default	No labeled property; see source	PASS SMT: 6.794 ms
BitWriter::into_inner	No labeled property; see source	PASS SMT: 21.325 ms
BitWriter::push_bit	No labeled property; see source	PASS SMT: 54.319 ms
BitWriter::push_u64	No labeled property; see source	PASS SMT: 296.550 ms
BitWriter::push_u8	No labeled property; see source	PASS SMT: 77.858 ms
byte_append	No labeled property; see source	PASS SMT: 37.205 ms
byte_join	No labeled property; see source	PASS SMT: 18.966 ms
byte_set	No labeled property; see source	PASS SMT: 16.818 ms
decode_head	No labeled property; see source	PASS SMT: 8.070 ms
equal_bytes	No labeled property; see source	PASS SMT: 14.296 ms
unescape	For arbitrary byte strings, unescape decodes backslash n/r/t/backslash/0/quote, removes the backslash before any other byte, drops a final unmatched backslash, and never lengthens the input	PASS SMT: 108.811 ms
unescaped	No labeled property; see source	PASS SMT: 6.755 ms
word_byte	No labeled property; see source	PASS SMT: 20.966 ms
word_prefix	No labeled property; see source	PASS SMT: 180.205 ms
zero_byte	No labeled property; see source	PASS SMT: 7.692 ms

tools::coding::verification

Function	Properties checked	Result
bit_roundtrip	Finishing a bit stream uses the minimum whole-byte length and pads only the final byte with fewer than eight zero bits For every finite bit slice, writing its bits and reading them back returns each original bit in order, including byte boundaries and empty input	PASS SMT: 114.395 ms
mixed_roundtrip	After every arbitrary-length bit prefix, an appended byte is recovered exactly by the unaligned byte reader without changing the preceding bits For every u64 value fitting a requested width from zero through 64 bits, push_u64 appends exactly that most-significant-first bit sequence after arbitrary preceding bits and a byte	PASS SMT: 643.454 ms

tools::ord_tools

Function	Properties checked	Result
impl&%0::T::chmax	No labeled property; see source	PASS SMT: 0.936 ms
impl&%0::T::chmin	No labeled property; see source	PASS SMT: 1.086 ms
impl&%0::T::minmax	No labeled property; see source	PASS SMT: 0.997 ms

tools::ord_tools::verification

Function	Properties checked	Result
extrema	Folding the actual chmin and chmax methods over every nonempty i64 slice, followed by minmax, returns attained global extrema that bound every input element; duplicate values and the full signed range are included	PASS SMT: 60.191 ms
unordered_or_equal	For any type obeying its partial-comparison model, chmin and chmax retain the original value when the comparison is equal or incomparable, while minmax reverses the pair in those cases; the helpers do not assume all pairs are comparable	PASS SMT: 3.158 ms

tools::partial_ignored_ord

Function	Properties checked	Result
PartialIgnoredOrd::clone	No labeled property; see source	PASS SMT: 0.112 ms
PartialIgnoredOrd::cmp	No labeled property; see source	PASS SMT: 1.603 ms
PartialIgnoredOrd::eq	No labeled property; see source	PASS SMT: 2.047 ms
PartialIgnoredOrd::partial_cmp	No labeled property; see source	PASS SMT: 1.668 ms

tools::partial_ignored_ord::verification

Function	Properties checked	Result
payload_is_ignored	PartialIgnoredOrd equality and both ordering operations depend only on the key, for arbitrary payload types and values, without requiring the payload to implement any comparison trait	PASS SMT: 4.387 ms

tools::xorshift

Function	Properties checked	Result
Xorshift::clone	No labeled property; see source	PASS SMT: 0.096 ms
Xorshift::default	No labeled property; see source	PASS SMT: 0.220 ms
Xorshift::new_with_seed	No labeled property; see source	PASS SMT: 0.884 ms
Xorshift::rand	No labeled property; see source	PASS SMT: 1.555 ms
Xorshift::rand64	No labeled property; see source	PASS SMT: 39.610 ms