Added challenge 11 proofs to workflow

Removed old unchecked_arithmetic proofs

Author: dkcumming

.github/workflows/kmir.yml

@@ -22,12 +22,12 @@ jobs:
       - name: Checkout Repository
         uses: actions/checkout@v4
 
-      - name: Run Proofs in Tool Container
+      - name: Run Challenge 11 Proofs
         run: |
           docker run --rm -t \
             --name ${{ env.container_name }} \
             -w /home/kmir/workspace \
             -u $(id -u):$(id -g) \
             -v $PWD:/home/kmir/workspace \
             runtimeverificationinc/kmir:ubuntu-jammy-latest \
-            kmir-proofs/unchecked_arithmetic/run-proofs.sh
+            kmir-proofs/0011-floats-ints/run-proofs.sh

kmir-proofs/0011-floats-ints/carrying_mul.rs

@@ -0,0 +1,36 @@
+#![feature(bigint_helper_methods)]
+
+fn main() {
+    carrying_mul_u8(0, 0, 0);
+    carrying_mul_u16(0, 0, 0);
+    carrying_mul_u32(0, 0, 0);
+    carrying_mul_u64(0, 0, 0);
+}
+
+fn carrying_mul_u8(a: u8, b: u8, c: u8) {
+    let (lo, hi) = a.carrying_mul(b, c);
+    let expected = (a as u16) * (b as u16) + (c as u16);
+    assert!(lo == (expected as u8));
+    assert!(hi == ((expected >> u8::BITS) as u8));
+}
+
+fn carrying_mul_u16(a: u16, b: u16, c: u16) {
+    let (lo, hi) = a.carrying_mul(b, c);
+    let expected = (a as u32) * (b as u32) + (c as u32);
+    assert!(lo == (expected as u16));
+    assert!(hi == ((expected >> u16::BITS) as u16));
+}
+
+fn carrying_mul_u32(a: u32, b: u32, c: u32) {
+    let (lo, hi) = a.carrying_mul(b, c);
+    let expected = (a as u64) * (b as u64) + (c as u64);
+    assert!(lo == (expected as u32));
+    assert!(hi == ((expected >> u32::BITS) as u32));
+}
+
+fn carrying_mul_u64(a: u64, b: u64, c: u64) {
+    let (lo, hi) = a.carrying_mul(b, c);
+    let expected = (a as u128) * (b as u128) + (c as u128);
+    assert!(lo == (expected as u64));
+    assert!(hi == ((expected >> u64::BITS) as u64));
+}

kmir-proofs/0011-floats-ints/run-proofs.sh

@@ -0,0 +1,81 @@
+#!/bin/bash
+# Run KMIR passing proofs for Challenge 11: Safety of Methods for Numeric Primitive Types
+# https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html
+
+set -eu
+
+if ! command -v kmir &> /dev/null; then
+    echo "ERROR: kmir not found on PATH"
+    exit 2
+fi
+
+DIR=$(realpath "$(dirname "$0")")
+cd "$DIR"
+
+PROOF_DIR=proofs
+FAILED_PROOFS=""
+
+# Mapping of FILENAME -> START_SYMBOLS
+declare -A FILE_SYMBOLS
+FILE_SYMBOLS=(
+    [unchecked_add]="unchecked_add_u8 unchecked_add_u16 unchecked_add_u32 unchecked_add_u64 unchecked_add_u128 unchecked_add_i8 unchecked_add_i16 unchecked_add_i32 unchecked_add_i64 unchecked_add_i128"
+    [unchecked_sub]="unchecked_sub_u8 unchecked_sub_u16 unchecked_sub_u32 unchecked_sub_u64 unchecked_sub_u128 unchecked_sub_i8 unchecked_sub_i16 unchecked_sub_i32 unchecked_sub_i64 unchecked_sub_i128"
+    [unchecked_mul]="unchecked_mul_u8 unchecked_mul_u16 unchecked_mul_u32 unchecked_mul_u64 unchecked_mul_u128 unchecked_mul_i8 unchecked_mul_i16 unchecked_mul_i32 unchecked_mul_i64 unchecked_mul_i128"
+    [unchecked_shl]="unchecked_shl_u8 unchecked_shl_u16 unchecked_shl_u32 unchecked_shl_u64 unchecked_shl_u128 unchecked_shl_i8 unchecked_shl_i16 unchecked_shl_i32 unchecked_shl_i64 unchecked_shl_i128"
+    [unchecked_shr]="unchecked_shr_u8 unchecked_shr_u16 unchecked_shr_u32 unchecked_shr_u64 unchecked_shr_u128 unchecked_shr_i8 unchecked_shr_i16 unchecked_shr_i32 unchecked_shr_i64 unchecked_shr_i128"
+    [unchecked_neg]="unchecked_neg_i8 unchecked_neg_i16 unchecked_neg_i32 unchecked_neg_i64 unchecked_neg_i128"
+    [wrapping_shl]="wrapping_shl_u8 wrapping_shl_u16 wrapping_shl_u32 wrapping_shl_u64 wrapping_shl_u128 wrapping_shl_i8 wrapping_shl_i16 wrapping_shl_i32 wrapping_shl_i64 wrapping_shl_i128"
+    [wrapping_shr]="wrapping_shr_u8 wrapping_shr_u16 wrapping_shr_u32 wrapping_shr_u64 wrapping_shr_u128 wrapping_shr_i8 wrapping_shr_i16 wrapping_shr_i32 wrapping_shr_i64 wrapping_shr_i128"
+    [widening_mul]="widening_mul_u8 widening_mul_u16 widening_mul_u32 widening_mul_u64"
+    [carrying_mul]="carrying_mul_u8 carrying_mul_u16 carrying_mul_u32 carrying_mul_u64"
+)
+
+for file in "${!FILE_SYMBOLS[@]}"; do
+    rs_file="${file}.rs"
+    if [ ! -f "$rs_file" ]; then
+        echo "ERROR: $rs_file not found"
+        FAILED_PROOFS="${FAILED_PROOFS} ${file}(missing)"
+        continue
+    fi
+
+    symbols="${FILE_SYMBOLS[$file]}"
+    echo "========================================="
+    echo "File: $rs_file"
+    echo "========================================="
+
+    for sym in $symbols; do
+        proof_id="${file}.${sym}"
+        echo "-----------------------------------------"
+        echo "Proving: ${proof_id}"
+        echo "-----------------------------------------"
+
+        if ! kmir prove --start-symbol "$sym" --terminate-on-thunk --proof-dir "$PROOF_DIR" --reload "$rs_file"; then
+            FAILED_PROOFS="${FAILED_PROOFS} ${proof_id}"
+        fi
+
+        kmir show --proof-dir "$PROOF_DIR" "${proof_id}" || true
+    done
+done
+
+echo ""
+echo "========================================="
+echo "SUMMARY"
+echo "========================================="
+
+if [ -n "$FAILED_PROOFS" ]; then
+    echo ""
+    echo "FAILED:"
+    for f in $FAILED_PROOFS; do
+        echo "  - $f"
+    done
+    echo ""
+    echo -e "\033[31m=========================================\033[0m"
+    echo -e "\033[31mSOME PROOFS FAILED\033[0m"
+    echo -e "\033[31m=========================================\033[0m"
+    exit 1
+fi
+
+echo ""
+echo -e "\033[32m=========================================\033[0m"
+echo -e "\033[32mALL PROOFS PASSED\033[0m"
+echo -e "\033[32m=========================================\033[0m"

