Merge remote-tracking branch 'origin/main' into gabriela/definition-u…

…pdate-procedure-extraction

CONTRIBUTING.md

@@ -82,6 +82,97 @@ FP code in this language, so we keep the balance between readability and
 FPness.  When the idiomatic JavaScript code is shorter and clearer than
 equivalent FP code, we write the idiomatic JavaScript code.
 
+### Ensure exhaustive matches
+
+The type system should help us keep the code base maintainable. But when
+`switch` statements and conditionals are used purely for side effects, we can
+lose the advantage of exhaustivness checking. Here's an example:
+
+Assume we have a type `T`
+
+```typescript
+type T = 'a' | 'b' | 'c'
+```
+
+We should structure our program such that
+
+- we can be sure every alternative is considered (as needed), and
+- whenever a new alternative is added to this type, the type system will warn us
+  about all the places we need to account for the new kind of data.
+
+If we use `T` with a `switch` or `if`/`then` statement that *returns values*,
+this indispensable help is ensured. E.g., if we try to write the following:
+
+```typescript
+function f(x:T): Number {
+  switch x {
+    case 'a':
+      return 0
+    case 'b':
+      return 1
+  }
+}
+```
+
+we will end up with a type error, because the annotation on `f` promises it will
+return a `Number`, but it might in fact return `undefined` since we are not
+handling `c`.
+
+However, if we are only using side effects in the switch, we lose this check!
+
+```typescript
+function f(x:T): Number {
+  let n = -1
+  switch x {
+    case 'a':
+      n = 0
+      break
+    case 'b':
+      n = 1
+      break
+  }
+  return ret
+}
+```
+
+Now the typechecker sees that we will be returning a number no matter what
+happens, even if none of our cases are hit, and we will not get a warning on the
+omitted check for `c`, or for any other data added to this type in the future.
+
+Now, sometimes this kind of catch-all default is what we want, but we should be
+very careful in relying on it, because it creates blind spots. As a rule, we
+should only allow cath-all defaults when the computation we are performing
+**must** be invariant under any expansion of the domain we are computing from.
+
+For all other cases, we can avoid these typechecking blind spots by following two guidelines:
+
+1. Prefer passing data by returning values whenever, and avoid needless mutable
+   assignments.
+2. When switches need to be used for side effects, provide a default that
+   calls `unreachable` on the expression to ensure all cases are handled:
+
+   ```typescript
+   import { unreachable } from './util'
+
+   function f(x:T): Number {
+     let n = -1
+     switch x {
+       case 'a':
+         n = 0
+         break
+       case 'b':
+         n = 1
+         break
+       default:
+         unreachable(x)
+     }
+     return ret
+   }
+   ```
+
+   Now the type checker will warn us that we aren't accounting for `c` (or any
+   additional alternatives added down the line).
+
 ### Using Either
 
 TODO
@@ -186,7 +277,7 @@ executable and the VSCode plugin.
 
   This will trigger the release and publication of the package to npm and
   GitHub.
-  
+
 ### VSCode Plugin
 
 #### Prerequisites
@@ -207,10 +298,9 @@ executable and the VSCode plugin.
   - Run `vsce publish`
     - requires access to https://dev.azure.com/informalsystems/
     - which allows creating the required PAT (see
-      https://code.visualstudio.com/api/working-with-extensions/publishing-extension) 
+      https://code.visualstudio.com/api/working-with-extensions/publishing-extension)
   - Use the web interface
     - Run `vsce package` to produce a the `.visx` archive
     - Navigate to
       https://marketplace.visualstudio.com/manage/publishers/informal, and click
       the `...` visible when hovering over `Quint` to upload the archive.
-

examples/.scripts/run-example.sh

@@ -55,7 +55,7 @@ result () {
       printf "<sup>https://github.com/informalsystems/quint/pull/1023</sup>"
     elif [[ "$file" == "cosmwasm/zero-to-hero/vote.qnt" && "$cmd" == "verify" ]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/693</sup>"
-    elif [[ "$file" == "language-features/option.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" ) ]] ; then
+    elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify"  ]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
     elif [[ "$file" == "language-features/tuples.qnt" && "$cmd" == "verify" ]] ; then
       printf "<sup>https://github.com/informalsystems/apalache/issues/2670</sup>"

examples/README.md

@@ -76,7 +76,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: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :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/244</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: | :x:<sup>https://github.com/informalsystems/apalache/issues/2670</sup> |

examples/spells/basicSpells.qnt

@@ -123,4 +123,21 @@ module basicSpells {
     assert(Map(3 -> 4, 7 -> 8) == Map(3 -> 4, 5 -> 6, 7 -> 8).mapRemove(5)),
     assert(Map() == Map().mapRemove(3)),
   }
-}
+
+  /// Removes a set of map entries.
+  ///
+  /// - @param __map a map to remove entries from
+  /// - @param __keys a set of keys for entries to remove from the map
+  /// - @returns a new map that contains all entries of __map
+  ///          that do not have a key in __keys
+  pure def mapRemoveAll(__map: a -> b, __keys: Set[a]): a -> b = {
+      __map.keys().exclude(__keys).mapBy(__k => __map.get(__k))
+  }
+
+  run mapRemoveAllTest =
+      val m = Map(3 -> 4, 5 -> 6, 7 -> 8)
+      all {
+          assert(m.mapRemoveAll(Set(5, 7)) == Map(3 -> 4)),
+          assert(m.mapRemoveAll(Set(5, 99999)) == Map(3 -> 4, 7 -> 8)),
+      }
+}

