Define a non-executable, fixpoint-based analogue of a symbolic-test-vector and prove properties that allow it to be used in decomposition proofs.

See also def-svtv-refinement, of which this is a wrapper.

To use this, first define an SVTV using defsvtv$
and (immediately after) save the contents of the resulting svtv-data
stobj to an object using def-svtv-data-export. Then invoke

(def-svtv-ideal ideal-name svtv-name data-name)

For example,

(sv::defsvtv$ my-mod-run ...) ;; must be immediately after the defsvtv$ (or at least ensure that the ;; svtv-data stobj is not modified in between) (sv::def-svtv-data-export my-mod-data) ;; may occur later, no more reliance on the svtv-data stobj: (sv::def-svtv-ideal my-mod-ideal my-mod-run my-mod-data)

This produces a 0-ary function (not intended to be executed) named

my-mod-ideal-refines-my-mod-run -- this allows us to infer facts aboutmy-mod-ideal from proofs aboutmy-mod-run , where potentially themy-mod-run proof may be done with override signals that may be removed from the theorem aboutmy-mod-ideal .my-mod-ideal-refines-my-mod-run-on-same-envs -- special case of the above theorem where the input environments are the same, i.e. no overrides are removed.my-mod-ideal-refines-my-mod-ideal -- this allows us to remove overrides from theorems aboutmy-mod-ideal .

Additionally, the