Merge pull request #10 from triblespace/codex/use-kani-config-limits-from-tribles-rust

Add default Kani unwinding limits

Author: somethingelseentirely

CHANGELOG.md

@@ -0,0 +1,5 @@
+# Changelog
+
+## Unreleased
+- limit Kani loop unwind by default and set per-harness bounds
+- increase unwind for prefix/suffix overflow proofs

Cargo.toml

@@ -26,3 +26,9 @@ pyo3 = ["dep:pyo3"]
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+
+[package.metadata.kani.flags]
+default-unwind = "1"
+
+[workspace.metadata.kani.flags]
+default-unwind = "1"

src/bytes.rs

@@ -360,6 +360,7 @@ mod verification {
     use kani::BoundedArbitrary;
 
     #[kani::proof]
+    #[kani::unwind(16)]
     pub fn check_take_prefix_ok() {
         let data: Vec<u8> = Vec::bounded_any::<16>();
         kani::assume(data.len() >= 5);
@@ -371,6 +372,7 @@ mod verification {
     }
 
     #[kani::proof]
+    #[kani::unwind(32)]
     pub fn check_take_prefix_too_large() {
         let data: Vec<u8> = Vec::bounded_any::<16>();
         let mut bytes = Bytes::from_source(data.clone());
@@ -381,6 +383,7 @@ mod verification {
     }
 
     #[kani::proof]
+    #[kani::unwind(16)]
     pub fn check_take_suffix_ok() {
         let data: Vec<u8> = Vec::bounded_any::<16>();
         kani::assume(data.len() >= 4);
@@ -392,6 +395,7 @@ mod verification {
     }
 
     #[kani::proof]
+    #[kani::unwind(32)]
     pub fn check_take_suffix_too_large() {
         let data: Vec<u8> = Vec::bounded_any::<16>();
         let mut bytes = Bytes::from_source(data.clone());
@@ -402,6 +406,7 @@ mod verification {
     }
 
     #[kani::proof]
+    #[kani::unwind(16)]
     pub fn check_slice_to_bytes_ok() {
         let data: Vec<u8> = Vec::bounded_any::<16>();
         kani::assume(data.len() >= 8);
@@ -412,6 +417,7 @@ mod verification {
     }
 
     #[kani::proof]
+    #[kani::unwind(16)]
     pub fn check_slice_to_bytes_unrelated() {
         let data: Vec<u8> = Vec::bounded_any::<16>();
         let bytes = Bytes::from_source(data.clone());