quint/src/cliCommands.ts

@@ -513,34 +513,21 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
       }
     }
 
-    // If nothing found, return a success. Otherwise, return an error.
-    let msg
-    switch (result.status) {
-      case 'ok':
-        return right({
-          ...simulator,
-          status: result.status,
-          trace: result.states,
-        })
-
-      case 'violation':
-        msg = 'Invariant violated'
-        break
-
-      case 'failure':
-        msg = 'Runtime error'
-        break
-
-      default:
-        msg = 'Unknown error'
+    if (result.status === 'ok') {
+      return right({
+        ...simulator,
+        status: result.status,
+        trace: result.states,
+      })
+    } else {
+      const msg = result.status === 'violation' ? 'Invariant violated' : 'Runtime error'
+      return cliErr(msg, {
+        ...simulator,
+        status: result.status,
+        trace: result.states,
+        errors: result.errors,
+      })
     }
-
-    return cliErr(msg, {
-      ...simulator,
-      status: result.status,
-      trace: result.states,
-      errors: result.errors,
-    })
   }
 }
 

quint/src/effects/EffectVisitor.ts

@@ -13,6 +13,7 @@
  * @module
  */
 
+import { unreachable } from '../util'
 import { ArrowEffect, ConcreteEffect, Effect, EffectVariable } from './base'
 
 /**
@@ -58,17 +59,21 @@ export function walkEffect(visitor: EffectVisitor, effect: Effect): void {
       }
       break
     }
-    case 'arrow': {
-      if (visitor.enterArrow) {
-        visitor.enterArrow(effect)
-      }
+    case 'arrow':
+      {
+        if (visitor.enterArrow) {
+          visitor.enterArrow(effect)
+        }
 
-      effect.params.forEach(e => walkEffect(visitor, e))
-      walkEffect(visitor, effect.result)
+        effect.params.forEach(e => walkEffect(visitor, e))
+        walkEffect(visitor, effect.result)
 
-      if (visitor.exitArrow) {
-        visitor.exitArrow(effect)
+        if (visitor.exitArrow) {
+          visitor.exitArrow(effect)
+        }
       }
-    }
+      break
+    default:
+      unreachable(effect)
   }
 }

quint/src/effects/builtinSignatures.ts

@@ -15,6 +15,7 @@
 import { ComponentKind, Effect, EffectComponent, EffectScheme, Entity, Signature, effectNames, toScheme } from './base'
 import { parseEffectOrThrow } from './parser'
 import { range, times } from 'lodash'
+import { QuintBuiltinOpcode } from '../ir/quintIr'
 
 export function getSignatures(): Map<string, Signature> {
   return new Map<string, Signature>(fixedAritySignatures.concat(multipleAritySignatures))
@@ -227,7 +228,7 @@ const otherOperators = [
   },
 ]
 
-const multipleAritySignatures: [string, Signature][] = [
+const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
   ['List', standardPropagation],
   ['Set', standardPropagation],
   ['Map', standardPropagation],

quint/src/effects/modeChecker.ts

@@ -18,6 +18,7 @@ import { qualifierToString } from '../ir/IRprinting'
 import { IRVisitor, walkDefinition } from '../ir/IRVisitor'
 import { QuintError } from '../quintError'
 import { OpQualifier, QuintDef, QuintInstance, QuintOpDef } from '../ir/quintIr'
+import { unreachable } from '../util'
 import { ArrowEffect, ComponentKind, EffectScheme, Entity, entityNames, stateVariables } from './base'
 import { effectToString, entityToString } from './printing'
 
@@ -247,26 +248,34 @@ function paramEntitiesByEffect(effect: ArrowEffect): Map<ComponentKind, Entity[]
 
   effect.params.forEach(p => {
     switch (p.kind) {
-      case 'concrete': {
-        p.components.forEach(c => {
-          const existing = entitiesByComponentKind.get(c.kind) || []
-          entitiesByComponentKind.set(c.kind, concatEntity(existing, c.entity))
-        })
-        break
-      }
-      case 'arrow': {
-        const nested = paramEntitiesByEffect(p)
-        nested.forEach((entities, kind) => {
-          const existing = entitiesByComponentKind.get(kind) || []
-          entitiesByComponentKind.set(kind, entities.reduce(concatEntity, existing))
-        })
-        if (p.result.kind === 'concrete') {
-          p.result.components.forEach(c => {
+      case 'concrete':
+        {
+          p.components.forEach(c => {
             const existing = entitiesByComponentKind.get(c.kind) || []
             entitiesByComponentKind.set(c.kind, concatEntity(existing, c.entity))
           })
         }
-      }
+        break
+      case 'arrow':
+        {
+          const nested = paramEntitiesByEffect(p)
+          nested.forEach((entities, kind) => {
+            const existing = entitiesByComponentKind.get(kind) || []
+            entitiesByComponentKind.set(kind, entities.reduce(concatEntity, existing))
+          })
+          if (p.result.kind === 'concrete') {
+            p.result.components.forEach(c => {
+              const existing = entitiesByComponentKind.get(c.kind) || []
+              entitiesByComponentKind.set(c.kind, concatEntity(existing, c.entity))
+            })
+          }
+        }
+        break
+      case 'variable':
+        // Nothing to gather
+        break
+      default:
+        unreachable(p)
     }
   })
 

quint/src/effects/simplification.ts

@@ -13,6 +13,7 @@
  */
 
 import isEqual from 'lodash.isequal'
