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

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)

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

See r1cs-verification-with-axe.

Subtopics

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