Upstream lemmas for bitwise arithmetic

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -5,6 +5,7 @@ requires "kmir-ast.md"
 requires "rt/data.md"
 requires "rt/configuration.md"
 requires "lemmas/kmir-lemmas.md"
+requires "lemmas/bitwise-lemmas.md"
 requires "cheatcodes.md"
 requires "intrinsics.md"
 ```
@@ -730,7 +731,7 @@ endmodule
 
 ## Top-level Module
 
-The top-level module `KMIR` includes both the control flow constructs (and transitively all modules related to runtime operations and AST) and a collection of simplification lemmas required for symbolic execution of MIR programs.
+The top-level module `KMIR` includes both the control flow constructs (and transitively all modules related to runtime operations and AST) and collections of simplification lemmas required for symbolic execution of MIR programs.
 
 ```k
 module KMIR
@@ -739,4 +740,5 @@ module KMIR
   imports KMIR-CHEATCODES
   imports KMIR-INTRINSICS
   imports KMIR-LEMMAS
+  imports KMIR-BITWISE-LEMMAS
 endmodule

kmir/src/kmir/kdist/mir-semantics/lemmas/bitwise-lemmas.md

@@ -0,0 +1,147 @@
+# Bitwise lemmas for MIR symbolic execution
+
+This file contains lemmas that rewrite bitwise operations on integers into arithmetic, and that bound the results of
+bitwise operations. They are imported into the `KMIR` module alongside the lemmas in `kmir-lemmas.md`.
+
+```k
+module KMIR-BITWISE-LEMMAS
+  imports INT
+  imports INT-SYMBOLIC
+  imports BOOL
+```
+
+The SMT solver treats `&Int`, `|Int`, `>>Int` and `<<Int` as uninterpreted functions, but `modInt` and `divInt` map to
+SMT `mod` and `div` (Euclidean division), and `/Int` to truncating division. For a positive power-of-two divisor,
+Euclidean division computes exactly what shifts and low masks do, so the following simplifications rewrite bitwise
+operations by a constant into arithmetic the solver can reason about. All of them hold for every integer, as K
+integers are two's complement of infinite width.
+
+The rules only apply to a concrete mask or shift amount, so that a shift by a symbolic amount does not turn into
+nonlinear arithmetic. They have a lower priority than the default, so that the more specific simplifications in
+`kmir-lemmas.md` (e.g. for round trips through bytes) apply first to a term that both match.
+
+A low mask `2^k - 1` keeps the low `k` bits, i.e. the remainder modulo `2^k` (also for negative `X`).
+`M &Int (M +Int 1) ==Int 0` holds iff `M + 1` is a power of two.
+
+```k
+  rule [bitwise-low-mask]:
+    X &Int M => X modInt (M +Int 1)
+    requires 0 <=Int M andBool M &Int (M +Int 1) ==Int 0
+    [simplification(60), preserves-definedness, concrete(M)]
+
+  rule [bitwise-low-mask-comm]:
+    M &Int X => X modInt (M +Int 1)
+    requires 0 <=Int M andBool M &Int (M +Int 1) ==Int 0
+    [simplification(60), preserves-definedness, concrete(M)]
+```
+
+An arithmetic right shift is floor division by `2^N`, which for `X >= 0` is truncating division (`/Int`). For negative
+`X` it equals Euclidean division (`divInt`) instead, but the rule is restricted to nonnegative values for simplicity.
+
+```k
+  rule [bitwise-shr]:
+    X >>Int N => X /Int (2 ^Int N)
+    requires 0 <=Int N andBool 0 <=Int X
+    [simplification(60), preserves-definedness, concrete(N)]
+```
+
+Repeated shifts give nested divisions, each of which the solver sees as a nested if-then-else; they are collapsed into
+one. Truncating division by a positive `A`, then by a positive `B`, equals truncating division by `A * B`, for either
+sign of `X`.
+
+```k
+  rule [bitwise-div-div]:
+    (X /Int A) /Int B => X /Int (A *Int B)
+    requires 0 <Int A andBool 0 <Int B andBool 0 <=Int X
+    [simplification, preserves-definedness, concrete(A, B)]
+```
+
+A left shift is a multiplication by `2^N`. The rule is restricted to nonnegative values for simplicity, but would also
+hold for negative ones.
+
+```k
+  rule [bitwise-shl]:
+    X <<Int N => X *Int (2 ^Int N)
+    requires 0 <=Int N andBool 0 <=Int X
+    [simplification(60), preserves-definedness, concrete(N)]
+```
+
+With the rules above, the bytes of a nonnegative number `X` become `(X /Int 256^k) modInt 256` instead of
+`(X >>Int 8 ... >>Int 8) &Int 255`, so the round-trip simplifications in `kmir-lemmas.md` no longer apply when the bytes are
+put back together. The following simplifications put them back together instead, from the most significant byte.
+Note that the second rule follows directly from the definition of integer division, and is equivalent to the first rule with
+`A ==Int 1`.
+
+```k
+  rule [bitwise-digits]:
+    (X /Int A) modInt N +Int N *Int (X /Int B) => X /Int A
+    requires 0 <=Int X andBool 0 <Int A andBool 0 <Int N andBool B ==Int A *Int N
+    [simplification, preserves-definedness, concrete(A, B, N)]
+
+  rule [bitwise-digits-low]:
+    X modInt N +Int N *Int (X /Int N) => X
+    requires 0 <=Int X andBool 0 <Int N
+    [simplification, preserves-definedness, concrete(N)]
+```
+
+For any other constant mask `0 < C < 2^k`, `X &Int C` only has bits of `C`, so it equals `(X &Int C) modInt 2^k`, and
+the solver knows that the remainder modulo `2^k` lies in `[0, 2^k)`. This bounds masks like `0xAAAAAAAA` below `2^32`.
+The rewrite puts the constant on the left, where this rule (with the constant on the right) does not match again.
+
+```k
+  rule [bitwise-mask-bound]:
+    X &Int C => (C &Int X) modInt (2 ^Int (log2Int(C) +Int 1))
+    requires 0 <Int C andBool C &Int (C +Int 1) =/=Int 0
+    [simplification(60), preserves-definedness, concrete(C), symbolic(X)]
+```
+
+Finally, comparisons that bound bitwise operations on nonnegative values. The bitwise and with a nonnegative value lies
+between zero and that value. The bitwise or of two values below `2^k` is below `2^k`, which bounds it by any constant
+`C` from the largest power of two not above `C` (or `C + 1` for `<=Int`).
+These only simplify comparisons of the given forms, for instance in the side conditions of the simplifications of
+masks and truncation in `kmir-lemmas.md`.
+
+```k
+  rule [bitwise-and-lower]:
+    0 <=Int X &Int _Y => true
+    requires 0 <=Int X
+    [simplification]
+
+  rule [bitwise-and-lower-ge]:
+    X &Int _Y >=Int 0 => true
+    requires 0 <=Int X
+    [simplification]
+
+  rule [bitwise-and-upper]:
+    X &Int _Y <=Int X => true
+    requires 0 <=Int X
+    [simplification]
+
+  rule [bitwise-and-upper-ge]:
+    X >=Int X &Int _Y => true
+    requires 0 <=Int X
+    [simplification]
+
+  rule [bitwise-or-lower]:
+    0 <=Int X |Int Y => true
+    requires 0 <=Int X andBool 0 <=Int Y
+    [simplification]
+
+  rule [bitwise-or-upper]:
+    X |Int Y <Int C => true
+    requires 0 <Int C
+     andBool 0 <=Int X andBool X <Int 2 ^Int log2Int(C)
+     andBool 0 <=Int Y andBool Y <Int 2 ^Int log2Int(C)
+    [simplification, concrete(C)]
+
+  rule [bitwise-or-upper-le]:
+    X |Int Y <=Int C => true
+    requires 0 <=Int C
+     andBool 0 <=Int X andBool X <Int 2 ^Int log2Int(C +Int 1)
+     andBool 0 <=Int Y andBool Y <Int 2 ^Int log2Int(C +Int 1)
+    [simplification, concrete(C)]
+```
+
+```k
+endmodule
+```

