And & Not decider implementation (#375)

* And & Not decider implementation
* Added directory for quantifiers to group them together

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

@@ -0,0 +1,75 @@
+import {
+  Decider,
+  Decision,
+  ImplicationProofItem,
+  Property,
+} from '../../../types/ovm'
+
+export interface AndDeciderInput {
+  left: Property
+  leftWitness: any
+  right: Property
+  rightWitness: any
+}
+
+/**
+ * Decider that decides true iff both of the provided properties evaluate to true.
+ */
+export class AndDecider implements Decider {
+  public async decide(
+    input: AndDeciderInput,
+    witness: undefined
+  ): 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),
+    ])
+
+    if (!leftDecision.outcome) {
+      return this.getDecision(input, leftDecision)
+    }
+    if (!rightDecision.outcome) {
+      return this.getDecision(input, rightDecision)
+    }
+
+    const justification: ImplicationProofItem[] = []
+    if (!!leftDecision.justification.length) {
+      justification.push(...leftDecision.justification)
+    }
+    if (!!rightDecision.justification.length) {
+      justification.push(...rightDecision.justification)
+    }
+
+    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.
+   *
+   * @param input The input that led to the Decision
+   * @param subDecision The decision of the wrapped Property, provided the witness
+   * @returns The Decision
+   */
+  private getDecision(input: AndDeciderInput, subDecision: Decision): Decision {
+    const justification: ImplicationProofItem[] = [
+      {
+        implication: {
+          decider: this,
+          input,
+        },
+        implicationWitness: undefined,
+      },
+      ...subDecision.justification,
+    ]
+
+    return {
+      outcome: subDecision.outcome,
+      justification,
+    }
+  }
+}

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

@@ -1,4 +1,4 @@
-import { Decision } from '../../../types/ovm/decider.interface'
+import { Decision } from '../../../types/ovm'
 import { DB } from '../../../types/db'
 import { KeyValueStoreDecider } from './key-value-store-decider'
 import { CannotDecideError, HashFunction } from './utils'

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

@@ -1,3 +1,5 @@
+export * from './and-decider'
 export * from './hash-preimage-existence-decider'
 export * from './key-value-store-decider'
+export * from './not-decider'
 export * from './utils'

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

@@ -1,4 +1,4 @@
-import { Decider, Decision } from '../../../types/ovm/decider.interface'
+import { Decider, Decision } from '../../../types/ovm'
 import { Bucket, DB } from '../../../types/db'
 import { Md5Hash } from '../../utils'
 

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

@@ -0,0 +1,58 @@
+import {
+  Decider,
+  Decision,
+  ImplicationProofItem,
+  Property,
+} from '../../../types/ovm'
+
+export interface NotDeciderInput {
+  property: Property
+  witness: any
+}
+
+/**
+ * Decider that decides true iff the provided property evaluates to false.
+ */
+export class NotDecider implements Decider {
+  public async decide(
+    input: NotDeciderInput,
+    witness: undefined
+  ): Promise<Decision> {
+    const decision: Decision = await input.property.decider.decide(
+      input.property.input,
+      input.witness
+    )
+
+    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.
+   *
+   * @param input The input that led to the Decision
+   * @param subDecision The decision of the wrapped Property, provided the witness
+   * @returns The Decision.
+   */
+  private getDecision(input: NotDeciderInput, subDecision: Decision): Decision {
+    const justification: ImplicationProofItem[] = [
+      {
+        implication: {
+          decider: this,
+          input,
+        },
+        implicationWitness: undefined,
+      },
+      ...subDecision.justification,
+    ]
+
+    return {
+      outcome: !subDecision.outcome,
+      justification,
+    }
+  }
+}

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

@@ -1,3 +1,4 @@
+export * from './deciders'
+export * from './quantifiers'
 export * from './state-db'
 export * from './state-manager'
-export * from './integer-quantifiers'

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

@@ -0,0 +1 @@
+export * from './integer-quantifiers'

packages/core/src/app/ovm/integer-quantifiers.ts → packages/core/src/app/ovm/quantifiers/integer-quantifiers.ts

@@ -1,4 +1,4 @@
-import { QuantifierResult, Quantifier } from '../../types'
+import { QuantifierResult, Quantifier } from '../../../types'
 
 // Helper function which returns an array of numbers, starting at start, ending at end, incrementing by 1.
 // Eg. [0, 1, 2,...end]

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

@@ -1,9 +1,9 @@
-export interface ProofElement {
+export interface ProofItem {
   property: Property
   witness: {}
 }
 
-export type Proof = ProofElement[]
+export type Proof = ProofItem[]
 
 export interface Property {
   decider: Decider
@@ -12,14 +12,14 @@ export interface Property {
 
 export type PropertyFactory = (input: any) => Property
 
-export interface ImplicationProofElement {
+export interface ImplicationProofItem {
   implication: Property
   implicationWitness: any
 }
 
 export interface Decision {
   outcome: boolean
-  justification: ImplicationProofElement[] // constructed such that claim[N] --> claim[N-1] --> claim[N-2]... Claim[0]
+  justification: ImplicationProofItem[] // constructed such that claim[N] --> claim[N-1] --> claim[N-2]... Claim[0]
 }
 
 /**

packages/core/src/types/ovm/index.ts

@@ -1,6 +1,7 @@
-export * from './state-manager.interface'
-export * from './state-db.interface'
+export * from './decider.interface'
 export * from './predicate-plugin.interface'
 export * from './plugin-manager.interface'
-export * from './sync-manager'
 export * from './quantifier.interface'
+export * from './state-db.interface'
+export * from './state-manager.interface'
+export * from './sync-manager'