diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 56a3a7357c7cf..eb1b18ba911e6 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -10,6 +10,8 @@ on: - 'library/**' - '.github/workflows/kani.yml' - 'scripts/run-kani.sh' + - 'scripts/kani-std-analysis/flt2dec_harnesses.py' + - 'scripts/kani-std-analysis/test_flt2dec_harnesses.py' defaults: run: @@ -35,10 +37,10 @@ jobs: WORKER_INDEX: ${{ matrix.partition }} # Total number of workers running this step WORKER_TOTAL: 4 - # Cap parallel harness verification on ubuntu-latest: its 4-core/16 GB - # runners get OOM-killed when 4 memory-hungry harnesses (up to ~10 GB - # each, e.g. the ffi::c_str ones) run concurrently. - KANI_JOBS: ${{ matrix.os == 'ubuntu-latest' && 2 || '' }} + # The same catalog assigns every excluded proof to a dedicated job on each OS. + KANI_SEPARATE_FLT2DEC: "true" + # Run one verifier per runner to bound proof concurrency. + KANI_JOBS: 1 steps: - name: Remove unnecessary software to free up disk space @@ -61,10 +63,87 @@ jobs: if: matrix.os == 'ubuntu-latest' run: sudo apt-get install -y jq - # Step 3: Run Kani on the std library (default configuration) + - name: Trust CBMC Homebrew tap + if: runner.os == 'macOS' + run: brew trust --tap diffblue/cbmc + + # Step 3: Run Kani on the std library - name: Run Kani Verification - run: head/scripts/run-kani.sh --path ${{github.workspace}}/head + run: | + # Run one proof at a time on each runner. + export KANI_JOBS=1 + export RAYON_NUM_THREADS=1 + head/scripts/run-kani.sh --path ${{github.workspace}}/head \ + --kani-args --harness-timeout 30m --fail-fast + flt2dec_matrix: + name: Prepare flt2dec proof groups + runs-on: ubuntu-latest + outputs: + matrix: ${{ steps.groups.outputs.matrix }} + steps: + - uses: actions/checkout@v4 + - name: Check proof routing + run: python3 -I -m unittest discover -s scripts/kani-std-analysis -p test_flt2dec_harnesses.py + - name: Build proof matrix + id: groups + run: | + flt2dec_matrix=$(python3 -I scripts/kani-std-analysis/flt2dec_harnesses.py --matrix) + printf 'matrix=%s\n' "$flt2dec_matrix" >> "$GITHUB_OUTPUT" + + check-flt2dec: + name: Verify flt2dec (${{ matrix.group.name }}, ${{ matrix.os }}) + needs: flt2dec_matrix + runs-on: ${{ matrix.os }} + strategy: + fail-fast: false + matrix: ${{ fromJSON(needs.flt2dec_matrix.outputs.matrix) }} + env: + KANI_JOBS: 1 + RAYON_NUM_THREADS: 1 + KANI_HARNESS_TIMEOUT: ${{ matrix.group.timeout_minutes }}m + KANI_OBJECT_BITS: ${{ (matrix.group.kind == 'contract' || matrix.group.kind == 'equivalence') && '12' || '14' }} + # Keep encoding experiments scoped to the diagnostic probes. + KANI_SYMEX_CACHE_DEREFERENCES: ${{ matrix.group.kind == 'probe' && 'true' || 'false' }} + # Dragon's fixed limb indices can use the default array field splitting. + KANI_ARRAY_FIELD_SENSITIVITY: ${{ matrix.group.kind == 'probe' && startsWith(matrix.group.name, 'grisu-') && 'false' || 'true' }} + HARNESS_GROUP: ${{ matrix.group.name }} + HARNESS_KIND: ${{ matrix.group.kind }} + steps: + - name: Remove unnecessary software to free up disk space + if: matrix.os == 'ubuntu-latest' + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup + + - name: Checkout Repository + uses: actions/checkout@v4 + with: + path: head + submodules: true + + - name: Trust CBMC Homebrew tap + if: runner.os == 'macOS' + run: brew trust --tap diffblue/cbmc + + - name: Verify selected proof groups + run: | + # Keep every group within four hours of proof budgets per job: + # two 120-minute or four 60-minute generators, or eight 30-minute cases. + harness_names=$(python3 -I head/scripts/kani-std-analysis/flt2dec_harnesses.py --group "$HARNESS_GROUP") + harness_args=() + while IFS= read -r harness; do + [[ -n "$harness" ]] || exit 1 + harness_args+=(--harness "$harness") + done <<< "$harness_names" + output_format=terse + if [[ "$HARNESS_KIND" == contract || "$HARNESS_KIND" == equivalence || "$HARNESS_KIND" == probe ]]; then + output_format=regular + fi + printf 'Selected %s harnesses\n' "$(( ${#harness_args[@]} / 2 ))" + head/scripts/run-kani.sh --path "${GITHUB_WORKSPACE}/head" \ + --kani-args --jobs 1 --harness-timeout "$KANI_HARNESS_TIMEOUT" --fail-fast --output-format="$output_format" \ + --exact "${harness_args[@]}" + kani_autoharness: name: Verify std library using autoharness runs-on: ${{ matrix.os }} @@ -93,6 +172,10 @@ jobs: with: submodules: true + - name: Trust CBMC Homebrew tap + if: runner.os == 'macOS' + run: brew trust --tap diffblue/cbmc + # Step 2: Run Kani autoharness on the std library for selected functions. # Uses "--include-pattern" to make sure we do not try to run across all # possible functions as that may take a lot longer than expected. Instead, @@ -103,6 +186,8 @@ jobs: # core_arch::x86:: functions that are known to verify successfully. - name: Run Kani Verification run: | + python3 -I -B -m unittest discover \ + -s scripts/kani-std-analysis -p test_log_parser.py scripts/run-kani.sh --run autoharness --kani-args \ --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \ --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::unchecked_disjoint_bitor" \ @@ -207,9 +292,9 @@ jobs: --exclude-pattern time::Duration::from_secs_f \ --include-pattern unicode::unicode_data::conversions::to_ \ --exclude-pattern ::precondition_check \ - --harness-timeout 10m \ + --harness-timeout 30m --fail-fast \ --default-unwind 1000 \ - --jobs=3 --output-format=terse | tee autoharness-verification.log + --jobs=1 --output-format=terse | tee autoharness-verification.log gzip autoharness-verification.log - name: Upload Autoharness Verification Log @@ -255,6 +340,10 @@ jobs: with: python-version: '3.x' + - name: Trust CBMC Homebrew tap + if: runner.os == 'macOS' + run: brew trust --tap diffblue/cbmc + # Step 2: Run list on the std library - name: Run Kani Metrics run: | diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 57864d80376c4..67558f6e413c5 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -75,6 +75,8 @@ #![no_core] #![rustc_coherence_is_core] #![rustc_preserve_ub_checks] +// Composed Kani stubs require more macro expansion depth. +#![cfg_attr(kani, recursion_limit = "256")] // // Lints: #![deny(rust_2021_incompatible_or_patterns)] diff --git a/library/core/src/num/bignum.rs b/library/core/src/num/bignum.rs index 95b49a38ded06..2b4b2a172984e 100644 --- a/library/core/src/num/bignum.rs +++ b/library/core/src/num/bignum.rs @@ -146,6 +146,10 @@ macro_rules! define_bignum { use crate::{cmp, iter}; let mut sz = cmp::max(self.size, other.size); + #[cfg(kani)] + { + sz = crate::num::bignum::kani_loop_size(sz); + } let mut carry = false; for (a, b) in iter::zip(&mut self.base[..sz], &other.base[..sz]) { let (v, c) = (*a).carrying_add(*b, carry); @@ -181,6 +185,8 @@ macro_rules! define_bignum { use crate::{cmp, iter}; let sz = cmp::max(self.size, other.size); + #[cfg(kani)] + let sz = crate::num::bignum::kani_loop_size(sz); let mut noborrow = true; for (a, b) in iter::zip(&mut self.base[..sz], &other.base[..sz]) { let (v, c) = (*a).carrying_add(!*b, noborrow); @@ -196,6 +202,10 @@ macro_rules! define_bignum { /// mutable reference. pub fn mul_small(&mut self, other: $ty) -> &mut $name { let mut sz = self.size; + #[cfg(kani)] + { + sz = crate::num::bignum::kani_loop_size(sz); + } let mut carry = 0; for a in &mut self.base[..sz] { let (v, c) = (*a).carrying_mul(other, carry); @@ -387,6 +397,218 @@ pub type Digit32 = u32; define_bignum!(Big32x40: type=Digit32, n=40); +// Proofs can expose fixed count bits while asserting equality with this identity. +// The arithmetic loops still run, and normal builds contain no instrumentation. +#[cfg(kani)] +pub(crate) fn kani_loop_size(size: usize) -> usize { + size +} + +#[cfg(kani)] +impl crate::kani::Arbitrary for Big32x40 { + fn any() -> Self { + Self { size: crate::kani::any(), base: crate::kani::any() } + } +} + +#[cfg(kani)] +impl Big32x40 { + pub(crate) fn kani_with_arbitrary_limbs(size: usize) -> Self { + Self { size, base: crate::kani::any() } + } + + pub(crate) fn kani_size(&self) -> usize { + self.size + } + + pub(crate) fn kani_limbs_mut(&mut self) -> &mut [u32; 40] { + &mut self.base + } + + pub(crate) fn kani_valid_storage(&self) -> bool { + // Constant indices avoid unfolding a symbolic slice iterator in every + // contract invocation. Eager Boolean operations preserve the predicate. + macro_rules! inactive_limbs_are_zero { + ($($index:literal),+ $(,)?) => { + true $(& ((self.size > $index) | (self.base[$index] == 0)))+ + }; + } + + self.size <= self.base.len() + && inactive_limbs_are_zero!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, + 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + ) + } + + // The equivalence proof in dragon_verify checks these constant-index + // models for every in-bounds storage size and arbitrary limb contents. + pub(crate) fn kani_cmp_model(&self, other: &Self) -> crate::cmp::Ordering { + use crate::cmp::Ordering::{Equal, Greater, Less}; + + assert!(self.size <= self.base.len() && other.size <= other.base.len()); + + macro_rules! compare_limbs { + ($($index:literal),+ $(,)?) => {{ + let less = false; + let greater = false; + $( + let active = (self.size > $index) | (other.size > $index); + let equal = self.base[$index] == other.base[$index]; + let preserve = !active | equal; + let less = (active & (self.base[$index] < other.base[$index])) + | (preserve & less); + let greater = (active & (self.base[$index] > other.base[$index])) + | (preserve & greater); + )+ + if less { Less } else if greater { Greater } else { Equal } + }}; + } + + // Like Ord::cmp, inspect both arrays through the larger active size. + // A differing higher limb supersedes every lower limb's ordering. + // Eager Boolean operations avoid a branch at each constant limb index. + compare_limbs!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, + 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + ) + } + + pub(crate) fn kani_is_zero_model(&self) -> bool { + assert!(self.size <= self.base.len()); + + macro_rules! limbs_are_zero { + ($($index:literal),+ $(,)?) => { + true $(& ((self.size <= $index) | (self.base[$index] == 0)))+ + }; + } + + limbs_are_zero!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, + 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + ) + } + + pub(crate) fn kani_same_storage(&self, other: &Self) -> bool { + macro_rules! equal_limbs { + ($($index:literal),+ $(,)?) => { + true $(& (self.base[$index] == other.base[$index]))+ + }; + } + + (self.size == other.size) + & equal_limbs!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, + 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + ) + } + + // Independent equivalence proofs compare every stored limb and the size. + // Addition and multiplication reserve one limb for a possible carry. + // Their size bounds are asserted here, including at generator call sites. + pub(crate) fn kani_add_model<'a>(&'a mut self, other: &Self) -> &'a mut Self { + assert!(self.size < self.base.len() && other.size < other.base.len()); + let mut sz = kani_loop_size(crate::cmp::max(self.size, other.size)); + + macro_rules! add_limbs { + ($($index:literal),+ $(,)?) => {{ + let carry = false; + $( + let carry = if $index < sz { + let (value, next) = self.base[$index].carrying_add(other.base[$index], carry); + self.base[$index] = value; + next + } else { + carry + }; + )+ + carry + }}; + } + + let carry = add_limbs!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, + 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + ); + if carry { + self.base[sz] = 1; + sz += 1; + } + self.size = sz; + self + } + + pub(crate) fn kani_sub_model<'a>(&'a mut self, other: &Self) -> &'a mut Self { + assert!(self.size <= self.base.len() && other.size <= other.base.len()); + assert!(self.kani_cmp_model(other) != crate::cmp::Ordering::Less); + let sz = kani_loop_size(crate::cmp::max(self.size, other.size)); + + macro_rules! subtract_limbs { + ($($index:literal),+ $(,)?) => {{ + let noborrow = true; + $( + let noborrow = if $index < sz { + let (value, next) = self.base[$index].carrying_add(!other.base[$index], noborrow); + self.base[$index] = value; + next + } else { + noborrow + }; + )+ + noborrow + }}; + } + + let noborrow = subtract_limbs!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, + 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + ); + assert!(noborrow); + self.size = sz; + self + } + + pub(crate) fn kani_mul_small_model(&mut self, other: u32) -> &mut Self { + assert!(self.size < self.base.len()); + let mut sz = kani_loop_size(self.size); + + macro_rules! multiply_limbs { + ($($index:literal),+ $(,)?) => {{ + let carry = 0; + $( + let carry = if $index < sz { + let (value, next) = self.base[$index].carrying_mul(other, carry); + self.base[$index] = value; + next + } else { + carry + }; + )+ + carry + }}; + } + + let carry = multiply_limbs!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, + 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + ); + if carry > 0 { + self.base[sz] = carry; + sz += 1; + } + self.size = sz; + self + } + + // Contract proofs include every storage size, including the empty zero + // representation. Leading zero limbs within the active prefix are valid. + pub(crate) fn kani_any_valid() -> Self { + let value: Self = crate::kani::any(); + crate::kani::assume(value.kani_valid_storage()); + value + } +} + // this one is used for testing only. #[doc(hidden)] pub mod tests { diff --git a/library/core/src/num/flt2dec/bit_scan_verify.rs b/library/core/src/num/flt2dec/bit_scan_verify.rs new file mode 100644 index 0000000000000..8a30043e6afe7 --- /dev/null +++ b/library/core/src/num/flt2dec/bit_scan_verify.rs @@ -0,0 +1,46 @@ +//! Exact bit-scan models for the flt2dec generator proofs. + +use crate::kani; + +// Expose fixed shifts to symbolic execution before expanding normalization and +// scaling. The independent proof below checks every input, including zero. +pub(crate) fn leading_zeros_u64(mut value: u64) -> u32 { + if value == 0 { + 64 + } else { + let mut count = 0; + macro_rules! scan_half { + ($bits:literal) => { + if value >> (64 - $bits) == 0 { + count += $bits; + value <<= $bits; + } + }; + } + scan_half!(32); + scan_half!(16); + scan_half!(8); + scan_half!(4); + scan_half!(2); + count + u32::from(value >> 63 == 0) + } +} + +pub(crate) fn leading_zeros_u32(value: u32) -> u32 { + leading_zeros_u64(u64::from(value)) - 32 +} + +#[kani::proof] +#[kani::solver(kissat)] +fn check_leading_zeros_models_agree() { + let wide: u64 = kani::any(); + let narrow: u32 = kani::any(); + assert!(leading_zeros_u64(wide) == wide.leading_zeros()); + assert!(leading_zeros_u32(narrow) == narrow.leading_zeros()); + kani::cover(wide == 0, "u64 zero has 64 leading zeros"); + kani::cover(wide == 1, "u64 one has 63 leading zeros"); + kani::cover(wide == 1 << 63, "u64 top bit has no leading zeros"); + kani::cover(narrow == 0, "u32 zero has 32 leading zeros"); + kani::cover(narrow == 1, "u32 one has 31 leading zeros"); + kani::cover(narrow == 1 << 31, "u32 top bit has no leading zeros"); +} diff --git a/library/core/src/num/flt2dec/estimator_verify.rs b/library/core/src/num/flt2dec/estimator_verify.rs new file mode 100644 index 0000000000000..e3d75c2f8d95a --- /dev/null +++ b/library/core/src/num/flt2dec/estimator_verify.rs @@ -0,0 +1,143 @@ +//! An exact exponent-estimator model with a separate equivalence proof. + +use crate::kani; + +fn scale_from_bits(bits: i64, exp: i16) -> i16 { + (((bits + exp as i64) * 1292913986) >> 32) as i16 +} + +// Compute the original formula in each leaf, before merging the branches. +// When the binary exponent is fixed, equal decimal exponents can then fold +// together without expanding unreachable bigint scaling paths. +pub(crate) fn estimate_scaling_factor(mant: u64, exp: i16) -> i16 { + assert!(mant > 0); + + macro_rules! choose_bits { + ($base:expr;) => { + scale_from_bits($base, exp) + }; + ($base:expr; $half:literal $(, $rest:literal)*) => { + if mant <= (1_u64 << ($base + $half - 1)) { + choose_bits!($base; $($rest),*) + } else { + choose_bits!($base + $half; $($rest),*) + } + }; + } + + // The remaining tree has exactly the 64 leaves for bit counts 0..=63. + // Every shift in it is at most 62, and mant == 1 selects bit count zero. + if mant > (1_u64 << 63) { + scale_from_bits(64, exp) + } else { + choose_bits!(0; 32, 16, 8, 4, 2, 1) + } +} + +// Partition mant - 1 by bit length. Zero gives mant == 1; bit lengths 1..=64 +// cover every other nonzero u64 mantissa. Only the predecessor u64::MAX is +// excluded, since adding one would produce the out-of-domain mantissa zero. +fn check_estimator_model_agrees() { + assert!(BITS <= 64); + let mant = if BITS == 0 { + 1 + } else { + let leading = 1_u64 << (BITS - 1); + let predecessor = leading | (kani::any::() & (leading - 1)); + kani::assume(predecessor < u64::MAX); + predecessor + 1 + }; + let exp: i16 = kani::any(); + + assert_eq!( + estimate_scaling_factor(mant, exp), + super::estimator::estimate_scaling_factor(mant, exp) + ); + if BITS == 0 { + kani::cover(mant == 1, "smallest nonzero mantissa"); + } + if BITS == 63 { + kani::cover(mant == (1_u64 << 63), "largest power-of-two boundary"); + } + if BITS == 64 { + kani::cover(mant == u64::MAX, "largest mantissa"); + } + kani::cover(exp == i16::MIN, "smallest binary exponent"); + kani::cover(exp == i16::MAX, "largest binary exponent"); +} + +macro_rules! check_bit_count { + ($name:ident, $bits:literal) => { + #[kani::proof] + #[kani::solver(kissat)] + fn $name() { + check_estimator_model_agrees::<$bits>(); + } + }; +} + +check_bit_count!(check_estimator_model_agrees_00, 0); +check_bit_count!(check_estimator_model_agrees_01, 1); +check_bit_count!(check_estimator_model_agrees_02, 2); +check_bit_count!(check_estimator_model_agrees_03, 3); +check_bit_count!(check_estimator_model_agrees_04, 4); +check_bit_count!(check_estimator_model_agrees_05, 5); +check_bit_count!(check_estimator_model_agrees_06, 6); +check_bit_count!(check_estimator_model_agrees_07, 7); +check_bit_count!(check_estimator_model_agrees_08, 8); +check_bit_count!(check_estimator_model_agrees_09, 9); +check_bit_count!(check_estimator_model_agrees_10, 10); +check_bit_count!(check_estimator_model_agrees_11, 11); +check_bit_count!(check_estimator_model_agrees_12, 12); +check_bit_count!(check_estimator_model_agrees_13, 13); +check_bit_count!(check_estimator_model_agrees_14, 14); +check_bit_count!(check_estimator_model_agrees_15, 15); +check_bit_count!(check_estimator_model_agrees_16, 16); +check_bit_count!(check_estimator_model_agrees_17, 17); +check_bit_count!(check_estimator_model_agrees_18, 18); +check_bit_count!(check_estimator_model_agrees_19, 19); +check_bit_count!(check_estimator_model_agrees_20, 20); +check_bit_count!(check_estimator_model_agrees_21, 21); +check_bit_count!(check_estimator_model_agrees_22, 22); +check_bit_count!(check_estimator_model_agrees_23, 23); +check_bit_count!(check_estimator_model_agrees_24, 24); +check_bit_count!(check_estimator_model_agrees_25, 25); +check_bit_count!(check_estimator_model_agrees_26, 26); +check_bit_count!(check_estimator_model_agrees_27, 27); +check_bit_count!(check_estimator_model_agrees_28, 28); +check_bit_count!(check_estimator_model_agrees_29, 29); +check_bit_count!(check_estimator_model_agrees_30, 30); +check_bit_count!(check_estimator_model_agrees_31, 31); +check_bit_count!(check_estimator_model_agrees_32, 32); +check_bit_count!(check_estimator_model_agrees_33, 33); +check_bit_count!(check_estimator_model_agrees_34, 34); +check_bit_count!(check_estimator_model_agrees_35, 35); +check_bit_count!(check_estimator_model_agrees_36, 36); +check_bit_count!(check_estimator_model_agrees_37, 37); +check_bit_count!(check_estimator_model_agrees_38, 38); +check_bit_count!(check_estimator_model_agrees_39, 39); +check_bit_count!(check_estimator_model_agrees_40, 40); +check_bit_count!(check_estimator_model_agrees_41, 41); +check_bit_count!(check_estimator_model_agrees_42, 42); +check_bit_count!(check_estimator_model_agrees_43, 43); +check_bit_count!(check_estimator_model_agrees_44, 44); +check_bit_count!(check_estimator_model_agrees_45, 45); +check_bit_count!(check_estimator_model_agrees_46, 46); +check_bit_count!(check_estimator_model_agrees_47, 47); +check_bit_count!(check_estimator_model_agrees_48, 48); +check_bit_count!(check_estimator_model_agrees_49, 49); +check_bit_count!(check_estimator_model_agrees_50, 50); +check_bit_count!(check_estimator_model_agrees_51, 51); +check_bit_count!(check_estimator_model_agrees_52, 52); +check_bit_count!(check_estimator_model_agrees_53, 53); +check_bit_count!(check_estimator_model_agrees_54, 54); +check_bit_count!(check_estimator_model_agrees_55, 55); +check_bit_count!(check_estimator_model_agrees_56, 56); +check_bit_count!(check_estimator_model_agrees_57, 57); +check_bit_count!(check_estimator_model_agrees_58, 58); +check_bit_count!(check_estimator_model_agrees_59, 59); +check_bit_count!(check_estimator_model_agrees_60, 60); +check_bit_count!(check_estimator_model_agrees_61, 61); +check_bit_count!(check_estimator_model_agrees_62, 62); +check_bit_count!(check_estimator_model_agrees_63, 63); +check_bit_count!(check_estimator_model_agrees_64, 64); diff --git a/library/core/src/num/flt2dec/mod.rs b/library/core/src/num/flt2dec/mod.rs index e79a00a865969..b8a25b6386249 100644 --- a/library/core/src/num/flt2dec/mod.rs +++ b/library/core/src/num/flt2dec/mod.rs @@ -666,3 +666,286 @@ where } } } + +#[cfg(kani)] +mod bit_scan_verify; +#[cfg(kani)] +mod estimator_verify; +#[cfg(kani)] +mod rounding_verify; + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod flt2dec_verify { + use super::*; + use crate::kani; + + // Use the real decoder so the exponent, rounding interval, and tie-breaking + // flag stay related. Choosing these fields independently admits values that + // neither primitive float type can produce. The sign does not affect Decoded. + pub(crate) fn arbitrary_finite_f32() -> Decoded { + assert!(GROUP < 4); + let bits = (GROUP << 29) | (kani::any::() & 0x1fff_ffff); + kani::assume(bits > 0 && bits < 0x7f80_0000); + finite_decoded(decode(f32::from_bits(bits)).1) + } + + pub(crate) fn arbitrary_finite_f64() -> Decoded { + assert!(GROUP < 32); + let bits = (GROUP << 58) | (kani::any::() & 0x03ff_ffff_ffff_ffff); + kani::assume(bits > 0 && bits < 0x7ff0_0000_0000_0000); + finite_decoded(decode(f64::from_bits(bits)).1) + } + + // Additional CI probes test whether fixing the exponent makes the real + // arithmetic tractable. Every significand bit remains symbolic, and the + // exhaustive groups below remain part of the required verification. + pub(crate) fn arbitrary_finite_f64_exponent() -> Decoded { + assert!(EXPONENT < 0x7ff); + let bits = (EXPONENT << 52) | (kani::any::() & 0x000f_ffff_ffff_ffff); + kani::assume(bits > 0); + finite_decoded(decode(f64::from_bits(bits)).1) + } + + // Additional diagnostics can span several exponents without fixing any + // significand bits. The complete finite partitions remain required above. + pub(crate) fn arbitrary_finite_f64_range() -> Decoded { + assert!(FIRST > 0 && FIRST < END && END <= 0x7ff0_0000_0000_0000); + let bits: u64 = kani::any(); + kani::assume(bits >= FIRST && bits < END); + kani::cover(bits == FIRST, "cached-power probe includes its first input"); + kani::cover(bits == END - 1, "cached-power probe includes its last input"); + finite_decoded(decode(f64::from_bits(bits)).1) + } + + fn finite_decoded(decoded: FullDecoded) -> Decoded { + match decoded { + FullDecoded::Finite(d) => d, + FullDecoded::Nan | FullDecoded::Infinite | FullDecoded::Zero => { + unreachable!("the input bits represent a positive finite nonzero float") + } + } + } + + // Exhaust the high exponent bits: 4 groups for f32 and 32 for f64. + // The remaining exponent bits and every significand bit stay symbolic. + // Their union is the original positive finite nonzero input domain, + // including subnormals. Every strategy instantiates the complete list. + // Fallback reachability is existential over the union. Check it in f64 + // group 16; individual groups need not contain a fallback case. + macro_rules! for_each_finite_partition { + ($proof:ident) => { + $proof!(f32_00, arbitrary_finite_f32, 0, false); + $proof!(f32_01, arbitrary_finite_f32, 1, false); + $proof!(f32_02, arbitrary_finite_f32, 2, false); + $proof!(f32_03, arbitrary_finite_f32, 3, false); + $proof!(f64_00, arbitrary_finite_f64, 0, false); + $proof!(f64_01, arbitrary_finite_f64, 1, false); + $proof!(f64_02, arbitrary_finite_f64, 2, false); + $proof!(f64_03, arbitrary_finite_f64, 3, false); + $proof!(f64_04, arbitrary_finite_f64, 4, false); + $proof!(f64_05, arbitrary_finite_f64, 5, false); + $proof!(f64_06, arbitrary_finite_f64, 6, false); + $proof!(f64_07, arbitrary_finite_f64, 7, false); + $proof!(f64_08, arbitrary_finite_f64, 8, false); + $proof!(f64_09, arbitrary_finite_f64, 9, false); + $proof!(f64_10, arbitrary_finite_f64, 10, false); + $proof!(f64_11, arbitrary_finite_f64, 11, false); + $proof!(f64_12, arbitrary_finite_f64, 12, false); + $proof!(f64_13, arbitrary_finite_f64, 13, false); + $proof!(f64_14, arbitrary_finite_f64, 14, false); + $proof!(f64_15, arbitrary_finite_f64, 15, false); + $proof!(f64_16, arbitrary_finite_f64, 16, true); + $proof!(f64_17, arbitrary_finite_f64, 17, false); + $proof!(f64_18, arbitrary_finite_f64, 18, false); + $proof!(f64_19, arbitrary_finite_f64, 19, false); + $proof!(f64_20, arbitrary_finite_f64, 20, false); + $proof!(f64_21, arbitrary_finite_f64, 21, false); + $proof!(f64_22, arbitrary_finite_f64, 22, false); + $proof!(f64_23, arbitrary_finite_f64, 23, false); + $proof!(f64_24, arbitrary_finite_f64, 24, false); + $proof!(f64_25, arbitrary_finite_f64, 25, false); + $proof!(f64_26, arbitrary_finite_f64, 26, false); + $proof!(f64_27, arbitrary_finite_f64, 27, false); + $proof!(f64_28, arbitrary_finite_f64, 28, false); + $proof!(f64_29, arbitrary_finite_f64, 29, false); + $proof!(f64_30, arbitrary_finite_f64, 30, false); + $proof!(f64_31, arbitrary_finite_f64, 31, false); + }; + } + pub(crate) use for_each_finite_partition; + + // Upper bound on the (symbolic) digit-buffer length used by the proofs of + // `digits_to_dec_str` / `digits_to_exp_str`. Their `assume_init` safety + // obligations depend only on control flow driven by `buf.len()`, `exp`, and + // the digit-count arguments, and every length-dependent branch is a + // comparison against a small value (`buf.len() == 1` in `digits_to_exp_str`, + // `exp < buf.len()` and `frac_digits > buf.len() - exp` in + // `digits_to_dec_str`), so a symbolic length in `1..=4` reaches every branch + // and therefore every distinct set of initialized `parts`; a longer buffer + // only adds digits to a `Part::Copy` slice. + const PROOF_BUFLEN: usize = 4; + + // A digit buffer of symbolic length `1..=PROOF_BUFLEN` whose first digit is + // nonzero, as the callees require. + fn any_digits(buf: &[u8; PROOF_BUFLEN]) -> &[u8] { + kani::assume(buf[0] > b'0'); + let n: usize = kani::any(); + kani::assume(n >= 1 && n <= PROOF_BUFLEN); + &buf[..n] + } + + // `digits_to_dec_str` writes 2, 3, or 4 `parts` depending on `exp` and + // `frac_digits`, then `assume_init_ref`s exactly the prefix it wrote. Kani + // checks that no uninitialized `Part` is ever read and that no UB occurs. + #[kani::proof] + fn check_digits_to_dec_str() { + let buf: [u8; PROOF_BUFLEN] = kani::any(); + let exp: i16 = kani::any(); + let frac_digits: usize = kani::any(); + let mut parts: [MaybeUninit>; 4] = [const { MaybeUninit::uninit() }; 4]; + let _ = digits_to_dec_str(any_digits(&buf), exp, frac_digits, &mut parts); + } + + // `digits_to_exp_str` writes a variable prefix of up to 6 `parts` and + // `assume_init_ref`s `parts[..n + 2]` for the `n` it actually wrote; the + // `buf.len() == 1` case takes its own (3-part) path. + #[kani::proof] + fn check_digits_to_exp_str() { + let buf: [u8; PROOF_BUFLEN] = kani::any(); + let exp: i16 = kani::any(); + let min_ndigits: usize = kani::any(); + let upper: bool = kani::any(); + let mut parts: [MaybeUninit>; 6] = [const { MaybeUninit::uninit() }; 6]; + let _ = digits_to_exp_str(any_digits(&buf), exp, min_ndigits, upper, &mut parts); + } + + // An arbitrary sign-formatting option. + fn any_sign() -> Sign { + if kani::any() { Sign::Minus } else { Sign::MinusPlus } + } + + // A stub digit generator standing in for `grisu`/`dragon` `format_shortest`. + // It writes one arbitrary nonzero digit into the scratch buffer and returns + // it with an arbitrary exponent. This isolates the `to_shortest_*` + // functions' own `unsafe` (the `assume_init` on `parts` and the delegation + // to the already-verified `digits_to_*_str`) from the loopy strategy code, + // which is verified separately. A generic `fn` is required here rather than + // a closure so it satisfies the higher-ranked lifetime in the `F` bound. + fn stub_shortest<'a>(_d: &Decoded, buf: &'a mut [MaybeUninit]) -> (&'a [u8], i16) { + let digit: u8 = kani::any(); + kani::assume(digit > b'0'); + buf[0] = MaybeUninit::new(digit); + let exp: i16 = kani::any(); + // SAFETY: we just initialized the element `..1`. + (unsafe { buf[..1].assume_init_ref() }, exp) + } + + // `to_shortest_str` handles NaN/Inf/Zero by writing `parts[..1]` and the + // finite case by delegating to `digits_to_dec_str`. An arbitrary `f64` + // reaches every `FullDecoded` arm. + #[kani::proof] + fn check_to_shortest_str() { + let v: f64 = kani::any(); + let sign = any_sign(); + let frac_digits: usize = kani::any(); + let mut buf: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let mut parts: [MaybeUninit>; 4] = [const { MaybeUninit::uninit() }; 4]; + let _ = to_shortest_str(stub_shortest, v, sign, frac_digits, &mut buf, &mut parts); + } + + // `to_shortest_exp_str` is the exponential-form analogue; its finite arm + // delegates to `digits_to_dec_str` or `digits_to_exp_str` per `dec_bounds`. + #[kani::proof] + fn check_to_shortest_exp_str() { + let v: f64 = kani::any(); + let sign = any_sign(); + let lo: i16 = kani::any(); + let hi: i16 = kani::any(); + kani::assume(lo <= hi); + let upper: bool = kani::any(); + let mut buf: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let mut parts: [MaybeUninit>; 6] = [const { MaybeUninit::uninit() }; 6]; + let _ = to_shortest_exp_str(stub_shortest, v, sign, (lo, hi), upper, &mut buf, &mut parts); + } + + // For `f64`, `decode` bottoms out at `decoded.exp == -1076` (normal-min, + // which subtracts 2 from `integer_decode`'s minimum of `-1074`), where + // `estimate_max_buf_len` returns 828. 1024 (the size the real `fmt` callers + // use) covers every reachable decoded exponent for the + // `buf.len() >= maxlen` assertions in both `to_exact_*` functions. + const PROOF_EXACT_BUFLEN: usize = 1024; + + // Stub `format_exact` for `to_exact_exp_str`, which always passes the result + // to `digits_to_exp_str` (it calls the generator with `limit = i16::MIN`, so + // the real one never returns an empty buffer here). Returns one nonzero + // digit with an arbitrary exponent. + fn stub_exact_full<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + _limit: i16, + ) -> (&'a [u8], i16) { + let digit: u8 = kani::any(); + kani::assume(digit > b'0'); + buf[0] = MaybeUninit::new(digit); + let exp: i16 = kani::any(); + // SAFETY: we just initialized the element `..1`. + (unsafe { buf[..1].assume_init_ref() }, exp) + } + + // Stub `format_exact` for `to_exact_fixed_str`, which branches on + // `exp <= limit`. That arm requires an empty result (the source + // `debug_assert_eq!`s `buf.len() == 0`); the other arm needs a valid nonzero + // digit with `exp > limit`. Couple the result to `limit` so both caller + // arms are exercised soundly. + fn stub_exact_limited<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + limit: i16, + ) -> (&'a [u8], i16) { + if kani::any() { + let exp: i16 = kani::any(); + kani::assume(exp <= limit); + // SAFETY: an empty prefix is trivially initialized. + (unsafe { buf[..0].assume_init_ref() }, exp) + } else { + let digit: u8 = kani::any(); + kani::assume(digit > b'0'); + buf[0] = MaybeUninit::new(digit); + let exp: i16 = kani::any(); + kani::assume(exp > limit); + // SAFETY: we just initialized the element `..1`. + (unsafe { buf[..1].assume_init_ref() }, exp) + } + } + + // `to_exact_exp_str` writes `parts[..1]` for NaN/Inf, `parts[..3]`/`parts[..1]` + // for zero, and delegates to `digits_to_exp_str` for finite values. + #[kani::proof] + fn check_to_exact_exp_str() { + let v: f64 = kani::any(); + let sign = any_sign(); + let ndigits: usize = kani::any(); + kani::assume(ndigits > 0); + let upper: bool = kani::any(); + let mut buf: [MaybeUninit; PROOF_EXACT_BUFLEN] = + [const { MaybeUninit::uninit() }; PROOF_EXACT_BUFLEN]; + let mut parts: [MaybeUninit>; 6] = [const { MaybeUninit::uninit() }; 6]; + let _ = to_exact_exp_str(stub_exact_full, v, sign, ndigits, upper, &mut buf, &mut parts); + } + + // `to_exact_fixed_str` additionally has a finite sub-branch (`exp <= limit`) + // that renders like zero; `stub_exact_limited` reaches both sub-branches. + #[kani::proof] + fn check_to_exact_fixed_str() { + let v: f64 = kani::any(); + let sign = any_sign(); + let frac_digits: usize = kani::any(); + let mut buf: [MaybeUninit; PROOF_EXACT_BUFLEN] = + [const { MaybeUninit::uninit() }; PROOF_EXACT_BUFLEN]; + let mut parts: [MaybeUninit>; 4] = [const { MaybeUninit::uninit() }; 4]; + let _ = to_exact_fixed_str(stub_exact_limited, v, sign, frac_digits, &mut buf, &mut parts); + } +} diff --git a/library/core/src/num/flt2dec/rounding_verify.rs b/library/core/src/num/flt2dec/rounding_verify.rs new file mode 100644 index 0000000000000..c00e35d22f374 --- /dev/null +++ b/library/core/src/num/flt2dec/rounding_verify.rs @@ -0,0 +1,100 @@ +//! A bounded contract for the rounding helper used by the strategy proofs. + +use super::round_up; +use crate::kani; + +const PROOF_BUFLEN: usize = 32; + +// Read only the active slice, checking the byte condition needed by round_up. +pub(crate) fn bytes_below_max(digits: &[u8]) -> bool { + assert!(digits.len() <= PROOF_BUFLEN); + macro_rules! check_bytes { + ($($index:literal),+ $(,)?) => { + true $(& ((digits.len() <= $index) || digits[$index] < u8::MAX))+ + }; + } + check_bytes!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, + 25, 26, 27, 28, 29, 30, 31, + ) +} + +// Read every byte with constant indices in helper proofs. +pub(crate) fn prefix_checksum(digits: &[u8]) -> u8 { + assert!(digits.len() <= PROOF_BUFLEN); + macro_rules! read_bytes { + ($($index:literal),+ $(,)?) => { + 0 $(^ (if digits.len() > $index { digits[$index] } else { 0 }))+ + }; + } + read_bytes!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, + 25, 26, 27, 28, 29, 30, 31, + ) +} + +// The fixed capacity lets contract predicates use constant indices instead of +// unfolding a symbolic iterator each time a generator rounds its output. +pub(crate) fn prefix_all( + digits: &[u8; PROOF_BUFLEN], + len: usize, + predicate: impl Fn(u8) -> bool, +) -> bool { + macro_rules! check_bytes { + ($($index:literal),+ $(,)?) => { + true $(& ((len <= $index) | predicate(digits[$index])))+ + }; + } + + check_bytes!( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, + 25, 26, 27, 28, 29, 30, 31, + ) +} + +// A fixed array gives the contract a sized write set. The adapter below copies +// only the active prefix back, so the contract cannot initialize unused bytes +// in a generator's MaybeUninit buffer. +#[kani::requires( + len <= PROOF_BUFLEN && prefix_all(digits, len, |digit| digit < u8::MAX) +)] +#[kani::ensures(|result| { + *result == old( + prefix_all(digits, len, |digit| digit == b'9') + .then_some(if len == 0 { b'1' } else { b'0' }) + ) +})] +#[kani::modifies(digits)] +pub(crate) fn round_up_contract(digits: &mut [u8; PROOF_BUFLEN], len: usize) -> Option { + round_up(&mut digits[..len]) +} + +// The caller's proof uses the contract for round_up_contract. No assumptions +// are made here: the contract checks the input byte constraint, and this +// adapter checks the bound before copying the caller's prefix. +pub(crate) fn stub_round_up(digits: &mut [u8]) -> Option { + let len = digits.len(); + assert!(len <= PROOF_BUFLEN); + let mut storage = [0; PROOF_BUFLEN]; + storage[..len].copy_from_slice(digits); + let result = round_up_contract(&mut storage, len); + digits.copy_from_slice(&storage[..len]); + result +} + +#[kani::proof_for_contract(round_up_contract)] +#[kani::unwind(33)] +fn check_round_up_contract() { + let mut digits: [u8; PROOF_BUFLEN] = kani::any(); + let len: usize = kani::any(); + let result = round_up_contract(&mut digits, len); + kani::cover(len == 0, "rounding accepts an empty prefix"); + kani::cover( + len == PROOF_BUFLEN && result == Some(b'0'), + "rounding carries across the full buffer", + ); + kani::cover( + len == PROOF_BUFLEN && result.is_none(), + "rounding can preserve the full buffer length", + ); +} diff --git a/library/core/src/num/flt2dec/strategy/dragon.rs b/library/core/src/num/flt2dec/strategy/dragon.rs index dd73e4b4846d5..4ac98bf621ba3 100644 --- a/library/core/src/num/flt2dec/strategy/dragon.rs +++ b/library/core/src/num/flt2dec/strategy/dragon.rs @@ -28,6 +28,8 @@ static POW5TO256: [Digit; 19] = [ #[doc(hidden)] pub fn mul_pow10(x: &mut Big, n: usize) -> &mut Big { + #[cfg(kani)] + let n = dragon_verify::proof_pow10_exponent(n); debug_assert!(n < 512); // Save ourself the left shift for the smallest cases. if n < 8 { @@ -387,3 +389,536 @@ pub fn format_exact<'a>( // SAFETY: we initialized that memory above. (unsafe { buf[..len].assume_init_ref() }, k) } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod dragon_verify { + use super::*; + use crate::kani; + use crate::num::flt2dec::flt2dec_verify::{ + arbitrary_finite_f32, arbitrary_finite_f64, arbitrary_finite_f64_exponent, + for_each_finite_partition, + }; + + // Keep exact comparison semantics and the generator's digit writes. The + // comparison models have a separate equivalence proof; exact mode also + // uses the division contract below for initial fixup. Neither termination + // nor the buffer index is assumed. Bigint unwind assertions remain enabled. + // Lengths above 32 require a separate proof; these harnesses are bounded. + const PROOF_BUFLEN: usize = 32; + const _: () = assert!(PROOF_BUFLEN <= u8::MAX as usize); + + // The models assert the size bounds checked by the independent equivalence + // proof, then compute exact results with constant limb indices. + fn stub_cmp(left: &Big, right: &Big) -> Ordering { + left.kani_cmp_model(right) + } + + fn stub_is_zero(value: &Big) -> bool { + value.kani_is_zero_model() + } + + #[kani::proof] + #[kani::unwind(41)] + #[kani::solver(kissat)] + fn check_comparison_models_agree() { + // These methods only need size bounds. Inactive limbs may be arbitrary; + // unlike arithmetic contracts, this proof needs no zero-tail invariant. + // Six symbolic bits represent every permitted size, 0 through 40, while + // keeping unused upper index bits concrete during symbolic execution. + let left = Big::kani_with_arbitrary_limbs(usize::from(kani::any::() & 0x3f)); + let right = Big::kani_with_arbitrary_limbs(usize::from(kani::any::() & 0x3f)); + // This is exactly the domain asserted by both models at their call sites. + kani::assume(left.kani_size() <= 40 && right.kani_size() <= 40); + assert!(left.cmp(&right) == left.kani_cmp_model(&right)); + assert!(left.is_zero() == left.kani_is_zero_model()); + let ordering = left.kani_cmp_model(&right); + kani::cover(ordering == Ordering::Less, "comparison can be less"); + kani::cover(ordering == Ordering::Equal, "comparison can be equal"); + kani::cover(ordering == Ordering::Greater, "comparison can be greater"); + kani::cover(left.kani_is_zero_model(), "zero testing accepts zero"); + kani::cover(!left.kani_is_zero_model(), "zero testing accepts nonzero limbs"); + kani::cover(left.kani_size() == 0, "comparison accepts empty zero storage"); + kani::cover(left.kani_size() == 40, "comparison accepts all bigint limbs"); + kani::cover( + left.kani_size() == 0 && !left.kani_valid_storage(), + "comparison models accept arbitrary inactive limbs", + ); + } + + #[kani::proof] + #[kani::unwind(41)] + #[kani::solver(kissat)] + fn check_add_model_agrees() { + let source = Big::kani_with_arbitrary_limbs(usize::from(kani::any::() & 0x3f)); + let other = Big::kani_with_arbitrary_limbs(usize::from(kani::any::() & 0x3f)); + kani::assume(source.kani_size() < 40 && other.kani_size() < 40); + kani::cover(source.kani_size() == 0, "addition accepts empty storage"); + kani::cover(source.kani_size() == 39, "addition accepts the largest model input"); + let mut actual = source.clone(); + let mut modeled = source; + let actual_start = &mut actual as *mut Big; + let modeled_start = &mut modeled as *mut Big; + assert!(actual.add(&other) as *mut Big == actual_start); + assert!(modeled.kani_add_model(&other) as *mut Big == modeled_start); + assert!(actual.kani_same_storage(&modeled)); + kani::cover(actual.kani_size() == 40, "addition can append a carry limb"); + } + + #[kani::proof] + #[kani::unwind(41)] + #[kani::solver(kissat)] + fn check_sub_model_agrees() { + let source = Big::kani_with_arbitrary_limbs(usize::from(kani::any::() & 0x3f)); + let other = Big::kani_with_arbitrary_limbs(usize::from(kani::any::() & 0x3f)); + kani::assume(source.kani_size() <= 40 && other.kani_size() <= 40); + kani::assume(source.kani_cmp_model(&other) != Ordering::Less); + kani::cover(source.kani_size() == 0, "subtraction accepts empty storage"); + kani::cover(source.kani_size() == 40, "subtraction accepts all limbs"); + let mut actual = source.clone(); + let mut modeled = source; + let actual_start = &mut actual as *mut Big; + let modeled_start = &mut modeled as *mut Big; + assert!(actual.sub(&other) as *mut Big == actual_start); + assert!(modeled.kani_sub_model(&other) as *mut Big == modeled_start); + assert!(actual.kani_same_storage(&modeled)); + } + + fn check_mul_small_model_agrees() { + assert!(SIZE < 40); + let source = Big::kani_with_arbitrary_limbs(SIZE); + let multiplier: u32 = kani::any(); + kani::cover(source.kani_size() == 0, "multiplication accepts empty storage"); + kani::cover(source.kani_size() == 39, "multiplication accepts the largest model input"); + kani::cover(multiplier == 0, "multiplication accepts zero"); + kani::cover(multiplier == u32::MAX, "multiplication accepts the largest digit"); + let mut actual = source.clone(); + let mut modeled = source; + let actual_start = &mut actual as *mut Big; + let modeled_start = &mut modeled as *mut Big; + assert!(actual.mul_small(multiplier) as *mut Big == actual_start); + assert!(modeled.kani_mul_small_model(multiplier) as *mut Big == modeled_start); + assert!(actual.kani_same_storage(&modeled)); + kani::cover(actual.kani_size() == 40, "multiplication can append a carry limb"); + } + + macro_rules! check_mul_size { + ($name:ident, $size:literal) => { + #[kani::proof] + #[kani::unwind(41)] + #[kani::solver(kissat)] + fn $name() { + check_mul_small_model_agrees::<$size>(); + } + }; + } + + // Together these cases retain every storage size accepted by the model. + check_mul_size!(check_mul_small_model_agrees_00, 0); + check_mul_size!(check_mul_small_model_agrees_01, 1); + check_mul_size!(check_mul_small_model_agrees_02, 2); + check_mul_size!(check_mul_small_model_agrees_03, 3); + check_mul_size!(check_mul_small_model_agrees_04, 4); + check_mul_size!(check_mul_small_model_agrees_05, 5); + check_mul_size!(check_mul_small_model_agrees_06, 6); + check_mul_size!(check_mul_small_model_agrees_07, 7); + check_mul_size!(check_mul_small_model_agrees_08, 8); + check_mul_size!(check_mul_small_model_agrees_09, 9); + check_mul_size!(check_mul_small_model_agrees_10, 10); + check_mul_size!(check_mul_small_model_agrees_11, 11); + check_mul_size!(check_mul_small_model_agrees_12, 12); + check_mul_size!(check_mul_small_model_agrees_13, 13); + check_mul_size!(check_mul_small_model_agrees_14, 14); + check_mul_size!(check_mul_small_model_agrees_15, 15); + check_mul_size!(check_mul_small_model_agrees_16, 16); + check_mul_size!(check_mul_small_model_agrees_17, 17); + check_mul_size!(check_mul_small_model_agrees_18, 18); + check_mul_size!(check_mul_small_model_agrees_19, 19); + check_mul_size!(check_mul_small_model_agrees_20, 20); + check_mul_size!(check_mul_small_model_agrees_21, 21); + check_mul_size!(check_mul_small_model_agrees_22, 22); + check_mul_size!(check_mul_small_model_agrees_23, 23); + check_mul_size!(check_mul_small_model_agrees_24, 24); + check_mul_size!(check_mul_small_model_agrees_25, 25); + check_mul_size!(check_mul_small_model_agrees_26, 26); + check_mul_size!(check_mul_small_model_agrees_27, 27); + check_mul_size!(check_mul_small_model_agrees_28, 28); + check_mul_size!(check_mul_small_model_agrees_29, 29); + check_mul_size!(check_mul_small_model_agrees_30, 30); + check_mul_size!(check_mul_small_model_agrees_31, 31); + check_mul_size!(check_mul_small_model_agrees_32, 32); + check_mul_size!(check_mul_small_model_agrees_33, 33); + check_mul_size!(check_mul_small_model_agrees_34, 34); + check_mul_size!(check_mul_small_model_agrees_35, 35); + check_mul_size!(check_mul_small_model_agrees_36, 36); + check_mul_size!(check_mul_small_model_agrees_37, 37); + check_mul_size!(check_mul_small_model_agrees_38, 38); + check_mul_size!(check_mul_small_model_agrees_39, 39); + + // Bigint division needs the remainder bound to justify the next limb's + // division. Prove that scalar obligation separately; the storage contract + // below does not depend on the quotient's numeric value. + #[kani::requires(borrow < divisor)] + #[kani::ensures(|result| result.1 < divisor)] + fn div_rem_digit_contract(digit: u32, divisor: u32, borrow: u32) -> (u32, u32) { + ::full_div_rem(digit, divisor, borrow) + } + + // Keep ordinary stub substitution separate from verified contract dispatch. + fn stub_div_rem_digit(digit: u32, divisor: u32, borrow: u32) -> (u32, u32) { + div_rem_digit_contract(digit, divisor, borrow) + } + + #[kani::proof_for_contract(div_rem_digit_contract)] + #[kani::solver(kissat)] + fn check_div_rem_digit_contract() { + let digit: u32 = kani::any(); + let divisor: u32 = kani::any(); + let borrow: u32 = kani::any(); + let (_, remainder) = div_rem_digit_contract(digit, divisor, borrow); + kani::cover(divisor == 1, "limb division accepts the unit divisor"); + kani::cover(divisor == u32::MAX, "limb division accepts the largest divisor"); + kani::cover(borrow == divisor - 1, "limb division accepts the largest borrow"); + kani::cover(remainder == 0, "limb division can have no remainder"); + } + + // Verify the limb loop separately from the outer power-of-ten loop. + // Only limbs are writable, so stubs retain the caller's size expression. + #[kani::requires(divisor > 0 && value.kani_valid_storage())] + #[kani::ensures(|result| { + value.kani_valid_storage() + && value.kani_size() == old(value.kani_size()) + && *result < divisor + })] + #[kani::modifies(value.kani_limbs_mut())] + fn div_rem_small_contract(value: &mut Big, divisor: u32) -> u32 { + value.div_rem_small(divisor).1 + } + + fn stub_div_rem_small(value: &mut Big, divisor: u32) -> (&mut Big, u32) { + let remainder = div_rem_small_contract(value, divisor); + (value, remainder) + } + + #[kani::proof_for_contract(div_rem_small_contract)] + #[kani::stub( + ::full_div_rem, + stub_div_rem_digit + )] + #[kani::stub_verified(div_rem_digit_contract)] + #[kani::unwind(41)] + #[kani::solver(kissat)] + fn check_div_rem_small_contract() { + let mut value = Big::kani_any_valid(); + let divisor: u32 = kani::any(); + let _ = div_rem_small_contract(&mut value, divisor); + kani::cover(divisor == 1, "bigint division accepts the unit divisor"); + kani::cover(divisor == u32::MAX, "bigint division accepts the largest divisor"); + kani::cover(value.kani_size() == 0, "bigint division accepts empty zero storage"); + kani::cover(value.kani_size() == 40, "bigint division accepts all limbs"); + } + + // Division preserves the bigint's allocated prefix and unused zero limbs. + // Its numeric result is overapproximated; the generator still performs the + // real addition, exact comparison semantics, and subsequent digit extraction. + // Read size without constructing a slice: old expressions must not panic. + #[kani::requires(n <= PROOF_BUFLEN && value.kani_valid_storage())] + #[kani::ensures(|_| { + value.kani_valid_storage() && value.kani_size() == old(value.kani_size()) + })] + #[kani::modifies(value.kani_limbs_mut())] + fn div_2pow10_contract(value: &mut Big, n: usize) { + let _ = div_2pow10(value, n); + } + + fn stub_div_2pow10(value: &mut Big, n: usize) -> &mut Big { + div_2pow10_contract(value, n); + value + } + + #[kani::proof_for_contract(div_2pow10_contract)] + #[kani::stub(Big::div_rem_small, stub_div_rem_small)] + #[kani::stub_verified(div_rem_small_contract)] + #[kani::unwind(5)] + #[kani::solver(kissat)] + fn check_div_2pow10_contract() { + let mut value = Big::kani_any_valid(); + let n: usize = kani::any(); + div_2pow10_contract(&mut value, n); + kani::cover(n == 0, "division accepts the minimum power"); + kani::cover(n == PROOF_BUFLEN, "division accepts the maximum proof power"); + kani::cover(value.kani_size() == 0, "division accepts empty zero storage"); + kani::cover(value.kani_size() == 40, "division accepts all bigint limbs"); + } + + // Only the additional [1, 2) probes use this adapter. Check the scaling + // value against the independently proved model for the actual arguments, + // then expose the literal zero before expanding bigint multiplication. + // A nonzero estimate fails the proof; it is never assumed away. + fn estimate_unit_scale(mant: u64, exp: i16) -> i16 { + assert_eq!(crate::num::flt2dec::estimator_verify::estimate_scaling_factor(mant, exp), 0); + 0 + } + + // Identity instrumentation lets each proof expose constant exponent bits + // before expanding the original multiplication body. The replacement + // checks equality on every call, so an invalid prefix fails verification. + pub(super) fn proof_pow10_exponent(n: usize) -> usize { + n + } + + struct FixedExponentBits(usize); + struct VariableExponentBits(usize); + + struct Pow10Prefix { + fixed: FixedExponentBits, + variable: VariableExponentBits, + } + + impl Pow10Prefix { + const fn for_range(range: crate::ops::RangeInclusive) -> Self { + let lower = *range.start(); + let upper = *range.end(); + assert!(lower <= upper); + let different = lower ^ upper; + let variable = if different == 0 { 0 } else { usize::MAX >> different.leading_zeros() }; + Self { + fixed: FixedExponentBits(lower & !variable), + variable: VariableExponentBits(variable), + } + } + + fn check(&self, n: usize) -> usize { + let encoded = self.fixed.0 | (n & self.variable.0); + assert_eq!(encoded, n); + encoded + } + } + + // For normal inputs with exponent field e, the estimator uses a binary + // exponent sum between e - bias and e - bias + 1. Group zero also includes + // subnormals, down to -149 for f32 and -1074 for f64. Applying the original + // integer scaling formula to those endpoints gives these magnitude ranges. + // They only choose an encoding; check() proves it equals the actual value. + const F32_POW10_PREFIXES: [Pow10Prefix; 4] = [ + Pow10Prefix::for_range(19..=45), + Pow10Prefix::for_range(0..=19), + Pow10Prefix::for_range(0..=19), + Pow10Prefix::for_range(19..=38), + ]; + + const F64_POW10_PREFIXES: [Pow10Prefix; 32] = [ + Pow10Prefix::for_range(289..=324), + Pow10Prefix::for_range(270..=289), + Pow10Prefix::for_range(251..=270), + Pow10Prefix::for_range(231..=251), + Pow10Prefix::for_range(212..=231), + Pow10Prefix::for_range(193..=212), + Pow10Prefix::for_range(174..=193), + Pow10Prefix::for_range(154..=174), + Pow10Prefix::for_range(135..=154), + Pow10Prefix::for_range(116..=135), + Pow10Prefix::for_range(97..=116), + Pow10Prefix::for_range(77..=97), + Pow10Prefix::for_range(58..=77), + Pow10Prefix::for_range(39..=58), + Pow10Prefix::for_range(19..=39), + Pow10Prefix::for_range(0..=19), + Pow10Prefix::for_range(0..=19), + Pow10Prefix::for_range(19..=38), + Pow10Prefix::for_range(38..=58), + Pow10Prefix::for_range(58..=77), + Pow10Prefix::for_range(77..=96), + Pow10Prefix::for_range(96..=115), + Pow10Prefix::for_range(115..=135), + Pow10Prefix::for_range(135..=154), + Pow10Prefix::for_range(154..=173), + Pow10Prefix::for_range(173..=192), + Pow10Prefix::for_range(192..=212), + Pow10Prefix::for_range(212..=231), + Pow10Prefix::for_range(231..=250), + Pow10Prefix::for_range(250..=270), + Pow10Prefix::for_range(270..=289), + Pow10Prefix::for_range(289..=308), + ]; + + fn checked_pow10_f32(n: usize) -> usize { + F32_POW10_PREFIXES[GROUP].check(n) + } + + fn checked_pow10_f64(n: usize) -> usize { + F64_POW10_PREFIXES[GROUP].check(n) + } + + fn checked_pow10_unit(n: usize) -> usize { + assert_eq!(EXPONENT, 1023); + Pow10Prefix::for_range(0..=0).check(n) + } + + struct LimbCountMask(usize); + + impl LimbCountMask { + fn check(&self, size: usize) -> usize { + let encoded = size & self.0; + assert_eq!(encoded, size); + encoded + } + } + + // Only the two unit-exponent diagnostics use these checked count encodings. + // A count outside the mask fails an assertion, without excluding any input. + fn unit_shortest_limb_count(size: usize) -> usize { + LimbCountMask(3).check(size) + } + + fn unit_exact_limb_count(size: usize) -> usize { + LimbCountMask(7).check(size) + } + + macro_rules! check_partition { + ($name:ident, arbitrary_finite_f32, $group:literal, $cover_fallback:literal) => { + check_partition!( + $name, + arbitrary_finite_f32, + $group, + $cover_fallback, + 19, + 33, + crate::num::flt2dec::estimator_verify::estimate_scaling_factor, + checked_pow10_f32 + ); + }; + ($name:ident, $decode:ident, $group:literal, $cover_fallback:literal) => { + check_partition!($name, $decode, $group, $cover_fallback, 41, 41); + }; + ( + $name:ident, $decode:ident, $group:literal, $cover_fallback:literal, + $shortest_unwind:literal, $exact_unwind:literal + ) => { + check_partition!( + $name, + $decode, + $group, + $cover_fallback, + $shortest_unwind, + $exact_unwind, + crate::num::flt2dec::estimator_verify::estimate_scaling_factor, + checked_pow10_f64 + ); + }; + ( + $name:ident, $decode:ident, $group:literal, $cover_fallback:literal, + $shortest_unwind:literal, $exact_unwind:literal, $estimate:path, $pow10:ident + $(, $shortest_limbs:path, $exact_limbs:path)? + ) => { + mod $name { + use super::*; + + fn stub_pow10_exponent(n: usize) -> usize { + $pow10::<$group>(n) + } + + #[kani::proof] + #[kani::unwind($shortest_unwind)] + $( + #[kani::stub(crate::num::bignum::kani_loop_size, $shortest_limbs)] + #[kani::stub(Big::add, Big::kani_add_model)] + #[kani::stub(Big::sub, Big::kani_sub_model)] + #[kani::stub(Big::mul_small, Big::kani_mul_small_model)] + )? + #[kani::stub(proof_pow10_exponent, stub_pow10_exponent)] + #[kani::stub(crate::num::flt2dec::estimator::estimate_scaling_factor, $estimate)] + #[kani::stub( + u64::leading_zeros, + crate::num::flt2dec::bit_scan_verify::leading_zeros_u64 + )] + #[kani::stub( + u32::leading_zeros, + crate::num::flt2dec::bit_scan_verify::leading_zeros_u32 + )] + #[kani::stub(::cmp, stub_cmp)] + #[kani::stub(Big::is_zero, stub_is_zero)] + #[kani::stub( + crate::num::flt2dec::round_up, + crate::num::flt2dec::rounding_verify::stub_round_up + )] + #[kani::stub_verified(crate::num::flt2dec::rounding_verify::round_up_contract)] + #[kani::solver(kissat)] + fn check_format_shortest() { + let d = $decode::<$group>(); + let len = usize::from(kani::any::()); + kani::assume(len >= MAX_SIG_DIGITS && len <= PROOF_BUFLEN); + let mut buf = [const { MaybeUninit::uninit() }; PROOF_BUFLEN]; + let start = buf.as_ptr().cast::(); + kani::cover(len == MAX_SIG_DIGITS, "shortest uses the minimum buffer"); + kani::cover(len == PROOF_BUFLEN, "shortest uses the largest proof buffer"); + let (digits, _) = format_shortest(&d, &mut buf[..len]); + kani::cover(digits.len() > 1, "shortest produces multiple digits"); + assert!(!digits.is_empty()); + assert!(digits.len() <= len); + assert_eq!(digits.as_ptr(), start); + } + + #[kani::proof] + #[kani::unwind($exact_unwind)] + $( + #[kani::stub(crate::num::bignum::kani_loop_size, $exact_limbs)] + #[kani::stub(Big::add, Big::kani_add_model)] + #[kani::stub(Big::sub, Big::kani_sub_model)] + #[kani::stub(Big::mul_small, Big::kani_mul_small_model)] + )? + #[kani::stub(proof_pow10_exponent, stub_pow10_exponent)] + #[kani::stub(crate::num::flt2dec::estimator::estimate_scaling_factor, $estimate)] + #[kani::stub( + u64::leading_zeros, + crate::num::flt2dec::bit_scan_verify::leading_zeros_u64 + )] + #[kani::stub( + u32::leading_zeros, + crate::num::flt2dec::bit_scan_verify::leading_zeros_u32 + )] + #[kani::stub(::cmp, stub_cmp)] + #[kani::stub(Big::is_zero, stub_is_zero)] + #[kani::stub( + crate::num::flt2dec::round_up, + crate::num::flt2dec::rounding_verify::stub_round_up + )] + #[kani::stub_verified(crate::num::flt2dec::rounding_verify::round_up_contract)] + #[kani::stub(div_2pow10, stub_div_2pow10)] + #[kani::stub_verified(div_2pow10_contract)] + #[kani::solver(kissat)] + fn check_format_exact() { + let d = $decode::<$group>(); + let limit: i16 = kani::any(); + let len = usize::from(kani::any::()); + kani::assume(len <= PROOF_BUFLEN); + let mut buf = [const { MaybeUninit::uninit() }; PROOF_BUFLEN]; + let start = buf.as_ptr().cast::(); + kani::cover(len == 0, "exact accepts an empty buffer"); + kani::cover(len == PROOF_BUFLEN, "exact uses the largest proof buffer"); + let (digits, _) = format_exact(&d, &mut buf[..len], limit); + kani::cover(digits.is_empty(), "exact can return an empty prefix"); + kani::cover(digits.len() > 1, "exact produces multiple digits"); + assert!(digits.len() <= len); + assert_eq!(digits.as_ptr(), start); + } + } + }; + } + + for_each_finite_partition!(check_partition); + // These inputs need fewer bigint limbs. Keep enough iterations for the + // digit and rounding loops; unwinding assertions check every loop bound. + check_partition!( + f64_exp_1023, + arbitrary_finite_f64_exponent, + 1023, + false, + 19, + 33, + estimate_unit_scale, + checked_pow10_unit, + unit_shortest_limb_count, + unit_exact_limb_count + ); +} diff --git a/library/core/src/num/flt2dec/strategy/grisu.rs b/library/core/src/num/flt2dec/strategy/grisu.rs index d3bbb0934e0ff..892d049dbef21 100644 --- a/library/core/src/num/flt2dec/strategy/grisu.rs +++ b/library/core/src/num/flt2dec/strategy/grisu.rs @@ -122,11 +122,20 @@ pub fn cached_power(alpha: i16, gamma: i16) -> (i16, Fp) { let range = (CACHED_POW10.len() as i32) - 1; let domain = (CACHED_POW10_LAST_E - CACHED_POW10_FIRST_E) as i32; let idx = ((gamma as i32) - offset) * range / domain; + #[cfg(kani)] + let idx = proof_cached_power_index(idx); let (f, e, k) = CACHED_POW10[idx as usize]; debug_assert!(alpha <= e && e <= gamma); (k, Fp { f, e }) } +// Diagnostics can expose a constant table entry after asserting its index. +// The original index calculation and table lookup still execute. +#[cfg(kani)] +fn proof_cached_power_index(index: i32) -> i32 { + index +} + /// Given `x > 0`, returns `(k, 10^k)` such that `10^k <= x < 10^(k+1)`. #[doc(hidden)] pub fn max_pow10_no_more_than(x: u32) -> (u8, u32) { @@ -166,6 +175,31 @@ pub fn format_shortest_opt<'a>( d: &Decoded, buf: &'a mut [MaybeUninit], ) -> Option<(/*digits*/ &'a [u8], /*exp*/ i16)> { + let rounding = generate_shortest(d, buf); + round_and_weed( + rounding.digits, + rounding.exp, + rounding.remainder, + rounding.threshold, + rounding.plus1v, + rounding.ten_kappa, + rounding.ulp, + ) +} + +// Keep the initialized prefix and numeric state together for one final call. +// Generation keeps its existing stopping conditions and argument order. +struct ShortestRounding<'a> { + digits: &'a mut [u8], + exp: i16, + remainder: u64, + threshold: u64, + plus1v: u64, + ten_kappa: u64, + ulp: u64, +} + +fn generate_shortest<'a>(d: &Decoded, buf: &'a mut [MaybeUninit]) -> ShortestRounding<'a> { assert!(d.mant > 0); assert!(d.minus > 0); assert!(d.plus > 0); @@ -273,16 +307,16 @@ pub fn format_shortest_opt<'a>( if plus1rem < delta1 { // `plus1 % 10^kappa < delta1 = plus1 - minus1`; we've found the correct `kappa`. let ten_kappa = (ten_kappa as u64) << e; // scale 10^kappa back to the shared exponent - return round_and_weed( + return ShortestRounding { // SAFETY: we initialized that memory above. - unsafe { buf[..i].assume_init_mut() }, + digits: unsafe { buf[..i].assume_init_mut() }, exp, - plus1rem, - delta1, - plus1 - v.f, + remainder: plus1rem, + threshold: delta1, + plus1v: plus1 - v.f, ten_kappa, - 1, - ); + ulp: 1, + }; } // break the loop when we have rendered all integral digits. @@ -322,130 +356,130 @@ pub fn format_shortest_opt<'a>( if r < threshold { let ten_kappa = 1 << e; // implicit divisor - return round_and_weed( + return ShortestRounding { // SAFETY: we initialized that memory above. - unsafe { buf[..i].assume_init_mut() }, + digits: unsafe { buf[..i].assume_init_mut() }, exp, - r, + remainder: r, threshold, - (plus1 - v.f) * ulp, + plus1v: (plus1 - v.f) * ulp, ten_kappa, ulp, - ); + }; } // restore invariants remainder = r; } +} - // we've generated all significant digits of `plus1`, but not sure if it's the optimal one. - // for example, if `minus1` is 3.14153... and `plus1` is 3.14158..., there are 5 different - // shortest representation from 3.14154 to 3.14158 but we only have the greatest one. - // we have to successively decrease the last digit and check if this is the optimal repr. - // there are at most 9 candidates (..1 to ..9), so this is fairly quick. ("rounding" phase) - // - // the function checks if this "optimal" repr is actually within the ulp ranges, - // and also, it is possible that the "second-to-optimal" repr can actually be optimal - // due to the rounding error. in either cases this returns `None`. ("weeding" phase) - // - // all arguments here are scaled by the common (but implicit) value `k`, so that: - // - `remainder = (plus1 % 10^kappa) * k` - // - `threshold = (plus1 - minus1) * k` (and also, `remainder < threshold`) - // - `plus1v = (plus1 - v) * k` (and also, `threshold > plus1v` from prior invariants) - // - `ten_kappa = 10^kappa * k` - // - `ulp = 2^-e * k` - fn round_and_weed( - buf: &mut [u8], - exp: i16, - remainder: u64, - threshold: u64, - plus1v: u64, - ten_kappa: u64, - ulp: u64, - ) -> Option<(&[u8], i16)> { - assert!(!buf.is_empty()); +// we've generated all significant digits of `plus1`, but not sure if it's the optimal one. +// for example, if `minus1` is 3.14153... and `plus1` is 3.14158..., there are 5 different +// shortest representation from 3.14154 to 3.14158 but we only have the greatest one. +// we have to successively decrease the last digit and check if this is the optimal repr. +// there are at most 9 candidates (..1 to ..9), so this is fairly quick. ("rounding" phase) +// +// the function checks if this "optimal" repr is actually within the ulp ranges, +// and also, it is possible that the "second-to-optimal" repr can actually be optimal +// due to the rounding error. in either cases this returns `None`. ("weeding" phase) +// +// all arguments here are scaled by the common (but implicit) value `k`, so that: +// - `remainder = (plus1 % 10^kappa) * k` +// - `threshold = (plus1 - minus1) * k` (and also, `remainder < threshold`) +// - `plus1v = (plus1 - v) * k` (and also, `threshold > plus1v` from prior invariants) +// - `ten_kappa = 10^kappa * k` +// - `ulp = 2^-e * k` +fn round_and_weed( + buf: &mut [u8], + exp: i16, + remainder: u64, + threshold: u64, + plus1v: u64, + ten_kappa: u64, + ulp: u64, +) -> Option<(&[u8], i16)> { + assert!(!buf.is_empty()); - // produce two approximations to `v` (actually `plus1 - v`) within 1.5 ulps. - // the resulting representation should be the closest representation to both. - // - // here `plus1 - v` is used since calculations are done with respect to `plus1` - // in order to avoid overflow/underflow (hence the seemingly swapped names). - let plus1v_down = plus1v + ulp; // plus1 - (v - 1 ulp) - let plus1v_up = plus1v - ulp; // plus1 - (v + 1 ulp) + // produce two approximations to `v` (actually `plus1 - v`) within 1.5 ulps. + // the resulting representation should be the closest representation to both. + // + // here `plus1 - v` is used since calculations are done with respect to `plus1` + // in order to avoid overflow/underflow (hence the seemingly swapped names). + let plus1v_down = plus1v + ulp; // plus1 - (v - 1 ulp) + let plus1v_up = plus1v - ulp; // plus1 - (v + 1 ulp) - // decrease the last digit and stop at the closest representation to `v + 1 ulp`. - let mut plus1w = remainder; // plus1w(n) = plus1 - w(n) - { - let last = buf.last_mut().unwrap(); - - // we work with the approximated digits `w(n)`, which is initially equal to `plus1 - - // plus1 % 10^kappa`. after running the loop body `n` times, `w(n) = plus1 - - // plus1 % 10^kappa - n * 10^kappa`. we set `plus1w(n) = plus1 - w(n) = - // plus1 % 10^kappa + n * 10^kappa` (thus `remainder = plus1w(0)`) to simplify checks. - // note that `plus1w(n)` is always increasing. - // - // we have three conditions to terminate. any of them will make the loop unable to - // proceed, but we then have at least one valid representation known to be closest to - // `v + 1 ulp` anyway. we will denote them as TC1 through TC3 for brevity. - // - // TC1: `w(n) <= v + 1 ulp`, i.e., this is the last repr that can be the closest one. - // this is equivalent to `plus1 - w(n) = plus1w(n) >= plus1 - (v + 1 ulp) = plus1v_up`. - // combined with TC2 (which checks if `w(n+1)` is valid), this prevents the possible - // overflow on the calculation of `plus1w(n)`. - // - // TC2: `w(n+1) < minus1`, i.e., the next repr definitely does not round to `v`. - // this is equivalent to `plus1 - w(n) + 10^kappa = plus1w(n) + 10^kappa > - // plus1 - minus1 = threshold`. the left hand side can overflow, but we know - // `threshold > plus1v`, so if TC1 is false, `threshold - plus1w(n) > - // threshold - (plus1v - 1 ulp) > 1 ulp` and we can safely test if - // `threshold - plus1w(n) < 10^kappa` instead. - // - // TC3: `abs(w(n) - (v + 1 ulp)) <= abs(w(n+1) - (v + 1 ulp))`, i.e., the next repr is - // no closer to `v + 1 ulp` than the current repr. given `z(n) = plus1v_up - plus1w(n)`, - // this becomes `abs(z(n)) <= abs(z(n+1))`. again assuming that TC1 is false, we have - // `z(n) > 0`. we have two cases to consider: - // - // - when `z(n+1) >= 0`: TC3 becomes `z(n) <= z(n+1)`. as `plus1w(n)` is increasing, - // `z(n)` should be decreasing and this is clearly false. - // - when `z(n+1) < 0`: - // - TC3a: the precondition is `plus1v_up < plus1w(n) + 10^kappa`. assuming TC2 is - // false, `threshold >= plus1w(n) + 10^kappa` so it cannot overflow. - // - TC3b: TC3 becomes `z(n) <= -z(n+1)`, i.e., `plus1v_up - plus1w(n) >= - // plus1w(n+1) - plus1v_up = plus1w(n) + 10^kappa - plus1v_up`. the negated TC1 - // gives `plus1v_up > plus1w(n)`, so it cannot overflow or underflow when - // combined with TC3a. - // - // consequently, we should stop when `TC1 || TC2 || (TC3a && TC3b)`. the following is - // equal to its inverse, `!TC1 && !TC2 && (!TC3a || !TC3b)`. - while plus1w < plus1v_up - && threshold - plus1w >= ten_kappa - && (plus1w + ten_kappa < plus1v_up - || plus1v_up - plus1w >= plus1w + ten_kappa - plus1v_up) - { - *last -= 1; - debug_assert!(*last > b'0'); // the shortest repr cannot end with `0` - plus1w += ten_kappa; - } - } + // decrease the last digit and stop at the closest representation to `v + 1 ulp`. + let mut plus1w = remainder; // plus1w(n) = plus1 - w(n) + { + let last = buf.last_mut().unwrap(); - // check if this representation is also the closest representation to `v - 1 ulp`. + // we work with the approximated digits `w(n)`, which is initially equal to `plus1 - + // plus1 % 10^kappa`. after running the loop body `n` times, `w(n) = plus1 - + // plus1 % 10^kappa - n * 10^kappa`. we set `plus1w(n) = plus1 - w(n) = + // plus1 % 10^kappa + n * 10^kappa` (thus `remainder = plus1w(0)`) to simplify checks. + // note that `plus1w(n)` is always increasing. + // + // we have three conditions to terminate. any of them will make the loop unable to + // proceed, but we then have at least one valid representation known to be closest to + // `v + 1 ulp` anyway. we will denote them as TC1 through TC3 for brevity. + // + // TC1: `w(n) <= v + 1 ulp`, i.e., this is the last repr that can be the closest one. + // this is equivalent to `plus1 - w(n) = plus1w(n) >= plus1 - (v + 1 ulp) = plus1v_up`. + // combined with TC2 (which checks if `w(n+1)` is valid), this prevents the possible + // overflow on the calculation of `plus1w(n)`. // - // this is simply same to the terminating conditions for `v + 1 ulp`, with all `plus1v_up` - // replaced by `plus1v_down` instead. overflow analysis equally holds. - if plus1w < plus1v_down + // TC2: `w(n+1) < minus1`, i.e., the next repr definitely does not round to `v`. + // this is equivalent to `plus1 - w(n) + 10^kappa = plus1w(n) + 10^kappa > + // plus1 - minus1 = threshold`. the left hand side can overflow, but we know + // `threshold > plus1v`, so if TC1 is false, `threshold - plus1w(n) > + // threshold - (plus1v - 1 ulp) > 1 ulp` and we can safely test if + // `threshold - plus1w(n) < 10^kappa` instead. + // + // TC3: `abs(w(n) - (v + 1 ulp)) <= abs(w(n+1) - (v + 1 ulp))`, i.e., the next repr is + // no closer to `v + 1 ulp` than the current repr. given `z(n) = plus1v_up - plus1w(n)`, + // this becomes `abs(z(n)) <= abs(z(n+1))`. again assuming that TC1 is false, we have + // `z(n) > 0`. we have two cases to consider: + // + // - when `z(n+1) >= 0`: TC3 becomes `z(n) <= z(n+1)`. as `plus1w(n)` is increasing, + // `z(n)` should be decreasing and this is clearly false. + // - when `z(n+1) < 0`: + // - TC3a: the precondition is `plus1v_up < plus1w(n) + 10^kappa`. assuming TC2 is + // false, `threshold >= plus1w(n) + 10^kappa` so it cannot overflow. + // - TC3b: TC3 becomes `z(n) <= -z(n+1)`, i.e., `plus1v_up - plus1w(n) >= + // plus1w(n+1) - plus1v_up = plus1w(n) + 10^kappa - plus1v_up`. the negated TC1 + // gives `plus1v_up > plus1w(n)`, so it cannot overflow or underflow when + // combined with TC3a. + // + // consequently, we should stop when `TC1 || TC2 || (TC3a && TC3b)`. the following is + // equal to its inverse, `!TC1 && !TC2 && (!TC3a || !TC3b)`. + while plus1w < plus1v_up && threshold - plus1w >= ten_kappa - && (plus1w + ten_kappa < plus1v_down - || plus1v_down - plus1w >= plus1w + ten_kappa - plus1v_down) + && (plus1w + ten_kappa < plus1v_up + || plus1v_up - plus1w >= plus1w + ten_kappa - plus1v_up) { - return None; + *last -= 1; + debug_assert!(*last > b'0'); // the shortest repr cannot end with `0` + plus1w += ten_kappa; } + } - // now we have the closest representation to `v` between `plus1` and `minus1`. - // this is too liberal, though, so we reject any `w(n)` not between `plus0` and `minus0`, - // i.e., `plus1 - plus1w(n) <= minus0` or `plus1 - plus1w(n) >= plus0`. we utilize the facts - // that `threshold = plus1 - minus1` and `plus1 - plus0 = minus0 - minus1 = 2 ulp`. - if 2 * ulp <= plus1w && plus1w <= threshold - 4 * ulp { Some((buf, exp)) } else { None } + // check if this representation is also the closest representation to `v - 1 ulp`. + // + // this is simply same to the terminating conditions for `v + 1 ulp`, with all `plus1v_up` + // replaced by `plus1v_down` instead. overflow analysis equally holds. + if plus1w < plus1v_down + && threshold - plus1w >= ten_kappa + && (plus1w + ten_kappa < plus1v_down + || plus1v_down - plus1w >= plus1w + ten_kappa - plus1v_down) + { + return None; } + + // now we have the closest representation to `v` between `plus1` and `minus1`. + // this is too liberal, though, so we reject any `w(n)` not between `plus0` and `minus0`, + // i.e., `plus1 - plus1w(n) <= minus0` or `plus1 - plus1w(n) >= plus0`. we utilize the facts + // that `threshold = plus1 - minus1` and `plus1 - plus0 = minus0 - minus1 = 2 ulp`. + if 2 * ulp <= plus1w && plus1w <= threshold - 4 * ulp { Some((buf, exp)) } else { None } } /// The shortest mode implementation for Grisu with Dragon fallback. @@ -473,6 +507,34 @@ pub fn format_exact_opt<'a>( buf: &'a mut [MaybeUninit], limit: i16, ) -> Option<(/*digits*/ &'a [u8], /*exp*/ i16)> { + generate_exact(d, buf, limit).and_then(|rounding| { + // SAFETY: generation initialized the recorded prefix, or selected an + // empty prefix. No buffer writes occur between generation and rounding. + unsafe { + possibly_round( + buf, + rounding.len, + rounding.exp, + limit, + rounding.remainder, + rounding.ten_kappa, + rounding.ulp, + ) + } + }) +} + +// Keep the rounding state separate from generation so every exit shares one +// final call. This also avoids repeating its proof contract at each loop step. +struct ExactRounding { + len: usize, + exp: i16, + remainder: u64, + ten_kappa: u64, + ulp: u64, +} + +fn generate_exact(d: &Decoded, buf: &mut [MaybeUninit], limit: i16) -> Option { assert!(d.mant > 0); assert!(d.mant < (1 << 61)); // we need at least three bits of additional precision assert!(!buf.is_empty()); @@ -536,10 +598,14 @@ pub fn format_exact_opt<'a>( // this will increase the false negative rate, but only very, *very* slightly; // it can only matter noticeably when the mantissa is bigger than 60 bits. // - // SAFETY: `len=0`, so the obligation of having initialized this memory is trivial. - return unsafe { - possibly_round(buf, 0, exp, limit, v.f / 10, (max_ten_kappa as u64) << e, err << e) - }; + // The empty prefix needs no initialization. + return Some(ExactRounding { + len: 0, + exp, + remainder: v.f / 10, + ten_kappa: (max_ten_kappa as u64) << e, + ulp: err << e, + }); } else if ((exp as i32 - limit as i32) as usize) < buf.len() { (exp - limit) as usize } else { @@ -569,10 +635,14 @@ pub fn format_exact_opt<'a>( // is the buffer full? run the rounding pass with the remainder. if i == len { let vrem = ((r as u64) << e) + vfrac; // == (v % 10^kappa) * 2^e - // SAFETY: we have initialized `len` many bytes. - return unsafe { - possibly_round(buf, len, exp, limit, vrem, (ten_kappa as u64) << e, err << e) - }; + // We have initialized `len` many bytes. + return Some(ExactRounding { + len, + exp, + remainder: vrem, + ten_kappa: (ten_kappa as u64) << e, + ulp: err << e, + }); } // break the loop when we have rendered all integral digits. @@ -622,8 +692,8 @@ pub fn format_exact_opt<'a>( // is the buffer full? run the rounding pass with the remainder. if i == len { - // SAFETY: we have initialized `len` many bytes. - return unsafe { possibly_round(buf, len, exp, limit, r, 1 << e, err) }; + // We have initialized `len` many bytes. + return Some(ExactRounding { len, exp, remainder: r, ten_kappa: 1 << e, ulp: err }); } // restore invariants @@ -631,130 +701,130 @@ pub fn format_exact_opt<'a>( } // further calculation is useless (`possibly_round` definitely fails), so we give up. - return None; + None +} + +// we've generated all requested digits of `v`, which should be also same to corresponding +// digits of `v - 1 ulp`. now we check if there is a unique representation shared by +// both `v - 1 ulp` and `v + 1 ulp`; this can be either same to generated digits, or +// to the rounded-up version of those digits. if the range contains multiple representations +// of the same length, we cannot be sure and should return `None` instead. +// +// all arguments here are scaled by the common (but implicit) value `k`, so that: +// - `remainder = (v % 10^kappa) * k` +// - `ten_kappa = 10^kappa * k` +// - `ulp = 2^-e * k` +// +// SAFETY: the first `len` bytes of `buf` must be initialized. +unsafe fn possibly_round( + buf: &mut [MaybeUninit], + mut len: usize, + mut exp: i16, + limit: i16, + remainder: u64, + ten_kappa: u64, + ulp: u64, +) -> Option<(&[u8], i16)> { + debug_assert!(remainder < ten_kappa); - // we've generated all requested digits of `v`, which should be also same to corresponding - // digits of `v - 1 ulp`. now we check if there is a unique representation shared by - // both `v - 1 ulp` and `v + 1 ulp`; this can be either same to generated digits, or - // to the rounded-up version of those digits. if the range contains multiple representations - // of the same length, we cannot be sure and should return `None` instead. + // 10^kappa + // : : :<->: : + // : : : : : + // :|1 ulp|1 ulp| : + // :|<--->|<--->| : + // ----|-----|-----|---- + // | v | + // v - 1 ulp v + 1 ulp // - // all arguments here are scaled by the common (but implicit) value `k`, so that: - // - `remainder = (v % 10^kappa) * k` - // - `ten_kappa = 10^kappa * k` - // - `ulp = 2^-e * k` + // (for the reference, the dotted line indicates the exact value for + // possible representations in given number of digits.) // - // SAFETY: the first `len` bytes of `buf` must be initialized. - unsafe fn possibly_round( - buf: &mut [MaybeUninit], - mut len: usize, - mut exp: i16, - limit: i16, - remainder: u64, - ten_kappa: u64, - ulp: u64, - ) -> Option<(&[u8], i16)> { - debug_assert!(remainder < ten_kappa); - - // 10^kappa - // : : :<->: : - // : : : : : - // :|1 ulp|1 ulp| : - // :|<--->|<--->| : - // ----|-----|-----|---- - // | v | - // v - 1 ulp v + 1 ulp - // - // (for the reference, the dotted line indicates the exact value for - // possible representations in given number of digits.) - // - // error is too large that there are at least three possible representations - // between `v - 1 ulp` and `v + 1 ulp`. we cannot determine which one is correct. - if ulp >= ten_kappa { - return None; - } + // error is too large that there are at least three possible representations + // between `v - 1 ulp` and `v + 1 ulp`. we cannot determine which one is correct. + if ulp >= ten_kappa { + return None; + } - // 10^kappa - // :<------->: - // : : - // : |1 ulp|1 ulp| - // : |<--->|<--->| - // ----|-----|-----|---- - // | v | - // v - 1 ulp v + 1 ulp - // - // in fact, 1/2 ulp is enough to introduce two possible representations. - // (remember that we need a unique representation for both `v - 1 ulp` and `v + 1 ulp`.) - // this won't overflow, as `ulp < ten_kappa` from the first check. - if ten_kappa - ulp <= ulp { - return None; - } + // 10^kappa + // :<------->: + // : : + // : |1 ulp|1 ulp| + // : |<--->|<--->| + // ----|-----|-----|---- + // | v | + // v - 1 ulp v + 1 ulp + // + // in fact, 1/2 ulp is enough to introduce two possible representations. + // (remember that we need a unique representation for both `v - 1 ulp` and `v + 1 ulp`.) + // this won't overflow, as `ulp < ten_kappa` from the first check. + if ten_kappa - ulp <= ulp { + return None; + } - // remainder - // :<->| : - // : | : - // :<--------- 10^kappa ---------->: - // | : | : - // |1 ulp|1 ulp| : - // |<--->|<--->| : - // ----|-----|-----|------------------------ - // | v | - // v - 1 ulp v + 1 ulp - // - // if `v + 1 ulp` is closer to the rounded-down representation (which is already in `buf`), - // then we can safely return. note that `v - 1 ulp` *can* be less than the current - // representation, but as `1 ulp < 10^kappa / 2`, this condition is enough: - // the distance between `v - 1 ulp` and the current representation - // cannot exceed `10^kappa / 2`. - // - // the condition equals to `remainder + ulp < 10^kappa / 2`. - // since this can easily overflow, first check if `remainder < 10^kappa / 2`. - // we've already verified that `ulp < 10^kappa / 2`, so as long as - // `10^kappa` did not overflow after all, the second check is fine. - if ten_kappa - remainder > remainder && ten_kappa - 2 * remainder >= 2 * ulp { - // SAFETY: our caller initialized that memory. - return Some((unsafe { buf[..len].assume_init_ref() }, exp)); - } + // remainder + // :<->| : + // : | : + // :<--------- 10^kappa ---------->: + // | : | : + // |1 ulp|1 ulp| : + // |<--->|<--->| : + // ----|-----|-----|------------------------ + // | v | + // v - 1 ulp v + 1 ulp + // + // if `v + 1 ulp` is closer to the rounded-down representation (which is already in `buf`), + // then we can safely return. note that `v - 1 ulp` *can* be less than the current + // representation, but as `1 ulp < 10^kappa / 2`, this condition is enough: + // the distance between `v - 1 ulp` and the current representation + // cannot exceed `10^kappa / 2`. + // + // the condition equals to `remainder + ulp < 10^kappa / 2`. + // since this can easily overflow, first check if `remainder < 10^kappa / 2`. + // we've already verified that `ulp < 10^kappa / 2`, so as long as + // `10^kappa` did not overflow after all, the second check is fine. + if ten_kappa - remainder > remainder && ten_kappa - 2 * remainder >= 2 * ulp { + // SAFETY: our caller initialized that memory. + return Some((unsafe { buf[..len].assume_init_ref() }, exp)); + } - // :<------- remainder ------>| : - // : | : - // :<--------- 10^kappa --------->: - // : | | : | - // : |1 ulp|1 ulp| - // : |<--->|<--->| - // -----------------------|-----|-----|----- - // | v | - // v - 1 ulp v + 1 ulp - // - // on the other hands, if `v - 1 ulp` is closer to the rounded-up representation, - // we should round up and return. for the same reason we don't need to check `v + 1 ulp`. - // - // the condition equals to `remainder - ulp >= 10^kappa / 2`. - // again we first check if `remainder > ulp` (note that this is not `remainder >= ulp`, - // as `10^kappa` is never zero). also note that `remainder - ulp <= 10^kappa`, - // so the second check does not overflow. - if remainder > ulp && ten_kappa - (remainder - ulp) <= remainder - ulp { - if let Some(c) = - // SAFETY: our caller must have initialized that memory. - round_up(unsafe { buf[..len].assume_init_mut() }) - { - // only add an additional digit when we've been requested the fixed precision. - // we also need to check that, if the original buffer was empty, - // the additional digit can only be added when `exp == limit` (edge case). - exp += 1; - if exp > limit && len < buf.len() { - buf[len] = MaybeUninit::new(c); - len += 1; - } + // :<------- remainder ------>| : + // : | : + // :<--------- 10^kappa --------->: + // : | | : | + // : |1 ulp|1 ulp| + // : |<--->|<--->| + // -----------------------|-----|-----|----- + // | v | + // v - 1 ulp v + 1 ulp + // + // on the other hands, if `v - 1 ulp` is closer to the rounded-up representation, + // we should round up and return. for the same reason we don't need to check `v + 1 ulp`. + // + // the condition equals to `remainder - ulp >= 10^kappa / 2`. + // again we first check if `remainder > ulp` (note that this is not `remainder >= ulp`, + // as `10^kappa` is never zero). also note that `remainder - ulp <= 10^kappa`, + // so the second check does not overflow. + if remainder > ulp && ten_kappa - (remainder - ulp) <= remainder - ulp { + if let Some(c) = + // SAFETY: our caller must have initialized that memory. + round_up(unsafe { buf[..len].assume_init_mut() }) + { + // only add an additional digit when we've been requested the fixed precision. + // we also need to check that, if the original buffer was empty, + // the additional digit can only be added when `exp == limit` (edge case). + exp += 1; + if exp > limit && len < buf.len() { + buf[len] = MaybeUninit::new(c); + len += 1; } - // SAFETY: we and our caller initialized that memory. - return Some((unsafe { buf[..len].assume_init_ref() }, exp)); } - - // otherwise we are doomed (i.e., some values between `v - 1 ulp` and `v + 1 ulp` are - // rounding down and others are rounding up) and give up. - None + // SAFETY: we and our caller initialized that memory. + return Some((unsafe { buf[..len].assume_init_ref() }, exp)); } + + // otherwise we are doomed (i.e., some values between `v - 1 ulp` and `v + 1 ulp` are + // rounding down and others are rounding up) and give up. + None } /// The exact and fixed mode implementation for Grisu with Dragon fallback. @@ -774,3 +844,518 @@ pub fn format_exact<'a>( None => fallback(d, buf, limit), } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod grisu_verify { + use super::*; + use crate::kani; + use crate::num::flt2dec::flt2dec_verify::{ + arbitrary_finite_f32, arbitrary_finite_f64, arbitrary_finite_f64_exponent, + arbitrary_finite_f64_range, for_each_finite_partition, + }; + + // The direct strategy harnesses execute the real generator bodies. Exact + // and shortest modes compose separately proved final-rounding contracts. + // Buffer lengths are symbolic: shortest mode includes the minimum legal + // buffer, and exact mode includes both one-byte and multi-digit buffers. + // These are bounded harnesses; a successful run covers lengths up to 32, + // not arbitrary slice lengths. Unwinding assertions remain enabled. + const PROOF_BUFLEN: usize = 32; + const _: () = assert!(PROOF_BUFLEN <= u8::MAX as usize); + + // At digit one the loop must stop. If its remainder would already exceed + // threshold, the loop's threshold check forces an earlier stop. With digit + // zero this checks the initial state, which must not decrement at all. + // Callers establish this numeric condition before using the helper model. + fn weed_stops_before_zero( + digit: u8, + remainder: u64, + threshold: u64, + plus1v: u64, + ten_kappa: u64, + ulp: u64, + ) -> bool { + // The caller bounds digit by nine. Saturation preserves comparison + // with threshold: an overflowing mathematical sum exceeds every u64. + // Repeated additions also match the real loop's remainder updates. + let after_1 = remainder.saturating_add(ten_kappa); + let after_2 = after_1.saturating_add(ten_kappa); + let after_3 = after_2.saturating_add(ten_kappa); + let after_4 = after_3.saturating_add(ten_kappa); + let after_5 = after_4.saturating_add(ten_kappa); + let after_6 = after_5.saturating_add(ten_kappa); + let after_7 = after_6.saturating_add(ten_kappa); + let after_8 = after_7.saturating_add(ten_kappa); + let terminal = match digit { + b'0' | b'1' => remainder, + b'2' => after_1, + b'3' => after_2, + b'4' => after_3, + b'5' => after_4, + b'6' => after_5, + b'7' => after_6, + b'8' => after_7, + _ => after_8, + }; + if terminal >= threshold { + true + } else { + let remainder = terminal; + let target = plus1v - ulp; + !(remainder < target + && threshold - remainder >= ten_kappa + && (remainder + ten_kappa < target + || target - remainder >= remainder + ten_kappa - target)) + } + } + + // Quantify the other prefix bytes inside the proof. The adapter checks the + // actual prefix and passes the final digit, which is the only byte changed. + #[kani::requires( + len > 0 && len <= PROOF_BUFLEN + && digit >= b'0' && digit <= b'9' + && remainder < threshold && ten_kappa > 0 + && ulp <= threshold / 4 && ulp <= plus1v && plus1v <= u64::MAX - ulp + && weed_stops_before_zero(digit, remainder, threshold, plus1v, ten_kappa, ulp) + )] + #[kani::ensures(|result| result.as_ref().is_none_or(|&(written, output_exp)| { + written == len && output_exp == exp + }))] + fn round_shortest_contract( + digit: u8, + len: usize, + exp: i16, + remainder: u64, + threshold: u64, + plus1v: u64, + ten_kappa: u64, + ulp: u64, + ) -> Option<(usize, i16)> { + let mut digits: [u8; PROOF_BUFLEN] = kani::any(); + digits[len - 1] = digit; + kani::assume(crate::num::flt2dec::rounding_verify::prefix_all(&digits, len, |byte| { + byte < u8::MAX + })); + let mut buf = [const { MaybeUninit::uninit() }; PROOF_BUFLEN]; + let start = buf.as_mut_ptr().cast::(); + // SAFETY: the contract bounds len by both distinct arrays' capacities. + unsafe { crate::ptr::copy_nonoverlapping(digits.as_ptr(), start, len) }; + round_and_weed( + // SAFETY: the copy initialized exactly this prefix. + unsafe { buf[..len].assume_init_mut() }, + exp, + remainder, + threshold, + plus1v, + ten_kappa, + ulp, + ) + .map(|(output, output_exp)| { + assert_eq!(output.as_ptr(), start.cast_const()); + let checksum = crate::num::flt2dec::rounding_verify::prefix_checksum(output); + kani::cover(checksum == 0, "shortest rounding returns readable bytes"); + kani::cover(output[len - 1] < digit, "shortest rounding can decrease the final digit"); + (output.len(), output_exp) + }) + } + + fn stub_round_and_weed( + buf: &mut [u8], + exp: i16, + remainder: u64, + threshold: u64, + plus1v: u64, + ten_kappa: u64, + ulp: u64, + ) -> Option<(&[u8], i16)> { + let len = buf.len(); + assert!(len > 0 && len <= PROOF_BUFLEN); + // Read and check every actual byte before invoking the numeric summary. + assert!(crate::num::flt2dec::rounding_verify::bytes_below_max(buf)); + let result = round_shortest_contract( + buf[len - 1], + len, + exp, + remainder, + threshold, + plus1v, + ten_kappa, + ulp, + ); + // Overapproximate output values within the initialized input prefix. + let output: [u8; PROOF_BUFLEN] = kani::any(); + buf.copy_from_slice(&output[..len]); + result.map(|(written, output_exp)| (&buf[..written], output_exp)) + } + + // The last digit is at most nine and the numeric precondition makes the + // loop stop before decrementing one, so at most eight iterations execute. + #[kani::proof_for_contract(round_shortest_contract)] + #[kani::unwind(9)] + #[kani::solver(kissat)] + fn check_round_shortest_contract() { + let digit: u8 = kani::any(); + let len = usize::from(kani::any::()); + let result = round_shortest_contract( + digit, + len, + kani::any(), + kani::any(), + kani::any(), + kani::any(), + kani::any(), + kani::any(), + ); + kani::cover(len == 1 && result.is_some(), "shortest rounding accepts a single digit"); + kani::cover( + len == PROOF_BUFLEN && result.is_some(), + "shortest rounding accepts a full buffer", + ); + kani::cover(result.is_none(), "shortest rounding can request the Dragon fallback"); + } + + // Keep uninitialized padding in this proof: only the initialized input + // prefix is copied before executing the real final-rounding helper. + #[kani::requires( + len <= capacity && capacity <= PROOF_BUFLEN + && exp < i16::MAX && remainder < ten_kappa + )] + #[kani::ensures(|result| result.as_ref().is_none_or(|&(written, _)| { + written >= len && written <= capacity && written - len <= 1 + }))] + fn round_exact_contract( + len: usize, + capacity: usize, + exp: i16, + limit: i16, + remainder: u64, + ten_kappa: u64, + ulp: u64, + ) -> Option<(usize, i16)> { + // Quantify every prefix allowed by the adapter's byte check here. + // The postcondition does not depend on its values, so callers pass + // only the numeric state after checking their actual input bytes. + let digits: [u8; PROOF_BUFLEN] = kani::any(); + kani::assume(crate::num::flt2dec::rounding_verify::prefix_all(&digits, len, |digit| { + digit < u8::MAX + })); + let mut buf = [const { MaybeUninit::uninit() }; PROOF_BUFLEN]; + let start = buf.as_mut_ptr().cast::(); + // SAFETY: the contract bounds len by both distinct arrays' capacities. + // This initializes exactly the prefix required by possibly_round. + unsafe { crate::ptr::copy_nonoverlapping(digits.as_ptr(), start, len) }; + // SAFETY: the copy above initialized the first len bytes. + unsafe { possibly_round(&mut buf[..capacity], len, exp, limit, remainder, ten_kappa, ulp) } + .map(|(output, output_exp)| { + assert_eq!(output.as_ptr(), start.cast_const()); + // Read every returned byte, including any appended carry. This + // checks initialization instead of merely inspecting slice metadata. + let checksum = crate::num::flt2dec::rounding_verify::prefix_checksum(output); + kani::cover(checksum == 0, "final rounding returns readable output bytes"); + (output.len(), output_exp) + }) + } + + // The verified contract overapproximates byte values and the decision to + // return None. It can write only the input prefix or a proved output prefix; + // unused padding in the generator's buffer remains uninitialized. + unsafe fn stub_possibly_round( + buf: &mut [MaybeUninit], + len: usize, + exp: i16, + limit: i16, + remainder: u64, + ten_kappa: u64, + ulp: u64, + ) -> Option<(&[u8], i16)> { + assert!(len <= buf.len() && buf.len() <= PROOF_BUFLEN); + // SAFETY: this adapter has possibly_round's initialized-prefix contract. + // Read every active byte before the model can write to this buffer. + let digits = unsafe { buf[..len].assume_init_ref() }; + assert!(crate::num::flt2dec::rounding_verify::bytes_below_max(digits)); + let result = round_exact_contract(len, buf.len(), exp, limit, remainder, ten_kappa, ulp); + let written = result.map_or(len, |(written, _)| written); + assert!(written <= buf.len()); + // The contract proves metadata and initialized output, without a byte + // value postcondition. Model those bytes here so the verified call has + // an empty write set instead of repeatedly havocing an array. + let output: [u8; PROOF_BUFLEN] = kani::any(); + // SAFETY: the contract bounds written by both distinct arrays. All + // source bytes are initialized; this initializes only the active prefix. + unsafe { + crate::ptr::copy_nonoverlapping(output.as_ptr(), buf.as_mut_ptr().cast(), written) + }; + result.map(|(written, output_exp)| { + // SAFETY: the copy above initialized this prefix. + (unsafe { buf[..written].assume_init_ref() }, output_exp) + }) + } + + #[kani::proof_for_contract(round_exact_contract)] + #[kani::unwind(33)] + #[kani::stub( + crate::num::flt2dec::round_up, + crate::num::flt2dec::rounding_verify::stub_round_up + )] + #[kani::stub_verified(crate::num::flt2dec::rounding_verify::round_up_contract)] + #[kani::solver(kissat)] + fn check_round_exact_contract() { + let len = usize::from(kani::any::()); + let capacity = usize::from(kani::any::()); + let result = round_exact_contract( + len, + capacity, + kani::any(), + kani::any(), + kani::any(), + kani::any(), + kani::any(), + ); + kani::cover(len == 0 && result.is_some(), "final rounding accepts an empty prefix"); + kani::cover( + len == PROOF_BUFLEN && result.is_some(), + "final rounding accepts a full buffer", + ); + kani::cover(result.is_none(), "final rounding can request the Dragon fallback"); + kani::cover( + result.is_some_and(|(written, _)| written > len), + "final rounding can append an initialized carry", + ); + } + + // An arbitrary `Decoded` satisfying every precondition the `grisu` entry + // points assert. `mant + plus < 2^61` (and the `checked_add`/`checked_sub` + // assumptions) keep the scaled `Fp` arithmetic inside `u64`. + fn arbitrary_decoded() -> Decoded { + let mant: u64 = kani::any(); + let minus: u64 = kani::any(); + let plus: u64 = kani::any(); + kani::assume(mant > 0); + kani::assume(minus > 0); + kani::assume(plus > 0); + kani::assume(mant.checked_add(plus).is_some()); + kani::assume(mant.checked_sub(minus).is_some()); + kani::assume(mant + plus < (1 << 61)); + let exp: i16 = kani::any(); + // `[-1076, 970]` is the exponent range of `decode()`; 971 is unreachable. + kani::assume(exp >= -1076 && exp <= 970); + Decoded { mant, minus, plus, exp, inclusive: kani::any() } + } + + // An arbitrary input for the exact-mode proofs: the full documented + // precondition of `format_exact_opt` (`0 < mant < 2^61`), with `exp` + // bounded to the decoder image so `cached_power` stays in its table domain. + fn arbitrary_decoded_exact() -> Decoded { + let mant: u64 = kani::any(); + kani::assume(mant > 0 && mant < (1 << 61)); + let exp: i16 = kani::any(); + kani::assume(exp >= -1076 && exp <= 970); + Decoded { mant, minus: 1, plus: 1, exp, inclusive: kani::any() } + } + + struct CachedPowerIndex(i32); + + impl CachedPowerIndex { + fn check(&self, actual: i32) -> i32 { + assert_eq!(actual, self.0); + self.0 + } + } + + fn checked_cached_power_39(index: i32) -> i32 { + CachedPowerIndex(39).check(index) + } + + // Call the real generator loops and compose the final-rounding proof. The + // wrapper harness below checks a separate obligation. + macro_rules! check_partition { + ($name:ident, $decode:ident, $group:literal, $cover_fallback:literal) => { + check_partition!($name, $decode::<$group>(), $cover_fallback); + }; + ($name:ident, $decoded:expr, $cover_fallback:literal $(, $cached_index:path)?) => { + mod $name { + use super::*; + + #[kani::proof] + #[kani::unwind(19)] + $(#[kani::stub(proof_cached_power_index, $cached_index)])? + #[kani::stub( + u64::leading_zeros, + crate::num::flt2dec::bit_scan_verify::leading_zeros_u64 + )] + #[kani::stub( + u32::leading_zeros, + crate::num::flt2dec::bit_scan_verify::leading_zeros_u32 + )] + #[kani::stub(round_and_weed, stub_round_and_weed)] + #[kani::stub_verified(round_shortest_contract)] + #[kani::solver(kissat)] + fn check_format_shortest_opt() { + let d = $decoded; + let len = usize::from(kani::any::()); + kani::assume(len >= MAX_SIG_DIGITS && len <= PROOF_BUFLEN); + let mut buf = [const { MaybeUninit::uninit() }; PROOF_BUFLEN]; + let start = buf.as_ptr().cast::(); + kani::cover(len == MAX_SIG_DIGITS, "shortest uses the minimum buffer"); + kani::cover(len == PROOF_BUFLEN, "shortest uses the largest proof buffer"); + let result = format_shortest_opt(&d, &mut buf[..len]); + if $cover_fallback { + kani::cover(result.is_none(), "shortest can request the Dragon fallback"); + } + let _ = result.map(|(digits, _)| { + kani::cover(digits.len() > 1, "shortest produces multiple digits"); + assert!(!digits.is_empty()); + assert!(digits.len() <= len); + assert_eq!(digits.as_ptr(), start); + }); + } + + // Integral extraction takes at most ten iterations. Fractional + // extraction stops once err = 10^18 >= 2^59: the cached power + // gives e <= 60, hence maxerr = 2^(e - 1) <= 2^59. The separate + // rounding contract retains its own 33-iteration proof bound. + #[kani::proof] + #[kani::unwind(19)] + $(#[kani::stub(proof_cached_power_index, $cached_index)])? + #[kani::stub( + u64::leading_zeros, + crate::num::flt2dec::bit_scan_verify::leading_zeros_u64 + )] + #[kani::stub( + u32::leading_zeros, + crate::num::flt2dec::bit_scan_verify::leading_zeros_u32 + )] + #[kani::stub(possibly_round, stub_possibly_round)] + #[kani::stub_verified(round_exact_contract)] + #[kani::solver(kissat)] + fn check_format_exact_opt() { + let d = $decoded; + let limit: i16 = kani::any(); + let len = usize::from(kani::any::()); + kani::assume(len > 0 && len <= PROOF_BUFLEN); + let mut buf = [const { MaybeUninit::uninit() }; PROOF_BUFLEN]; + let start = buf.as_ptr().cast::(); + kani::cover(len == 1, "exact uses a one-byte buffer"); + kani::cover(len == PROOF_BUFLEN, "exact uses the largest proof buffer"); + let result = format_exact_opt(&d, &mut buf[..len], limit); + if $cover_fallback { + kani::cover(result.is_none(), "exact can request the Dragon fallback"); + } + let _ = result.map(|(digits, _)| { + kani::cover(digits.is_empty(), "exact can return an empty prefix"); + kani::cover(digits.len() > 1, "exact produces multiple digits"); + assert!(digits.len() <= len); + assert_eq!(digits.as_ptr(), start); + }); + } + } + }; + } + + for_each_finite_partition!(check_partition); + check_partition!(f64_exp_1023, arbitrary_finite_f64_exponent, 1023, false); + + // All positive f64 values in [2^-8, 2^18), with every significand bit symbolic. + // These additional probes assert the cached index instead of assuming it. + check_partition!( + f64_cached_power_39, + arbitrary_finite_f64_range::<0x3f70_0000_0000_0000, 0x4110_0000_0000_0000>(), + false, + checked_cached_power_39 + ); + + // Wholesale havoc stub for the dragon fallback (modelled as an opaque op that + // writes a digit and returns an in-bounds slice of `buf`). + fn stub_dragon_format_exact<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + _limit: i16, + ) -> (&'a [u8], i16) { + let digit: u8 = kani::any(); + kani::assume(digit >= b'0' && digit <= b'9'); + buf[0] = MaybeUninit::new(digit); + // SAFETY: we just initialized element 0. + (unsafe { buf[..1].assume_init_ref() }, kani::any()) + } + + // Wholesale havoc stub for `format_exact_opt`: nondeterministically returns + // `None` (released its borrow of `buf`) or `Some` slice of `buf`. Modelling + // both callees as opaque isolates the WRAPPER's only `unsafe`: the + // lifetime-laundering reborrow `&mut *(buf as *mut _)`, whose soundness rests + // on `buf` being reused only on the `None` path. + fn stub_format_exact_opt<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + _limit: i16, + ) -> Option<(&'a [u8], i16)> { + if kani::any() { + let digit: u8 = kani::any(); + kani::assume(digit >= b'0' && digit <= b'9'); + buf[0] = MaybeUninit::new(digit); + // SAFETY: we just initialized element 0. + Some((unsafe { buf[..1].assume_init_ref() }, kani::any())) + } else { + // The real function writes digits before it gives up; model that + // dirtying so the wrapper's reuse of `buf` on the `None` path is + // exercised against a modified buffer. + buf[0] = MaybeUninit::new(kani::any()); + None + } + } + + #[kani::proof] + #[kani::stub(format_exact_opt, stub_format_exact_opt)] + #[kani::stub(crate::num::flt2dec::strategy::dragon::format_exact, stub_dragon_format_exact)] + fn check_format_exact() { + let d = arbitrary_decoded_exact(); + let limit: i16 = kani::any(); + let mut buf: [MaybeUninit; 4] = [const { MaybeUninit::uninit() }; 4]; + let _ = format_exact(&d, &mut buf, limit); + } + + // Wholesale havoc stubs for `format_shortest`'s callees (no `limit` arg). + fn stub_dragon_format_shortest<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + ) -> (&'a [u8], i16) { + let digit: u8 = kani::any(); + kani::assume(digit >= b'0' && digit <= b'9'); + buf[0] = MaybeUninit::new(digit); + // SAFETY: we just initialized element 0. + (unsafe { buf[..1].assume_init_ref() }, kani::any()) + } + + fn stub_format_shortest_opt<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + ) -> Option<(&'a [u8], i16)> { + if kani::any() { + let digit: u8 = kani::any(); + kani::assume(digit >= b'0' && digit <= b'9'); + buf[0] = MaybeUninit::new(digit); + // SAFETY: we just initialized element 0. + Some((unsafe { buf[..1].assume_init_ref() }, kani::any())) + } else { + // The real function writes digits before it gives up; model that + // dirtying so the wrapper's reuse of `buf` on the `None` path is + // exercised against a modified buffer. + buf[0] = MaybeUninit::new(kani::any()); + None + } + } + + // `format_shortest` mirrors `format_exact`: its only `unsafe` is the + // lifetime-laundering reborrow, verified by modelling both callees as opaque. + #[kani::proof] + #[kani::stub(format_shortest_opt, stub_format_shortest_opt)] + #[kani::stub( + crate::num::flt2dec::strategy::dragon::format_shortest, + stub_dragon_format_shortest + )] + fn check_format_shortest() { + let d = arbitrary_decoded(); + let mut buf: [MaybeUninit; 4] = [const { MaybeUninit::uninit() }; 4]; + let _ = format_shortest(&d, &mut buf); + } +} diff --git a/scripts/kani-std-analysis/flt2dec_harnesses.py b/scripts/kani-std-analysis/flt2dec_harnesses.py new file mode 100644 index 0000000000000..435249c0a6a3d --- /dev/null +++ b/scripts/kani-std-analysis/flt2dec_harnesses.py @@ -0,0 +1,112 @@ +"""Assign flt2dec proofs to dedicated CI jobs without duplicating std partitions.""" + +import argparse +import json +import sys + + +DRAGON = "num::flt2dec::strategy::dragon::dragon_verify" +GRISU = "num::flt2dec::strategy::grisu::grisu_verify" +OPERATING_SYSTEMS = ["ubuntu-latest", "macos-latest"] + + +def proof_groups(): + groups = [] + + def add(name, kind, harnesses, timeout_minutes): + groups.append({"name": name, "kind": kind, "harnesses": harnesses, + "timeout_minutes": timeout_minutes}) + + for name, module, proof, batch_size, timeout_minutes in [ + ("dragon-exact", DRAGON, "check_format_exact", 4, 60), + ("dragon-shortest", DRAGON, "check_format_shortest", 4, 60), + ("grisu-exact", GRISU, "check_format_exact_opt", 4, 60), + ("grisu-shortest", GRISU, "check_format_shortest_opt", 2, 120), + ]: + for width, count in ((32, 4), (64, 32)): + for first in range(0, count, batch_size): + last = first + batch_size - 1 + partition = f"f{width}" if count == batch_size else f"f{width}-{first:02d}-{last:02d}" + add(f"{name}-{partition}", f"generator-f{width}", [ + f"{module}::f{width}_{group:02d}::{proof}" for group in range(first, last + 1) + ], timeout_minutes) + add(f"{name}-fixed-exponent", "probe", [ + f"{module}::f64_exp_1023::{proof}" + ], timeout_minutes) + + for mode in ("exact", "shortest"): + add(f"grisu-{mode}-cached-power-39", "probe", [ + f"{GRISU}::f64_cached_power_39::check_format_{mode}_opt" + ], 120 if mode == "shortest" else 60) + + for name, module, proof, kind in [ + ("division-contract", DRAGON, "check_div_2pow10_contract", "contract"), + ("limb-division-contract", DRAGON, "check_div_rem_digit_contract", "contract"), + ("bigint-small-division-contract", DRAGON, "check_div_rem_small_contract", "contract"), + ("rounding-contract", "num::flt2dec::rounding_verify", "check_round_up_contract", "contract"), + ("grisu-exact-rounding-contract", GRISU, "check_round_exact_contract", "contract"), + ("grisu-shortest-rounding-contract", GRISU, "check_round_shortest_contract", "contract"), + ("comparison-equivalence", DRAGON, "check_comparison_models_agree", "equivalence"), + ("addition-equivalence", DRAGON, "check_add_model_agrees", "equivalence"), + ("subtraction-equivalence", DRAGON, "check_sub_model_agrees", "equivalence"), + ("bit-scan-equivalence", "num::flt2dec::bit_scan_verify", "check_leading_zeros_models_agree", "equivalence"), + ]: + add(name, kind, [f"{module}::{proof}"], 30) + + for first in range(0, 40, 8): + add(f"small-multiplication-equivalence-{first:02d}-{first + 7:02d}", "equivalence", [ + f"{DRAGON}::check_mul_small_model_agrees_{size:02d}" + for size in range(first, first + 8) + ], 30) + + for first in range(0, 65, 8): + last = min(first + 7, 64) + add(f"estimator-equivalence-{first:02d}-{last:02d}", "equivalence", [ + f"num::flt2dec::estimator_verify::check_estimator_model_agrees_{bits:02d}" + for bits in range(first, last + 1) + ], 30) + return groups + + +def remaining_harnesses(inventory): + if inventory.get("file-version") != "0.1": + raise ValueError("Expected kani-list.json file-version 0.1") + listed = [ + harness + for section in ("standard-harnesses", "contract-harnesses") + for harnesses in inventory[section].values() + for harness in harnesses + ] + dedicated = {harness for group in proof_groups() for harness in group["harnesses"]} + missing = dedicated.difference(listed) + if missing: + raise ValueError("Dedicated flt2dec harnesses missing from kani list: " + ", ".join(sorted(missing))) + # Keep unrecognized harnesses, including future flt2dec proofs, in the general suite. + # Preserve the original list order and duplicates outside the dedicated catalog. + return [harness for harness in listed if harness not in dedicated] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + mode = parser.add_mutually_exclusive_group(required=True) + mode.add_argument("--matrix", action="store_true") + mode.add_argument("--group", choices=[group["name"] for group in proof_groups()]) + mode.add_argument("--remaining", metavar="KANI_LIST_JSON") + args = parser.parse_args() + if args.matrix: + print(json.dumps({"os": OPERATING_SYSTEMS, "group": proof_groups()}, separators=(",", ":"))) + elif args.group: + group = next(group for group in proof_groups() if group["name"] == args.group) + print("\n".join(group["harnesses"])) + else: + try: + with open(args.remaining, encoding="utf-8") as source: + remaining = remaining_harnesses(json.load(source)) + except (OSError, ValueError, KeyError, TypeError) as error: + parser.error(str(error)) + if remaining: + print("\n".join(remaining)) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/kani-std-analysis/log_parser.py b/scripts/kani-std-analysis/log_parser.py index 8f25ffea614e0..244ba018495f3 100755 --- a/scripts/kani-std-analysis/log_parser.py +++ b/scripts/kani-std-analysis/log_parser.py @@ -1,7 +1,7 @@ #!/usr/bin/env python3 """ -Parse log file of multi-threaded Kani run (terse output) into JSON. +Parse log file of a Kani run (terse output) into JSON. Given a run of Kani on the standard library with `--jobs= --output-format=terse` (and, typically, `autoharness`) enabled this produces a machine-processable JSON result via @@ -465,7 +465,7 @@ def parse_autoharness_info(lines, i): def parse_log_lines( lines, contract_harnesses, standard_harnesses, scanner_data): - """Parse (terse) output from multi-threaded Kani run while considering list + """Parse (terse) output from a Kani run while considering list and scanner data.""" # Regular expressions for matching patterns start_work_autoharness_contract_pattern = re.compile( @@ -485,6 +485,7 @@ def parse_log_lines( active_threads = {} # thread_id -> list of result lines all_results = [] thread_id = None + autoharness_info = {} i = 0 while i < len(lines): @@ -494,6 +495,13 @@ def parse_log_lines( line = lines[i].rstrip() i += 1 + # A single worker omits thread labels, including the result marker. + # Associate its output with thread 0 from the start of the harness. + if line.startswith(('Checking harness ', + 'Autoharness: Checking function ')): + line = f'Thread 0: {line}' + thread_id = 0 + # Check if a thread is starting work if start_match := start_work_autoharness_contract_pattern.search(line): init_entry( diff --git a/scripts/kani-std-analysis/test_flt2dec_harnesses.py b/scripts/kani-std-analysis/test_flt2dec_harnesses.py new file mode 100644 index 0000000000000..aa3fb9c82a9d0 --- /dev/null +++ b/scripts/kani-std-analysis/test_flt2dec_harnesses.py @@ -0,0 +1,69 @@ +import unittest + +from flt2dec_harnesses import OPERATING_SYSTEMS, proof_groups, remaining_harnesses + + +class Flt2decHarnessesTests(unittest.TestCase): + def setUp(self): + self.groups = proof_groups() + self.dedicated = [harness for group in self.groups for harness in group["harnesses"]] + self.inventory = { + "file-version": "0.1", + "standard-harnesses": {"generators": self.dedicated[:144]}, + "contract-harnesses": {"other": self.dedicated[144:]}, + } + + def test_complete_disjoint_batches_on_both_platforms(self): + self.assertEqual(OPERATING_SYSTEMS, ["ubuntu-latest", "macos-latest"]) + self.assertEqual(len(self.groups), 75) + self.assertEqual(len({group["name"] for group in self.groups}), 75) + self.assertEqual(len(self.dedicated), 265) + self.assertEqual(len(set(self.dedicated)), 265) + self.assertLessEqual(len(self.groups) * len(OPERATING_SYSTEMS), 256) + for group in self.groups: + minutes = group["timeout_minutes"] + with self.subTest(group=group["name"]): + self.assertTrue(group["harnesses"]) + self.assertIn(minutes, (30, 60, 120)) + self.assertLessEqual(minutes * len(group["harnesses"]), 240) + + def test_all_float_partitions_and_equivalence_cases_remain(self): + generators = [group for group in self.groups if group["kind"].startswith("generator-")] + self.assertEqual(sum(len(group["harnesses"]) for group in generators), 144) + for family in ("dragon-exact", "dragon-shortest", "grisu-exact", "grisu-shortest"): + targets = [harness for group in generators if group["name"].startswith(family + "-") + for harness in group["harnesses"]] + partitions = {harness.split("::")[-2] for harness in targets} + self.assertEqual(partitions, {f"f32_{i:02d}" for i in range(4)} | + {f"f64_{i:02d}" for i in range(32)}) + cases = [harness for group in self.groups if group["name"].startswith("estimator-") + for harness in group["harnesses"]] + self.assertEqual({int(harness.rsplit("_", 1)[1]) for harness in cases}, set(range(65))) + multiplication = [harness for group in self.groups + if group["name"].startswith("small-multiplication-") + for harness in group["harnesses"]] + self.assertEqual({int(harness.rsplit("_", 1)[1]) for harness in multiplication}, set(range(40))) + + def test_only_exact_catalog_names_are_removed(self): + retained = ["num::flt2dec::check_wrapper", "num::flt2dec::check_future_proof", + self.dedicated[0] + "_extra", "unrelated::proof", "unrelated::proof"] + self.inventory["standard-harnesses"]["retained"] = retained[:3] + self.inventory["contract-harnesses"]["retained"] = retained[3:] + self.assertEqual(remaining_harnesses(self.inventory), retained) + + def test_missing_dedicated_harness_fails(self): + self.inventory["standard-harnesses"]["generators"].pop() + with self.assertRaisesRegex(ValueError, "Dedicated flt2dec harnesses missing"): + remaining_harnesses(self.inventory) + + def test_unknown_inventory_version_fails(self): + self.inventory["file-version"] = "0.2" + with self.assertRaisesRegex(ValueError, "file-version 0.1"): + remaining_harnesses(self.inventory) + + def test_empty_remaining_inventory(self): + self.assertEqual(remaining_harnesses(self.inventory), []) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/kani-std-analysis/test_log_parser.py b/scripts/kani-std-analysis/test_log_parser.py new file mode 100644 index 0000000000000..f7d1f7e24071e --- /dev/null +++ b/scripts/kani-std-analysis/test_log_parser.py @@ -0,0 +1,102 @@ +import unittest + +from log_parser import parse_log_lines + + +class ParseLogLinesTests(unittest.TestCase): + def test_serial_manual_success_failure_and_timeout(self): + lines = """Checking harness successful... +VERIFICATION RESULT: + ** 0 of 2 failed +VERIFICATION:- SUCCESSFUL +Verification Time: 1s +Checking harness failed... +VERIFICATION RESULT: + ** 1 of 5 failed +Failed Checks: pointer dereference +VERIFICATION:- FAILED +Verification Time: 2s +Checking harness timed_out... +VERIFICATION:- TIMEOUT +CBMC timed out. +""".splitlines() + results = parse_log_lines(lines, {}, {}, {}) + self.assertEqual([entry['thread_id'] for entry in results], [0, 0, 0]) + self.assertEqual( + [entry['result']['harness'] for entry in results], + ['successful', 'failed', 'timed_out']) + self.assertEqual( + [entry['result']['result'] for entry in results], + ['SUCCESSFUL', 'FAILED', 'TIMEOUT']) + self.assertEqual( + [entry['result']['time'] for entry in results], ['1s', '2s', 'TO']) + self.assertEqual(results[0]['result']['n_failed_properties'], 0) + self.assertEqual(results[1]['result']['n_failed_properties'], 1) + self.assertEqual(results[1]['result']['n_total_properties'], 5) + self.assertIn('Failed Checks: pointer dereference', + results[1]['result']['output']) + self.assertIsNone(results[2]['result']['n_failed_properties']) + + def test_parallel_results_can_finish_out_of_order(self): + lines = """Thread 0: Checking harness first... +Thread 1: Checking harness second... +Thread 1: +VERIFICATION RESULT: + ** 1 of 5 failed +VERIFICATION:- FAILED +Verification Time: 2s +Thread 0: +VERIFICATION RESULT: + ** 0 of 2 failed +VERIFICATION:- SUCCESSFUL +Verification Time: 3s +""".splitlines() + results = parse_log_lines(lines, {}, {}, {}) + self.assertEqual([entry['thread_id'] for entry in results], [1, 0]) + self.assertEqual(results[0]['result']['harness'], 'second') + self.assertEqual(results[0]['result']['result'], 'FAILED') + self.assertEqual(results[0]['result']['n_failed_properties'], 1) + self.assertEqual(results[1]['result']['harness'], 'first') + self.assertEqual(results[1]['result']['result'], 'SUCCESSFUL') + self.assertEqual(results[1]['result']['time'], '3s') + + def test_serial_autoharness_results_match_threaded_results(self): + header = """Kani generated automatic harnesses for 1 functions ++--+ +| Crate | Selected Function | ++==+ +| core | example | ++--+ +Kani did not generate automatic harnesses for 0 functions ++--+ +| Crate | Skipped Function | Reason | ++==+ ++--+ +""" + metadata = {'example': { + 'crate': 'core', 'function': 'example', 'target_safeness': 'safe', + 'public_target': True, 'file_name': 'example.rs'}} + for contract in ['', "'s contract"]: + with self.subTest(contract=contract): + start = (f'Autoharness: Checking function example{contract} ' + 'against all possible inputs...\n') + result = ('VERIFICATION RESULT:\n ** 0 of 2 failed\n' + 'VERIFICATION:- SUCCESSFUL\nVerification Time: 1s\n') + serial = parse_log_lines( + (header + start + result).splitlines(), {}, metadata, {}) + threaded = parse_log_lines( + (header + 'Thread 0: ' + start + 'Thread 0:\n' + result) + .splitlines(), {}, metadata, {}) + self.assertEqual(serial, threaded) + self.assertEqual(len(serial), 1) + self.assertTrue(serial[0]['result']['is_autoharness']) + self.assertEqual(serial[0]['result']['with_contract'], + bool(contract)) + + def test_incomplete_serial_harness_is_rejected(self): + with self.assertRaises(AssertionError): + parse_log_lines(['Checking harness incomplete...'], {}, {}, {}) + + +if __name__ == '__main__': + unittest.main() diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 72c08b984ead9..b654dce4f9a73 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -14,7 +14,17 @@ usage() { } # Initialize variables +# Generator proofs need more objects; helper jobs can select a smaller capacity. declare -a command_args +kani_object_bits="${KANI_OBJECT_BITS:-14}" +# Optional encoding experiments preserve the verification checks and bounds. +kani_cbmc_args=(--object-bits "$kani_object_bits") +if [[ "${KANI_SYMEX_CACHE_DEREFERENCES:-false}" == true ]]; then + kani_cbmc_args+=(--symex-cache-dereferences) +fi +if [[ "${KANI_ARRAY_FIELD_SENSITIVITY:-true}" == false ]]; then + kani_cbmc_args+=(--no-array-field-sensitivity) +fi path="" run_command="verify-std" with_autoharness="false" @@ -192,11 +202,20 @@ get_harnesses() { fi # Extract the harnesses inside "standard-harnesses" and "contract-harnesses" # into an array called ALL_HARNESSES and the length of that array into HARNESS_COUNT - ALL_HARNESSES=($(jq -r ' - ([.["standard-harnesses"] | to_entries | .[] | .value[]] + - [.["contract-harnesses"] | to_entries | .[] | .value[]]) | - .[] - ' $WORK_DIR/kani-list.json)) + if [[ "${KANI_SEPARATE_FLT2DEC:-false}" == true ]]; then + # Dedicated jobs verify these exact names on both operating systems. + # Fail if any expected target is absent instead of silently dropping it. + local remaining_harnesses + remaining_harnesses=$(python3 -I "$WORK_DIR/scripts/kani-std-analysis/flt2dec_harnesses.py" \ + --remaining "$WORK_DIR/kani-list.json") + ALL_HARNESSES=($remaining_harnesses) + else + ALL_HARNESSES=($(jq -r ' + ([.["standard-harnesses"] | to_entries | .[] | .value[]] + + [.["contract-harnesses"] | to_entries | .[] | .value[]]) | + .[] + ' "$WORK_DIR/kani-list.json")) + fi HARNESS_COUNT=${#ALL_HARNESSES[@]} } @@ -204,7 +223,12 @@ get_harnesses() { run_verification_subset() { local kani_path="$1" local harnesses=("${@:2}") # All arguments after kani_path are harness names - + + if (( ${#harnesses[@]} == 0 )); then + echo "No harnesses assigned to this partition." + return + fi + # Build the --harness arguments local harness_args="" for harness in "${harnesses[@]}"; do @@ -213,21 +237,15 @@ run_verification_subset() { echo "Running verification for harnesses:" printf '%s\n' "${harnesses[@]}" - # Use KANI_JOBS to cap the number of parallel harnesses; some harnesses peak - # at close to 10 GB of memory, so running one per core can exhaust the - # memory of smaller CI runners (e.g., 4-core/16 GB ubuntu-latest). - local jobs_arg="-j" - if [[ -n "${KANI_JOBS:-}" ]]; then - jobs_arg="--jobs=${KANI_JOBS}" - fi + # Honor KANI_JOBS and default to one verifier per runner. "$kani_path" verify-std -Z unstable-options ./library \ $unstable_args \ --no-assert-contracts \ $harness_args --exact \ - $jobs_arg \ + --jobs "${KANI_JOBS:-1}" \ --output-format=terse \ "${command_args[@]}" \ - --cbmc-args --object-bits 12 + --cbmc-args "${kani_cbmc_args[@]}" } # Check if binary exists and is up to date @@ -308,7 +326,7 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - --cbmc-args --object-bits 12 + --cbmc-args "${kani_cbmc_args[@]}" fi elif [[ "$run_command" == "autoharness" ]]; then # Run verification for a subset of automatically generated harnesses @@ -318,7 +336,7 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - --cbmc-args --object-bits 12 + --cbmc-args "${kani_cbmc_args[@]}" elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." if [[ "$with_autoharness" == "true" ]]; then @@ -353,7 +371,7 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - --cbmc-args --object-bits 12 + --cbmc-args "${kani_cbmc_args[@]}" # remove metadata file for Kani-generated "dummy" crate that we won't # get scanner data for local target=$(find "target/kani_verify_std/target/" -mindepth 1 \