Added more prove-rs failing tests (#577)

Added some failing tests, specifically:
- `assert_eq_exp-fail.rs`: which fails since the operand inside
`assert_eq` that is an addition expression being treated as an
`Operand::Constant` which is then promoted to the `GlobalAlloc`s. So
@gtrepta you were right that `assert_eq` was working, but only with
`Operand::{Copy,Move}`. I encourage you to run `rustc --emir mir` to see
the promoted constant in the textual mir.
- `bitwise-fail.rs`: which fails since the bitwise operators are not
implemented

---------

Co-authored-by: devops <[email protected]>

Author: dkcumming

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.155"
+version = "0.3.156"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.155'
+VERSION: Final = '0.3.156'

kmir/src/tests/integration/data/prove-rs/assert_eq_exp-fail.rs

@@ -0,0 +1,5 @@
+fn main() {
+    let a = 42;
+
+    assert_eq!(3 + 39, a);
+}

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

@@ -0,0 +1,31 @@
+fn and(x: i32, y: i32) -> i32 {
+    x & y
+}
+
+fn or(x: i32, y: i32) -> i32 {
+    x | y
+}
+
+fn xor(x: i32, y: i32) -> i32 {
+    x ^ y
+}
+
+fn shift_left(x: i32, y: i32) -> i32 {
+    x << y
+}
+
+fn shift_right(x: i32, y: i32) -> i32 {
+    x >> y
+}
+
+fn main() {
+    assert!(and(3, 4) == 0);
+
+    assert!(or(3, 4) == 7);
+
+    assert!(xor(3, 7) == 4);
+
+    assert!(shift_left(1, 4) == 16);
+
+    assert!(shift_right(32, 4) == 2);
+}

kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected

@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "assert_eq_exp_fail" ) globalAllocEntry ( 0 , Memory ( allocati
+│   function: main
+│   span: 93
+│
+│  (88 steps)
+└─ 3 (stuck, leaf)
+    #readProjection ( typedValue ( Any , ty ( 25 ) , mutabilityNot ) , projectionEle
+    function: main
+    span: 101
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+

kmir/src/tests/integration/data/prove-rs/show/bitwise-fail.expected

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "bitwise_fail" ) globalAllocEntry ( 5 , Memory ( allocation ( .
+│   function: main
+│   span: 68
+│
+│  (30 steps)
+└─ 3 (stuck, leaf)
+    #compute ( binOpBitAnd , typedValue ( Integer ( 3 , 32 , true ) , ty ( 16 ) , mu
+    span: 50
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+

kmir/src/tests/integration/test_integration.py

@@ -438,6 +438,8 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None:
 PROVING_FILES = list(PROVING_DIR.glob('*.rs'))
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',
+    'assert_eq_exp-fail',
+    'bitwise-fail',
 ]
 
 

kmir/uv.lock

@@ -1 +1 @@
-0.3.155
+0.3.156