		Search-engine friendly clone of the ACL2 documentation.

Lift-zcash-r1cs

A tool to lift a zcash R1CS

General Form:

(lift-zcash-r1cs name-of-defconst
                 vars
                 constraints
                 &key
                 :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.

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

This tool is a wrapper for r1cs::lift-r1cs that sets the prime to jubjub-q and sets the package to ZCASH. See also r1cs::r1cs-verification-with-axe.