Merge pull request #1119 from informalsystems/gabriela/new-flattening…

…-wiring

New flattening

examples/README.md

@@ -62,7 +62,7 @@ listed without any additional command line arguments.
 | [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693,</sup><sup>https://github.com/informalsystems/quint/pull/975</sup> |
 | [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/tendermint/TendermintAcc005.qnt](./cosmos/tendermint/TendermintAcc005.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/pull/1023</sup> | :x:<sup>https://github.com/informalsystems/quint/pull/1023</sup> |
 | [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693</sup> |

examples/cosmos/tendermint/TendermintAcc005.qnt

@@ -665,6 +665,7 @@ module TendermintAcc {
 // Tests that demonstrate typical behavior.
 module TendermintTest {
   import TendermintAcc.*
+  export TendermintAcc.*
 
   // Quint will automatically compute the unchanged block in the future
   action unchangedAll = all {

examples/language-features/instances.qnt

@@ -24,9 +24,6 @@ module instances {
   // the above is equivalent to TLA+'s instance:
   // A2 == INSTANCE A WITH x <- 15, y <- MyY
 
-  export A1
-  export A2
-
   action init = true
   action step = true
 }

examples/language-features/instancesFrom.qnt

@@ -15,9 +15,6 @@ module instancesFrom {
   // the above is equivalent to TLA+'s instance:
   // A2 == INSTANCE A WITH x <- 15, y <- MyY
 
-  export A1
-  export A2
-
   action init = true
   action step = true
 }

quint/apalache-tests.md

@@ -29,7 +29,8 @@ quint verify --init=invalidInit ../examples/language-features/booleans.qnt
 <!-- !test exit 1 -->
 <!-- !test err invalid init -->
 ```
-error: Configuration error (see the manual): Operator invalidInit not found (used as the initialization predicate)
+error: [QNT404] Name 'invalidInit' not found
+error: name resolution failed
 ```
 
 

quint/src/cliCommands.ts

@@ -17,6 +17,7 @@ import {
   ErrorMessage,
   Loc,
   compactSourceMap,
+  parseDefOrThrow,
   parsePhase1fromText,
   parsePhase2sourceResolution,
   parsePhase3importAndNameResolution,
@@ -42,8 +43,8 @@ import { verbosity } from './verbosity'
 import { Rng, newRng } from './rng'
 import { fileSourceResolver } from './parsing/sourceResolver'
 import { verify } from './quintVerifier'
-import { flattenModules } from './flattening'
-import { analyzeModules } from './quintAnalyzer'
+import { flattenModules } from './flattening/fullFlattener'
+import { analyzeInc, analyzeModules } from './quintAnalyzer'
 import { ExecutionFrame } from './runtime/trace'
 
 export type stage = 'loading' | 'parsing' | 'typechecking' | 'testing' | 'running' | 'documentation'
@@ -542,6 +543,34 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
   // TODO error handing for file reads and deserde
   const loadedConfig = args.apalacheConfig ? JSON.parse(readFileSync(args.apalacheConfig, 'utf-8')) : {}
 
+  const mainArg = prev.args.main
+  const mainName = mainArg ? mainArg : basename(prev.args.input, '.qnt')
+  const main = verifying.modules.find(m => m.name === mainName)
+  if (!main) {
+    return cliErr(`module ${mainName} does not exist`, { ...verifying, errors: [], sourceCode: '' })
+  }
+
+  // Wrap init, step and invariant in other definitions, to make sure they are not considered unused in the main module
+  // and, therefore, ignored by the flattener
+  const extraDefsAsText = [`action q::init = ${args.init}`, `action q::step = ${args.step}`]
+  if (args.invariant) {
+    extraDefsAsText.push(`val q::inv = and(${args.invariant.join(',')})`)
+  }
+
+  const extraDefs = extraDefsAsText.map(d => parseDefOrThrow(d, verifying.idGen, new Map()))
+  main.declarations.push(...extraDefs)
+
+  // We have to update the lookup table and analysis result with the new definitions. This is not ideal, and the problem
+  // is that is hard to add this definitions in the proper stage, in our current setup. We should try to tackle this
+  // while solving #1052.
+  const resolutionResult = parsePhase3importAndNameResolution(prev)
+  if (resolutionResult.isLeft()) {
+    return cliErr('name resolution failed', { ...verifying, errors: resolutionResult.value })
+  }
+
+  verifying.table = resolutionResult.unwrap().table
+  extraDefs.forEach(def => analyzeInc(verifying, verifying.table, def))
+
   // Flatten modules, replacing instances, imports and exports with their definitions
   const { flattenedModules, flattenedTable, flattenedAnalysis } = flattenModules(
     verifying.modules,
@@ -552,15 +581,9 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
   )
 
   // Pick main module, we only pass this on to Apalache
-  const mainArg = prev.args.main
-  const mainName = mainArg ? mainArg : basename(prev.args.input, '.qnt')
-  const main = flattenedModules.find(m => m.name === mainName)
-
-  if (!main) {
-    return cliErr(`module ${mainName} does not exist`, { ...verifying, errors: [], sourceCode: '' })
-  }
+  const flatMain = flattenedModules.find(m => m.name === mainName)!
 
-  const veryfiyingFlat = { ...verifying, ...flattenedAnalysis, modules: [main], table: flattenedTable }
+  const veryfiyingFlat = { ...verifying, ...flattenedAnalysis, modules: [flatMain], table: flattenedTable }
   const parsedSpec = jsonStringOfOutputStage(pickOutputStage(veryfiyingFlat))
 
   // We need to insert the data form CLI args into thier appropriate locations
@@ -578,9 +601,9 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
     checker: {
       ...(loadedConfig.checker ?? {}),
       length: args.maxSteps,
-      init: args.init,
-      next: args.step,
-      inv: args.invariant,
+      init: 'q::init',
+      next: 'q::step',
+      inv: args.invariant ? ['q::inv'] : undefined,
     },
   }