kmir-proofs/0011-floats-ints/unchecked_add.rs

@@ -0,0 +1,84 @@
+#![feature(unchecked_math)]
+
+fn main() {
+    unchecked_add_u8(0, 0);
+    unchecked_add_u16(0, 0);
+    unchecked_add_u32(0, 0);
+    unchecked_add_u64(0, 0);
+    unchecked_add_u128(0, 0);
+    unchecked_add_i8(0, 0);
+    unchecked_add_i16(0, 0);
+    unchecked_add_i32(0, 0);
+    unchecked_add_i64(0, 0);
+    unchecked_add_i128(0, 0);
+}
+
+fn unchecked_add_u8(a: u8, b: u8) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_u16(a: u16, b: u16) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_u32(a: u32, b: u32) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_u64(a: u64, b: u64) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_u128(a: u128, b: u128) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_i8(a: i8, b: i8) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_i16(a: i16, b: i16) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_i32(a: i32, b: i32) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_i64(a: i64, b: i64) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_add_i128(a: i128, b: i128) {
+    if let Some(expected) = a.checked_add(b) {
+        let result = unsafe { a.unchecked_add(b) };
+        assert!(result == expected);
+    }
+}

kmir-proofs/0011-floats-ints/unchecked_mul.rs

@@ -0,0 +1,84 @@
+#![feature(unchecked_math)]
+
+fn main() {
+    unchecked_mul_u8(0, 0);
+    unchecked_mul_u16(0, 0);
+    unchecked_mul_u32(0, 0);
+    unchecked_mul_u64(0, 0);
+    unchecked_mul_u128(0, 0);
+    unchecked_mul_i8(0, 0);
+    unchecked_mul_i16(0, 0);
+    unchecked_mul_i32(0, 0);
+    unchecked_mul_i64(0, 0);
+    unchecked_mul_i128(0, 0);
+}
+
+fn unchecked_mul_u8(a: u8, b: u8) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_u16(a: u16, b: u16) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_u32(a: u32, b: u32) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_u64(a: u64, b: u64) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_u128(a: u128, b: u128) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_i8(a: i8, b: i8) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_i16(a: i16, b: i16) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_i32(a: i32, b: i32) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_i64(a: i64, b: i64) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_mul_i128(a: i128, b: i128) {
+    if let Some(expected) = a.checked_mul(b) {
+        let result = unsafe { a.unchecked_mul(b) };
+        assert!(result == expected);
+    }
+}

kmir-proofs/0011-floats-ints/unchecked_neg.rs

@@ -0,0 +1,44 @@
+#![feature(unchecked_neg)]
+
+fn main() {
+    unchecked_neg_i8(0);
+    unchecked_neg_i16(0);
+    unchecked_neg_i32(0);
+    unchecked_neg_i64(0);
+    unchecked_neg_i128(0);
+}
+
+fn unchecked_neg_i8(a: i8) {
+    if let Some(expected) = a.checked_neg() {
+        let result = unsafe { a.unchecked_neg() };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_neg_i16(a: i16) {
+    if let Some(expected) = a.checked_neg() {
+        let result = unsafe { a.unchecked_neg() };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_neg_i32(a: i32) {
+    if let Some(expected) = a.checked_neg() {
+        let result = unsafe { a.unchecked_neg() };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_neg_i64(a: i64) {
+    if let Some(expected) = a.checked_neg() {
+        let result = unsafe { a.unchecked_neg() };
+        assert!(result == expected);
+    }
+}
+
+fn unchecked_neg_i128(a: i128) {
+    if let Some(expected) = a.checked_neg() {
+        let result = unsafe { a.unchecked_neg() };
+        assert!(result == expected);
+    }
+}