Generating G-bindings from an STV in a particular way.
(stv-easy-bindings stv order) → *
(stv-easy-bindings stv order) is a macro for proving theorems about symbolic-test-vectors using gl. It returns a list of G-bindings for use with def-gl-thm. That is, you can write something like:
(def-gl-thm foo ... :g-bindings (stv-easy-bindings (my-stv) '(opcode size special (:mix a b) c)))
This is probably only useful when:
As in gl::auto-bindings, you can also use
An especially nice feature of easy-bindings is that they automatically adjust when inputs to the STV are resized, when new inputs are added, and when irrelevant inputs are removed.
(defun stv-easy-bindings (stv order) (declare (xargs :guard (processed-stv-p stv))) (let ((__function__ 'stv-easy-bindings)) (declare (ignorable __function__)) (b* ((binds (stv-easy-bindings-main order stv)) (unbound (set-difference-equal (stv->ins stv) (pat-flatten1 binds)))) (gl::auto-bindings-fn (append binds (stv-easy-bindings-inside-mix unbound stv))))))