Correct Build Action

.github/workflows/rust.yml

@@ -21,7 +21,7 @@ jobs:
           rustflags: ""
     - name: Build
       run: cargo build -vv
+      env:
+        CORSET_TEST_LIMIT: 1000
     - name: Run tests
       run: cargo test -v
-      env:
-        CORSET_TEST_LIMIT: 4

build.rs

@@ -58,7 +58,7 @@ fn generate_tests_from_lisp_files() {
     let out_dir = std::env::var("OUT_DIR").unwrap();
     let limit = match env::var("CORSET_TEST_LIMIT") {
         Ok(s) => s.parse().unwrap(),
-        Err(_) => 0,
+        Err(_) => 100,
     };
     let target = std::path::Path::new(&out_dir).join("lisp_tests.rs");
     let mut f = fs::File::create(target).unwrap();
@@ -70,7 +70,6 @@ fn generate_tests_from_lisp_files() {
         writeln!(f, "fn test_{}() {{ check(\"{}\"); }}", m.name, m.name).unwrap();
         // Check whether oracle provided or not
         if m.oracle.is_some() {
-            let limit = limit.max(m.limit);
             // Generate trace inputs (accepts / rejects)
             let (accepts, rejects) = m.generate_traces_upto(limit);
             // Write them out.

tests/models.rs

@@ -4,35 +4,35 @@
 /// be accepted and which should be rejected.  In essence, we are
 /// comparing a Rust function (the model) against the constraints
 /// evaluated on the trace.
 struct Model {
     /// The name of this test (which should correspond to a lisp
     /// file).
     name: &'static str,
     /// The column names needed for this test.
     cols: &'static [&'static str],
-    /// Number of rows to generate for.
-    limit: usize,
     /// The oracle determines, for a given set of column data, whether
     /// or not it should be accepted or rejected.
     oracle: Option<fn(data: &Trace) -> bool>,
 }
 
 impl Model {
     const MIN_ELEMENT: isize = -1;
     const MAX_ELEMENT: isize = 1;
 
     /// Generate all traces matching the model configuration upto
     /// length `n`, and split them into the `accepts` and `rejects`.
     /// The former are those traces which are expected to pass, whilst
     /// the latter are those which are expected to fail.
-    pub fn generate_traces_upto(&self, n: usize) -> (Vec<Trace>, Vec<Trace>) {
+    pub fn generate_traces_upto(&self, m: usize) -> (Vec<Trace>, Vec<Trace>) {
+        let max_rows = Self::determine_max_rows(self.cols.len(), m);
+        //
         let Some(oracle) = self.oracle else {
             panic!();
         };
         let mut accepts = Vec::new();
         let mut rejects = Vec::new();
         //
-        for i in 0..n {
+        for i in 0..max_rows {
             for tr in self.generate_all_traces(i) {
                 // Test the trace using the given oracle to check whether
                 // (or not) it should be accepted.
@@ -77,11 +77,41 @@
         // no more
         return false;
     }
+
+    // Determine maximum number of trace rows we can generate within
+    // the given budget (i.e. maximum number of traces).
+    fn determine_max_rows(n: usize, m: usize) -> usize {
+        let mut cost = 0;
+        // You can compute this with pow
+        for i in 0..10 {
+            let ith = Self::cost_max_rows(i, n);
+            //
+            if (cost + ith) >= m {
+                return i;
+            }
+            //
+            cost += ith;
+        }
+        // Should be
+        unreachable!()
+    }
+
+    fn cost_max_rows(i: usize, n: usize) -> usize {
+        let diff = 1 + (Self::MAX_ELEMENT - Self::MIN_ELEMENT) as usize;
+        //
+        let mut acc = 1;
+        // You can compute this with pow
+        for _ in 0..(i * n) {
+            acc *= diff;
+        }
+        //
+        acc
+    }
 }
 
 /// Represents an individial trace which, for a given number of rows,
 /// contains values for each of the columns.
 struct Trace {
     /// Simplistic column schema.
     cols: &'static [&'static str],
     /// The trace data, whose length must be divisible by `width`.
@@ -92,7 +122,7 @@
 }
 
 impl Trace {
     pub fn new(cols: &'static [&'static str], data: Vec<isize>) -> Self {
         Self {
             cols,
             data,
@@ -133,7 +163,7 @@
 
 /// Represents a single column which can contain zero (or more) rows
 /// of padding at the beginning.
 struct Column<'a> {
     // The raw data underlying this column
     data: &'a [isize],
     // The number of rows of passing which are assumed to be prepended
@@ -159,53 +189,45 @@
 
 /// The master list of active models.  Tests will be automatically
 /// generated for each item in this list.
 static MODELS: &[Model] = &[
     Model {
         name: "arrays_1",
         cols: &["A", "B_1", "B_2", "B_3"],
-        limit: 2,
         oracle: Some(arrays_1_oracle),
     },
     Model {
         name: "iszero",
         cols: &["A", "B"],
-        limit: 3,
         oracle: Some(iszero_oracle),
     },
     Model {
         name: "shift_1",
         cols: &["A", "B"],
-        limit: 3,
         oracle: Some(shift_1_oracle),
     },
     Model {
         name: "shift_2",
         cols: &["A", "B"],
-        limit: 3,
         oracle: Some(shift_2_oracle),
     },
     Model {
         name: "shift_3",
         cols: &["A", "B"],
-        limit: 3,
         oracle: Some(shift_3_oracle),
     },
     Model {
         name: "shift_5",
         cols: &["A", "B", "C"],
-        limit: 2,
         oracle: Some(shift_5_oracle),
     },
     Model {
         name: "vanish_1",
         cols: &["X"],
-        limit: 3,
         oracle: Some(|_| false),
     },
     Model {
         name: "vanish_2",
         cols: &["X"],
-        limit: 3,
         oracle: Some(|_| false),
     },
 ];
@@ -215,7 +237,7 @@
 // ===================================================================
 
 #[allow(non_snake_case)]
 fn arrays_1_oracle(tr: &Trace) -> bool {
     let (A, B_1, B_2, B_3) = (tr.col("A"), tr.col("B_1"), tr.col("B_2"), tr.col("B_3"));
 
     for k in 0..tr.height() {
@@ -234,7 +256,7 @@
 // // ===================================================================
 
 #[allow(non_snake_case)]
 fn iszero_oracle(tr: &Trace) -> bool {
     let (A, B) = (tr.col("A"), tr.col("B"));
 
     for k in 0..tr.height() {