Add #[verifier::allow(...)] to suppress warnings#2284

Chris-Hawblitzel wants to merge 5 commits into

mainverus-lang/verus:mainfrom

warn-allowverus-lang/verus:warn-allowCopy head branch name to clipboard