Fix effect substitutions, free names and unification of entities

CHANGELOG.md

@@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Fixed internal bugs in the effect checker that could cause an incorrect effect
+  to be inferred or error to be reported (#1203)
+
 ### Security
 
 ## v0.14.4 -- 2023-10-02

quint/src/effects/base.ts

@@ -18,6 +18,7 @@ import { Substitutions, applySubstitution, applySubstitutionToEntity, compose }
 import { Error, ErrorTree, buildErrorLeaf, buildErrorTree } from '../errorTree'
 import { flattenUnions, simplify } from './simplification'
 import isEqual from 'lodash.isequal'
+import { differenceWith, intersectionWith } from 'lodash'
 
 /* Kinds for concrete effect components */
 export type ComponentKind = 'read' | 'update' | 'temporal'
@@ -323,19 +324,22 @@ export function unifyEntities(va: Entity, vb: Entity): Either<ErrorTree, Substit
     return bindEntity(v1.name, v2).mapLeft(msg => buildErrorLeaf(location, msg))
   } else if (v2.kind === 'variable') {
     return bindEntity(v2.name, v1).mapLeft(msg => buildErrorLeaf(location, msg))
-  } else {
-    if (isEqual(v1, v2)) {
-      return right([])
-    }
-
-    if (v1.kind === 'union' && v2.kind === 'concrete') {
-      return mergeInMany(v1.entities.map(v => unifyEntities(v, v2)))
-        .map(subs => subs.flat())
-        .mapLeft(err => buildErrorTree(location, err))
-    }
-
-    if (v1.kind === 'concrete' && v2.kind === 'union') {
-      return unifyEntities(v2, v1)
+  } else if (isEqual(v1, v2)) {
+    return right([])
+  } else if (v1.kind === 'union' && v2.kind === 'concrete') {
+    return mergeInMany(v1.entities.map(v => unifyEntities(v, v2)))
+      .map(subs => subs.flat())
+      .mapLeft(err => buildErrorTree(location, err))
+  } else if (v1.kind === 'concrete' && v2.kind === 'union') {
+    return unifyEntities(v2, v1)
+  } else if (v1.kind === 'union' && v2.kind === 'union') {
+    const intersection = intersectionWith(v1.entities, v2.entities, isEqual)
+    if (intersection.length > 0) {
+      const s1 = { ...v1, entities: differenceWith(v1.entities, intersection, isEqual) }
+      const s2 = { ...v2, entities: differenceWith(v2.entities, intersection, isEqual) }
+
+      // There was an intersection, try to unify the remaining entities
+      return unifyEntities(s1, s2)
     }
 
     // At least one of the entities is a union
@@ -346,6 +350,8 @@ export function unifyEntities(va: Entity, vb: Entity): Either<ErrorTree, Substit
       message: 'Unification for unions of entities is not implemented',
       children: [],
     })
+  } else {
+    throw new Error(`Impossible: all cases should be covered`)
   }
 }
 

quint/src/effects/inferrer.ts

@@ -31,7 +31,7 @@ import {
   QuintStr,
   QuintVar,
 } from '../ir/quintIr'
-import { Effect, EffectScheme, Signature, effectNames, toScheme, unify } from './base'
+import { Effect, EffectScheme, Signature, effectNames, entityNames, toScheme, unify } from './base'
 import { Substitutions, applySubstitution, compose } from './substitutions'
 import { Error, ErrorTree, buildErrorLeaf, buildErrorTree, errorTreeToString } from '../errorTree'
 import { getSignatures, standardPropagation } from './builtinSignatures'
@@ -82,6 +82,10 @@ export class EffectInferrer implements IRVisitor {
   // Track location descriptions for error tree traces
   private location: string = ''
 
+  // A stack of free effect variables and entity variables for lambda expressions.
+  // Nested lambdas add new entries to the stack, and pop them when exiting.
+  private freeNames: { effectVariables: Set<string>; entityVariables: Set<string> }[] = []
+
   // the current depth of operator definitions: top-level defs are depth 0
   private definitionDepth: number = 0
 
@@ -148,21 +152,25 @@ export class EffectInferrer implements IRVisitor {
       })
     )
 
