A tool to verify a semaphore R1CS
(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 )
A DAG representing the lifted R1CS
A term over the input and output vars (this input is not evaluated)
Variables for which to generate BITP assumptions
The Axe tactic to use
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.
Rules to add to every rule-list in the sequence
Axe :use hints for the proof (satisfies axe-use-hintp)
An interpreted-function-alist to evaluate ground terms
Whether to split into cases
Rules to monitor during rewriting
Axe print argument
This tool is a wrapper for r1cs::verify-r1cs that sets the prime to baby-jubjub-prime. See also r1cs::r1cs-verification-with-axe.