A tool to verify a zcash R1CS
(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 )
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)
Ordering on the vars, to restrict substitutions that express earlier vars in terms of later vars. Not all vars need to be mentioned.
An interpreted-function-alist to evaluate ground terms
Whether to split into cases
Whether to print proof goals as clauses (disjunctions to be proved), rather than conjunctions of negated literals (to be proved contradictory)
Rules to monitor during rewriting
Axe print argument