Unchecked arithmetic proofs and lemmas (#571)

The proofs for unchecked arithmetic (from AWS initiative challenge 11)
require additional lemmas to confirm that no truncation is happening.
These lemmas are added here, also removing one lemma that we had twice
(in the lemmas file and in `numbers.md` where `truncate` is defined).

Also checking in the Rust code over which we run the proofs, and will
set up a convention for which functions to run in `prove-rs`
(suggestion: one-line comment containing a list of `start-symbol`
parameters at the top of the file).

---------

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

Author: jberthold

kmir/pyproject.toml

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

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.151'
+VERSION: Final = '0.3.152'

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

@@ -50,6 +50,38 @@ Therefore, its value range should be simplified for symbolic input asserted to b
      [simplification]
 ```
 
+However, `truncate` gets evaluated and is therefore not present any more for this simplification.
+The following simplification rules operate on the expression created by evaluating `truncate` when
+`WIDTH` is 8, 16, 32, 64, or 128 and the mode is `Unsigned`. The simplification would hold for any
+power of two but the semantics will always operate with these particular ones.
+
+```k
+  rule VAL &Int MASK => VAL 
+    requires 0   <=Int VAL 
+     andBool VAL <=Int MASK
+     andBool ( MASK ==Int bitmask8
+        orBool MASK ==Int bitmask16
+        orBool MASK ==Int bitmask32
+        orBool MASK ==Int bitmask64
+        orBool MASK ==Int bitmask128
+     )
+    [simplification, preserves-definedness]
+
+  syntax Int ::= "bitmask8"    [macro]
+               | "bitmask16"   [macro]
+               | "bitmask32"   [macro]
+               | "bitmask64"   [macro]
+               | "bitmask128"  [macro]
+
+  rule bitmask8   => ( 1 <<Int 8  ) -Int 1
+  rule bitmask16  => ( 1 <<Int 16 ) -Int 1
+  rule bitmask32  => ( 1 <<Int 32 ) -Int 1
+  rule bitmask64  => ( 1 <<Int 64 ) -Int 1
+  rule bitmask128 => ( 1 <<Int 128) -Int 1
+
+```
+
+
 ```k
 endmodule
 ```

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

@@ -74,15 +74,12 @@ This truncation function is instrumental in the implementation of Integer arithm
     requires WIDTH <=Int 0
   // unsigned values can be truncated using a simple bitmask
   // NB if VAL is negative (underflow), the truncation will yield a positive number
+
   rule truncate(VAL, WIDTH, Unsigned)
       => // mask with relevant bits
         VAL &Int ((1 <<Int WIDTH) -Int 1)
     requires 0 <Int WIDTH
     [preserves-definedness]
-  rule truncate(VAL, WIDTH, Unsigned)
-      => VAL // shortcut when there is nothing to do
-    requires 0 <Int WIDTH andBool VAL <Int 1 <<Int WIDTH
-    [simplification, preserves-definedness]
 
   // for signed values we need to preserve/restore the sign
   rule truncate(VAL, WIDTH, Signed)

kmir/src/tests/integration/data/prove-rs/unchecked_arithmetic.rs

@@ -0,0 +1,119 @@
+// @kmir prove-rs: unchecked_add_i32 unchecked_sub_usize unchecked_mul_isize
+
+fn main() {
+    unchecked_add_i32(1,2);
+    unchecked_sub_usize(1, 2);
+    unchecked_mul_isize(1, 2);
+}
+
+/// If the precondition is not met, the program is not executed (exits cleanly, ex falso quodlibet)
+macro_rules! precondition {
+    ($pre:expr, $block:expr) => {
+        if $pre { $block }
+    };
+}
+
+fn unchecked_add_i32(a: i32, b: i32) {
+
+    precondition!(
+        ((a as i64 + b as i64) <= i32::MAX as i64) &&
+        ( a as i64 + b as i64  >= i32::MIN as i64),
+        // =========================================
+         unsafe {
+            let result = a.unchecked_add(b);
+            assert!(result as i64 == a as i64 + b as i64)
+        }
+    );
+}
+
+
+macro_rules! unchecked_add_claim_for {
+    ($name:ident, $ty:ident) => {
+        #[allow(unused)]
+        fn $name(a: $ty, b: $ty)
+        {
+            use std::$ty;
+            precondition!(
+                ((a as i128 + b as i128) <= $ty::MAX as i128) &&
+                ( a as i128 + b as i128  >= $ty::MIN as i128),
+                // =========================================
+                 unsafe {
+                    let result = a.unchecked_add(b);
+                    assert!(result as i128 == a as i128 + b as i128)
+                }
+            );
+        }
+    }
+}
+
+unchecked_add_claim_for!(unchecked_add_i8   , i8   );
+unchecked_add_claim_for!(unchecked_add_i16  , i16  );
+// unchecked_add_claim_for!(unchecked_add_i32  , i32  ); // already above
+unchecked_add_claim_for!(unchecked_add_i64  , i64  );
+unchecked_add_claim_for!(unchecked_add_isize, isize);
+unchecked_add_claim_for!(unchecked_add_u8   , u8   );
+unchecked_add_claim_for!(unchecked_add_u16  , u16  );
+unchecked_add_claim_for!(unchecked_add_u32  , u32  );
+unchecked_add_claim_for!(unchecked_add_u64  , u64  );
+unchecked_add_claim_for!(unchecked_add_usize, usize);
+
+macro_rules! unchecked_sub_claim_for {
+    ($name:ident, $ty:ident) => {
+        #[allow(unused)]
+        fn $name(a: $ty, b: $ty)
+        {
+            use std::$ty;
+            precondition!(
+                ((a as i128 - b as i128) <= $ty::MAX as i128) &&
+                ( a as i128 - b as i128  >= $ty::MIN as i128),
+                // =========================================
+                 unsafe {
+                    let result = a.unchecked_sub(b);
+                    assert!(result as i128 == a as i128 - b as i128)
+                }
+            );
+        }
+    }
+}
+
+unchecked_sub_claim_for!(unchecked_sub_i8   , i8   );
+unchecked_sub_claim_for!(unchecked_sub_i16  , i16  );
+unchecked_sub_claim_for!(unchecked_sub_i32  , i32  );
+unchecked_sub_claim_for!(unchecked_sub_i64  , i64  );
+unchecked_sub_claim_for!(unchecked_sub_isize, isize);
+unchecked_sub_claim_for!(unchecked_sub_u8   , u8   );
+unchecked_sub_claim_for!(unchecked_sub_u16  , u16  );
+unchecked_sub_claim_for!(unchecked_sub_u32  , u32  );
+unchecked_sub_claim_for!(unchecked_sub_u64  , u64  );
+unchecked_sub_claim_for!(unchecked_sub_usize, usize);
+
+macro_rules! unchecked_mul_claim_for {
+    ($name:ident, $ty:ident) => {
+        #[allow(unused)]
+        fn $name(a: $ty, b: $ty)
+        {
+            use std::$ty;
+            precondition!(
+                ((a as i128 * b as i128) <= $ty::MAX as i128) &&
+                ( a as i128 * b as i128  >= $ty::MIN as i128),
+                // =========================================
+                    unsafe {
+                    let result = a.unchecked_mul(b);
+                    assert!(result as i128 == a as i128 * b as i128)
+                }
+            );
+        }
+    }
+}
+
+unchecked_mul_claim_for!(unchecked_mul_i8   , i8   );
+unchecked_mul_claim_for!(unchecked_mul_i16  , i16  );
+unchecked_mul_claim_for!(unchecked_mul_i32  , i32  );
+unchecked_mul_claim_for!(unchecked_mul_i64  , i64  );
+unchecked_mul_claim_for!(unchecked_mul_isize, isize);
+unchecked_mul_claim_for!(unchecked_mul_u8   , u8   );
+unchecked_mul_claim_for!(unchecked_mul_u16  , u16  );
+unchecked_mul_claim_for!(unchecked_mul_u32  , u32  );
+// insufficient bit size for precondition
+// unchecked_mul_claim_for!(unchecked_mul_u64  , u64  );
+// unchecked_mul_claim_for!(unchecked_mul_usize, usize);

kmir/src/tests/integration/test_integration.py

@@ -451,16 +451,36 @@ def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> No
     should_show = rs_file.stem in PROVE_RS_SHOW_SPECS
 
     prove_rs_opts = ProveRSOpts(rs_file)
-    apr_proof = kmir.prove_rs(prove_rs_opts)
-
-    if not should_fail:
-        assert apr_proof.passed
-    else:
-        assert apr_proof.failed
 
     if should_show:
+        # always run `main` when kmir show is tested
+        apr_proof = kmir.prove_rs(prove_rs_opts)
+
+        if not should_fail:
+            assert apr_proof.passed
+        else:
+            assert apr_proof.failed
+
         shower = APRProofShow(kmir, node_printer=KMIRAPRNodePrinter(kmir, apr_proof, full_printer=False))
         show_res = '\n'.join(shower.show(apr_proof))
         assert_or_update_show_output(
             show_res, PROVING_DIR / f'show/{rs_file.stem}.expected', update=update_expected_output
         )
+    else:
+        # read start symbol(s) from the first line (default: [main] otherwise)
+        start_sym_prefix = '// @kmir prove-rs:'
+        with open(rs_file) as f:
+            headline = f.readline().strip('\n')
+
+        if headline.startswith(start_sym_prefix):
+            start_symbols = headline.removeprefix(start_sym_prefix).split()
+        else:
+            start_symbols = ['main']
+
+        for start_symbol in start_symbols:
+            prove_rs_opts.start_symbol = start_symbol
+            apr_proof = kmir.prove_rs(prove_rs_opts)
+            if not should_fail:
+                assert apr_proof.passed
+            else:
+                assert apr_proof.failed

kmir/uv.lock

@@ -1 +1 @@
-0.3.151
+0.3.152