[enhancement][long-term] Quickcheck proofs that can be leveraged by the optimizer

### What's hard to do? (limit 100 words)

Just filing for a far out idea that I'm sure there's been academic research on but I'm not super familiar with this landscape.

(Another wrinkle in this idea is that we don't yet have parametrized quickchecks, but...)

But generally it'd be super cool if one could write a quickcheck property that was proven correct and (a) cache the proven-ness of the quickcheck property (b) mix that in to the optimizer as a sort of lemma. I'm thinking of things like, I write a new `abs_diff` routine as in #2024 and I prove that like `|x - y|` is only zero when `y == x` in the input domain, can I teach the system to leverage that proven property since I proved it already and the quickcheck effective prescribes a predicate that has an implication.

(Some wrinkles immediately spring to mind, though.) Since not all substitutions are going to be to less costly forms we'd need to have some way of assessing the cost of the RHS of the implication, and we'd also need to choose one of several possibilities, and as they were composed if feels like there's NP completeness in "which should I apply in which order", but if we don't overthink the optimality of it there might be something stripped down in the simple/easy/effective realm. Could be a powerful mechanism to have easily invoked by the user and it would lead to more incentive to write quickchecks and describe / think about the DUT's formal properties.

### Current best alternative workaround (limit 100 words)

Rely on the optimizer to see the properties of interest after "desugaring" via its built in notion of simplification and substitution for built-in types and functions.

### Your view of the "best case XLS enhancement" (limit 100 words)

We create some way to have a limited pattern of quickchecks that can be "gifted" to the optimizer for application.