+import { unreachable } from '../util'
 import { ConcreteEffect, Effect, Entity, StateVariable } from './base'
 
 /**
@@ -57,35 +58,35 @@ export function simplify(e: Effect): Effect {
  *          Otherwise, the entity without change.
  */
 export function flattenUnions(entity: Entity): Entity {
-  switch (entity.kind) {
-    case 'union': {
-      const unionEntities: Entity[] = []
-      const vars: StateVariable[] = []
-      const flattenEntities = entity.entities.map(v => flattenUnions(v))
-      flattenEntities.forEach(v => {
-        switch (v.kind) {
-          case 'variable':
-            unionEntities.push(v)
-            break
-          case 'concrete':
-            vars.push(...v.stateVariables)
-            break
-          case 'union':
-            unionEntities.push(...v.entities)
-            break
-        }
-      })
-
-      if (unionEntities.length > 0) {
-        const entities =
-          vars.length > 0 ? unionEntities.concat({ kind: 'concrete', stateVariables: vars }) : unionEntities
-        return entities.length > 1 ? { kind: 'union', entities: entities } : entities[0]
-      } else {
-        return { kind: 'concrete', stateVariables: vars }
+  if (entity.kind == 'union') {
+    const unionEntities: Entity[] = []
+    const vars: StateVariable[] = []
+    const flattenEntities = entity.entities.map(v => flattenUnions(v))
+    flattenEntities.map(v => {
+      switch (v.kind) {
+        case 'variable':
+          unionEntities.push(v)
+          break
+        case 'concrete':
+          vars.push(...v.stateVariables)
+          break
+        case 'union':
+          unionEntities.push(...v.entities)
+          break
+        default:
+          unreachable(v)
       }
+    })
+
+    if (unionEntities.length > 0) {
+      const entities =
+        vars.length > 0 ? unionEntities.concat({ kind: 'concrete', stateVariables: vars }) : unionEntities
+      return entities.length > 1 ? { kind: 'union', entities: entities } : entities[0]
+    } else {
+      return { kind: 'concrete', stateVariables: vars }
     }
-    default:
-      return entity
+  } else {
+    return entity
   }
 }