kmir/src/tests/integration/data/prove-rs/bitwise-lemmas.rs

@@ -0,0 +1,103 @@
+// Bitwise operations on symbolic values that the prover can only reason about after the bitwise lemmas in
+// `bitwise-lemmas.md` turn them into arithmetic (`modInt`, `/Int`, `*Int`) that Z3 understands. Without them, each
+// assertion splits into a branch where it fails.
+
+/// A low mask is the remainder for nonnegative values. For negative values, `%` keeps the sign of `x` but the mask
+/// does not, so a nonzero remainder is off by 256.
+#[no_mangle]
+pub fn mask_is_rem(x: i64) {
+    let m = x & 0xFF;
+    if x >= 0 {
+        assert_eq!(m, x % 256);
+    } else {
+        let r = x % 256;
+        assert_eq!(m, if r == 0 { 0 } else { r + 256 });
+    }
+}
+
+/// A low mask is the same with the mask on either side.
+#[no_mangle]
+pub fn mask_comm(x: i64) {
+    assert_eq!(0xFF & x, x & 0xFF);
+}
+
+/// A right shift is a division.
+#[no_mangle]
+pub fn shr_is_div(x: u64) {
+    assert_eq!(x >> 8, x / 256);
+}
+
+/// Repeated right shifts are a single division.
+#[no_mangle]
+pub fn shr_shr_is_div(x: u64) {
+    assert_eq!((x >> 1) >> 2, x / 8);
+}
+
+/// A left shift that does not overflow is a multiplication. `<<` drops the bits shifted out but `*` checks for overflow,
+/// so the value is widened first.
+#[no_mangle]
+pub fn shl_is_mul(x: u32) {
+    let y = x as u64;
+    assert_eq!(y << 3, y * 8);
+}
+
+/// The first step of a parallel bit count: masking with 0x5555_5555 bounds both halves below 2^31, so their sum
+/// cannot overflow.
+#[no_mangle]
+pub fn masked_sum_no_overflow(x: u32) -> u32 {
+    (x & 0x5555_5555) + ((x >> 1) & 0x5555_5555)
+}
+
+/// The bitwise and with a nonnegative value lies between zero and that value.
+#[no_mangle]
+pub fn and_nonneg_bounds(x: i64, y: i64) {
+    if x >= 0 {
+        assert!(0 <= x & y);
+        assert!(x & y >= 0);
+        assert!(x & y <= x);
+        assert!(x >= x & y);
+    }
+}
+
+/// The bitwise or of two nonnegative values is nonnegative.
+#[no_mangle]
+pub fn or_nonneg(x: i64, y: i64) {
+    if x >= 0 && y >= 0 {
+        assert!(0 <= x | y);
+    }
+}
+
+/// The bitwise or of two bytes is a byte.
+#[no_mangle]
+pub fn or_bytes_fit(a: u8, b: u8) {
+    let (a, b) = (a as u16, b as u16);
+    assert!(a | b < 256);
+}
+
+/// The bitwise or of two bytes is at most the largest byte.
+#[no_mangle]
+pub fn or_bytes_fit_le(a: u8, b: u8) {
+    let (a, b) = (a as u16, b as u16);
+    assert!(a | b <= 255);
+}
+
+/// A round trip through the native-endian bytes is a cast. Not a test of the bitwise lemmas, but of their interaction
+/// with the existing round-trip lemmas.
+#[no_mangle]
+pub fn ne_bytes_roundtrip(x: i64) {
+    assert_eq!(u64::from_ne_bytes(x.to_ne_bytes()), x as u64);
+}
+
+fn main() {
+    mask_is_rem(-0x1234);
+    mask_comm(-0x1234);
+    shr_is_div(0x1234);
+    shr_shr_is_div(0x1234);
+    shl_is_mul(0x1234);
+    masked_sum_no_overflow(0xFFFF_FFFF);
+    and_nonneg_bounds(6, -3);
+    or_nonneg(6, 3);
+    or_bytes_fit(0x0F, 0xF0);
+    or_bytes_fit_le(0x0F, 0xF0);
+    ne_bytes_roundtrip(-2);
+}

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u128.expected

