thanhnguyen-aws

Add loop-contracts support for `for` loop

1

This PR adds loop-contracts support for `for` loop for 4 types: array, slice, Iter, Vec, Range, StepBy, Map, Chain, Zip, Enumerate. Main ideas: `for` loop implementation: A `for` loop of...

Function contract doesn't propagate `const` function bodies correctly

5

I tried this code: ```rust #[ensures(|result| result.as_usize().is_power_of_two())] pub const fn Align_of() -> Self { // This can't actually panic since type alignment is always a power of two. const {...

I tried this code: ```rust struct Foo { vec: Vec } #[kani::requires (e Instead, this happened: 1. proof_foo_push_contract takes a lot of time and returns "Failed Checks: Check that ptr...

Recursion unwinding does not terminate

5

I ran a small experiment to check the equivalence of the two versions of the greatest-common-divisor function, one is written with a loop and one in recursion. I tried this...

Quantifier panic when array size is greater than 64

2

I tried this code: ```rust const fn memchr_naive(x: u8, text: &[u8]) -> Option { let mut i = 0; #[kani::loop_invariant( i Instead, this happened: thread '

I tried this code: ```rust #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] fn simple_while_loops(x: &mut u8, y: &mut u8) { let mut closure_with_loop = || { #[kani::loop_invariant(*x >= 2)] #[kani::loop_modifies(x as *const _, y as...

Quantifier failure for arbitrary range

1

I tried this code: ```rust #[kani::proof] #[kani::solver(cvc5)] fn test_quantifier1() { let a: [u8; 32] = kani::any(); let slice = kani::slice::any_slice_of_array(&a); let len = slice.len(); kani::assume(kani::forall!(|i in (0,len)| unsafe {*slice.as_ptr().wrapping_add(i)} !=...

Quantifier failure in loop invariant

3

I tried this code: ```rust #[kani::proof] fn main() { let a: [usize; 60] = kani::any(); kani::assume(kani::forall!(|i in (0,60)| a[i] Instead, this happened: ``` warning: ignoring forall * type: bool 0:...