Support for inductively verifying contracts of recursive functions (#…

…2809)

This adds support for verifying the contracts of recursive functions
inductively.

The idea is quite simple. We use a global variable to track whether
we're reentering a function and depending on that value we either
continue with checking the contract or assume the hypothesis by using
its replacement.

The precise mechanism that I implemented is explained in the
documentation
[here](https://github.com/JustusAdam/kani/blob/a31176c79098205ca0b2c2b199cdf06653754551/library/kani_macros/src/sysroot/contracts.rs#L126)

Resolves #2724 

**Open Question:** to facilitate induction the return type of the
function must implement `kani::Arbitrary`. Since we can't discriminate
between recursive and non-recursive functions in the proc-macro this
means that this applies to all functions with contracts, not just
recursive ones. This may be an unacceptable restriction. We could
consider making inductive verification explicit with an annotation like
`#[kani::inductive]` or conversely make inductive the default and let
users opt-out with `#[kani::no_inductive]`. This is now tracked in #2823

I had to remove the names of the functions in which the messages occur
in the test cases, since they are now generated, hard to read names

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

library/kani/src/contracts.rs

@@ -134,8 +134,8 @@
 //! one specification attribute is considered to "have a contract" and any
 //! absent specification type defaults to its most general interpretation
 //! (`true`). All functions with not a single specification attribute are
-//! considered "not to have a contract" and are ineligible for use as the
-//! target of a [`proof_for_contract`][macro@proof_for_contract] of
+//! considered "not to have a contract" and are ineligible for use as the target
+//! of a [`proof_for_contract`][macro@proof_for_contract] of
 //! [`stub_verified`][macro@stub_verified] attribute.
 //!
 //! ## Contract Use Attributes Overview
@@ -170,4 +170,23 @@
 //!
 //! Unlike `proof_for_contract` multiple `stub_verified` attributes are allowed
 //! on the same proof harness though they must target different functions.
+//!
+//! ## Inductive Verification
+//!
+//! Function contracts by default use inductive verification to efficiently
+//! verify recursive functions. In inductive verification a recursive function
+//! is executed once and every recursive call instead uses the contract
+//! replacement. In this way many recursive calls can be checked with a
+//! single verification pass.
+//!
+//! The downside of inductive verification is that the return value of a
+//! contracted function must implement `kani::Arbitrary`. Due to restrictions to
+//! code generation in proc macros, the contract macros cannot determine reliably
+//! in all cases whether a given function with a contract is recursive. As a
+//! result it conservatively sets up inductive verification for every function
+//! and requires the `kani::Arbitrary` constraint for contract checks.
+//!
+//! If you feel strongly about this issue you can join the discussion on issue
+//! [#2823](https://github.com/model-checking/kani/issues/2823) to enable
+//! opt-out of inductive verification.
 pub use super::{ensures, proof_for_contract, requires, stub_verified};

scripts/kani-regression.sh

@@ -42,6 +42,9 @@ cargo test -p kani-compiler
 cargo test -p kani-driver
 cargo test -p kani_metadata
 cargo test -p kani --lib # skip doc tests.
+# Test the actual macros, skipping doc tests and enabling extra traits for "syn"
+# so we can debug print AST
+RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib
 
 # Declare testing suite information (suite and mode)
 TESTS=(

tests/expected/function-contract/arbitrary_ensures_fail.expected

@@ -1,4 +1,4 @@
-max.assertion\
+assertion\
 - Status: FAILURE\
 - Description: "result == x"\
 in function max 

tests/expected/function-contract/arbitrary_ensures_pass.expected

@@ -1,4 +1,4 @@
-max.assertion\
+assertion\
 - Status: SUCCESS\
 - Description: "result == x || result == y"\
 in function max

tests/expected/function-contract/arbitrary_requires_pass.expected

@@ -1,4 +1,4 @@
-div.arithmetic_overflow\
+arithmetic_overflow\
 - Status: SUCCESS\
 - Description: "attempt to divide by zero"\
 in function div

tests/expected/function-contract/fail_on_two.expected

@@ -0,0 +1,12 @@
+assertion\
+- Status: FAILURE\
+- Description: "internal error: entered unreachable code: fail on two"
+
+Failed Checks: internal error: entered unreachable code: fail on two
+
+
+assertion\
+- Status: FAILURE\
+- Description: "result < 3"
+
+Failed Checks: result < 3

tests/expected/function-contract/fail_on_two.rs

@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! The test cases try to ensure applying the hypothesis is only done in
+//! inductive verification of a function call. E.g. on every second encounter of
+//! the called function in its own call stack rather than globally in the
+//! program.
+//!
+//! In each case we have a recursive function that is called and we expect that
+//! the recursive call within the first call has the hypothesis applied. (That's
+//! not actually tested here but separately.)
+//!
+//! Then we call the function again and we've set up the cases such that *if*
+//! the actual body is used then that call with fail (once because of panic,
+//! once because the postcondition is violated). If instead the hypothesis (e.g.
+//! contract replacement) is used we'd expect the verification to succeed.
+
+#[kani::ensures(result < 3)]
+fn fail_on_two(i: i32) -> i32 {
+ match i {
+ 0 => fail_on_two(i + 1),
+ 1 => 2,
+ _ => unreachable!("fail on two"),
+ }
+}
+
+#[kani::proof_for_contract(fail_on_two)]
+fn harness() {
+ let first = fail_on_two(0);
+ let _ = fail_on_two(first);
+}
+
+#[kani::ensures(result < 3)]
+fn fail_on_two_in_postcondition(i: i32) -> i32 {
+ let j = i + 1;
+ if i < 2 { fail_on_two_in_postcondition(j) } else { j }
+}
+
+#[kani::proof_for_contract(fail_on_two_in_postcondition)]
+fn harness2() {
+ let first = fail_on_two_in_postcondition(1);
+ let _ = fail_on_two_in_postcondition(first);
+}

tests/expected/function-contract/gcd_failure_code.expected

@@ -1,4 +1,4 @@
-gcd.assertion\
+assertion\
 - Status: FAILURE\
 - Description: "result != 0 && x % result == 0 && y % result == 0"\
 in function gcd

tests/expected/function-contract/gcd_failure_contract.expected

@@ -1,4 +1,4 @@
-gcd.assertion\
+assertion\
 - Status: FAILURE\
 - Description: "result != 0 && x % result == 1 && y % result == 0"\
 in function gcd\

tests/expected/function-contract/gcd_rec_code_fail.expected

@@ -0,0 +1,3 @@
+Failed Checks: result != 0 && x % result == 0 && y % result == 0
+
+VERIFICATION:- FAILED

tests/expected/function-contract/gcd_rec_code_fail.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+type T = u8;
+
+/// Euclid's algorithm for calculating the GCD of two numbers
+#[kani::requires(x != 0 && y != 0)]
+#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+fn gcd(x: T, y: T) -> T {
+ let mut max = x;
+ let mut min = y;
+ if min > max {
+ let val = max;
+ max = min;
+ min = val;
+ }
+ let res = max % min;
+ if res == 0 { min } else { gcd(min, res + 1) }
+}
+
+#[kani::proof_for_contract(gcd)]
+fn simple_harness() {
+ let _ = gcd(kani::any(), kani::any());
+}

tests/expected/function-contract/gcd_rec_comparison_pass.expected

@@ -0,0 +1,9 @@
+assertion\
+- Status: SUCCESS\
+- Description: "x != 0 && y != 0"
+
+assertion\
+- Status: SUCCESS\
+- Description: "result != 0 && x % result == 0 && y % result == 0"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/gcd_rec_comparison_pass.rs

@@ -0,0 +1,68 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+type T = u8;
+
+/// Euclid's algorithm for calculating the GCD of two numbers
+#[kani::requires(x != 0 && y != 0)]
+#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+fn gcd(x: T, y: T) -> T {
+ let mut max = x;
+ let mut min = y;
+ if min > max {
+ let val = max;
+ max = min;
+ min = val;
+ }
+
+ let res = max % min;
+ if res == 0 { min } else { gcd(min, res) }
+}
+
+struct Frac {
+ pub num: T,
+ pub den: T,
+}
+
+impl Frac {
+ // constructor
+ pub fn new(num: T, den: T) -> Self {
+ Frac { num, den }
+ }
+
+ /// Method to simplify fraction
+ /// For example, `Frac { num: 10, den: 15 }` gets simplified to
+ /// `Frac { num: 2, num: 3 }`
+ pub fn simplify(&self) -> Frac {
+ let gcd = gcd(self.num, self.den);
+ Frac::new(self.num / gcd, self.den / gcd)
+ }
+
+ pub fn check_equals(&self, f2: Frac) {
+ assert_eq!(self.num % f2.num, 0);
+ assert_eq!(self.den % f2.den, 0);
+ let gcd1 = self.num / f2.num;
+ let gcd2 = self.den / f2.den;
+ assert_eq!(gcd1, gcd2);
+ }
+}
+
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(12)]
+fn harness_as_check() {
+ gcd_harness()
+}
+
+fn gcd_harness() {
+ // Needed to avoid having `free` be removed as unused function. This is
+ // because DFCC contract enforcement assumes that a definition for `free`
+ // exists.
+ let _ = Box::new(9_usize);
+ let num: T = kani::any();
+ let den: T = kani::any();
+ kani::assume(num != 0);
+ kani::assume(den != 0);
+ let frac = Frac::new(num, den);
+ let simplified_frac = frac.simplify();
+ frac.check_equals(simplified_frac);
+}

