ForAllSuchThatDecider (#376)

* Implemented ForAllSuchThatDecider and associated tests
* Removed `checkDecision` from `Decider` interface in favor of always reading from cache unless otherwise indicated
* Updating other `Deciders` and tests according to the new interface

packages/core/src/app/ovm/deciders/and-decider.ts

@@ -18,11 +18,16 @@ export interface AndDeciderInput {
 export class AndDecider implements Decider {
   public async decide(
     input: AndDeciderInput,
-    witness: undefined
+    witness?: undefined,
+    noCache?: boolean
   ): Promise<Decision> {
     const [leftDecision, rightDecision] = await Promise.all([
-      input.left.decider.decide(input.left.input, input.leftWitness),
-      input.right.decider.decide(input.right.input, input.rightWitness),
+      input.left.decider.decide(input.left.input, input.leftWitness, noCache),
+      input.right.decider.decide(
+        input.right.input,
+        input.rightWitness,
+        noCache
+      ),
     ])
 
     if (!leftDecision.outcome) {
@@ -43,10 +48,6 @@ export class AndDecider implements Decider {
     return this.getDecision(input, { outcome: true, justification })
   }
 
-  public async checkDecision(input: AndDeciderInput): Promise<Decision> {
-    return this.decide(input, undefined)
-  }
-
   /**
    * Gets the Decision that results from invocation of the And decider, which simply
    * returns true if both sub-Decisions returned true.

packages/core/src/app/ovm/deciders/for-all-such-that-decider.ts

@@ -0,0 +1,117 @@
+import {
+  Decider,
+  Decision,
+  ImplicationProofItem,
+  Property,
+  PropertyFactory,
+  Quantifier,
+  QuantifierResult,
+  WitnessFactory,
+} from '../../../types/ovm'
+import { CannotDecideError } from './utils'
+
+export interface ForAllSuchThatInput {
+  quantifier: Quantifier
+  quantifierParameters: any
+  propertyFactory: PropertyFactory
+  witnessFactory: WitnessFactory | undefined
+}
+
+/**
+ * Decider that decides true iff the provided quantifier quantifies all results and they all evaluate to true.
+ * If any evaluates to false, it will decide false. Otherwise, it is undecidable.
+ */
+export class ForAllSuchThatDecider implements Decider {
+  public async decide(
+    input: ForAllSuchThatInput,
+    _witness?: undefined,
+    noCache?: boolean
+  ): Promise<Decision> {
+    const quantifierResult: QuantifierResult = await input.quantifier.getAllQuantified(
+      input.quantifierParameters
+    )
+
+    let anyUndecided: boolean = false
+    let falseDecision: Decision
+    const trueDecisions: Decision[] = []
+    for (const res of quantifierResult.results) {
+      const prop: Property = input.propertyFactory(res)
+      const witness: any = !!input.witnessFactory
+        ? input.witnessFactory(res)
+        : undefined
+      try {
+        const decision: Decision = await prop.decider.decide(
+          prop.input,
+          witness,
+          noCache
+        )
+        if (!decision.outcome) {
+          falseDecision = decision
+          break
+        }
+        trueDecisions.push(decision)
+      } catch (e) {
+        if (e instanceof CannotDecideError) {
+          anyUndecided = true
+        } else {
+          throw e
+        }
+      }
+    }
+
+    return this.getDecision(
+      input,
+      falseDecision,
+      trueDecisions,
+      anyUndecided || !quantifierResult.allResultsQuantified
+    )
+  }
+
+  private async checkDecision(input: ForAllSuchThatInput): Promise<Decision> {
+    return this.decide(input, undefined)
+  }
+
+  /**
+   * Gets the Decision that results from invocation of the ForAllSuchThat Decider.
+   *
+   * @param input The input that led to the Decision
+   * @param falseDecision A [possibly undefined] Decision failing this Decider to be used as proof
+   * @param trueDecisions An array of true Decisions to use as justification for this Decider returning True.
+   * @param undecided Whether or not some results of this Decider are undecided
+   * @returns The Decision.
+   */
+  private getDecision(
+    input: ForAllSuchThatInput,
+    falseDecision: Decision,
+    trueDecisions: Decision[],
+    undecided: boolean
+  ): Decision {
+    if (!falseDecision && undecided) {
+      throw new CannotDecideError(
+        'Cannot decide ForAllSuchThat due to undecided Decision or not all results being quantified.'
+      )
+    }
+    const justification: ImplicationProofItem[] = [
+      {
+        implication: {
+          decider: this,
+          input,
+        },
+        implicationWitness: undefined,
+      },
+    ]
+
+    if (!!falseDecision) {
+      justification.push(...falseDecision.justification)
+    } else {
+      for (const decision of trueDecisions) {
+        justification.push(...decision.justification)
+      }
+    }
+
+    return {
+      outcome: !falseDecision,
+      justification,
+    }
+  }
+}

packages/core/src/app/ovm/deciders/hash-preimage-existence-decider.ts

@@ -25,15 +25,20 @@ export class HashPreimageExistenceDecider extends KeyValueStoreDecider {
     this.hashFunction = hashFunction
   }
 
-  public async decide(
+  protected async makeDecision(
     input: HashInput,
     witness: PreimageWitness
   ): Promise<Decision> {
-    const outcome = this.hashFunction(witness.preimage).equals(input.hash)
+    const outcome =
+      !!witness && this.hashFunction(witness.preimage).equals(input.hash)
 
     if (!outcome) {
       throw new CannotDecideError(
-        `Preimage [${witness.preimage}] does not match hash [${input.hash}], so we cannot decide whether a preimage exists for the hash.`
+        `Witness [${JSON.stringify(
+          witness
+        )}] does not match hash [${JSON.stringify(
+          input
+        )}], so we cannot decide whether a preimage exists for the hash.`
       )
     }
 

packages/core/src/app/ovm/deciders/index.ts

@@ -1,4 +1,5 @@
 export * from './and-decider'
+export * from './for-all-such-that-decider'
 export * from './hash-preimage-existence-decider'
 export * from './key-value-store-decider'
 export * from './not-decider'

packages/core/src/app/ovm/deciders/key-value-store-decider.ts

@@ -1,6 +1,7 @@
 import { Decider, Decision } from '../../../types/ovm'
 import { Bucket, DB } from '../../../types/db'
 import { Md5Hash } from '../../utils'
+import { CannotDecideError } from './utils'
 
 export abstract class KeyValueStoreDecider implements Decider {
   private readonly decisionBucket: Bucket
@@ -9,12 +10,30 @@ export abstract class KeyValueStoreDecider implements Decider {
     this.decisionBucket = db.bucket(Buffer.from(this.getUniqueId()))
   }
 
-  public async checkDecision(input: any): Promise<Decision> {
+  public async decide(
+    input: any,
+    witness?: any,
+    noCache?: boolean
+  ): Promise<Decision> {
+    if (!noCache) {
+      try {
+        return await this.checkDecision(input)
+      } catch (e) {
+        if (!(e instanceof CannotDecideError)) {
+          throw e
+        }
+      }
+    }
+
+    return this.makeDecision(input, witness)
+  }
+
+  private async checkDecision(input: any): Promise<Decision> {
     const hash: Buffer = this.getCacheKey(input)
     const decisionBuffer: Buffer = await this.decisionBucket.get(hash)
 
-    if (decisionBuffer === null) {
-      return undefined
+    if (decisionBuffer === null || decisionBuffer === undefined) {
+      throw new CannotDecideError('No decision was made!')
     }
 
     return this.deserializeDecision(decisionBuffer)
@@ -49,7 +68,7 @@ export abstract class KeyValueStoreDecider implements Decider {
    * ABSTRACT METHODS *
    ********************/
 
-  public abstract decide(input: any, witness: any): Promise<Decision>
+  protected abstract makeDecision(input: any, witness: any): Promise<Decision>
 
   /**
    * Returns the unique ID of this Decider.

packages/core/src/app/ovm/deciders/not-decider.ts

@@ -16,20 +16,18 @@ export interface NotDeciderInput {
 export class NotDecider implements Decider {
   public async decide(
     input: NotDeciderInput,
-    witness: undefined
+    witness?: undefined,
+    noCache?: boolean
   ): Promise<Decision> {
     const decision: Decision = await input.property.decider.decide(
       input.property.input,
-      input.witness
+      input.witness,
+      noCache
     )
 
     return this.getDecision(input, decision)
   }
 
-  public async checkDecision(input: NotDeciderInput): Promise<Decision> {
-    return this.decide(input, undefined)
-  }
-
   /**
    * Gets the Decision that results from invocation of the Not decider, which simply
    * returns the opposite outcome than the provided Decision.

packages/core/src/types/ovm/decider.interface.ts

@@ -11,6 +11,7 @@ export interface Property {
 }
 
 export type PropertyFactory = (input: any) => Property
+export type WitnessFactory = (input: any) => any
 
 export interface ImplicationProofItem {
   implication: Property
@@ -27,21 +28,22 @@ export interface Decision {
  * on the provided input according to the logic of the specific implementation.
  *
  * For example: A PreimageExistsDecider would be able to make decisions on whether
- * or not the provided _witness, when hashed, results in the provided _input.
+ * or not the provided witness, when hashed, results in the provided input.
  */
 export interface Decider {
   /**
-   * Makes a Decision on the provided input
-   * @param input
-   * @param witness
+   * Makes a Decision on the provided input, given the provided witness.
+   *
+   * If this Decider is capable of caching and the noCache flag is not set,
+   * it will first check to see if a decision has already been made on this input.
+   * If this Decider is capable of caching and the noCache flag is set,
+   * it will make the Decision, if possible, and overwrite the cache.
+   *
+   * @param input The input on which a decision is being made
+   * @param witness [optional] The evidence for the decision if not relying on cached decisions
+   * @param noCache [optional] Flag set when caching should not be used.
+   * @returns the Decision that was made if one was possible
+   * @throws CannotDecideError if it cannot decide.
    */
-  decide(input: any, witness: any): Promise<Decision>
-
-  /**
-   * Checks whether or not a decision has been made for the provided Input
-   * Note: This should access a cache decisions that have been made
-   * @param _input
-   * @returns the Decision that was made, if one was made.
-   */
-  checkDecision(input: any): Promise<Decision>
+  decide(input: any, witness?: any, noCache?: boolean): Promise<Decision>
 }