diff --git a/chapter1/Cargo.lock b/chapter1/Cargo.lock new file mode 100644 index 0000000..cb7bad7 --- /dev/null +++ b/chapter1/Cargo.lock @@ -0,0 +1,25 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "chapter1" +version = "0.1.0" +dependencies = [ + "prusti-contracts", +] + +[[package]] +name = "prusti-contracts" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0a55ba828aceca3c0786a6dd252e1d219720d15f4c454b70fee282111469c940" +dependencies = [ + "prusti-contracts-proc-macros", +] + +[[package]] +name = "prusti-contracts-proc-macros" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b74f012498f2f2239b7c99cb07c6fd18271587163d1710a242f00b6af5d9043d" diff --git a/chapter1/Cargo.toml b/chapter1/Cargo.toml new file mode 100644 index 0000000..93390c8 --- /dev/null +++ b/chapter1/Cargo.toml @@ -0,0 +1,10 @@ +[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 = { path = "/r/prusti-dev-master/prusti-contracts/prusti-contracts" } +# prusti-contracts = "0.1.9" diff --git a/chapter1/Prusti.toml b/chapter1/Prusti.toml new file mode 100644 index 0000000..ddace53 --- /dev/null +++ b/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"] \ No newline at end of file diff --git a/chapter1/src/examples.rs b/chapter1/src/examples.rs new file mode 100644 index 0000000..c545c36 --- /dev/null +++ b/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; diff --git a/chapter1/src/examples/example_1_0.rs b/chapter1/src/examples/example_1_0.rs new file mode 100644 index 0000000..5b5527f --- /dev/null +++ b/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 +} diff --git a/chapter1/src/examples/example_1_1.rs b/chapter1/src/examples/example_1_1.rs new file mode 100644 index 0000000..2ced44b --- /dev/null +++ b/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 +} diff --git a/chapter1/src/examples/example_1_2.rs b/chapter1/src/examples/example_1_2.rs new file mode 100644 index 0000000..9247a23 --- /dev/null +++ b/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 +} diff --git a/chapter1/src/examples/example_1_3_1.rs b/chapter1/src/examples/example_1_3_1.rs new file mode 100644 index 0000000..81f4c2b --- /dev/null +++ b/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 +} diff --git a/chapter1/src/examples/example_1_3_2.rs b/chapter1/src/examples/example_1_3_2.rs new file mode 100644 index 0000000..fd75568 --- /dev/null +++ b/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 +} diff --git a/chapter1/src/examples/example_1_4_1.rs b/chapter1/src/examples/example_1_4_1.rs new file mode 100644 index 0000000..e83f8db --- /dev/null +++ b/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 +} diff --git a/chapter1/src/examples/example_1_5_0.rs b/chapter1/src/examples/example_1_5_0.rs new file mode 100644 index 0000000..667517e --- /dev/null +++ b/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) +} diff --git a/chapter1/src/examples/example_1_6_1.rs b/chapter1/src/examples/example_1_6_1.rs new file mode 100644 index 0000000..981aea1 --- /dev/null +++ b/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 +} diff --git a/chapter1/src/examples/example_1_6_2.rs b/chapter1/src/examples/example_1_6_2.rs new file mode 100644 index 0000000..3b29305 --- /dev/null +++ b/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 +} diff --git a/chapter1/src/exercises.rs b/chapter1/src/exercises.rs new file mode 100644 index 0000000..2ff4abd --- /dev/null +++ b/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; diff --git a/chapter1/src/exercises/exercise_1_0.rs b/chapter1/src/exercises/exercise_1_0.rs new file mode 100644 index 0000000..132cbec --- /dev/null +++ b/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) +} diff --git a/chapter1/src/exercises/exercise_1_1.rs b/chapter1/src/exercises/exercise_1_1.rs new file mode 100644 index 0000000..723925f --- /dev/null +++ b/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) +} diff --git a/chapter1/src/exercises/exercise_1_2.rs b/chapter1/src/exercises/exercise_1_2.rs new file mode 100644 index 0000000..3cd3e27 --- /dev/null +++ b/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)); +} diff --git a/chapter1/src/exercises/exercise_1_3.rs b/chapter1/src/exercises/exercise_1_3.rs new file mode 100644 index 0000000..b35ba8c --- /dev/null +++ b/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 +} diff --git a/chapter1/src/lib.rs b/chapter1/src/lib.rs new file mode 100644 index 0000000..74e8d1e --- /dev/null +++ b/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; diff --git a/chapter2/Cargo.lock b/chapter2/Cargo.lock new file mode 100644 index 0000000..50d9827 --- /dev/null +++ b/chapter2/Cargo.lock @@ -0,0 +1,25 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "chapter2" +version = "0.1.0" +dependencies = [ + "prusti-contracts", +] + +[[package]] +name = "prusti-contracts" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0a55ba828aceca3c0786a6dd252e1d219720d15f4c454b70fee282111469c940" +dependencies = [ + "prusti-contracts-proc-macros", +] + +[[package]] +name = "prusti-contracts-proc-macros" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b74f012498f2f2239b7c99cb07c6fd18271587163d1710a242f00b6af5d9043d" diff --git a/chapter2/Cargo.toml b/chapter2/Cargo.toml new file mode 100644 index 0000000..7594963 --- /dev/null +++ b/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.1.4" diff --git a/chapter2/Prusti.toml b/chapter2/Prusti.toml new file mode 100644 index 0000000..1e6bcab --- /dev/null +++ b/chapter2/Prusti.toml @@ -0,0 +1 @@ +check_overflows = false \ No newline at end of file diff --git a/chapter2/src/examples.rs b/chapter2/src/examples.rs new file mode 100644 index 0000000..c8a7f55 --- /dev/null +++ b/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; diff --git a/chapter2/src/examples/example_2_0.rs b/chapter2/src/examples/example_2_0.rs new file mode 100644 index 0000000..99f5b21 --- /dev/null +++ b/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 +} diff --git a/chapter2/src/examples/example_2_3_0.rs b/chapter2/src/examples/example_2_3_0.rs new file mode 100644 index 0000000..d446389 --- /dev/null +++ b/chapter2/src/examples/example_2_3_0.rs @@ -0,0 +1,18 @@ +use prusti_contracts::*; + +// 2.3.0.dfy +// method Swap0(x: int, y: int) +// method Swap1(x: int, y: int) returns (a: int, b: int) + +#[ensures(result == (y, x))] +pub fn swap0(x: i64, y: i64) -> (i64, i64) { + let tmp = x; + let x = y; + let y = tmp; + (x, y) +} + +#[ensures(result == (y, x))] +pub fn swap1(x: i64, y: i64) -> (i64, i64) { + (y, x) +} diff --git a/chapter2/src/examples/example_2_3_1.rs b/chapter2/src/examples/example_2_3_1.rs new file mode 100644 index 0000000..d477757 --- /dev/null +++ b/chapter2/src/examples/example_2_3_1.rs @@ -0,0 +1,41 @@ +use prusti_contracts::*; + +// 2.3.1.dfy +// method Swap(x: int, y: int) returns (a: int, b: int) + +#[ensures(result == (y, x))] +pub fn swap_a(x: i64, y: i64) -> (i64, i64) { + let mut x = x; + let mut y = y; + x = y - x; + y -= x; + x += y; + (x, y) +} + +// // FUTURE: mutable_fn_args +// #[ensures(result == old((y, x)))] +// pub fn swap(mut x: i64, mut y: i64) -> (i64, i64) { +// x = y - x; +// y = y - x; +// x = y + x; +// (x, y) +// } + +// // FUTURE: mutable_fn_args +// #[ensures(result == old((y, x)))] +// pub fn swap_annotated(mut x: i64, mut y: i64) -> (i64, i64) { +// let x0 = x; +// let y0 = y; +// prusti_assert!(x == x0 && y == y0); +// x = y - x; +// prusti_assert!(x == y0 - x0 && y == y0); +// y = y - x; +// prusti_assert!(x == y0 - x0 && y == y0 - (y0 - x0)); +// prusti_assert!(x == y0 - x0 && y == x0); +// x = y + x; +// prusti_assert!(x == x0 + y0 - x0 && y == x0); +// prusti_assert!(x == y0 && y == x0); +// (x, y) +// // (y, x) +// } diff --git a/chapter2/src/exercises.rs b/chapter2/src/exercises.rs new file mode 100644 index 0000000..cd8f67b --- /dev/null +++ b/chapter2/src/exercises.rs @@ -0,0 +1,6 @@ +pub mod exercise_2_17; +pub mod exercise_2_18; +pub mod exercise_2_19; +pub mod exercise_2_20; +pub mod exercise_2_24; +pub mod exercise_2_25; diff --git a/chapter2/src/exercises/exercise_2_17.rs b/chapter2/src/exercises/exercise_2_17.rs new file mode 100644 index 0000000..28e588e --- /dev/null +++ b/chapter2/src/exercises/exercise_2_17.rs @@ -0,0 +1,18 @@ +use prusti_contracts::*; + +// 2.17.dfy +// method exercise (x: int) returns (y: int) + +#[requires(x != 5)] // weakest precondition +#[ensures(result < 10)] +pub fn exercise(x: i64) -> i64 { + if x < 8 { + if x == 5 { + 10 + } else { + 2 + } + } else { + 0 + } +} diff --git a/chapter2/src/exercises/exercise_2_18.rs b/chapter2/src/exercises/exercise_2_18.rs new file mode 100644 index 0000000..40289d8 --- /dev/null +++ b/chapter2/src/exercises/exercise_2_18.rs @@ -0,0 +1,18 @@ +use prusti_contracts::*; + +// 2.18.dfy +// method exercise (x: int) returns (y: int) + +#[requires(x >= 10)] +#[ensures(result % 2 == 0)] +pub fn exercise(x: i64) -> i64 { + if x < 10 { + if x < 20 { + 1 + } else { + 2 + } + } else { + 4 + } +} diff --git a/chapter2/src/exercises/exercise_2_19.rs b/chapter2/src/exercises/exercise_2_19.rs new file mode 100644 index 0000000..a628a27 --- /dev/null +++ b/chapter2/src/exercises/exercise_2_19.rs @@ -0,0 +1,21 @@ +use prusti_contracts::*; + +// 2.19.dfy +// method exercise (x: int) returns (y: int) + +#[requires(x >= 4 && x < 8)] +#[ensures(result % 2 == 0)] +pub fn exercise(x: i64) -> i64 { + if x < 8 { + if x < 4 { + let x_new = x + 1; + unreachable!(); + } else { + 2 + } + } else if x < 32 { + 1 + } else { + unreachable!(); + } +} diff --git a/chapter2/src/exercises/exercise_2_20.rs b/chapter2/src/exercises/exercise_2_20.rs new file mode 100644 index 0000000..5775530 --- /dev/null +++ b/chapter2/src/exercises/exercise_2_20.rs @@ -0,0 +1,21 @@ +use prusti_contracts::*; + +// 2.20.dfy +// method exercise (x: int) returns (y: int) + +#[requires((x == 2) || (x >= 34 && x < 55))] +#[ensures(0 <= result && result < 100)] +// #[ensures((0..100).contains(&result))] // FUTURE: std_lib_extern_spec_enhancement (contains) +pub fn exercise(x: i64) -> i64 { + if x < 34 { + if x == 2 { + x + 1 + } else { + 233 + } + } else if x < 55 { + 21 + } else { + 144 + } +} diff --git a/chapter2/src/exercises/exercise_2_24.rs b/chapter2/src/exercises/exercise_2_24.rs new file mode 100644 index 0000000..89acbf6 --- /dev/null +++ b/chapter2/src/exercises/exercise_2_24.rs @@ -0,0 +1,21 @@ +use prusti_contracts::*; + +// 2.24.dfy +// method exercise (u: int) returns (t: int) + +#[requires(u < 0)] +#[ensures(u < result)] +pub fn exercise(u: i64) -> i64 { + abs(7 * u) +} + +#[requires(x != i64::MIN)] // Fix for `-x` potentially overflowing (not from the book) +#[ensures(0 <= result && (x == result || x == -result))] +pub fn abs(x: i64) -> i64 { + if x >= 0 { + x + } else { + // FUTURE: negate_no_overflow: https://github.com/viperproject/prusti-dev/issues/881 + -x + } +} diff --git a/chapter2/src/exercises/exercise_2_25.rs b/chapter2/src/exercises/exercise_2_25.rs new file mode 100644 index 0000000..878d5ef --- /dev/null +++ b/chapter2/src/exercises/exercise_2_25.rs @@ -0,0 +1,40 @@ +use prusti_contracts::*; + +// 2.25.dfy +// method exerciseA (x: int, y: int) +// method exerciseB (x: int, y: int) +// method exerciseC (x: int, y: int) +// method exerciseD (x: int, y: int) +// method exerciseE (x: int, y: int) + +#[ensures(x < 100)] +#[requires(x < 100 && y == 25)] // weakest precondition +pub fn exercise_a(x: i64, y: i64) { + assert!(y == 25); +} + +#[ensures(x < 100)] +#[requires(0 <= x && x < 100)] // weakest precondition +pub fn exercise_b(x: i64, y: i64) { + assert!(0 <= x); +} + +#[ensures(x < 100)] +#[requires(x < 100)] // weakest precondition +pub fn exercise_c(x: i64, y: i64) { + assert!(x < 200); +} + +#[ensures(x < 100)] +#[requires(x < 100)] // weakest precondition +pub fn exercise_d(x: i64, y: i64) { + assert!(x <= 100); +} + +#[allow(clippy::manual_range_contains)] +#[ensures(x < 100)] +#[requires(0 <= x && x < 100)] // weakest precondition +pub fn exercise_e(x: i64, y: i64) { + // assert!((0..100).contains(&x)); // FUTURE: std_lib_extern_spec_enhancement (contains) + assert!(0 <= x && x < 100); +} diff --git a/chapter2/src/lib.rs b/chapter2/src/lib.rs new file mode 100644 index 0000000..74e8d1e --- /dev/null +++ b/chapter2/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; diff --git a/chapter3/Cargo.lock b/chapter3/Cargo.lock new file mode 100644 index 0000000..4a15c0a --- /dev/null +++ b/chapter3/Cargo.lock @@ -0,0 +1,91 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "cfg-if" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" + +[[package]] +name = "chapter3" +version = "0.1.0" +dependencies = [ + "prusti-contracts", + "rand", +] + +[[package]] +name = "getrandom" +version = "0.2.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c05aeb6a22b8f62540c194aac980f2115af067bfe15a0734d7277a768d396b31" +dependencies = [ + "cfg-if", + "libc", + "wasi", +] + +[[package]] +name = "libc" +version = "0.2.135" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68783febc7782c6c5cb401fbda4de5a9898be1762314da0bb2c10ced61f18b0c" + +[[package]] +name = "ppv-lite86" +version = "0.2.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eb9f9e6e233e5c4a35559a617bf40a4ec447db2e84c20b55a6f83167b7e57872" + +[[package]] +name = "prusti-contracts" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0a55ba828aceca3c0786a6dd252e1d219720d15f4c454b70fee282111469c940" +dependencies = [ + "prusti-contracts-proc-macros", +] + +[[package]] +name = "prusti-contracts-proc-macros" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b74f012498f2f2239b7c99cb07c6fd18271587163d1710a242f00b6af5d9043d" + +[[package]] +name = "rand" +version = "0.8.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" +dependencies = [ + "libc", + "rand_chacha", + "rand_core", +] + +[[package]] +name = "rand_chacha" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" +dependencies = [ + "ppv-lite86", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" +dependencies = [ + "getrandom", +] + +[[package]] +name = "wasi" +version = "0.11.0+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" diff --git a/chapter3/Cargo.toml b/chapter3/Cargo.toml new file mode 100644 index 0000000..ed4bb4b --- /dev/null +++ b/chapter3/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "chapter3" +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.1.4" +rand = "0.8.5" diff --git a/chapter3/Prusti.toml b/chapter3/Prusti.toml new file mode 100644 index 0000000..1e6bcab --- /dev/null +++ b/chapter3/Prusti.toml @@ -0,0 +1 @@ +check_overflows = false \ No newline at end of file diff --git a/chapter3/src/examples.rs b/chapter3/src/examples.rs new file mode 100644 index 0000000..eb3cbc3 --- /dev/null +++ b/chapter3/src/examples.rs @@ -0,0 +1,12 @@ +pub mod example_3_0_1; +pub mod example_3_0_2; +pub mod example_3_0_3; +pub mod example_3_0_4; +pub mod example_3_0_5; +pub mod example_3_1_1; +pub mod example_3_1_2; +pub mod example_3_3_0; +pub mod example_3_3_1; +pub mod example_3_3_2; +pub mod example_3_3_3_1; +// pub mod example_3_3_3_2; // BUGGED, see: https://github.com/viperproject/prusti-dev/issues/1214 diff --git a/chapter3/src/examples/example_3_0_1.rs b/chapter3/src/examples/example_3_0_1.rs new file mode 100644 index 0000000..adfda7a --- /dev/null +++ b/chapter3/src/examples/example_3_0_1.rs @@ -0,0 +1,14 @@ +use prusti_contracts::*; + +// 3.0_1.dfy +// method BadDouble(x: int) returns (d: int) + +// Adding this to decrease the amount of warnings +#[allow(unconditional_recursion)] +#[allow(clippy::only_used_in_recursion)] +// FUTURE: termination_check +#[ensures(result == 2*x)] +pub fn bad_double(x: i64) -> i64 { + let y = bad_double(x - 1); + y + 2 +} diff --git a/chapter3/src/examples/example_3_0_2.rs b/chapter3/src/examples/example_3_0_2.rs new file mode 100644 index 0000000..bd9e0b9 --- /dev/null +++ b/chapter3/src/examples/example_3_0_2.rs @@ -0,0 +1,16 @@ +use prusti_contracts::*; + +// 3.0_2.dfy +// method PartialId(x: int) returns (y: int) + +// Note (2022-10-19): Neither rustc, clippy or Prusti generate any warnings/errors on this code + +// FUTURE: termination_check +#[ensures(result == x)] +pub fn partial_id(x: i64) -> i64 { + if x % 2 == 0 { + x + } else { + partial_id(x) + } +} diff --git a/chapter3/src/examples/example_3_0_3.rs b/chapter3/src/examples/example_3_0_3.rs new file mode 100644 index 0000000..07aee11 --- /dev/null +++ b/chapter3/src/examples/example_3_0_3.rs @@ -0,0 +1,51 @@ +use prusti_contracts::*; + +// 3.0_3.dfy +// method Squarish(x: int, guess: int) returns (y: int) + +// Note (2022-10-19): Neither rustc, clippy or Prusti generate any warnings/errors on this code + +// FUTURE: termination_check +// Note: this is not a perfect translation, since Dafny has non-deterministic match statements +// See attempts at non-determinism below +#[ensures(result == x * x)] +pub fn squarish(x: i64, guess: i64) -> i64 { + if guess == x * x { + guess + } else if true { + squarish(x, guess - 1) + } else { + squarish(x, guess + 1) + } +} + +#[ensures(result == x * x)] +pub fn squarish_non_deterministic(x: i64, guess: i64) -> i64 { + loop { + let r: u64 = rand::random::() % 3; + if r == 0 && guess == x * x { + return guess; + } else if r == 1 { + return squarish(x, guess - 1); + } else if r == 2 { + return squarish(x, guess + 1); + } + } +} + +// This function is non-deterministic from Prusti's point of view: +#[trusted] +pub fn rand_bool() -> bool { + true +} + +#[ensures(result == x * x)] +pub fn squarish_non_deterministic_2(x: i64, guess: i64) -> i64 { + if rand_bool() && guess == x * x { + guess + } else if rand_bool() { + squarish(x, guess - 1) + } else { + squarish(x, guess + 1) + } +} diff --git a/chapter3/src/examples/example_3_0_4.rs b/chapter3/src/examples/example_3_0_4.rs new file mode 100644 index 0000000..7df78f1 --- /dev/null +++ b/chapter3/src/examples/example_3_0_4.rs @@ -0,0 +1,13 @@ +use prusti_contracts::*; + +// 3.0_4.dfy +// method Impossible(x: int) returns (y: int) + +// Adding this to decrease the amount of warnings +#[allow(unconditional_recursion)] +#[allow(clippy::only_used_in_recursion)] +// FUTURE: termination_check +#[ensures(result % 2 == 0 && result == 10 * x - 3)] +pub fn impossible(x: i64) -> i64 { + impossible(x) +} diff --git a/chapter3/src/examples/example_3_0_5.rs b/chapter3/src/examples/example_3_0_5.rs new file mode 100644 index 0000000..b0dc16f --- /dev/null +++ b/chapter3/src/examples/example_3_0_5.rs @@ -0,0 +1,12 @@ +use prusti_contracts::*; + +// 3.0_5.dfy +// function method Dubious(): int + +// Adding this to decrease the amount of warnings +#[allow(unconditional_recursion)] +// FUTURE: termination_check +#[pure] +pub fn dubious() -> i64 { + 1 + dubious() +} diff --git a/chapter3/src/examples/example_3_1_1.rs b/chapter3/src/examples/example_3_1_1.rs new file mode 100644 index 0000000..010a220 --- /dev/null +++ b/chapter3/src/examples/example_3_1_1.rs @@ -0,0 +1,14 @@ +use prusti_contracts::*; + +// 3.1_1.dfy +// function Fib(n: nat): nat + +#[pure] +// #[decreases(n)] // FUTURE: termination_check +pub fn fib(n: u64) -> u64 { + if n < 2 { + n + } else { + fib(n - 2) + fib(n - 1) + } +} diff --git a/chapter3/src/examples/example_3_1_2.rs b/chapter3/src/examples/example_3_1_2.rs new file mode 100644 index 0000000..e8d61fb --- /dev/null +++ b/chapter3/src/examples/example_3_1_2.rs @@ -0,0 +1,45 @@ +use prusti_contracts::*; + +// 3.1_2.dfy +// function SeqSum(s: seq, lo: int, hi: int): int + +// FUTURE: seq_support +// Sequences are replaced with slices in this example + +pub fn slice_sum(s: &[i64]) -> i64 { + // if s.is_empty() { // FUTURE: std_lib_extern_spec_enhancement + #[allow(clippy::len_zero)] + if s.len() == 0 { + 0 + } else { + s[0] + slice_sum(&s[1..s.len()]) + } +} + +#[pure] +#[requires(lo <= hi && hi <= s.len())] +// #[decreases(hi - lo)] // FUTURE: termination_check +pub fn slice_sum_index(s: &[i64], lo: usize, hi: usize) -> i64 { + if lo == hi { + 0 + } else { + s[lo] + slice_sum_index(s, lo + 1, hi) + } +} + +// FUTURE: std_lib_extern_spec_enhancement +// #[pure] +// pub fn slice_sum_iter(s: &[i64]) -> i64 { +// s.iter().sum() +// } + +#[pure] +pub fn slice_sum_recursive(s: &[i64]) -> i64 { + // if s.is_empty() { // FUTURE: std_lib_extern_spec_enhancement + #[allow(clippy::len_zero)] + if s.len() == 0 { + 0 + } else { + s[0] + slice_sum_recursive(&s[1..s.len()]) + } +} diff --git a/chapter3/src/examples/example_3_3_0.rs b/chapter3/src/examples/example_3_3_0.rs new file mode 100644 index 0000000..f9bb9e4 --- /dev/null +++ b/chapter3/src/examples/example_3_3_0.rs @@ -0,0 +1,22 @@ +use prusti_contracts::*; + +// 3.3.0.dfy +// method RequiredStudyTime(c: nat) returns (hours: nat) +// method Study(n: nat, h: nat) + +#[trusted] +pub fn required_study_time(c: u64) -> u64 { + unimplemented!() +} + +// #[decreases(n, h)] // FUTURE: termination_check +pub fn study(n: u64, h: u64) { + if h != 0 { + study(n, h - 1); + } else if n == 0 { + } else { + let hours = required_study_time(n - 1); + + study(n - 1, hours); + } +} diff --git a/chapter3/src/examples/example_3_3_1.rs b/chapter3/src/examples/example_3_3_1.rs new file mode 100644 index 0000000..2420a1a --- /dev/null +++ b/chapter3/src/examples/example_3_3_1.rs @@ -0,0 +1,15 @@ +use prusti_contracts::*; + +// 3.3.1.dfy +// function Ack(m: nat, n: nat): nat + +// #[decreases(m, n)] // FUTURE: termination_check +pub fn ack(m: u64, n: u64) -> u64 { + if m == 0 { + n + 1 + } else if n == 0 { + ack(m - 1, 1) + } else { + ack(m - 1, ack(m, n - 1)) + } +} diff --git a/chapter3/src/examples/example_3_3_2.rs b/chapter3/src/examples/example_3_3_2.rs new file mode 100644 index 0000000..091084d --- /dev/null +++ b/chapter3/src/examples/example_3_3_2.rs @@ -0,0 +1,31 @@ +use prusti_contracts::*; + +// 3.3.2.dfy +// method RequiredStudyTime(c: nat) returns (hours: nat) +// method StudyPlan(n: nat) +// method Learn(n: nat, h: nat) + +#[trusted] +pub fn required_study_time(c: u64) -> u64 { + unimplemented!() +} + +#[requires(n <= 40)] +// #[decreases(40 - n)] // FUTURE: termination_check +pub fn study_plan(n: u64) { + if n == 40 { + } else { + let hours = required_study_time(n); + learn(n, hours); + } +} + +#[requires(n < 40)] +// #[decreases(40 - n, h)] // FUTURE: termination_check +pub fn learn(n: u64, h: u64) { + if h == 0 { + study_plan(n + 1); + } else { + learn(n, h - 1); + } +} diff --git a/chapter3/src/examples/example_3_3_3_1.rs b/chapter3/src/examples/example_3_3_3_1.rs new file mode 100644 index 0000000..c9221cd --- /dev/null +++ b/chapter3/src/examples/example_3_3_3_1.rs @@ -0,0 +1,13 @@ +use prusti_contracts::*; + +// 3.3.3_1.dfy +// function ExpLess1(n: nat): nat + +// FUTURE: termination_check +pub fn exp_less1(n: u64) -> u64 { + if n == 0 { + 0 + } else { + 2 * exp_less1(n - 1) + 1 + } +} diff --git a/chapter3/src/examples/example_3_3_3_2.rs b/chapter3/src/examples/example_3_3_3_2.rs new file mode 100644 index 0000000..c48b4e0 --- /dev/null +++ b/chapter3/src/examples/example_3_3_3_2.rs @@ -0,0 +1,29 @@ +use prusti_contracts::*; + +// 3.3.3_2.dfy +// function ExpLess1(n: nat): nat +// function ExpLess2(n: nat): nat + +// FUTURE: mutually_rec_pure_fn +// Issue: https://github.com/viperproject/prusti-dev/issues/1214 + +#[pure] +// FUTURE: termination_check +pub fn exp_less1(n: u64) -> u64 { + if n == 0 { + 0 + } else { + 2 * exp_less2(n - 1) + 1 + } +} + +#[pure] +// FUTURE: termination_check +#[requires(1 <= n)] +pub fn exp_less2(n: u64) -> u64 { + if n == 0 { + 0 + } else { + 2 * exp_less1(n - 1) + 1 + } +} \ No newline at end of file diff --git a/chapter3/src/exercises.rs b/chapter3/src/exercises.rs new file mode 100644 index 0000000..1242a07 --- /dev/null +++ b/chapter3/src/exercises.rs @@ -0,0 +1,16 @@ +pub mod exercise_3_0; +pub mod exercise_3_1; +pub mod exercise_3_11; +pub mod exercise_3_12; // Bug in book, fixed here +pub mod exercise_3_13; +pub mod exercise_3_2; +pub mod exercise_3_3; +pub mod exercise_3_4; +pub mod exercise_3_5; +pub mod exercise_3_6; +pub mod exercise_3_7; +pub mod exercise_3_8; +pub mod exercise_3_9; +// pub mod exercise_3_14; // BUGGED, see: https://github.com/viperproject/prusti-dev/issues/1214 +pub mod exercise_3_15; +pub mod exercise_3_16; diff --git a/chapter3/src/exercises/exercise_3_0.rs b/chapter3/src/exercises/exercise_3_0.rs new file mode 100644 index 0000000..b0407f0 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_0.rs @@ -0,0 +1,14 @@ +use prusti_contracts::*; + +// 3.0.dfy +// function F(x: int): int + +#[pure] +// #[decreases(x)] // FUTURE: termination_check +pub fn f(x: i64) -> i64 { + if x < 10 { + x + } else { + f(x - 1) + } +} diff --git a/chapter3/src/exercises/exercise_3_1.rs b/chapter3/src/exercises/exercise_3_1.rs new file mode 100644 index 0000000..3577d59 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_1.rs @@ -0,0 +1,14 @@ +use prusti_contracts::*; + +// 3.1.dfy +// function G(x: int): int + +#[pure] +// #[decreases(x)] // FUTURE: termination_check +pub fn g(x: i64) -> i64 { + if 0 <= x { + g(x - 2) + } else { + x + } +} diff --git a/chapter3/src/exercises/exercise_3_11.rs b/chapter3/src/exercises/exercise_3_11.rs new file mode 100644 index 0000000..c2892c9 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_11.rs @@ -0,0 +1,22 @@ +use prusti_contracts::*; + +// 3.11.dfy +// method RequiredStudyTime(c: nat) returns (hours: nat) +// method Study(n: nat, h: nat) + +#[trusted] +pub fn required_study_time(c: u64) -> u64 { + unimplemented!() +} + +// #[decreases(n * 200 + h + n)] // FUTURE: termination_check +pub fn study(n: u64, h: u64) { + if h != 0 { + study(n, h - 1); + } else if n == 0 { + } else { + let hours = required_study_time(n - 1); + + study(n - 1, hours); + } +} diff --git a/chapter3/src/exercises/exercise_3_12.rs b/chapter3/src/exercises/exercise_3_12.rs new file mode 100644 index 0000000..893064a --- /dev/null +++ b/chapter3/src/exercises/exercise_3_12.rs @@ -0,0 +1,51 @@ +use prusti_contracts::*; + +// 3.12.dfy +// method RequiredStudyTime(c: nat) returns (hours: nat) +// method StudyPlan(n: nat) +// method Learn(n: nat, h: nat) +// method Outer(a: nat) +// method Inner(a: nat, b: nat) + +#[trusted] +pub fn required_study_time(c: u64) -> u64 { + unimplemented!() +} + +#[requires(n <= 40)] +// #[decreases(40 - n)] // FUTURE: termination_check +pub fn study_plan(n: u64) { + if n == 40 { + } else { + let hours = required_study_time(n); + learn(n, hours); + } +} + +#[requires(n < 40)] +// #[decreases(40 - n, h)] // FUTURE: termination_check +pub fn learn(n: u64, h: u64) { + if h == 0 { + study_plan(n + 1); + } else { + learn(n, h - 1); + } +} + +// #[decreases(a, a)] // FUTURE: termination_check +pub fn outer(a: u64) { + if a != 0 { + let b = required_study_time(a - 1); + inner(a, b); + } +} + +#[requires(a != 0)] // Note: Fix for a bug in the book +// #[decreases(a, 1, b)] // FUTURE: termination_check +pub fn inner(a: u64, b: u64) { + if b == 0 { + outer(a - 1); // Note: This is present in the book draft (Dafny code fails too) + } else { + inner(a, b - 1); + } +} diff --git a/chapter3/src/exercises/exercise_3_13.rs b/chapter3/src/exercises/exercise_3_13.rs new file mode 100644 index 0000000..5198236 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_13.rs @@ -0,0 +1,49 @@ +use prusti_contracts::*; + +// 3.13.dfy +// method RequredStudyTime(c: nat) returns (hours: nat) +// method StudyPlan(n: nat) +// method Outer(a: nat) +// method Inner(a: nat, b: nat) + +#[trusted] +pub fn required_study_time(c: u64) -> u64 { + unimplemented!() +} + +#[requires(n <= 40)] +// #[decreases(40 - n)] // FUTURE: termination_check +pub fn study_plan(n: u64) { + if n == 40 { + } else { + let hours = required_study_time(n); + learn(n, hours); + } +} + +#[requires(n < 40)] +// #[decreases(40 - n, h)] // FUTURE: termination_check +pub fn learn(n: u64, h: u64) { + if h == 0 { + study_plan(n + 1); + } else { + learn(n, h - 1); + } +} + +// #[decreases(a, 0)] // FUTURE: termination_check +pub fn outer(a: u64) { + if a != 0 { + let b = required_study_time(a - 1); + inner(a - 1, b); + } +} + +// #[decreases(a, 1, b)] // FUTURE: termination_check +pub fn inner(a: u64, b: u64) { + if b == 0 { + outer(a); + } else { + inner(a, b - 1); + } +} diff --git a/chapter3/src/exercises/exercise_3_14.rs b/chapter3/src/exercises/exercise_3_14.rs new file mode 100644 index 0000000..5a9573f --- /dev/null +++ b/chapter3/src/exercises/exercise_3_14.rs @@ -0,0 +1,29 @@ +use prusti_contracts::*; + +// 3.14.dfy +// function F(n: nat): nat +// function M(n: nat): nat + +// BUG: f() encoded as both a Viper Function and a Method +// FUTURE: mutually_rec_pure_fn +// See: https://github.com/viperproject/prusti-dev/issues/1214 + +#[pure] +// #[decreases(n, 1)] // FUTURE: termination_check +pub fn f(n: u64) -> u64 { + if n == 0 { + 1 + } else { + n - m(f(n - 1)) + } +} + +#[pure] +// #[decreases(n, 0)] // FUTURE: termination_check +pub fn m(n: u64) -> u64 { + if n == 0 { + 0 + } else { + n - f(m(n - 1)) + } +} \ No newline at end of file diff --git a/chapter3/src/exercises/exercise_3_15.rs b/chapter3/src/exercises/exercise_3_15.rs new file mode 100644 index 0000000..ae20bc0 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_15.rs @@ -0,0 +1,31 @@ +use prusti_contracts::*; + +// 3.15.dfy +// method RequiredStudyTime(c: nat) returns (hours: nat) +// method StudyPlan(n: nat) +// method Learn(n: nat, h: nat) + +#[trusted] +pub fn required_study_time(c: u64) -> u64 { + unimplemented!() +} + +#[requires(n <= 40)] +// #[decreases(40 - n, 1, 0)] // FUTURE: termination_check +pub fn study_plan(n: u64) { + if n == 40 { + } else { + let hours = required_study_time(n); + learn(n, hours); + } +} + +#[requires(n < 40)] +// #[decreases(40 - n, 0, h)] // FUTURE: termination_check +pub fn learn(n: u64, h: u64) { + if h == 0 { + study_plan(n + 1); + } else { + learn(n, h - 1); + } +} diff --git a/chapter3/src/exercises/exercise_3_16.rs b/chapter3/src/exercises/exercise_3_16.rs new file mode 100644 index 0000000..d395efa --- /dev/null +++ b/chapter3/src/exercises/exercise_3_16.rs @@ -0,0 +1,18 @@ +use prusti_contracts::*; + +// 3.16.dfy +// function F(x: nat, y: nat): int + +#[pure] +// #[decreases(x % 2 == 1, if x % 2 == 1 {x} else {1000 - x})] // FUTURE: termination_check +pub fn f(x: u64, y: u64) -> u64 { + if 1000 <= x { + x + y + } else if x % 2 == 0 { + f(x + 2, y + 1) + } else if x < 6 { + f(2 * y, y) + } else { + f(x - 4, y + 3) + } +} diff --git a/chapter3/src/exercises/exercise_3_2.rs b/chapter3/src/exercises/exercise_3_2.rs new file mode 100644 index 0000000..f3a51ce --- /dev/null +++ b/chapter3/src/exercises/exercise_3_2.rs @@ -0,0 +1,14 @@ +use prusti_contracts::*; + +// 3.2.dfy +// function H(x: int): int + +#[pure] +// #[decreases(x + 60)] // FUTURE: termination_check +pub fn h(x: i64) -> i64 { + if x < -60 { + x + } else { + h(x - 1) + } +} diff --git a/chapter3/src/exercises/exercise_3_3.rs b/chapter3/src/exercises/exercise_3_3.rs new file mode 100644 index 0000000..e0cdb6f --- /dev/null +++ b/chapter3/src/exercises/exercise_3_3.rs @@ -0,0 +1,16 @@ +use prusti_contracts::*; + +// 3.3.dfy +// function I(x: nat, y: nat): int + +#[pure] +// #[decreases(x + y)] // FUTURE: termination_check +pub fn i(x: u64, y: u64) -> u64 { + if x == 0 || y == 0 { + 12 + } else if x % 2 == y % 2 { + i(x - 1, y) + } else { + i(x, y - 1) + } +} diff --git a/chapter3/src/exercises/exercise_3_4.rs b/chapter3/src/exercises/exercise_3_4.rs new file mode 100644 index 0000000..fc554d6 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_4.rs @@ -0,0 +1,16 @@ +use prusti_contracts::*; + +// 3.4.dfy +// function J(x: nat, y: nat): int + +#[pure] +// #[decreases(4 * x + y)] // FUTURE: termination_check +pub fn j(x: u64, y: u64) -> u64 { + if x == 0 { + y + } else if y == 0 { + j(x - 1, 3) + } else { + j(x, y - 1) + } +} diff --git a/chapter3/src/exercises/exercise_3_5.rs b/chapter3/src/exercises/exercise_3_5.rs new file mode 100644 index 0000000..88772d0 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_5.rs @@ -0,0 +1,18 @@ +use prusti_contracts::*; + +// 3.5.dfy +// function K(x: nat, y: nat, z: nat): int + +#[allow(clippy::only_used_in_recursion)] +#[pure] +// #[decreases(x + y)] // FUTURE: termination_check +#[requires(x >= 0 && y >= 0 && z >= 0)] +pub fn k(x: i64, y: i64, z: i64) -> i64 { + if x < 10 || y < 5 { + x + y + } else if z == 0 { + k(x - 1, y, 5) + } else { + k(x, y - 1, z - 1) + } +} diff --git a/chapter3/src/exercises/exercise_3_6.rs b/chapter3/src/exercises/exercise_3_6.rs new file mode 100644 index 0000000..8679bdc --- /dev/null +++ b/chapter3/src/exercises/exercise_3_6.rs @@ -0,0 +1,14 @@ +use prusti_contracts::*; + +// 3.6.dfy +// function L(x: int): int + +#[pure] +// #[decreases(100 - x)] // FUTURE: termination_check +pub fn l(x: i64) -> i64 { + if x < 100 { + l(x + 1) + 10 + } else { + x + } +} diff --git a/chapter3/src/exercises/exercise_3_7.rs b/chapter3/src/exercises/exercise_3_7.rs new file mode 100644 index 0000000..50a946a --- /dev/null +++ b/chapter3/src/exercises/exercise_3_7.rs @@ -0,0 +1,18 @@ +use prusti_contracts::*; + +// 3.7.dfy +// function G(n: nat): nat + +#[pure] +// #[decreases(n)] // FUTURE: termination_check +// Note: This is required since the decreases notation doesn't exist (yet), +// otherwise there is an error for potentially negative results of unsigned integer subtraction +// `result <= n` can be derived from `decreases(n)` +#[ensures(result <= n)] +pub fn g(n: u64) -> u64 { + if n == 0 { + 0 + } else { + n - g(g(n - 1)) + } +} diff --git a/chapter3/src/exercises/exercise_3_8.rs b/chapter3/src/exercises/exercise_3_8.rs new file mode 100644 index 0000000..019cc32 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_8.rs @@ -0,0 +1,14 @@ +use prusti_contracts::*; + +// 3.8.dfy +// function M(x: int, b: bool): int + +#[pure] +// #[decreases(!b)] // FUTURE: termination_check +pub fn m(x: i64, b: bool) -> i64 { + if b { + x + } else { + m(x + 25, true) + } +} diff --git a/chapter3/src/exercises/exercise_3_9.rs b/chapter3/src/exercises/exercise_3_9.rs new file mode 100644 index 0000000..67cd162 --- /dev/null +++ b/chapter3/src/exercises/exercise_3_9.rs @@ -0,0 +1,16 @@ +use prusti_contracts::*; + +// 3.9.dfy +// function N(x: int, y: int, b: bool): int + +#[pure] +// #[decreases(x, b)] // FUTURE: termination_check +pub fn n(x: i64, y: i64, b: bool) -> i64 { + if x <= 0 || y <= 0 { + x + y + } else if b { + n(x, y + 3, !b) + } else { + n(x - 1, y, true) + } +} diff --git a/chapter3/src/lib.rs b/chapter3/src/lib.rs new file mode 100644 index 0000000..74e8d1e --- /dev/null +++ b/chapter3/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; diff --git a/chapter4/Cargo.lock b/chapter4/Cargo.lock new file mode 100644 index 0000000..8db21af --- /dev/null +++ b/chapter4/Cargo.lock @@ -0,0 +1,25 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "chapter4" +version = "0.1.0" +dependencies = [ + "prusti-contracts", +] + +[[package]] +name = "prusti-contracts" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0a55ba828aceca3c0786a6dd252e1d219720d15f4c454b70fee282111469c940" +dependencies = [ + "prusti-contracts-proc-macros", +] + +[[package]] +name = "prusti-contracts-proc-macros" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b74f012498f2f2239b7c99cb07c6fd18271587163d1710a242f00b6af5d9043d" diff --git a/chapter4/Cargo.toml b/chapter4/Cargo.toml new file mode 100644 index 0000000..65dc8c7 --- /dev/null +++ b/chapter4/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "chapter4" +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.1.4" + +[features] +# To check failing code too, either enable ["pass", "fail"] as the default below, +# or run: cargo clippy --all-features -- -D warnings +default = ["pass"] +# default = ["pass", "fail"] +pass = [] # Code that can be verified +fail = [] # Code that cannot be verified (yet) diff --git a/chapter4/Prusti.toml b/chapter4/Prusti.toml new file mode 100644 index 0000000..1e6bcab --- /dev/null +++ b/chapter4/Prusti.toml @@ -0,0 +1 @@ +check_overflows = false \ No newline at end of file diff --git a/chapter4/src/examples.rs b/chapter4/src/examples.rs new file mode 100644 index 0000000..23bc503 --- /dev/null +++ b/chapter4/src/examples.rs @@ -0,0 +1,12 @@ +#[cfg(feature = "pass")] +mod pass { + mod example_4_1_1_to_4_2_2; + mod example_4_2_3_and_4_2_4; + mod example_4_4; + mod example_4_5_1_and_4_5_2; +} + +#[cfg(feature = "fail")] +mod fail { + mod example_4_6; // FUTURE: reference_typed_structures +} \ No newline at end of file diff --git a/chapter4/src/examples/fail/example_4_6.rs b/chapter4/src/examples/fail/example_4_6.rs new file mode 100644 index 0000000..081cde9 --- /dev/null +++ b/chapter4/src/examples/fail/example_4_6.rs @@ -0,0 +1,68 @@ +use prusti_contracts::*; + +// 4.6.dfy +// datatype Expr = Const(nat) | Var(string) |Node(op: Op, args: List) +// datatype Op = Add | Mul +// datatype List = Nil | Cons(head: T, tail: List) +// function method Eval(e: Expr, env: map): nat +// function method EvalList(args: List, op: Op, env: map): nat + +pub enum Op { + Add, + Mul, +} + +pub enum List { + Nil, + Cons(T, Box>), +} + +pub enum Expr { + Const(u64), + Var(String), + Node(Op, Box>), +} + +// FUTURE: map_support +use std::collections::HashMap; +type Environment = HashMap; + +use Expr::*; +use List::*; +use Op::*; + +impl Expr { + // FUTURE: reference_typed_structures + #[pure] + pub fn eval(&self, env: &Environment) -> u64 { + match self { + Const(c) => *c, + Var(s) => { + if let Some(&val) = env.get(s) { + val + } else { + 0 + } + } + Node(op, args) => Expr::eval_list(args, op, env), + } + } + + #[pure] + fn eval_list(args: &List, op: &Op, env: &Environment) -> u64 { + match args { + Nil => match op { + Add => 0, + Mul => 1, + }, + Cons(e, tail) => { + let v0 = e.eval(env); + let v1 = Expr::eval_list(tail, op, env); + match op { + Add => v0 + v1, + Mul => v0 * v1, + } + } + } + } +} diff --git a/chapter4/src/examples/pass/example_4_1_1_to_4_2_2.rs b/chapter4/src/examples/pass/example_4_1_1_to_4_2_2.rs new file mode 100644 index 0000000..7648e33 --- /dev/null +++ b/chapter4/src/examples/pass/example_4_1_1_to_4_2_2.rs @@ -0,0 +1,105 @@ +use prusti_contracts::*; + +// 4.1_1.dfy +// datatype BYTree = BlueLeaf | YellowLeaf| Node(BYTree, BYTree) +// function BlueCount(t: BYTree): nat +// 4.1_2.dfy +// function LeftLinks(t: BYTree): nat +// 4.2_1.dfy +// predicate IsNode(t: BYTree) +// 4.2_2.dfy +// function GetLeft(t: BYTree): BYTree + +// #[derive(std::fmt::Debug)] // FUTURE: derive_debug +enum BYTree { + BlueLeaf, + YellowLeaf, + Node(Box, Box), +} + +impl BYTree { + // example_4.1_1 + // FUTURE: termination_check + #[pure] + pub fn blue_count(&self) -> u64 { + match self { + BYTree::BlueLeaf => 1, + BYTree::YellowLeaf => 0, + BYTree::Node(left, right) => left.blue_count() + right.blue_count(), + } + } + + // example_4.1_2 + #[pure] + pub fn left_links(&self) -> u64 { + match self { + BYTree::BlueLeaf => 1, + BYTree::YellowLeaf => 0, + BYTree::Node(left, _) => left.left_links(), + } + } + + // example_4.2_1 + #[pure] + pub fn is_node(&self) -> bool { + matches!(self, BYTree::Node(..)) + } + + // example_4.2_2 + #[pure] + #[requires(self.is_node())] + pub fn get_left(&self) -> &BYTree { + match self { + BYTree::Node(left, _) => left, + _ => unreachable!(), + } + } +} + +use std::fmt; + +impl fmt::Debug for BYTree { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + BYTree::BlueLeaf => f.write_str("BlueLeaf")?, + BYTree::YellowLeaf => f.write_str("YellowLeaf")?, + BYTree::Node(left, right) => { + f.write_str("[")?; + left.fmt(f)?; + f.write_str(", ")?; + right.fmt(f)?; + f.write_str("]")?; + } + } + Ok(()) + } +} + +// Note: These tests are not part of the book +#[cfg(test)] +mod tests { + use super::*; + + // these tests are ignored by Prusti (due to #[cfg(test)] and #[test]) + + #[test] + fn test_blue_count() { + use BYTree::*; + let left = Node(Box::new(BlueLeaf), Box::new(YellowLeaf)); + let right = Node(Box::new(YellowLeaf), Box::new(BlueLeaf)); + let tree = Node(Box::new(left), Box::new(right)); + let blue_count = tree.blue_count(); + assert_eq!(blue_count, 2); + } + + #[test] + fn test_debug_print() { + use BYTree::*; + let left = BlueLeaf; + let right = YellowLeaf; + let tree = Node(Box::new(left), Box::new(right)); + let result = format!("{tree:?}"); // Note: Can only debug print here if it is implemented/derived for the BYTree // FUTURE: derive_debug + println!("{result}"); + assert_eq!(result, "[BlueLeaf, YellowLeaf]"); + } +} diff --git a/chapter4/src/examples/pass/example_4_2_3_and_4_2_4.rs b/chapter4/src/examples/pass/example_4_2_3_and_4_2_4.rs new file mode 100644 index 0000000..39a029e --- /dev/null +++ b/chapter4/src/examples/pass/example_4_2_3_and_4_2_4.rs @@ -0,0 +1,29 @@ +use prusti_contracts::*; + +// 4.2_3.dfy +// datatype BYTree = BlueLeaf | YellowLeaf| Node(left: BYTree, right: BYTree) +// 4.2_4.dfy +// function BlueCount(t: BYTree): nat + +// example_4.2_3 +pub enum BYTree { + BlueLeaf, + YellowLeaf, + Node { + left: Box, + right: Box, + }, +} + +// example_4.2_4 +impl BYTree { + // FUTURE: termination_check + #[pure] + pub fn blue_count(&self) -> u64 { + match self { + BYTree::BlueLeaf => 1, + BYTree::YellowLeaf => 0, + BYTree::Node { left, right } => left.blue_count() + right.blue_count(), + } + } +} diff --git a/chapter4/src/examples/pass/example_4_4.rs b/chapter4/src/examples/pass/example_4_4.rs new file mode 100644 index 0000000..1d9c736 --- /dev/null +++ b/chapter4/src/examples/pass/example_4_4.rs @@ -0,0 +1,35 @@ +use prusti_contracts::*; + +// 4.4.dfy +// datatype ColoredTree = Leaf(Color) | Node(ColoredTree, ColoredTree) +// datatype Color = Blue | Yellow | Green | Red +// predicate IsSwedishFlagColor(c: Color) +// predicate IsLithuanianFlagColor(c: Color) + +pub enum Color { + Blue, + Yellow, + Green, + Red, +} + +// #[derive(Debug)] // FUTURE: derive_debug +pub enum ColoredTree { + Leaf(Color), + Node(Box, Box), +} + +use Color::*; +use ColoredTree::*; + +impl Color { + #[pure] + pub fn is_swedish_flag_color(&self) -> bool { + matches!(self, Blue | Yellow) + } + + #[pure] + pub fn is_lithuanian_flag_color(&self) -> bool { + !matches!(self, Blue) + } +} diff --git a/chapter4/src/examples/pass/example_4_5_1_and_4_5_2.rs b/chapter4/src/examples/pass/example_4_5_1_and_4_5_2.rs new file mode 100644 index 0000000..38f3475 --- /dev/null +++ b/chapter4/src/examples/pass/example_4_5_1_and_4_5_2.rs @@ -0,0 +1,52 @@ +use prusti_contracts::*; + +// 4.5.1.dfy +// datatype Tree = Leaf(data: T) | Node(left: Tree, right: Tree) +// datatype Color = Blue | Yellow | Green | Red +// predicate AllBlue(t: Tree) +// 4.5.2.dfy +// function Size(t: Tree): nat +// function SizeOmit(t: Tree): nat + +pub enum Color { + Blue, + Yellow, + Green, + Red, +} + +pub enum Tree { + Leaf(T), + Node(Box>, Box>), +} + +use Color::*; +use Tree::*; + +// example_4.5_1 +impl Tree { + // FUTURE: termination_check + #[pure] + pub fn all_blue(&self) -> bool { + match self { + Leaf(Blue) => true, + Node(left, right) => left.all_blue() && right.all_blue(), + _ => false, + } + } +} + +// example_4.5_2 +impl Tree { + // FUTURE: termination_check + #[pure] + pub fn size(&self) -> u64 { + match self { + Leaf(_) => 1, + Node(left, right) => { + // Tree::::size(left) + Tree::::size(right) + left.size() + right.size() + } + } + } +} diff --git a/chapter4/src/exercises.rs b/chapter4/src/exercises.rs new file mode 100644 index 0000000..6e9e6f5 --- /dev/null +++ b/chapter4/src/exercises.rs @@ -0,0 +1,13 @@ +#[cfg(feature = "pass")] +mod pass { + mod exercise_4_5; +} + +#[cfg(feature = "fail")] +mod fail { + mod exercise_4_1_to_4_4; // FUTURE: non_copy_types_in_pure_fn + allocation_in_pure_fn + mod exercise_4_6; // FUTURE: non_copy_types_in_pure_fn + allocation_in_pure_fn + mod exercise_4_7; // FUTURE: reference_typed_structures + allocation_in_pure_fn + mod exercise_4_8; // FUTURE: reference_typed_structures + allocation_in_pure_fn + mutually_rec_pure_fn + mod exercise_4_9; // FUTURE: reference_typed_structures + allocation_in_pure_fn + mutually_rec_pure_fn +} \ No newline at end of file diff --git a/chapter4/src/exercises/fail/exercise_4_1_to_4_4.rs b/chapter4/src/exercises/fail/exercise_4_1_to_4_4.rs new file mode 100644 index 0000000..efd84a4 --- /dev/null +++ b/chapter4/src/exercises/fail/exercise_4_1_to_4_4.rs @@ -0,0 +1,140 @@ +use prusti_contracts::*; + +// 4.1.dfy +// datatype BYTree = BlueLeaf | YellowLeaf| Node(BYTree, BYTree) +// function ReverseColors(t: BYTree): BYTree +// 4.2.dfy +// function Oceanize(t: BYTree): BYTree +// 4.3.dfy +// function LeftLinks(t: BYTree): nat +// 4.4.dfy +// predicate HasLeftTree1(t: BYTree, u: BYTree) +// predicate HasLeftTree2(t: BYTree, u: BYTree) + +// #[derive(Debug)] // FUTURE: derive_debug +// #[derive(PartialEq, Eq)] // FUTURE: derive_partial_eq +#[derive(Clone)] +pub enum BYTree { + BlueLeaf, + YellowLeaf, + Node(Box, Box), +} + +// // FUTURE: allocation_in_pure_fn +// #[extern_spec] +// impl Box { +// #[pure] +// #[trusted] +// fn new(t: T) -> Self; +// } + +use BYTree::*; + +// FUTURE: non_copy_types_in_pure_fn +// FUTURE: allocation_in_pure_fn +#[pure] +pub fn reverse_colors(t: &BYTree) -> BYTree { + match t { + BlueLeaf => BlueLeaf, + YellowLeaf => YellowLeaf, + Node(left, right) => Node( + Box::new(reverse_colors(left)), + Box::new(reverse_colors(right)), + ), + } +} + +impl BYTree { + // Exercise 4.1 + // FUTURE: non_copy_types_in_pure_fn + // FUTURE: allocation_in_pure_fn + #[pure] + pub fn reverse_colors(&self) -> BYTree { + match self { + BlueLeaf => YellowLeaf, + YellowLeaf => BlueLeaf, + Node(left, right) => Node( + Box::new(right.reverse_colors()), + Box::new(left.reverse_colors()), + ), + } + } + + // Exercise 4.2 + // FUTURE: allocation_in_pure_fn + // FUTURE: allocation_in_pure_fn + #[pure] + pub fn oceanize(&self) -> BYTree { + match self { + BlueLeaf => BlueLeaf, + YellowLeaf => BlueLeaf, + Node(left, right) => Node(Box::new(left.oceanize()), Box::new(right.oceanize())), + } + } + + // Exercise 4.3 + #[pure] // FUTURE: allocation_in_pure_fn + pub fn left_links(&self) -> u64 { + match self { + BlueLeaf => 1, + YellowLeaf => 0, + Node(left, _) => left.left_links(), + } + } + + // // Exercise 4.4 + // #[pure] // FUTURE: allocation_in_pure_fn + // pub fn has_left_tree(&self, u: &BYTree) -> bool { + // if let Node(left, _) = self { + // left.as_ref() == u // FUTURE: derive_partial_eq + // } else { + // false + // } + // } + + // // Exercise 4.4 + // #[pure] // FUTURE: allocation_in_pure_fn + pub fn has_left_tree(&self, u: &BYTree) -> bool { + fn eq(a: &BYTree, b: &BYTree) -> bool { + match (a, b) { + (BlueLeaf, BlueLeaf) | (YellowLeaf, YellowLeaf) => true, + (Node(a_left, a_right), Node(b_left, b_right)) => { + eq(a_left, b_left) && eq(a_right, b_right) + } + _ => false, + } + } + if let Node(left, _) = self { + eq(left.as_ref(), u) + } else { + false + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + // these tests are ignored by Prusti (due to cfg(test)) + + #[test] + fn test_has_left_tree_0() { + use BYTree::*; + let left = Node(Box::new(BlueLeaf), Box::new(YellowLeaf)); + let u = left.clone(); + let right = Node(Box::new(YellowLeaf), Box::new(BlueLeaf)); + let tree = Node(Box::new(left), Box::new(right)); + assert!(tree.has_left_tree(&u)); + } + + #[test] + fn test_has_left_tree_1() { + use BYTree::*; + let left = Node(Box::new(BlueLeaf), Box::new(YellowLeaf)); + let right = Node(Box::new(YellowLeaf), Box::new(BlueLeaf)); + let u = right.clone(); + let tree = Node(Box::new(left), Box::new(right)); + assert!(!tree.has_left_tree(&u)); + } +} diff --git a/chapter4/src/exercises/fail/exercise_4_6.rs b/chapter4/src/exercises/fail/exercise_4_6.rs new file mode 100644 index 0000000..dfac884 --- /dev/null +++ b/chapter4/src/exercises/fail/exercise_4_6.rs @@ -0,0 +1,43 @@ +use prusti_contracts::*; + +// 4.6.dfy +// datatype Tree = Leaf(data: T) | Node(left: Tree, right: Tree) +// datatype Color = Blue | Yellow | Green | Red + +pub enum Color { + Blue, + Yellow, + Green, + Red, +} + +pub enum Tree { + Leaf(T), + Node(Box>, Box>), +} + +impl Tree { + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + // FUTURE: allocation_in_pure_fn + #[pure] + pub fn mirror_clone(&self) -> Self { + match self { + Tree::Leaf(t) => Tree::Leaf(t.clone()), + Tree::Node(l, r) => Tree::Node(Box::new(r.mirror_clone()), Box::new(l.mirror_clone())), + } + } +} + +impl Tree { + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + // FUTURE: allocation_in_pure_fn + #[pure] + pub fn mirror(self) -> Self { + match self { + Tree::Leaf(t) => Tree::Leaf(t), + Tree::Node(l, r) => Tree::Node(Box::new(r.mirror()), Box::new(l.mirror())), + } + } +} diff --git a/chapter4/src/exercises/fail/exercise_4_7.rs b/chapter4/src/exercises/fail/exercise_4_7.rs new file mode 100644 index 0000000..7248ed0 --- /dev/null +++ b/chapter4/src/exercises/fail/exercise_4_7.rs @@ -0,0 +1,72 @@ +use prusti_contracts::*; + +// Identical to Example 4.6 + +// 4.7.dfy +// datatype Expr = Const(nat) | Var(string) |Node(op: Op, args: List) +// datatype Op = Add | Mul +// datatype List = Nil | Cons(head: T, tail: List) +// function method Eval(e: Expr, env: map): nat +// function method EvalList( op: Op, args: List, env: map): nat + +pub enum Op { + Add, + Mul, +} + +pub enum List { + Nil, + Cons(T, Box>), +} + +pub enum Expr { + Const(u64), + Var(String), + Node(Op, Box>), +} + +use std::collections::HashMap; +type Environment = HashMap; + +use Expr::*; +use List::*; +use Op::*; + +impl Expr { + // FUTURE: termination_check + // FUTURE: allocation_in_pure_fn + // FUTURE: reference_typed_structures + #[pure] + pub fn eval(&self, env: &Environment) -> u64 { + match self { + Const(c) => *c, + Var(s) => { + if let Some(&val) = env.get(s) { + val + } else { + 0 + } + } + Node(op, args) => Expr::eval_list(args, op, env), + } + } + + #[pure] // FUTURE: allocation_in_pure_fn + // #[decreases(args)] // FUTURE: termination_check + fn eval_list(args: &List, op: &Op, env: &Environment) -> u64 { + match args { + Nil => match op { + Add => 0, + Mul => 1, + }, + Cons(e, tail) => { + let v0 = e.eval(env); + let v1 = Expr::eval_list(tail, op, env); + match op { + Add => v0 + v1, + Mul => v0 * v1, + } + } + } + } +} diff --git a/chapter4/src/exercises/fail/exercise_4_8.rs b/chapter4/src/exercises/fail/exercise_4_8.rs new file mode 100644 index 0000000..1c90db8 --- /dev/null +++ b/chapter4/src/exercises/fail/exercise_4_8.rs @@ -0,0 +1,93 @@ +use prusti_contracts::*; + +// First parts identical to Example 4.6 and Exercise 4.7 + +// 4.8.dfy +// datatype Expr = Const(nat) | Var(string) |Node(op: Op, args: List) +// datatype Op = Add | Mul +// datatype List = Nil | Cons(head: T, tail: List) +// function method Eval(e: Expr, env: map): nat +// function method EvalList(args: List, op: Op, env: map): nat +// predicate GoodEnv(e: Expr, env: map) +// predicate helper(args: List, env: map) + +pub enum Op { + Add, + Mul, +} + +pub enum List { + Nil, + Cons(T, Box>), +} + +pub enum Expr { + Const(u64), + Var(String), + Node(Op, Box>), +} + +use std::collections::HashMap; +type Environment = HashMap; + +use Expr::*; +use List::*; +use Op::*; + +impl Expr { + // FUTURE: termination_check + // FUTURE: allocation_in_pure_fn + // FUTURE: reference_typed_structures + #[pure] + pub fn eval(&self, env: &Environment) -> u64 { + match self { + Const(c) => *c, + Var(s) => { + if let Some(&val) = env.get(s) { + val + } else { + 0 + } + } + Node(op, args) => Expr::eval_list(args, op, env), + } + } + + #[pure] // FUTURE: allocation_in_pure_fn + // #[decreases(args)] // FUTURE: termination_check + fn eval_list(args: &List, op: &Op, env: &Environment) -> u64 { + match args { + Nil => match op { + Add => 0, + Mul => 1, + }, + Cons(e, tail) => { + let v0 = e.eval(env); + let v1 = Expr::eval_list(tail, op, env); + match op { + Add => v0 + v1, + Mul => v0 * v1, + } + } + } + } + + // New parts of Exercise 4.8 start here: + // FUTURE: mutually_rec_pure_fn + // FUTURE: termination_check + #[pure] + pub fn good_env(&self, env: &Environment) -> bool { + #[pure] + fn helper(args: &List, env: &Environment) -> bool { + match args { + Nil => true, + Cons(h, t) => h.good_env(env) && helper(t, env), + } + } + match self { + Const(_) => true, + Var(s) => env.contains_key(s), // FUTURE: map_support, std_lib_extern_spec_enhancement + Node(_, args) => helper(args, env), + } + } +} diff --git a/chapter4/src/exercises/fail/exercise_4_9.rs b/chapter4/src/exercises/fail/exercise_4_9.rs new file mode 100644 index 0000000..a14ea4e --- /dev/null +++ b/chapter4/src/exercises/fail/exercise_4_9.rs @@ -0,0 +1,98 @@ +use prusti_contracts::*; + +// First parts identical to Example 4.6 abd Exercise 4.7 + +// 4.9.dfy +// datatype Expr = Const(nat) | Var(string) |Node(op: Op, args: List) +// datatype Op = Add | Mul +// datatype List = Nil | Cons(head: T, tail: List) +// function method Eval(e: Expr, env: map): nat +// function method EvalList(args: List, op: Op, env: map): nat +// predicate GoodEnv(e: Expr, env: map) +// predicate helper(args: List, env: map) + +pub enum Op { + Add, + Mul, +} + +pub enum List { + Nil, + Cons(T, Box>), +} + +pub enum Expr { + Const(u64), + Var(String), + Node(Op, Box>), +} + +use std::collections::HashMap; +type Environment = HashMap; + +use Expr::*; +use List::*; +use Op::*; + +impl Expr { + // FUTURE: termination_check + // FUTURE: allocation_in_pure_fn + // FUTURE: reference_typed_structures + #[pure] + #[requires(self.good_env(env))] + pub fn eval(&self, env: &Environment) -> u64 { + match self { + Const(c) => *c, + Var(s) => { + if let Some(&val) = env.get(s) { + val + } else { + 0 + } + } + Node(op, args) => Expr::eval_list(args, op, env), + } + } + + #[pure] // FUTURE: allocation_in_pure_fn + // #[decreases(args)] // FUTURE: termination_check + #[requires(args.helper(env))] + fn eval_list(args: &List, op: &Op, env: &Environment) -> u64 { + match args { + Nil => match op { + Add => 0, + Mul => 1, + }, + Cons(e, tail) => { + let v0 = e.eval(env); + let v1 = Expr::eval_list(tail, op, env); + match op { + Add => v0 + v1, + Mul => v0 * v1, + } + } + } + } + + // New parts of Exercise 4.8 start here: + // FUTURE: mutually_rec_pure_fn + // FUTURE: termination_check + #[pure] + pub fn good_env(&self, env: &Environment) -> bool { + match self { + Const(_) => true, + Var(s) => env.contains_key(s), // FUTURE: map_support, std_lib_extern_spec_enhancement + Node(_, args) => args.helper(env), + } + } +} + +impl List { + #[pure] + fn helper(&self, env: &Environment) -> bool { + match self { + Nil => true, + Cons(head, tail) => head.good_env(env) && tail.helper(env), + } + } +} diff --git a/chapter4/src/exercises/pass/exercise_4_5.rs b/chapter4/src/exercises/pass/exercise_4_5.rs new file mode 100644 index 0000000..95c67c6 --- /dev/null +++ b/chapter4/src/exercises/pass/exercise_4_5.rs @@ -0,0 +1,42 @@ +use prusti_contracts::*; + +// 4.5.dfy +// datatype ColoredTree = Leaf(Color) | Node(ColoredTree, ColoredTree) +// datatype Color = Blue | Yellow | Green | Red +// predicate IsSwedishFlagColor(c: Color) +// predicate IsSwedishColoredTree(t: ColoredTree) + +pub enum Color { + Blue, + Yellow, + Green, + Red, +} + +pub enum ColoredTree { + Leaf(Color), + Node(Box, Box), +} + +use Color::*; +use ColoredTree::*; + +impl Color { + #[pure] + pub fn is_swedish_flag_color(&self) -> bool { + matches!(self, Blue | Yellow) + } +} + +impl ColoredTree { + // FUTURE: termination_check + #[pure] + pub fn is_swedish_colored_tree(&self) -> bool { + match self { + // Leaf(c) if c.is_swedish_flag_color() => true, // FUTURE: shallow_borrow (not needed here, but it shows the missing feature) + Leaf(c) => c.is_swedish_flag_color(), + Node(l, r) => l.is_swedish_colored_tree() && r.is_swedish_colored_tree(), + _ => false, + } + } +} diff --git a/chapter4/src/lib.rs b/chapter4/src/lib.rs new file mode 100644 index 0000000..74e8d1e --- /dev/null +++ b/chapter4/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; diff --git a/chapter5/Cargo.lock b/chapter5/Cargo.lock new file mode 100644 index 0000000..7309a1f --- /dev/null +++ b/chapter5/Cargo.lock @@ -0,0 +1,25 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "chapter5" +version = "0.1.0" +dependencies = [ + "prusti-contracts", +] + +[[package]] +name = "prusti-contracts" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0a55ba828aceca3c0786a6dd252e1d219720d15f4c454b70fee282111469c940" +dependencies = [ + "prusti-contracts-proc-macros", +] + +[[package]] +name = "prusti-contracts-proc-macros" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b74f012498f2f2239b7c99cb07c6fd18271587163d1710a242f00b6af5d9043d" diff --git a/chapter5/Cargo.toml b/chapter5/Cargo.toml new file mode 100644 index 0000000..72153c4 --- /dev/null +++ b/chapter5/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "chapter5" +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.1.4" + +[features] +# To check failing code too, either enable ["pass", "fail"] as the default below, +# or run: cargo clippy --all-features -- -D warnings +default = ["pass"] +# default = ["pass", "fail"] +pass = [] # Code that can be verified +fail = [] # Code that cannot be verified (yet) diff --git a/chapter5/Prusti.toml b/chapter5/Prusti.toml new file mode 100644 index 0000000..0311c33 --- /dev/null +++ b/chapter5/Prusti.toml @@ -0,0 +1 @@ +check_overflows = false diff --git a/chapter5/src/examples.rs b/chapter5/src/examples.rs new file mode 100644 index 0000000..7ffe42c --- /dev/null +++ b/chapter5/src/examples.rs @@ -0,0 +1,25 @@ +#[cfg(feature = "pass")] +mod pass { + mod example_5_2_1; + mod example_5_2_2; + mod example_5_3_1; + mod example_5_4_0_1; + mod example_5_4_0_2; + mod example_5_5; + mod example_5_5_1; + mod example_5_6; +} + +#[cfg(feature = "fail")] +pub use fail::example_5_8_0::*; + +#[cfg(feature = "fail")] +mod fail { + mod example_5_0; // FUTURE: lemma_induction_proof + mod example_5_1; // FUTURE: lemma_induction_proof + mod example_5_7_0; // FUTURE: allocation_in_pure_fn + non_copy_types_in_pure_fn + std_lib_extern_spec_requirement + mod example_5_7_1; // FUTURE: allocation_in_pure_fn + non_copy_types_in_pure_fn + std_lib_extern_spec_requirement + pub mod example_5_8_0; // FUTURE: allocation_in_pure_fn + non_copy_types_in_pure_fn + map_support + reference_typed_structures + mod example_5_8_1_1; // FUTURE: non_copy_types_in_pure_fn + allocation_in_pure_fn + mod example_5_8_1_2; // FUTURE: non_copy_types_in_pure_fn + allocation_in_pure_fn +} diff --git a/chapter5/src/examples/fail/example_5_0.rs b/chapter5/src/examples/fail/example_5_0.rs new file mode 100644 index 0000000..906d7da --- /dev/null +++ b/chapter5/src/examples/fail/example_5_0.rs @@ -0,0 +1,21 @@ +use prusti_contracts::*; + +// 5.0.dfy +// function method More(x: int): int +// lemma Increasing(x: int) + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: lemma_syntax +// FUTURE: lemma_induction_proof +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing_automatic(x: i64) {} diff --git a/chapter5/src/examples/fail/example_5_1.rs b/chapter5/src/examples/fail/example_5_1.rs new file mode 100644 index 0000000..eb615d1 --- /dev/null +++ b/chapter5/src/examples/fail/example_5_1.rs @@ -0,0 +1,31 @@ +use prusti_contracts::*; + +// 5.1.dfy +// function method More(x: int): int +// lemma Increasing(x: int) +// method ExampleLemmaUse(a: int) + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: lemma_syntax +// FUTURE: lemma_induction_proof +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing(x: i64) {} + +pub fn example_lemma_use(a: i64) { + let b = more(a); + lemma_increasing(a); + lemma_increasing(b); + prusti_assert!(a < b); + let c = more(b); + prusti_assert!(2 <= c - a); +} diff --git a/chapter5/src/examples/fail/example_5_7_0.rs b/chapter5/src/examples/fail/example_5_7_0.rs new file mode 100644 index 0000000..df93d6c --- /dev/null +++ b/chapter5/src/examples/fail/example_5_7_0.rs @@ -0,0 +1,98 @@ +use prusti_contracts::*; + +// 5.7.0.dfy +// datatype Tree +// function Mirror(t: Tree): Tree +// lemma {:induction false} MirrorMirror(t: Tree) + +#[derive(Clone, PartialEq, Eq)] // FUTURE: derive_partial_eq +pub enum Tree { + Leaf(T), + Node(Box>, Box>), +} + +// impl Eq for Tree +// where T: Clone + Eq +// {} + +// impl PartialEq for Tree +// where T: Clone + Eq { +// #[pure] +// fn eq(&self, other: &Self) -> bool { +// // FUTURE: reference_typed_structures +// // FUTURE: std_lib_extern_spec_requirement (PartialEq::eq and Box dereferencing) +// match (self, other) { +// (Tree::Leaf(x), Tree::Leaf(y)) => x == y, +// (Tree::Node(left, right), Tree::Node(other_left, other_right)) => { +// left == right && other_left == other_right +// }, +// _ => false +// } +// } +// // Note: This is a workaround for references in structures not being allowed +// // Here another problem stops the verification: The trait function PartialEq::Eq is not marked +// // as pure in Prusti. Extern spec for the Box dereferenciation are also still needed here. +// // FUTURE: std_lib_extern_spec_requirement +// // #[pure] +// // fn eq(&self, other: &Self) -> bool { +// // match self { +// // Tree::Leaf(x) => match other { +// // Tree::Leaf(y) => x == y, +// // _ => false +// // }, +// // Tree::Node(left, right) => { +// // match other { +// // Tree::Node(other_left, other_right) => { +// // other_left == left && +// // other_right == right +// // }, +// // _ => false +// // } +// // } +// // } +// // } +// } + +impl Tree { + // FUTURE: termination_check + // FUTURE: std_lib_extern_spec_requirement (for clone) + // FUTURE: allocation_in_pure_fn + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn mirror(&self) -> Tree { + match self { + Tree::Leaf(l) => Tree::Leaf(l.clone()), + Tree::Node(left, right) => { + Tree::Node(Box::new(right.mirror()), Box::new(left.mirror())) + } + } + } + + // FUTURE: termination_check + // FUTURE: lemma_syntax + // FUTURE: calc_block + // FUTURE: allocation_in_pure_fn (box::new()) + // FUTURE: std_lib_extern_spec_requirement (for PartialEq::eq) + #[pure] + #[ensures(snap(self) === snap(&self).mirror().mirror())] + fn lemma_mirror_mirror(&self) { + use Tree::*; + match self { + Leaf(l) => {} // trivial + Node(left, right) => { + let a = Node(snap(left), snap(right)).mirror().mirror(); + let b = Node(Box::new(right.mirror()), Box::new(left.mirror())).mirror(); + let c = Node( + Box::new(left.mirror().mirror()), + Box::new(right.mirror().mirror()), + ); + let d = Node(snap(left), snap(right)); + prusti_assert!(a === b); + prusti_assert!(b === c); + left.lemma_mirror_mirror(); + right.lemma_mirror_mirror(); + prusti_assert!(c === d); + } + } + } +} diff --git a/chapter5/src/examples/fail/example_5_7_1.rs b/chapter5/src/examples/fail/example_5_7_1.rs new file mode 100644 index 0000000..f2ec315 --- /dev/null +++ b/chapter5/src/examples/fail/example_5_7_1.rs @@ -0,0 +1,46 @@ +use prusti_contracts::*; + +// 5.7.1.dfy +// datatype Tree +// function Size(t: Tree): nat +// function Mirror(t: Tree): Tree +// lemma {:induction false} MirrorSize(t: Tree) + +#[derive(Clone)] +pub enum Tree { + Leaf(T), + Node(Box>, Box>), +} + +impl Tree { + // FUTURE: termination_check + // FUTURE: std_lib_extern_spec_requirement (for clone) + // FUTURE: allocation_in_pure_fn + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn mirror(&self) -> Tree { + match self { + Tree::Leaf(l) => Tree::Leaf(l.clone()), + Tree::Node(left, right) => { + Tree::Node(Box::new(right.mirror()), Box::new(left.mirror())) + } + } + } + + // FUTURE: termination_check + #[pure] + pub fn size(&self) -> u64 { + match self { + Tree::Leaf(l) => 1, + Tree::Node(left, right) => left.size() + right.size(), + } + } + + // FUTURE: lemma_syntax + // FUTURE: termination_check + #[pure] + #[ensures(self.mirror().size() == self.size())] + fn lemma_mirror_size(&self) { + todo!(); + } +} diff --git a/chapter5/src/examples/fail/example_5_8_0.rs b/chapter5/src/examples/fail/example_5_8_0.rs new file mode 100644 index 0000000..7e06b08 --- /dev/null +++ b/chapter5/src/examples/fail/example_5_8_0.rs @@ -0,0 +1,127 @@ +use prusti_contracts::*; + +// 5.8.0.dfy +// datatype List +// datatype Op +// datatype Expr +// function method Substitute(e: Expr, n: string, c: nat): Expr +// function method SubstituteList(es: List, n: string, c: nat): List +// function method Eval(e: Expr, env: map): nat +// function method EvalList(args: List, op: Op, env: map): nat +// lemma EvalSubstitute(e: Expr, n: string, c: nat, env: map) +// lemma {:induction false} EvalSubstituteList(args: List, op: Op, n: string, c: nat, env: map) + +pub enum List { + Nil, + Cons(T, Box>), +} + +#[derive(Clone, Copy)] +pub enum Op { + Add, + Mul, +} + +pub enum Expr { + Const(u64), + Var(String), + Node(Op, Box>), +} + +// FUTURE: map_support +// FUTURE: std_lib_extern_spec_requirement +pub type Environment = std::collections::HashMap; + +impl Expr { + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + // FUTURE: allocation_in_pure_fn (Box::new()) + #[pure] + pub fn substitute(self, n: &str, c: u64) -> Expr { + match self { + Expr::Const(_) => self, + Expr::Var(s) => { + if s == n { + Expr::Const(c) + } else { + Expr::Var(s) + } + } + Expr::Node(op, args) => Expr::Node(op, Box::new(Self::substitute_list(*args, n, c))), + } + } + + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + // FUTURE: allocation_in_pure_fn (Box::new()) + #[pure] + pub fn substitute_list(es: List, n: &str, c: u64) -> List { + match es { + List::Nil => es, + List::Cons(e, tail) => List::Cons( + e.substitute(n, c), + Box::new(Self::substitute_list(*tail, n, c)), + ), + } + } + + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + // FUTURE: allocation_in_pure_fn (Box::new()) + #[pure] + pub fn eval(self, env: &Environment) -> u64 { + match self { + Expr::Const(c) => c, + Expr::Var(s) => { + let result = env.get(&s); + match result { + Some(&v) => v, // FUTURE: reference_typed_structures + None => 0, + } + // if result.is_some() { + // *result.unwrap() + // } else { + // 0 + // } + // *result.unwrap_or_else(|| &0) + // if let Some(v) = env.get(&s) { + // *v + // } else { + // 0 + // } + } + Expr::Node(op, args) => Expr::eval_list(*args, op, env), + } + } + + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn eval_list(args: List, op: Op, env: &Environment) -> u64 { + match args { + List::Nil => match op { + Op::Add => 0, + Op::Mul => 1, + }, + List::Cons(e, tail) => { + let v0 = e.eval(env); + let v1 = Self::eval_list(*tail, op, env); + match op { + Op::Add => v0 + v1, + Op::Mul => v0 * v1, + } + } + } + } +} + +// FUTURE: lemma_syntax +// FUTURE: map_support +#[pure] +// Cannot encode, because required functions cannot be made pure +// #[ensures(e.substitute(n, c).eval(env) == {env.set(n, c); e.eval()})] +pub fn lemma_eval_substitute(e: &Expr, n: &str, c: u64, env: &Environment) {} + +// FUTURE: lemma_syntax +#[pure] +pub fn lemma_eval_substitute_list() {} diff --git a/chapter5/src/examples/fail/example_5_8_1_1.rs b/chapter5/src/examples/fail/example_5_8_1_1.rs new file mode 100644 index 0000000..3a19a3e --- /dev/null +++ b/chapter5/src/examples/fail/example_5_8_1_1.rs @@ -0,0 +1,92 @@ +use prusti_contracts::*; + +// 5.8.1_1.dfy +// datatype List +// datatype Op +// datatype Expr +// function method Unit(op: Op): nat +// function method Optimize(e: Expr): Expr +// function method Shorten(op: Op, args: List): Expr +// function method OptimizeAndFilter(es: List, unit: nat): List + +pub enum List { + Nil, + Cons(T, Box>), +} + +#[derive(Clone, Copy)] +pub enum Op { + Add, + Mul, +} + +pub enum Expr { + Const(u64), + Var(String), + Node(Op, Box>), +} + +impl Op { + #[pure] + pub fn unit(self) -> u64 { + match self { + Op::Add => 0, + Op::Mul => 1, + } + } +} + +impl Expr { + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn optimize(self) -> Self { + if let Expr::Node(op, args) = self { + let args = optimize_and_filter(*args, op.unit()); + shorten(op, args) + } else { + self + } + } +} + +// FUTURE: non_copy_types_in_pure_fn +// FUTURE: box_syntax +#[pure] +pub fn shorten(op: Op, args: List) -> Expr { + use List::*; + match args { + Nil => Expr::Const(op.unit()), + Cons(e, next_box) => { + let next: &List = &next_box; + match next { + Nil => e, + Cons(..) => Expr::Node(op, Box::new(Cons(e, next_box))), + } + } + } +} + +// FUTURE: termination_check +// FUTURE: non_copy_types_in_pure_fn +// FUTURE: allocation_in_pure_fn (Box::new()) +#[pure] +pub fn optimize_and_filter(es: List, unit: u64) -> List { + use List::*; + match es { + Nil => Nil, + Cons(e, tail) => { + let e_ = e.optimize(); + let tail_ = optimize_and_filter(*tail, unit); + match e_ { + Expr::Const(u) if u == unit => tail_, + _ => Cons(e_, Box::new(tail_)), + } + // if let Expr::Const(u) = e_ && u == unit { + // tail_ + // } else { + // Cons(e_, Box::new(tail_)) + // } + } + } +} diff --git a/chapter5/src/examples/fail/example_5_8_1_2.rs b/chapter5/src/examples/fail/example_5_8_1_2.rs new file mode 100644 index 0000000..674aa62 --- /dev/null +++ b/chapter5/src/examples/fail/example_5_8_1_2.rs @@ -0,0 +1,203 @@ +use prusti_contracts::*; + +// 5.8.1_1.dfy +// datatype List +// datatype Op +// datatype Expr +// function method Substitute(e: Expr, n: string, c: nat): Expr +// function method SubstituteList(es: List, n: string, c: nat): List +// function method Eval(e: Expr, env: map): nat +// function method EvalList(args: List, op: Op, env: map): nat +// lemma EvalSubstitute(e: Expr, n: string, c: nat, env: map) +// lemma {:induction false} EvalSubstituteList(args: List, op: Op, n: string, c: nat, env: map) +// function method Unit(op: Op): nat +// function method Optimize(e: Expr): Expr +// function method Shorten(op: Op, args: List): Expr +// function method OptimizeAndFilter(es: List, unit: nat): List +// lemma OptimizeCorrect(e: Expr, env: map) +// lemma ShortenCorrect(op:Op, args: List, env: map) +// lemma OptimizeAndFilterCorrect(args: List, op: Op, env: map) + +pub enum List { + Nil, + Cons(T, Box>), +} + +impl Clone for List { + fn clone(&self) -> Self { + match self { + List::Nil => List::Nil, + List::Cons(h, tail) => List::Cons(h.clone(), tail.clone()), + } + } +} + +#[derive(Clone, Copy)] +pub enum Op { + Add, + Mul, +} + +#[derive(Clone)] +pub enum Expr { + Const(u64), + Var(String), + Node(Op, Box>), +} + +type Environment = std::collections::HashMap; + +impl Op { + #[pure] + pub fn unit(self) -> u64 { + match self { + Op::Add => 0, + Op::Mul => 1, + } + } +} + +impl Expr { + // FUTURE: termination_check + // FUTURE: allocation_in_pure_fn + // FUTURE: non_copy_types_in_pure_fn (Box::new()) + #[pure] + pub fn substitute(self, n: &str, c: u64) -> Expr { + match self { + Expr::Const(_) => self, + Expr::Var(s) => { + if s == n { + Expr::Const(c) + } else { + Expr::Var(s) + } + } + Expr::Node(op, args) => Expr::Node(op, Box::new(Self::substitute_list(*args, n, c))), + } + } + + // FUTURE: termination_check + // FUTURE: allocation_in_pure_fn (Box::new()) + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn substitute_list(es: List, n: &str, c: u64) -> List { + match es { + List::Nil => es, + List::Cons(e, tail) => List::Cons( + e.substitute(n, c), + Box::new(Self::substitute_list(*tail, n, c)), + ), + } + } + + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn eval(self, env: &Environment) -> u64 { + match self { + Expr::Const(c) => c, + Expr::Var(s) => { + let result = env.get(&s); + match result { + Some(&v) => v, // FUTURE: reference_typed_structures + None => 0, + } + // if result.is_some() { + // *result.unwrap() + // } else { + // 0 + // } + // *result.unwrap_or_else(|| &0) + // if let Some(v) = env.get(&s) { + // *v + // } else { + // 0 + // } + } + Expr::Node(op, args) => Expr::eval_list(*args, op, env), + } + } + + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn eval_list(args: List, op: Op, env: &Environment) -> u64 { + match args { + List::Nil => match op { + Op::Add => 0, + Op::Mul => 1, + }, + List::Cons(e, tail) => { + let v0 = e.eval(env); + let v1 = Self::eval_list(*tail, op, env); + match op { + Op::Add => v0 + v1, + Op::Mul => v0 * v1, + } + } + } + } + + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn optimize(self) -> Self { + if let Expr::Node(op, args) = self { + let args = Self::optimize_and_filter(&args, op.unit()); + Self::shorten(op, args) + } else { + self + } + } + + // FUTURE: termination_check + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn shorten(op: Op, args: List) -> Self { + match args { + List::Nil => Expr::Const(op.unit()), + _ => todo!(), // See example_5_8_1_2.rs + // List::Cons => + } + } + + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn optimize_and_filter(es: &List, unit: u64) -> List { + todo!() + } +} + +// FUTURE: lemma_syntax +#[pure] +// #[ensures(Expr::shorten(op, args).eval(env) +// === Expr::Node(op, args).eval(env)] +pub fn lemma_shorten_correct(op: Op, args: List, env: &mut Environment) { + todo!() +} + +// FUTURE: lemma_syntax +#[pure] +pub fn lemma_eval_substitute_list() {} + +// FUTURE: lemma_syntax +#[pure] +// Cannot encode, because other functions cannot be made pure +// #[ensures(self.optimize().eval(env) == self.eval(env))] +pub fn lemma_optimize_correct(e: &Expr, env: &Environment) { + todo!() +} + +// FUTURE: lemma_syntax +#[allow(clippy::only_used_in_recursion)] +#[pure] +#[ensures(Expr::Node(op, Box::new(Expr::optimize_and_filter(args, op.unit()))).eval(env) + === Expr::Node(op, Box::new((*args).clone())).eval(env))] +pub fn lemma_optimize_and_filter_correct(args: &List, op: Op, env: &Environment) { + match args { + List::Nil => {} + List::Cons(e, tail) => { + lemma_optimize_correct(e, env); + lemma_optimize_and_filter_correct(tail, op, env); + } + } +} diff --git a/chapter5/src/examples/pass/example_5_2_1.rs b/chapter5/src/examples/pass/example_5_2_1.rs new file mode 100644 index 0000000..937e4bc --- /dev/null +++ b/chapter5/src/examples/pass/example_5_2_1.rs @@ -0,0 +1,26 @@ +use prusti_contracts::*; + +// 5.2_1.dfy +// function method More(x: int): int +// lemma {:induction false} Increasing(x: int) + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: lemma_syntax +// FUTURE: termination_check +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing(x: i64) { + if x <= 0 { + } else { + lemma_increasing(x - 2) + } +} diff --git a/chapter5/src/examples/pass/example_5_2_2.rs b/chapter5/src/examples/pass/example_5_2_2.rs new file mode 100644 index 0000000..e26c85f --- /dev/null +++ b/chapter5/src/examples/pass/example_5_2_2.rs @@ -0,0 +1,25 @@ +use prusti_contracts::*; + +// 5.2_2.dfy +// function method More(x: int): int +// lemma {:induction false} Increasing(x: int) + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: lemma_syntax +// FUTURE: termination_check +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing(x: i64) { + if 0 < x { + lemma_increasing(x - 2) + } +} diff --git a/chapter5/src/examples/pass/example_5_3_1.rs b/chapter5/src/examples/pass/example_5_3_1.rs new file mode 100644 index 0000000..fa576dc --- /dev/null +++ b/chapter5/src/examples/pass/example_5_3_1.rs @@ -0,0 +1,31 @@ +use prusti_contracts::*; + +// 5.3.1.dfy +// function method More(x: int): int { +// lemma {:induction false} Increasing(x: int) + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: lemma_syntax +// FUTURE: termination_check +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing(x: i64) { + if x <= 0 { + prusti_assert!(more(x) == 1); + } else { + prusti_assert!(more(x) == more(x - 2) + 3); + lemma_increasing(x - 2); + prusti_assert!(x - 2 < more(x - 2)); + prusti_assert!(x + 1 < more(x - 2) + 3); + prusti_assert!(x + 1 < more(x)); + } +} diff --git a/chapter5/src/examples/pass/example_5_4_0_1.rs b/chapter5/src/examples/pass/example_5_4_0_1.rs new file mode 100644 index 0000000..732fa7f --- /dev/null +++ b/chapter5/src/examples/pass/example_5_4_0_1.rs @@ -0,0 +1,32 @@ +use prusti_contracts::*; + +// 5.4.0_1.dfy +// function method More(x: int): int { +// lemma {:induction false} Increasing(x: int) + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: lemma_syntax +// FUTURE: termination_check +// FUTURE: calc_block +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing(x: i64) { + if x <= 0 { + prusti_assert!(more(x) == 1); + } else { + prusti_assert!(more(x) == more(x - 2) + 3); + lemma_increasing(x - 2); + prusti_assert!(x - 2 < more(x - 2)); + prusti_assert!(x + 1 < more(x - 2) + 3); + prusti_assert!(x + 1 < more(x)); + } +} diff --git a/chapter5/src/examples/pass/example_5_4_0_2.rs b/chapter5/src/examples/pass/example_5_4_0_2.rs new file mode 100644 index 0000000..8d54291 --- /dev/null +++ b/chapter5/src/examples/pass/example_5_4_0_2.rs @@ -0,0 +1,32 @@ +use prusti_contracts::*; + +// 5.4.0_2.dfy +// function method More(x: int): int { +// lemma {:induction false} Increasing(x: int) + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: lemma_syntax +// FUTURE: termination_check +// FUTURE: calc_block +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing(x: i64) { + if x <= 0 { + prusti_assert!(more(x) == 1); + } else { + prusti_assert!(more(x) == more(x - 2) + 3); + lemma_increasing(x - 2); + prusti_assert!(x - 2 < more(x - 2)); + prusti_assert!(x + 1 < more(x - 2) + 3); + prusti_assert!(x + 1 < more(x)); + } +} diff --git a/chapter5/src/examples/pass/example_5_5.rs b/chapter5/src/examples/pass/example_5_5.rs new file mode 100644 index 0000000..d5e4f58 --- /dev/null +++ b/chapter5/src/examples/pass/example_5_5.rs @@ -0,0 +1,15 @@ +use prusti_contracts::*; + +// 5.5.dfy +// function Reduce(m: nat, x: int): int + +// FUTURE: termination_check +#[pure] +#[requires(m >= 0)] +pub fn reduce(m: i64, x: i64) -> i64 { + if m == 0 { + x + } else { + reduce(m / 2, x + 1) - m + } +} diff --git a/chapter5/src/examples/pass/example_5_5_1.rs b/chapter5/src/examples/pass/example_5_5_1.rs new file mode 100644 index 0000000..65ca1b2 --- /dev/null +++ b/chapter5/src/examples/pass/example_5_5_1.rs @@ -0,0 +1,35 @@ +use prusti_contracts::*; + +// 5.5.1.dfy +// function Reduce(m: nat, x: int): int +// lemma {:induction false} ReduceLowerBound(m:nat, x: int) + +// FUTURE: termination_check +#[pure] +#[requires(m >= 0)] +pub fn reduce(m: i64, x: i64) -> i64 { + if m == 0 { + x + } else { + reduce(m / 2, x + 1) - m + } +} + +// FUTURE: lemma_syntax +// FUTURE: termination_check +#[allow(clippy::only_used_in_recursion)] +#[pure] +#[requires(m >= 0)] +#[ensures(x - 2 * m <= reduce(m, x))] +pub fn lemma_reduce_lower_bound(m: i64, x: i64) { + if m == 0 { + } else { + // FUTURE: calc_block + prusti_assert!(reduce(m, x) == reduce(m / 2, x + 1) - m); + lemma_reduce_lower_bound(m / 2, x + 1); + prusti_assert!(x + 1 - 2 * (m / 2) <= reduce(m / 2, x + 1)); + prusti_assert!(reduce(m / 2, x + 1) - m >= x + 1 - 2 * (m / 2) - m); + prusti_assert!(2 * (m / 2) <= m); + prusti_assert!(x + 1 - m - m > x - 2 * m); + } +} diff --git a/chapter5/src/examples/pass/example_5_6.rs b/chapter5/src/examples/pass/example_5_6.rs new file mode 100644 index 0000000..f887f47 --- /dev/null +++ b/chapter5/src/examples/pass/example_5_6.rs @@ -0,0 +1,40 @@ +use prusti_contracts::*; + +// 5.6.dfy +// function Mult(x: nat, y: nat): nat +// lemma {: induction false} MultCommutative(x: nat, y: nat) + +// FUTURE: termination_check +#[pure] +pub fn mult(x: u64, y: u64) -> u64 { + if y == 0 { + 0 + } else { + x + mult(x, y - 1) + } +} + +// FUTURE: lemma_syntax +// FUTURE: termination_check +#[pure] +#[ensures(mult(x, y) == mult(y, x))] +pub fn lemma_mult_commutative(x: u64, y: u64) { + if x == y { + } else if x == 0 { + lemma_mult_commutative(x, y - 1); + } else if y == 0 { + lemma_mult_commutative(x - 1, y); + } else { + // FUTURE: calc_block + prusti_assert!(mult(x, y) == x + mult(x, y - 1)); + lemma_mult_commutative(x, y - 1); + prusti_assert!(x + mult(x, y - 1) == x + mult(y - 1, x)); + prusti_assert!(x + mult(y - 1, x) == x + y - 1 + mult(y - 1, x - 1)); + lemma_mult_commutative(x - 1, y - 1); + prusti_assert!(x + y - 1 + mult(y - 1, x - 1) == x + y - 1 + mult(x - 1, y - 1)); + prusti_assert!(x + y - 1 + mult(x - 1, y - 1) == y + mult(x - 1, y)); + lemma_mult_commutative(x - 1, y); + prusti_assert!(y + mult(x - 1, y) == y + mult(y, x - 1)); + prusti_assert!(y + mult(y, x - 1) == mult(y, x)); + } +} diff --git a/chapter5/src/exercises.rs b/chapter5/src/exercises.rs new file mode 100644 index 0000000..0eb38f3 --- /dev/null +++ b/chapter5/src/exercises.rs @@ -0,0 +1,20 @@ +#[cfg(feature = "pass")] +mod pass { + mod exercise_5_5; + mod exercise_5_7; +} + +#[cfg(feature = "fail")] +mod fail { + mod exercise_5_0; // FUTURE: lemma_induction_proof + mod exercise_5_3; // Verification should and does fail here + mod exercise_5_8; // FUTURE: std_lib_extern_spec_requirement + allocation_in_pure_fn + non_copy_types_in_pure_fn + mod exercise_5_10; // FUTURE: map_support + mod exercise_5_11; // FUTURE: std_lib_extern_spec_requirement, map_support + mod exercise_5_12; // FUTURE: allocation_in_pure_fn + non_copy_types_in_pure_fn +} + +// exercise_5_9: skipped, builds on (failing) example_5_8_0.rs +// exercise_5_13: not a coding task +// exercise_5_14: skipped, builds on (failing) example_5_8_1_2.rs, requires termination checks +// exercise_5_15; skipped, builds on (failing) example_5_8_1_2.rs diff --git a/chapter5/src/exercises/fail/exercise_5_0.rs b/chapter5/src/exercises/fail/exercise_5_0.rs new file mode 100644 index 0000000..ead8a43 --- /dev/null +++ b/chapter5/src/exercises/fail/exercise_5_0.rs @@ -0,0 +1,33 @@ +use prusti_contracts::*; + +// 5.0.dfy +// function method More(x: int): int +// lemma Increasing(x: int) +// method ExampleLemmaUse(a: int) + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: termination_check +// FUTURE: lemma_syntax +// FUTURE: lemma_induction_proof +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing(x: i64) {} + +pub fn example_lemma_use(a: i64) { + lemma_increasing(a); + let b = more(a); + let c = more(b); + if a < 1000 { + lemma_increasing(more(a)); + } + prusti_assert!(2 <= c - a || 200 <= a); +} diff --git a/chapter5/src/exercises/fail/exercise_5_10.rs b/chapter5/src/exercises/fail/exercise_5_10.rs new file mode 100644 index 0000000..cbcd30e --- /dev/null +++ b/chapter5/src/exercises/fail/exercise_5_10.rs @@ -0,0 +1,35 @@ +use prusti_contracts::*; + +// 5.10.dfy +// lemma EvalEnv(e: Expr, n: string, env: map) +// lemma {:induction false} EvalEnvList(args: List, op: Op, n: string, c: nat, env: map) + +// Like example_5_8_0.rs + eval_env + eval_env_list +use super::super::super::examples::{Environment, Expr, List, Op}; + +// FUTURE: termination_check +// FUTURE: lemma_syntax +#[pure] +#[requires(env.contains_key(n))] // FUTURE: std_lib_extern_spec_requirement, map_support +#[ensures(snap(e).eval(env) === snap(e).substitute(n, env[n]).eval(env))] +pub fn lemma_eval_env(e: &Expr, n: &str, env: &Environment) { + if let Expr::Node(op, args) = e { + lemma_eval_env_list(args, *op, n, env[n], env); // FUTURE: map_support + } +} + +// FUTURE: termination_check +// FUTURE: lemma_syntax +#[allow(clippy::only_used_in_recursion)] +#[pure] +#[requires(env.contains_key(n))] // FUTURE: std_lib_extern_spec_requirement, map_support +#[ensures(Expr::eval_list(snap(args), op, env) === Expr::eval_list(Expr::substitute_list(snap(args), n, env[n]), op, env))] +pub fn lemma_eval_env_list(args: &List, op: Op, n: &str, c: u64, env: &Environment) { + match args { + List::Nil => {} + List::Cons(e, tail) => { + lemma_eval_env(e, n, env); + lemma_eval_env_list(tail, op, n, env[n], env); // FUTURE: map_support + } + } +} diff --git a/chapter5/src/exercises/fail/exercise_5_11.rs b/chapter5/src/exercises/fail/exercise_5_11.rs new file mode 100644 index 0000000..196418d --- /dev/null +++ b/chapter5/src/exercises/fail/exercise_5_11.rs @@ -0,0 +1,33 @@ +use prusti_contracts::*; + +// 5.11.dfy +// lemma EvalEnvDefault(e: Expr, n: string, env: map) +// lemma EvalEnvDefaultList(args: List, op: Op, n: string, c: nat, env: map) + +use super::super::super::examples::{Environment, Expr, List, Op}; +use super::exercise_5_10::*; + +// FUTURE: termination_check +// FUTURE: lemma_syntax +#[pure] +#[requires(env.contains_key(n))] // FUTURE: std_lib_extern_spec_requirement, map_support +#[ensures(snap(e).eval(env) === snap(e).substitute(n, 0).eval(env))] +pub fn lemma_eval_env_default(e: &Expr, n: &str, env: &Environment) { + if let Expr::Node(op, args) = e { + lemma_eval_env_default_list(args, *op, n, env); + } +} + +// FUTURE: termination_check +// FUTURE: lemma_syntax +#[allow(clippy::only_used_in_recursion)] +#[pure] +#[requires(env.contains_key(n))] // FUTURE: std_lib_extern_spec_requirement, map_support +#[ensures(Expr::eval_list(snap(args), op, env) + === Expr::eval_list(Expr::substitute_list(snap(args), n, 0), op, env))] +pub fn lemma_eval_env_default_list(args: &List, op: Op, n: &str, env: &Environment) { + if let List::Cons(e, tail) = args { + lemma_eval_env_default(e, n, env); + lemma_eval_env_default_list(tail, op, n, env); + } +} diff --git a/chapter5/src/exercises/fail/exercise_5_12.rs b/chapter5/src/exercises/fail/exercise_5_12.rs new file mode 100644 index 0000000..e3f2d08 --- /dev/null +++ b/chapter5/src/exercises/fail/exercise_5_12.rs @@ -0,0 +1,51 @@ +use prusti_contracts::*; + +// 5.12.dfy +// lemma Sublist(args: List, n: string, c: nat) +// lemma SubstituteIdempotent(e: Expr, n: string, c: nat) + +use super::super::super::examples::{Expr, List}; +use super::exercise_5_11::*; + +// FUTURE: termination_check +// FUTURE: lemma_syntax +// FUTURE: non_copy_types_in_pure_fn +#[pure] +#[ensures(Expr::substitute_list(Expr::substitute_list(snap(args), n, c), n, c) + === Expr::substitute_list(snap(args), n, c))] +pub fn lemma_sublist(args: &List, n: &str, c: u64) { + if let List::Cons(e, tail) = args { + lemma_substitute_idempotent(e, n, c); + lemma_sublist(tail, n, c); + } +} + +// FUTURE: termination_check +// FUTURE: lemma_syntax +#[pure] +#[ensures(snap(e).substitute(n, c).substitute(n, c) + === snap(e).substitute(n, c))] +pub fn lemma_substitute_idempotent(e: &Expr, n: &str, c: u64) { + if let Expr::Node(op, args) = e { + // FUTURE: calc_block + // FUTURE: allocation_in_pure_fn + // FUTURE: non_copy_types_in_pure_fn + let b0 = snap(e).substitute(n, c).substitute(n, c); // Note: snap should not be called in normal code + let b1 = + Expr::Node(*op, Box::new(Expr::substitute_list(snap(args), n, c))).substitute(n, c); + let b2 = Expr::Node( + *op, + Box::new(Expr::substitute_list( + Expr::substitute_list(snap(args), n, c), + n, + c, + )), + ); + let b3 = snap(e).substitute(n, c); // Note: snap should not be called in normal code + + prusti_assert!(b0 === b1); + prusti_assert!(b1 === b2); + lemma_sublist(args, n, c); + prusti_assert!(b2 === b3); + } +} diff --git a/chapter5/src/exercises/fail/exercise_5_3.rs b/chapter5/src/exercises/fail/exercise_5_3.rs new file mode 100644 index 0000000..c099aed --- /dev/null +++ b/chapter5/src/exercises/fail/exercise_5_3.rs @@ -0,0 +1,32 @@ +use prusti_contracts::*; + +// 5.3.dfy +// function method More(x: int): int +// lemma {:induction false} Increasing(x: int) + +// NOTE: Verification should fail + +// FUTURE: termination_check +#[pure] +pub fn more(x: i64) -> i64 { + if x <= 0 { + 1 + } else { + more(x - 2) + 3 + } +} + +// FUTURE: lemma_syntax +// FUTURE: numberOfErrorsToReport +#[pure] +#[ensures(x < more(x))] +pub fn lemma_increasing(x: i64) { + if x <= 0 { + assert!(more(x) == 2); // Should and does fail + } else { + assert!(more(x) == more(x - 2) + 3); + assert!(x - 2 < more(x - 2)); // Should fail, but Prusti only reports 1 error per function + assert!(x + 1 < more(x - 2) + 3); + assert!(x + 1 < more(x)); + } +} diff --git a/chapter5/src/exercises/fail/exercise_5_8.rs b/chapter5/src/exercises/fail/exercise_5_8.rs new file mode 100644 index 0000000..cfbd623 --- /dev/null +++ b/chapter5/src/exercises/fail/exercise_5_8.rs @@ -0,0 +1,53 @@ +use prusti_contracts::*; + +// 5.8.dfy +// datatype Tree = Leaf(data: T) | Node(left: Tree, right: Tree) +// function Size(t: Tree): nat +// function Mirror(t: Tree): Tree +// lemma {:induction false} MirrorSize(t: Tree) + +#[derive(Clone)] +pub enum Tree { + Leaf(T), + Node(Box>, Box>), +} + +impl Tree { + // FUTURE: termination_check + // FUTURE: std_lib_extern_spec_requirement (for clone) + // FUTURE: allocation_in_pure_fn + // FUTURE: non_copy_types_in_pure_fn + #[pure] + pub fn mirror(&self) -> Tree { + match self { + Tree::Leaf(l) => Tree::Leaf(l.clone()), + Tree::Node(left, right) => { + Tree::Node(Box::new(right.mirror()), Box::new(left.mirror())) + } + } + } + + // FUTURE: termination_check + #[pure] + pub fn size(&self) -> u64 { + match self { + Tree::Leaf(l) => 1, + Tree::Node(left, right) => left.size() + right.size(), + } + } + + // FUTURE: lemma_syntax + // FUTURE: non_copy_types_in_pure_fn + // FUTURE: std_lib_extern_spec_requirement (for box deref) + #[pure] + #[ensures(self.size() == self.mirror().size())] + pub fn lemma_mirror_size(&self) { + match self { + Tree::Leaf(_) => {} // trivial + Tree::Node(left, right) => { + left.lemma_mirror_size(); + right.lemma_mirror_size(); + } + } + } +} diff --git a/chapter5/src/exercises/pass/exercise_5_5.rs b/chapter5/src/exercises/pass/exercise_5_5.rs new file mode 100644 index 0000000..f8259af --- /dev/null +++ b/chapter5/src/exercises/pass/exercise_5_5.rs @@ -0,0 +1,94 @@ +use prusti_contracts::*; + +// 5.5.dfy +// function Reduce(m: nat, x: int): int +// lemma {:induction false} ReduceUpperBound(m:nat, x: int) +// lemma {:induction false} ReduceUpperBound1(m:nat, x: int) +// lemma {:induction false} ReduceUpperBound2(m:nat, x: int) +// lemma {:induction false} ReduceUpperBound3(m:nat, x: int) + +// FUTURE: termination_check +#[pure] +#[requires(m >= 0)] +pub fn reduce(m: i64, x: i64) -> i64 { + if m == 0 { + x + } else { + reduce(m / 2, x + 1) - m + } +} + +// FUTURE: termination_check +// FUTURE: lemma_syntax +// FUTURE: calc_block +// FUTURE: prusti_assert_eq +#[allow(clippy::only_used_in_recursion)] +#[pure] +#[requires(m >= 0)] +#[ensures(reduce(m, x) <= x)] +pub fn lemma_reduce_upper_bound(m: i64, x: i64) { + if m == 0 { + } else { + prusti_assert!(reduce(m, x) == reduce(m / 2, x + 1) - m); + lemma_reduce_upper_bound(m / 2, x + 1); + prusti_assert!(reduce(m / 2, x + 1) <= x + 1); + prusti_assert!(reduce(m / 2, x + 1) - m <= x + 1 - m); + prusti_assert!(0 < m); + prusti_assert!(x + 1 - m <= x); + } +} + +// FUTURE: termination_check +// FUTURE: lemma_syntax +// FUTURE: calc_block +// FUTURE: prusti_assert_eq +#[allow(clippy::only_used_in_recursion)] +#[pure] +#[requires(m >= 0)] +#[ensures(reduce(m, x) <= x)] +pub fn lemma_reduce_upper_bound_1(m: i64, x: i64) { + if m == 0 { + } else { + prusti_assert!(reduce(m, x) == reduce(m / 2, x + 1) - m); + lemma_reduce_upper_bound_1(m / 2, x + 1); + prusti_assert!(reduce(m / 2, x + 1) <= x + 1); + prusti_assert!(x + 1 - m <= x); + } +} + +// FUTURE: termination_check +// FUTURE: lemma_syntax +// FUTURE: calc_block +// FUTURE: prusti_assert_eq +#[allow(clippy::only_used_in_recursion)] +#[pure] +#[requires(m >= 0)] +#[ensures(reduce(m, x) <= x)] +pub fn lemma_reduce_upper_bound_2(m: i64, x: i64) { + if m == 0 { + } else { + prusti_assert!(x >= x + 1 - m); + lemma_reduce_upper_bound_2(m / 2, x + 1); + prusti_assert!(x + 1 - m >= reduce(m / 2, x + 1) - m); + prusti_assert!(reduce(m / 2, x + 1) - m == reduce(m, x)); + } +} + +// FUTURE: termination_check +// FUTURE: lemma_syntax +// FUTURE: calc_block +// FUTURE: prusti_assert_eq +#[allow(clippy::only_used_in_recursion)] +#[pure] +#[requires(m >= 0)] +#[ensures(reduce(m, x) <= x)] +pub fn lemma_reduce_upper_bound_3(m: i64, x: i64) { + if m != 0 { + prusti_assert!(reduce(m, x) == reduce(m / 2, x + 1) - m); + lemma_reduce_upper_bound_3(m / 2, x + 1); + prusti_assert!(reduce(m / 2, x + 1) <= x + 1); + prusti_assert!(reduce(m / 2, x + 1) - m <= x + 1 - m); + prusti_assert!(0 < m); + prusti_assert!(x + 1 - m <= x); + } +} diff --git a/chapter5/src/exercises/pass/exercise_5_7.rs b/chapter5/src/exercises/pass/exercise_5_7.rs new file mode 100644 index 0000000..082c95f --- /dev/null +++ b/chapter5/src/exercises/pass/exercise_5_7.rs @@ -0,0 +1,42 @@ +use prusti_contracts::*; + +// 5.7.dfy +// function Mult(x: nat, y: nat): nat +// lemma {: induction false} MultCommutative(x: nat, y: nat) + +// FUTURE: termination_check +#[pure] +pub fn mult(x: u64, y: u64) -> u64 { + if y == 0 { + 0 + } else { + x + mult(x, y - 1) + } +} + +// FUTURE: lemma_syntax +// FUTURE: calc_block +#[pure] +#[ensures(mult(x, y) == mult(y, x))] +// #[decreases(x + y)] // FUTURE: termination_check +pub fn lemma_mult_commutative(x: u64, y: u64) { + if x == y { + } else if x == 0 { + lemma_mult_commutative(x, y - 1); + } else if y == 0 { + lemma_mult_commutative(x - 1, y); + } else if y < x { + lemma_mult_commutative(y, x); + } else { + prusti_assert!(mult(x, y) == x + mult(x, y - 1)); + lemma_mult_commutative(x, y - 1); + prusti_assert!(x + mult(x, y - 1) == x + mult(y - 1, x)); + prusti_assert!(x + mult(y - 1, x) == x + y - 1 + mult(y - 1, x - 1)); + lemma_mult_commutative(x - 1, y - 1); + prusti_assert!(x + y - 1 + mult(y - 1, x - 1) == x + y - 1 + mult(x - 1, y - 1)); + prusti_assert!(x + y - 1 + mult(x - 1, y - 1) == y + mult(x - 1, y)); + lemma_mult_commutative(x - 1, y); + prusti_assert!(y + mult(x - 1, y) == y + mult(y, x - 1)); + prusti_assert!(y + mult(y, x - 1) == mult(y, x)); + } +} diff --git a/chapter5/src/lib.rs b/chapter5/src/lib.rs new file mode 100644 index 0000000..4427518 --- /dev/null +++ b/chapter5/src/lib.rs @@ -0,0 +1,9 @@ +// #![warn(clippy::pedantic)] + +#[allow(clippy::wildcard_imports)] +#[allow(unused)] +pub mod examples; + +#[allow(clippy::wildcard_imports)] +#[allow(unused)] +pub mod exercises;