feat: Add support for multiple invariants in CLI commands

docs/pages/docs/checking-properties.mdx

@@ -54,12 +54,12 @@ quint run gettingStarted.qnt --witnesses=alice_more_than_bob --max-steps=5
 
 Quint reports:
 ```ansi
-[ok] No violation found (599ms).
-You may increase --max-samples and --max-steps.
-Use --verbosity to produce more (or less) output.
-Witnesses:
-alice_more_than_bob was witnessed in 7094 trace(s) out of 10000 explored (70.94%)
-Use --seed=0x1c8a2137939c73 to reproduce.
+[ok] No violation found (599ms).
+You may increase --max-samples and --max-steps.
+Use --verbosity to produce more (or less) output.
+Witnesses:
+alice_more_than_bob was witnessed in 7094 trace(s) out of 10000 explored (70.94%)
+Use --seed=0x1c8a2137939c73 to reproduce.
 ```
 
 And that informs us that, in most executions, there is a state where Alice has a larger balance than that of Bob.
@@ -78,16 +78,50 @@ quint run gettingStarted.qnt --invariant="not(alice_more_than_bob)" --max-steps=
 
 Quint reports:
 ```ansi
-An example execution:
-
-[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
-
-[State 1] { balances: Map("alice" -> 9, "bob" -> 0, "charlie" -> 0) }
-
-[violation] Found an issue (8ms).
-Use --verbosity=3 to show executions.
-Use --seed=0xa0bbf64f2c03 to reproduce.
-error: Invariant violated
+An example execution:
+
+[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
+
+[State 1] { balances: Map("alice" -> 9, "bob" -> 0, "charlie" -> 0) }
+
+[violation] Found an issue (8ms).
+Use --verbosity=3 to show executions.
+Use --seed=0xa0bbf64f2c03 to reproduce.
+error: Invariant violated
 ```
 
 Although it says "Invariant violated", this is exactly what we wanted: an example where Alice has more balance than Bob.
+
+### Using multiple invariants with `--invariants`
+
+If you want to check multiple invariants at once and determine which ones are violated, you can use the `--invariants` option:
+
+```sh
+quint run bank.qnt --invariants no_negatives accounts_match total_positive
+```
+
+Quint will check all three invariants and report which specific ones are violated:
+
+```ansi
+[90mAn example execution:[39m
+[90m[39m
+[[1mState 0[22m] { balances[90m:[39m [32mMap[39m([32m"alice"[39m[90m ->[39m [33m0[39m, [32m"bob"[39m[90m ->[39m [33m0[39m, [32m"charlie"[39m[90m ->[39m [33m0[39m) }
+
+[[1mState 1[22m] { balances[90m:[39m [32mMap[39m([32m"alice"[39m[90m ->[39m [33m-63[39m, [32m"bob"[39m[90m ->[39m [33m0[39m, [32m"charlie"[39m[90m ->[39m [33m0[39m) }
+
+[31m[violation][39m Found an issue [90m(44ms).[39m
+[31mViolated invariants:[39m
+[31m  - no_negatives[39m
+[31m  - total_positive[39m
+[90mUse --verbosity=3 to show executions.[39m
+[90mUse --seed=0x4e85b3a53f7ef to reproduce.[39m
+error: Invariant violated
+```
+
+This makes it easier to identify which specific properties are being violated when you have multiple invariants to check.
+
+The `--invariants` option also works with the `verify` command, allowing you to check multiple invariants with formal verification:
+
+```sh
+quint verify bank.qnt --invariants no_negatives accounts_match total_positive
+```

quint/src/cli.ts

@@ -266,8 +266,13 @@ const runCmd = {
         type: 'string',
         default: 'step',
       })
+      .option('invariants', {
+        desc: 'space separated list of invariants to check (definition names). When specified, all invariants are combined with AND and checked together, with detailed reporting of which ones were violated',
+        type: 'array',
+        default: [],
+      })
       .option('invariant', {
-        desc: 'invariant to check: a definition name or an expression',
+        desc: 'invariant to check: a definition name or an expression. Can be used together with --invariants',
         type: 'string',
         default: 'true',
       })
