mirror of
https://github.com/logos-co/staking.git
synced 2025-01-10 10:46:01 +00:00
0566bd9faa
This refactors the spec to no longer rely on the `simplification()` but instead filter out the vacuous rules from the get go. Using the `simplification()` previously was needed so that the prover will ignore cases that revert by design. This made some invariants vacuous. Having vacuous rules or invariants is still considered a failure, so to make get prover happy, we're using filtered invariants instead which renders the `simplification` obsolete.