Adding proofs negative harnesses (forgotton last commit)

Author: dkcumming

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

@@ -0,0 +1,64 @@
+#![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) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_u16(a: u16, b: u16) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_u32(a: u32, b: u32) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_u64(a: u64, b: u64) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_u128(a: u128, b: u128) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i8(a: i8, b: i8) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i16(a: i16, b: i16) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i32(a: i32, b: i32) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i64(a: i64, b: i64) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i128(a: i128, b: i128) {
+    let result = unsafe { a.unchecked_add(b) };
+    assert!(result == a.wrapping_add(b));
+}

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

@@ -0,0 +1,64 @@
+#![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) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_u16(a: u16, b: u16) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_u32(a: u32, b: u32) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_u64(a: u64, b: u64) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_u128(a: u128, b: u128) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i8(a: i8, b: i8) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i16(a: i16, b: i16) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i32(a: i32, b: i32) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i64(a: i64, b: i64) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i128(a: i128, b: i128) {
+    let result = unsafe { a.unchecked_mul(b) };
+    assert!(result == a.wrapping_mul(b));
+}

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

@@ -0,0 +1,34 @@
+#![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) {
+    let result = unsafe { a.unchecked_neg() };
+    assert!(result == a.wrapping_neg());
+}
+
+fn unchecked_neg_i16(a: i16) {
+    let result = unsafe { a.unchecked_neg() };
+    assert!(result == a.wrapping_neg());
+}
+
+fn unchecked_neg_i32(a: i32) {
+    let result = unsafe { a.unchecked_neg() };
+    assert!(result == a.wrapping_neg());
+}
+
+fn unchecked_neg_i64(a: i64) {
+    let result = unsafe { a.unchecked_neg() };
+    assert!(result == a.wrapping_neg());
+}
+
+fn unchecked_neg_i128(a: i128) {
+    let result = unsafe { a.unchecked_neg() };
+    assert!(result == a.wrapping_neg());
+}

kmir-proofs/0011-floats-ints/unchecked_shl-fail.rs

@@ -0,0 +1,64 @@
+#![feature(unchecked_shifts)]
+
+fn main() {
+    unchecked_shl_u8(0, 0);
+    unchecked_shl_u16(0, 0);
+    unchecked_shl_u32(0, 0);
+    unchecked_shl_u64(0, 0);
+    unchecked_shl_u128(0, 0);
+    unchecked_shl_i8(0, 0);
+    unchecked_shl_i16(0, 0);
+    unchecked_shl_i32(0, 0);
+    unchecked_shl_i64(0, 0);
+    unchecked_shl_i128(0, 0);
+}
+
+fn unchecked_shl_u8(a: u8, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_u16(a: u16, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_u32(a: u32, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_u64(a: u64, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_u128(a: u128, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i8(a: i8, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i16(a: i16, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i32(a: i32, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i64(a: i64, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i128(a: i128, b: u32) {
+    let result = unsafe { a.unchecked_shl(b) };
+    assert!(result == a.wrapping_shl(b));
+}

kmir-proofs/0011-floats-ints/unchecked_shr-fail.rs

@@ -0,0 +1,64 @@
+#![feature(unchecked_shifts)]
+
+fn main() {
+    unchecked_shr_u8(0, 0);
+    unchecked_shr_u16(0, 0);
+    unchecked_shr_u32(0, 0);
+    unchecked_shr_u64(0, 0);
+    unchecked_shr_u128(0, 0);
+    unchecked_shr_i8(0, 0);
+    unchecked_shr_i16(0, 0);
+    unchecked_shr_i32(0, 0);
+    unchecked_shr_i64(0, 0);
+    unchecked_shr_i128(0, 0);
+}
+
+fn unchecked_shr_u8(a: u8, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_u16(a: u16, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_u32(a: u32, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_u64(a: u64, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_u128(a: u128, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i8(a: i8, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i16(a: i16, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i32(a: i32, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i64(a: i64, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i128(a: i128, b: u32) {
+    let result = unsafe { a.unchecked_shr(b) };
+    assert!(result == a.wrapping_shr(b));
+}

kmir-proofs/0011-floats-ints/unchecked_sub-fail.rs

@@ -0,0 +1,64 @@
+#![feature(unchecked_math)]
+
+fn main() {
+    unchecked_sub_u8(0, 0);
+    unchecked_sub_u16(0, 0);
+    unchecked_sub_u32(0, 0);
+    unchecked_sub_u64(0, 0);
+    unchecked_sub_u128(0, 0);
+    unchecked_sub_i8(0, 0);
+    unchecked_sub_i16(0, 0);
+    unchecked_sub_i32(0, 0);
+    unchecked_sub_i64(0, 0);
+    unchecked_sub_i128(0, 0);
+}
+
+fn unchecked_sub_u8(a: u8, b: u8) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_u16(a: u16, b: u16) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_u32(a: u32, b: u32) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_u64(a: u64, b: u64) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_u128(a: u128, b: u128) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i8(a: i8, b: i8) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i16(a: i16, b: i16) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i32(a: i32, b: i32) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i64(a: i64, b: i64) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i128(a: i128, b: i128) {
+    let result = unsafe { a.unchecked_sub(b) };
+    assert!(result == a.wrapping_sub(b));
+}