Propagators that evaluate structural BitVec operations on literals.
The arguments are matched modulo equalities: given x = 42#64, the propagator for
extractLsb' asserts BitVec.extractLsb' 63 32 x = 0#32. The proofs combine the generic
congruence theorems Grind.eval_congr₁/Grind.eval_congr₂ with an Eq.refl hypothesis
discharged by kernel reduction. Arguments that occur in the result type (widths, extract
bounds, replicate counts) must be syntactic literals; the remaining arguments only need to
be equal to literals.
We deliberately skip:
- arithmetic operations and comparisons (
+,*,-,/,%, division variants,<,≤): they are handled bycutsat; setWidth'andshiftLeftZeroExtend(rare, and their argument order does not fit the suffix-application scheme used by the congruence theorems);BitVec.cast,ofFin/toFin.
The table.