@@ -12,7 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 34028236692093846346337460743176
+┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int , 128 , false )
+~> #freezer#setLocalV
 ┃  │   span: 332
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u16.expected

@@ -12,8 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 65535 , 16 , false )
-~> #freezer
+┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int , 16 , false )
+~> #freezer#setLocalVa
 ┃  │   span: 208
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u32.expected

@@ -12,8 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 4294967295 , 32 , false )
-~> #fr
+┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int , 32 , false )
+~> #freezer#setLocalVa
 ┃  │   span: 239
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u64.expected

@@ -12,7 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709551615 , 64 , fals
+┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int , 64 , false )
+~> #freezer#setLocalVa
 ┃  │   span: 270
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u8.expected

@@ -12,8 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 255 , 8 , false )
-~> #freezer#se
+┃  │   Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int , 8 , false )
+~> #freezer#setLocalVal
 ┃  │   span: 84
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u128.expected

@@ -12,7 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 34028236692093846346337460743176
+┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int , 128 , false )
+~> #freezer#setLocalV
 ┃  │   span: 332
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u16.expected

@@ -12,8 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 65535 , 16 , false )
-~> #freezer
+┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int , 16 , false )
+~> #freezer#setLocalVa
 ┃  │   span: 208
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u32.expected

@@ -12,8 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 4294967295 , 32 , false )
-~> #fr
+┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int , 32 , false )
+~> #freezer#setLocalVa
 ┃  │   span: 239
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u64.expected

@@ -12,7 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 18446744073709551615 , 64 , fals
+┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int , 64 , false )
+~> #freezer#setLocalVa
 ┃  │   span: 270
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u8.expected

@@ -12,8 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 255 , 8 , false )
-~> #freezer#se
+┃  │   Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int , 8 , false )
+~> #freezer#setLocalVal
 ┃  │   span: 84
 ┃  │
 ┃  │  (71 steps)

kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u128.expected

@@ -12,7 +12,8 @@
 ┣━━┓
 ┃  │
 ┃  ├─ 4
-┃  │   Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 34028236692093846346337460743176
+┃  │   Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int , 128 , false )
+~> #freezer#setLocalV
 ┃  │   span: 332
 ┃  │
 ┃  │  (71 steps)