Merge pull request #1359 from informalsystems/1356/effect-cyclical-binding-bug

Remove erroneous occurs check from "effect entity" unfication

Author: Shon Feder

CHANGELOG.md

@@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Erroneous effect checking failure resulting from invalid occurs check. This
+  error prevented some valid specs from being simulated or verified (#1359).
+
 ### Security
 
 ## v0.18.2 -- 2024-01-26

quint/src/cliCommands.ts

@@ -255,12 +255,12 @@ export function mkErrorMessage(sourceMap: SourceMap): (_: QuintError) => ErrorMe
  */
 export async function typecheck(parsed: ParsedStage): Promise<CLIProcedure<TypecheckedStage>> {
   const { table, modules, sourceMap } = parsed
-  const typechecking = { ...parsed, stage: 'typechecking' as stage }
 
   const [errorMap, result] = analyzeModules(table, modules)
 
+  const typechecking = { ...parsed, ...result, stage: 'typechecking' as stage }
   if (errorMap.length === 0) {
-    return right({ ...typechecking, ...result })
+    return right(typechecking)
   } else {
     const errors = errorMap.map(mkErrorMessage(sourceMap))
     return cliErr('typechecking failed', { ...typechecking, errors })

quint/src/effects/base.ts

@@ -81,11 +81,11 @@ export interface StateVariable {
  * entity variable or a combination of other entities.
  */
 export type Entity =
-  /* A list of state variables */
+  /* A set of state variables, represented as a list */
   | { kind: 'concrete'; stateVariables: StateVariable[] }
-  /* A variable representing some entity */
+  /* A variable representing some set of entities */
   | { kind: 'variable'; name: string; reference?: bigint }
-  /* A combination of entities */
+  /* The union of sets of entities, represented as a list */
   | { kind: 'union'; entities: Entity[] }
 
 /*
@@ -177,11 +177,36 @@ function bindEffect(name: string, effect: Effect): Either<string, Substitutions>
   }
 }
 
-function bindEntity(name: string, entity: Entity): Either<string, Substitutions> {
-  if (entityNames(entity).includes(name)) {
-    return left(`Can't bind ${name} to ${entityToString(entity)}: cyclical binding`)
-  } else {
-    return right([{ kind: 'entity', name, value: entity }])
+function bindEntity(name: string, entity: Entity): Substitutions {
+  switch (entity.kind) {
+    case 'concrete':
+    case 'variable':
+      return [{ kind: 'entity', name, value: entity }]
+    case 'union':
+      if (entityNames(entity).includes(name)) {
+        // An entity variable (which always stands for a set of state variables)
+        // unifies with the union of n sets of entities that may include itself,
+        // iff it unifies with each set.
+        //
+        // I.e.:
+        //
+        //   (v1 =.= v1 ∪ ... ∪ vn) <=> (v1 =.= ... =.= vn)
+        //
+        // We call this function recursively because, in the general case,
+        // occurrences of `v1` may be nested, as in:
+        //
+        //    v1 =.= v1 ∪ (v2 ∪ (v3 ∪ v1)) ∪ v4
+        //
+        // In practice, we are flattening unions before we call this function,
+        // but solving the general case ensures we preserve correct behavior
+        // even if this function is used on its own, without incurring any
+        // notable overhead when `entities` is already flat.
+        return entity.entities.flatMap(e => bindEntity(name, e))
+      } else {
+        // Otherwise, the variable may be bound to the union of the entities
+        // without qualification.
+        return [{ kind: 'entity', name, value: entity }]
+      }
   }
 }
 
@@ -321,9 +346,9 @@ export function unifyEntities(va: Entity, vb: Entity): Either<ErrorTree, Substit
   } else if (v1.kind === 'variable' && v2.kind === 'variable' && v1.name === v2.name) {
     return right([])
   } else if (v1.kind === 'variable') {
-    return bindEntity(v1.name, v2).mapLeft(msg => buildErrorLeaf(location, msg))
+    return right(bindEntity(v1.name, v2))
   } else if (v2.kind === 'variable') {
-    return bindEntity(v2.name, v1).mapLeft(msg => buildErrorLeaf(location, msg))
+    return right(bindEntity(v2.name, v1))
   } else if (isEqual(v1, v2)) {
     return right([])
   } else if (v1.kind === 'union' && v2.kind === 'concrete') {

quint/src/effects/inferrer.ts

@@ -37,7 +37,7 @@ import { Error, ErrorTree, buildErrorLeaf, buildErrorTree, errorTreeToString } f
 import { getSignatures, standardPropagation } from './builtinSignatures'
 import { FreshVarGenerator } from '../FreshVarGenerator'
 import { effectToString } from './printing'
-import { zip } from 'lodash'
+import { zip } from '../util'
 import { addNamespaces } from './namespaces'
 
 export type EffectInferenceResult = [Map<bigint, ErrorTree>, Map<bigint, EffectScheme>]
@@ -185,11 +185,6 @@ export class EffectInferrer implements IRVisitor {
                 effects,
                 expr.args.map(a => a.id)
               ).forEach(([effect, id]) => {
-                if (!effect || !id) {
-                  // Impossible: effects and expr.args are the same length
-                  throw new Error(`Expected ${expr.args.length} effects, but got ${effects.length}`)
-                }
-
                 const r = applySubstitution(s, effect).map(toScheme)
                 this.addToResults(id, r)
               })

quint/test/effects/base.test.ts

@@ -375,48 +375,39 @@ describe('unify', () => {
       assert.isTrue(result.isLeft())
     })
 
-    it('returs error when entity names are cyclical', () => {
-      const e1 = parseEffectOrThrow('Read[v1]')
-      const e2 = parseEffectOrThrow('Read[v1, v2]')
-
-      const result = unify(e1, e2)
-
-      result.mapLeft(e =>
-        assert.deepEqual(e, {
-          location: 'Trying to unify Read[v1] and Read[v1, v2]',
-          children: [
-            {
-              location: 'Trying to unify entities [v1] and [v1, v2]',
-              message: "Can't bind v1 to v1, v2: cyclical binding",
-              children: [],
-            },
-          ],
-        })
-      )
-
-      assert.isTrue(result.isLeft())
-    })
-
-    it('returs error when entity names are cyclical in other way', () => {
-      const e1 = parseEffectOrThrow('Temporal[v1, v2]')
-      const e2 = parseEffectOrThrow('Temporal[v1]')
-
-      const result = unify(e1, e2)
-
-      result.mapLeft(e =>
-        assert.deepEqual(e, {
-          location: 'Trying to unify Temporal[v1, v2] and Temporal[v1]',
-          children: [
-            {
-              location: 'Trying to unify entities [v1, v2] and [v1]',
-              message: "Can't bind v1 to v1, v2: cyclical binding",
-              children: [],
-            },
-          ],
-        })
-      )
-
-      assert.isTrue(result.isLeft())
+    it('can unify entities when a single variable in the lhs appears in a union on the rhs', () => {
+      // E.g., given the unification problem
+      //
+      //    v1 =.= v1 ∪ v2
+      //
+      // We should be able to form a valid substitution iff v1 =.= v2, since
+      // this then simplifies to
+      //
+      //   v1 =.= v1 =.= v2
+      //
+      // NOTE: This test was inverted after an incorrect occurs check was
+      // causing erroneous effect checking failures, as reported in
+      // https://github.com/informalsystems/quint/issues/1356
+      //
+      // Occurs checks are called for to prevent the attempt to unify a free
+      // variable with a term that includes that variable as a subterm. E.g., `X
+      // =.= foo(a, X)`, which can never be resolved into a ground term.
+      // However, despite appearances, the unification of so called "entity
+      // unions", as in the example above is not such a case. Each "entity
+      // variable" stands for a set of possible state variables. As such, the
+      // unification problem above can be expanded to
+      //
+      //     v1 ∪ {} =.= v1 ∪ v2 ∪ {}
+      //
+      // Which helps make clear why the unification succeeds iff v1 =.= v2.
+      const read1 = parseEffectOrThrow('Read[v1]')
+      const read2 = parseEffectOrThrow('Read[v1, v2]')
+      assert.isTrue(unify(read1, read2).isRight())
+
+      // Check the symmetrical case.
+      const temporal1 = parseEffectOrThrow('Temporal[v1, v2]')
+      const temporal2 = parseEffectOrThrow('Temporal[v1]')
+      assert.isTrue(unify(temporal1, temporal2).isRight())
     })
   })
 })

quint/test/effects/inferrer.test.ts

@@ -207,6 +207,19 @@ describe('inferEffects', () => {
     assert.deepEqual(effectForDef(defs, effects, 'CoolAction'), expectedEffect)
   })
 
+  it('avoids invalid cyclical binding error (regression on #1356)', () => {
+    const defs = [
+      `pure def foo(s: int, g: int => int): int = {
+        val r = if (true) s else g(s)
+        g(r)
+      }`,
+    ]
+
+    const [errors, _] = inferEffectsForDefs(defs)
+
+    assert.isEmpty(errors, `Should find no errors, found: ${[...errors.values()].map(errorTreeToString)}`)
+  })
+
   it('returns error when operator signature is not unifiable with args', () => {
     const defs = [`def a = S.map(p => x' = p)`]