@@ -318,6 +323,11 @@ const verifyCmd = {
   desc: `Verify a Quint specification via Apalache`,
   builder: (yargs: any) =>
     compileOpts(yargs)
+      .option('invariants', {
+        desc: 'space separated list of invariants to check (definition names). When specified, all invariants are combined with AND and checked together, with detailed reporting of which ones were violated',
+        type: 'array',
+        default: [],
+      })
       .option('out-itf', {
         desc: 'output the trace in the Informal Trace Format to file, e.g., out.itf.json (suppresses all console output)',
         type: 'string',

quint/src/cliCommands.ts

@@ -335,11 +335,11 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
   }
   const rng = rngOrError.unwrap()
 
-  const matchFun = (n: string): boolean => isMatchingTest(testing.args.match, n)
-  const maxSamples = testing.args.maxSamples
+  const matchFun = (n: string): boolean => isMatchingTest(prev.args.match, n)
+  const maxSamples = prev.args.maxSamples
   const options: TestOptions = {
     testMatch: matchFun,
-    maxSamples: testing.args.maxSamples,
+    maxSamples: prev.args.maxSamples,
     rng,
     verbosity: verbosityLevel,
     onTrace: (index: number) => (name: string, status: string, vars: string[], states: QuintEx[]) => {
@@ -358,7 +358,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
 
   const out = console.log
 
-  const outputTemplate = testing.args.outItf
+  const outputTemplate = prev.args.outItf
 
   // Start the Timer and being running the tests
   const startMs = Date.now()
@@ -371,37 +371,35 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
     .flat()
     .filter(d => d.kind === 'def' && options.testMatch(d.name))
 
-  const evaluator = new Evaluator(testing.table, newTraceRecorder(verbosityLevel, rng, 1), rng)
-  const results: TestResult[] = []
-  let nFailures = 1
+  const evaluator = new Evaluator(prev.table, newTraceRecorder(verbosityLevel, rng, 1), rng)
+  const results = testDefs.map((def, index) => {
+    return evaluator.test(def, maxSamples, options.onTrace(index))
+  })
 
-  // Run each test and display results immediately
-  for (const def of testDefs) {
-    const result = evaluator.test(def, maxSamples, options.onTrace(results.length))
-    results.push(result)
+  // We're finished running the tests
+  const elapsedMs = Date.now() - startMs
 
-    // Display result immediately
-    if (verbosity.hasResults(verbosityLevel)) {
-      if (result.status === 'passed') {
-        out(`    ${chalk.green('ok')} ${result.name} passed ${result.nsamples} test(s)`)
+  // output the status for every test
+  let nFailures = 1
+  if (verbosity.hasResults(verbosityLevel)) {
+    results.forEach(res => {
+      if (res.status === 'passed') {
+        out(`    ${chalk.green('ok')} ${res.name} passed ${res.nsamples} test(s)`)
       }
-      if (result.status === 'failed') {
+      if (res.status === 'failed') {
         const errNo = chalk.red(nFailures)
-        out(`    ${errNo}) ${result.name} failed after ${result.nsamples} test(s)`)
+        out(`    ${errNo}) ${res.name} failed after ${res.nsamples} test(s)`)
         nFailures++
       }
-    }
+    })
   }
 
-  // We're finished running the tests
-  const elapsedMs = Date.now() - startMs
-
   const passed = results.filter(r => r.status === 'passed')
   const failed = results.filter(r => r.status === 'failed')
   const ignored = results.filter(r => r.status === 'ignored')
   const namedErrors: [TestResult, ErrorMessage][] = failed.reduce(
     (acc: [TestResult, ErrorMessage][], failure) =>
-      acc.concat(failure.errors.map(e => [failure, mkErrorMessage(testing.sourceMap)(e)])),
+      acc.concat(failure.errors.map(e => [failure, mkErrorMessage(prev.sourceMap)(e)])),
     []
   )
 
@@ -532,10 +530,28 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
   }
   const rng = rngOrError.unwrap()
 
+  // Process both invariant and invariants options
+  let invariantsList: string[] = []
+  if (prev.args.invariant && prev.args.invariant !== 'true') {
+    invariantsList.push(prev.args.invariant)
+  }
+  if (prev.args.invariants && prev.args.invariants.length > 0) {
+    invariantsList = invariantsList.concat(prev.args.invariants)
+  }
+  // If no invariants specified, use the default 'true'
+  const invariantString = invariantsList.length > 0 ? invariantsList.join(' and ') : 'true'
+  // Keep track of individual invariants for reporting
+  const individualInvariants = invariantsList.length > 0 ? invariantsList : ['true']
+
+  // We use:
+  // - 'invariantString' as the combined invariant string for the simulator to check
+  // - 'individualInvariants' for reporting which specific invariants were violated
+
   const options: SimulatorOptions = {
     init: prev.args.init,
     step: prev.args.step,
-    invariant: prev.args.invariant,
+    invariant: invariantString,
+    individualInvariants: individualInvariants,
     maxSamples: prev.args.maxSamples,
     maxSteps: prev.args.maxSteps,
     rng,
@@ -576,7 +592,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
   }
 
   const argsParsingResult = mergeInMany(
-    [prev.args.init, prev.args.step, prev.args.invariant, ...prev.args.witnesses].map(toExpr)
+    [prev.args.init, prev.args.step, invariantString, ...prev.args.witnesses].map(toExpr)
   )
   if (argsParsingResult.isLeft()) {
     return cliErr('Argument error', {
@@ -595,9 +611,18 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
       console.warn(chalk.yellow('Use the typescript backend if you need that functionality.'))
     }
 
+    // Parse the combined invariant for the Rust backend
+    const invariantExpr = toExpr(invariantString)
+    if (invariantExpr.isLeft()) {
+      return cliErr('Argument error', {
+        ...simulator,
+        errors: [mkErrorMessage(prev.sourceMap)(invariantExpr.value)],
+      })
+    }
+
     const quintRustWrapper = new QuintRustWrapper(verbosityLevel)
     outcome = await quintRustWrapper.simulate(
-      { modules: [], table: prev.resolver.table, main: mainName, init, step, invariant },
+      { modules: [], table: prev.resolver.table, main: mainName, init, step, invariant: invariantExpr.value },
       prev.path,
       witnesses,
       prev.args.maxSamples,
@@ -692,10 +717,34 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
       if (verbosity.hasResults(verbosityLevel)) {
         console.log(chalk.red(`[violation]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
 
-        if (verbosity.hasHints(verbosityLevel)) {
-          console.log(chalk.gray('Use --verbosity=3 to show executions.'))
+        // Show which invariants were violated, if we had multiple
+        if (individualInvariants.length > 1) {
+          console.log(chalk.red('Violated invariants:'))
+
+          // For each individual invariant, check if it's violated in the final state
+          for (const inv of individualInvariants) {
+            // Skip the default 'true' invariant
+            if (inv === 'true') continue
+
+            // Create a new evaluator to check just this invariant
+            const singleInvResult = toExpr(inv)
+            if (singleInvResult.isRight()) {
+              const testEvaluator = new Evaluator(prev.resolver.table, recorder, options.rng, options.storeMetadata)
+              const evalResult = testEvaluator.evaluate(singleInvResult.value)
+
+              // If we can evaluate it and it's false, it's violated
+              if (evalResult.isRight() && evalResult.value.kind === 'bool' && !evalResult.value.value) {
+                console.log(chalk.red(`  - ${inv}`))
+              }
+            }
+          }
         }
       }
+
+      if (verbosity.hasHints(verbosityLevel)) {
+        console.log(chalk.gray('Use --verbosity=3 to show executions.'))
+      }
+
       maybePrintWitnesses(verbosityLevel, outcome, prev.args.witnesses)
 
       return cliErr('Invariant violated', {
@@ -719,14 +768,20 @@ export async function compile(typechecked: TypecheckedStage): Promise<CLIProcedu
     return cliErr(`module ${mainName} does not exist`, { ...typechecked, errors: [], sourceCode: new Map() })
   }
 
-  // Wrap init, step, invariant and temporal properties in other definitions,
-  // to make sure they are not considered unused in the main module and,
-  // therefore, ignored by the flattener
+  // Process both invariant and invariants options
+  let invariantsList: string[] = []
+  if (args.invariant && args.invariant !== 'true') {
+    invariantsList.push(args.invariant)
+  }
+  if (args.invariants && args.invariants.length > 0) {
+    invariantsList = invariantsList.concat(args.invariants)
+  }
+  // If no invariants specified, use the default 'true'
+  const invariantString = invariantsList.length > 0 ? invariantsList.join(' and ') : 'true'
+
   const extraDefsAsText = [`action q::init = ${args.init}`, `action q::step = ${args.step}`]
+  extraDefsAsText.push(`val q::inv = and(${invariantString})`)
 
-  if (args.invariant) {
-    extraDefsAsText.push(`val q::inv = and(${args.invariant})`)
-  }
   if (args.temporal) {
     extraDefsAsText.push(`temporal q::temporalProps = and(${args.temporal})`)
   }
@@ -875,6 +930,15 @@ export async function verifySpec(prev: CompiledStage): Promise<CLIProcedure<Trac
   const veryfiyingFlat = { ...prev, modules: [prev.mainModule] }
   const parsedSpec = jsonStringOfOutputStage(pickOutputStage(veryfiyingFlat))
 
+  // Process both invariant and invariants options for verification
+  let hasInvariants = false
+  if (args.invariant && args.invariant !== 'true') {
+    hasInvariants = true
+  }
+  if (args.invariants && args.invariants.length > 0) {
+    hasInvariants = true
+  }
+
   // We need to insert the data form CLI args into their appropriate locations
   // in the Apalache config
   const config = {
@@ -892,7 +956,7 @@ export async function verifySpec(prev: CompiledStage): Promise<CLIProcedure<Trac
       length: args.maxSteps,
       init: 'q::init',
       next: 'q::step',
-      inv: args.invariant ? ['q::inv'] : undefined,
+      inv: hasInvariants ? ['q::inv'] : undefined,
       'temporal-props': args.temporal ? ['q::temporalProps'] : undefined,
       tuning: {
         ...(loadedConfig.checker?.tuning ?? {}),

quint/src/simulation.ts

@@ -19,6 +19,7 @@ export interface SimulatorOptions {
   init: string
   step: string
   invariant: string
+  individualInvariants?: string[]
   maxSamples: number
   maxSteps: number
   numberOfTraces: number