Checks for misuse of nondet and oneOf

CHANGELOG.md

@@ -8,6 +8,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## UNRELEASED
 
 ### Added
+
+- Added static analysis checks to ensure proper usage of `nondet` and `oneOf` (#1431).
+
 ### Changed
 ### Deprecated
 ### Removed

examples/README.md

@@ -66,7 +66,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: | :white_check_mark: |
 | [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: | :white_check_mark: | :x: |
+| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/tendermint/Tendermint.qnt](./cosmos/tendermint/Tendermint.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/tendermint/TendermintModels.qnt](./cosmos/tendermint/TendermintModels.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/cosmos/ics20/ics20.qnt

@@ -611,7 +611,7 @@ module ics20Test {
       // Check that there is a single incoming acknowledgement on chain A,
       // that indicates failure.
       assert(chainStates.get("B").inAcknowledgements.size() == 1),
-      val ack = chainStates.get("B").inAcknowledgements.oneOf()
+      nondet ack = chainStates.get("B").inAcknowledgements.oneOf()
       assert(ack.success == false and ack.errorMessage == "transfer coins failed"),
 
       // Process the acknowledgement on chain A; this triggers step 3.6 above.

examples/cosmos/lightclient/Lightclient.qnt

@@ -199,7 +199,7 @@ module Lightclient {
             // Record that one more probe has been done (for complexity and model checking)
             nprobes' = nprobes + 1,
             // Verify the current block
-            nondet verdict = API::ValidAndVerified(latestVerified, current, true)
+            val verdict = API::ValidAndVerified(latestVerified, current, true)
             all {
                 MonitorTransition(latestVerified, current, API::localClock, verdict),
                 // Decide whether/how to continue

quint/src/effects/NondetChecker.ts

@@ -0,0 +1,108 @@
+/* ----------------------------------------------------------------------------------
+ * Copyright 2024 Informal Systems
+ * Licensed under the Apache License, Version 2.0.
+ * See LICENSE in the project root for license information.
+ * --------------------------------------------------------------------------------- */
+
+/**
+ * Checking for the misuse of 'nondet' and 'oneOf'. Necessary to ensure they are
+ * compatible with the exists operator from TLA+.
+ *
+ * @author Gabriela Moreira
+ *
+ * @module
+ */
+
+import { IRVisitor, walkDeclaration } from '../ir/IRVisitor'
+import { OpQualifier, QuintApp, QuintDeclaration, QuintLet, QuintOpDef } from '../ir/quintIr'
+import { LookupTable } from '../names/base'
+import { QuintError } from '../quintError'
+import { TypeScheme } from '../types/base'
+import { typeSchemeToString } from '../types/printing'
+
+export class NondetChecker implements IRVisitor {
+  private table: LookupTable
+  private types: Map<bigint, TypeScheme> = new Map()
+  private lastDefQualifier: OpQualifier = 'def'
+
+  private errors: QuintError[] = []
+
+  constructor(table: LookupTable) {
+    this.table = table
+  }
+
+  /**
+   * Checks declarations for misuse of 'nondet' and 'oneOf'.
+   *
+   * @param types - the types of the declarations
+   * @param declarations - the declarations to check
+   *
+   * @returns a list of errors (empty if no errors are found)
+   */
+  checkNondets(types: Map<bigint, TypeScheme>, declarations: QuintDeclaration[]): QuintError[] {
+    this.types = types
+
+    declarations.forEach(d => walkDeclaration(this, d))
+    return this.errors
+  }
+
+  enterOpDef(def: QuintOpDef) {
+    this.lastDefQualifier = def.qualifier
+
+    if (def.qualifier === 'nondet' && this.table.get(def.id)!.depth === 0) {
+      this.errors.push({
+        code: 'QNT206',
+        message: `'nondet' can only be used inside actions, not at the top level`,
+        reference: def.id,
+        data: {},
+      })
+    }
+  }
+
+  enterApp(app: QuintApp) {
+    if (app.opcode !== 'oneOf') {
+      // nothing to check
+      return
+    }
+
+    if (this.lastDefQualifier !== 'nondet') {
+      this.errors.push({
+        code: 'QNT203',
+        message: `'oneOf' must be used inside a nondet definition`,
+        reference: app.id,
+        data: {},
+      })
+      return
+    }
+  }
+
+  enterLet(expr: QuintLet) {
+    if (expr.opdef.qualifier !== 'nondet') {
+      return
+    }
+
+    // body of nondet must be an application of oneOf
+    const body = expr.opdef.expr
+    if (body.kind !== 'app' || body.opcode !== 'oneOf') {
+      this.errors.push({
+        code: 'QNT204',
+        message: `'oneOf' must be the outermost expression in a nondet definition`,
+        reference: body.id,
+        data: {},
+      })
+    }
+
+    // if the opdef is nondet, the return type must be bool
+    const expressionType = this.types.get(expr.expr.id)!
+    if (expressionType.type.kind !== 'bool') {
+      this.errors.push({
+        code: 'QNT205',
+        message: `nondet bindings can only be used with boolean expressions, but expression has type: ${typeSchemeToString(
+          expressionType
+        )}`,
+        reference: expr.id,
+        data: {},
+      })
+    }
+  }
+}

quint/src/generated/Quint.g4

@@ -31,11 +31,6 @@ declaration : 'const' qualId ':' type                     # const
             | typeDef                                     # typeDefs
             | importMod                                   # importDef
             | exportMod                                   # exportDef
-            // https://github.com/informalsystems/quint/issues/378
-            //| 'nondet' qualId (':' type)? '=' expr ';'? expr {
-            //  const m = "QNT007: 'nondet' is only allowed inside actions"
-            //  this.notifyErrorListeners(m)
-            //}                                                 # nondetError
             ;
 
 // An operator definition.
@@ -76,15 +71,14 @@ sumTypeDefinition : '|'? typeSumVariant ('|' typeSumVariant)* ;
 // E.g., `A(t)` or `A`.
 typeSumVariant : sumLabel=simpleId["variant label"] ('(' type ')')? ;
 
-nondetOperDef : 'nondet' qualId (':' type)? '=' expr ';'?;
-
 qualifier : 'val'
           | 'def'
           | 'pure' 'val'
           | 'pure' 'def'
           | 'action'
           | 'run'
           | 'temporal'
+          | 'nondet'
           ;
 
 importMod : 'import' name '.' identOrStar ('from' fromSource)?
@@ -188,7 +182,6 @@ expr:           // apply a built-in operator via the dot notation
         |       '[' (expr (',' expr)*)? ','? ']'                    # list
         |       'if' '(' expr ')' expr 'else' expr                  # ifElse
         |       operDef expr                                        # letIn
-        |       nondetOperDef expr                                  # nondet
         |       '(' expr ')'                                        # paren
         |       '{' expr '}'                                        # braces
         ;