		Search-engine friendly clone of the ACL2 documentation.

Verify-semaphore-r1cs

A tool to verify a semaphore R1CS

General Form:

(verify-semaphore-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 baby-jubjub-prime. See also r1cs::r1cs-verification-with-axe.