		Search-engine friendly clone of the ACL2 documentation.

Verify-zcash-r1cs

A tool to verify a zcash R1CS

General Form:

(verify-zcash-r1cs lifted-r1cs
                   spec-term
                   &key
                   :bit-inputs                  ; default nil
                   :tactic                      ; default '(:rep :rewrite :subst)
                   :rule-lists                  ; default nil
                   :global-rules                ; default nil
                   :use                         ; default nil
                   :interpreted-function-alist  ; default nil
                   :no-splitp                   ; default t
                   :monitor                     ; default nil
                   :print                       ; default :brief
                   )

Inputs:

lifted-r1cs — (required)

A DAG representing the lifted R1CS

spec-term — (required)

A term over the input and output vars (this input is not evaluated)

:bit-inputs — default nil

Variables for which to generate BITP assumptions

:tactic — default (:rep :rewrite :subst)

The Axe tactic to use

:rule-lists — default nil

A sequence of Axe rule sets, each of which is a list of rule names and/or calls of 0-ary functions that return lists of rule names. These are applied one after the other.

:global-rules — default nil

Rules to add to every rule-list in the sequence

:use — default nil

Axe :use hints for the proof (satisfies axe-use-hintp)

:interpreted-function-alist — default nil

An interpreted-function-alist to evaluate ground terms

:no-splitp — default t

Whether to split into cases

:monitor — default nil

Rules to monitor during rewriting

:print — default :brief

Axe print argument

Description:

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