Make it more pleasant to write a proof-by-computation over a range of…

… values (#1338)

source/rust_verify_test/tests/assert_by_compute.rs

@@ -583,3 +583,86 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "failed to simplify down to true")
 }
+
+test_verify_one_file! {
+    #[test] range_all_simple verus_code! {
+        use vstd::prelude::*;
+        use core::ops::Range;
+        use vstd::compute::*;
+
+        proof fn test() {
+            assert({
+                let r = 2..4int;
+                let prop = |v: int| (v as u64) & 0xf000 == 0;
+                r.all_spec(prop)
+            }) by (compute_only);
+            let r = 2..4int;
+            let prop = |v: int| (v as u64) & 0xf000 == 0;
+            assert(prop(3));
+            assert(3u64 & 0xf000 == 0);
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] range_all_complex verus_code! {
+        use vstd::prelude::*;
+        use core::ops::Range;
+        use vstd::compute::*;
+        use vstd::std_specs::bits::u64_leading_zeros;
+        global size_of usize == 8;
+
+        pub const BIN_HUGE: u64 = 73;
+
+        pub open spec fn valid_bin_idx(bin_idx: int) -> bool {
+            1 <= bin_idx <= BIN_HUGE
+        }
+
+        pub open spec fn pow2(i: int) -> nat
+            decreases i
+        {
+            if i <= 0 {
+                1
+            } else {
+                pow2(i - 1) * 2
+            }
+        }
+
+        pub open spec fn smallest_bin_fitting_size(size: int) -> int {
+            let bytes_per_word = (usize::BITS / 8) as int;
+            let wsize = (size + bytes_per_word - 1) / bytes_per_word;
+            if wsize <= 1 {
+                1
+            } else if wsize <= 8 {
+                wsize
+            } else if wsize > 524288 {
+                BIN_HUGE as int
+            } else {
+                let w = (wsize - 1) as u64;
+                //let lz = w.leading_zeros();
+                let lz = u64_leading_zeros(w);
+                let b = (usize::BITS - 1 - lz) as u8;
+                let shifted = (w >> (b - 2) as u64) as u8;
+                let bin_idx = ((b * 4) + (shifted & 0x03)) - 3;
+                bin_idx
+            }
+        }
+
+        spec fn property_bounds_for_smallest_bitting_size(size:int) -> bool
+        {
+            valid_bin_idx(smallest_bin_fitting_size(size))
+        }
+
+        pub proof fn bounds_for_smallest_bin_fitting_size_alt(size: int)
+            requires 0 <= size <= 10,
+            ensures
+                valid_bin_idx(smallest_bin_fitting_size(size)),
+        {
+            assert({let r = 0..11int;
+                    r.all_spec(|v| property_bounds_for_smallest_bitting_size(v))
+                    }) by (compute);
+            let prop = |v| property_bounds_for_smallest_bitting_size(v);
+            assert(prop(size));
+        }
+    } => Ok(())
+}

source/vir/src/poly.rs

@@ -525,7 +525,7 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp {
             let e1 = visit_exp(ctx, state, e1);
             match op {
                 UnaryOpr::Box(_) | UnaryOpr::Unbox(_) => {
-                    panic!("internal error: already has Box/Unbox")
+                    panic!("internal error: {:?} already has Box/Unbox", e1)
                 }
                 UnaryOpr::HasType(t) => {
                     // REVIEW: not clear that typ_to_poly is appropriate here for abstract datatypes

source/vstd/compute.rs

@@ -0,0 +1,38 @@
+use super::prelude::*;
+use core::ops::Range;
+
+verus! {
+
+/// Simplify proofs-by-computation for ranges of values
+pub trait RangeAll where Self: Sized {
+    spec fn all_spec(self, p: spec_fn(int) -> bool) -> bool;
+}
+
+pub open spec fn range_all_spec_rec(r: Range<int>, p: spec_fn(int) -> bool) -> bool
+    decreases r.end - r.start,
+{
+    if r.start >= r.end {
+        true
+    } else {
+        p(r.start) && range_all_spec_rec(r.start + 1..r.end, p)
+    }
+}
+
+impl RangeAll for Range<int> {
+    open spec fn all_spec(self, p: spec_fn(int) -> bool) -> bool {
+        range_all_spec_rec(self, p)
+    }
+}
+
+pub broadcast proof fn all_spec_implies(r: Range<int>, p: spec_fn(int) -> bool)
+    ensures
+        #[trigger] r.all_spec(p) ==> (forall|i| r.start <= i < r.end ==> #[trigger] p(i)),
+    decreases r.end - r.start,
+{
+    if r.start >= r.end {
+    } else {
+        all_spec_implies(r.start + 1..r.end, p);
+    }
+}
+
+} // verus!

source/vstd/vstd.rs

@@ -27,6 +27,7 @@ pub mod bits;
 pub mod bytes;
 pub mod calc_macro;
 pub mod cell;
+pub mod compute;
 pub mod function;
 #[cfg(all(feature = "alloc", feature = "std"))]
 pub mod hash_map;
@@ -96,6 +97,7 @@ pub broadcast group group_vstd_default {
     string::group_string_axioms,
     std_specs::range::group_range_axioms,
     raw_ptr::group_raw_ptr_axioms,
+    compute::all_spec_implies,
 }
 
 #[cfg(not(feature = "alloc"))]
@@ -114,6 +116,7 @@ pub broadcast group group_vstd_default {
     string::group_string_axioms,
     std_specs::range::group_range_axioms,
     raw_ptr::group_raw_ptr_axioms,
+    compute::all_spec_implies,
 }
 
 } // verus!