_{By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/verus-lang/verus/blob/main/LICENSE).}