chapters 1 to 5

chapter1/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "chapter1"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+prusti-contracts = "0.2.0"

chapter1/Prusti.toml

@@ -0,0 +1,5 @@
+check_overflows = false
+
+# FUTURE: numberOfErrorsToReport
+# See: https://github.com/viperproject/prusti-dev/issues/1213
+extra_verifier_args = ["--numberOfErrorsToReport=0"]

chapter1/src/examples.rs

@@ -0,0 +1,10 @@
+// All of these examples work as expected:
+pub mod example_1_0;
+pub mod example_1_1;
+// pub mod example_1_2; // Should and does fail
+pub mod example_1_3_1;
+pub mod example_1_3_2;
+// pub mod example_1_4_1; // Should and does fail
+pub mod example_1_5_0;
+pub mod example_1_6_1;
+pub mod example_1_6_2;

chapter1/src/examples/example_1_0.rs

@@ -0,0 +1,7 @@
+// 1.0.dfy
+// method Triple (x: int) returns (r:int)
+
+pub fn triple(x: i64) -> i64 {
+    let y = 2 * x;
+    x + y
+}

chapter1/src/examples/example_1_1.rs

@@ -0,0 +1,9 @@
+// 1.1.dfy
+// method Triple(x: int) returns (r: int)
+
+pub fn triple(x: i64) -> i64 {
+    let y = 2 * x;
+    let r = x + y;
+    assert!(r == 3 * x);
+    r
+}

chapter1/src/examples/example_1_2.rs

@@ -0,0 +1,19 @@
+// 1.2.dfy
+// method Triple(x: int) returns (r: int)
+
+// Disable clippy warning for assert!(false);
+#[allow(clippy::assertions_on_constants)]
+
+// Note: This file correctly fails verification
+
+// FUTURE: numberOfErrorsToReport
+//   Here Prusti should show that (r < 5) is correct, since (r == 10 * x) was checked a line before.
+//   See: https://github.com/viperproject/prusti-dev/issues/1213
+pub fn triple(x: i64) -> i64 {
+    let y = 2 * x;
+    let r = x + y;
+    assert!(r == 10 * x); // Prusti finds error here
+    assert!(r < 5); // not checked, but should be correct
+    assert!(false); // not checked, but should be shown as incorrect
+    r
+}

chapter1/src/examples/example_1_3_1.rs

@@ -0,0 +1,13 @@
+// 1.3_1.dfy
+// method Triple(x: int) returns (r: int)
+
+pub fn triple(x: i64) -> i64 {
+    let r = if x == 0 {
+        0
+    } else {
+        let y = 2 * x;
+        x + y
+    };
+    assert!(r == 3 * x);
+    r
+}

chapter1/src/examples/example_1_3_2.rs

@@ -0,0 +1,19 @@
+// 1.3_2.dfy
+// method Triple(x: int) returns (r: int)
+
+pub fn triple(x: i64) -> i64 {
+    // Note: this translation is not a direct mapping because Dafny uses
+    // a non-deterministic choice here.
+    let r = if x < 18 {
+        let a = 2 * x;
+        let b = 4 * x;
+        (a + b) / 2
+    } else if 0 <= x {
+        let y = 2 * x;
+        x + y
+    } else {
+        unreachable!();
+    };
+    assert!(r == 3 * x);
+    r
+}

chapter1/src/examples/example_1_4_1.rs

@@ -0,0 +1,31 @@
+// 1.4_1.dfy
+// method Triple(x: int) returns (r: int)
+// method Caller()
+
+// Note: This file correctly fails verification
+
+pub fn triple(x: i64) -> i64 {
+    // Note: this translation is not a direct mapping because Dafny uses
+    // a non-deterministic choice here.
+    let r = match x {
+        x if x < 18 => {
+            let a = 2 * x;
+            let b = 4 * x;
+            (a + b) / 2
+        }
+        x if 0 <= x => {
+            let y = 2 * x;
+            x + y
+        }
+        _ => {
+            unreachable!();
+        }
+    };
+    assert!(r == 3 * x);
+    r
+}
+
+pub fn caller() {
+    let t = triple(18);
+    assert!(t < 100); // cannot be proven due to missing postcondition of triple
+}