-    const resultEffect: Effect = { kind: 'variable', name: this.freshVarGenerator.freshVar('e') }
-    const arrowEffect = paramsResult.map(params => {
-      const effect: Effect = {
-        kind: 'arrow',
-        params,
-        result: resultEffect,
-      }
+    const resultEffect: Effect = { kind: 'variable', name: this.freshVarGenerator.freshVar('_e') }
+    const arrowEffect = paramsResult
+      .map(params => {
+        const effect: Effect = {
+          kind: 'arrow',
+          params,
+          result: resultEffect,
+        }
 
-      return effect
-    })
+        return effect
+      })
+      .chain(e => applySubstitution(this.substitutions, e))
 
     this.effectForName(expr.opcode, expr.id, expr.args.length)
       .mapLeft(err => buildErrorTree(this.location, err))
       .chain(signature => {
-        const substitution = arrowEffect.chain(effect => unify(signature, effect))
+        const substitution = arrowEffect.chain(effect =>
+          applySubstitution(this.substitutions, signature).chain(s => unify(s, effect))
+        )
 
         const resultEffectWithSubs = substitution
           .chain(s => compose(this.substitutions, s))
@@ -183,6 +191,9 @@ export class EffectInferrer implements IRVisitor {
                 this.addToResults(id, r)
               })
             )
+            // For every free name we are binding in the substitutions, the names occuring in the value of the
+            // substitution have to become free as well.
+            this.addBindingsToFreeNames(s)
 
             return applySubstitution(s, resultEffect)
           })
@@ -222,10 +233,10 @@ export class EffectInferrer implements IRVisitor {
       // Don't try to infer let if there are errors with the defined expression
       return
     }
-    const result = this.fetchResult(def.expr.id)
 
-    // Set the expression effect as the definition effect for it to be available at the result
-    this.addToResults(def.id, result)
+    this.fetchResult(def.expr.id).map(e => {
+      this.addToResults(def.id, right(this.quantify(e.effect)))
+    })
 
     this.definitionDepth--
     // When exiting top-level definitions, clear the substitutions
