Module 1-Impl.Constraint

Rank-1 constraints over Var.ts.

The type of constraints. In the proof system, every constraint is a rank-1 constraint; that is, the constraint takes the form a * b = c for some a, b and c which are made up of some linear combination of Field.Var.ts.

For example, a constraint could be (w + 2*x) * (y + z) = a + b, where w, x, y, z, a, and b are field variables. Note that a linear combination is the result of adding together some of these variables, each multiplied by a field constant (Field.t); any time we want to multiply our *variables*, we need to add a new rank-1 constraint.

type 'k with_constraint_args = ?label:string -> 'k
val boolean : ( Field.Var.t -> t ) with_constraint_args

A constraint that asserts that the field variable is a boolean: either Field.zero or Field.one.

A constraint that asserts that the field variable arguments are equal.

A bare rank-1 constraint.

A constraint that asserts that the first variable squares to the second, ie. square x y => x*x = y within the field.