Two fixes for Paxos simulation

CHANGELOG.md

@@ -21,6 +21,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Topological sorting of modules (#1268)
 - The effect checker will now check for consistency of updates across different
   cases inside `match` (#1272)
+- Fix problems in the integration of sum types in `run`, `test`, and `verify` commands (#1276)
+- Fix some corner cases with the usage of complex expressions inside `assume`
+  and `import (...)` (#1276)
 
 ### Security
 

examples/.scripts/run-example.sh

@@ -15,6 +15,7 @@ result () {
 
     # Skip tests for parameterized modules
     if [[ "$cmd" == "test" && (
+            "$file" == "classic/distributed/Paxos/Voting.qnt" ||
             "$file" == "cosmos/tendermint/Tendermint.qnt" ||
             "$file" == "cosmos/tendermint/TendermintTest.qnt" ||
             "$file" == "cosmos/lightclient/Blockchain.qnt" ||
@@ -24,6 +25,7 @@ result () {
     fi
     # Skip verification for specs that do not define a state machine
     if [[ "$cmd" == "verify" && (
+            "$file" == "classic/distributed/Paxos/Voting.qnt" ||
             "$file" == "cosmos/lightclient/Blockchain.qnt" ||
             "$file" == "cosmos/lightclient/LCVerificationApi.qnt" ||
             "$file" == "cosmos/lightclient/typedefs.qnt" ||
@@ -46,12 +48,10 @@ result () {
     fi
 
     # Print additional explanations
-    if [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
-    elif [[ "$file" == "classic/distributed/Paxos/Voting.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
+    if [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" &&  "$cmd" == "verify" ]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/1034</sup>"
     elif [[ "$file" == "language-features/option.qnt" && "$cmd" == verify ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
+      printf "<sup>https://github.com/informalsystems/quint/issues/1034</sup>"
     elif [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/1019</sup>"
     fi
@@ -66,6 +66,8 @@ get_main () {
     main="--main=ReadersWriters_5"
   elif [[ "$file" == "classic/distributed/ewd840/ewd840.qnt" ]] ; then
     main="--main=ewd840_3"
+  elif [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" ]] ; then
+    main="--main=Paxos_val2_accept3_quorum2"
   elif [[ "$file" == "classic/sequential/BinSearch/BinSearch.qnt" ]] ; then
     main="--main=BinSearch10"
   elif [[ "$file" == "cosmos/ics20/bank.qnt" ]] ; then

examples/README.md

@@ -51,8 +51,8 @@ listed without any additional command line arguments.
 | [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
-| [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
+| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1034</sup> |
+| [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
@@ -80,7 +80,7 @@ listed without any additional command line arguments.
 | [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
+| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1034</sup> |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

quint/src/effects/inferrer.ts

@@ -87,7 +87,9 @@ export class EffectInferrer implements IRVisitor {
   private freeNames: { effectVariables: Set<string>; entityVariables: Set<string> }[] = []
 
   // the current depth of operator definitions: top-level defs are depth 0
-  private definitionDepth: number = 0
+  // FIXME(#1279): The walk* functions update this value, but they need to be
+  // initialized to -1 here for that to work on all scenarios.
+  definitionDepth: number = -1
 
   enterExpr(e: QuintEx) {
     this.location = `Inferring effect for ${expressionToString(e)}`
@@ -221,10 +223,6 @@ export class EffectInferrer implements IRVisitor {
     )
   }
 
-  enterOpDef(_def: QuintOpDef): void {
-    this.definitionDepth++
-  }
-
   //           Γ ⊢ expr: E
   // ---------------------------------- (OPDEF)
   //  Γ ⊢ (def op(params) = expr): E
@@ -238,7 +236,6 @@ export class EffectInferrer implements IRVisitor {
       this.addToResults(def.id, right(this.quantify(e.effect)))
     })
 
-    this.definitionDepth--
     // When exiting top-level definitions, clear the substitutions
     if (this.definitionDepth === 0) {
       this.substitutions = []

quint/src/ir/IRTransformer.ts

@@ -238,14 +238,22 @@ export function transformType(transformer: IRTransformer, type: t.QuintType): t.
       break
 
     case 'sum':
-      if (transformer.enterSumType) {
-        newType = transformer.enterSumType(newType)
-      }
-      if (transformer.exitSumType) {
-        newType = transformer.exitSumType(newType)
+      {
+        if (transformer.enterSumType) {
+          newType = transformer.enterSumType(newType)
+        }
+        // Sum types, transform all types
+        const newFields = transformRow(transformer, newType.fields)
+        if (newFields.kind !== 'row') {
+          throw new Error('Impossible: sum type fields transformed into non-row')
+        }
+        newType.fields = newFields
+
+        if (transformer.exitSumType) {
+          newType = transformer.exitSumType(newType)
+        }
       }
       break
-
     default:
       unreachable(newType)
   }

quint/src/ir/IRVisitor.ts

@@ -22,6 +22,13 @@ import { unreachable } from '../util'
  * Optionally defines functions for each IR component.
  */
 export interface IRVisitor {
+  /* Keeps track of the depth of the current definition, to be updated by the
+   * walk* functions and used by implementations of the interface. Should be
+   * initialized to -1, so if `walkDefinition` is called from a different place
+   * than `walkDeclaration` (which does set this to -1), the increments and
+   * decrements work as expected. */
+  definitionDepth?: number
+
   enterModule?: (_module: ir.QuintModule) => void
   exitModule?: (_module: ir.QuintModule) => void
 
@@ -261,14 +268,23 @@ export function walkDeclaration(visitor: IRVisitor, decl: ir.QuintDeclaration):
     visitor.enterDecl(decl)
   }
 
+  // The standard depth starts at 0, so definitions inside delclarations (i.e.
+  // assume and instance overrides) are not considered top-level
+  visitor.definitionDepth = 0
+
   switch (decl.kind) {
     case 'const':
     case 'var':
-    case 'def':
     case 'typedef':
     case 'assume':
       walkDefinition(visitor, decl)
       break
+    case 'def':
+      // depth will be increased inside `walkDefinition`, so we set it to -1 in
+      // order for it to be 0 there
+      visitor.definitionDepth = -1
+      walkDefinition(visitor, decl)
+      break
     case 'instance':
       if (visitor.enterInstance) {
         visitor.enterInstance(decl)
@@ -312,9 +328,14 @@ export function walkDeclaration(visitor: IRVisitor, decl: ir.QuintDeclaration):
  * @returns nothing, any collected information has to be a state inside the IRVisitor instance.
  */
 export function walkDefinition(visitor: IRVisitor, def: ir.QuintDef): void {
+  if (visitor.definitionDepth !== undefined) {
+    visitor.definitionDepth++
+  }
+
   if (visitor.enterDef) {
     visitor.enterDef(def)
   }
+
   if (ir.isAnnotatedDef(def)) {
     walkType(visitor, def.typeAnnotation)
   } else if (ir.isTypeAlias(def)) {
@@ -372,6 +393,10 @@ export function walkDefinition(visitor: IRVisitor, def: ir.QuintDef): void {
   if (visitor.exitDef) {
     visitor.exitDef(def)
   }
+
+  if (visitor.definitionDepth !== undefined) {
+    visitor.definitionDepth--
+  }
 }
 
 export function walkExpression(visitor: IRVisitor, expr: ir.QuintEx): void {

quint/src/ir/IRprinting.ts

@@ -13,7 +13,7 @@
  */
 
 import { OpQualifier, QuintDeclaration, QuintDef, QuintEx, QuintModule, isAnnotatedDef } from './quintIr'
-import { QuintSumType, QuintType, Row, RowField, isUnitType } from './quintTypes'
+import { ConcreteRow, QuintSumType, QuintType, Row, RowField, isUnitType } from './quintTypes'
 import { TypeScheme } from '../types/base'
 import { typeSchemeToString } from '../types/printing'
 
@@ -210,18 +210,23 @@ export function rowToString(r: Row): string {
  * @returns a string with the pretty printed sum
  */
 export function sumToString(s: QuintSumType): string {
+  return '(' + sumFieldsToString(s.fields) + ')'
+}
+
+function sumFieldsToString(r: ConcreteRow): string {
   return (
-    '(' +
-    s.fields.fields
+    r.fields
       .map((f: RowField) => {
         if (isUnitType(f.fieldType)) {
           return `${f.fieldName}`
         } else {
           return `${f.fieldName}(${typeToString(f.fieldType)})`
         }
       })
-      .join(' | ') +
-    ')'
+      // We are not exposing open rows in sum types currently
+      // So we do not show show row variables.
+      .concat(r.other.kind === 'row' ? [sumFieldsToString(r.other)] : [])
+      .join(' | ')
   )
 }
 

quint/src/names/collector.ts

@@ -54,8 +54,13 @@ export class NameCollector implements IRVisitor {
   definitionsByModule: DefinitionsByModule = new Map()
   errors: QuintError[] = []
   table: LookupTable = new Map()
+
+  // the current depth of operator definitions: top-level defs are depth 0
+  // FIXME(#1279): The walk* functions update this value, but they need to be
+  // initialized to -1 here for that to work on all scenarios.
+  definitionDepth: number = -1
+
   private currentModuleName: string = ''
-  private definitionDepth: number = 0
 
   enterModule(module: QuintModule): void {
     this.currentModuleName = module.name
@@ -87,12 +92,6 @@ export class NameCollector implements IRVisitor {
       // collect only top-level definitions
       this.collectDefinition({ ...def, typeAnnotation: undefined, depth: this.definitionDepth })
     }
-
-    this.definitionDepth++
-  }
-
-  exitOpDef(_def: QuintOpDef): void {
-    this.definitionDepth--
   }
 
   enterTypeDef(def: QuintTypeDef): void {

quint/src/names/resolver.ts

@@ -43,7 +43,11 @@ class NameResolver implements IRVisitor {
   collector: NameCollector
   errors: QuintError[] = []
   table: LookupTable = new Map()
-  private definitionDepth: number = 0
+
+  // the current depth of operator definitions: top-level defs are depth 0
+  // FIXME(#1279): The walk* functions update this value, but they need to be
+  // initialized to -1 here for that to work on all scenarios.
+  definitionDepth: number = -1
 
   constructor() {
     this.collector = new NameCollector()
@@ -73,12 +77,6 @@ class NameResolver implements IRVisitor {
     if (this.definitionDepth > 0) {
       this.collector.collectDefinition({ ...def, depth: this.definitionDepth })
     }
-
-    this.definitionDepth++
-  }
-
-  exitOpDef(_def: QuintOpDef): void {
-    this.definitionDepth--
   }
 
   exitLet(expr: QuintLet): void {

quint/src/runtime/impl/compilerImpl.ts

@@ -161,7 +161,9 @@ export class CompilerVisitor implements IRVisitor {
   // execution listener
   private execListener: ExecutionListener
   // the current depth of operator definitions: top-level defs are depth 0
-  private definitionDepth: number = 0
+  // FIXME(#1279): The walk* functions update this value, but they need to be
+  // initialized to -1 here for that to work on all scenarios.
+  definitionDepth: number = -1
 
   constructor(
     lookupTable: LookupTable,
@@ -230,12 +232,7 @@ export class CompilerVisitor implements IRVisitor {
     return this.errorTracker.runtimeErrors
   }
 
-  enterOpDef(_: ir.QuintOpDef) {
-    this.definitionDepth++
-  }
-
   exitOpDef(opdef: ir.QuintOpDef) {
-    this.definitionDepth--
     // Either a runtime value, or a def, action, etc.
     // All of them are compiled to callables, which may have zero parameters.
     let boundValue = this.compStack.pop()

quint/src/types/simplification.ts

@@ -37,7 +37,7 @@ export function simplify(typeScheme: TypeScheme): TypeScheme {
  * A row like `{ a: int | { b: bool | r } }` becomes
  * `{ a: int, b: bool | r }`.
  *
- * @param row - The tow to be simplified
+ * @param row - The row to be simplified
  *
  * @returns The simplified row
  */

quint/test/names/collector.test.ts

@@ -224,6 +224,26 @@ describe('NameCollector', () => {
         { code: 'QNT404', message: "Name 'test_module::other' not found", reference: 0n, data: {} },
       ])
     })
+
+    it('does not collect nested defs inside assume', () => {
+      const quintModule = buildModuleWithDecls(['assume _ = val foo = 1 { foo }'], undefined, zerog)
+
+      const [errors, definitions] = collect(quintModule)
+
+      assert.isEmpty(errors)
+
+      assert.isFalse(definitions.has('foo'))
+    })
+
+    it('does not collect nested defs inside instances', () => {
+      const quintModule = buildModuleWithDecls(['import test_module(c1 = (val foo = 1 { foo })).*'], undefined, zerog)
+
+      const [errors, definitions] = collect(quintModule)
+
+      assert.isEmpty(errors)
+
+      assert.isFalse(definitions.has('foo'))
+    })
   })
 
   describe('conflicts', () => {

quint/test/types/aliasInliner.test.ts

@@ -22,7 +22,7 @@ function inlineModule(text: string): { modules: QuintModule[]; table: LookupTabl
 }
 
 describe('inlineAliases', () => {
-  it('should inline aliases in a simple module', () => {
+  it('inlines aliases in a simple module', () => {
     const quintModule = `module A {
       type MY_ALIAS = int
       var x: MY_ALIAS
@@ -42,7 +42,7 @@ describe('inlineAliases', () => {
     assert.deepEqual(analysisOutput.types.get(4n)?.type.kind, 'int')
   })
 
-  it('should handle nested aliases', () => {
+  it('handles nested aliases', () => {
     const quintModule = `module A {
       type MY_ALIAS = int
       type MY_OTHER_ALIAS = MY_ALIAS
@@ -59,4 +59,26 @@ describe('inlineAliases', () => {
 
     assert.deepEqual(moduleToString(modules[0]), expectedModule)
   })
+
+  it('handles nested sum types constructors', () => {
+    const quintModule = `module A {
+      type T1 = B | C
+      type T2 = Some(T1) | None
+      var x: T2
+    }`
+
+    const { modules } = inlineModule(quintModule)
+
+    const expectedModule = dedent(`module A {
+                                  |  type T1 = (B({}) | C({}))
+                                  |  val C: (B({}) | C({})) = variant("C", Rec())
+                                  |  type T2 = (Some((B({}) | C({}))) | None({}))
+                                  |  val B: (B({}) | C({})) = variant("B", Rec())
+                                  |  def Some: ((B({}) | C({}))) => (Some((B({}) | C({}))) | None({})) = ((__SomeParam) => variant("Some", __SomeParam))
+                                  |  val None: (Some((B({}) | C({}))) | None({})) = variant("None", Rec())
+                                  |  var x: (Some((B({}) | C({}))) | None({}))
+                                  |}`)
+
+    assert.deepEqual(moduleToString(modules[0]), expectedModule)
+  })
 })