From 5112ccf492b114ec5422f34a18bfc521d2da4cfd Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Mon, 6 Apr 2026 11:30:40 -0700 Subject: [PATCH] Verus verification --- .gitignore | 3 + Cargo.lock | 85 ++++- Cargo.toml | 11 + src/builtins/numbers.rs | 12 + src/lib.rs | 5 +- src/number.rs | 381 ++++++++++++++++++++- src/verusspec/bigint.rs | 712 ++++++++++++++++++++++++++++++++++++++++ src/verusspec/float.rs | 122 +++++++ src/verusspec/mod.rs | 3 + src/verusspec/utils.rs | 65 ++++ 10 files changed, 1390 insertions(+), 9 deletions(-) create mode 100644 src/verusspec/bigint.rs create mode 100644 src/verusspec/float.rs create mode 100644 src/verusspec/mod.rs create mode 100644 src/verusspec/utils.rs diff --git a/.gitignore b/.gitignore index 9634914..eb1d76a 100644 --- a/.gitignore +++ b/.gitignore @@ -54,3 +54,6 @@ bindings/ruby/bin/ bindings/java/.classpath bindings/java/.project bindings/java/.settings/ + +# Emacs temporary files +*~ diff --git a/Cargo.lock b/Cargo.lock index 526114c..7e2b4ba 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -598,6 +598,12 @@ dependencies = [ "zerocopy", ] +[[package]] +name = "hashbrown" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" + [[package]] name = "hashbrown" version = "0.14.5" @@ -794,6 +800,16 @@ dependencies = [ "icu_properties", ] +[[package]] +name = "indexmap" +version = "1.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99" +dependencies = [ + "autocfg", + "hashbrown 0.12.3", +] + [[package]] name = "indexmap" version = "2.13.0" @@ -1386,6 +1402,7 @@ dependencies = [ "thiserror", "url", "uuid", + "vstd", "walkdir", ] @@ -1485,7 +1502,7 @@ version = "0.9.34+deprecated" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47" dependencies = [ - "indexmap", + "indexmap 2.13.0", "itoa", "ryu", "serde", @@ -1641,7 +1658,7 @@ version = "0.25.10+spec-1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a82418ca169e235e6c399a84e395ab6debeb3bc90edc959bf0f48647c6a32d1b" dependencies = [ - "indexmap", + "indexmap 2.13.0", "toml_datetime", "toml_parser", "toml_writer", @@ -1749,12 +1766,76 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +[[package]] +name = "verus_builtin" +version = "0.0.0-2026-03-17-2326" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d7ab914ab490975465ecb3286edceecb0743c3628ddeefcdf25158683e83e2fe" + +[[package]] +name = "verus_builtin_macros" +version = "0.0.0-2026-03-17-2326" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "46f1f1ee124e0bcb5cec79836ff015d138ea53bff51839a85b8364cdc8b79232" +dependencies = [ + "proc-macro2 1.0.106", + "quote 1.0.44", + "syn 2.0.114", + "synstructure", + "verus_prettyplease", + "verus_syn", +] + +[[package]] +name = "verus_prettyplease" +version = "0.0.0-2026-03-15-0111" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eadebc1e3b522b32c178fd2fb882e691880ff983415497232c74aa9b72bc0b65" +dependencies = [ + "proc-macro2 1.0.106", + "verus_syn", +] + +[[package]] +name = "verus_state_machines_macros" +version = "0.0.0-2026-03-15-0111" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b824c6405f8e8a063ca4a26fca1f454cb02de0c1c4da685e3e7f1974899129d5" +dependencies = [ + "indexmap 1.9.3", + "proc-macro2 1.0.106", + "quote 1.0.44", + "verus_syn", +] + +[[package]] +name = "verus_syn" +version = "0.0.0-2026-03-15-0111" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1694faf01f89e1abc996da7b8d24a4e0d1ebd70147dc659e7a5dd680af696772" +dependencies = [ + "proc-macro2 1.0.106", + "quote 1.0.44", + "unicode-ident", +] + [[package]] name = "vsimd" version = "0.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64" +[[package]] +name = "vstd" +version = "0.0.0-2026-03-17-2326" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "13bbf59dfaa6a7bcb327412c778a5d2b2c226dc65473a981ae6ec53a04c75aba" +dependencies = [ + "verus_builtin", + "verus_builtin_macros", + "verus_state_machines_macros", +] + [[package]] name = "walkdir" version = "2.5.0" diff --git a/Cargo.toml b/Cargo.toml index 4dab3e6..cb7fa1e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,6 +14,11 @@ license = "MIT AND Apache-2.0 AND BSD-3-Clause" repository = "https://github.com/microsoft/regorus" keywords = ["interpreter", "no_std", "opa", "policy-as-code", "rego"] +# Enable verification with Verus + +[package.metadata.verus] +verify = true + # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [lib] @@ -134,6 +139,9 @@ mimalloc = { package = "regorus-mimalloc", path = "mimalloc", version = "2.2.6", indexmap = { version = "2.12.1", default-features = false, features = ["serde"], optional = true } postcard = { version = "1.1.3", default-features = false, features = ["alloc"], optional = true } +# Use Verus for verification +vstd = { version = "0.0.0-2026-03-17-2326" } + [dev-dependencies] anyhow = "1.0.102" cfg-if = "1.0.0" @@ -214,3 +222,6 @@ doctest=false # RUSTDOCFLAGS="--cfg docsrs" cargo +nightly doc --all-features --no-deps all-features = true rustdoc-args = ["--cfg", "docsrs"] + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_keep_ghost)'] } diff --git a/src/builtins/numbers.rs b/src/builtins/numbers.rs index 2c55fcb..4986e41 100644 --- a/src/builtins/numbers.rs +++ b/src/builtins/numbers.rs @@ -21,6 +21,8 @@ use anyhow::{bail, Result}; #[cfg(feature = "std")] use rand::RngExt; +use vstd::prelude::*; + pub fn register(m: &mut builtins::BuiltinsMap<&'static str, builtins::BuiltinFcn>) { m.insert("abs", (abs, 1)); m.insert("ceil", (ceil, 1)); @@ -188,3 +190,13 @@ fn intn(span: &Span, params: &[Ref], args: &[Value], _strict: bool) -> Res _ => Value::Undefined, }) } + +// Prove properties with Verus + +verus! { + proof fn lemma_test_one_plus_one_equals_two() + ensures + 1 + 1 == 2, + { + } +} diff --git a/src/lib.rs b/src/lib.rs index 0056fa0..df6bd86 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -3,7 +3,9 @@ // Unsafe code should not be used. // Hard to reason about correctness, and maintainability. -#![forbid(unsafe_code)] +#![cfg_attr(not(verus_keep_ghost), forbid(unsafe_code))] +#![cfg_attr(verus_keep_ghost, feature(proc_macro_hygiene))] +#![cfg_attr(verus_keep_ghost, feature(stmt_expr_attributes))] // Ensure that all lint names are valid. #![deny(unknown_lints)] // Fail-fast lints: correctness, safety, and API surface @@ -125,6 +127,7 @@ mod compiler; mod engine; mod indexchecker; mod interpreter; +mod verusspec; pub mod languages { #[cfg(feature = "azure_policy")] diff --git a/src/number.rs b/src/number.rs index 35e5b3b..4d94650 100644 --- a/src/number.rs +++ b/src/number.rs @@ -27,12 +27,29 @@ use num_traits::{One, Signed, ToPrimitive, Zero}; use serde::ser::Serializer; use serde::Serialize; +#[cfg(verus_keep_ghost)] +use vstd::float::*; +use vstd::prelude::*; +#[cfg(verus_keep_ghost)] +use vstd::std_specs::cmp::*; +#[cfg(verus_keep_ghost)] +use vstd::std_specs::convert::*; + use crate::*; +#[cfg(verus_keep_ghost)] +use crate::verusspec::bigint::*; +use crate::verusspec::float::*; + +#[verus_verify] pub type BigInt = NumBigInt; +verus! { // TODO: Change to #[verus_verify] after PR #2243 const F64_SAFE_INTEGER: f64 = 9_007_199_254_740_992.0; // 2^53 +} +#[verus_verify] +#[verus_verify(external_derive)] #[derive(Clone)] pub enum Number { UInt(u64), @@ -41,7 +58,210 @@ pub enum Number { BigInt(Rc), } +#[cfg(verus_keep_ghost)] +verus! { + +pub assume_specification[ ::clone ](n: &Number) -> (res: Number) + ensures + res == n, +; + +pub enum NumberView { + Integer(int), + Float(f64), +} + +impl View for Number +{ + type V = NumberView; + + open spec fn view(&self) -> NumberView + { + match self { + Number::UInt(n) => NumberView::Integer(n as int), + Number::Int(n) => NumberView::Integer(n as int), + Number::Float(f) => NumberView::Float(*f), + Number::BigInt(b) => NumberView::Integer(b@), + } + } +} + +pub open spec fn float_to_small_int(value: f64) -> Option +{ + if !value.is_finite_spec() || + !spec_f64_fract(value).eq_spec(&0.0f64) || + spec_f64_abs(value) > 9_007_199_254_740_992.0 { + None + } + else if value >= 0.0 { + if ieee_float_cast::(ieee_float_cast::(value)).eq_spec(&value) { + Some(ieee_float_cast::(value) as int) + } + else { + None + } + } + else { + if ieee_float_cast::(ieee_float_cast::(value)).eq_spec(&value) { + Some(ieee_float_cast::(value) as int) + } + else { + None + } + } +} + +impl NumberView { + pub open spec fn to_int(&self) -> Option + { + match *self { + Self::Integer(n) => Some(n), + Self::Float(f) => float_to_small_int(f), + } + } + + pub open spec fn to_f64_lossy_ensures(self: Self, f: f64) -> bool + { + match self { + NumberView::Integer(v) => + { + ||| 0 <= v <= u64::MAX && f == ieee_float_cast::(v as u64) + ||| i64::MIN <= v <= i64::MAX && f == ieee_float_cast::(v as i64) + ||| exists|bi: BigInt| { + &&& bi@ == v + &&& match #[trigger] verusspec::bigint::ToPrimitiveSpec::spec_to_f64(&bi) { + Some(x) => f == x, + None => f == if v < 0 { spec_f64_neg_infinity() } else { spec_f64_infinity() } + } + } + }, + NumberView::Float(v) => f == v, + } + } +} + +impl FromSpecImpl for Number { + open spec fn obeys_from_spec() -> bool + { + false + } + + uninterp spec fn from_spec(v: BigInt) -> Number; +} + +impl FromSpecImpl for Number { + open spec fn obeys_from_spec() -> bool + { + false + } + + uninterp spec fn from_spec(v: u64) -> Number; +} + +impl FromSpecImpl for Number { + open spec fn obeys_from_spec() -> bool + { + false + } + + uninterp spec fn from_spec(v: usize) -> Number; +} + +impl FromSpecImpl for Number { + open spec fn obeys_from_spec() -> bool + { + false + } + + uninterp spec fn from_spec(v: u128) -> Number; +} + +impl FromSpecImpl for Number { + open spec fn obeys_from_spec() -> bool + { + false + } + + uninterp spec fn from_spec(v: i64) -> Number; +} + +impl FromSpecImpl for Number { + open spec fn obeys_from_spec() -> bool + { + false + } + + uninterp spec fn from_spec(v: i128) -> Number; +} + +impl FromSpecImpl for Number { + open spec fn obeys_from_spec() -> bool + { + false + } + + uninterp spec fn from_spec(v: f64) -> Number; +} + +impl PartialEqSpecImpl for Number { + open spec fn obeys_eq_spec() -> bool + { + false + } + + open spec fn eq_spec(&self, other: &Self) -> bool + { + *self == *other + } +} + impl Number { + spec fn spec_to_f64_lossy(&self) -> f64 + { + match *self { + Number::UInt(v) => ieee_float_cast::(v), + Number::Int(v) => ieee_float_cast::(v), + Number::Float(v) => v, + Number::BigInt(v) => { + if let Some(f) = ::spec_to_f64(&v) { + f + } else if v@ < 0 { + spec_f64_neg_infinity() + } else { + spec_f64_infinity() + } + }, + } + } +} + +impl OrdSpecImpl for Number { + open spec fn obeys_cmp_spec() -> bool + { + true + } + + closed spec fn cmp_spec(&self, other: &Self) -> Ordering + { + match (self@.to_int(), other@.to_int()) { + (Some(n1), Some(n2)) => n1.cmp_spec(&n2), + _ => { + let f1 = self.spec_to_f64_lossy(); + let f2 = self.spec_to_f64_lossy(); + f1.partial_cmp_spec(&f2).unwrap_or(Ordering::Equal) + }, + } + } +} + +} // end verus! + +#[verus_verify] +impl Number { + #[verus_spec(result => + ensures + result@ == NumberView::Integer(value@), + )] fn from_bigint_owned(value: BigInt) -> Self { if value.is_zero() { return Number::Int(0); @@ -60,6 +280,10 @@ impl Number { Number::BigInt(Rc::new(value)) } + #[verus_spec(result => + ensures + result@ == NumberView::Integer(value as int), + )] fn from_i128(value: i128) -> Self { if value >= 0 { if let Ok(u) = u64::try_from(value) { @@ -74,6 +298,19 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => result matches Some(bi) && bi@ == n, + NumberView::Float(f) => + { + match result { + Some(bi) => float_to_small_int(f) == Some(bi@), + None => float_to_small_int(f) is None, + } + }, + }, + )] fn to_bigint_owned(&self) -> Option { match self { Number::UInt(v) => Some(BigInt::from(*v)), @@ -83,7 +320,21 @@ impl Number { } } + #[verus_spec(result => + ensures + match result { + Some(bi) => float_to_small_int(value) == Some(bi@), + None => float_to_small_int(value) is None, + }, + )] fn float_to_small_bigint(value: f64) -> Option { + proof! { + axiom_f64_obeys_eq_spec(); + axiom_f64_obeys_partial_cmp_spec(); + axiom_f64_ops_deterministic(); + axiom_f64_comparisons_match_ieee(); + } + if !value.is_finite() || value.fract() != 0.0 { return None; } @@ -94,12 +345,12 @@ impl Number { if value >= 0.0 { let u = value as u64; - if (u as f64) == value { + if u as f64 == value { return Some(BigInt::from(u)); } } else { let i = value as i64; - if (i as f64) == value { + if i as f64 == value { return Some(BigInt::from(i)); } } @@ -107,6 +358,17 @@ impl Number { None } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => result matches Some(bi) && bi@ == n, + NumberView::Float(f) => + match result { + Some(bi) => float_to_small_int(f) == Some(bi@), + None => float_to_small_int(f) is None, + }, + }, + )] fn to_bigint_rc(&self) -> Option> { match self { Number::BigInt(v) => Some(v.clone()), @@ -114,7 +376,13 @@ impl Number { } } + #[verus_spec(result => + ensures + self@.to_f64_lossy_ensures(result), + result == self.spec_to_f64_lossy(), + )] fn to_f64_lossy(&self) -> f64 { + proof! { axiom_f64_ops_deterministic(); } match self { Number::UInt(v) => *v as f64, Number::Int(v) => *v as f64, @@ -123,15 +391,23 @@ impl Number { if let Some(f) = v.to_f64() { f } else if v.is_negative() { - f64::NEG_INFINITY + f64_neg_infinity() } else { - f64::INFINITY + f64_infinity() } } } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => result == (n == 0), + NumberView::Float(f) => result == f.eq_spec(&0.0f64), + }, + )] fn is_zero(&self) -> bool { + proof! { axiom_f64_obeys_eq_spec(); } match self { Number::UInt(0) | Number::Int(0) => true, Number::Float(f) => *f == 0.0, @@ -140,17 +416,39 @@ impl Number { } } + #[verus_spec(result => + requires + a@ is Integer, + b@ is Integer, + ensures + a@ matches NumberView::Integer(m) && result.0@ == m, + b@ matches NumberView::Integer(n) && result.1@ == n, + )] fn ints_to_bigint(a: &Number, b: &Number) -> (BigInt, BigInt) { (a.to_bigint_owned().unwrap(), b.to_bigint_owned().unwrap()) } + #[verus_spec(result => + ensures + match result@ { + NumberView::Integer(n) => float_to_small_int(value) == Some(n), + NumberView::Float(f) => float_to_small_int(value) is None && f == value, + } + )] fn normalize_float(value: f64) -> Number { - if let Some(int) = Self::float_to_small_bigint(value) { - return Self::from_bigint_owned(int); + if let Some(i) = Self::float_to_small_bigint(value) { + return Self::from_bigint_owned(i); } Number::Float(value) } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(v) => if 0 <= v <= u32::MAX { result == Some(v as u32) } else { result is None }, + NumberView::Float(_) => result is None, + }, + )] fn as_u32(&self) -> Option { match self { Number::UInt(v) if *v <= u32::MAX as u64 => Some(*v as u32), @@ -179,25 +477,45 @@ impl Serialize for Number { } } +#[verus_verify] impl From for Number { + #[verus_spec(result => + ensures + result@ == NumberView::Integer(value@), + )] fn from(value: BigInt) -> Self { Number::from_bigint_owned(value) } } +#[verus_verify] impl From for Number { + #[verus_spec(result => + ensures + result@ == NumberView::Integer(value as int), + )] fn from(value: u64) -> Self { Number::UInt(value) } } +#[verus_verify] impl From for Number { + #[verus_spec(result => + ensures + result@ == NumberView::Integer(value as int), + )] fn from(value: usize) -> Self { Number::UInt(value as u64) } } +#[verus_verify] impl From for Number { + #[verus_spec(result => + ensures + result@ == NumberView::Integer(value as int), + )] fn from(value: u128) -> Self { if let Ok(n) = u64::try_from(value) { Number::UInt(n) @@ -207,19 +525,34 @@ impl From for Number { } } +#[verus_verify] impl From for Number { + #[verus_spec(result => + ensures + result@ == NumberView::Integer(value as int), + )] fn from(value: i64) -> Self { Number::Int(value) } } +#[verus_verify] impl From for Number { + #[verus_spec(result => + ensures + result@ == NumberView::Integer(value as int), + )] fn from(value: i128) -> Self { Number::from_i128(value) } } +#[verus_verify] impl From for Number { + #[verus_spec(result => + ensures + result@ == NumberView::Float(value), + )] fn from(value: f64) -> Self { Number::Float(value) } @@ -287,8 +620,25 @@ impl FromStr for Number { } } +#[verus_verify] impl PartialEq for Number { + #[verus_spec(result => + ensures + match (self@.to_int(), other@.to_int()) { + (Some(n1), Some(n2)) => result == (n1 == n2), + _ => exists|f1: f64, f2: f64| #![trigger self@.to_f64_lossy_ensures(f1), other@.to_f64_lossy_ensures(f2)] { + &&& self@.to_f64_lossy_ensures(f1) + &&& other@.to_f64_lossy_ensures(f2) + &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2)) + }, + }, + )] fn eq(&self, other: &Self) -> bool { + proof! { + axiom_bigint_obeys_eq_spec(); + axiom_f64_obeys_eq_spec(); + } + if let (Some(a), Some(b)) = (self.to_bigint_owned(), other.to_bigint_owned()) { return a == b; } @@ -304,12 +654,31 @@ impl PartialEq for Number { impl Eq for Number {} +#[verus_verify] impl Ord for Number { + #[verus_spec(result => + ensures + match (self@.to_int(), other@.to_int()) { + (Some(n1), Some(n2)) => result == n1.cmp_spec(&n2), + _ => exists|f1: f64, f2: f64| #![trigger self@.to_f64_lossy_ensures(f1), other@.to_f64_lossy_ensures(f2)] { + &&& self@.to_f64_lossy_ensures(f1) + &&& other@.to_f64_lossy_ensures(f2) + &&& result == f1.partial_cmp_spec(&f2).unwrap_or(Ordering::Equal) + }, + }, + )] fn cmp(&self, other: &Self) -> Ordering { + proof! { + axiom_f64_obeys_partial_cmp_spec(); + axiom_bigint_obeys_cmp_spec(); + } if let (Some(a), Some(b)) = (self.to_bigint_owned(), other.to_bigint_owned()) { return a.cmp(&b); } + proof! { + assume(false); + } self.to_f64_lossy() .partial_cmp(&other.to_f64_lossy()) .unwrap_or(Ordering::Equal) diff --git a/src/verusspec/bigint.rs b/src/verusspec/bigint.rs new file mode 100644 index 0000000..e7ea9a9 --- /dev/null +++ b/src/verusspec/bigint.rs @@ -0,0 +1,712 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. +#![allow( + clippy::arithmetic_side_effects, + clippy::float_cmp, + clippy::unwrap_used, + clippy::unreachable, + clippy::option_if_let_else, + clippy::unseparated_literal_suffix, + clippy::as_conversions, + clippy::unused_trait_names, + clippy::pattern_type_mismatch +)] + +#[cfg(verus_keep_ghost)] +use core::cmp::Ordering; +#[cfg(verus_keep_ghost)] +use num_bigint::BigInt; +#[cfg(verus_keep_ghost)] +use vstd::std_specs::cmp::OrdSpec; +use vstd::prelude::*; + +verus! { + +#[cfg(verus_keep_ghost)] +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExNumBigInt(num_bigint::BigInt); + +pub assume_specification[ ::clone ](n: &BigInt) -> (res: BigInt) + ensures + res == n, +; + +#[cfg(verus_keep_ghost)] +pub trait BigIntAdditionalSpecFns { + spec fn view(&self) -> int; +} + +#[cfg(verus_keep_ghost)] +impl BigIntAdditionalSpecFns for BigInt { + uninterp spec fn view(&self) -> int; +} + +// Conditions + +pub assume_specification[ ::is_zero ](x: &BigInt) -> (res: bool) + ensures + res == (x@ == 0), +; + +pub assume_specification[ ::is_negative ](x: &BigInt) -> (res: bool) + ensures + res == (x@ < 0), +; + +// PartialEq + +pub axiom fn axiom_bigint_obeys_eq_spec() + ensures + ::obeys_eq_spec(), +; + +pub axiom fn axiom_bigint_obeys_partial_cmp_spec() + ensures + ::obeys_partial_cmp_spec(), +; + +pub assume_specification[ ::eq ](x: &BigInt, y: &BigInt) -> (res: bool) + ensures + res == (x@ == y@), +; + +// Ord + +pub axiom fn axiom_bigint_obeys_cmp_spec() + ensures + ::obeys_cmp_spec(), + forall|b1: &BigInt, b2: &BigInt| b1.cmp_spec(b2) == b1@.cmp_spec(&b2@), +; + +pub assume_specification[ ::cmp ](x: &BigInt, y: &BigInt) -> (res: Ordering) + ensures + res == x@.cmp_spec(&y@), +; + +// From + +pub assume_specification[ >::from ](i: i64) -> (res: BigInt) + ensures + res@ == i, +; + +pub assume_specification[ >::from ](i: i128) -> (res: BigInt) + ensures + res@ == i, +; + +pub assume_specification[ >::from ](u: u64) -> (res: BigInt) + ensures + res@ == u, +; + +pub assume_specification[ >::from ](u: u128) -> (res: BigInt) + ensures + res@ == u, +; + +// Negation + +pub assume_specification[ ::neg ](x: BigInt) -> (y: BigInt) + ensures + y@ == -x@, +; + +// Addition + +pub assume_specification[ ::add ](x: BigInt, y: BigInt) -> (o: BigInt) + ensures + o@ == x@ + y@, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &BigInt) -> (o: BigInt) + ensures + o@ == x@ + (*y)@, +; + +pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Add<&BigInt>>::add ](x: &'b BigInt, y: &BigInt) -> (o: BigInt) + ensures + o@ == (*x)@ + (*y)@, +; + +pub assume_specification[ >::add ](x: BigInt, y: u8) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: u16) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: u32) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: u64) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: u128) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: i8) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: i16) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: i32) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: i64) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification[ >::add ](x: BigInt, y: i128) -> (o: BigInt) + ensures + o@ == x@ + y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &u8) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &u16) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &u32) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &u64) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &u128) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &i8) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &i16) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &i32) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &i64) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +pub assume_specification<'a>[ >::add ](x: BigInt, y: &i128) -> (o: BigInt) + ensures + o@ == x@ + *y, +; + +// Subtraction + +pub assume_specification[ ::sub ](x: BigInt, y: BigInt) -> (o: BigInt) + ensures + o@ == x@ - y@, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &BigInt) -> (o: BigInt) + ensures + o@ == x@ - (*y)@, +; + +pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Sub<&BigInt>>::sub ](x: &'b BigInt, y: &BigInt) -> (o: BigInt) + ensures + o@ == (*x)@ - (*y)@, +; + +pub assume_specification[ >::sub ](x: BigInt, y: u8) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: u16) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: u32) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: u64) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: u128) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: i8) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: i16) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: i32) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: i64) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification[ >::sub ](x: BigInt, y: i128) -> (o: BigInt) + ensures + o@ == x@ - y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &u8) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &u16) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &u32) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &u64) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &u128) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &i8) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &i16) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &i32) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &i64) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +pub assume_specification<'a>[ >::sub ](x: BigInt, y: &i128) -> (o: BigInt) + ensures + o@ == x@ - *y, +; + +// Multiplication + +pub assume_specification[ ::mul ](x: BigInt, y: BigInt) -> (o: BigInt) + ensures + o@ == x@ * y@, +; + +pub assume_specification<'a>[ >::mul ](x: BigInt, y: &BigInt) -> (o: BigInt) + ensures + o@ == x@ * (*y)@, +; + +pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Mul<&BigInt>>::mul ](x: &'b BigInt, y: &BigInt) -> (o: BigInt) + ensures + o@ == (*x)@ * (*y)@, +; + +pub assume_specification[ >::mul ](x: BigInt, y: u8) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: u16) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: u32) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: u64) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: u128) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: i8) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: i16) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: i32) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: i64) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification[ >::mul ](x: BigInt, y: i128) -> (o: BigInt) + ensures + o@ == x@ * y, +; + +pub assume_specification<'a>[ >::mul ](x: BigInt, y: &u8) -> (o: BigInt) + ensures + o@ == x@ * *y, +; + +// Division + +pub assume_specification[ ::div ](x: BigInt, y: BigInt) -> (o: BigInt) + ensures + o@ == x@ / y@, +; + +pub assume_specification<'a>[ >::div ](x: BigInt, y: &BigInt) -> (o: BigInt) + ensures + o@ == x@ / (*y)@, +; + +pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Div<&BigInt>>::div ](x: &'b BigInt, y: &BigInt) -> (o: BigInt) + ensures + o@ == (*x)@ / (*y)@, +; + +pub assume_specification[ >::div ](x: BigInt, y: u8) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: u16) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: u32) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: u64) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: u128) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: i8) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: i16) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: i32) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: i64) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification[ >::div ](x: BigInt, y: i128) -> (o: BigInt) + ensures + o@ == x@ / (y as int), +; + +pub assume_specification<'a>[ >::div ](x: BigInt, y: &u8) -> (o: BigInt) + ensures + o@ == x@ / (*y as int), +; + +} // end verus! + +// Verus's encoding of ToPrimitive relies on an unstable feature +// `sized_hierarchy`, so we can only talk about it when verifying. +// So, we wrap it all in `#[cfg(verus_keep_ghost)]`. + +#[cfg(verus_keep_ghost)] +verus! { + +// ToPrimitive + +#[verifier::external_trait_specification] +#[verifier::external_trait_extension(ToPrimitiveSpec via ToPrimitiveSpecImpl)] +pub trait ExToPrimitive { + type ExternalTraitSpecificationFor: num_traits::ToPrimitive; + + spec fn obeys_to_primitive_spec() -> bool; + + spec fn spec_to_int(&self) -> Option; + + fn to_isize(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(isize::MIN <= n <= isize::MAX), + }, + default_ensures + true, + ; + + fn to_i8(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(i8::MIN <= n <= i8::MAX), + }, + default_ensures + true, + ; + + fn to_i16(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(i16::MIN <= n <= i16::MAX), + }, + default_ensures + true, + ; + + fn to_i32(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(i32::MIN <= n <= i32::MAX), + }, + default_ensures + true, + ; + + fn to_i64(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(i64::MIN <= n <= i64::MAX), + }, + ; + + fn to_i128(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(i128::MIN <= n <= i128::MAX), + }, + default_ensures + true, + ; + + fn to_usize(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(usize::MIN <= n <= usize::MAX), + }, + default_ensures + true, + ; + + fn to_u8(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(u8::MIN <= n <= u8::MAX), + }, + default_ensures + true, + ; + + fn to_u16(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(u16::MIN <= n <= u16::MAX), + }, + default_ensures + true, + ; + + fn to_u32(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(u32::MIN <= n <= u32::MAX), + }, + default_ensures + true, + ; + + fn to_u64(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(u64::MIN <= n <= u64::MAX), + }, + ; + + fn to_u128(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> + match (self.spec_to_int(), res) { + (None, None) => true, + (None, Some(_)) => false, + (Some(n1), Some(n2)) => n1 == n2, + (Some(n), None) => !(u128::MIN <= n <= u128::MAX), + }, + default_ensures + true, + ; + + spec fn spec_to_f32(&self) -> Option; + + fn to_f32(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> res == self.spec_to_f32(), + default_ensures + true, + ; + + spec fn spec_to_f64(&self) -> Option; + + fn to_f64(&self) -> (res: Option) + ensures + Self::obeys_to_primitive_spec() ==> res == self.spec_to_f64(), + default_ensures + true, + ; +} + +impl ToPrimitiveSpecImpl for num_bigint::BigInt +{ + open spec fn obeys_to_primitive_spec() -> bool + { + true + } + + open spec fn spec_to_int(&self) -> Option + { + Some(self@) + } + + uninterp spec fn spec_to_f32(&self) -> Option; + + uninterp spec fn spec_to_f64(&self) -> Option; +} + +// These are the methods of ToPrimitive that BigInt implements because there is no default in ToPrimitive +pub assume_specification[ ::to_i64 ](x: &BigInt) -> (res: Option); +pub assume_specification[ ::to_u64 ](x: &BigInt) -> (res: Option); + +// These are the methods of ToPrimitive that BigInt overrides the defaults for because they'd otherwise be wrong +pub assume_specification[ ::to_i128 ](x: &BigInt) -> (res: Option); +pub assume_specification[ ::to_u128 ](x: &BigInt) -> (res: Option); +pub assume_specification[ ::to_f32 ](x: &BigInt) -> (res: Option); +pub assume_specification[ ::to_f64 ](x: &BigInt) -> (res: Option); + +} // end verus! hidden by cfg(verus_keep_ghost) diff --git a/src/verusspec/float.rs b/src/verusspec/float.rs new file mode 100644 index 0000000..6ab6a44 --- /dev/null +++ b/src/verusspec/float.rs @@ -0,0 +1,122 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. +#![allow( + clippy::arithmetic_side_effects, + clippy::float_cmp, + clippy::unwrap_used, + clippy::unreachable, + clippy::option_if_let_else, + clippy::unseparated_literal_suffix, + clippy::as_conversions, + clippy::unused_trait_names, + clippy::pattern_type_mismatch +)] + +#[cfg(verus_keep_ghost)] +use vstd::float::*; +#[cfg(verus_keep_ghost)] +use vstd::std_specs::cmp::PartialEqIs; +#[cfg(verus_keep_ghost)] +use vstd::std_specs::cmp::PartialOrdIs; +use vstd::prelude::*; + +verus! { + +pub axiom fn axiom_f64_obeys_eq_spec() + ensures + ::obeys_eq_spec(), +; + +pub axiom fn axiom_f64_obeys_partial_cmp_spec() + ensures + ::obeys_partial_cmp_spec(), +; + +pub axiom fn axiom_f64_comparisons_match_ieee() + ensures + forall|f1: f64, f2: f64| #[trigger] f1.ieee_lt(f2) <==> f1.is_lt(&f2), + forall|f1: f64, f2: f64| #[trigger] f1.ieee_le(f2) <==> f1.is_le(&f2), + forall|f1: f64, f2: f64| #[trigger] f1.ieee_gt(f2) <==> f1.is_gt(&f2), + forall|f1: f64, f2: f64| #[trigger] f1.ieee_ge(f2) <==> f1.is_ge(&f2), +; + +pub axiom fn axiom_f64_ops_deterministic() + ensures + ::obeys_neg_spec(), + ::obeys_add_spec(), + ::obeys_sub_spec(), + ::obeys_mul_spec(), + ::obeys_div_spec(), + forall|n: i8, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u8, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i8, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u8, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: i16, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u16, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i16, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u16, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: i32, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u32, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i32, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u32, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: i64, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u64, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i64, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u64, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: i128, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u128, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i128, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u128, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), +; + +pub assume_specification [ f64::is_finite ](f: f64) -> (res: bool) + ensures + res == f.is_finite_spec(), +; + +pub uninterp spec fn spec_f64_fract(f: f64) -> f64; + +pub assume_specification [ f64::fract ](f: f64) -> (res: f64) + requires + f.is_finite_spec(), + ensures + res == spec_f64_fract(f), +; + +pub uninterp spec fn spec_f64_abs(f: f64) -> f64; + +pub assume_specification [ f64::abs ](f: f64) -> (res: f64) + requires + f.is_finite_spec(), + ensures + res == spec_f64_abs(f), +; + +pub assume_specification [ f64::is_nan ](f: f64) -> (res: bool) + ensures + res == f.is_nan_spec(), +; + +pub uninterp spec fn spec_f64_neg_infinity() -> f64; + +#[inline] +#[verifier::external_body] +pub fn f64_neg_infinity() -> (res: f64) + ensures + res == spec_f64_neg_infinity(), +{ + f64::NEG_INFINITY +} + +pub uninterp spec fn spec_f64_infinity() -> f64; + +#[inline] +#[verifier::external_body] +pub fn f64_infinity() -> (res: f64) + ensures + res == spec_f64_infinity(), +{ + f64::INFINITY +} + +} // end verus! diff --git a/src/verusspec/mod.rs b/src/verusspec/mod.rs new file mode 100644 index 0000000..6319b84 --- /dev/null +++ b/src/verusspec/mod.rs @@ -0,0 +1,3 @@ +pub(crate) mod bigint; +pub(crate) mod float; +pub(crate) mod utils; diff --git a/src/verusspec/utils.rs b/src/verusspec/utils.rs new file mode 100644 index 0000000..a6d0f9c --- /dev/null +++ b/src/verusspec/utils.rs @@ -0,0 +1,65 @@ +use anyhow::{bail, Result}; +use std::format; +use std::string::String; + +use vstd::prelude::*; + +verus! { + +#[cfg(verus_keep_ghost)] +#[verifier::external_body] +pub fn verus_format_helper() -> String +{ + format!("who cares") +} + +macro_rules! verus_format { + ( $( $tt0:tt )* ) => { + { + #[cfg(not(verus_keep_ghost))] + { format!($($tt0)*) } + #[cfg(verus_keep_ghost)] + { verus_format_helper() } + } + } +} + +#[allow(dead_code)] +fn my_test_verus_format(fcn: &'static str, x: u32) -> String +{ + verus_format!("The parameters are `{fcn}` and `{x}`") +} + +#[cfg(verus_keep_ghost)] +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExAnyhowError(anyhow::Error); + +#[cfg(verus_keep_ghost)] +#[verifier::external_body] +pub fn verus_bail_helper() -> Result +{ + bail!("who cares") +} + +macro_rules! verus_bail { + ( $( $tt0:tt )* ) => { + { + #[cfg(not(verus_keep_ghost))] + { bail!($($tt0)*) } + #[cfg(verus_keep_ghost)] + { return verus_bail_helper(); } + } + } +} + +#[allow(dead_code)] +fn my_test_verus_bail(fcn: &'static str, x: u32) -> Result<()> +{ + if x > 0 { + verus_bail!("Invalid parameters `{}` and `{}`", fcn, x) + } + Ok(()) +} + +} // end verus!