		Search-engine friendly clone of the ACL2 documentation.

R1cs-verification-with-axe

Verify-r1cs

A tool to verify an R1CS

General Form:

(verify-r1cs lifted-r1cs
             spec-term
             prime
             &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
             :no-print-fns               ; default '(fe-listp)
             :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)

prime — (required)

The prime for the R1CS

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

:no-print-fns — default (fe-listp)

Functions to skip over when printing the current case.

:monitor — default nil

Rules to monitor during rewriting

:print — default :brief

Axe print argument

Description:

See r1cs-verification-with-axe.

Subtopics

Verify-zcash-r1cs: A tool to verify a zcash R1CS