chapter1/src/examples/example_1_5_0.rs

@@ -0,0 +1,22 @@
+use prusti_contracts::*;
+
+// 1.5.0.dfy
+// method Triple(x: int) returns (r: int)
+// ghost method DoubleQuadruple(x: int) returns (a: int, b: int)
+
+#[ensures(result == x * 3)]
+pub fn triple(x: i64) -> i64 {
+    let y = 2 * x;
+    let r = x + y;
+
+    //FUTURE: ghost_variables
+    let (a, b) = ghost_double_quadruple(x);
+    prusti_assert!((a <= r && r <= b) || (b <= r && r <= a));
+    r
+}
+
+// FUTURE: ghost_functions
+#[pure]
+fn ghost_double_quadruple(x: i64) -> (i64, i64) {
+    (2 * x, 4 * x)
+}

chapter1/src/examples/example_1_6_1.rs

@@ -0,0 +1,21 @@
+use prusti_contracts::*;
+
+// 1.6_1.dfy
+// function Average(a: int, b: int): int
+// method Triple'(x: int) returns (r: int)
+
+#[pure]
+pub fn average(a: i64, b: i64) -> i64 {
+    (a + b) / 2
+}
+
+#[ensures(average(result, x * 3) == x * 3)]
+pub fn triple_wrong(x: i64) -> i64 {
+    x * 3 + 1
+}
+
+#[ensures(average(result, x * 3) == x * 3)]
+#[ensures(result % 2 == (x * 3) % 2)]
+pub fn triple_correct(x: i64) -> i64 {
+    x * 3
+}

chapter1/src/examples/example_1_6_2.rs

@@ -0,0 +1,11 @@
+use prusti_contracts::*;
+
+// 1.6_2.dfy
+// predicate IsEven(x: int)
+// function IsEven2(x: int): bool
+
+#[pure]
+#[ensures(result == (x % 2 == 0))] // technically not needed due to #[pure]
+pub fn is_even(x: i64) -> bool {
+    x % 2 == 0
+}

chapter1/src/exercises.rs

@@ -0,0 +1,5 @@
+// All these exercises can be verified as expected
+pub mod exercise_1_0;
+pub mod exercise_1_1;
+pub mod exercise_1_2;
+pub mod exercise_1_3;

chapter1/src/exercises/exercise_1_0.rs

@@ -0,0 +1,15 @@
+use prusti_contracts::*;
+
+// 1.0.dfy
+// method Min(x: int, y: int) returns (m: int)
+
+#[ensures(result <= x && result <= y)]
+pub fn min(x: i64, y: i64) -> i64 {
+    if x < y {
+        x - 1
+    } else {
+        y - 1
+    }
+    // FUTURE: std_lib_extern_spec_enhancement
+    // x.min(y)
+}

chapter1/src/exercises/exercise_1_1.rs

@@ -0,0 +1,23 @@
+use prusti_contracts::*;
+
+// 1.1.dfy
+// method MaxSum(x: int, y: int) returns (s: int, m: int)
+// method CallMaxSum() returns (s: int, m: int)
+
+#[ensures(result.0 == x + y)]
+#[ensures(result.1 >= x && result.1 >= y)]
+#[ensures(result.1 == x || result.1 == y)]
+pub fn max_sum(x: i64, y: i64) -> (i64, i64) {
+    let s = x + y;
+    let m = if x > y { x } else { y };
+    (s, m)
+    // FUTURE: std_lib_extern_spec_enhancement
+    // (x + y, x.max(y))
+}
+
+pub fn call_max_sum() -> (i64, i64) {
+    let (s, m) = max_sum(1928, 1);
+    prusti_assert!(s == 1929);
+    prusti_assert!(m == 1928);
+    (s, m)
+}

