Assertions

Establishing relationships and constraints between inputs, outputs and variables is key to building a ZK program.

assert :: Boolean -> Comp ()

To generate a constraint, use predicates like eq that produce Boolean results as the argument for assert. This will create constraints that are fulfilled when the predicate is true.

Predicates

Equality

The eq predicate returns true when the expressions on both sides of the equation evaluate to the same value.

eq :: Field   -> Field   -> Boolean
eq :: Boolean -> Boolean -> Boolean
eq :: UInt w  -> UInt w  -> Boolean

Inequality

Similar to eq, but returns the opposite result.

neq :: Field   -> Field   -> Boolean
neq :: Boolean -> Boolean -> Boolean
neq :: UInt w  -> UInt w  -> Boolean

Comparisons

Less than or equal to

lte :: UInt w -> UInt w -> Boolean

Less than

lt  :: UInt w -> UInt w -> Boolean

Greater than or equal to

gte :: UInt w -> UInt w -> Boolean

Greater than

gt  :: UInt w -> UInt w -> Boolean

Logical operations

Any functions that produces Boolean will do, here are some common built-in Boolean operators.

Conjunction

(.&.) :: Boolean -> Boolean -> Boolean

Disjunction

(.|.) :: Boolean -> Boolean -> Boolean

Exclusive disjunction

(.^.) :: Boolean -> Boolean -> Boolean

Complement

complement :: Boolean -> Boolean

Examples

square

Here's another program that takes two inputs and asserts that the second input is the square of the first input:

src/Tutorial.hs

-- | A program that expects the second input to be the square of the first input
square :: Comp ()
square = do
  x <- inputField Public -- request for a public input and bind it to 'x'
  y <- inputField Private -- request for a private input and bind it to 'y'
  assert ((x * x) `eq` y) -- assert that 'y' equals to 'x' squared

Compiling this function would result in:

ghci

> compile GF181 square
Right R1CS {
  Constriant (1):
    Ordinary constriants (1):

      $0 * $0 = $1

  Variables (2):

    Public Input variable : $0
    Private Input variable : $1

}

The resulting constraint system has two input variables, $0 and $1, and an additional constraint stating that $1 should be the square of $0, which is exactly what we want.

Note that because square returns () , it would generate no output variable when compiled.