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.



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


Similar to eq, but returns the opposite result.

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


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.


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


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

Exclusive disjunction

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


complement :: Boolean -> Boolean



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

-- | 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:

> 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.

Last updated


Copyright © 2023 BTQ