simulator: add counterexample minimization

simulator/generation/plan.rs

@@ -1,8 +1,6 @@
 use std::{fmt::Display, rc::Rc};
 
 use limbo_core::{Connection, Result, StepResult};
-use rand::SeedableRng;
-use rand_chacha::ChaCha8Rng;
 
 use crate::{
     model::{
@@ -19,20 +17,56 @@ use super::{pick, pick_index};
 pub(crate) type ResultSet = Result<Vec<Vec<Value>>>;
 
 pub(crate) struct InteractionPlan {
-    pub(crate) plan: Vec<Interaction>,
+    pub(crate) plan: Vec<Property>,
     pub(crate) stack: Vec<ResultSet>,
     pub(crate) interaction_pointer: usize,
+    pub(crate) secondary_pointer: usize,
+}
+
+pub(crate) struct Property {
+    pub(crate) name: Option<String>,
+    pub(crate) interactions: Vec<Interaction>,
+}
+
+impl Property {
+    pub(crate) fn new(name: Option<String>, interactions: Vec<Interaction>) -> Self {
+        Self { name, interactions }
+    }
+
+    pub(crate) fn anonymous(interactions: Vec<Interaction>) -> Self {
+        Self {
+            name: None,
+            interactions,
+        }
+    }
 }
 
 impl Display for InteractionPlan {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        for interaction in &self.plan {
-            match interaction {
-                Interaction::Query(query) => writeln!(f, "{};", query)?,
-                Interaction::Assertion(assertion) => {
-                    writeln!(f, "-- ASSERT: {};", assertion.message)?
+        for property in &self.plan {
+            if let Some(name) = &property.name {
+                writeln!(f, "-- begin testing '{}'", name)?;
+            }
+
+            for interaction in &property.interactions {
+                if property.name.is_some() {
+                    write!(f, "\t")?;
                 }
-                Interaction::Fault(fault) => writeln!(f, "-- FAULT: {};", fault)?,
+
+                match interaction {
+                    Interaction::Query(query) => writeln!(f, "{};", query)?,
+                    Interaction::Assumption(assumption) => {
+                        writeln!(f, "-- ASSUME: {};", assumption.message)?
+                    }
+                    Interaction::Assertion(assertion) => {
+                        writeln!(f, "-- ASSERT: {};", assertion.message)?
+                    }
+                    Interaction::Fault(fault) => writeln!(f, "-- FAULT: {};", fault)?,
+                }
+            }
+
+            if let Some(name) = &property.name {
+                writeln!(f, "-- end testing '{}'", name)?;
             }
         }
 
@@ -60,6 +94,7 @@ impl Display for InteractionStats {
 
 pub(crate) enum Interaction {
     Query(Query),
+    Assumption(Assertion),
     Assertion(Assertion),
     Fault(Fault),
 }
@@ -68,13 +103,14 @@ impl Display for Interaction {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
             Self::Query(query) => write!(f, "{}", query),
+            Self::Assumption(assumption) => write!(f, "ASSUME: {}", assumption.message),
             Self::Assertion(assertion) => write!(f, "ASSERT: {}", assertion.message),
             Self::Fault(fault) => write!(f, "FAULT: {}", fault),
         }
     }
 }
 
-type AssertionFunc = dyn Fn(&Vec<ResultSet>) -> bool;
+type AssertionFunc = dyn Fn(&Vec<ResultSet>, &SimulatorEnv) -> bool;
 
 pub(crate) struct Assertion {
     pub(crate) func: Box<AssertionFunc>,
@@ -93,11 +129,9 @@ impl Display for Fault {
     }
 }
 
-pub(crate) struct Interactions(Vec<Interaction>);
-
-impl Interactions {
+impl Property {
     pub(crate) fn shadow(&self, env: &mut SimulatorEnv) {
-        for interaction in &self.0 {
+        for interaction in &self.interactions {
             match interaction {
                 Interaction::Query(query) => match query {
                     Query::Create(create) => {
@@ -117,6 +151,7 @@ impl Interactions {
                     Query::Select(_) => {}
                 },
                 Interaction::Assertion(_) => {}
+                Interaction::Assumption(_) => {}
                 Interaction::Fault(_) => {}
             }
         }
@@ -129,29 +164,29 @@ impl InteractionPlan {
             plan: Vec::new(),
             stack: Vec::new(),
             interaction_pointer: 0,
+            secondary_pointer: 0,
         }
     }
 
-    pub(crate) fn push(&mut self, interaction: Interaction) {
-        self.plan.push(interaction);
-    }
-
     pub(crate) fn stats(&self) -> InteractionStats {
         let mut read = 0;
         let mut write = 0;
         let mut delete = 0;
         let mut create = 0;
 
-        for interaction in &self.plan {
-            match interaction {
-                Interaction::Query(query) => match query {
-                    Query::Select(_) => read += 1,
-                    Query::Insert(_) => write += 1,
-                    Query::Delete(_) => delete += 1,
-                    Query::Create(_) => create += 1,
-                },
-                Interaction::Assertion(_) => {}
-                Interaction::Fault(_) => {}
+        for property in &self.plan {
+            for interaction in &property.interactions {
+                match interaction {
+                    Interaction::Query(query) => match query {
+                        Query::Select(_) => read += 1,
+                        Query::Insert(_) => write += 1,
+                        Query::Delete(_) => delete += 1,
+                        Query::Create(_) => create += 1,
+                    },
+                    Interaction::Assertion(_) => {}
+                    Interaction::Assumption(_) => {}
+                    Interaction::Fault(_) => {}
+                }
             }
         }
 
@@ -164,36 +199,33 @@ impl InteractionPlan {
     }
 }
 
-impl ArbitraryFrom<SimulatorEnv> for InteractionPlan {
-    fn arbitrary_from<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Self {
+impl InteractionPlan {
+    // todo: This is a hack to get around the fact that `ArbitraryFrom<T>` can't take a mutable
+    // reference of T, so instead write a bespoke function without using the trait system.
+    pub(crate) fn arbitrary_from<R: rand::Rng>(rng: &mut R, env: &mut SimulatorEnv) -> Self {
         let mut plan = InteractionPlan::new();
 
-        let mut env = SimulatorEnv {
-            opts: env.opts.clone(),
-            tables: vec![],
-            connections: vec![],
-            io: env.io.clone(),
-            db: env.db.clone(),
-            rng: ChaCha8Rng::seed_from_u64(rng.next_u64()),
-        };
-
         let num_interactions = env.opts.max_interactions;
 
         // First create at least one table
         let create_query = Create::arbitrary(rng);
         env.tables.push(create_query.table.clone());
-        plan.push(Interaction::Query(Query::Create(create_query)));
+
+        plan.plan.push(Property {
+            name: Some("initial table creation".to_string()),
+            interactions: vec![Interaction::Query(Query::Create(create_query))],
+        });
 
         while plan.plan.len() < num_interactions {
             log::debug!(
                 "Generating interaction {}/{}",
                 plan.plan.len(),
                 num_interactions
             );
-            let interactions = Interactions::arbitrary_from(rng, &(&env, plan.stats()));
-            interactions.shadow(&mut env);
+            let property = Property::arbitrary_from(rng, &(env, plan.stats()));
+            property.shadow(env);
 
-            plan.plan.extend(interactions.0.into_iter());
+            plan.plan.push(property);
         }
 
         log::info!("Generated plan with {} interactions", plan.plan.len());
@@ -251,31 +283,67 @@ impl Interaction {
             Self::Assertion(_) => {
                 unreachable!("unexpected: this function should only be called on queries")
             }
-            Interaction::Fault(_) => {
+            Self::Assumption(_) => {
+                unreachable!("unexpected: this function should only be called on queries")
+            }
+            Self::Fault(_) => {
                 unreachable!("unexpected: this function should only be called on queries")
             }
         }
     }
 
-    pub(crate) fn execute_assertion(&self, stack: &Vec<ResultSet>) -> Result<()> {
+    pub(crate) fn execute_assertion(
+        &self,
+        stack: &Vec<ResultSet>,
+        env: &SimulatorEnv,
+    ) -> Result<()> {
         match self {
             Self::Query(_) => {
                 unreachable!("unexpected: this function should only be called on assertions")
             }
             Self::Assertion(assertion) => {
-                if !assertion.func.as_ref()(stack) {
+                if !assertion.func.as_ref()(stack, env) {
                     return Err(limbo_core::LimboError::InternalError(
                         assertion.message.clone(),
                     ));
                 }
                 Ok(())
             }
+            Self::Assumption(_) => {
+                unreachable!("unexpected: this function should only be called on assertions")
+            }
             Self::Fault(_) => {
                 unreachable!("unexpected: this function should only be called on assertions")
             }
         }
     }
 
+    pub(crate) fn execute_assumption(
+        &self,
+        stack: &Vec<ResultSet>,
+        env: &SimulatorEnv,
+    ) -> Result<()> {
+        match self {
+            Self::Query(_) => {
+                unreachable!("unexpected: this function should only be called on assumptions")
+            }
+            Self::Assertion(_) => {
+                unreachable!("unexpected: this function should only be called on assumptions")
+            }
+            Self::Assumption(assumption) => {
+                if !assumption.func.as_ref()(stack, env) {
+                    return Err(limbo_core::LimboError::InternalError(
+                        assumption.message.clone(),
+                    ));
+                }
+                Ok(())
+            }
+            Self::Fault(_) => {
+                unreachable!("unexpected: this function should only be called on assumptions")
+            }
+        }
+    }
+
     pub(crate) fn execute_fault(&self, env: &mut SimulatorEnv, conn_index: usize) -> Result<()> {
         match self {
             Self::Query(_) => {
@@ -284,6 +352,9 @@ impl Interaction {
             Self::Assertion(_) => {
                 unreachable!("unexpected: this function should only be called on faults")
             }
+            Self::Assumption(_) => {
+                unreachable!("unexpected: this function should only be called on faults")
+            }
             Self::Fault(fault) => {
                 match fault {
                     Fault::Disconnect => {
@@ -306,7 +377,7 @@ impl Interaction {
     }
 }
 
-fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Interactions {
+fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Property {
     // Get a random table
     let table = pick(&env.tables, rng);
     // Pick a random column
@@ -324,6 +395,18 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Inte
             row.push(value);
         }
     }
+
+    // Check that the table exists
+    let assumption = Interaction::Assumption(Assertion {
+        message: format!("table {} exists", table.name),
+        func: Box::new({
+            let table_name = table.name.clone();
+            move |_: &Vec<ResultSet>, env: &SimulatorEnv| {
+                env.tables.iter().any(|t| t.name == table_name)
+            }
+        }),
+    });
+
     // Insert the row
     let insert_query = Interaction::Query(Query::Insert(Insert {
         table: table.name.clone(),
@@ -345,7 +428,7 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Inte
             column.name,
             value,
         ),
-        func: Box::new(move |stack: &Vec<ResultSet>| {
+        func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
             let rows = stack.last().unwrap();
             match rows {
                 Ok(rows) => rows.iter().any(|r| r == &row),
@@ -354,10 +437,13 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Inte
         }),
     });
 
-    Interactions(vec![insert_query, select_query, assertion])
+    Property::new(
+        Some("select contains inserted value".to_string()),
+        vec![assumption, insert_query, select_query, assertion],
+    )
 }
 
-fn property_double_create_failure<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv) -> Interactions {
+fn property_double_create_failure<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv) -> Property {
     let create_query = Create::arbitrary(rng);
     let table_name = create_query.table.name.clone();
     let cq1 = Interaction::Query(Query::Create(create_query.clone()));
@@ -367,7 +453,7 @@ fn property_double_create_failure<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv
         message:
             "creating two tables with the name should result in a failure for the second query"
                 .to_string(),
-        func: Box::new(move |stack: &Vec<ResultSet>| {
+        func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
             let last = stack.last().unwrap();
             match last {
                 Ok(_) => false,
@@ -378,31 +464,34 @@ fn property_double_create_failure<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv
         }),
     });
 
-    Interactions(vec![cq1, cq2, assertion])
+    Property::new(
+        Some("creating the same table twice fails".to_string()),
+        vec![cq1, cq2, assertion],
+    )
 }
 
-fn create_table<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv) -> Interactions {
+fn create_table<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv) -> Property {
     let create_query = Interaction::Query(Query::Create(Create::arbitrary(rng)));
-    Interactions(vec![create_query])
+    Property::anonymous(vec![create_query])
 }
 
-fn random_read<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Interactions {
+fn random_read<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Property {
     let select_query = Interaction::Query(Query::Select(Select::arbitrary_from(rng, &env.tables)));
-    Interactions(vec![select_query])
+    Property::anonymous(vec![select_query])
 }
 
-fn random_write<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Interactions {
+fn random_write<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Property {
     let table = pick(&env.tables, rng);
     let insert_query = Interaction::Query(Query::Insert(Insert::arbitrary_from(rng, table)));
-    Interactions(vec![insert_query])
+    Property::anonymous(vec![insert_query])
 }
 
-fn random_fault<R: rand::Rng>(_rng: &mut R, _env: &SimulatorEnv) -> Interactions {
+fn random_fault<R: rand::Rng>(_rng: &mut R, _env: &SimulatorEnv) -> Property {
     let fault = Interaction::Fault(Fault::Disconnect);
-    Interactions(vec![fault])
+    Property::anonymous(vec![fault])
 }
 
-impl ArbitraryFrom<(&SimulatorEnv, InteractionStats)> for Interactions {
+impl ArbitraryFrom<(&SimulatorEnv, InteractionStats)> for Property {
     fn arbitrary_from<R: rand::Rng>(
         rng: &mut R,
         (env, stats): &(&SimulatorEnv, InteractionStats),