		Search-engine friendly clone of the ACL2 documentation.

Verify-zcash-r1cs

A tool to verify a zcash R1CS

Description:

This tool is a wrapper for r1cs::verify-r1cs that sets the prime to jubjub-q. See also ACL2::axe-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
                   :var-ordering               ; default nil
                   :interpreted-function-alist ; default nil
                   :no-splitp                  ; default t
                   :print-as-clausesp          ; default nil
                   :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)

:var-ordering — default nil

Ordering on the vars, to restrict substitutions that express earlier vars in terms of later vars. Not all vars need to be mentioned.

:interpreted-function-alist — default nil

An interpreted-function-alist to evaluate ground terms

:no-splitp — default t

Whether to split into cases

:print-as-clausesp — default nil

Whether to print proof goals as clauses (disjunctions to be proved), rather than conjunctions of negated literals (to be proved contradictory)

:monitor — default nil

Rules to monitor during rewriting

:print — default :brief

Axe print argument