Use resource limits rather than time limits for verification

[0xabu]

Dafny now supports Z3 resource limits (dafny-lang/dafny#106). We should convert to them to avoid unstable / unpredictable timeouts when verifying. This will require determining appropriate limits and updating the lemmas for which we have hardcoded time limit multipliers.