		Search-engine friendly clone of the ACL2 documentation.

R1cs-verification-with-axe

Lift-r1cs

A tool to lift an R1CS into logic

General Form:

(lift-r1cs name-of-defconst
           vars
           constraints
           prime
           &key
           :package         ; default :auto
           :rules           ; default :auto
           :extra-rules     ; default nil
           :remove-rules    ; default nil
           :monitor         ; default nil
           :memoizep        ; default nil
           :count-hits      ; default nil
           :print           ; default nil
           )

Inputs:

name-of-defconst — (required)

The name of the defconst (a symbol) that will be created to hold the DAG. This name should start and end with *.

vars — (required)

A form that evaluates to the variables of the R1CS.

constraints — (required)

A form that evaluates to the constraints of the R1CS.

prime — (required)

A form that evaluates to the prime of the R1CS.

:package — default :auto

The package to use for the variables of the DAG (a string), or :auto. If package is :auto, the variables in the DAG are the same as the variables in the R1CS, except that keywords are changed to the ACL2 package (since keywords are not legal variable names in ACL2).

:rules — default :auto

Either :auto, or a form that evaluates to a list of symbols. If the latter, the given rules replace the default rules used for lifting.

:extra-rules — default nil

Rules to be added to the default rule set used for lifting. A form that evaluates to a list of symbols. May be non-nil only when rules is :auto.

:remove-rules — default nil

Rules to be removed from the default rule set used for lifting. A form that evaluates to a list of symbols. May be non-nil only when rules is :auto.

:monitor — default nil

Rules to monitor during rewriting. A form that evaluates to a list of symbols

:memoizep — default nil

Whether to perform memoization during rewriting. A boolean. This may actually slow down the lifting process.

:count-hits — default nil

Whether to count rule hits during rewriting (may cause rewriting to be somewhat slower). A boolean.

:print — default nil

Axe print argument

Description:

Lifts an R1CS into a logical term, represented as an Axe DAG. Takes an R1CS, given as a list of variables, a list of constraints, and a prime. Creates a constant DAG whose name is the name-of-defconst input supplied by the user. The lifting is done by applying the Axe Rewriter. See also r1cs-verification-with-axe.

Subtopics

Lift-zcash-r1cs: A tool to lift a zcash R1CS