tests/expected/function-contract/gcd_rec_contract_fail.expected

@@ -0,0 +1,3 @@
+Failed Checks: result != 0 && x % result == 1 && y % result == 0
+
+VERIFICATION:- FAILED

tests/expected/function-contract/gcd_rec_contract_fail.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+type T = u8;
+
+/// Euclid's algorithm for calculating the GCD of two numbers
+#[kani::requires(x != 0 && y != 0)]
+// Changed `0` to `1` in `x % result == 0` to mess with this contract
+#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)]
+fn gcd(x: T, y: T) -> T {
+ let mut max = x;
+ let mut min = y;
+ if min > max {
+ let val = max;
+ max = min;
+ min = val;
+ }
+
+ let res = max % min;
+ if res == 0 { min } else { gcd(min, res) }
+}
+#[kani::proof_for_contract(gcd)]
+fn simple_harness() {
+ let _ = gcd(kani::any(), kani::any());
+}

tests/expected/function-contract/gcd_rec_replacement_pass.expected

@@ -0,0 +1,17 @@
+Frac::check_equals.assertion\
+- Status: SUCCESS\
+- Description: "assertion failed: self.num % f2.num == 0"
+
+Frac::check_equals.assertion\
+- Status: SUCCESS\
+- Description: "assertion failed: self.den % f2.den == 0"
+
+Frac::check_equals.assertion\
+- Status: SUCCESS\
+- Description: "assertion failed: gcd1 == gcd2"
+
+gcd.assertion\
+- Status: SUCCESS\
+- Description: "x != 0 && y != 0"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/gcd_rec_replacement_pass.rs

