Faster proof of `lemma_hoist_over_denominator`

verus-lang / verus

Verified Rust for low-level systems code

MIT License

1.06k stars 58 forks source link

Faster proof of `lemma_hoist_over_denominator` #1206

Open jaylorch opened 3 days ago

jaylorch commented 3 days ago

Every time we build vstd as part of building Verus, the verifier complains that lemma_hoist_over_denominator takes well over 2 seconds to verify. This fixes that issue.