chapter1/src/exercises/exercise_1_2.rs

@@ -0,0 +1,23 @@
+use prusti_contracts::*;
+
+// 1.2.dfy
+// method MaxSum(x: int, y: int) returns (s: int, m: int)
+// method ReconstructFromMaxSum(s: int, m: int) returns (x: int, y: int)
+// method TestMaxSum(x: int, y: int)
+
+use super::exercise_1_1::max_sum;
+
+#[ensures(s == result.0 + result.1)]
+#[ensures((m == result.0 || m == result.1) && result.0 <= m && result.1 <= m)]
+#[requires(s <= 2 * m)]
+pub fn reconstruct_from_max_sum(s: i64, m: i64) -> (i64, i64) {
+    let x = m;
+    let y = s - m;
+    (x, y)
+}
+
+pub fn test_max_sum(x: i64, y: i64) {
+    let (s, m) = max_sum(x, y);
+    let (x_, y_) = reconstruct_from_max_sum(s, m);
+    prusti_assert!((x_ == x && y_ == y) || (x_ == y && y_ == x));
+}

chapter1/src/exercises/exercise_1_3.rs

@@ -0,0 +1,15 @@
+use prusti_contracts::*;
+
+// 1.3.dfy
+// function Average(a: int, b: int): int
+// method Triple'(x: int) returns (r: int)
+
+#[pure]
+pub fn average(a: i64, b: i64) -> i64 {
+    (a + b) / 2
+}
+
+#[ensures(average(result, x * 3) == x * 3)]
+pub fn triple_(x: i64) -> i64 {
+    x * 3 + 1
+}

chapter1/src/lib.rs

@@ -0,0 +1,9 @@
+// #![warn(clippy::pedantic)]
+
+#[allow(clippy::wildcard_imports)]
+#[allow(unused)]
+mod examples;
+
+#[allow(clippy::wildcard_imports)]
+#[allow(unused)]
+mod exercises;

chapter2/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "chapter2"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+prusti-contracts = "0.2.0"

chapter2/Prusti.toml

@@ -0,0 +1 @@
+check_overflows = false

chapter2/src/examples.rs

@@ -0,0 +1,3 @@
+pub mod example_2_0;
+pub mod example_2_3_0;
+pub mod example_2_3_1;

chapter2/src/examples/example_2_0.rs

@@ -0,0 +1,42 @@
+use prusti_contracts::*;
+
+// 2.0.dfy
+// method MyMethod(x: int) returns (y: int)
+
+#[requires(10 <= x)]
+#[ensures(25 <= result)]
+pub fn my_method(x: i64) -> i64 {
+    let a = x + 3;
+    let b = 12;
+    a + b
+}
+
+#[allow(clippy::let_and_return)]
+#[requires(10 <= x)]
+#[ensures(25 <= result)]
+pub fn my_method_with_backwards_annotations(x: i64) -> i64 {
+    prusti_assert!(10 <= x);
+    prusti_assert!(25 <= x + 3 + 12);
+    let a = x + 3;
+    prusti_assert!(25 <= a + 12);
+    let b = 12;
+    prusti_assert!(25 <= a + b);
+    let result = a + b;
+    prusti_assert!(25 <= result); // postcondition
+    result
+}
+
+#[allow(clippy::let_and_return)]
+#[requires(10 <= x)]
+#[ensures(25 <= result)]
+pub fn my_method_with_forwards_annotations(x: i64) -> i64 {
+    prusti_assert!(10 <= x); // precondition
+    let a = x + 3;
+    prusti_assert!(10 <= x && a == x + 3);
+    let b = 12;
+    prusti_assert!(10 <= x && a == x + 3 && b == 12);
+    let result = a + b;
+    prusti_assert!(10 <= x && a == x + 3 && b == 12 && result == a + b);
+    prusti_assert!(25 <= result);
+    result
+}