@@ -0,0 +1,68 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+type T = u8;
+
+/// Euclid's algorithm for calculating the GCD of two numbers
+#[kani::requires(x != 0 && y != 0)]
+#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+fn gcd(x: T, y: T) -> T {
+ let mut max = x;
+ let mut min = y;
+ if min > max {
+ let val = max;
+ max = min;
+ min = val;
+ }
+
+ let res = max % min;
+ if res == 0 { min } else { gcd(min, res) }
+}
+
+struct Frac {
+ pub num: T,
+ pub den: T,
+}
+
+impl Frac {
+ // constructor
+ pub fn new(num: T, den: T) -> Self {
+ Frac { num, den }
+ }
+
+ /// Method to simplify fraction
+ /// For example, `Frac { num: 10, den: 15 }` gets simplified to
+ /// `Frac { num: 2, num: 3 }`
+ pub fn simplify(&self) -> Frac {
+ let gcd = gcd(self.num, self.den);
+ Frac::new(self.num / gcd, self.den / gcd)
+ }
+
+ pub fn check_equals(&self, f2: Frac) {
+ assert_eq!(self.num % f2.num, 0);
+ assert_eq!(self.den % f2.den, 0);
+ let gcd1 = self.num / f2.num;
+ let gcd2 = self.den / f2.den;
+ assert_eq!(gcd1, gcd2);
+ }
+}
+
+#[kani::proof]
+#[kani::stub_verified(gcd)]
+fn gcd_as_replace() {
+ gcd_harness()
+}
+
+fn gcd_harness() {
+ // Needed to avoid having `free` be removed as unused function. This is
+ // because DFCC contract enforcement assumes that a definition for `free`
+ // exists.
+ let _ = Box::new(9_usize);
+ let num: T = kani::any();
+ let den: T = kani::any();
+ kani::assume(num != 0);
+ kani::assume(den != 0);
+ let frac = Frac::new(num, den);
+ let simplified_frac = frac.simplify();
+ frac.check_equals(simplified_frac);
+}

tests/expected/function-contract/gcd_rec_simple_pass.expected

@@ -0,0 +1,9 @@
+assertion\
+- Status: SUCCESS\
+- Description: "x != 0 && y != 0"
+
+assertion\
+- Status: SUCCESS\
+- Description: "result != 0 && x % result == 0 && y % result == 0"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/gcd_rec_simple_pass.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+type T = u8;
+
+/// Euclid's algorithm for calculating the GCD of two numbers
+#[kani::requires(x != 0 && y != 0)]
+#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+fn gcd(x: T, y: T) -> T {
+ let mut max = x;
+ let mut min = y;
+ if min > max {
+ let val = max;
+ max = min;
+ min = val;
+ }
+
+ let res = max % min;
+ if res == 0 { min } else { gcd(min, res) }
+}
+
+#[kani::proof_for_contract(gcd)]
+fn simple_harness() {
+ let _ = gcd(kani::any(), kani::any());
+}

tests/expected/function-contract/gcd_success.expected

@@ -1,4 +1,4 @@
-gcd.assertion\
+assertion\
 - Status: SUCCESS\
 - Description: "result != 0 && x % result == 0 && y % result == 0"\
 in function gcd