@@ -256,10 +267,19 @@ export class EffectInferrer implements IRVisitor {
   // ------------------------------------------------------- (UNDERSCORE)
   //                   Γ ⊢ '_': e
   enterLambda(expr: QuintLambda): void {
+    const lastParamNames = this.currentFreeNames()
+    const paramNames = {
+      effectVariables: new Set(lastParamNames.effectVariables),
+      entityVariables: new Set(lastParamNames.entityVariables),
+    }
+
     expr.params.forEach(p => {
-      const varName = p.name === '_' ? this.freshVarGenerator.freshVar('e') : `e_${p.name}_${p.id}`
+      const varName = p.name === '_' ? this.freshVarGenerator.freshVar('_e') : `e_${p.name}_${p.id}`
+      paramNames.effectVariables.add(varName)
       this.addToResults(p.id, right(toScheme({ kind: 'variable', name: varName })))
     })
+
+    this.freeNames.push(paramNames)
   }
 
   //                  Γ ⊢ expr: E
@@ -269,6 +289,10 @@ export class EffectInferrer implements IRVisitor {
     if (this.errors.size > 0) {
       return
     }
+    // For every free name we are binding in the substitutions, the names occuring in the value of the substitution
+    // have to become free as well.
+    this.addBindingsToFreeNames(this.substitutions)
+
     const exprResult = this.fetchResult(lambda.expr.id)
     const params = mergeInMany(
       lambda.params.map(p => {
@@ -302,21 +326,11 @@ export class EffectInferrer implements IRVisitor {
           this.addToResults(lambda.expr.id, left(error))
         }
 
-        const nonFreeNames = effect.params.reduce(
-          (names, p) => {
-            const { effectVariables, entityVariables } = effectNames(p)
-            return {
-              effectVariables: new Set([...names.effectVariables, ...effectVariables]),
-              entityVariables: new Set([...names.entityVariables, ...entityVariables]),
-            }
-          },
-          { effectVariables: new Set<string>(), entityVariables: new Set<string>() }
-        )
-
-        return { ...nonFreeNames, effect }
+        return toScheme(effect)
       })
 
     this.addToResults(lambda.id, result)
+    this.freeNames.pop()
   }
 
   private addToResults(exprId: bigint, result: Either<Error, EffectScheme>) {
@@ -359,10 +373,10 @@ export class EffectInferrer implements IRVisitor {
 
   private newInstance(effect: EffectScheme): Effect {
     const effectSubs: Substitutions = [...effect.effectVariables].map(name => {
-      return { kind: 'effect', name: name, value: { kind: 'variable', name: this.freshVarGenerator.freshVar('e') } }
+      return { kind: 'effect', name: name, value: { kind: 'variable', name: this.freshVarGenerator.freshVar('_e') } }
     })
     const entitySubs: Substitutions = [...effect.entityVariables].map(name => {
-      return { kind: 'entity', name: name, value: { kind: 'variable', name: this.freshVarGenerator.freshVar('v') } }
+      return { kind: 'entity', name: name, value: { kind: 'variable', name: this.freshVarGenerator.freshVar('_v') } }
     })
 
     const result = compose(effectSubs, entitySubs).chain(s => applySubstitution(s, effect.effect))
@@ -373,4 +387,48 @@ export class EffectInferrer implements IRVisitor {
       return result.value
     }
   }
+
+  private currentFreeNames(): { effectVariables: Set<string>; entityVariables: Set<string> } {
+    return (
+      this.freeNames[this.freeNames.length - 1] ?? {
+        effectVariables: new Set(),
+        entityVariables: new Set(),
+      }
+    )
+  }
+
+  private quantify(effect: Effect): EffectScheme {
+    const freeNames = this.currentFreeNames()
+    const nonFreeNames = {
+      effectVariables: new Set(
+        [...effectNames(effect).effectVariables].filter(name => !freeNames.effectVariables.has(name))
+      ),
+      entityVariables: new Set(
+        [...effectNames(effect).entityVariables].filter(name => !freeNames.entityVariables.has(name))
+      ),
+    }
+    return { ...nonFreeNames, effect: effect }
+  }
+
+  private addBindingsToFreeNames(substitutions: Substitutions) {
+    // Assumes substitutions are topologically sorted, i.e. [ t0 |-> (t1, t2), t1 |-> (t3, t4) ]
+    substitutions.forEach(s => {
+      switch (s.kind) {
+        case 'effect':
+          this.freeNames
+            .filter(free => free.effectVariables.has(s.name))
+            .forEach(free => {
+              const names = effectNames(s.value)
+              names.effectVariables.forEach(v => free.effectVariables.add(v))
+              names.entityVariables.forEach(v => free.entityVariables.add(v))
+            })
+          return
+        case 'entity':
+          this.freeNames
+            .filter(free => free.entityVariables.has(s.name))
+            .forEach(free => entityNames(s.value).forEach(v => free.entityVariables.add(v)))
+          return
+      }
+    })
+  }
 }

quint/src/effects/printing.ts

@@ -13,7 +13,7 @@
  */
 
 import { Effect, EffectComponent, EffectScheme, Entity } from './base'
-import { Substitutions, applySubstitution, compose } from './substitutions'
+import { Substitutions, applySubstitution } from './substitutions'
 
 /**
  * Formats the string representation of  an effect
@@ -65,8 +65,8 @@ export function effectSchemeToString(e: EffectScheme): string {
     return { kind: 'entity', name: name, value: { kind: 'variable', name: `v${i}` } }
   })
 
-  const subs = compose(effectSubs, entitySubs)
-  const effect = subs.chain(s => applySubstitution(s, e.effect))
+  const subs = effectSubs.concat(entitySubs)
+  const effect = applySubstitution(subs, e.effect)
   if (effect.isLeft()) {
     throw new Error('Unexpected error while formatting effect scheme')
   } else {

quint/src/effects/substitutions.ts

@@ -14,9 +14,10 @@
 
 import { Either, mergeInMany, right } from '@sweet-monads/either'
 import { ErrorTree, buildErrorTree } from '../errorTree'
-import { Effect, Entity, unify, unifyEntities } from './base'
+import { Effect, Entity } from './base'
 import { effectToString, substitutionsToString } from './printing'
 import { simplify } from './simplification'
+import { isEqual } from 'lodash'
 
 /*
  * Substitutions can be applied to both effects and entities, replacing
@@ -37,7 +38,7 @@ type Substitution = { kind: 'entity'; name: string; value: Entity } | { kind: 'e
  */
 export function compose(s1: Substitutions, s2: Substitutions): Either<ErrorTree, Substitutions> {
   return applySubstitutionsToSubstitutions(s1, s2)
-    .chain(sa => applySubstitutionsToSubstitutions(sa, s1).map((sb: Substitutions) => sb.concat(sa)))
+    .map((sb: Substitutions) => sb.concat(s1))
     .mapLeft(error =>
       buildErrorTree(`Composing substitutions ${substitutionsToString(s1)} and ${substitutionsToString(s2)}`, error)
     )
@@ -86,7 +87,14 @@ export function applySubstitution(subs: Substitutions, e: Effect): Either<ErrorT
     }
   }
 
-  return result.map(simplify)
+  return result.map(simplify).chain(r => {
+    if (!isEqual(r, e)) {
+      // Keep re-applying the substitutions until the effect is unchanged.
+      // Useful when substitutions have a transitive pattern [ a |-> b, b |-> c ]
+      return applySubstitution(subs, r)
+    }
+    return right(r)
+  })
 }
 
 /**
@@ -130,23 +138,6 @@ function emptyEntity(entity: Entity): boolean {
 function applySubstitutionsToSubstitutions(s1: Substitutions, s2: Substitutions): Either<ErrorTree[], Substitutions> {
   return mergeInMany(
     s2.map((s: Substitution): Either<ErrorTree, Substitutions> => {
-      const sub = s1.find(sub => s.name === sub.name)
-      if (sub) {
-        if (sub.kind === 'effect' && s.kind === 'effect') {
-          return unify(s.value, sub.value).mapLeft(err =>
-            buildErrorTree(`Unifying substitutions with same name: ${s.name}`, err)
-          )
-        } else if (sub.kind === 'entity' && s.kind === 'entity') {
-          return unifyEntities(s.value, sub.value).mapLeft(err =>
-            buildErrorTree(`Unifying substitutions with same name: ${s.name}`, err)
-          )
-        } else {
-          throw new Error(
-            `Substitutions with same name (${s.name}) but incompatible kinds: ${substitutionsToString([sub, s])}`
-          )
-        }
-      }
-
       switch (s.kind) {
         case 'effect':
           return applySubstitution(s1, s.value).map(v => [{ kind: s.kind, name: s.name, value: v }])

quint/test/effects/base.test.ts

@@ -284,6 +284,17 @@ describe('unify', () => {
       )
     })
 
+    it('simplifies unions of entities before giving up on unifying them', () => {
+      const e1 = parseEffectOrThrow("Read[r1, r2, 'x']")
+      const e2 = parseEffectOrThrow("Read[r1, 'x']")
+
+      const result = unify(e1, e2)
+      assert.isTrue(result.isRight())
+      result.map(r =>
+        assert.sameDeepMembers(r, [{ kind: 'entity', name: 'r2', value: { kind: 'concrete', stateVariables: [] } }])
+      )
+    })
+
     it('returns error with effect with incompatible entity variables', () => {
       const e1 = parseEffectOrThrow('(Read[r1] & Update[u], Read[r2] & Update[u]) => Read[r1, r2] & Update[u]')
       const e2 = parseEffectOrThrow("(Read['y'] & Update['x'], Read['z'] & Update['x']) => Read['y'] & Update[u]")