From 5456714c5dd952ec8cade50adff6f0c09ce03fdb Mon Sep 17 00:00:00 2001 From: Matt Borland Date: Tue, 9 Jun 2026 10:54:30 -0400 Subject: [PATCH 1/3] Add floats theorem --- test/theorems/floats.why | 743 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 743 insertions(+) create mode 100644 test/theorems/floats.why diff --git a/test/theorems/floats.why b/test/theorems/floats.why new file mode 100644 index 0000000..7d85357 --- /dev/null +++ b/test/theorems/floats.why @@ -0,0 +1,743 @@ +(* + * Formal Verification of Floating-Point Error Classification + * for Boost.SafeNumbers + * + * Copyright 2026 Matt Borland + * Distributed under the Boost Software License, Version 1.0. + * https://www.boost.org/LICENSE_1_0.txt + * + * This file formally proves the correctness of the error classification + * performed by the floating-point operations (+, -, *, /) and the + * comparison operators of Boost.SafeNumbers. The C++ implementation is in: + * + * include/boost/safe_numbers/detail/float_basis.hpp + * + * with f32 = detail::float_basis and f64 = detail::float_basis + * (floats.hpp lines 10-17). + * + * Each checked operation runs the native IEEE-754 operation and then + * classifies the result and operands into error_category + * (float_basis.hpp lines 494-502): + * + * no_error, overflow, underflow, divide_by_zero, nan_op, invalid_op + * + * We model the control flow of these classifiers branch for branch: + * + * checked_float_addition lines 525-561 + * checked_float_subtraction lines 773-809 + * checked_float_multiplication lines 1027-1063 + * checked_float_division lines 1285-1337 + * + * following IEEE-754-2008 sections 6.1 (infinity arithmetic), 6.2 (NaN + * operands), 7.2 (invalid operations) and 7.3 (divideByZero). The native + * result res is modeled by the Why3 standard library operation + * add/sub/mul/div in mode RNE, because the C++ uses the default + * round-to-nearest rounding. The IEEE special-value behavior is supplied + * by the ieee_float standard library axioms (add_special, add_finite, ...). + * We therefore prove the classifier against the standard library and, for + * the native float types < float 8 24 > and < float 11 53 >, against the + * SMT-LIB floating-point theory used by Z3 and Alt-Ergo, rather than against + * a hand-written specification. + * + * Modeling notes (the bridge to the C++ is established by inspection, the + * same way the integer proofs connect to their basis headers): + * - constexpr_isinf v corresponds to is_infinite v + * - constexpr_isnan v corresponds to is_nan v + * - is_true_zero v corresponds to is_zero v (this assumes the + * platform does not flush denormals to zero; the C++ is_true_zero + * handles DAZ by bit inspection, which is outside this real-number model) + * - the C++ test res > 0 on an infinite res corresponds to is_positive res + * - signaling NaN: ieee_float has no signaling concept, so is_signaling is + * an abstract predicate refining is_nan (axiom is_signaling x -> is_nan + * x). The faithfulness of the bit-level constexpr_issignaling to this + * abstraction is checked by the C++ unit tests, not here. + * + * Naming: the library category "underflow" means the result saturates to + * negative infinity (negative overflow); it is NOT IEEE-754 tininess. + * Gradual underflow to a subnormal or zero is finite and classifies as + * no_error. + * + * Because ieee_float.Float32 and ieee_float.Float64 are both instances of + * GenericFloat, the two theories below (Float32Checks and Float64Checks) are + * textually identical apart from the imported format, and cover f32 and f64 + * respectively. + * + * Verification: all 86 lemmas (43 for each of f32 and f64) are proved using + * two complementary provers: + * - Alt-Ergo 2.4.3: proves 86/86 (slowest goal about 4.4s) + * - Z3 4.15.4: proves 60/86 + * Alt-Ergo discharges every goal. Z3 proves all of the floating-point + * classification goals natively but times out on the real-number bridge + * lemmas (the soundness and correctness lemmas), whose round / no_overflow + * reasoning lies outside the SMT-LIB float theory. Every lemma is proved by + * at least one prover (zero gaps). + * + * why3 prove -P alt-ergo -t 10 -L theorems theorems/floats.why + * why3 prove -P z3 -t 30 -L theorems theorems/floats.why + *) + +(* ================================================================ + * Theory: Defs + * + * The result categories shared by every operation. category mirrors the + * C++ enum class error_category; ordering mirrors the four possible + * results of operator<=> (std::partial_ordering). + * ================================================================ *) +theory Defs + + type category = NoError | Overflow | Underflow | DivByZero | NanOp | InvalidOp + + type ordering = Less | Greater | Equivalent | Unordered + +end + +(* ================================================================ + * Theory: Float32Checks + * + * Classification proofs for f32 = float_basis, modeled on + * ieee_float.Float32 (the IEEE-754 binary32 format, < float 8 24 >). + * ================================================================ *) +theory Float32Checks + + use Defs + use real.RealInfix + use ieee_float.Float32 + + (* Float32 substitutes is_finite and to_real by the built-in projections of + * the < float 8 24 > type when it clones GenericFloat, so those two names + * are not exposed (unlike is_nan, is_zero, ...). Reintroduce them. *) + function to_real (x : t) : real = t'real x + predicate is_finite (x : t) = t'isFinite x + + (* ---- Signaling NaN abstraction ---- + * ieee_float does not model signaling NaNs. is_signaling is an abstract + * predicate that refines is_nan; this is all the classifier needs. *) + predicate is_signaling (x : t) + axiom signaling_is_nan : forall x : t. is_signaling x -> is_nan x + + (* ---- Classifiers modeling the C++ control flow ---- *) + + (* checked_float_addition, float_basis.hpp lines 525-561. + * 7.2.a signaling, 7.2.d addition of infinities of differing sign, + * 6.2 NaN operand, 6.1 saturation to +/- infinity. *) + function classify_add (x y : t) : category = + let r = add RNE x y in + if is_finite r then NoError + else if is_signaling x \/ is_signaling y then InvalidOp + else if is_infinite x /\ is_infinite y /\ diff_sign x y then InvalidOp + else if is_nan x \/ is_nan y then NanOp + else if is_positive r then Overflow + else Underflow + + (* checked_float_subtraction, float_basis.hpp lines 773-809. + * Differs from addition only in the infinity invalid case: subtraction + * of infinities of the SAME sign cancels to NaN. *) + function classify_sub (x y : t) : category = + let r = sub RNE x y in + if is_finite r then NoError + else if is_signaling x \/ is_signaling y then InvalidOp + else if is_infinite x /\ is_infinite y /\ same_sign x y then InvalidOp + else if is_nan x \/ is_nan y then NanOp + else if is_positive r then Overflow + else Underflow + + (* checked_float_multiplication, float_basis.hpp lines 1027-1063. + * 7.2.c multiplication of zero by an infinity in either order. *) + function classify_mul (x y : t) : category = + let r = mul RNE x y in + if is_finite r then NoError + else if is_signaling x \/ is_signaling y then InvalidOp + else if (is_zero x /\ is_infinite y) \/ (is_infinite x /\ is_zero y) then InvalidOp + else if is_nan x \/ is_nan y then NanOp + else if is_positive r then Overflow + else Underflow + + (* checked_float_division, float_basis.hpp lines 1285-1337. + * 7.2.b 0/0 and inf/inf, then 7.3 finite-nonzero / zero. *) + function classify_div (x y : t) : category = + let r = div RNE x y in + if is_finite r then NoError + else if is_signaling x \/ is_signaling y then InvalidOp + else if is_zero x /\ is_zero y then InvalidOp + else if is_infinite x /\ is_infinite y then InvalidOp + else if is_zero y /\ not (is_infinite x) /\ not (is_nan x) then DivByZero + else if is_nan x \/ is_nan y then NanOp + else if is_positive r then Overflow + else Underflow + + (* ---- Comparison modeling operator<=> ---- *) + + function compare (x y : t) : ordering = + if is_nan x \/ is_nan y then Unordered + else if lt x y then Less + else if gt x y then Greater + else Equivalent + + (* ================= Addition ================= *) + + (* The hot path fires exactly on a finite result. *) + lemma add_no_error_iff : + forall x y : t. classify_add x y = NoError <-> is_finite (add RNE x y) + + (* Saturation to +infinity is flagged as overflow, and only then. *) + lemma add_overflow_iff : + forall x y : t. classify_add x y = Overflow <-> is_plus_infinity (add RNE x y) + + (* Saturation to -infinity is flagged as underflow (negative overflow). *) + lemma add_underflow_iff : + forall x y : t. classify_add x y = Underflow <-> is_minus_infinity (add RNE x y) + + (* invalid_op fires exactly on a signaling operand or inf + (-inf). *) + lemma add_invalid_iff : + forall x y : t. + classify_add x y = InvalidOp <-> + (is_signaling x \/ is_signaling y \/ + (is_infinite x /\ is_infinite y /\ diff_sign x y)) + + (* nan_op fires exactly on a (quiet) NaN operand with no signaling. *) + lemma add_nan_op_iff : + forall x y : t. + classify_add x y = NanOp <-> + ((is_nan x \/ is_nan y) /\ not (is_signaling x) /\ not (is_signaling y)) + + (* Soundness against the reals: a genuine positive overflow of two finite + * operands is flagged as overflow. *) + lemma add_overflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x +. to_real y)) -> + (to_real x +. to_real y) >. 0.0 -> + classify_add x y = Overflow + + lemma add_underflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x +. to_real y)) -> + (to_real x +. to_real y) <. 0.0 -> + classify_add x y = Underflow + + (* No false positive: finite operands whose exact sum is representable + * are not flagged. *) + lemma add_finite_no_error : + forall x y : t. + is_finite x -> is_finite y -> + no_overflow RNE (to_real x +. to_real y) -> + classify_add x y = NoError + + (* Correctness: when not flagged, the result is the correctly rounded sum. *) + lemma add_correctness : + forall x y : t. + is_finite x -> is_finite y -> + no_overflow RNE (to_real x +. to_real y) -> + to_real (add RNE x y) = round RNE (to_real x +. to_real y) + + (* ================= Subtraction ================= *) + + lemma sub_no_error_iff : + forall x y : t. classify_sub x y = NoError <-> is_finite (sub RNE x y) + + lemma sub_overflow_iff : + forall x y : t. classify_sub x y = Overflow <-> is_plus_infinity (sub RNE x y) + + lemma sub_underflow_iff : + forall x y : t. classify_sub x y = Underflow <-> is_minus_infinity (sub RNE x y) + + lemma sub_invalid_iff : + forall x y : t. + classify_sub x y = InvalidOp <-> + (is_signaling x \/ is_signaling y \/ + (is_infinite x /\ is_infinite y /\ same_sign x y)) + + lemma sub_nan_op_iff : + forall x y : t. + classify_sub x y = NanOp <-> + ((is_nan x \/ is_nan y) /\ not (is_signaling x) /\ not (is_signaling y)) + + lemma sub_overflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x -. to_real y)) -> + (to_real x -. to_real y) >. 0.0 -> + classify_sub x y = Overflow + + lemma sub_underflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x -. to_real y)) -> + (to_real x -. to_real y) <. 0.0 -> + classify_sub x y = Underflow + + lemma sub_correctness : + forall x y : t. + is_finite x -> is_finite y -> + no_overflow RNE (to_real x -. to_real y) -> + to_real (sub RNE x y) = round RNE (to_real x -. to_real y) + + (* ================= Multiplication ================= *) + + lemma mul_no_error_iff : + forall x y : t. classify_mul x y = NoError <-> is_finite (mul RNE x y) + + lemma mul_overflow_iff : + forall x y : t. classify_mul x y = Overflow <-> is_plus_infinity (mul RNE x y) + + lemma mul_underflow_iff : + forall x y : t. classify_mul x y = Underflow <-> is_minus_infinity (mul RNE x y) + + lemma mul_invalid_iff : + forall x y : t. + classify_mul x y = InvalidOp <-> + (is_signaling x \/ is_signaling y \/ + (is_zero x /\ is_infinite y) \/ (is_infinite x /\ is_zero y)) + + lemma mul_nan_op_iff : + forall x y : t. + classify_mul x y = NanOp <-> + ((is_nan x \/ is_nan y) /\ not (is_signaling x) /\ not (is_signaling y)) + + (* For multiplication the sign of the result follows the operand signs + * (product_sign), so the sound lemmas take same_sign / diff_sign as the + * sign condition. The bridge to the real product sign is the stdlib's + * same_sign_product and diff_sign_product. *) + lemma mul_overflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x *. to_real y)) -> + same_sign x y -> + classify_mul x y = Overflow + + lemma mul_underflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x *. to_real y)) -> + diff_sign x y -> + classify_mul x y = Underflow + + lemma mul_correctness : + forall x y : t. + is_finite x -> is_finite y -> + no_overflow RNE (to_real x *. to_real y) -> + to_real (mul RNE x y) = round RNE (to_real x *. to_real y) + + (* ================= Division ================= *) + + lemma div_no_error_iff : + forall x y : t. classify_div x y = NoError <-> is_finite (div RNE x y) + + lemma div_invalid_iff : + forall x y : t. + classify_div x y = InvalidOp <-> + (is_signaling x \/ is_signaling y \/ + (is_zero x /\ is_zero y) \/ (is_infinite x /\ is_infinite y)) + + (* divide_by_zero fires exactly on finite-nonzero / zero. *) + lemma div_divbyzero_iff : + forall x y : t. + classify_div x y = DivByZero <-> + (not (is_signaling x) /\ not (is_signaling y) /\ + is_finite x /\ not (is_zero x) /\ is_zero y) + + (* and that case produces an infinity. *) + lemma div_divbyzero_inf : + forall x y : t. + is_finite x -> not (is_zero x) -> is_zero y -> + is_infinite (div RNE x y) + + lemma div_nan_op_iff : + forall x y : t. + classify_div x y = NanOp <-> + ((is_nan x \/ is_nan y) /\ not (is_signaling x) /\ not (is_signaling y)) + + (* Overflow in division still implies a positive infinite result. The + * converse fails because finite-nonzero / zero is classified DivByZero, + * so we give the implication plus a soundness lemma rather than an iff. *) + lemma div_overflow_imp : + forall x y : t. classify_div x y = Overflow -> is_plus_infinity (div RNE x y) + + lemma div_underflow_imp : + forall x y : t. classify_div x y = Underflow -> is_minus_infinity (div RNE x y) + + (* As with multiplication, the quotient sign follows the operand signs. *) + lemma div_overflow_sound : + forall x y : t. + is_finite x -> is_finite y -> not (is_zero y) -> + not (no_overflow RNE (to_real x /. to_real y)) -> + same_sign x y -> + classify_div x y = Overflow + + lemma div_underflow_sound : + forall x y : t. + is_finite x -> is_finite y -> not (is_zero y) -> + not (no_overflow RNE (to_real x /. to_real y)) -> + diff_sign x y -> + classify_div x y = Underflow + + lemma div_correctness : + forall x y : t. + is_finite x -> is_finite y -> not (is_zero y) -> + no_overflow RNE (to_real x /. to_real y) -> + to_real (div RNE x y) = round RNE (to_real x /. to_real y) + + (* ================= Comparison ================= *) + + (* NaN compares unordered, and only NaN does. *) + lemma cmp_unordered_iff : + forall x y : t. compare x y = Unordered <-> (is_nan x \/ is_nan y) + + lemma cmp_less_iff : + forall x y : t. + compare x y = Less <-> (not (is_nan x) /\ not (is_nan y) /\ lt x y) + + lemma cmp_greater_iff : + forall x y : t. + compare x y = Greater <-> + (not (is_nan x) /\ not (is_nan y) /\ not (lt x y) /\ gt x y) + + lemma cmp_equiv_iff : + forall x y : t. + compare x y = Equivalent <-> + (not (is_nan x) /\ not (is_nan y) /\ not (lt x y) /\ not (gt x y)) + + (* operator== is the IEEE eq: false on any NaN, reflexive otherwise, and + * +0 == -0. *) + lemma eqeq_nan_false : + forall x y : t. (is_nan x \/ is_nan y) -> not (eq x y) + + lemma eqeq_refl_non_nan : + forall x : t. not (is_nan x) -> eq x x + + lemma eqeq_signed_zero : + forall x y : t. is_zero x -> is_zero y -> eq x y + + (* operator== and operator<=> agree on finite values. *) + lemma eq_iff_equivalent_finite : + forall x y : t. + is_finite x -> is_finite y -> (eq x y <-> compare x y = Equivalent) + +end + +(* ================================================================ + * Theory: Float64Checks + * + * Classification proofs for f64 = float_basis, modeled on + * ieee_float.Float64 (the IEEE-754 binary64 format, < float 11 53 >). + * Identical to Float32Checks apart from the imported format. + * ================================================================ *) +theory Float64Checks + + use Defs + use real.RealInfix + use ieee_float.Float64 + + (* Float64 substitutes is_finite and to_real by the built-in projections of + * the < float 11 53 > type when it clones GenericFloat, so those two names + * are not exposed (unlike is_nan, is_zero, ...). Reintroduce them. *) + function to_real (x : t) : real = t'real x + predicate is_finite (x : t) = t'isFinite x + + (* ---- Signaling NaN abstraction ---- + * ieee_float does not model signaling NaNs. is_signaling is an abstract + * predicate that refines is_nan; this is all the classifier needs. *) + predicate is_signaling (x : t) + axiom signaling_is_nan : forall x : t. is_signaling x -> is_nan x + + (* ---- Classifiers modeling the C++ control flow ---- *) + + (* checked_float_addition, float_basis.hpp lines 525-561. + * 7.2.a signaling, 7.2.d addition of infinities of differing sign, + * 6.2 NaN operand, 6.1 saturation to +/- infinity. *) + function classify_add (x y : t) : category = + let r = add RNE x y in + if is_finite r then NoError + else if is_signaling x \/ is_signaling y then InvalidOp + else if is_infinite x /\ is_infinite y /\ diff_sign x y then InvalidOp + else if is_nan x \/ is_nan y then NanOp + else if is_positive r then Overflow + else Underflow + + (* checked_float_subtraction, float_basis.hpp lines 773-809. + * Differs from addition only in the infinity invalid case: subtraction + * of infinities of the SAME sign cancels to NaN. *) + function classify_sub (x y : t) : category = + let r = sub RNE x y in + if is_finite r then NoError + else if is_signaling x \/ is_signaling y then InvalidOp + else if is_infinite x /\ is_infinite y /\ same_sign x y then InvalidOp + else if is_nan x \/ is_nan y then NanOp + else if is_positive r then Overflow + else Underflow + + (* checked_float_multiplication, float_basis.hpp lines 1027-1063. + * 7.2.c multiplication of zero by an infinity in either order. *) + function classify_mul (x y : t) : category = + let r = mul RNE x y in + if is_finite r then NoError + else if is_signaling x \/ is_signaling y then InvalidOp + else if (is_zero x /\ is_infinite y) \/ (is_infinite x /\ is_zero y) then InvalidOp + else if is_nan x \/ is_nan y then NanOp + else if is_positive r then Overflow + else Underflow + + (* checked_float_division, float_basis.hpp lines 1285-1337. + * 7.2.b 0/0 and inf/inf, then 7.3 finite-nonzero / zero. *) + function classify_div (x y : t) : category = + let r = div RNE x y in + if is_finite r then NoError + else if is_signaling x \/ is_signaling y then InvalidOp + else if is_zero x /\ is_zero y then InvalidOp + else if is_infinite x /\ is_infinite y then InvalidOp + else if is_zero y /\ not (is_infinite x) /\ not (is_nan x) then DivByZero + else if is_nan x \/ is_nan y then NanOp + else if is_positive r then Overflow + else Underflow + + (* ---- Comparison modeling operator<=> ---- *) + + function compare (x y : t) : ordering = + if is_nan x \/ is_nan y then Unordered + else if lt x y then Less + else if gt x y then Greater + else Equivalent + + (* ================= Addition ================= *) + + (* The hot path fires exactly on a finite result. *) + lemma add_no_error_iff : + forall x y : t. classify_add x y = NoError <-> is_finite (add RNE x y) + + (* Saturation to +infinity is flagged as overflow, and only then. *) + lemma add_overflow_iff : + forall x y : t. classify_add x y = Overflow <-> is_plus_infinity (add RNE x y) + + (* Saturation to -infinity is flagged as underflow (negative overflow). *) + lemma add_underflow_iff : + forall x y : t. classify_add x y = Underflow <-> is_minus_infinity (add RNE x y) + + (* invalid_op fires exactly on a signaling operand or inf + (-inf). *) + lemma add_invalid_iff : + forall x y : t. + classify_add x y = InvalidOp <-> + (is_signaling x \/ is_signaling y \/ + (is_infinite x /\ is_infinite y /\ diff_sign x y)) + + (* nan_op fires exactly on a (quiet) NaN operand with no signaling. *) + lemma add_nan_op_iff : + forall x y : t. + classify_add x y = NanOp <-> + ((is_nan x \/ is_nan y) /\ not (is_signaling x) /\ not (is_signaling y)) + + (* Soundness against the reals: a genuine positive overflow of two finite + * operands is flagged as overflow. *) + lemma add_overflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x +. to_real y)) -> + (to_real x +. to_real y) >. 0.0 -> + classify_add x y = Overflow + + lemma add_underflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x +. to_real y)) -> + (to_real x +. to_real y) <. 0.0 -> + classify_add x y = Underflow + + (* No false positive: finite operands whose exact sum is representable + * are not flagged. *) + lemma add_finite_no_error : + forall x y : t. + is_finite x -> is_finite y -> + no_overflow RNE (to_real x +. to_real y) -> + classify_add x y = NoError + + (* Correctness: when not flagged, the result is the correctly rounded sum. *) + lemma add_correctness : + forall x y : t. + is_finite x -> is_finite y -> + no_overflow RNE (to_real x +. to_real y) -> + to_real (add RNE x y) = round RNE (to_real x +. to_real y) + + (* ================= Subtraction ================= *) + + lemma sub_no_error_iff : + forall x y : t. classify_sub x y = NoError <-> is_finite (sub RNE x y) + + lemma sub_overflow_iff : + forall x y : t. classify_sub x y = Overflow <-> is_plus_infinity (sub RNE x y) + + lemma sub_underflow_iff : + forall x y : t. classify_sub x y = Underflow <-> is_minus_infinity (sub RNE x y) + + lemma sub_invalid_iff : + forall x y : t. + classify_sub x y = InvalidOp <-> + (is_signaling x \/ is_signaling y \/ + (is_infinite x /\ is_infinite y /\ same_sign x y)) + + lemma sub_nan_op_iff : + forall x y : t. + classify_sub x y = NanOp <-> + ((is_nan x \/ is_nan y) /\ not (is_signaling x) /\ not (is_signaling y)) + + lemma sub_overflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x -. to_real y)) -> + (to_real x -. to_real y) >. 0.0 -> + classify_sub x y = Overflow + + lemma sub_underflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x -. to_real y)) -> + (to_real x -. to_real y) <. 0.0 -> + classify_sub x y = Underflow + + lemma sub_correctness : + forall x y : t. + is_finite x -> is_finite y -> + no_overflow RNE (to_real x -. to_real y) -> + to_real (sub RNE x y) = round RNE (to_real x -. to_real y) + + (* ================= Multiplication ================= *) + + lemma mul_no_error_iff : + forall x y : t. classify_mul x y = NoError <-> is_finite (mul RNE x y) + + lemma mul_overflow_iff : + forall x y : t. classify_mul x y = Overflow <-> is_plus_infinity (mul RNE x y) + + lemma mul_underflow_iff : + forall x y : t. classify_mul x y = Underflow <-> is_minus_infinity (mul RNE x y) + + lemma mul_invalid_iff : + forall x y : t. + classify_mul x y = InvalidOp <-> + (is_signaling x \/ is_signaling y \/ + (is_zero x /\ is_infinite y) \/ (is_infinite x /\ is_zero y)) + + lemma mul_nan_op_iff : + forall x y : t. + classify_mul x y = NanOp <-> + ((is_nan x \/ is_nan y) /\ not (is_signaling x) /\ not (is_signaling y)) + + (* For multiplication the sign of the result follows the operand signs + * (product_sign), so the sound lemmas take same_sign / diff_sign as the + * sign condition. The bridge to the real product sign is the stdlib's + * same_sign_product and diff_sign_product. *) + lemma mul_overflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x *. to_real y)) -> + same_sign x y -> + classify_mul x y = Overflow + + lemma mul_underflow_sound : + forall x y : t. + is_finite x -> is_finite y -> + not (no_overflow RNE (to_real x *. to_real y)) -> + diff_sign x y -> + classify_mul x y = Underflow + + lemma mul_correctness : + forall x y : t. + is_finite x -> is_finite y -> + no_overflow RNE (to_real x *. to_real y) -> + to_real (mul RNE x y) = round RNE (to_real x *. to_real y) + + (* ================= Division ================= *) + + lemma div_no_error_iff : + forall x y : t. classify_div x y = NoError <-> is_finite (div RNE x y) + + lemma div_invalid_iff : + forall x y : t. + classify_div x y = InvalidOp <-> + (is_signaling x \/ is_signaling y \/ + (is_zero x /\ is_zero y) \/ (is_infinite x /\ is_infinite y)) + + (* divide_by_zero fires exactly on finite-nonzero / zero. *) + lemma div_divbyzero_iff : + forall x y : t. + classify_div x y = DivByZero <-> + (not (is_signaling x) /\ not (is_signaling y) /\ + is_finite x /\ not (is_zero x) /\ is_zero y) + + (* and that case produces an infinity. *) + lemma div_divbyzero_inf : + forall x y : t. + is_finite x -> not (is_zero x) -> is_zero y -> + is_infinite (div RNE x y) + + lemma div_nan_op_iff : + forall x y : t. + classify_div x y = NanOp <-> + ((is_nan x \/ is_nan y) /\ not (is_signaling x) /\ not (is_signaling y)) + + (* Overflow in division still implies a positive infinite result. The + * converse fails because finite-nonzero / zero is classified DivByZero, + * so we give the implication plus a soundness lemma rather than an iff. *) + lemma div_overflow_imp : + forall x y : t. classify_div x y = Overflow -> is_plus_infinity (div RNE x y) + + lemma div_underflow_imp : + forall x y : t. classify_div x y = Underflow -> is_minus_infinity (div RNE x y) + + (* As with multiplication, the quotient sign follows the operand signs. *) + lemma div_overflow_sound : + forall x y : t. + is_finite x -> is_finite y -> not (is_zero y) -> + not (no_overflow RNE (to_real x /. to_real y)) -> + same_sign x y -> + classify_div x y = Overflow + + lemma div_underflow_sound : + forall x y : t. + is_finite x -> is_finite y -> not (is_zero y) -> + not (no_overflow RNE (to_real x /. to_real y)) -> + diff_sign x y -> + classify_div x y = Underflow + + lemma div_correctness : + forall x y : t. + is_finite x -> is_finite y -> not (is_zero y) -> + no_overflow RNE (to_real x /. to_real y) -> + to_real (div RNE x y) = round RNE (to_real x /. to_real y) + + (* ================= Comparison ================= *) + + (* NaN compares unordered, and only NaN does. *) + lemma cmp_unordered_iff : + forall x y : t. compare x y = Unordered <-> (is_nan x \/ is_nan y) + + lemma cmp_less_iff : + forall x y : t. + compare x y = Less <-> (not (is_nan x) /\ not (is_nan y) /\ lt x y) + + lemma cmp_greater_iff : + forall x y : t. + compare x y = Greater <-> + (not (is_nan x) /\ not (is_nan y) /\ not (lt x y) /\ gt x y) + + lemma cmp_equiv_iff : + forall x y : t. + compare x y = Equivalent <-> + (not (is_nan x) /\ not (is_nan y) /\ not (lt x y) /\ not (gt x y)) + + (* operator== is the IEEE eq: false on any NaN, reflexive otherwise, and + * +0 == -0. *) + lemma eqeq_nan_false : + forall x y : t. (is_nan x \/ is_nan y) -> not (eq x y) + + lemma eqeq_refl_non_nan : + forall x : t. not (is_nan x) -> eq x x + + lemma eqeq_signed_zero : + forall x y : t. is_zero x -> is_zero y -> eq x y + + (* operator== and operator<=> agree on finite values. *) + lemma eq_iff_equivalent_finite : + forall x y : t. + is_finite x -> is_finite y -> (eq x y <-> compare x y = Equivalent) + +end From e0837b1b89993206af20ef5b83e5b85223a05beb Mon Sep 17 00:00:00 2001 From: Matt Borland Date: Tue, 9 Jun 2026 13:37:40 -0400 Subject: [PATCH 2/3] Significant simplifications using the why3 stdlib --- test/theorems/unsigned_integers.why | 1630 +++------------------------ 1 file changed, 145 insertions(+), 1485 deletions(-) diff --git a/test/theorems/unsigned_integers.why b/test/theorems/unsigned_integers.why index bce3b28..185d881 100644 --- a/test/theorems/unsigned_integers.why +++ b/test/theorems/unsigned_integers.why @@ -6,1545 +6,205 @@ * Distributed under the Boost Software License, Version 1.0. * https://www.boost.org/LICENSE_1_0.txt * - * This file formally proves the correctness of all five unsigned - * arithmetic operations (+, -, *, /, %) in Boost.SafeNumbers. - * The C++ implementation is in: + * This file formally proves the correctness of all five unsigned arithmetic + * operations (+, -, *, /, %) in Boost.SafeNumbers. The C++ implementation is + * in: * * include/boost/safe_numbers/detail/unsigned_integer_basis.hpp * - * The portable overflow detection for addition (lines 184-197) is: - * - * result = static_cast(lhs + rhs); // wrapping addition - * return result < lhs; // overflow detection - * - * The portable underflow detection for subtraction (lines 570-583) is: - * - * result = static_cast(lhs - rhs); // wrapping subtraction - * return result > lhs; // underflow detection - * - * Multiplication overflow detection uses two strategies: - * - * 1. Wide multiplication (u8-u64, lines 842-852): - * Promote to 2N-bit type, compute exact product, check temp > max(T). - * - * 2. Division check (u128, lines 854-858): - * return rhs != 0 && lhs > max(uint128) / rhs; - * - * We model these as: given N-bit unsigned values a, b in [0, 2^N - 1], - * the wrapping result is (a op b) mod 2^N, and overflow/underflow is - * detected by comparing the result against a (for add/sub) or using - * the division check (for mul). - * - * The default operator+ (line 391-395) throws std::overflow_error. - * The default operator- (line 762-766) throws std::underflow_error. - * The default operator* (line 1046-1050) throws std::overflow_error. - * The default operator/ (line 1201-1205) throws std::domain_error on div-by-zero. - * The default operator% (line 1356-1360) throws std::domain_error on mod-by-zero. - * - * The connection between this Why3 model and the C++ code is established - * by inspection: C++ unsigned arithmetic wraps modulo 2^N by definition - * (C++ [basic.fundamental]/4), and the comparison result < lhs is a - * standard unsigned comparison. - * - * Verification: All 168 lemmas are proved using two complementary provers: - * - Alt-Ergo 2.4.3: proves 160/168 - * - Z3 4.15.4: proves 131/168 - * Every lemma is proved by at least one prover (zero gaps). + * Rather than re-deriving modular arithmetic by hand, this proof models the + * unsigned types directly with the Why3 standard library bitvector theory + * (bv.BV8/16/32/64/128). Those modules already provide everything the C++ + * relies on, mapped onto the native SMT-LIB bitvector theory: + * + * C++ / safe_numbers concept Why3 bv.BV_Gen + * -------------------------- -------------- + * the N-bit value as an integer to_uint : t -> int (0 <= . < 2^N) + * 2^N, max value 2^N - 1 two_power_size, max_int + * wrapping lhs + rhs add (to_uint_add: mod 2^N) + * wrapping lhs - rhs sub (to_uint_sub: mod 2^N) + * wrapping lhs * rhs mul (to_uint_mul: mod 2^N) + * unsigned <, > ult, ugt + * lhs / rhs, lhs % rhs udiv, urem + * + * The portable overflow detection for addition is result < lhs, modeled as + * ult (add a b) a. The underflow detection for subtraction is result > lhs, + * modeled as ugt (sub a b) a. Multiplication overflow is detected either by + * the u128 division check (rhs != 0 && lhs > max / rhs) or by the u8-u64 + * wide-multiplication (the exact product fits in 2N bits); both are proved. + * + * The generic theory UnsignedOverflow clones the abstract bv.BV_Gen, so a + * single proof covers every bit width N >= 1, hence all of u8, u16, u32, + * u64, u128 (= bv.BV8/16/32/64/128) at once. The per-width theories below + * add concrete boundary witnesses for the individual C++ types. + * + * Verification: all 40 lemmas are proved using two complementary provers: + * - Alt-Ergo 2.4.3: proves 39/40 + * - Z3 4.15.4: proves the nonlinear product bound (prod_lt_sq) + * Every lemma is proved by at least one prover (zero gaps). Alt-Ergo is the + * workhorse; Z3 supplies the one nonlinear-arithmetic goal Alt-Ergo cannot. * * why3 prove -P alt-ergo -t 10 -L theorems theorems/unsigned_integers.why * why3 prove -P z3 -t 30 -L theorems theorems/unsigned_integers.why *) (* ================================================================ - * Theory: PowerOfTwo + * Theory: IntLemmas * - * Step-by-step computation of power 2 N for specific bit widths. - * Automated provers struggle to unfold the recursive definition of - * power more than a few levels. This theory provides a doubling - * chain: each step uses Power_sum to derive power 2 (2*k) from - * (power 2 k)^2, giving the provers concrete values to work with. + * Pure-integer nonlinear facts the SMT provers need stated explicitly + * (multiplication and Euclidean-division reasoning). These guide the + * multiplication-overflow proofs below. * ================================================================ *) -theory PowerOfTwo +theory IntLemmas use int.Int - use int.Power - - (* Base cases: direct unfolding of the Power_s axiom *) - lemma p2_1: power 2 1 = 2 - lemma p2_2: power 2 2 = 4 - lemma p2_4: power 2 4 = 16 - - (* Doubling via Power_sum: power 2 (n+n) = power 2 n * power 2 n *) - lemma p2_8: power 2 8 = 256 - lemma p2_16: power 2 16 = 65536 - lemma p2_32: power 2 32 = 4294967296 - lemma p2_64: power 2 64 = 18446744073709551616 - lemma p2_128: power 2 128 = 340282366920938463463374607431768211456 - -end - -(* ================================================================ - * Theory: UnsignedAddOverflow - * - * Parametric proofs over an arbitrary bit-width N >= 1. - * All four main properties are proved: - * 1. Soundness -- overflow implies detection - * 2. No false positives -- no overflow implies no detection - * 3. Correctness -- no overflow implies exact result - * 4. Biconditional -- detection iff overflow - * ================================================================ *) -theory UnsignedAddOverflow - - use int.Int - use int.Power use int.EuclideanDivision - (* ---- Definitions modeling the C++ implementation ---- *) - - (* The modulus for an N-bit unsigned type: M = 2^N *) - function modulus (n: int) : int = power 2 n + (* Product of two values each in [0, m) is below m*m: justifies the + * u8-u64 wide-multiply (the exact product fits in a 2N-bit type). *) + lemma prod_lt_sq : + forall a b m : int. 0 <= a < m -> 0 <= b < m -> a * b < m * m - (* The maximum representable value for an N-bit unsigned type *) - function max_val (n: int) : int = power 2 n - 1 + (* Euclidean division bracketing: q*d <= n < (q+1)*d for d > 0. *) + lemma euclid_q : + forall n d : int. d > 0 -> (div n d) * d <= n < ((div n d) + 1) * d - (* Whether a value is a valid N-bit unsigned integer *) - predicate valid (x: int) (n: int) = - 0 <= x /\ x <= max_val n - - (* The wrapping addition result: (a + b) mod 2^N - * Models: result = static_cast(lhs + rhs) - * Reference: unsigned_integer_basis.hpp line 193 *) - function wrap_add (a b: int) (n: int) : int = - mod (a + b) (modulus n) - - (* The overflow detection predicate: result < lhs - * Models: return result < lhs - * Reference: unsigned_integer_basis.hpp line 196 *) - predicate detected (a b: int) (n: int) = - wrap_add a b n < a - - (* True mathematical overflow: a + b exceeds the representable range *) - predicate overflows (a b: int) (n: int) = - a + b > max_val n - - (* ---- Helper lemmas ---- *) - - (* These intermediate lemmas guide the automated provers (Alt-Ergo, Z3, - * CVC5) through the key steps of the reasoning. The central insight is - * that when adding two N-bit values, the true sum lies in - * [0, 2*(2^N - 1)] = [0, 2^(N+1) - 2], which is strictly less than - * 2 * 2^N. Therefore the sum wraps at most once, and mod behaves in - * one of exactly two ways: - * - * Case 1 (no overflow): 0 <= a+b < 2^N ==> mod(a+b, 2^N) = a+b - * Case 2 (overflow): 2^N <= a+b ==> mod(a+b, 2^N) = a+b - 2^N - *) - - (* Lemma: 2^N > 0 for any N >= 1. Required by mod properties. *) - lemma power_pos: - forall n: int. n >= 1 -> power 2 n > 0 - - (* Lemma: For valid N-bit values, mod is identity when sum < 2^N *) - lemma mod_identity: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a + b < modulus n -> - mod (a + b) (modulus n) = a + b - - (* Lemma: The true sum of two N-bit values is bounded above by - * 2*(2^N - 1), which is strictly less than 2 * 2^N. - * This means at most one wrap occurs. *) - lemma sum_upper_bound: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a + b <= 2 * (modulus n) - 2 - - (* Lemma: When a value is in [m, 2m), mod subtracts m exactly once. - * This is the "single-wrap" case: if m <= x < 2*m, then - * x = 1*m + (x - m) with 0 <= x-m < m, so mod x m = x - m. *) - lemma mod_single_wrap: - forall x m: int. - m > 0 -> - x >= m -> - x < 2 * m -> - mod x m = x - m - - (* Corollary: For valid N-bit values, mod subtracts 2^N when sum >= 2^N. - * Follows from mod_single_wrap and sum_upper_bound. *) - lemma mod_subtract: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a + b >= modulus n -> - mod (a + b) (modulus n) = a + b - modulus n - - (* Lemma: When overflow occurs, the wrapped result is strictly less - * than a. This is the core of soundness. - * - * Proof sketch: If a + b >= 2^N, then wrap_add = a + b - 2^N. - * Since b <= 2^N - 1, we have a + b - 2^N <= a - 1 < a. *) - lemma overflow_implies_wrap_lt: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a + b >= modulus n -> - a + b - modulus n < a - - (* Lemma: When no overflow occurs, the wrapped result equals the - * true sum, which is >= a (since b >= 0). *) - lemma no_overflow_implies_wrap_ge: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a + b < modulus n -> - a + b >= a - - (* ---- Main Theorems ---- *) - - (* Theorem 1 (Soundness / No False Negatives): - * If the true sum overflows, the detection fires. - * - * In C++ terms: if lhs + rhs > max(T), then result < lhs is true. - * Equivalently: unsigned_no_intrin_add returns true. - * Consequence: throw_exception policy always throws on overflow. *) - lemma soundness: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - overflows a b n -> - detected a b n - - (* Theorem 2 (No False Positives): - * If the true sum does not overflow, detection does not fire. - * - * In C++ terms: if lhs + rhs <= max(T), then result < lhs is false. - * Equivalently: unsigned_no_intrin_add returns false. - * Consequence: throw_exception policy never throws for valid sums. *) - lemma no_false_positives: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - not (overflows a b n) -> - not (detected a b n) - - (* Theorem 3 (Correctness): - * When no overflow occurs, the wrapping result equals the true sum. - * - * In C++ terms: if lhs + rhs <= max(T), then - * static_cast(lhs + rhs) == lhs + rhs - * (no information is lost in the cast). *) - lemma correctness: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - not (overflows a b n) -> - wrap_add a b n = a + b - - (* Theorem 4 (Biconditional / Completeness): - * Detection fires if and only if overflow occurs. - * This combines Theorems 1 and 2. *) - lemma biconditional: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - (detected a b n <-> overflows a b n) + (* The u128 multiply-overflow check: for non-negative operands and bound, + * (rhs != 0 && lhs > m / rhs) holds exactly when lhs * rhs exceeds m. *) + lemma div_check_id : + forall a b m : int. 0 <= a -> 0 <= b -> 0 <= m -> + ((b <> 0 /\ a > div m b) <-> a * b > m) end (* ================================================================ - * Theory: UnsignedSubUnderflow - * - * Parametric proofs over an arbitrary bit-width N >= 1. - * Proves the underflow detection for unsigned subtraction. + * Theory: UnsignedOverflow * - * The portable underflow detection (lines 570-583) is: + * Generic over an arbitrary bit width (the abstract bv.BV_Gen, cloned with + * its standard-library lemmas assumed). Proving here covers every concrete + * width, so u8/u16/u32/u64/u128 are all handled by one proof. * - * template - * constexpr bool unsigned_no_intrin_sub(const T lhs, const T rhs, T& result) - * { - * result = static_cast(lhs - rhs); // wrapping subtraction - * return result > lhs; // underflow detection - * } - * - * The default operator- (lines 762-766) uses throw_exception policy, - * throwing std::underflow_error when the detection fires. + * For each operation the four standard properties are established: + * 1. Soundness -- overflow implies the C++ check fires + * 2. No false positives -- no overflow implies the check does not fire + * 3. Correctness -- with no overflow the result equals the exact value + * 4. Biconditional -- the check fires iff overflow occurs * ================================================================ *) -theory UnsignedSubUnderflow +theory UnsignedOverflow + clone export bv.BV_Gen with axiom . use int.Int - use int.Power use int.EuclideanDivision - use UnsignedAddOverflow - - (* ---- Subtraction-specific definitions ---- *) - - (* Wrapping subtraction: (a - b) mod 2^N - * Models: result = static_cast(lhs - rhs) - * Reference: unsigned_integer_basis.hpp line 579 *) - function wrap_sub (a b: int) (n: int) : int = - mod (a - b) (modulus n) - - (* Underflow detection: result > lhs - * Models: return result > lhs - * Reference: unsigned_integer_basis.hpp line 582 *) - predicate sub_detected (a b: int) (n: int) = - wrap_sub a b n > a - - (* True mathematical underflow: a - b goes below zero *) - predicate underflows (a b: int) = - a < b - - (* ---- Helper lemmas ---- *) - - (* For unsigned subtraction the difference a - b lies in - * [-(2^N - 1), 2^N - 1]. There are two cases: - * - * Case 1 (no underflow): a >= b, so 0 <= a-b < 2^N - * => mod(a-b, 2^N) = a-b - * - * Case 2 (underflow): a < b, so -2^N < a-b < 0 - * => mod(a-b, 2^N) = a-b + 2^N - *) - - (* General mod property: mod is identity for non-negative values < m *) - lemma mod_nonneg_small: - forall x m: int. - m > 0 -> - 0 <= x -> - x < m -> - mod x m = x - - (* General mod property: for negative values in (-m, 0), mod adds m *) - lemma mod_neg_wrap: - forall x m: int. - m > 0 -> - x < 0 -> - x > -m -> - mod x m = x + m - - (* The difference of two N-bit values is bounded below by -(2^N - 1), - * which is strictly greater than -2^N. *) - lemma sub_bounded_below: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a - b > -(modulus n) - - (* When no underflow, the wrapped result equals the true difference *) - lemma no_underflow_wrap_eq: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a >= b -> - wrap_sub a b n = a - b - - (* When no underflow, result <= lhs (since b >= 0) *) - lemma no_underflow_wrap_le: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a >= b -> - a - b <= a - - (* When underflow, the wrapped result = a - b + 2^N *) - lemma underflow_wrap_eq: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a < b -> - wrap_sub a b n = a - b + modulus n - - (* When underflow, result > lhs because 2^N > b for any valid b *) - lemma underflow_wrap_gt: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a < b -> - a - b + modulus n > a - - (* ---- Main Theorems ---- *) - - (* Theorem 1 (Soundness / No False Negatives): - * If a < b (underflow), the detection fires. - * - * In C++ terms: if lhs < rhs, then result > lhs is true. - * Equivalently: unsigned_no_intrin_sub returns true. - * Consequence: throw_exception policy always throws on underflow. *) - lemma sub_soundness: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - underflows a b -> - sub_detected a b n - - (* Theorem 2 (No False Positives): - * If a >= b (no underflow), the detection does not fire. - * - * In C++ terms: if lhs >= rhs, then result > lhs is false. - * Equivalently: unsigned_no_intrin_sub returns false. - * Consequence: throw_exception policy never throws for valid differences. *) - lemma sub_no_false_positives: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - not (underflows a b) -> - not (sub_detected a b n) - - (* Theorem 3 (Correctness): - * When no underflow, the wrapping result equals the true difference. - * - * In C++ terms: if lhs >= rhs, then - * static_cast(lhs - rhs) == lhs - rhs - * (no information is lost in the cast). *) - lemma sub_correctness: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - not (underflows a b) -> - wrap_sub a b n = a - b - - (* Theorem 4 (Biconditional / Completeness): - * Detection fires if and only if underflow occurs. - * Combines Theorems 1 and 2. *) - lemma sub_biconditional: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - (sub_detected a b n <-> underflows a b) - -end - -(* ================================================================ - * Theory: UnsignedMulOverflow - * - * Parametric proofs over an arbitrary bit-width N >= 1. - * Proves the overflow detection for unsigned multiplication. - * - * Two detection strategies are used in the C++ implementation: - * - * 1. Wide multiplication (u8, u16, u32, u64) - lines 842-852: - * Promotes to a type with >= 2N bits, computes the exact product, - * and checks: temp > max(T). - * This is trivially correct since the wide type holds the full - * product without loss. - * - * 2. Division check (u128) - lines 854-858: - * result = lhs * rhs; // wrapping - * return rhs != 0 && lhs > max(uint128) / rhs; // overflow detection - * This is the classic overflow-safe check for unsigned multiplication. - * - * Both strategies detect the same condition: a * b > max_val(n). - * The default operator* (lines 1046-1050) throws std::overflow_error. - * ================================================================ *) -theory UnsignedMulOverflow - - use int.Int - use int.Power - use int.EuclideanDivision - use UnsignedAddOverflow - - (* ---- Multiplication-specific definitions ---- *) - - (* Wrapping multiplication: (a * b) mod 2^N - * Models: result = static_cast(lhs * rhs) *) - function wrap_mul (a b: int) (n: int) : int = - mod (a * b) (modulus n) - - (* True mathematical overflow: product exceeds representable range *) - predicate mul_overflows (a b: int) (n: int) = - a * b > max_val n - - (* Division-check detection (used for u128): - * rhs != 0 && lhs > max / rhs (integer division) - * Reference: unsigned_integer_basis.hpp line 857 *) - predicate div_check_detected (a b: int) (n: int) = - b > 0 /\ a > div (max_val n) b - - (* ---- Helper lemmas ---- *) - - (* Product of two non-negative values is non-negative *) - lemma product_nonneg: - forall a b: int. - 0 <= a -> 0 <= b -> 0 <= a * b - - (* Multiplication is monotone in each argument for non-negative values. - * This guides the provers for product_bounded below. *) - lemma mul_mono_right: - forall a b c: int. - 0 <= c -> 0 <= a -> a <= b -> a * c <= b * c - - lemma mul_mono_left: - forall a b c: int. - 0 <= c -> 0 <= a -> a <= b -> c * a <= c * b - - (* Product of two N-bit values is bounded: a*b <= (2^N - 1)^2. - * Step 1: a <= max => a*b <= max*b (mono in first arg) - * Step 2: b <= max => max*b <= max*max (mono in second arg) *) - lemma product_bounded_step1: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a * b <= max_val n * b - - lemma product_bounded: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a * b <= max_val n * max_val n + use IntLemmas - (* (2^N - 1)^2 < 2^(2N), so the product fits in 2N bits. - * This justifies the wide-multiplication approach: promoting - * to a type with >= 2N bits guarantees no overflow in the - * intermediate computation. - * Uses Power_sum: power 2 (2*n) = power 2 n * power 2 n *) - lemma product_fits_in_2n: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - a * b < modulus (2 * n) + (* ---- Addition: C++ result = lhs + rhs (wrapping); overflow iff result < lhs ---- *) - (* When no overflow, the product is within [0, max_val n], - * so mod is identity *) - lemma mul_mod_identity: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - not (mul_overflows a b n) -> - mod (a * b) (modulus n) = a * b + predicate add_detected (a b : t) = ult (add a b) a + predicate add_overflows (a b : t) = to_uint a + to_uint b > max_int - (* ---- Division-check correctness (u128 path) ---- *) + lemma add_soundness : + forall a b : t. add_overflows a b -> add_detected a b + lemma add_no_false_positives : + forall a b : t. not (add_overflows a b) -> not (add_detected a b) + lemma add_correctness : + forall a b : t. not (add_overflows a b) -> to_uint (add a b) = to_uint a + to_uint b + lemma add_biconditional : + forall a b : t. add_detected a b <-> add_overflows a b - (* Multiplying by zero never overflows *) - lemma mul_by_zero_no_overflow: - forall a n: int. - n >= 1 -> - valid a n -> - not (mul_overflows a 0 n) + (* boundary: the maximum value plus any positive value overflows *) + lemma add_overflow_at_max : + forall a b : t. to_uint a = max_int -> 0 < to_uint b -> add_overflows a b - (* When b = 0, detection correctly does not fire *) - lemma div_check_zero_rhs: - forall a n: int. - n >= 1 -> - valid a n -> - not (div_check_detected a 0 n) + (* ---- Subtraction: C++ result = lhs - rhs (wrapping); underflow iff result > lhs ---- *) - (* Division-check soundness: a > max/b implies a*b > max. - * - * Proof sketch: Let q = div(max, b) and r = mod(max, b). - * Then max = q*b + r with 0 <= r < b. - * If a > q, then a >= q+1, so a*b >= (q+1)*b = q*b + b > q*b + r = max. - * - * We provide two helpers to guide the provers through this reasoning. *) + predicate sub_detected (a b : t) = ugt (sub a b) a + predicate sub_underflows (a b : t) = to_uint a < to_uint b - (* Helper: a > q implies a*b >= (q+1)*b *) - lemma div_check_step1: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - a > div (max_val n) b -> - a * b >= (div (max_val n) b + 1) * b + lemma sub_soundness : + forall a b : t. sub_underflows a b -> sub_detected a b + lemma sub_no_false_positives : + forall a b : t. not (sub_underflows a b) -> not (sub_detected a b) + lemma sub_correctness : + forall a b : t. not (sub_underflows a b) -> to_uint (sub a b) = to_uint a - to_uint b + lemma sub_biconditional : + forall a b : t. sub_detected a b <-> sub_underflows a b - (* Helper: (q+1)*b > max, because max = q*b + r with r < b *) - lemma div_check_step2: - forall b n: int. - n >= 1 -> - valid b n -> - b > 0 -> - (div (max_val n) b + 1) * b > max_val n + (* boundary: zero minus any positive value underflows *) + lemma sub_underflow_at_zero : + forall a b : t. to_uint a = 0 -> 0 < to_uint b -> sub_underflows a b - lemma div_check_soundness: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - a > div (max_val n) b -> - mul_overflows a b n - - (* Division-check no false positives: a <= max/b implies a*b <= max. - * - * Proof sketch: If a <= q = div(max, b), then - * a*b <= q*b = max - r <= max. *) - lemma div_check_no_false_positives: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - a <= div (max_val n) b -> - not (mul_overflows a b n) - - (* Division check is equivalent to overflow when b > 0 *) - lemma div_check_iff_overflow_pos: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - (a > div (max_val n) b <-> mul_overflows a b n) - - (* Full division-check detection equivalence including b = 0 case *) - lemma div_check_biconditional: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - (div_check_detected a b n <-> mul_overflows a b n) - - (* ---- Main Theorems ---- *) - - (* Theorem 1 (Correctness): - * When no overflow occurs, the wrapping result equals the true product. - * - * In C++ terms: if lhs * rhs <= max(T), then - * static_cast(lhs * rhs) == lhs * rhs *) - lemma mul_correctness: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - not (mul_overflows a b n) -> - wrap_mul a b n = a * b - - (* Theorem 2 (Wide multiplication safety): - * The product of two N-bit values fits in 2N bits. - * This proves that promoting to a wider type (u8->u16, u16->u32, - * u32->u64, u64->u128) allows exact computation of the product, - * making the subsequent "temp > max" check trivially correct. *) - lemma wide_mul_safe: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - valid (a * b) (2 * n) - - (* Theorem 3 (Division-check equivalence): - * The division-based detection (b != 0 && a > max/b) correctly - * identifies all and only overflowing multiplications. - * This covers the u128 code path. *) - lemma div_check_complete: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - (div_check_detected a b n <-> mul_overflows a b n) - -end - -(* ================================================================ - * Theory: UnsignedDivSafety - * - * Proves that unsigned integer division is safe: the only error - * case is division by zero, and for any non-zero divisor the result - * is always a valid N-bit unsigned value. - * - * The C++ implementation (lines 1069-1107, 1201-1205): - * - * if (rhs == 0) throw std::domain_error("Unsigned division by zero"); - * return lhs / rhs; - * - * The default operator/ (lines 1201-1205) uses throw_exception policy. - * - * Unlike addition/subtraction/multiplication, unsigned division - * CANNOT overflow: a / b <= a <= max_val(n) for all b >= 1. - * ================================================================ *) -theory UnsignedDivSafety - - use int.Int - use int.Power - use int.EuclideanDivision - use UnsignedAddOverflow - - (* ---- Definitions ---- *) - - (* Integer division for unsigned values. - * Models: static_cast(lhs) / static_cast(rhs) - * Reference: unsigned_integer_basis.hpp line 1100/1104 *) - function udiv (a b: int) : int = div a b - - (* The only error condition: divisor is zero *) - predicate div_by_zero (b: int) = b = 0 - - (* ---- Helper lemmas ---- *) - - (* Division of non-negative by positive is non-negative *) - lemma div_nonneg: - forall a b: int. - 0 <= a -> b > 0 -> 0 <= div a b - - (* Division reduces the dividend: a / b <= a for a >= 0, b >= 1 *) - lemma div_le_dividend: - forall a b: int. - 0 <= a -> b >= 1 -> div a b <= a - - (* ---- Main Theorems ---- *) - - (* Theorem 1 (Result validity): - * For non-zero divisor, the quotient is a valid N-bit value. - * Since 0 <= a/b <= a <= max_val(n), the result fits. *) - lemma div_result_valid: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - valid (udiv a b) n - - (* Theorem 2 (Correctness): - * The result is the true mathematical (Euclidean) quotient. - * No wrapping or truncation occurs. *) - lemma div_correctness: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - udiv a b = div a b - - (* Theorem 3 (No overflow): - * Unsigned division never overflows. The only error is div-by-zero. - * This justifies the C++ implementation having no overflow check. *) - lemma div_no_overflow: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - udiv a b <= max_val n - - (* Theorem 4 (Complete error detection): - * The div-by-zero check (rhs == 0) catches exactly the error cases. - * There are no other failure modes for unsigned division. *) - lemma div_error_iff_zero: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - (div_by_zero b <-> b = 0) - -end - -(* ================================================================ - * Theory: UnsignedModSafety - * - * Proves that unsigned integer modulo is safe: the only error - * case is modulo by zero, and for any non-zero divisor the result - * is always a valid N-bit unsigned value. - * - * The C++ implementation (lines 1224-1262, 1356-1360): - * - * if (rhs == 0) throw std::domain_error("Unsigned modulo by zero"); - * return lhs % rhs; - * - * The default operator% (lines 1356-1360) uses throw_exception policy. - * - * Unsigned modulo CANNOT overflow: a % b < b <= max_val(n) for b >= 1. - * ================================================================ *) -theory UnsignedModSafety - - use int.Int - use int.Power - use int.EuclideanDivision - use UnsignedAddOverflow - - (* ---- Definitions ---- *) - - (* Integer modulo for unsigned values. - * Models: static_cast(lhs) % static_cast(rhs) - * Reference: unsigned_integer_basis.hpp line 1255/1259 *) - function umod (a b: int) : int = mod a b - - (* The only error condition: divisor is zero *) - predicate mod_by_zero (b: int) = b = 0 - - (* ---- Helper lemmas ---- *) - - (* Modulo of non-negative by positive is non-negative *) - lemma mod_nonneg: - forall a b: int. - 0 <= a -> b > 0 -> 0 <= mod a b - - (* Modulo is strictly less than the divisor *) - lemma mod_lt_divisor: - forall a b: int. - 0 <= a -> b > 0 -> mod a b < b - - (* ---- Main Theorems ---- *) - - (* Theorem 1 (Result validity): - * For non-zero divisor, the remainder is a valid N-bit value. - * Since 0 <= a%b < b <= max_val(n), the result fits. *) - lemma mod_result_valid: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - valid (umod a b) n - - (* Theorem 2 (Correctness): - * The result is the true mathematical (Euclidean) remainder. - * No wrapping or truncation occurs. *) - lemma mod_correctness: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - umod a b = mod a b - - (* Theorem 3 (No overflow): - * Unsigned modulo never overflows. The only error is mod-by-zero. - * This justifies the C++ implementation having no overflow check. *) - lemma mod_no_overflow: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - b > 0 -> - umod a b <= max_val n - - (* Theorem 4 (Euclidean relationship): - * The quotient and remainder satisfy: a = (a/b)*b + (a%b). - * This is the fundamental property that ties division and modulo. *) - lemma div_mod_relationship: - forall a b: int. - 0 <= a -> b > 0 -> - a = div a b * b + mod a b + (* ---- Multiplication ---- *) - (* Theorem 5 (Complete error detection): - * The mod-by-zero check (rhs == 0) catches exactly the error cases. *) - lemma mod_error_iff_zero: - forall a b n: int. - n >= 1 -> - valid a n -> - valid b n -> - (mod_by_zero b <-> b = 0) + predicate mul_overflows (a b : t) = to_uint a * to_uint b > max_int + (* C++ u128 detection: rhs != 0 && lhs > max / rhs *) + predicate mul_div_check (a b : t) = to_uint b <> 0 /\ to_uint a > div max_int (to_uint b) + + lemma mul_correctness : + forall a b : t. not (mul_overflows a b) -> to_uint (mul a b) = to_uint a * to_uint b + lemma mul_div_check_biconditional : + forall a b : t. mul_div_check a b <-> mul_overflows a b + (* C++ u8-u64 strategy: the exact product fits in a 2N-bit type *) + lemma mul_wide_safe : + forall a b : t. to_uint a * to_uint b < two_power_size * two_power_size + + (* ---- Division / Modulo (the only runtime error is divide-by-zero) ---- *) + + lemma div_result_valid : + forall a b : t. to_uint b <> 0 -> 0 <= to_uint (udiv a b) <= max_int + lemma div_correctness : + forall a b : t. to_uint b <> 0 -> to_uint (udiv a b) = div (to_uint a) (to_uint b) + lemma mod_result_valid : + forall a b : t. to_uint b <> 0 -> 0 <= to_uint (urem a b) < to_uint b + lemma mod_correctness : + forall a b : t. to_uint b <> 0 -> to_uint (urem a b) = mod (to_uint a) (to_uint b) end (* ================================================================ - * Theory: UnsignedU8 - * - * Concrete instantiation for uint8_t (N = 8, modulus = 256). - * - * Models: boost::safe_numbers::u8 - * = detail::unsigned_integer_basis - * Reference: unsigned_integers.hpp line 20 + * Per-width concrete boundary witnesses. * - * Note: For uint8_t and uint16_t, the C++ implementation performs - * intermediate arithmetic in uint32_t before truncating: - * result = static_cast(static_cast(lhs +/- rhs)); - * (unsigned_integer_basis.hpp lines 187-190, 573-576) - * The mathematical model is identical: the final stored result is - * still (a +/- b) mod 2^N. + * Each theory instantiates the proof at one concrete C++ type and checks a + * couple of boundary cases directly on the corresponding bitvector module: + * u8 = BV8, u16 = BV16, u32 = BV32, u64 = BV64, u128 = BV128. + * (int.Int is intentionally not imported here: its constants one/zero would + * clash with the bitvector constants one/zeros/ones.) * ================================================================ *) theory UnsignedU8 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use UnsignedAddOverflow - use UnsignedSubUnderflow - use UnsignedMulOverflow - use UnsignedDivSafety - use UnsignedModSafety - - constant n8 : int = 8 - - lemma n8_valid: n8 >= 1 - - lemma u8_modulus: modulus n8 = 256 - - lemma u8_max: max_val n8 = 255 - - (* ---- Addition ---- *) - - lemma u8_add_soundness: - forall a b: int. - valid a n8 -> valid b n8 -> - overflows a b n8 -> - detected a b n8 - - lemma u8_add_no_false_positives: - forall a b: int. - valid a n8 -> valid b n8 -> - not (overflows a b n8) -> - not (detected a b n8) - - lemma u8_add_correctness: - forall a b: int. - valid a n8 -> valid b n8 -> - not (overflows a b n8) -> - wrap_add a b n8 = a + b - - lemma u8_add_biconditional: - forall a b: int. - valid a n8 -> valid b n8 -> - (detected a b n8 <-> overflows a b n8) - - (* Addition boundary tests *) - - lemma u8_add_max_plus_one: - overflows 255 1 n8 - - lemma u8_add_max_plus_zero: - not (overflows 255 0 n8) - - lemma u8_add_half_plus_half: - overflows 128 128 n8 - - lemma u8_add_half_plus_half_minus_one: - not (overflows 128 127 n8) - - (* ---- Subtraction ---- *) - - lemma u8_sub_soundness: - forall a b: int. - valid a n8 -> valid b n8 -> - underflows a b -> - sub_detected a b n8 - - lemma u8_sub_no_false_positives: - forall a b: int. - valid a n8 -> valid b n8 -> - not (underflows a b) -> - not (sub_detected a b n8) - - lemma u8_sub_correctness: - forall a b: int. - valid a n8 -> valid b n8 -> - not (underflows a b) -> - wrap_sub a b n8 = a - b - - lemma u8_sub_biconditional: - forall a b: int. - valid a n8 -> valid b n8 -> - (sub_detected a b n8 <-> underflows a b) - - (* Subtraction boundary tests *) - - (* 0 - 1 underflows *) - lemma u8_sub_zero_minus_one: - underflows 0 1 - - (* 0 - 0 does not underflow *) - lemma u8_sub_zero_minus_zero: - not (underflows 0 0) - - (* 100 - 101 underflows *) - lemma u8_sub_small_underflow: - underflows 100 101 - - (* 200 - 100 does not underflow *) - lemma u8_sub_no_underflow: - not (underflows 200 100) - - (* ---- Multiplication ---- *) - - lemma u8_mul_correctness: - forall a b: int. - valid a n8 -> valid b n8 -> - not (mul_overflows a b n8) -> - wrap_mul a b n8 = a * b - - lemma u8_mul_wide_safe: - forall a b: int. - valid a n8 -> valid b n8 -> - valid (a * b) (2 * n8) - - lemma u8_mul_div_check: - forall a b: int. - valid a n8 -> valid b n8 -> - (div_check_detected a b n8 <-> mul_overflows a b n8) - - (* Multiplication boundary tests *) - - (* 16 * 16 = 256 overflows u8 *) - lemma u8_mul_overflow: - mul_overflows 16 16 n8 - - (* 15 * 17 = 255 does not overflow u8 *) - lemma u8_mul_no_overflow: - not (mul_overflows 15 17 n8) - - (* 255 * 0 = 0 does not overflow *) - lemma u8_mul_by_zero: - not (mul_overflows 255 0 n8) - - (* ---- Division ---- *) - - lemma u8_div_valid: - forall a b: int. - valid a n8 -> valid b n8 -> b > 0 -> - valid (udiv a b) n8 - - lemma u8_div_correctness: - forall a b: int. - valid a n8 -> valid b n8 -> b > 0 -> - udiv a b = div a b - - (* Division boundary tests *) - - (* 255 / 1 = 255, valid u8 *) - lemma u8_div_max_by_one: - udiv 255 1 = 255 - - (* 200 / 3 = 66, valid u8 *) - lemma u8_div_normal: - udiv 200 3 = 66 - - (* 0 / 255 = 0 *) - lemma u8_div_zero_dividend: - udiv 0 255 = 0 - - (* ---- Modulo ---- *) - - lemma u8_mod_valid: - forall a b: int. - valid a n8 -> valid b n8 -> b > 0 -> - valid (umod a b) n8 - - lemma u8_mod_correctness: - forall a b: int. - valid a n8 -> valid b n8 -> b > 0 -> - umod a b = mod a b - - (* Modulo boundary tests *) - - (* 255 % 1 = 0 *) - lemma u8_mod_by_one: - umod 255 1 = 0 - - (* 200 % 3 = 2 *) - lemma u8_mod_normal: - umod 200 3 = 2 - - (* 0 % 255 = 0 *) - lemma u8_mod_zero_dividend: - umod 0 255 = 0 - - (* 100 % 100 = 0 *) - lemma u8_mod_equal: - umod 100 100 = 0 - + use bv.BV8 + lemma u8_add_max_plus_one : ult (add ones one) ones (* max + 1 wraps -> detected *) + lemma u8_add_max_plus_zero : not (ult (add ones zeros) ones) (* max + 0 -> not detected *) + lemma u8_sub_zero_minus_one : ugt (sub zeros one) zeros (* 0 - 1 wraps -> detected *) + lemma u8_sub_no_underflow : not (ugt (sub ones one) ones) (* max - 1 -> not detected *) end -(* ================================================================ - * Theory: UnsignedU16 - * - * Concrete instantiation for uint16_t (N = 16, modulus = 65536). - * - * Models: boost::safe_numbers::u16 - * = detail::unsigned_integer_basis - * Reference: unsigned_integers.hpp line 22 - * ================================================================ *) theory UnsignedU16 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use UnsignedAddOverflow - use UnsignedSubUnderflow - use UnsignedMulOverflow - use UnsignedDivSafety - use UnsignedModSafety - - constant n16 : int = 16 - - lemma n16_valid: n16 >= 1 - - lemma u16_modulus: modulus n16 = 65536 - - lemma u16_max: max_val n16 = 65535 - - (* ---- Addition ---- *) - - lemma u16_add_soundness: - forall a b: int. - valid a n16 -> valid b n16 -> - overflows a b n16 -> - detected a b n16 - - lemma u16_add_no_false_positives: - forall a b: int. - valid a n16 -> valid b n16 -> - not (overflows a b n16) -> - not (detected a b n16) - - lemma u16_add_correctness: - forall a b: int. - valid a n16 -> valid b n16 -> - not (overflows a b n16) -> - wrap_add a b n16 = a + b - - lemma u16_add_biconditional: - forall a b: int. - valid a n16 -> valid b n16 -> - (detected a b n16 <-> overflows a b n16) - - (* ---- Subtraction ---- *) - - lemma u16_sub_soundness: - forall a b: int. - valid a n16 -> valid b n16 -> - underflows a b -> - sub_detected a b n16 - - lemma u16_sub_no_false_positives: - forall a b: int. - valid a n16 -> valid b n16 -> - not (underflows a b) -> - not (sub_detected a b n16) - - lemma u16_sub_correctness: - forall a b: int. - valid a n16 -> valid b n16 -> - not (underflows a b) -> - wrap_sub a b n16 = a - b - - lemma u16_sub_biconditional: - forall a b: int. - valid a n16 -> valid b n16 -> - (sub_detected a b n16 <-> underflows a b) - - (* ---- Multiplication ---- *) - - lemma u16_mul_correctness: - forall a b: int. - valid a n16 -> valid b n16 -> - not (mul_overflows a b n16) -> - wrap_mul a b n16 = a * b - - lemma u16_mul_wide_safe: - forall a b: int. - valid a n16 -> valid b n16 -> - valid (a * b) (2 * n16) - - lemma u16_mul_div_check: - forall a b: int. - valid a n16 -> valid b n16 -> - (div_check_detected a b n16 <-> mul_overflows a b n16) - - (* ---- Division ---- *) - - lemma u16_div_valid: - forall a b: int. - valid a n16 -> valid b n16 -> b > 0 -> - valid (udiv a b) n16 - - lemma u16_div_correctness: - forall a b: int. - valid a n16 -> valid b n16 -> b > 0 -> - udiv a b = div a b - - (* ---- Modulo ---- *) - - lemma u16_mod_valid: - forall a b: int. - valid a n16 -> valid b n16 -> b > 0 -> - valid (umod a b) n16 - - lemma u16_mod_correctness: - forall a b: int. - valid a n16 -> valid b n16 -> b > 0 -> - umod a b = mod a b - + use bv.BV16 + lemma u16_add_max_plus_one : ult (add ones one) ones (* max + 1 wraps -> detected *) + lemma u16_add_max_plus_zero : not (ult (add ones zeros) ones) (* max + 0 -> not detected *) + lemma u16_sub_zero_minus_one : ugt (sub zeros one) zeros (* 0 - 1 wraps -> detected *) + lemma u16_sub_no_underflow : not (ugt (sub ones one) ones) (* max - 1 -> not detected *) end -(* ================================================================ - * Theory: UnsignedU32 - * - * Concrete instantiation for uint32_t (N = 32, modulus = 2^32). - * - * Models: boost::safe_numbers::u32 - * = detail::unsigned_integer_basis - * Reference: unsigned_integers.hpp line 24 - * ================================================================ *) theory UnsignedU32 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use UnsignedAddOverflow - use UnsignedSubUnderflow - use UnsignedMulOverflow - use UnsignedDivSafety - use UnsignedModSafety - - constant n32 : int = 32 - - lemma n32_valid: n32 >= 1 - - lemma u32_modulus: modulus n32 = 4294967296 - - lemma u32_max: max_val n32 = 4294967295 - - (* ---- Addition ---- *) - - lemma u32_add_soundness: - forall a b: int. - valid a n32 -> valid b n32 -> - overflows a b n32 -> - detected a b n32 - - lemma u32_add_no_false_positives: - forall a b: int. - valid a n32 -> valid b n32 -> - not (overflows a b n32) -> - not (detected a b n32) - - lemma u32_add_correctness: - forall a b: int. - valid a n32 -> valid b n32 -> - not (overflows a b n32) -> - wrap_add a b n32 = a + b - - lemma u32_add_biconditional: - forall a b: int. - valid a n32 -> valid b n32 -> - (detected a b n32 <-> overflows a b n32) - - (* ---- Subtraction ---- *) - - lemma u32_sub_soundness: - forall a b: int. - valid a n32 -> valid b n32 -> - underflows a b -> - sub_detected a b n32 - - lemma u32_sub_no_false_positives: - forall a b: int. - valid a n32 -> valid b n32 -> - not (underflows a b) -> - not (sub_detected a b n32) - - lemma u32_sub_correctness: - forall a b: int. - valid a n32 -> valid b n32 -> - not (underflows a b) -> - wrap_sub a b n32 = a - b - - lemma u32_sub_biconditional: - forall a b: int. - valid a n32 -> valid b n32 -> - (sub_detected a b n32 <-> underflows a b) - - (* ---- Multiplication ---- *) - - lemma u32_mul_correctness: - forall a b: int. - valid a n32 -> valid b n32 -> - not (mul_overflows a b n32) -> - wrap_mul a b n32 = a * b - - lemma u32_mul_wide_safe: - forall a b: int. - valid a n32 -> valid b n32 -> - valid (a * b) (2 * n32) - - lemma u32_mul_div_check: - forall a b: int. - valid a n32 -> valid b n32 -> - (div_check_detected a b n32 <-> mul_overflows a b n32) - - (* ---- Division ---- *) - - lemma u32_div_valid: - forall a b: int. - valid a n32 -> valid b n32 -> b > 0 -> - valid (udiv a b) n32 - - lemma u32_div_correctness: - forall a b: int. - valid a n32 -> valid b n32 -> b > 0 -> - udiv a b = div a b - - (* ---- Modulo ---- *) - - lemma u32_mod_valid: - forall a b: int. - valid a n32 -> valid b n32 -> b > 0 -> - valid (umod a b) n32 - - lemma u32_mod_correctness: - forall a b: int. - valid a n32 -> valid b n32 -> b > 0 -> - umod a b = mod a b - + use bv.BV32 + lemma u32_add_max_plus_one : ult (add ones one) ones (* max + 1 wraps -> detected *) + lemma u32_add_max_plus_zero : not (ult (add ones zeros) ones) (* max + 0 -> not detected *) + lemma u32_sub_zero_minus_one : ugt (sub zeros one) zeros (* 0 - 1 wraps -> detected *) + lemma u32_sub_no_underflow : not (ugt (sub ones one) ones) (* max - 1 -> not detected *) end -(* ================================================================ - * Theory: UnsignedU64 - * - * Concrete instantiation for uint64_t (N = 64, modulus = 2^64). - * - * Models: boost::safe_numbers::u64 - * = detail::unsigned_integer_basis - * Reference: unsigned_integers.hpp line 26 - * ================================================================ *) theory UnsignedU64 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use UnsignedAddOverflow - use UnsignedSubUnderflow - use UnsignedMulOverflow - use UnsignedDivSafety - use UnsignedModSafety - - constant n64 : int = 64 - - lemma n64_valid: n64 >= 1 - - lemma u64_modulus: modulus n64 = 18446744073709551616 - - lemma u64_max: max_val n64 = 18446744073709551615 - - (* ---- Addition ---- *) - - lemma u64_add_soundness: - forall a b: int. - valid a n64 -> valid b n64 -> - overflows a b n64 -> - detected a b n64 - - lemma u64_add_no_false_positives: - forall a b: int. - valid a n64 -> valid b n64 -> - not (overflows a b n64) -> - not (detected a b n64) - - lemma u64_add_correctness: - forall a b: int. - valid a n64 -> valid b n64 -> - not (overflows a b n64) -> - wrap_add a b n64 = a + b - - lemma u64_add_biconditional: - forall a b: int. - valid a n64 -> valid b n64 -> - (detected a b n64 <-> overflows a b n64) - - (* ---- Subtraction ---- *) - - lemma u64_sub_soundness: - forall a b: int. - valid a n64 -> valid b n64 -> - underflows a b -> - sub_detected a b n64 - - lemma u64_sub_no_false_positives: - forall a b: int. - valid a n64 -> valid b n64 -> - not (underflows a b) -> - not (sub_detected a b n64) - - lemma u64_sub_correctness: - forall a b: int. - valid a n64 -> valid b n64 -> - not (underflows a b) -> - wrap_sub a b n64 = a - b - - lemma u64_sub_biconditional: - forall a b: int. - valid a n64 -> valid b n64 -> - (sub_detected a b n64 <-> underflows a b) - - (* ---- Multiplication ---- *) - - lemma u64_mul_correctness: - forall a b: int. - valid a n64 -> valid b n64 -> - not (mul_overflows a b n64) -> - wrap_mul a b n64 = a * b - - lemma u64_mul_wide_safe: - forall a b: int. - valid a n64 -> valid b n64 -> - valid (a * b) (2 * n64) - - lemma u64_mul_div_check: - forall a b: int. - valid a n64 -> valid b n64 -> - (div_check_detected a b n64 <-> mul_overflows a b n64) - - (* ---- Division ---- *) - - lemma u64_div_valid: - forall a b: int. - valid a n64 -> valid b n64 -> b > 0 -> - valid (udiv a b) n64 - - lemma u64_div_correctness: - forall a b: int. - valid a n64 -> valid b n64 -> b > 0 -> - udiv a b = div a b - - (* ---- Modulo ---- *) - - lemma u64_mod_valid: - forall a b: int. - valid a n64 -> valid b n64 -> b > 0 -> - valid (umod a b) n64 - - lemma u64_mod_correctness: - forall a b: int. - valid a n64 -> valid b n64 -> b > 0 -> - umod a b = mod a b - + use bv.BV64 + lemma u64_add_max_plus_one : ult (add ones one) ones (* max + 1 wraps -> detected *) + lemma u64_add_max_plus_zero : not (ult (add ones zeros) ones) (* max + 0 -> not detected *) + lemma u64_sub_zero_minus_one : ugt (sub zeros one) zeros (* 0 - 1 wraps -> detected *) + lemma u64_sub_no_underflow : not (ugt (sub ones one) ones) (* max - 1 -> not detected *) end -(* ================================================================ - * Theory: UnsignedU128 - * - * Concrete instantiation for uint128_t (N = 128, modulus = 2^128). - * - * Models: boost::safe_numbers::u128 - * = detail::unsigned_integer_basis - * Reference: unsigned_integers.hpp line 28 - * ================================================================ *) theory UnsignedU128 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use UnsignedAddOverflow - use UnsignedSubUnderflow - use UnsignedMulOverflow - use UnsignedDivSafety - use UnsignedModSafety - - constant n128 : int = 128 - - lemma n128_valid: n128 >= 1 - - (* 2^128 = 340282366920938463463374607431768211456 *) - lemma u128_modulus: modulus n128 = 340282366920938463463374607431768211456 - - (* 2^128 - 1 = 340282366920938463463374607431768211455 *) - lemma u128_max: max_val n128 = 340282366920938463463374607431768211455 - - (* ---- Addition ---- *) - - lemma u128_add_soundness: - forall a b: int. - valid a n128 -> valid b n128 -> - overflows a b n128 -> - detected a b n128 - - lemma u128_add_no_false_positives: - forall a b: int. - valid a n128 -> valid b n128 -> - not (overflows a b n128) -> - not (detected a b n128) - - lemma u128_add_correctness: - forall a b: int. - valid a n128 -> valid b n128 -> - not (overflows a b n128) -> - wrap_add a b n128 = a + b - - lemma u128_add_biconditional: - forall a b: int. - valid a n128 -> valid b n128 -> - (detected a b n128 <-> overflows a b n128) - - (* ---- Subtraction ---- *) - - lemma u128_sub_soundness: - forall a b: int. - valid a n128 -> valid b n128 -> - underflows a b -> - sub_detected a b n128 - - lemma u128_sub_no_false_positives: - forall a b: int. - valid a n128 -> valid b n128 -> - not (underflows a b) -> - not (sub_detected a b n128) - - lemma u128_sub_correctness: - forall a b: int. - valid a n128 -> valid b n128 -> - not (underflows a b) -> - wrap_sub a b n128 = a - b - - lemma u128_sub_biconditional: - forall a b: int. - valid a n128 -> valid b n128 -> - (sub_detected a b n128 <-> underflows a b) - - (* ---- Multiplication ---- *) - (* Note: u128 uses the division-check path exclusively since - * there is no wider type available. - * Reference: unsigned_integer_basis.hpp lines 854-858 *) - - lemma u128_mul_correctness: - forall a b: int. - valid a n128 -> valid b n128 -> - not (mul_overflows a b n128) -> - wrap_mul a b n128 = a * b - - lemma u128_mul_div_check: - forall a b: int. - valid a n128 -> valid b n128 -> - (div_check_detected a b n128 <-> mul_overflows a b n128) - - (* ---- Division ---- *) - - lemma u128_div_valid: - forall a b: int. - valid a n128 -> valid b n128 -> b > 0 -> - valid (udiv a b) n128 - - lemma u128_div_correctness: - forall a b: int. - valid a n128 -> valid b n128 -> b > 0 -> - udiv a b = div a b - - (* ---- Modulo ---- *) - - lemma u128_mod_valid: - forall a b: int. - valid a n128 -> valid b n128 -> b > 0 -> - valid (umod a b) n128 - - lemma u128_mod_correctness: - forall a b: int. - valid a n128 -> valid b n128 -> b > 0 -> - umod a b = mod a b - + use bv.BV128 + lemma u128_add_max_plus_one : ult (add ones one) ones (* max + 1 wraps -> detected *) + lemma u128_add_max_plus_zero : not (ult (add ones zeros) ones) (* max + 0 -> not detected *) + lemma u128_sub_zero_minus_one : ugt (sub zeros one) zeros (* 0 - 1 wraps -> detected *) + lemma u128_sub_no_underflow : not (ugt (sub ones one) ones) (* max - 1 -> not detected *) end From ea7b46090d115c4b9ce5e8ef5ddac226d3b82694 Mon Sep 17 00:00:00 2001 From: Matt Borland Date: Tue, 9 Jun 2026 15:23:30 -0400 Subject: [PATCH 3/3] Significant simplification of signed behavior --- test/theorems/signed_integers.why | 1293 ++--------------------------- 1 file changed, 77 insertions(+), 1216 deletions(-) diff --git a/test/theorems/signed_integers.why b/test/theorems/signed_integers.why index 81de5d4..1c8c756 100644 --- a/test/theorems/signed_integers.why +++ b/test/theorems/signed_integers.why @@ -6,115 +6,47 @@ * Distributed under the Boost Software License, Version 1.0. * https://www.boost.org/LICENSE_1_0.txt * - * This file formally proves the correctness of all signed arithmetic - * operations (+, -, *, /, %, unary -, ++, --) in Boost.SafeNumbers. * The C++ implementation is in: * * include/boost/safe_numbers/detail/signed_integer_basis.hpp * - * The portable overflow detection for addition (lines 461-488) is: - * - * temp = (unsigned)lhs + (unsigned)rhs; // wrapping addition - * result = (signed)temp; // two's complement cast - * has_overflow = ((~(ulhs ^ urhs)) & (ulhs ^ temp)) >> (N-1); - * - * This bit formula evaluates to 1 iff the sign bits of lhs and rhs agree - * AND the sign bit of the result differs from lhs. We model it in Why3 - * as an arithmetic predicate over the unsigned view of each value. - * - * The portable overflow detection for subtraction (lines 1074-1101) is: - * - * temp = (unsigned)lhs - (unsigned)rhs; // wrapping subtraction - * has_overflow = ((ulhs ^ urhs) & (ulhs ^ temp)) >> (N-1); - * - * This fires iff the operand signs differ AND the result sign differs - * from lhs. - * - * Multiplication overflow detection uses two strategies: - * - * 1. Wide multiplication (i8/i16/i32/i64, lines 1609-1656): - * Promote to a wider signed type, compute exact product, check - * against max() and min(). - * - * 2. Absolute-value division check (i128, lines 1573-1608): - * abs_lhs = |a|, abs_rhs = |b| computed in unsigned domain; - * max_magnitude = max() if signs agree, |min()| if signs differ; - * overflow iff abs_rhs != 0 && abs_lhs > max_magnitude / abs_rhs. - * - * Division (lines 2040-2149): throws domain_error on rhs == 0, and - * overflow_error on lhs == min() && rhs == -1 (the only overflowing - * pair of signed operands). - * - * Modulo (lines 2305-2500): throws domain_error on rhs == 0, and - * overflow_error on lhs == min() && rhs == -1. The latter is C++ UB - * for native types even though the mathematical remainder is 0; the - * library treats it as overflow for consistency with division. - * - * Unary minus (lines 348-356): throws domain_error on -min(). - * Increment (lines 2578-2603): throws overflow_error on a == max(). - * Decrement (lines 2611-2636): throws underflow_error on a == min(). - * - * Modeling notes: - * - Signed wrap is s_wrap(s, n) = either mod s 2^n or mod s 2^n - 2^n, - * chosen to land in [-2^(n-1), 2^(n-1)). Euclidean mod is used - * throughout the wrap-based theories. - * - Signed div/mod use int.ComputerDivision (truncated toward zero) - * to match C++ / and % semantics. The alias `Comp` disambiguates - * against EuclideanDivision's div/mod when both are in scope. - * - The connection between this Why3 model and the C++ bit formula - * is established by inspection: the shift-by-(N-1) extracts the - * high bit, which our model encodes as is_neg_bit u n := u >= 2^(n-1). - * - * Verification: All 287 lemmas are proved using two complementary provers: - * - Alt-Ergo 2.4.3: proves 285/287 - * - Z3 4.15.4: proves the remaining 2 (div_neg_below_zero and - * mul_monotone_bounds) in under 20 ms combined. - * Every lemma is proved by at least one prover (zero gaps). + * Addition, subtraction, division, modulo, unary minus and increment / + * decrement are verified directly on the Why3 standard library bitvector + * theory (bv.BV8/16/32/64/128) in the generic theory SignedOverflow below: + * a single proof over the abstract bv.BV_Gen covers every width, hence all + * of i8, i16, i32, i64, i128 at once. Detection mirrors the C++ exactly: + * + * signed add overflow same operand signs, flipped result sign + * (sge a zeros = sge b zeros, etc.) + * signed sub overflow different operand signs, result sign != lhs sign + * signed division the sole overflow is INT_MIN / -1; the sole other + * error is divide-by-zero (sdiv / srem, to_int) + * unary minus overflow iff the operand is INT_MIN + * + * Multiplication is the one operation the bitvector standard library cannot + * verify at the result-value level: it exposes to_uint_mul but no + * to_int_mul, and the signed-product correctness goal + * (to_int (mul a b) = to_int a * to_int b when no overflow) is nonlinear and + * does not discharge for widths >= 16 with the available provers (Alt-Ergo, + * Z3; no CVC5 is installed). Multiplication therefore keeps the integer + * model (theories SignedBounds, SignedWrap, SignedMulOverflow), which proves + * full result correctness and overflow detection (wide-multiply and the + * i128 division check) for all widths, with the C++ correspondence + * established by inspection -- the same bridge the integer model uses + * throughout. + * + * Verification: all 69 lemmas are proved using two complementary provers: + * - Alt-Ergo 2.4.3: proves 67/69 + * - Z3 4.15.4: proves the remaining 2 nonlinear goals + * (div_neg_below_zero, mul_monotone_bounds) + * Every lemma is proved by at least one prover (zero gaps). * * why3 prove -P alt-ergo -t 10 -L theorems theorems/signed_integers.why * why3 prove -P z3 -t 30 -L theorems theorems/signed_integers.why *) (* ================================================================ - * Theory: PowerOfTwo - * - * Step-by-step computation of power 2 N for specific bit widths. - * Duplicated from unsigned_integers.why so this file is standalone. - * ================================================================ *) -theory PowerOfTwo - - use int.Int - use int.Power - - lemma p2_1: power 2 1 = 2 - lemma p2_2: power 2 2 = 4 - lemma p2_4: power 2 4 = 16 - lemma p2_7: power 2 7 = 128 - lemma p2_8: power 2 8 = 256 - (* Odd exponents: decompose via Power_sum so Alt-Ergo can close - * the concrete value from the two halves it already knows. *) - lemma p2_15_split: power 2 15 = power 2 7 * power 2 8 - lemma p2_15: power 2 15 = 32768 - lemma p2_16: power 2 16 = 65536 - lemma p2_31_split: power 2 31 = power 2 15 * power 2 16 - lemma p2_31: power 2 31 = 2147483648 - lemma p2_32: power 2 32 = 4294967296 - lemma p2_63_split: power 2 63 = power 2 31 * power 2 32 - lemma p2_63: power 2 63 = 9223372036854775808 - lemma p2_64: power 2 64 = 18446744073709551616 - lemma p2_127_split: power 2 127 = power 2 63 * power 2 64 - lemma p2_127: power 2 127 = 170141183460469231731687303715884105728 - lemma p2_128: power 2 128 = 340282366920938463463374607431768211456 - -end - -(* ================================================================ - * Theory: SignedBounds - * - * The signed N-bit representable range and its basic properties. - * Kept free of any division/mod theory so that the div/mod proof - * theories (which need int.ComputerDivision) can depend on it - * without creating a name clash against int.EuclideanDivision. + * Theory: SignedBounds (integer model, retained for multiplication) * ================================================================ *) theory SignedBounds @@ -198,12 +130,7 @@ theory SignedBounds end (* ================================================================ - * Theory: SignedWrap - * - * Two's complement wrapping interpretation of an arbitrary integer - * into a signed N-bit value. Uses Euclidean mod (non-negative) - * internally. Exposes uview, is_neg_bit, and s_wrap, the primitives - * used to express the C++ bit-pattern detection predicates. + * Theory: SignedWrap (integer model, retained for multiplication) * ================================================================ *) theory SignedWrap @@ -327,251 +254,8 @@ theory SignedWrap end (* ================================================================ - * Theory: SignedAddOverflow - * - * Signed N-bit addition with two's complement wrap and bit-pattern - * overflow detection. - * ================================================================ *) -theory SignedAddOverflow - - use int.Int - use int.Power - use int.EuclideanDivision - use SignedBounds - use SignedWrap - - (* Wrapping signed addition: the signed interpretation of (a+b) mod 2^n *) - function wrap_add_s (a b n: int) : int = s_wrap (a + b) n - - (* True mathematical overflow / underflow *) - predicate add_overflows (a b n: int) = a + b > max_s n - predicate add_underflows (a b n: int) = a + b < min_s n - - (* Bit-pattern detection: signs agree in, signs differ out. - * Models the C++ formula ((~(ulhs^urhs)) & (ulhs^temp)) >> (N-1). - * Reference: signed_integer_basis.hpp line 480 *) - predicate add_detected (a b n: int) = - (is_neg_bit (uview a n) n = is_neg_bit (uview b n) n) /\ - (is_neg_bit (uview a n) n <> is_neg_bit (uview (a + b) n) n) - - (* ---- Helper lemmas ---- *) - - (* Sum bounds for valid operands: a+b in [2*min_s, 2*max_s], - * strictly inside (-2^n, 2^n). *) - lemma sum_bounds_signed: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - 2 * min_s n <= a + b /\ a + b <= 2 * max_s n - - (* Sum is within one modulus of zero: exactly in [-2^n, 2^n - 2]. - * The lower bound is achieved at a = b = min_s n (sum = -2^n), so - * we use <=, not <. *) - lemma sum_in_open_modulus: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - - power 2 n <= a + b /\ a + b < power 2 n - - (* Case quadrants: an overflow only happens when both operands are - * non-negative, and an underflow only when both are negative. *) - lemma overflow_implies_both_nonneg: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - add_overflows a b n -> a >= 0 /\ b >= 0 - - lemma underflow_implies_both_neg: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - add_underflows a b n -> a < 0 /\ b < 0 - - (* When signs differ, no overflow or underflow. *) - lemma diff_signs_no_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - ((a >= 0 /\ b < 0) \/ (a < 0 /\ b >= 0)) -> - not (add_overflows a b n) /\ not (add_underflows a b n) - - (* Sign of (a+b)'s unsigned view in each case *) - lemma uview_sum_nonneg_no_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - a >= 0 -> b >= 0 -> not (add_overflows a b n) -> - not (is_neg_bit (uview (a + b) n) n) - - lemma uview_sum_nonneg_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - a >= 0 -> b >= 0 -> add_overflows a b n -> - is_neg_bit (uview (a + b) n) n - - lemma uview_sum_neg_no_underflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - a < 0 -> b < 0 -> not (add_underflows a b n) -> - is_neg_bit (uview (a + b) n) n - - lemma uview_sum_neg_underflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - a < 0 -> b < 0 -> add_underflows a b n -> - not (is_neg_bit (uview (a + b) n) n) - - lemma uview_sum_diff_signs: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - ((a >= 0 /\ b < 0) \/ (a < 0 /\ b >= 0)) -> - (is_neg_bit (uview (a + b) n) n <-> a + b < 0) - - (* ---- Main Theorems ---- *) - - (* Theorem 1 (Soundness): true overflow/underflow implies detection. *) - lemma add_soundness: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - (add_overflows a b n \/ add_underflows a b n) -> - add_detected a b n - - (* Theorem 2 (No false positives): no overflow/underflow implies no detection. *) - lemma add_no_false_positives: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - not (add_overflows a b n) -> not (add_underflows a b n) -> - not (add_detected a b n) - - (* Theorem 3 (Correctness): when no overflow/underflow, wrap = true sum. *) - lemma add_correctness: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - not (add_overflows a b n) -> not (add_underflows a b n) -> - wrap_add_s a b n = a + b - - (* Theorem 4 (Biconditional): detection iff overflow or underflow. *) - lemma add_biconditional: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - (add_detected a b n <-> (add_overflows a b n \/ add_underflows a b n)) - - (* Theorem 5 (Direction classification): when detection fires, the - * sign of lhs correctly identifies overflow vs underflow. - * Models: classify_signed_overflow(lhs) at line 390. *) - lemma classify_direction_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - add_overflows a b n -> a >= 0 - - lemma classify_direction_underflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - add_underflows a b n -> a < 0 - -end - -(* ================================================================ - * Theory: SignedSubOverflow - * - * Signed N-bit subtraction with two's complement wrap and bit-pattern - * overflow detection. - * ================================================================ *) -theory SignedSubOverflow - - use int.Int - use int.Power - use int.EuclideanDivision - use SignedBounds - use SignedWrap - - function wrap_sub_s (a b n: int) : int = s_wrap (a - b) n - - predicate sub_overflows (a b n: int) = a - b > max_s n - predicate sub_underflows (a b n: int) = a - b < min_s n - - (* Subtraction detection: signs differ in, lhs differs from result out. - * Models: ((ulhs ^ urhs) & (ulhs ^ temp)) >> (N-1). - * Reference: signed_integer_basis.hpp line 1093 *) - predicate sub_detected (a b n: int) = - (is_neg_bit (uview a n) n <> is_neg_bit (uview b n) n) /\ - (is_neg_bit (uview a n) n <> is_neg_bit (uview (a - b) n) n) - - (* ---- Helper lemmas ---- *) - - lemma diff_bounds_signed: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - min_s n - max_s n <= a - b /\ a - b <= max_s n - min_s n - - lemma diff_in_open_modulus: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - - power 2 n < a - b /\ a - b < power 2 n - - lemma sub_overflow_needs_pos_neg: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - sub_overflows a b n -> a >= 0 /\ b < 0 - - lemma sub_underflow_needs_neg_pos: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - sub_underflows a b n -> a < 0 /\ b >= 0 - - lemma sub_same_signs_no_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - ((a >= 0 /\ b >= 0) \/ (a < 0 /\ b < 0)) -> - not (sub_overflows a b n) /\ not (sub_underflows a b n) - - (* Sign of the unsigned view of a-b in each quadrant *) - lemma uview_diff_same_sign: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - ((a >= 0 /\ b >= 0) \/ (a < 0 /\ b < 0)) -> - (is_neg_bit (uview (a - b) n) n <-> a - b < 0) - - lemma uview_diff_pos_neg_no_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - a >= 0 -> b < 0 -> not (sub_overflows a b n) -> - not (is_neg_bit (uview (a - b) n) n) - - lemma uview_diff_pos_neg_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - a >= 0 -> b < 0 -> sub_overflows a b n -> - is_neg_bit (uview (a - b) n) n - - lemma uview_diff_neg_pos_no_underflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - a < 0 -> b >= 0 -> not (sub_underflows a b n) -> - is_neg_bit (uview (a - b) n) n - - lemma uview_diff_neg_pos_underflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - a < 0 -> b >= 0 -> sub_underflows a b n -> - not (is_neg_bit (uview (a - b) n) n) - - (* ---- Main Theorems ---- *) - - lemma sub_soundness: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - (sub_overflows a b n \/ sub_underflows a b n) -> - sub_detected a b n - - lemma sub_no_false_positives: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - not (sub_overflows a b n) -> not (sub_underflows a b n) -> - not (sub_detected a b n) - - lemma sub_correctness: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - not (sub_overflows a b n) -> not (sub_underflows a b n) -> - wrap_sub_s a b n = a - b - - lemma sub_biconditional: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - (sub_detected a b n <-> (sub_overflows a b n \/ sub_underflows a b n)) - - (* Direction classification for subtraction uses lhs's sign. *) - lemma sub_classify_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - sub_overflows a b n -> a >= 0 - - lemma sub_classify_underflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - sub_underflows a b n -> a < 0 - -end - -(* ================================================================ - * Theory: SignedMulOverflow - * - * Signed N-bit multiplication. Two detection strategies are used in - * the C++ code (both proved correct here): - * - * 1. Wide multiplication (i8, i16, i32, i64) -- lines 1609-1656: - * Promote to a wider signed type that can hold a*b exactly, then - * check temp > max() or temp < min(). Justified by wide_mul_safe_s - * (the product fits in 2N bits). - * - * 2. Absolute-value division check (i128) -- lines 1573-1608: - * abs_lhs = |a|, abs_rhs = |b| (computed via two's complement in - * the C++ code, modeled as abs_s in Why3); max_magnitude is max() - * when signs agree and |min()| when signs differ; overflow iff - * abs_rhs != 0 && abs_lhs > max_magnitude / abs_rhs. + * Theory: SignedMulOverflow (integer model: full multiplication + * correctness + overflow detection for all widths) * ================================================================ *) theory SignedMulOverflow @@ -714,872 +398,49 @@ theory SignedMulOverflow end (* ================================================================ - * Theory: SignedDivSafety - * - * Signed integer division. Uses C-style truncated division - * (int.ComputerDivision) to match C++ operator/ semantics. - * - * The two error conditions are: - * - rhs == 0 -> std::domain_error - * - lhs == min && rhs == -1 -> std::overflow_error - * - * For all other valid operand pairs, the truncated quotient is a - * valid signed N-bit value. - * Reference: signed_integer_basis.hpp lines 2040-2149 - * ================================================================ *) -theory SignedDivSafety - - use int.Int - use int.Power - use int.ComputerDivision - use SignedBounds - - (* Truncated-toward-zero division / modulo. Matches C++ semantics. *) - function sdiv (a b: int) : int = div a b - - (* The complete error predicate for signed division. *) - predicate div_error_s (a b n: int) = - b = 0 \/ (a = min_s n /\ b = -1) - - (* ---- Helper lemmas about truncated division ---- *) - - (* For b != 0, |a/b| <= |a|, except in the min/-1 case where the - * result overflows (|min/-1| = |min| = max + 1). *) - lemma sdiv_abs_le: - forall a b: int. b <> 0 -> abs_s (div a b) <= abs_s a - - lemma sdiv_nonneg_when_same_sign: - forall a b: int. b <> 0 -> (a >= 0) = (b >= 0) -> div a b >= 0 - - lemma sdiv_nonpos_when_diff_sign: - forall a b: int. b <> 0 -> (a >= 0) <> (b >= 0) -> div a b <= 0 - - lemma sdiv_by_one: - forall a: int. div a 1 = a - - lemma sdiv_by_neg_one: - forall a: int. div a (-1) = - a - - (* Special case: min / -1 = -min = 2^(n-1) = max + 1 > max. *) - lemma sdiv_min_neg_one_equals_neg_min: - forall n: int. n >= 1 -> div (min_s n) (-1) = - min_s n - - lemma sdiv_min_neg_one_equals_half: - forall n: int. n >= 1 -> div (min_s n) (-1) = power 2 (n - 1) - - lemma sdiv_min_neg_one_overflows: - forall n: int. n >= 1 -> div (min_s n) (-1) > max_s n - - (* Abs bound when not in the min/-1 case: |a/b| <= 2^(n-1). - * The tight bound is |min_s / 1| = 2^(n-1) = max_s + 1, so we - * cannot strengthen to max_s without excluding that boundary. *) - lemma sdiv_abs_bounded: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - b <> 0 -> not (a = min_s n /\ b = -1) -> - abs_s (div a b) <= power 2 (n - 1) - - (* ---- Main Theorems ---- *) - - (* Theorem 1 (Result validity): for non-error inputs, sdiv is valid. *) - lemma sdiv_result_valid: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - not (div_error_s a b n) -> - valid_s (sdiv a b) n - - (* Theorem 2 (Correctness): sdiv is the true truncated quotient. *) - lemma sdiv_correctness: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - not (div_error_s a b n) -> - sdiv a b = div a b - - (* Theorem 3 (Error completeness): the C++ checks (rhs==0 OR min/-1) - * catch exactly the cases where no valid result exists. *) - lemma sdiv_error_complete: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - div_error_s a b n <-> - (b = 0 \/ (b <> 0 /\ not (valid_s (div a b) n))) - - (* Theorem 4 (Min/-1 is the only overflowing division). *) - lemma sdiv_unique_overflow: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - b <> 0 -> not (valid_s (div a b) n) -> - a = min_s n /\ b = -1 - -end - -(* ================================================================ - * Theory: SignedModSafety - * - * Signed integer modulo with C-style truncated remainder (same sign - * as dividend, |a%b| < |b|). The error conditions match those of - * division: rhs==0 (domain_error) and min%-1 (treated as overflow - * even though the mathematical remainder is 0, to match C++ UB). - * Reference: signed_integer_basis.hpp lines 2305-2500 - * ================================================================ *) -theory SignedModSafety - - use int.Int - use int.Power - use int.ComputerDivision - use SignedBounds - - function smod (a b: int) : int = mod a b - - predicate mod_error_s (a b n: int) = - b = 0 \/ (a = min_s n /\ b = -1) - - (* ---- Helper lemmas: ComputerDivision properties ---- *) - - lemma smod_abs_lt_divisor: - forall a b: int. b <> 0 -> abs_s (mod a b) < abs_s b - - lemma smod_sign_matches_dividend: - forall a b: int. b <> 0 -> - (a >= 0 -> mod a b >= 0) /\ (a < 0 -> mod a b <= 0) - - (* Mathematically min % -1 = 0, but the library rejects this case - * to stay consistent with min / -1 being rejected. *) - lemma smod_min_neg_one_is_zero_math: - forall n: int. n >= 1 -> mod (min_s n) (-1) = 0 - - lemma smod_div_mod_relation: - forall a b: int. b <> 0 -> a = div a b * b + mod a b - - (* Abs bound: |a%b| <= max_s n when b is a valid signed value. *) - lemma smod_abs_bounded: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - b <> 0 -> - abs_s (mod a b) <= max_s n - - (* ---- Main Theorems ---- *) - - lemma smod_result_valid: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - not (mod_error_s a b n) -> - valid_s (smod a b) n - - lemma smod_correctness: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - not (mod_error_s a b n) -> - smod a b = mod a b - - lemma smod_result_always_valid_when_b_nonzero: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - b <> 0 -> - valid_s (mod a b) n - - lemma smod_error_complete: - forall a b n: int. n >= 1 -> valid_s a n -> valid_s b n -> - (mod_error_s a b n -> b = 0 \/ (a = min_s n /\ b = -1)) - -end - -(* ================================================================ - * Theory: SignedUnaryMinus - * - * Unary negation for signed N-bit integers. The only overflow case - * is -min_s = 2^(n-1) = max_s + 1, which is unrepresentable. - * Reference: signed_integer_basis.hpp lines 348-356 + * Theory: SignedOverflow (bitvector stdlib model: add, sub, div, + * mod, unary minus, inc/dec, generic over all bit widths) * ================================================================ *) -theory SignedUnaryMinus - +theory SignedOverflow + clone export bv.BV_Gen with axiom . use int.Int - use int.Power - use SignedBounds - - predicate unary_minus_error (a n: int) = a = min_s n - - lemma neg_valid_when_not_min: - forall a n: int. n >= 1 -> valid_s a n -> a <> min_s n -> - valid_s (- a) n - - lemma neg_min_unrepresentable: - forall n: int. n >= 1 -> - min_s n = max_s n + 1 /\ max_s n + 1 > max_s n - - lemma unary_minus_error_iff: - forall a n: int. n >= 1 -> valid_s a n -> - (unary_minus_error a n <-> not (valid_s (- a) n)) - - lemma neg_correctness_when_not_min: - forall a n: int. n >= 1 -> valid_s a n -> a <> min_s n -> - - (- a) = a - -end - -(* ================================================================ - * Theory: SignedIncDec - * - * Increment overflows at max_s; decrement underflows at min_s. - * Reference: signed_integer_basis.hpp lines 2578-2636 - * ================================================================ *) -theory SignedIncDec - - use int.Int - use int.Power - use SignedBounds - - predicate inc_error (a n: int) = a = max_s n - predicate dec_error (a n: int) = a = min_s n - - lemma inc_valid_iff_not_max: - forall a n: int. n >= 1 -> valid_s a n -> - (valid_s (a + 1) n <-> a <> max_s n) - - lemma dec_valid_iff_not_min: - forall a n: int. n >= 1 -> valid_s a n -> - (valid_s (a - 1) n <-> a <> min_s n) - - lemma inc_overflows_only_at_max: - forall a n: int. n >= 1 -> valid_s a n -> - a + 1 > max_s n <-> a = max_s n - - lemma dec_underflows_only_at_min: - forall a n: int. n >= 1 -> valid_s a n -> - a - 1 < min_s n <-> a = min_s n - -end - -(* ================================================================ - * Theory: SignedI8 - * - * Concrete instantiation for int8_t (N = 8, range [-128, 127]). - * Models: boost::safe_numbers::i8 - * = detail::signed_integer_basis - * Reference: signed_integers.hpp line 21 - * ================================================================ *) -theory SignedI8 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use SignedBounds - use SignedWrap - use SignedAddOverflow - use SignedSubOverflow - use SignedMulOverflow - use SignedDivSafety - use SignedModSafety - use SignedUnaryMinus - use SignedIncDec - - constant n8 : int = 8 - - lemma n8_valid: n8 >= 1 - - lemma i8_max: max_s n8 = 127 - lemma i8_min: min_s n8 = -128 - - (* ---- Addition ---- *) - - lemma i8_add_soundness: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - (add_overflows a b n8 \/ add_underflows a b n8) -> - add_detected a b n8 - - lemma i8_add_no_false_positives: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - not (add_overflows a b n8) -> not (add_underflows a b n8) -> - not (add_detected a b n8) - - lemma i8_add_correctness: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - not (add_overflows a b n8) -> not (add_underflows a b n8) -> - wrap_add_s a b n8 = a + b - - lemma i8_add_biconditional: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - (add_detected a b n8 <-> (add_overflows a b n8 \/ add_underflows a b n8)) - - (* Addition boundary tests *) - lemma i8_add_max_plus_one: add_overflows 127 1 n8 - lemma i8_add_max_plus_zero: not (add_overflows 127 0 n8) - lemma i8_add_min_plus_neg_one: add_underflows (-128) (-1) n8 - lemma i8_add_min_plus_zero: not (add_underflows (-128) 0 n8) - lemma i8_add_half_plus_half: add_overflows 64 64 n8 - lemma i8_add_half_plus_half_valid: not (add_overflows 64 63 n8) - - (* ---- Subtraction ---- *) - - lemma i8_sub_soundness: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - (sub_overflows a b n8 \/ sub_underflows a b n8) -> - sub_detected a b n8 - - lemma i8_sub_no_false_positives: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - not (sub_overflows a b n8) -> not (sub_underflows a b n8) -> - not (sub_detected a b n8) - - lemma i8_sub_correctness: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - not (sub_overflows a b n8) -> not (sub_underflows a b n8) -> - wrap_sub_s a b n8 = a - b - - lemma i8_sub_biconditional: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - (sub_detected a b n8 <-> (sub_overflows a b n8 \/ sub_underflows a b n8)) - - (* Subtraction boundary tests *) - lemma i8_sub_min_minus_one: sub_underflows (-128) 1 n8 - lemma i8_sub_min_minus_zero: not (sub_underflows (-128) 0 n8) - lemma i8_sub_max_minus_neg_one: sub_overflows 127 (-1) n8 - lemma i8_sub_zero_minus_min: sub_overflows 0 (-128) n8 - - (* ---- Multiplication ---- *) - - lemma i8_mul_correctness: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - not (mul_overflows_s a b n8) -> - wrap_mul_s a b n8 = a * b - - lemma i8_mul_wide_safe: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - min_s (2 * n8) <= a * b /\ a * b <= max_s (2 * n8) - - lemma i8_mul_div_check: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - (signed_div_check a b n8 <-> mul_overflows_s a b n8) - - (* Multiplication boundary tests *) - lemma i8_mul_half_squared: mul_overflows_s 12 12 n8 (* 144 > 127 *) - lemma i8_mul_half_squared_pos: not (mul_overflows_s 11 11 n8) (* 121 valid *) - lemma i8_mul_neg_half_squared: mul_overflows_s (-12) (-12) n8 - lemma i8_mul_min_by_neg_one: mul_overflows_s (-128) (-1) n8 - lemma i8_mul_min_by_two: mul_overflows_s (-128) 2 n8 - lemma i8_mul_by_zero: not (mul_overflows_s 127 0 n8) - lemma i8_mul_min_by_zero: not (mul_overflows_s (-128) 0 n8) - - (* ---- Division ---- *) - - lemma i8_div_result_valid: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - not (div_error_s a b n8) -> - valid_s (sdiv a b) n8 - - lemma i8_div_error_complete: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - div_error_s a b n8 <-> - (b = 0 \/ (b <> 0 /\ not (valid_s (sdiv a b) n8))) - - (* Division boundary tests *) - lemma i8_div_min_by_neg_one_is_error: div_error_s (-128) (-1) n8 - lemma i8_div_min_by_one: not (div_error_s (-128) 1 n8) - lemma i8_div_max_by_neg_one: not (div_error_s 127 (-1) n8) - lemma i8_div_by_zero: div_error_s 5 0 n8 - - (* ---- Modulo ---- *) - - lemma i8_mod_result_valid: - forall a b: int. valid_s a n8 -> valid_s b n8 -> - not (mod_error_s a b n8) -> - valid_s (smod a b) n8 - - (* Modulo boundary tests *) - lemma i8_mod_min_by_neg_one_is_error: mod_error_s (-128) (-1) n8 - lemma i8_mod_by_zero: mod_error_s 5 0 n8 - - (* ---- Unary Minus ---- *) - - lemma i8_neg_min_is_error: unary_minus_error (-128) n8 - - lemma i8_neg_min_unrepresentable: - - min_s n8 = max_s n8 + 1 - - lemma i8_neg_max_valid: valid_s (-(127)) n8 - lemma i8_neg_zero_valid: valid_s (-0) n8 - - (* ---- Increment / Decrement ---- *) - - lemma i8_inc_max_errors: inc_error (max_s n8) n8 - lemma i8_dec_min_errors: dec_error (min_s n8) n8 - - lemma i8_inc_max_overflows: 127 + 1 > max_s n8 - lemma i8_dec_min_underflows: -128 - 1 < min_s n8 - -end - -(* ================================================================ - * Theory: SignedI16 - * - * Concrete instantiation for int16_t (N = 16, range [-32768, 32767]). - * Models: boost::safe_numbers::i16 - * Reference: signed_integers.hpp line 23 - * ================================================================ *) -theory SignedI16 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use SignedBounds - use SignedWrap - use SignedAddOverflow - use SignedSubOverflow - use SignedMulOverflow - use SignedDivSafety - use SignedModSafety - use SignedUnaryMinus - use SignedIncDec - - constant n16 : int = 16 - - lemma n16_valid: n16 >= 1 - lemma i16_max: max_s n16 = 32767 - lemma i16_min: min_s n16 = -32768 - - (* ---- Addition ---- *) - - lemma i16_add_soundness: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - (add_overflows a b n16 \/ add_underflows a b n16) -> - add_detected a b n16 - - lemma i16_add_no_false_positives: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - not (add_overflows a b n16) -> not (add_underflows a b n16) -> - not (add_detected a b n16) - - lemma i16_add_correctness: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - not (add_overflows a b n16) -> not (add_underflows a b n16) -> - wrap_add_s a b n16 = a + b - - lemma i16_add_biconditional: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - (add_detected a b n16 <-> (add_overflows a b n16 \/ add_underflows a b n16)) - - lemma i16_add_max_plus_one: add_overflows 32767 1 n16 - lemma i16_add_min_plus_neg_one: add_underflows (-32768) (-1) n16 - - (* ---- Subtraction ---- *) - - lemma i16_sub_soundness: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - (sub_overflows a b n16 \/ sub_underflows a b n16) -> - sub_detected a b n16 - - lemma i16_sub_no_false_positives: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - not (sub_overflows a b n16) -> not (sub_underflows a b n16) -> - not (sub_detected a b n16) - - lemma i16_sub_correctness: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - not (sub_overflows a b n16) -> not (sub_underflows a b n16) -> - wrap_sub_s a b n16 = a - b - - lemma i16_sub_biconditional: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - (sub_detected a b n16 <-> (sub_overflows a b n16 \/ sub_underflows a b n16)) - - lemma i16_sub_min_minus_one: sub_underflows (-32768) 1 n16 - lemma i16_sub_max_minus_neg_one: sub_overflows 32767 (-1) n16 - - (* ---- Multiplication ---- *) - - lemma i16_mul_correctness: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - not (mul_overflows_s a b n16) -> - wrap_mul_s a b n16 = a * b - - lemma i16_mul_wide_safe: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - min_s (2 * n16) <= a * b /\ a * b <= max_s (2 * n16) - - lemma i16_mul_div_check: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - (signed_div_check a b n16 <-> mul_overflows_s a b n16) - - lemma i16_mul_min_by_neg_one: mul_overflows_s (-32768) (-1) n16 - lemma i16_mul_half_overflow: mul_overflows_s 256 128 n16 - lemma i16_mul_by_zero: not (mul_overflows_s 32767 0 n16) - - (* ---- Division ---- *) - - lemma i16_div_result_valid: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - not (div_error_s a b n16) -> - valid_s (sdiv a b) n16 - - lemma i16_div_min_by_neg_one_is_error: div_error_s (-32768) (-1) n16 - - (* ---- Modulo ---- *) - - lemma i16_mod_result_valid: - forall a b: int. valid_s a n16 -> valid_s b n16 -> - not (mod_error_s a b n16) -> - valid_s (smod a b) n16 - - lemma i16_mod_min_by_neg_one_is_error: mod_error_s (-32768) (-1) n16 - - (* ---- Unary Minus / Inc / Dec ---- *) - - lemma i16_neg_min_is_error: unary_minus_error (-32768) n16 - lemma i16_inc_max_errors: inc_error (max_s n16) n16 - lemma i16_dec_min_errors: dec_error (min_s n16) n16 - -end - -(* ================================================================ - * Theory: SignedI32 - * - * Concrete instantiation for int32_t (N = 32). - * Models: boost::safe_numbers::i32 - * Reference: signed_integers.hpp line 25 - * ================================================================ *) -theory SignedI32 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use SignedBounds - use SignedWrap - use SignedAddOverflow - use SignedSubOverflow - use SignedMulOverflow - use SignedDivSafety - use SignedModSafety - use SignedUnaryMinus - use SignedIncDec - - constant n32 : int = 32 - - lemma n32_valid: n32 >= 1 - lemma i32_max: max_s n32 = 2147483647 - lemma i32_min: min_s n32 = -2147483648 - - (* ---- Addition ---- *) - - lemma i32_add_soundness: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - (add_overflows a b n32 \/ add_underflows a b n32) -> - add_detected a b n32 - - lemma i32_add_no_false_positives: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - not (add_overflows a b n32) -> not (add_underflows a b n32) -> - not (add_detected a b n32) - - lemma i32_add_correctness: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - not (add_overflows a b n32) -> not (add_underflows a b n32) -> - wrap_add_s a b n32 = a + b - - lemma i32_add_biconditional: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - (add_detected a b n32 <-> (add_overflows a b n32 \/ add_underflows a b n32)) - - lemma i32_add_max_plus_one: add_overflows 2147483647 1 n32 - lemma i32_add_min_plus_neg_one: add_underflows (-2147483648) (-1) n32 - - (* ---- Subtraction ---- *) - - lemma i32_sub_soundness: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - (sub_overflows a b n32 \/ sub_underflows a b n32) -> - sub_detected a b n32 - - lemma i32_sub_no_false_positives: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - not (sub_overflows a b n32) -> not (sub_underflows a b n32) -> - not (sub_detected a b n32) - - lemma i32_sub_correctness: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - not (sub_overflows a b n32) -> not (sub_underflows a b n32) -> - wrap_sub_s a b n32 = a - b - - lemma i32_sub_biconditional: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - (sub_detected a b n32 <-> (sub_overflows a b n32 \/ sub_underflows a b n32)) - - (* ---- Multiplication ---- *) - - lemma i32_mul_correctness: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - not (mul_overflows_s a b n32) -> - wrap_mul_s a b n32 = a * b - - lemma i32_mul_wide_safe: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - min_s (2 * n32) <= a * b /\ a * b <= max_s (2 * n32) - - lemma i32_mul_div_check: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - (signed_div_check a b n32 <-> mul_overflows_s a b n32) - - lemma i32_mul_min_by_neg_one: mul_overflows_s (-2147483648) (-1) n32 - lemma i32_mul_by_zero: not (mul_overflows_s 2147483647 0 n32) - - (* ---- Division ---- *) - - lemma i32_div_result_valid: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - not (div_error_s a b n32) -> - valid_s (sdiv a b) n32 - - lemma i32_div_min_by_neg_one_is_error: div_error_s (-2147483648) (-1) n32 - - (* ---- Modulo ---- *) - - lemma i32_mod_result_valid: - forall a b: int. valid_s a n32 -> valid_s b n32 -> - not (mod_error_s a b n32) -> - valid_s (smod a b) n32 - - lemma i32_mod_min_by_neg_one_is_error: mod_error_s (-2147483648) (-1) n32 - - (* ---- Unary Minus / Inc / Dec ---- *) - - lemma i32_neg_min_is_error: unary_minus_error (-2147483648) n32 - lemma i32_inc_max_errors: inc_error (max_s n32) n32 - lemma i32_dec_min_errors: dec_error (min_s n32) n32 - -end - -(* ================================================================ - * Theory: SignedI64 - * - * Concrete instantiation for int64_t (N = 64). - * Models: boost::safe_numbers::i64 - * Reference: signed_integers.hpp line 27 - * ================================================================ *) -theory SignedI64 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use SignedBounds - use SignedWrap - use SignedAddOverflow - use SignedSubOverflow - use SignedMulOverflow - use SignedDivSafety - use SignedModSafety - use SignedUnaryMinus - use SignedIncDec - - constant n64 : int = 64 - - lemma n64_valid: n64 >= 1 - lemma i64_max: max_s n64 = 9223372036854775807 - lemma i64_min: min_s n64 = -9223372036854775808 - - (* ---- Addition ---- *) - - lemma i64_add_soundness: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - (add_overflows a b n64 \/ add_underflows a b n64) -> - add_detected a b n64 - - lemma i64_add_no_false_positives: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - not (add_overflows a b n64) -> not (add_underflows a b n64) -> - not (add_detected a b n64) - - lemma i64_add_correctness: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - not (add_overflows a b n64) -> not (add_underflows a b n64) -> - wrap_add_s a b n64 = a + b - - lemma i64_add_biconditional: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - (add_detected a b n64 <-> (add_overflows a b n64 \/ add_underflows a b n64)) - - lemma i64_add_max_plus_one: add_overflows 9223372036854775807 1 n64 - lemma i64_add_min_plus_neg_one: add_underflows (-9223372036854775808) (-1) n64 - - (* ---- Subtraction ---- *) - - lemma i64_sub_soundness: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - (sub_overflows a b n64 \/ sub_underflows a b n64) -> - sub_detected a b n64 - - lemma i64_sub_no_false_positives: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - not (sub_overflows a b n64) -> not (sub_underflows a b n64) -> - not (sub_detected a b n64) - - lemma i64_sub_correctness: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - not (sub_overflows a b n64) -> not (sub_underflows a b n64) -> - wrap_sub_s a b n64 = a - b - - lemma i64_sub_biconditional: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - (sub_detected a b n64 <-> (sub_overflows a b n64 \/ sub_underflows a b n64)) - - (* ---- Multiplication ---- *) - - lemma i64_mul_correctness: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - not (mul_overflows_s a b n64) -> - wrap_mul_s a b n64 = a * b - - lemma i64_mul_wide_safe: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - min_s (2 * n64) <= a * b /\ a * b <= max_s (2 * n64) - - lemma i64_mul_div_check: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - (signed_div_check a b n64 <-> mul_overflows_s a b n64) - - lemma i64_mul_min_by_neg_one: mul_overflows_s (-9223372036854775808) (-1) n64 - lemma i64_mul_by_zero: not (mul_overflows_s 9223372036854775807 0 n64) - - (* ---- Division ---- *) - - lemma i64_div_result_valid: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - not (div_error_s a b n64) -> - valid_s (sdiv a b) n64 - - lemma i64_div_min_by_neg_one_is_error: div_error_s (-9223372036854775808) (-1) n64 - - (* ---- Modulo ---- *) - - lemma i64_mod_result_valid: - forall a b: int. valid_s a n64 -> valid_s b n64 -> - not (mod_error_s a b n64) -> - valid_s (smod a b) n64 - - lemma i64_mod_min_by_neg_one_is_error: mod_error_s (-9223372036854775808) (-1) n64 - - (* ---- Unary Minus / Inc / Dec ---- *) - - lemma i64_neg_min_is_error: unary_minus_error (-9223372036854775808) n64 - lemma i64_inc_max_errors: inc_error (max_s n64) n64 - lemma i64_dec_min_errors: dec_error (min_s n64) n64 - -end - -(* ================================================================ - * Theory: SignedI128 - * - * Concrete instantiation for int128_t (N = 128). - * Models: boost::safe_numbers::i128 - * = detail::signed_integer_basis - * Reference: signed_integers.hpp line 29 - * - * Note: multiplication uses the division-check path exclusively - * (no wider type available). Reference: signed_integer_basis.hpp - * lines 1573-1608. - * ================================================================ *) -theory SignedI128 - - use int.Int - use int.Power - use int.EuclideanDivision - use PowerOfTwo - use SignedBounds - use SignedWrap - use SignedAddOverflow - use SignedSubOverflow - use SignedMulOverflow - use SignedDivSafety - use SignedModSafety - use SignedUnaryMinus - use SignedIncDec - - constant n128 : int = 128 - - lemma n128_valid: n128 >= 1 - lemma i128_max: max_s n128 = 170141183460469231731687303715884105727 - lemma i128_min: min_s n128 = -170141183460469231731687303715884105728 - - (* ---- Addition ---- *) - - lemma i128_add_soundness: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - (add_overflows a b n128 \/ add_underflows a b n128) -> - add_detected a b n128 - - lemma i128_add_no_false_positives: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - not (add_overflows a b n128) -> not (add_underflows a b n128) -> - not (add_detected a b n128) - - lemma i128_add_correctness: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - not (add_overflows a b n128) -> not (add_underflows a b n128) -> - wrap_add_s a b n128 = a + b - - lemma i128_add_biconditional: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - (add_detected a b n128 <-> (add_overflows a b n128 \/ add_underflows a b n128)) - - lemma i128_add_max_plus_one: - add_overflows 170141183460469231731687303715884105727 1 n128 - lemma i128_add_min_plus_neg_one: - add_underflows (-170141183460469231731687303715884105728) (-1) n128 - - (* ---- Subtraction ---- *) - - lemma i128_sub_soundness: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - (sub_overflows a b n128 \/ sub_underflows a b n128) -> - sub_detected a b n128 - - lemma i128_sub_no_false_positives: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - not (sub_overflows a b n128) -> not (sub_underflows a b n128) -> - not (sub_detected a b n128) - - lemma i128_sub_correctness: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - not (sub_overflows a b n128) -> not (sub_underflows a b n128) -> - wrap_sub_s a b n128 = a - b - - lemma i128_sub_biconditional: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - (sub_detected a b n128 <-> (sub_overflows a b n128 \/ sub_underflows a b n128)) - - (* ---- Multiplication (division-check path only for i128) ---- *) - - lemma i128_mul_correctness: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - not (mul_overflows_s a b n128) -> - wrap_mul_s a b n128 = a * b - - lemma i128_mul_div_check: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - (signed_div_check a b n128 <-> mul_overflows_s a b n128) - - lemma i128_mul_min_by_neg_one: - mul_overflows_s (-170141183460469231731687303715884105728) (-1) n128 - lemma i128_mul_by_zero: - not (mul_overflows_s 170141183460469231731687303715884105727 0 n128) - - (* ---- Division ---- *) - - lemma i128_div_result_valid: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - not (div_error_s a b n128) -> - valid_s (sdiv a b) n128 - - - lemma i128_div_min_by_neg_one_is_error: - div_error_s (-170141183460469231731687303715884105728) (-1) n128 - - (* ---- Modulo ---- *) - - lemma i128_mod_result_valid: - forall a b: int. valid_s a n128 -> valid_s b n128 -> - not (mod_error_s a b n128) -> - valid_s (smod a b) n128 - - lemma i128_mod_min_by_neg_one_is_error: - mod_error_s (-170141183460469231731687303715884105728) (-1) n128 - - (* ---- Unary Minus / Inc / Dec ---- *) - - lemma i128_neg_min_is_error: - unary_minus_error (-170141183460469231731687303715884105728) n128 - lemma i128_inc_max_errors: inc_error (max_s n128) n128 - lemma i128_dec_min_errors: dec_error (min_s n128) n128 - + use int.ComputerDivision as CD + + (* ---- Addition: sign-bit overflow detection (same input signs, flipped result sign) ---- *) + predicate sadd_detected (a b : t) = + (sge a zeros = sge b zeros) /\ (sge a zeros <> sge (add a b) zeros) + predicate sadd_overflows (a b : t) = + to_int a + to_int b < - two_power_size_minus_one \/ to_int a + to_int b >= two_power_size_minus_one + lemma sadd_biconditional : forall a b : t. sadd_detected a b <-> sadd_overflows a b + lemma sadd_correctness : forall a b : t. not (sadd_overflows a b) -> to_int (add a b) = to_int a + to_int b + + (* ---- Subtraction: different input signs, result sign differs from lhs ---- *) + predicate ssub_detected (a b : t) = + (sge a zeros <> sge b zeros) /\ (sge a zeros <> sge (sub a b) zeros) + predicate ssub_overflows (a b : t) = + to_int a - to_int b < - two_power_size_minus_one \/ to_int a - to_int b >= two_power_size_minus_one + lemma ssub_biconditional : forall a b : t. ssub_detected a b <-> ssub_overflows a b + lemma ssub_correctness : forall a b : t. not (ssub_overflows a b) -> to_int (sub a b) = to_int a - to_int b + + (* ---- Division: errors are divide-by-zero and INT_MIN / -1 ---- *) + predicate sdiv_overflows (a b : t) = to_int a = - two_power_size_minus_one /\ to_int b = -1 + lemma sdiv_correctness : forall a b : t. + to_int b <> 0 -> not (sdiv_overflows a b) -> to_int (sdiv a b) = CD.div (to_int a) (to_int b) + lemma sdiv_result_valid : forall a b : t. + to_int b <> 0 -> not (sdiv_overflows a b) -> + - two_power_size_minus_one <= to_int (sdiv a b) < two_power_size_minus_one + + (* ---- Modulo: remainder always valid; matches ComputerDivision ---- *) + lemma srem_correctness : forall a b : t. to_int b <> 0 -> to_int (srem a b) = CD.mod (to_int a) (to_int b) + + (* ---- Unary minus: overflow iff at INT_MIN ---- *) + predicate neg_overflows (a : t) = to_int a = - two_power_size_minus_one + lemma neg_detect : forall a : t. (to_int (neg a) <> - to_int a) <-> neg_overflows a + lemma neg_correctness : forall a : t. not (neg_overflows a) -> to_int (neg a) = - to_int a + + (* ---- Increment / decrement (operand of magnitude 1) ---- *) + lemma inc_biconditional : forall a b : t. to_int b = 1 -> + ((to_int (add a b) <> to_int a + 1) <-> (to_int a = two_power_size_minus_one - 1)) + lemma dec_biconditional : forall a b : t. to_int b = 1 -> + ((to_int (sub a b) <> to_int a - 1) <-> (to_int a = - two_power_size_minus_one)) end