From 6515efeb73b5a7b5dffb7eac464fac4d44804f85 Mon Sep 17 00:00:00 2001 From: KtorZ Date: Fri, 15 Mar 2024 13:36:05 +0100 Subject: [PATCH] Implementing remaining shrinking strategies. This makes the search for counterexample slower in some cases by 30-40% with the hope of finding better counterexamples. We might want to add a flag '--simplification-level' to the command-line to let users decide on the level of simplifications. --- crates/aiken-project/src/test_framework.rs | 104 ++++++++++++++------- 1 file changed, 69 insertions(+), 35 deletions(-) diff --git a/crates/aiken-project/src/test_framework.rs b/crates/aiken-project/src/test_framework.rs index 11d162c3..90e0c4ae 100644 --- a/crates/aiken-project/src/test_framework.rs +++ b/crates/aiken-project/src/test_framework.rs @@ -8,6 +8,7 @@ use aiken_lang::{ }; use cryptoxide::{blake2b::Blake2b, digest::Digest}; use indexmap::IndexMap; +use itertools::Itertools; use owo_colors::{OwoColorize, Stream}; use pallas::ledger::primitives::alonzo::{Constr, PlutusData}; use patricia_tree::PatriciaMap; @@ -580,10 +581,10 @@ impl<'a> Counterexample<'a> { /// /// - Deleting chunks /// - Transforming chunks into sequence of zeroes - /// - Decrementing chunks of values - /// - Replacing chunks of values - /// - Sorting chunks - /// - Redistribute values between nearby pairs + /// - Replacing chunks of values with smaller values + /// - Sorting chunks in ascending order + /// - Swapping nearby pairs + /// - Redistributing values between nearby pairs fn simplify(&mut self) { let mut prev; @@ -640,37 +641,71 @@ impl<'a> Counterexample<'a> { k /= 2 } - // Now we try replacing region of choices with zeroes. Note that unlike the above we - // skip k = 1 because we handle that in the next step. Often (but not always) a block - // of all zeroes is the smallest value that a region can be. - let mut k: isize = 8; - while k > 1 { - let mut i: isize = self.choices.len() as isize - k; - while i >= 0 { - let ivs = (i..i + k).map(|j| (j as usize, 0)).collect::>(); - i -= if self.replace(ivs) { k } else { 1 } + if !self.choices.is_empty() { + // Now we try replacing region of choices with zeroes. Note that unlike the above we + // skip k = 1 because we handle that in the next step. Often (but not always) a block + // of all zeroes is the smallest value that a region can be. + let mut k = 8; + while k > 1 { + let mut i = self.choices.len(); + while i >= k { + let ivs = (i - k..i).map(|j| (j, 0)).collect::>(); + i -= if self.replace(ivs) { k } else { 1 } + } + k /= 2 } - k /= 2 - } - // Replace choices with smaller value, by doing a binary search. This will replace n - // with 0 or n - 1, if possible, but will also more efficiently replace it with, a - // smaller number than doing multiple subtractions would. - let (mut i, mut underflow) = if self.choices.is_empty() { - (0, true) - } else { - (self.choices.len() - 1, false) - }; - while !underflow { - self.binary_search_replace(0, self.choices[i], |v| vec![(i, v)]); - (i, underflow) = i.overflowing_sub(1); - } + // Replace choices with smaller value, by doing a binary search. This will replace n + // with 0 or n - 1, if possible, but will also more efficiently replace it with, a + // smaller number than doing multiple subtractions would. + let (mut i, mut underflow) = (self.choices.len() - 1, false); + while !underflow { + self.binary_search_replace(0, self.choices[i], |v| vec![(i, v)]); + (i, underflow) = i.overflowing_sub(1); + } - // TODO: Remaining shrinking strategies... - // - // - Swaps - // - Sorting - // - Pair adjustments + // Sort out of orders chunks in ascending order + let mut k = 8; + while k > 1 { + let mut i = self.choices.len() - 1; + while i >= k { + let (from, to) = (i - k, i); + self.replace( + (from..to) + .zip(self.choices[from..to].iter().cloned().sorted()) + .collect(), + ); + i -= 1; + } + k /= 2 + } + + // Try adjusting nearby pairs by: + // + // - Swapping them if they are out-of-order + // - Redistributing values between them. + for k in [2, 1] { + let mut j = self.choices.len() - 1; + while j >= k { + let i = j - k; + + // Swap + if self.choices[i] > self.choices[j] { + self.replace(vec![(i, self.choices[j]), (j, self.choices[i])]); + } + + let iv = self.choices[i]; + let jv = self.choices[j]; + + // Replace + if iv > 0 && jv <= u8::max_value() - iv { + self.binary_search_replace(0, iv, |v| vec![(i, v), (j, jv + (iv - v))]); + } + + j -= 1 + } + } + } // If we've reached a fixed point, then we cannot shrink further. We've reached a // (local) minimum, which is as good as a counterexample we'll get with this approach. @@ -682,7 +717,6 @@ impl<'a> Counterexample<'a> { /// Try to replace a value with a smaller value by doing a binary search between /// two extremes. This converges relatively fast in order to shrink down values. - /// fast. fn binary_search_replace(&mut self, lo: u8, hi: u8, f: F) -> u8 where F: Fn(u8) -> Vec<(usize, u8)>, @@ -1508,8 +1542,8 @@ mod test { counterexample.simplify(); - assert_eq!(counterexample.choices, vec![252, 149]); - assert_eq!(reify(counterexample.value), "(252, 149)"); + assert_eq!(counterexample.choices, vec![149, 252]); + assert_eq!(reify(counterexample.value), "(149, 252)"); } #[test]