Circuits
AleoVM circuits.
The subset of the AleoVM language that executes off-chain
is compiled to zero-knowledge circuits
that are incorporated into the zero-knowledge proofs
of off-chain execution.
As in other forms of compilation,
the same AleoVM code could be compiled
to different zero-knowledge circuits,
so long as they are functionally equivalent.
Here we formalize the zero-knowledge circuits
that the AleoVM language is compiled to in snarkVM. We prove those circuits correct
with respect to high-level specifications that we also provide.
snarkVM generates zero-knowledge circuits in R1CS form.
In circuits-pfcs,
we use our PFCS formalism
to formalize and verify the circuits in a compositional way,
as described in our SBC 2023 paper and in our ACL2-2023 Workshop paper.
Subtopics
- Circuits-pfcs
- AleoVM circuits in PFCS form.
- Field-div-flagged
- Formalization and verification of a circuit
for flagged field division.
- Boolean-assert-true
- Formalization and verification of a circuit
for asserting that a boolean is true.
- Field-inv-flagged
- Formalization and verification of a circuit
for flagged field inversion.
- Boolean-assert
- Formalization and verification of a circuit
for asserting that a field element is a boolean (i.e. 0 or 1).
- Field-div-unchecked
- Formalization and verification of a circuit
for unchecked field division.
- Field-neq
- Formalization and verification of a circuit
for field non-equality.
- Boolean-not
- Formalization and verification of a circuit
for boolean negation.
- Boolean-assert-all
- Formalization and verification of a circuit
for asserting that zero or more field elements are booleans
(i.e. 0 or 1).
- Boolean-if
- Formalization and verification of a circuit
for boolean ternary conditional.
- Field-if
- Formalization and verification of a circuit
for field ternary conditional.
- Boolean-xor
- Formalization and verification of a circuit
for boolean exclusive disjunction.
- Boolean-or
- Formalization and verification of a circuit
for boolean (inclusive) disjunction.
- Boolean-nor
- Formalization and verification of a circuit
for boolean negated (inclusive) disjunction.
- Boolean-and
- Formalization and verification of a circuit
for boolean conjunction.
- Boolean-nand
- Formalization and verification of a circuit
for boolean negated conjunction.
- Boolean-neq
- Formalization and verification of a circuit
for boolean non-equality.
- Boolean-eq
- Formalization and verification of a circuit
for boolean non-equality.
- Boolean-assert-neq
- Formalization and verification of a circuit
for asserting that two booleans are not equal.
- Boolean-assert-eq
- Formalization and verification of a circuit
for asserting that two booleans are equal.
- Field-eq
- Formalization and verification of a circuit
for field non-equality.
- Field-div-checked
- Formalization and verification of a circuit
for checked field division.
- Field-inv-checked
- Formalization and verification of a circuit
for checked field inversion.
- Field-assert-neq
- Formalization and verification of a circuit
for asserting that two field elements are equal.
- Field-assert-eq
- Formalization and verification of a circuit
for asserting that two field elements are equal.
- Field-mul
- Formalization and verification of a circuit
for field multiplication.
- Field-sub
- Formalization and verification of a circuit
for field subtraction.
- Field-square
- Formalization and verification of a circuit
for field squaring.
- Field-neg
- Formalization and verification of a circuit
for field negation.
- Field-double
- Formalization and verification of a circuit
for field doubling.
- Field-add
- Formalization and verification of a circuit
for field addition.
