|
|
|---|
|
|
|
|---|
AleoVM circuits in R1CS form.
See circuits for background.
We formalize and verify circuits for the operations (and sub-operations) in snarkVM. Each circuit is an ACL2 function that constructs R1CS constraints, paremeterized over the choice of variable names, and possibly over the choice of number of variables and constraints. This follows the approach described in the papers referenced in circuits.
This approach is superseded by the approach in circuits-pfcs, also described in the aforementioned papers, which also explain how the PFCS approach solves a scalability problem inherent to the R1CS approach. Thus, the formalization and verification of circuits in R1CS form is now essentially legacy code, which we keep mainly for historical and testing purposes, and also because not all the circuits in R1CS forms have been ported to PFCS form yet.
These circuits in R1CS form are documented with comments in the files, not in XDOC; thus, this XDOC topic has no subtopics for the circuits.
For some of these circuits in R1CS form, we prove both soundness and completeness, while for others, we only prove soundness; this was work in progress, but we switched to the PFCS approach at some point (see circuits-pfcs). See the papers referenced in circuits for the notions of `soundness' and `completeness' in this context.