diff --git a/.dir-locals.el b/.dir-locals.el deleted file mode 100644 index 1542960e4..000000000 --- a/.dir-locals.el +++ /dev/null @@ -1,12 +0,0 @@ -;;; Directory Local Variables -*- no-byte-compile: t; -*- -;;; For more information see (info "(emacs) Directory Variables") - -;; Regorus is a cargo-verus project (package.metadata.verus.verify = true), so -;; verus-mode.el runs `cargo verus verify' rather than the raw `verus' binary. -;; The cargo-verus path ignores `package.metadata.verus.ide.extra_args' and -;; instead reads `verus-cargo-verus-arguments'. We set it here so that Verus is -;; invoked with the `verus' Cargo feature enabled. -;; -;; Everything before `--' is passed to cargo-verus; everything after `--' is -;; forwarded to the Verus binary. The `--' is required by verus-mode.el. -((verus-mode . ((verus-cargo-verus-arguments . ("--features" "verus" "--"))))) diff --git a/.github/skills/verus-verification/SKILL.md b/.github/skills/verus-verification/SKILL.md new file mode 100644 index 000000000..28b0cead6 --- /dev/null +++ b/.github/skills/verus-verification/SKILL.md @@ -0,0 +1,309 @@ +--- +name: verus-verification +description: >- + Rigorous Verus specification and proof work for Regorus. Use when adding, + strengthening, debugging, or reviewing Verus contracts, proofs, external-body + boundaries, assume_specification declarations, BigInt or Number models, or + minimal Verus bug reproducers. Preserves executable behavior while minimizing + trusted assumptions and verifier workarounds. +--- + +# Regorus Verus Verification + +Use this workflow for proof-oriented changes in Regorus, especially `Number`, +`BigInt`, arithmetic, conversions, and policy-critical value semantics. + +The objective is not merely to make Verus pass. The objective is to establish an +exact, useful contract for the real executable implementation with the smallest +honest trusted boundary. + +## Core Rules + +1. **Specify executable semantics exactly.** + - Model every meaningful result variant and error path. + - Preserve distinctions such as integer versus float representation. + - For floating-point operations, specify IEEE-754 behavior rather than ideal + real arithmetic. + - Do not weaken a contract just because the stronger proof is inconvenient. + +2. **Prove bodies whenever Verus supports them.** + - Prefer a verified implementation over `assume_specification`. + - Remove a trusted assumption once the implementation carries a proved spec. + - Never describe an `external_body` function as body-proved. + +3. **Preserve executable behavior.** + - Before editing, compare the function with `main` or the relevant base. + - Keep executable statements unchanged unless the task explicitly requires a + runtime fix. + - Never use conditional compilation to give Verus and ordinary Rust different + executable bodies or behavior. If Verus cannot verify the shared body, + retain the narrowest `external_body` boundary and document the unsupported + construct. + - Put ghost reasoning in `proof!` blocks. Move proof work to the beginning of + the function when it depends only on inputs. + - Afterward, inspect the focused diff against the base and confirm that only + contracts and erased proof code differ, unless a runtime change was intended. + +4. **Do not use preconditions to hide valid edge cases.** + - Check minimum signed values, maximum values, zero, and representation + boundaries explicitly. + - Negating `i32::MIN` as `i32` overflows, but its magnitude $2^31$ fits in + `u32`. Widen before negation, for example `(-(e as i64)) as u32`. + - If the API can compute a valid result, prove and compute it instead of + excluding the input or returning an invented error. + +5. **Reuse existing semantic models.** + - Search `src/verify/` before adding an uninterpreted spec function. + - Prefer established models such as `pow2`, `NumberView`, + `to_f64_lossy_ensures`, and BigInt view/spec traits. + - If the same mathematical value can have representation-dependent runtime + behavior, quantify over the concrete modeled value rather than pretending + the view alone determines the result. + - When a view deliberately merges concrete variants, use a relational + postcondition for representation-sensitive operations. For example, + `NumberView::Integer` merges `Int`, `UInt`, and `BigInt`, whose lossy float + conversions and boundary behavior need not be a function of the view alone. + - Propagate that relation through callers with existential result witnesses. + Do not recover hidden representation by existentially inventing a concrete + `Number` whose view matches; that leaks internals and may choose a witness + unrelated to the executable receiver. + +6. **Minimize and explain trust.** + - Use `external_body` only at the smallest unsupported boundary. + - Give an exact postcondition, not merely positivity or successful return, + whenever downstream proofs depend on exact behavior. + - Add a short comment naming the concrete verifier limitation, for example: + overloaded `<<=`/`>>=` is unsupported, or overloaded `!` on external + `BigInt` crashes this Verus version. + - Avoid broad external wrappers around otherwise verifiable callers. + +## Workflow + +### 1. Establish the Runtime Baseline + +Start with the function, its helper contracts, its callers, and any existing +trusted specification. + +```bash +git show main:path/to/file.rs +rg -n 'function_name|assume_specification|relevant_helper' src tests +``` + +Record one falsifiable hypothesis: +- what the exact behavior should be; +- which helper contracts it depends on; +- the cheapest verification or runtime check that could disprove it. + +Do not map the whole subsystem before making a small grounded edit. + +### 2. Write the Contract Before the Proof + +The contract should answer: +- Which inputs return `Ok`, `Err`, `Some`, or `None`? +- What exact mathematical value is represented? +- Is the result an integer or float variant? +- Which rounding, overflow, saturation, or lossy-conversion rule applies? +- Are multiple concrete representations possible for the same view? + +For arithmetic returning `Result`, avoid vague contracts such as only +`result is Ok` when the exact value is knowable. + +Write contracts around semantic inputs first, then state the result with +`result matches ...`, `result is None`, or `result is Err`. This is usually +clearer than matching every input/result tuple and separately excluding each +impossible result variant. + +If an abstract view erases representation but the API result depends on it, +allow the honest overlap in the postcondition and explain the boundary. For +example, at `+/-2^53`, primitive and BigInt-backed `Number` values with the same +view can legitimately differ between `Some` and `None` in an exact-float API. + +For BigInt operators, provide exact operator models and prove the caller against +them. For division producing a float, model the exact lossy conversions used by +the executable code. + +### 3. Remove Redundant Trust + +Search for existing assumptions: + +```bash +rg -n 'assume_specification.*function_name|uninterp spec fn' src/verify src +``` + +When moving a spec onto a body-verified function: +- delete the old `assume_specification` in the same change; +- ensure no duplicate specification remains; +- strengthen helper contracts only as much as the body proof requires. + +An external helper may remain trusted when Verus cannot translate its syntax, +but its contract must expose all facts needed by verified callers. + +### 4. Keep Proofs Separate From Execution + +Prefer this shape: + +```rust +pub fn operation(input: i32) -> Result { + proof! { + // Input-only lemmas, cast equalities, and arithmetic facts. + } + + // Original executable body. +} +``` + +Use local proof blocks later only when facts genuinely depend on an executable +value produced at that point. + +Do not introduce executable temporaries solely to help a proof. If a temporary +is ghost-only, keep it inside `proof!`. + +### 5. Handle Casts and Boundaries Explicitly + +Verus often needs explicit facts connecting machine integers and mathematical +integers/naturals: + +```rust +assert((e as u32) as nat == e as nat); +``` + +For negative signed values, widen before negating: + +```rust +let magnitude = (-(e as i64)) as u32; +``` + +Then prove: +- the magnitude is positive; +- its cast equals the intended mathematical magnitude; +- required power/division lemmas apply; +- remainder is nonzero when the runtime should choose floating division. + +Check memory implications separately. A mathematically valid BigInt may be very +large. Prove extreme paths, but do not execute resource-heavy regression tests +unless the cost is acceptable and intentional. Test the conversion and a smaller +representative behavior instead. + +For signed division and remainder, model Rust semantics with `rust_div` and +`rust_rem`; mathematical `/` and `%` do not capture truncation toward zero for +all negative inputs. Bridge primitive operator specs such as `RemSpec` to those +models with focused lemmas. Handle `MIN / -1` before either `/` or `%`, because +both machine operations overflow, and prove the exact quotient fits before +connecting a mathematical result to `checked_div` or a narrowing cast. + +### 6. Use Verification Attributes Deliberately + +- `#[verus_verify]` on an `impl` applies to all methods in that impl. +- Do not split adjacent inherent impls merely to change verification scope when + one impl-level annotation plus narrow method overrides is clearer. +- Use `#[verus_verify(external)]` only when an item must remain entirely outside + verification and has a separate specification. +- Use `#[verus_verify(external_body)]` when Verus should trust a stated contract + but cannot verify the implementation body. +- Method-level attributes can override the impl-wide default. + +Before diagnosing missing internal markers or macro bugs, inspect braces and +attributes. Confirm the method is actually inside the annotated impl. + +### 7. Preserve Production Macros + +Do not replace `bail!`, `anyhow!`, or formatting in the executable body merely +to make translation easier. Inspect the macro expansion and specify the +smallest unsupported pieces. For `anyhow!`, this may mean narrow specifications +for `Arguments::from_str`, `format_err`, and `must_use`; if verified callers +only rely on taking the error branch, those assumptions need not promise +anything about the error value. + +After a Verus upgrade, retry the original macro and previously externalized +bodies. Translation support changes, so stale shims and `external_body` +annotations should not become permanent trusted surface by inertia. + +## Diagnosing Verus Failures + +### Trigger Failure + +Before repairing or replacing a rejected trigger, check whether the quantifier +is semantically necessary. If its bound variables merely name fields of fixed +arguments through equalities such as `lhs == NumberView::Integer(integer_lhs)`, +match on those arguments and state the branch-specific condition directly. This +preserves the contract while removing the quantifier, its trigger, and needless +solver instantiation. Use a natural or artificial trigger only when the contract +genuinely ranges over multiple values that are not determined by fixed inputs. + +### Translation or Compiler Failure + +1. Reduce to the exact operator, type, attribute, and impl context. +2. Test a one-file reproducer with the same relevant structure. +3. Do not introduce macros, missing impl annotations, or different ownership + patterns unless they exist in the failing code. +4. If a small candidate passes, it is not a reproducer. Keep reducing the real + context or state that the failure was caused by local annotation structure. +5. Inspect `~/verus` only after the local code path is understood. + +A valid verifier bug report must: +- fail on the stated Verus version; +- contain no unrelated repository dependencies when avoidable; +- reproduce the same failure mechanism; +- document any workaround retained in Regorus. + +### Proof Failure + +Treat the first focused failure as evidence: +- failed arithmetic safety means the implementation has an unhandled machine + boundary or needs a justified precondition; +- failed postcondition may indicate a missing helper fact, a representation + mismatch, or an incorrect contract; +- unsupported library internals should be isolated in the narrowest helper, not + used to externalize the verified caller. + +Do not respond to a failed proof by immediately weakening the postcondition. +First trace a concrete input through the runtime behavior. + +## Validation + +After the first substantive edit, immediately run the narrowest check: + +```bash +cargo verus verify \ + --fwd-verus-args-to roots -- --verify-module number +``` + +Use a fresh target directory when checking for stale macro or compiler behavior. + +After the focused proof passes: + +```bash +cargo test focused_test_name +cargo fmt --all -- --check +git diff --check +``` + +For broader or final validation, use repository commands as appropriate: + +```bash +cargo xtask fmt +cargo xtask clippy +cargo xtask ci-debug +``` + +Report verification counts accurately. Distinguish: +- body-verified functions; +- external-body contracts; +- trusted assumptions; +- runtime tests actually executed; +- extreme tests skipped due to resource cost. + +## Completion Checklist + +- [ ] Contract matches exact executable semantics. +- [ ] Integer/float and `Undefined` distinctions remain intact where relevant. +- [ ] Minimum/maximum signed values and casts were considered. +- [ ] Original executable body is preserved unless a runtime bug was fixed. +- [ ] Proof-only code is inside `proof!` and placed early when possible. +- [ ] No redundant uninterpreted helper or trusted assumption remains. +- [ ] Every `external_body` has the narrowest useful exact contract and a reason. +- [ ] Impl-level verification annotations cover the intended methods without + unnecessary splits. +- [ ] Any claimed verifier reproducer is representative and independently fails. +- [ ] Focused Verus verification passes. +- [ ] Relevant runtime tests, formatting, and diff checks pass. diff --git a/.github/workflows/verus.yml b/.github/workflows/verus.yml index d17b41848..81384141c 100644 --- a/.github/workflows/verus.yml +++ b/.github/workflows/verus.yml @@ -77,4 +77,4 @@ jobs: export PATH="$(dirname "$cargo_verus_bin"):$(dirname "$verus_bin"):$PATH" cargo verus --help cargo fetch --locked - cargo verus verify --locked --features verus + cargo verus verify --locked diff --git a/.gitignore b/.gitignore index 9634914ba..174ef0274 100644 --- a/.gitignore +++ b/.gitignore @@ -54,3 +54,6 @@ bindings/ruby/bin/ bindings/java/.classpath bindings/java/.project bindings/java/.settings/ + +# Emacs backup files +*~ diff --git a/Cargo.toml b/Cargo.toml index 4eb8f18a6..f60459c7e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -26,7 +26,6 @@ doctest = false [features] default = ["full-opa", "arc", "rvm"] -verus = ["dep:vstd"] arc = [] ast = [] @@ -50,7 +49,7 @@ cache = ["dep:lru"] rvm = ["dep:postcard", "dep:indexmap"] semver = ["dep:semver"] allocator-memory-limits = ["std", "mimalloc", "mimalloc/allocator-memory-limits"] -std = ["rand/std", "rand/std_rng", "serde_json/std", "indexmap?/std", "msvc_spectre_libs", "dep:parking_lot", "vstd?/std" ] +std = ["rand/std", "rand/std_rng", "serde_json/std", "indexmap?/std", "msvc_spectre_libs", "dep:parking_lot", "vstd/std" ] time = ["dep:chrono", "dep:chrono-tz"] uuid = ["dep:uuid"] urlquery = ["dep:url"] @@ -136,7 +135,7 @@ rand = { version = "0.10.0", default-features = false, features = ["thread_rng"] # Causes the project to link with the Spectre-mitigated CRT and libs. msvc_spectre_libs = { version = "0.1", features = ["error"], optional = true } dashmap = { version = "6.1", default-features = false, optional = true } -lru = { version = "0.18", default-features = false, optional = true } +lru = { version = "0.18.2", default-features = false, optional = true } mimalloc = { package = "regorus-mimalloc", path = "mimalloc", version = "2.2.7", optional = true } # rvm related deps @@ -144,9 +143,9 @@ indexmap = { version = "2.13.1", default-features = false, features = ["serde"], postcard = { version = "1.1.3", default-features = false, features = ["alloc"], optional = true } # Verus-related dependencies. -# vstd is enabled via the `verus` feature. In no_std builds only the `alloc` feature is used; -# the crate's `std` feature additionally enables `vstd/std` (matching vstd's default features). -vstd = { version = "=0.0.0-2026-08-09-0044", optional = true, default-features = false, features = ["alloc"] } +# In no_std builds only the `alloc` feature is used; the crate's `std` feature +# additionally enables `vstd/std` (matching vstd's default features). +vstd = { version = "=0.0.0-2026-08-09-0044", default-features = false, features = ["alloc"] } [dev-dependencies] anyhow = "1.0.102" diff --git a/src/lib.rs b/src/lib.rs index 953d8bbe1..27776974e 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,12 +1,27 @@ // Copyright (c) Microsoft Corporation. // Licensed under the MIT License. -// Unsafe code should not be used. -// Hard to reason about correctness, and maintainability. -#![forbid(unsafe_code)] +// Unsafe code should not be used since it's hard to reason about +// its correctness and maintainability. +// However, `verus_keep_ghost` is only set during verification, +// never in production builds, so it's OK to allow unsafe code +// during verification. The `forbid` remains in force for all +// shipped code. +#![cfg_attr(not(verus_keep_ghost), forbid(unsafe_code))] +// `anyhow!` with a literal lowers to `Arguments::from_str`, which is unstable. +// Verus needs to name it to give it a specification. Verification builds use the +// Verus toolchain, so this gate never applies to shipped code. +#![cfg_attr(verus_keep_ghost, feature(fmt_arguments_from_str))] +// Loop invariants are attached with `#[verus_spec(invariant ...)]` on the loop +// statement itself. Applying a proc-macro attribute in statement position is +// still unstable, so verification builds opt in. Shipped builds strip the +// attribute via `cfg_attr` and therefore never need this feature. +#![cfg_attr(verus_keep_ghost, feature(proc_macro_hygiene))] // Ensure that all lint names are valid. #![deny(unknown_lints)] // Fail-fast lints: correctness, safety, and API surface +#![cfg_attr(not(verus_keep_ghost), deny(dead_code))] // ban unused items +#![cfg_attr(not(verus_keep_ghost), deny(missing_debug_implementations))] // require Debug on public types #![deny( // Panic sources - catch all ways code can panic clippy::panic, // forbid explicit panic! macro @@ -21,7 +36,6 @@ clippy::panic_in_result_fn, // disallow panic inside functions returning Result // Rust warnings/upstream - dead_code, // ban unused items deprecated, // prevent use of deprecated APIs deprecated_in_future, // catch items scheduled for deprecation exported_private_dependencies, // avoid leaking private deps in public API @@ -29,7 +43,6 @@ invalid_doc_attributes, // ensure doc attributes are valid keyword_idents, // disallow identifiers that are keywords macro_use_extern_crate, // block legacy macro_use extern crate - missing_debug_implementations, // require Debug on public types // TODO: Address in future pass // missing_docs, // require docs on public items non_ascii_idents, // disallow non-ASCII identifiers @@ -125,6 +138,8 @@ mod compiler; mod engine; mod indexchecker; mod interpreter; +#[cfg(any(verus_keep_ghost, test))] +mod verify; pub mod languages { #[cfg(feature = "azure_policy")] diff --git a/src/number.rs b/src/number.rs index 326fd1e4d..45dd12cfb 100644 --- a/src/number.rs +++ b/src/number.rs @@ -27,16 +27,36 @@ use num_traits::{One, Signed, ToPrimitive, Zero}; use serde::ser::Serializer; use serde::Serialize; -#[cfg(feature = "verus")] use vstd::prelude::*; +#[cfg(verus_keep_ghost)] +use crate::verify::bigint_assumptions::*; +#[cfg(verus_keep_ghost)] +use crate::verify::bigint_proofs::*; +#[cfg(verus_keep_ghost)] +use crate::verify::f64_assumptions::*; +#[cfg(verus_keep_ghost)] +use crate::verify::number_proofs::*; +#[cfg(verus_keep_ghost)] +use crate::verify::number_specs::*; +#[cfg(verus_keep_ghost)] +use vstd::arithmetic::power2::pow2; +#[cfg(verus_keep_ghost)] +use vstd::float::*; +#[cfg(verus_keep_ghost)] +use vstd::std_specs::cmp::*; +#[cfg(verus_keep_ghost)] +use vstd::std_specs::convert::*; + use crate::*; pub type BigInt = NumBigInt; -#[cfg_attr(feature = "verus", verus_verify)] +#[verus_verify] 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), @@ -45,7 +65,12 @@ pub enum Number { BigInt(Rc), } +#[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); @@ -64,6 +89,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) { @@ -78,6 +107,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)), @@ -87,7 +129,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; } @@ -111,6 +167,17 @@ impl Number { None } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => result matches Some(bi) && bi@ == n, + NumberView::Float(f) => + match float_to_small_int(f) { + Some(i) => result matches Some(bi) && bi@ == i, + None => result is None, + }, + }, + )] fn to_bigint_rc(&self) -> Option> { match self { Number::BigInt(v) => Some(v.clone()), @@ -118,7 +185,12 @@ impl Number { } } + #[verus_spec(result => + ensures + self@.to_f64_lossy_ensures(result), + )] 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, @@ -135,7 +207,15 @@ impl Number { } } + #[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, @@ -144,6 +224,10 @@ impl Number { } } + #[verus_spec(result => + ensures + result@ == normalize_float(value), + )] fn normalize_float(value: f64) -> Number { if let Some(i) = Self::float_to_small_bigint(value) { return Self::from_bigint_owned(i); @@ -151,6 +235,13 @@ impl Number { 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 +270,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 +318,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 +413,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,8 +447,29 @@ 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)) => + match result { + Ordering::Less => n1 < n2, + Ordering::Greater => n1 > n2, + Ordering::Equal => 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.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); } @@ -322,8 +486,38 @@ impl PartialOrd for Number { } } +#[verus_verify] impl Number { + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => { + if 0 <= n <= u128::MAX { + result matches Some(value) && value as int == n + } else { + result is None + } + }, + NumberView::Float(f) => { + if f.is_finite_spec() + && f.ieee_ge(0.0f64) + && spec_f64_fract(f).eq_spec(&0.0f64) + && ieee_float_cast::(ieee_float_cast::(f)).eq_spec(&f) { + result matches Some(value) && value == ieee_float_cast::(f) + } + else { + result is None + } + }, + }, + )] pub fn as_u128(&self) -> Option { + proof! { + axiom_f64_obeys_eq_spec(); + axiom_f64_obeys_partial_cmp_spec(); + axiom_f64_ops_deterministic(); + axiom_f64_comparisons_match_ieee(); + } match self { Number::UInt(v) => Some(*v as u128), Number::Int(v) if *v >= 0 => Some(*v as u128), @@ -341,7 +535,33 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => { + if i128::MIN <= n <= i128::MAX { + result matches Some(value) && value as int == n + } else { + result is None + } + }, + NumberView::Float(f) => { + if f.is_finite_spec() + && spec_f64_fract(f).eq_spec(&0.0f64) + && ieee_float_cast::(ieee_float_cast::(f)).eq_spec(&f) { + result matches Some(value) && value == ieee_float_cast::(f) + } + else { + result is None + } + }, + }, + )] pub fn as_i128(&self) -> Option { + proof! { + axiom_f64_obeys_eq_spec(); + axiom_f64_ops_deterministic(); + } match self { Number::UInt(v) => Some(*v as i128), Number::Int(v) => Some(*v as i128), @@ -358,7 +578,37 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => { + if 0 <= n <= u64::MAX { + result matches Some(value) && value as int == n + } else { + result is None + } + }, + NumberView::Float(f) => { + if f.is_finite_spec() + && f.ieee_ge(0.0f64) + && spec_f64_fract(f).eq_spec(&0.0f64) + && f.ieee_le(ieee_float_cast::(u64::MAX)) + && ieee_float_cast::(ieee_float_cast::(f)).eq_spec(&f) { + result matches Some(value) && value == ieee_float_cast::(f) + } + else { + result is None + } + }, + }, + )] pub fn as_u64(&self) -> Option { + proof! { + axiom_f64_obeys_eq_spec(); + axiom_f64_obeys_partial_cmp_spec(); + axiom_f64_ops_deterministic(); + axiom_f64_comparisons_match_ieee(); + } match self { Number::UInt(v) => Some(*v), Number::Int(v) if *v >= 0 => Some(*v as u64), @@ -376,7 +626,37 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => { + if i64::MIN <= n <= i64::MAX { + result matches Some(value) && value as int == n + } else { + result is None + } + }, + NumberView::Float(f) => { + if f.is_finite_spec() + && spec_f64_fract(f).eq_spec(&0.0f64) + && f.ieee_ge(ieee_float_cast::(i64::MIN)) + && f.ieee_le(ieee_float_cast::(i64::MAX)) + && ieee_float_cast::(ieee_float_cast::(f)).eq_spec(&f) { + result matches Some(value) && value == ieee_float_cast::(f) + } + else { + result is None + } + }, + }, + )] pub fn as_i64(&self) -> Option { + proof! { + axiom_f64_obeys_eq_spec(); + axiom_f64_obeys_partial_cmp_spec(); + axiom_f64_ops_deterministic(); + axiom_f64_comparisons_match_ieee(); + } match self { Number::UInt(v) if *v <= i64::MAX as u64 => Some(*v as i64), Number::Int(v) => Some(*v), @@ -398,7 +678,28 @@ impl Number { } } + #[verus_spec(result => + ensures + match (self@, result) { + (NumberView::Float(f), Some(value)) => f.is_finite_spec() && value == f, + (NumberView::Float(f), None) => !f.is_finite_spec(), + (NumberView::Integer(n), Some(value)) => { + &&& -9_007_199_254_740_992 <= n <= 9_007_199_254_740_992 + &&& self@.to_f64_lossy_ensures(value) + }, + // The bounds intentionally overlap at +/-2^53: primitive variants return + // Some there, while a BigInt variant with the same NumberView returns None. + (NumberView::Integer(n), None) => { + n <= -9_007_199_254_740_992 || 9_007_199_254_740_992 <= n + }, + }, + )] pub fn as_f64(&self) -> Option { + proof! { + axiom_f64_ops_deterministic(); + axiom_f64_safe_integer_casts(); + lemma_bigint_bits_le_53(); + } match self { Number::Float(f) if f.is_finite() => Some(*f), Number::UInt(v) if *v <= F64_SAFE_INTEGER as u64 => Some(*v as f64), @@ -414,28 +715,64 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => result matches Some(bi) && bi@ == n, + NumberView::Float(f) => { + match float_to_small_int(f) { + Some(i) => result matches Some(bi) && bi@ == i, + None => result is None, + } + }, + }, + )] pub fn as_big(&self) -> Option> { self.to_bigint_rc() } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => result matches Ok(bi) && bi@ == n, + NumberView::Float(f) => { + match float_to_small_int(f) { + Some(i) => result matches Ok(bi) && bi@ == i, + None => result is Err, + } + }, + }, + )] pub fn to_big(&self) -> Result> { self.as_big() .ok_or_else(|| anyhow!("Number::to_big failed")) } + #[verus_spec(result => + ensures + result is Ok, + old(self)@.add_ensures(rhs@, final(self)@), + )] pub fn add_assign(&mut self, rhs: &Self) -> Result<()> { *self = self.add(rhs)?; Ok(()) } + #[verus_spec(result => + ensures + result matches Ok(value) && self@.add_ensures(rhs@, value@), + )] pub fn add(&self, rhs: &Self) -> Result { - if matches!(self, Number::Float(_)) || matches!(rhs, Number::Float(_)) { - return Ok(Number::normalize_float( - self.to_f64_lossy() + rhs.to_f64_lossy(), - )); + proof! { + axiom_f64_ops_deterministic(); + axiom_bigint_obeys_add_spec(); + axiom_bigint_obeys_add_assign_spec(); } match (self, rhs) { + (Number::Float(_), _) | (_, Number::Float(_)) => Ok(Number::normalize_float( + self.to_f64_lossy() + rhs.to_f64_lossy(), + )), (Number::UInt(a), Number::UInt(b)) => { if let Some(sum) = a.checked_add(*b) { Ok(Number::UInt(sum)) @@ -465,23 +802,34 @@ impl Number { sum += other.to_bigint_owned().unwrap(); Ok(Number::from_bigint_owned(sum)) } - _ => unreachable!(), } } + #[verus_spec(result => + ensures + result is Ok, + old(self)@.sub_ensures(rhs@, final(self)@), + )] pub fn sub_assign(&mut self, rhs: &Self) -> Result<()> { *self = self.sub(rhs)?; Ok(()) } + #[verus_spec(result => + ensures + result matches Ok(value) && self@.sub_ensures(rhs@, value@), + )] pub fn sub(&self, rhs: &Self) -> Result { - if matches!(self, Number::Float(_)) || matches!(rhs, Number::Float(_)) { - return Ok(Number::normalize_float( - self.to_f64_lossy() - rhs.to_f64_lossy(), - )); + proof! { + axiom_f64_ops_deterministic(); + axiom_bigint_obeys_sub_spec(); + axiom_bigint_obeys_sub_assign_spec(); } match (self, rhs) { + (Number::Float(_), _) | (_, Number::Float(_)) => Ok(Number::normalize_float( + self.to_f64_lossy() - rhs.to_f64_lossy(), + )), (Number::UInt(a), Number::UInt(b)) => { if a >= b { Ok(Number::UInt(a - b)) @@ -513,23 +861,43 @@ impl Number { diff -= (**b).clone(); Ok(Number::from_bigint_owned(diff)) } - _ => unreachable!(), } } + #[verus_spec(result => + ensures + result is Ok, + old(self)@.mul_ensures(rhs@, final(self)@), + )] pub fn mul_assign(&mut self, rhs: &Self) -> Result<()> { *self = self.mul(rhs)?; Ok(()) } + #[verus_spec(result => + ensures + result matches Ok(value) && self@.mul_ensures(rhs@, value@), + )] pub fn mul(&self, rhs: &Self) -> Result { - if matches!(self, Number::Float(_)) || matches!(rhs, Number::Float(_)) { - return Ok(Number::normalize_float( - self.to_f64_lossy() * rhs.to_f64_lossy(), - )); + proof! { + axiom_f64_ops_deterministic(); + axiom_bigint_obeys_mul_spec(); + if let (Number::UInt(lhs), Number::UInt(rhs_value)) = (self, rhs) { + assert((*lhs as int) * (*rhs_value as int) <= u128::MAX as int) + by(nonlinear_arith); + } + // Some cases are handled by an or-pattern that computes the product + // with the operands swapped. + if self@ is Integer && rhs@ is Integer { + assert(self@->Integer_0 * rhs@->Integer_0 == rhs@->Integer_0 + * self@->Integer_0) by(nonlinear_arith); + } } match (self, rhs) { + (Number::Float(_), _) | (_, Number::Float(_)) => Ok(Number::normalize_float( + self.to_f64_lossy() * rhs.to_f64_lossy(), + )), (Number::UInt(a), Number::UInt(b)) => { let product = (*a as u128) * (*b as u128); if let Ok(v) = u64::try_from(product) { @@ -565,11 +933,24 @@ impl Number { let product = (**a).clone() * other.to_bigint_owned().unwrap(); Ok(Number::from_bigint_owned(product)) } - _ => unreachable!(), } } + #[verus_spec(result => + ensures + match result { + Ok(value) => self@.div_ensures(rhs@, value@), + Err(_) => rhs@.is_zero(), + }, + )] pub fn divide(self, rhs: &Self) -> Result { + proof! { + axiom_f64_ops_deterministic(); + axiom_bigint_obeys_div_rem_spec(); + lemma_div_ensures_cases(self@, rhs@); + lemma_number_primitive_division_facts(&self, rhs); + } + if rhs.is_zero() { bail!("division by zero"); } @@ -593,6 +974,9 @@ impl Number { Ok(Number::from_bigint_owned(quotient)) } else if *a % *b == 0 { if let Some(q) = a.checked_div(*b) { + proof! { + lemma_checked_div_matches_rust_i64(*a, *b, q); + } Ok(Number::Int(q)) } else { let quotient = BigInt::from(*a) / BigInt::from(*b); @@ -659,7 +1043,26 @@ impl Number { } } + #[verus_spec(result => + ensures + match (self@.to_int(), rhs@.to_int()) { + (Some(a), Some(b)) => + if b == 0 { + result is Err + } else { + result matches Ok(value) + && value@ == NumberView::Integer( + vstd::arithmetic::div_mod::rust_rem(a, b), + ) + }, + _ => result is Err, + }, + )] pub fn modulo(self, rhs: &Self) -> Result { + proof! { + axiom_bigint_obeys_div_rem_spec(); + } + // Conversion fails for a non-integral float, and also for an integral // one whose magnitude exceeds 2^53, which cannot be represented exactly. let (a, b) = match (self.to_bigint_owned(), rhs.to_bigint_owned()) { @@ -675,13 +1078,28 @@ impl Number { Ok(Number::from_bigint_owned(rem)) } + #[verus_spec(result => + ensures + result == match self@ { + NumberView::Integer(_) => true, + NumberView::Float(f) => f.is_finite_spec() && spec_f64_fract(f).eq_spec(&0.0f64), + }, + )] pub fn is_integer(&self) -> bool { + proof! { axiom_f64_obeys_eq_spec(); } match self { Number::Float(f) => f.is_finite() && f.fract() == 0.0, _ => true, } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(n) => result == (n >= 0), + NumberView::Float(f) => result == spec_f64_is_sign_positive(f), + }, + )] pub fn is_positive(&self) -> bool { match self { Number::UInt(_) => true, @@ -691,6 +1109,14 @@ impl Number { } } + #[verus_spec(result => + ensures + match (a@.to_int(), b@.to_int()) { + (Some(lhs), Some(rhs)) => + result matches Some((a, b)) && a@ == lhs && b@ == rhs, + _ => result is None, + } + )] #[allow(clippy::if_then_some_else_none)] fn ensure_integers(a: &Number, b: &Number) -> Option<(BigInt, BigInt)> { if a.is_integer() && b.is_integer() { @@ -700,6 +1126,13 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@.to_int() { + Some(value) => result matches Some(big) && big@ == value, + None => result is None, + }, + )] fn ensure_integer(&self) -> Option { if self.is_integer() { self.to_bigint_owned() @@ -708,41 +1141,123 @@ impl Number { } } + #[verus_spec(result => + ensures + match (self@.to_int(), rhs@.to_int()) { + (Some(a), Some(b)) => + result matches Some(value) && + value@ == NumberView::Integer(spec_bigint_bitand(a, b)), + _ => result is None, + }, + )] pub fn and(&self, rhs: &Self) -> Option { + proof! { axiom_bigint_obeys_bitand_spec(); } let (a, b) = Self::ensure_integers(self, rhs)?; Some(Number::from_bigint_owned(a & b)) } + #[verus_spec(result => + ensures + match (self@.to_int(), rhs@.to_int()) { + (Some(a), Some(b)) => + result matches Some(value) + && value@ == NumberView::Integer(spec_bigint_bitor(a, b)), + _ => result is None, + }, + )] pub fn or(&self, rhs: &Self) -> Option { + proof! { axiom_bigint_obeys_bitor_spec(); } let (a, b) = Self::ensure_integers(self, rhs)?; Some(Number::from_bigint_owned(a | b)) } + #[verus_spec(result => + ensures + match (self@.to_int(), rhs@.to_int()) { + (Some(a), Some(b)) => + result matches Some(value) + && value@ == NumberView::Integer(spec_bigint_bitxor(a, b)), + _ => result is None, + }, + )] pub fn xor(&self, rhs: &Self) -> Option { + proof! { axiom_bigint_obeys_bitxor_spec(); } let (a, b) = Self::ensure_integers(self, rhs)?; Some(Number::from_bigint_owned(a ^ b)) } + #[verus_spec(result => + ensures + match (self@.to_int(), rhs@) { + (Some(value), NumberView::Integer(shift)) => { + if 0 <= shift <= u32::MAX { + result matches Some(r) + && r@ == NumberView::Integer(value * pow2(shift as nat) as int) + } + else { + result is None + } + }, + _ => result is None, + }, + )] pub fn lsh(&self, rhs: &Self) -> Option { + proof! { axiom_bigint_obeys_shl_assign_spec(); } let shift = rhs.as_u32()? as usize; let mut value = self.ensure_integer()?; value <<= shift; Some(Number::from_bigint_owned(value)) } + #[verus_spec(result => + ensures + match (self@.to_int(), rhs@) { + (Some(value), NumberView::Integer(shift)) => { + if 0 <= shift <= u32::MAX { + result matches Some(r) + && r@ == NumberView::Integer(value / pow2(shift as nat) as int) + } + else { + result is None + } + }, + _ => result is None, + }, + )] pub fn rsh(&self, rhs: &Self) -> Option { + proof! { axiom_bigint_obeys_shr_assign_spec(); } let shift = rhs.as_u32()? as usize; let mut value = self.ensure_integer()?; value >>= shift; Some(Number::from_bigint_owned(value)) } + #[verus_spec(result => + ensures + match self@.to_int() { + Some(value) => { + result matches Some(r) + && r@ == NumberView::Integer(-value - 1) + }, + None => result is None, + }, + )] pub fn neg(&self) -> Option { let mut value = self.ensure_integer()?; + proof! { axiom_bigint_not_spec(value); } value = !value; Some(Number::from_bigint_owned(value)) } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(value) => { + result@ matches NumberView::Integer(abs) && abs == if value < 0 { -value } else { value } + }, + NumberView::Float(value) => result@ == NumberView::Float(spec_f64_abs(value)), + }, + )] pub fn abs(&self) -> Number { match self { Number::UInt(_) => self.clone(), @@ -758,6 +1273,13 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(_) => result@ == self@, + NumberView::Float(value) => result@ == normalize_float(spec_f64_floor(value)), + }, + )] pub fn floor(&self) -> Number { match self { Number::Float(f) => Number::normalize_float(f.floor()), @@ -765,6 +1287,13 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(_) => result@ == self@, + NumberView::Float(value) => result@ == normalize_float(spec_f64_ceil(value)), + }, + )] pub fn ceil(&self) -> Number { match self { Number::Float(f) => Number::normalize_float(f.ceil()), @@ -772,6 +1301,13 @@ impl Number { } } + #[verus_spec(result => + ensures + match self@ { + NumberView::Integer(_) => result@ == self@, + NumberView::Float(value) => result@ == normalize_float(spec_f64_round(value)), + }, + )] pub fn round(&self) -> Number { match self { Number::Float(f) => Number::normalize_float(f.round()), @@ -779,7 +1315,32 @@ impl Number { } } + #[verus_spec(result => + ensures + result matches Ok(value) && if e >= 0 { + value@ == NumberView::Integer(pow2(e as nat) as int) + } else { + NumberView::Integer(1).div_ensures( + NumberView::Integer(pow2((-(e as int)) as nat) as int), + value@, + ) + }, + )] pub fn two_pow(e: i32) -> Result { + proof! { + axiom_f64_ops_deterministic(); + if e >= 0 { + assert((e as u32) as nat == e as nat); + } else { + let exp = (-(e as i64)) as u32; + assert(exp > 0); + vstd::arithmetic::power2::lemma2_to64(); + vstd::arithmetic::power2::lemma_pow2_strictly_increases(0, exp as nat); + assert(1 < pow2(exp as nat)); + vstd::arithmetic::div_mod::lemma_small_mod(1, pow2(exp as nat)); + assert(vstd::arithmetic::div_mod::rust_rem(1, pow2(exp as nat) as int) == 1); + } + } if e >= 0 { Ok(two_pow_positive(e as u32)) } else { @@ -789,7 +1350,37 @@ impl Number { } } + #[verus_spec(result => + ensures + result matches Ok(value) && if e >= 0 { + value@ == NumberView::Integer(vstd::arithmetic::power::pow(10, e as nat)) + } else { + NumberView::Integer(1).div_ensures( + NumberView::Integer( + vstd::arithmetic::power::pow(10, (-(e as int)) as nat) + ), + value@, + ) + }, + )] pub fn ten_pow(e: i32) -> Result { + proof! { + axiom_f64_ops_deterministic(); + if e < 0 { + let exp = (-(e as i64)) as u32; + assert(exp > 0); + vstd::arithmetic::power::lemma_pow0(10); + vstd::arithmetic::power::lemma_pow_strictly_increases(10, 0, exp as nat); + assert(1 < vstd::arithmetic::power::pow(10, exp as nat)); + vstd::arithmetic::div_mod::lemma_small_mod( + 1, + vstd::arithmetic::power::pow(10, exp as nat) as nat, + ); + } else { + assert((e as u32) as nat == e as nat); + vstd::arithmetic::power::lemma_pow_positive(10, (e as u32) as nat); + } + } if e >= 0 { Ok(ten_pow_positive(e as u32)) } else { @@ -811,6 +1402,9 @@ impl Number { .unwrap_or_default() } + // Verus doesn't support format! + #[verus_verify(external_body)] + #[verus_spec(ensures true)] pub fn format_scientific(&self) -> String { match self { Number::Float(f) => format!("{:e}", f), @@ -836,6 +1430,9 @@ impl Number { } } + // Verus doesn't support format! + #[verus_verify(external_body)] + #[verus_spec(ensures true)] pub fn format_decimal_with_width(&self, d: u32) -> String { match self { Number::Float(f) => { @@ -860,17 +1457,35 @@ impl Number { } } +#[verus_spec(result => + ensures + result@ == NumberView::Integer(pow2(exp as nat) as int), +)] fn two_pow_positive(exp: u32) -> Number { if exp < 64 { + proof! { + vstd::arithmetic::power2::lemma2_to64(); + vstd::arithmetic::power2::lemma_pow2_strictly_increases(exp as nat, 64); + vstd::bits::lemma_u64_shl_is_mul(1u64, exp as u64); + } Number::UInt(1u64 << exp) } else { let mut value = BigInt::one(); + proof! { axiom_bigint_obeys_shl_assign_spec(); } value <<= exp as usize; Number::from_bigint_owned(value) } } +#[verus_spec(result => + ensures + result@ == vstd::arithmetic::power::pow(10, exp as nat), +)] fn pow10_bigint(exp: u32) -> BigInt { + proof! { + vstd::arithmetic::power::lemma_pow0(10); + } + if exp == 0 { return BigInt::one(); } @@ -879,7 +1494,31 @@ fn pow10_bigint(exp: u32) -> BigInt { let mut base = BigInt::from(10u8); let mut e = exp; + #[cfg_attr(verus_keep_ghost, verus_spec( + invariant + result@ * vstd::arithmetic::power::pow(base@, e as nat) + == vstd::arithmetic::power::pow(10, exp as nat), + decreases e, + ))] while e > 0 { + proof! { + axiom_bigint_obeys_mul_spec(); + axiom_bigint_obeys_mul_assign_ref_spec(); + assert(e & 1 == e % 2) by (bit_vector); + assert(e >> 1 == e / 2) by (bit_vector); + // `pow(base, 2) == base * base`, so squaring `base` halves `e`. + vstd::arithmetic::power::lemma_pow0(base@); + vstd::arithmetic::power::lemma_pow1(base@); + vstd::arithmetic::power::lemma_pow_adds(base@, 1, 1); + vstd::arithmetic::power::lemma_pow_multiplies(base@, 2, (e / 2) as nat); + // Peeling one factor off when `e` is odd. + vstd::arithmetic::power::lemma_pow_adds(base@, 1, (e - e % 2) as nat); + vstd::arithmetic::mul::lemma_mul_is_associative( + result@, + base@, + vstd::arithmetic::power::pow(base@, (e - e % 2) as nat), + ); + } if e & 1 == 1 { result *= &base; } @@ -889,9 +1528,15 @@ fn pow10_bigint(exp: u32) -> BigInt { e >>= 1; } + proof! { vstd::arithmetic::power::lemma_pow0(base@); } + result } +#[verus_spec(result => + ensures + result@ == NumberView::Integer(vstd::arithmetic::power::pow(10, exp as nat)), +)] fn ten_pow_positive(exp: u32) -> Number { if let Some(value) = 10u64.checked_pow(exp) { Number::UInt(value) @@ -1056,4 +1701,20 @@ mod tests { Some("modulo on floating-point number".to_string()) ); } + + #[test] + fn ten_pow_computes_negative_exponent() { + assert!(matches!( + Number::ten_pow(-3), + Ok(Number::Float(value)) if value == 0.001 + )); + } + + #[test] + fn divide_handles_minimum_i64_by_negative_one() { + assert!(matches!( + Number::Int(i64::MIN).divide(&Number::Int(-1)), + Ok(Number::UInt(value)) if value == 1u64 << 63 + )); + } } diff --git a/src/verify/bigint_assumptions.rs b/src/verify/bigint_assumptions.rs new file mode 100644 index 000000000..383807da1 --- /dev/null +++ b/src/verify/bigint_assumptions.rs @@ -0,0 +1,680 @@ +// This file contains assumptions about the BigInt library, encoded +// in Verus. +// +// 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 +)] + +use vstd::prelude::*; + +verus! { + +use core::cmp::Ordering; +use num_bigint::BigInt; +use vstd::arithmetic::div_mod::{rust_div, rust_rem}; +use vstd::arithmetic::power2::pow2; +use vstd::std_specs::cmp::OrdSpec; + +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExNumBigInt(num_bigint::BigInt); + +/// A `BigInt` is abstracted as an `int`. + +pub trait BigIntAdditionalSpecFns { + spec fn view(&self) -> int; +} + +impl BigIntAdditionalSpecFns for BigInt { + uninterp spec fn view(&self) -> int; +} + +/// Semantics for BigInt::Clone + +// We assume that `a.clone()` has the same view as `BigInt` `a`. +pub assume_specification[ ::clone ](n: &BigInt) -> (res: BigInt) + ensures + res == n, +; + +/// Addition + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// `(a + b)@ == a@ + b@. +pub axiom fn axiom_bigint_obeys_add_spec() + ensures + ::obeys_add_spec(), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::add_req(lhs, rhs), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::add_spec(lhs, rhs)@ + == lhs@ + rhs@, +; + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// `a += b` causes the resulting `a@` to be the old value of `a@` plus `b@`. +pub axiom fn axiom_bigint_obeys_add_assign_spec() + ensures + >::obeys_add_assign_spec(), + forall|value: BigInt, rhs: BigInt| #[trigger] + >::add_assign_req(&value, rhs), + forall|value: BigInt, rhs: BigInt| #[trigger] + >::add_assign_spec(&value, rhs)@ == + value@ + rhs@, +; + +/// Subtraction + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// `(a - b)@ == a@ - b@. +pub axiom fn axiom_bigint_obeys_sub_spec() + ensures + ::obeys_sub_spec(), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::sub_req(lhs, rhs), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::sub_spec(lhs, rhs)@ + == lhs@ - rhs@, +; + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// `a -= b` causes the resulting `a@` to be the old value of `a@` minus `b@`. +pub axiom fn axiom_bigint_obeys_sub_assign_spec() + ensures + >::obeys_sub_assign_spec(), + forall|value: BigInt, rhs: BigInt| #[trigger] + >::sub_assign_req(&value, rhs), + forall|value: BigInt, rhs: BigInt| #[trigger] + >::sub_assign_spec(&value, rhs)@ == + value@ - rhs@, +; + +/// Multiplication + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// `(a * b)@ == a@ * b@. +pub axiom fn axiom_bigint_obeys_mul_spec() + ensures + ::obeys_mul_spec(), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::mul_req(lhs, rhs), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::mul_spec(lhs, rhs)@ + == lhs@ * rhs@, +; + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// `a *= b` causes the resulting `a@` to be the old value of `a@` times `b@`. +pub axiom fn axiom_bigint_obeys_mul_assign_spec() + ensures + >::obeys_mul_assign_spec(), + forall|value: BigInt, rhs: BigInt| #[trigger] + >::mul_assign_req(&value, rhs), + forall|value: BigInt, rhs: BigInt| #[trigger] + >::mul_assign_spec(&value, rhs)@ == + value@ * rhs@, +; + +pub axiom fn axiom_bigint_obeys_mul_assign_ref_spec() + ensures + >::obeys_mul_assign_spec(), + forall|value: BigInt, rhs: &BigInt| #[trigger] + >::mul_assign_req(&value, rhs), + forall|value: BigInt, rhs: &BigInt| #[trigger] + >::mul_assign_spec(&value, rhs)@ == + value@ * (*rhs)@, +; + +/// Division + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// `(a / b)@ == rust_div(a@, b@), and `(a % b)@ == rust_rem(a@, b@)`. +pub axiom fn axiom_bigint_obeys_div_rem_spec() + ensures + ::obeys_div_spec(), + ::obeys_rem_spec(), + forall|lhs: BigInt, rhs: BigInt| rhs@ != 0 ==> #[trigger] + ::div_req(lhs, rhs), + forall|lhs: BigInt, rhs: BigInt| rhs@ != 0 ==> #[trigger] + ::rem_req(lhs, rhs), + forall|lhs: BigInt, rhs: BigInt| rhs@ != 0 ==> #[trigger] + ::div_spec(lhs, rhs)@ + == rust_div(lhs@, rhs@), + forall|lhs: BigInt, rhs: BigInt| rhs@ != 0 ==> #[trigger] + ::rem_spec(lhs, rhs)@ + == rust_rem(lhs@, rhs@), +; + +/// Bitwise AND + +// This function describes the result of performing a bitwise AND +// operation on two unbounded-precision integers. +pub open spec fn spec_bigint_bitand(lhs: int, rhs: int) -> int + decreases + if lhs >= 0 { lhs } else { -(lhs + 1) }, + if rhs >= 0 { rhs } else { -(rhs + 1) } +{ + let lsb: int = if (lhs % 2 == 1) && (rhs % 2 == 1) { 1int } else { 0int }; + if (lhs == 0 || lhs == -1) && (rhs == 0 || rhs == -1) { + -lsb + } + else { + spec_bigint_bitand(lhs / 2, rhs / 2) * 2 + lsb + } +} + +// To help demonstrate that the spec for `spec_bigint_bitand` is +// valid, prove that it's equivalent to `&` for arbitrary `i16` +// values. (Using 16 bits is enough for high confidence, and doesn't +// tax the bit-vector solver.) +proof fn lemma_test_spec_bigint_bitand_for_i16(lhs: i16, rhs: i16) + ensures + spec_bigint_bitand(lhs as int, rhs as int) == (lhs & rhs) as int, + decreases + if lhs >= 0 { lhs as int } else { -(lhs + 1) }, + if rhs >= 0 { rhs as int } else { -(rhs + 1) } +{ + let lsb: i16 = if (lhs % 2 == 1) && (rhs % 2 == 1) { 1i16 } else { 0i16 }; + if (lhs == 0 || lhs == -1) && (rhs == 0 || rhs == -1) { + assert(-lsb == lhs & rhs) by (bit_vector) + requires + lhs == 0 || lhs == -1, + rhs == 0 || rhs == -1, + lsb == if (lhs % 2 == 1) && (rhs % 2 == 1) { 1i16 } else { 0i16 }, + ; + } + else { + lemma_test_spec_bigint_bitand_for_i16((lhs / 2) as i16, (rhs / 2) as i16); + assert(((lhs / 2) as i16 & (rhs / 2) as i16) * 2 + lsb == lhs & rhs) by (bit_vector) + requires + lsb == if (lhs % 2 == 1) && (rhs % 2 == 1) { 1i16 } else { 0i16 }, + ; + } +} + +// To help demonstrate that the spec for `spec_bigint_bitand` +// corresponds to what's implemented by the BigInt library, prove that +// its results match examples given in comments at: +// https://docs.rs/num-bigint/latest/src/num_bigint/bigint/bits.rs.html +proof fn lemma_test_spec_bigint_bitand_with_examples() + ensures + // From documentation for bitand_pos_neg: + spec_bigint_bitand(1, -0xff) == 1, + spec_bigint_bitand(0xff, -1) == 0xff, + // From documentation for bitand_neg_pos: + spec_bigint_bitand(-1, 0xff) == 0xff, + spec_bigint_bitand(-0xff, 1) == 1, + // From documentation for bitand_neg_neg: + spec_bigint_bitand(-1, -0xff) == -0xff, + spec_bigint_bitand(-0xff, -1) == -0xff, + spec_bigint_bitand(-0xff, -0xfe) == -0x100, +{ + assert(spec_bigint_bitand(1, -0xff) == 1) by (compute); + assert(spec_bigint_bitand(0xff, -1) == 0xff) by (compute); + + assert(spec_bigint_bitand(-1, 0xff) == 0xff) by (compute); + assert(spec_bigint_bitand(-0xff, 1) == 1) by (compute); + + assert(spec_bigint_bitand(-1, -0xff) == -0xff) by (compute); + assert(spec_bigint_bitand(-0xff, -1) == -0xff) by (compute); + assert(spec_bigint_bitand(-0xff, -0xfe) == -0x100) by (compute); +} + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// (a & b)@ == spec_bigint_bitand(a@, b@). It's justified by the +// lemmas above named `lemma_test_spec_bigint_bitand_for_i16` +// and `lemma_test_spec_bigint_bitand_with_examples`. +pub axiom fn axiom_bigint_obeys_bitand_spec() + ensures + ::obeys_bitand_spec(), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::bitand_req(lhs, rhs), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::bitand_spec(lhs, rhs)@ + == spec_bigint_bitand(lhs@, rhs@), +; + +/// Bitwise OR + +// This function describes the result of performing a bitwise OR +// operation on two unbounded-precision integers. +pub open spec fn spec_bigint_bitor(lhs: int, rhs: int) -> int + decreases + if lhs >= 0 { lhs } else { -(lhs + 1) }, + if rhs >= 0 { rhs } else { -(rhs + 1) } +{ + let lsb: int = if (lhs % 2 == 1) || (rhs % 2 == 1) { 1int } else { 0int }; + if (lhs == 0 || lhs == -1) && (rhs == 0 || rhs == -1) { + -lsb + } + else { + spec_bigint_bitor(lhs / 2, rhs / 2) * 2 + lsb + } +} + +// To help demonstrate that the spec for `spec_bigint_bitor` is +// valid, prove that it's equivalent to `|` for arbitrary `i16` +// values. (Using 16 bits is enough for high confidence, and doesn't +// tax the bit-vector solver.) +proof fn lemma_test_spec_bigint_bitor_for_i16(lhs: i16, rhs: i16) + ensures + spec_bigint_bitor(lhs as int, rhs as int) == (lhs | rhs) as int, + decreases + if lhs >= 0 { lhs as int } else { -(lhs + 1) }, + if rhs >= 0 { rhs as int } else { -(rhs + 1) } +{ + let lsb: i16 = if (lhs % 2 == 1) || (rhs % 2 == 1) { 1i16 } else { 0i16 }; + if (lhs == 0 || lhs == -1) && (rhs == 0 || rhs == -1) { + assert(-lsb == lhs | rhs) by (bit_vector) + requires + lhs == 0 || lhs == -1, + rhs == 0 || rhs == -1, + lsb == if (lhs % 2 == 1) || (rhs % 2 == 1) { 1i16 } else { 0i16 }, + ; + } + else { + lemma_test_spec_bigint_bitor_for_i16((lhs / 2) as i16, (rhs / 2) as i16); + assert(((lhs / 2) as i16 | (rhs / 2) as i16) * 2 + lsb == lhs | rhs) by (bit_vector) + requires + lsb == if (lhs % 2 == 1) || (rhs % 2 == 1) { 1i16 } else { 0i16 }, + ; + } +} + +// To help demonstrate that the spec for `spec_bigint_bitor` +// corresponds to what's implemented by the BigInt library, prove that +// its results match examples given in comments at: +// https://docs.rs/num-bigint/latest/src/num_bigint/bigint/bits.rs.html +proof fn lemma_test_spec_bigint_bitor_with_examples() + ensures + // From documentation for bitor_pos_neg: + spec_bigint_bitor(1, -0xff) == -0xff, + spec_bigint_bitor(0xff, -1) == -1, + + // From documentation for bitor_neg_pos: + spec_bigint_bitor(-1, 0xff) == -1, + spec_bigint_bitor(-0xff, 1) == -0xff, + + // From documentation for bitor_neg_neg: + spec_bigint_bitor(-1, -0xff) == -1, + spec_bigint_bitor(-0xff, -1) == -1, +{ + assert(spec_bigint_bitor(1, -0xff) == -0xff) by (compute); + assert(spec_bigint_bitor(0xff, -1) == -1) by (compute); + + assert(spec_bigint_bitor(-1, 0xff) == -1) by (compute); + assert(spec_bigint_bitor(-0xff, 1) == -0xff) by (compute); + + assert(spec_bigint_bitor(-1, -0xff) == -1) by (compute); + assert(spec_bigint_bitor(-0xff, -1) == -1) by (compute); +} + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// (a | b)@ == spec_bigint_bitor(a@, b@). It's justified by the +// lemmas above named `lemma_test_spec_bigint_bitor_for_i16` +// and `lemma_test_spec_bigint_bitor_with_examples`. +pub axiom fn axiom_bigint_obeys_bitor_spec() + ensures + ::obeys_bitor_spec(), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::bitor_req(lhs, rhs), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::bitor_spec(lhs, rhs)@ + == spec_bigint_bitor(lhs@, rhs@), +; + +/// Bitwise XOR + +// This function describes the result of performing a bitwise XOR +// operation on two unbounded-precision integers. +pub open spec fn spec_bigint_bitxor(lhs: int, rhs: int) -> int + decreases + if lhs >= 0 { lhs } else { -(lhs + 1) }, + if rhs >= 0 { rhs } else { -(rhs + 1) } +{ + let lsb: int = if (lhs % 2 == 1) != (rhs % 2 == 1) { 1int } else { 0int }; + if (lhs == 0 || lhs == -1) && (rhs == 0 || rhs == -1) { + -lsb + } + else { + spec_bigint_bitxor(lhs / 2, rhs / 2) * 2 + lsb + } +} + +// To help demonstrate that the spec for `spec_bigint_bitxor` is +// valid, prove that it's equivalent to `^` for arbitrary `i16` +// values. (Using 16 bits is enough for high confidence, and doesn't +// tax the bit-vector solver.) +proof fn lemma_test_spec_bigint_bitxor_for_i16(lhs: i16, rhs: i16) + ensures + spec_bigint_bitxor(lhs as int, rhs as int) == (lhs ^ rhs) as int, + decreases + if lhs >= 0 { lhs as int } else { -(lhs + 1) }, + if rhs >= 0 { rhs as int } else { -(rhs + 1) } +{ + let lsb: i16 = if (lhs % 2 == 1) != (rhs % 2 == 1) { 1i16 } else { 0i16 }; + if (lhs == 0 || lhs == -1) && (rhs == 0 || rhs == -1) { + assert(-lsb == lhs ^ rhs) by (bit_vector) + requires + lhs == 0 || lhs == -1, + rhs == 0 || rhs == -1, + lsb == if (lhs % 2 == 1) != (rhs % 2 == 1) { 1i16 } else { 0i16 }, + ; + } + else { + lemma_test_spec_bigint_bitxor_for_i16((lhs / 2) as i16, (rhs / 2) as i16); + assert(((lhs / 2) as i16 ^ (rhs / 2) as i16) * 2 + lsb == lhs ^ rhs) by (bit_vector) + requires + lsb == if (lhs % 2 == 1) != (rhs % 2 == 1) { 1i16 } else { 0i16 }, + ; + } +} + +// To help demonstrate that the spec for `spec_bigint_bitxor` +// corresponds to what's implemented by the BigInt library, prove that +// its results match examples given in comments at: +// https://docs.rs/num-bigint/latest/src/num_bigint/bigint/bits.rs.html +proof fn lemma_test_spec_bigint_bitxor_with_examples() + ensures + // From documentation for bitxor_pos_neg: + spec_bigint_bitxor(1, -0xff) == -0x100, + spec_bigint_bitxor(0xff, -1) == -0x100, + + // From documentation for bitxor_neg_pos: + spec_bigint_bitxor(-1, 0xff) == -0x100, + spec_bigint_bitxor(-0xff, 1) == -0x100, + + // From documentation for bitxor_neg_neg: + spec_bigint_bitxor(-1, -0xff) == 0xfe, + spec_bigint_bitxor(-0xff, -1) == 0xfe, +{ + assert(spec_bigint_bitxor(1, -0xff) == -0x100) by (compute); + assert(spec_bigint_bitxor(0xff, -1) == -0x100) by (compute); + + assert(spec_bigint_bitxor(-1, 0xff) == -0x100) by (compute); + assert(spec_bigint_bitxor(-0xff, 1) == -0x100) by (compute); + + assert(spec_bigint_bitxor(-1, -0xff) == 0xfe) by (compute); + assert(spec_bigint_bitxor(-0xff, -1) == 0xfe) by (compute); +} + +// This axiom says that, for any pair of `BigInt`s `a` and `b`, +// (a | b)@ == spec_bigint_bitxor(a@, b@). It's justified by the +// lemmas above named `lemma_test_spec_bigint_bitxor_for_i16` +// and `lemma_test_spec_bigint_bitxor_with_examples`. +pub axiom fn axiom_bigint_obeys_bitxor_spec() + ensures + ::obeys_bitxor_spec(), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::bitxor_req(lhs, rhs), + forall|lhs: BigInt, rhs: BigInt| #[trigger] + ::bitxor_spec(lhs, rhs)@ + == spec_bigint_bitxor(lhs@, rhs@), +; + +/// Bitwise NOT + +// This axiom says that, for `BigInt` `a`, `(~a)@ == -a@ - 1`. +// This corresponds to twos-complement bitwise negation. +pub axiom fn axiom_bigint_not_spec(value: BigInt) + ensures + ::obeys_not_spec(), + ::not_req(value), + ::not_spec(value)@ == -(value@) - 1, +; + +/// Bitwise shifting + +// This axiom says that BigInt supports the expected semantics for +// core::ops::ShrAssign, i.e., `>>=`. That is, for any BigInt 'a' and +// any shift amount `u: usize`, `a >>= u` causes the resulting `a@` to +// be the old `a@` shifted right by `u` bits. +pub axiom fn axiom_bigint_obeys_shr_assign_spec() + ensures + >::obeys_shr_assign_spec(), + forall|value: BigInt, shift: usize| #[trigger] + >::shr_assign_req(&value, shift), + forall|value: BigInt, shift: usize| #[trigger] + >::shr_assign_spec(&value, shift)@ == + value@ / pow2(shift as nat) as int, +; + +// This axiom says that BigInt supports the expected semantics for +// core::ops::ShlAssign, i.e., `<<=`. That is, for any BigInt 'a' and +// any shift amount `u: usize`, `a <<= u` causes the resulting `a@` to +// be the old `a@` shifted left by `u` bits. +pub axiom fn axiom_bigint_obeys_shl_assign_spec() + ensures + >::obeys_shl_assign_spec(), + forall|value: BigInt, shift: usize| #[trigger] + >::shl_assign_req(&value, shift), + forall|value: BigInt, shift: usize| #[trigger] + >::shl_assign_spec(&value, shift)@ == + value@ * pow2(shift as nat) as int, +; + +/// Unary operations + +// We assume that `x.is_zero()` gives the same result as `x@ == 0`. +pub assume_specification[ ::is_zero ](x: &BigInt) -> (res: bool) + ensures + res == (x@ == 0), +; + +// We assume that `x.is_negative()` gives the same result as `x@ < 0`. +pub assume_specification[ ::is_negative ](x: &BigInt) -> (res: bool) + ensures + res == (x@ < 0), +; + +// We assume that `x.abs()` produces a `BigInt` `y` such that `y@ == abs(x@)`. +pub assume_specification[ ::abs ](x: &BigInt) -> (res: BigInt) + ensures + res@ == if x@ < 0 { -x@ } else { x@ }, +; + +// This is the specification for what `BigInt::bits` produces. +// According to the documentation +// (https://docs.rs/num-bigint/latest/num_bigint/struct.BigInt.html#method.bits), +// it's the fewest bits necessary to express its value, not including the sign. +pub open spec fn bigint_bits_ensures(value: int, bits: nat) -> bool +{ + &&& -(pow2(bits) as int) < value < pow2(bits) + &&& forall|n: nat| #![trigger pow2(n)] n < bits ==> + !( -(pow2(n) as int) < value < pow2(n) ) +} + +pub assume_specification[ BigInt::bits ](x: &BigInt) -> (res: u64) + ensures + bigint_bits_ensures(x@, res as nat), +; + +/// Negation + +// This axiom says that, for `BigInt` `a`, `(-a)@ == -a@`. +pub axiom fn axiom_bigint_neg_spec(value: BigInt) + ensures + ::obeys_neg_spec(), + ::neg_req(value), + ::neg_spec(value)@ == -value@, +; + +/// Formatting + +// Nothing is promised about the rendered digits; callers only need this to be +// callable from verified code. +pub assume_specification[ BigInt::to_str_radix ](x: &BigInt, radix: u32) -> (res: + alloc::string::String); + +/// Equality + +// This axiom says that if we execute `a == b` for two `BigInt`s `a` and `b`, +// the result is equal to `a@ == b@`. +pub axiom fn axiom_bigint_obeys_eq_spec() + ensures + ::obeys_eq_spec(), + forall|a: BigInt, b: BigInt| #[trigger] + ::eq_spec(&a, &b) == (a@ == b@), +; + +/// Comparison + +// This axiom says that comparison operators on `BigInt`s return what would +// result from comparing their views. +pub axiom fn axiom_bigint_obeys_cmp_spec() + ensures + ::obeys_cmp_spec(), + forall|b1: &BigInt, b2: &BigInt| match #[trigger] b1.cmp_spec(b2) { + Ordering::Less => b1@ < b2@, + Ordering::Greater => b1@ > b2@, + Ordering::Equal => b1@ == b2@, + }, +; + +/// From + +// We assume that `BigInt::from(i)` where `i` has type `i64` produces a `BigInt` +// whose view equals `i`. +pub assume_specification[ >::from ](i: i64) -> (res: BigInt) + ensures + res@ == i, +; + +// We assume that `BigInt::from(i)` where `i` has type `i128` produces a `BigInt` +// whose view equals `i`. +pub assume_specification[ >::from ](i: i128) -> (res: BigInt) + ensures + res@ == i, +; + +// We assume that `BigInt::from(u)` where `u` has type `u64` produces a `BigInt` +// whose view equals `u`. +pub assume_specification[ >::from ](u: u64) -> (res: BigInt) + ensures + res@ == u, +; + +// We assume that `BigInt::from(u)` where `u` has type `u128` produces a `BigInt` +// whose view equals `u`. +pub assume_specification[ >::from ](u: u128) -> (res: BigInt) + ensures + res@ == u, +; + +// We assume that `BigInt::from(u)` where `u` has type `u8` produces a `BigInt` +// whose view equals `u`. +pub assume_specification[ >::from ](u: u8) -> (res: BigInt) + ensures + res@ == u, +; + +/// BigInt::one + +// We assume that `BigInt::one` produces a value whose view is 1. +pub assume_specification[ ::one ]() -> (res: BigInt) + ensures + res@ == 1, +; + +// ToPrimitive + +// Verus does not support `assume_specification` for provided trait methods, so +// `to_u32` needs a minimal external trait specification. BigInt's overridden +// conversion methods are specified directly below. +#[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_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, + ; +} + +impl ToPrimitiveSpecImpl for BigInt { + open spec fn obeys_to_primitive_spec() -> bool + { + true + } + + open spec fn spec_to_int(&self) -> Option + { + Some(self@) + } +} + +// We assume that `b.to_i64()` where `b` is of type `BigInt` produces `Some(i)` +// if its view `i` is in the range of an `i64` and `None` otherwise. +pub assume_specification[ ::to_i64 ](x: &BigInt) -> (res: Option) + ensures + match res { + Some(value) => x@ == value, + None => !(i64::MIN <= x@ <= i64::MAX), + }, +; + +// We assume that `b.to_i128()` where `b` is of type `BigInt` produces `Some(i)` +// if its view `i` is in the range of an `i128` and `None` otherwise. +pub assume_specification[ ::to_i128 ](x: &BigInt) -> (res: Option) + ensures + match res { + Some(value) => x@ == value, + None => !(i128::MIN <= x@ <= i128::MAX), + }, +; + +// We assume that `b.to_u64()` where `b` is of type `BigInt` produces `Some(u)` +// if its view `u` is in the range of a `u64` and `None` otherwise. +pub assume_specification[ ::to_u64 ](x: &BigInt) -> (res: Option) + ensures + match res { + Some(value) => x@ == value, + None => !(u64::MIN <= x@ <= u64::MAX), + }, +; + +// We assume that `b.to_u128()` where `b` is of type `BigInt` produces `Some(u)` +// if its view `u` is in the range of a `u128` and `None` otherwise. +pub assume_specification[ ::to_u128 ](x: &BigInt) -> (res: Option) + ensures + match res { + Some(value) => x@ == value, + None => !(u128::MIN <= x@ <= u128::MAX), + }, +; + +pub uninterp spec fn spec_bigint_to_f64(x: &BigInt) -> Option; + +// We define the value returned by `b.to_f64()` as `spec_bigint_to_f64(&b)`. +// We assume that this is `Some` if `b` is in the range -2^53 to 2^53 inclusive. +// (It may be `Some` elsewhere; we don't assume either way.) +pub assume_specification[ ::to_f64 ](x: &BigInt) -> (res: Option) + ensures + res == spec_bigint_to_f64(x), + -9_007_199_254_740_992 <= x@ <= 9_007_199_254_740_992 ==> res is Some, +; + +} // end verus! diff --git a/src/verify/bigint_proofs.rs b/src/verify/bigint_proofs.rs new file mode 100644 index 000000000..ae24bd705 --- /dev/null +++ b/src/verify/bigint_proofs.rs @@ -0,0 +1,31 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +use vstd::prelude::*; + +verus! { + +use super::bigint_assumptions::bigint_bits_ensures; +use vstd::arithmetic::power2::{lemma2_to64_rest, lemma_pow2_strictly_increases, pow2}; + +pub proof fn lemma_bigint_bits_le_53() + ensures + forall|value: int, bits: nat| #[trigger] bigint_bits_ensures(value, bits) ==> + ((bits <= 53) == (-9_007_199_254_740_992 < value < 9_007_199_254_740_992)), +{ + lemma2_to64_rest(); + assert(pow2(53) == 9_007_199_254_740_992); + assert forall|value: int, bits: nat| #[trigger] bigint_bits_ensures(value, bits) implies + ((bits <= 53) == (-9_007_199_254_740_992 < value < 9_007_199_254_740_992)) by + { + if bigint_bits_ensures(value, bits) { + if bits < 53 { + lemma_pow2_strictly_increases(bits, 53); + } else if bits > 53 { + assert(!( -(pow2(53) as int) < value < pow2(53) )); + } + } + } +} + +} diff --git a/src/verify/f64_assumptions.rs b/src/verify/f64_assumptions.rs new file mode 100644 index 000000000..ce990f576 --- /dev/null +++ b/src/verify/f64_assumptions.rs @@ -0,0 +1,173 @@ +// This file contains assumptions about `f64`, encoded in Verus. +// +// 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 +)] + +use vstd::prelude::*; + +verus! { + +use vstd::float::*; +use vstd::std_specs::cmp::PartialEqIs; +use vstd::std_specs::cmp::PartialOrdIs; + +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|lhs: f64, rhs: f64| #[trigger] + ::add_req(lhs, rhs), + forall|lhs: f64, rhs: f64| #[trigger] + ::add_spec(lhs, rhs) + == lhs.ieee_add(rhs), + forall|lhs: f64, rhs: f64| #[trigger] + ::sub_req(lhs, rhs), + forall|lhs: f64, rhs: f64| #[trigger] + ::sub_spec(lhs, rhs) + == lhs.ieee_sub(rhs), + forall|lhs: f64, rhs: f64| #[trigger] + ::mul_req(lhs, rhs), + forall|lhs: f64, rhs: f64| #[trigger] + ::mul_spec(lhs, rhs) + == lhs.ieee_mul(rhs), + forall|lhs: f64, rhs: f64| #[trigger] + ::div_req(lhs, rhs), + forall|lhs: f64, rhs: f64| #[trigger] + ::div_spec(lhs, rhs) + == lhs.ieee_div(rhs), + 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), +; + +// The executable test in `f64_tests.rs` validates these casts and justifies +// this axiom. +pub axiom fn axiom_f64_safe_integer_casts() + ensures + ieee_float_cast::(9_007_199_254_740_992.0f64) == 9_007_199_254_740_992u64, + ieee_float_cast::(9_007_199_254_740_992.0f64) == 9_007_199_254_740_992i128, +; + +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) + ensures + res == spec_f64_abs(f), +; + +pub assume_specification [ ::abs ](f: &f64) -> (res: f64) + ensures + res == spec_f64_abs(*f), +; + +pub uninterp spec fn spec_f64_floor(f: f64) -> f64; + +pub assume_specification [ f64::floor ](f: f64) -> (res: f64) + ensures + res == spec_f64_floor(f), +; + +pub uninterp spec fn spec_f64_ceil(f: f64) -> f64; + +pub assume_specification [ f64::ceil ](f: f64) -> (res: f64) + ensures + res == spec_f64_ceil(f), +; + +pub uninterp spec fn spec_f64_round(f: f64) -> f64; + +pub assume_specification [ f64::round ](f: f64) -> (res: f64) + ensures + res == spec_f64_round(f), +; + +pub assume_specification [ f64::is_nan ](f: f64) -> (res: bool) + ensures + res == f.is_nan_spec(), +; + +pub uninterp spec fn spec_f64_is_sign_positive(f: f64) -> bool; + +pub assume_specification [ f64::is_sign_positive ](f: f64) -> (res: bool) + ensures + res == spec_f64_is_sign_positive(f), +; + +pub uninterp spec fn spec_f64_neg_infinity() -> f64; + +pub uninterp spec fn spec_f64_infinity() -> f64; + +pub assume_specification[ f64::NEG_INFINITY ] -> (res: f64) + ensures + res == spec_f64_neg_infinity(), +; + +pub assume_specification[ f64::INFINITY ] -> (res: f64) + ensures + res == spec_f64_infinity(), +; + +} // end verus! diff --git a/src/verify/f64_tests.rs b/src/verify/f64_tests.rs new file mode 100644 index 000000000..c5920fa28 --- /dev/null +++ b/src/verify/f64_tests.rs @@ -0,0 +1,14 @@ +// This file contains executable tests that justify the assumptions about `f64` +// declared in `f64_assumptions.rs`. +// +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. +#![allow(clippy::as_conversions, clippy::unseparated_literal_suffix)] + +#[test] +fn f64_safe_integer_casts_match_runtime() { + let safe_integer = 9_007_199_254_740_992.0f64; + + assert_eq!(safe_integer as u64, 9_007_199_254_740_992u64); + assert_eq!(safe_integer as i128, 9_007_199_254_740_992i128); +} diff --git a/src/verify/mod.rs b/src/verify/mod.rs new file mode 100644 index 000000000..5a26bccea --- /dev/null +++ b/src/verify/mod.rs @@ -0,0 +1,16 @@ +#[cfg(verus_keep_ghost)] +pub(crate) mod bigint_assumptions; +#[cfg(verus_keep_ghost)] +pub(crate) mod bigint_proofs; +#[cfg(verus_keep_ghost)] +pub(crate) mod f64_assumptions; +#[cfg(test)] +mod f64_tests; +#[cfg(verus_keep_ghost)] +pub(crate) mod num_assumptions; +#[cfg(verus_keep_ghost)] +pub(crate) mod number_proofs; +#[cfg(verus_keep_ghost)] +pub mod number_specs; +#[cfg(verus_keep_ghost)] +pub(crate) mod utils; diff --git a/src/verify/num_assumptions.rs b/src/verify/num_assumptions.rs new file mode 100644 index 000000000..a4ce7cca6 --- /dev/null +++ b/src/verify/num_assumptions.rs @@ -0,0 +1,37 @@ +// This file contains assumptions about Rust's primitive numeric types, +// encoded in Verus. +// +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +use vstd::prelude::*; + +verus! { + +use vstd::arithmetic::power::pow; + +pub assume_specification[ i128::abs ](value: i128) -> (res: i128) + requires + value != i128::MIN, + ensures + res as int == if value < 0 { -(value as int) } else { value as int }, +; + +pub assume_specification[ i64::checked_abs ](value: i64) -> (res: Option) + ensures + if value == i64::MIN { + res is None + } else { + res matches Some(abs) && abs as int == if value < 0 { -(value as int) } else { value as int } + }, +; + +pub assume_specification[ u64::checked_pow ](x: u64, exp: u32) -> (res: Option) + ensures + match res { + Some(value) => value == pow(x as int, exp as nat), + None => pow(x as int, exp as nat) > u64::MAX, + }, +; + +} // end verus! diff --git a/src/verify/number_proofs.rs b/src/verify/number_proofs.rs new file mode 100644 index 000000000..d5064419a --- /dev/null +++ b/src/verify/number_proofs.rs @@ -0,0 +1,487 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +use vstd::prelude::*; + +verus! { + +use core::cmp::Ordering; +use crate::number::Number; +use num_bigint::BigInt; +use super::bigint_assumptions::*; +use super::number_specs::NumberView; +use vstd::arithmetic::div_mod::{ + lemma_div_of0, + lemma_fundamental_div_mod, + rust_div, + rust_rem, +}; +use vstd::arithmetic::mul::{ + lemma_mul_cancels_negatives, + lemma_mul_increases, + lemma_mul_strictly_increases, + lemma_mul_unary_negation, +}; +use vstd::float::*; +use vstd::std_specs::cmp::*; +use vstd::std_specs::convert::*; +use vstd::std_specs::ops::*; + +/// Spec trait implementations + +// For various `T`, we implement `From` for `Number`. This means +// that Verus demands a proof that it implements `FromSpecImpl`. +// The easiest (and most obviously correct) way to do this is to just +// define `obeys_from_spec()` as always returning `false`. We also +// need to define a `from_spec`, but it's meaningless since +// `obeys_from_spec()` always returns false. So we may as well leave +// it uninterpreted. + +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; +} + +// We implement `PartialEq` for `Number`. This means that Verus +// demands a proof that it implements `PartialEqSpecImpl`. The +// simplest, and most obviously correct, way to do this is to just say +// that `obeys_eq_spec()` always returns `false`. This makes all the +// postconditions trivial. We also need to define an `eq_spec`, but +// it's meaningless since `obeys_from_spec()` always returns false. So +// we may as well leave it uninterpreted. + +impl PartialEqSpecImpl for Number { + open spec fn obeys_eq_spec() -> bool + { + false + } + + uninterp spec fn eq_spec(&self, other: &Self) -> bool; +} + +// We implement `Ord` for `Number`. This means that Verus demands a +// proof that it implements `OrdSpecImpl`. The simplest, and most +// obviously correct, way to do this is to just say that +// `obeys_eq_spec()` always returns `false`. This makes all the +// postconditions trivial. We also need to define a `cmp_spec`, but +// it's meaningless since `obeys_from_spec()` always returns false. So +// we may as well leave it uninterpreted. + +impl OrdSpecImpl for Number { + open spec fn obeys_cmp_spec() -> bool + { + false + } + + uninterp spec fn cmp_spec(&self, other: &Self) -> Ordering; +} + +/// View implementation (internal to crate) + +impl View for Number +{ + type V = NumberView; + + open(crate) 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@), + } + } +} + +/// Helpful lemmas + +pub proof fn lemma_div_ensures_cases(lhs: NumberView, rhs: NumberView) + ensures + match (lhs, rhs) { + (NumberView::Integer(integer_lhs), NumberView::Integer(divisor)) => { + divisor != 0 && rust_rem(integer_lhs, divisor) == 0 + ==> lhs.div_ensures( + rhs, + NumberView::Integer(rust_div(integer_lhs, divisor)), + ) + }, + _ => true, + }, + forall|lhs_float: f64, rhs_float: f64| + lhs is Integer && rhs is Integer && rhs->Integer_0 != 0 && rust_rem( + lhs->Integer_0, + rhs->Integer_0, + ) != 0 && lhs.to_f64_lossy_ensures(lhs_float) && rhs.to_f64_lossy_ensures(rhs_float) + ==> #[trigger] lhs.div_ensures(rhs, NumberView::Float(lhs_float / rhs_float)), + forall|lhs_float: f64, rhs_float: f64| + (lhs is Float || rhs is Float) && !rhs.is_zero() && lhs.to_f64_lossy_ensures(lhs_float) + && rhs.to_f64_lossy_ensures(rhs_float) + ==> #[trigger] lhs.div_ensures(rhs, NumberView::Float(lhs_float / rhs_float)), +{ + reveal(NumberView::is_zero); + reveal(NumberView::div_ensures); +} + +proof fn lemma_rust_div_rem_identity(lhs: int, rhs: int) + requires + rhs != 0, + ensures + lhs == rhs * rust_div(lhs, rhs) + rust_rem(lhs, rhs), +{ + reveal(rust_div); + reveal(rust_rem); + if lhs == 0 { + lemma_div_of0(rhs); + lemma_fundamental_div_mod(lhs, rhs); + } else if lhs > 0 { + lemma_fundamental_div_mod(lhs, rhs); + } else { + let positive_lhs = -lhs; + let quotient = positive_lhs / rhs; + let remainder = positive_lhs % rhs; + lemma_fundamental_div_mod(positive_lhs, rhs); + lemma_mul_unary_negation(rhs, quotient); + assert(positive_lhs == rhs * quotient + remainder); + assert(rhs * (-quotient) == -(rhs * quotient)); + assert(lhs == rhs * (-quotient) + (-remainder)); + assert(rust_div(lhs, rhs) == -quotient); + assert(rust_rem(lhs, rhs) == -remainder); + } +} + +proof fn lemma_exact_rust_div_fits( + dividend: int, + divisor: int, + minimum: int, + maximum: int, +) + requires + minimum == -maximum - 1, + minimum <= dividend <= maximum, + minimum <= divisor <= maximum, + divisor != 0, + !(dividend == minimum && divisor == -1), + rust_rem(dividend, divisor) == 0, + ensures + minimum <= rust_div(dividend, divisor) <= maximum, +{ + let quotient = rust_div(dividend, divisor); + lemma_rust_div_rem_identity(dividend, divisor); + assert(dividend == divisor * quotient); + + if quotient < minimum { + assert(quotient <= minimum - 1); + assert(-quotient > maximum); + if divisor > 0 { + lemma_mul_increases(divisor, -quotient); + lemma_mul_unary_negation(divisor, quotient); + assert(divisor * quotient <= quotient); + assert(dividend < minimum); + } else { + assert(divisor <= -1); + lemma_mul_increases(-divisor, -quotient); + lemma_mul_cancels_negatives(divisor, quotient); + assert(dividend > maximum); + } + } else if quotient > maximum { + assert(quotient >= maximum + 1); + assert(quotient >= -minimum); + if divisor > 0 { + lemma_mul_increases(divisor, quotient); + assert(dividend > maximum); + } else { + assert(divisor <= -1); + lemma_mul_increases(-divisor, quotient); + lemma_mul_unary_negation(divisor, quotient); + assert(dividend <= minimum); + assert(dividend == minimum); + if divisor < -1 { + lemma_mul_strictly_increases(-divisor, quotient); + assert(quotient < (-divisor) * quotient); + assert((-divisor) * quotient == -dividend); + assert(false); + } + assert(divisor == -1); + } + } +} + +pub proof fn lemma_rust_div_fits_i64(lhs: i64, rhs: i64) + requires + rhs != 0, + !(lhs == i64::MIN && rhs == -1), + rust_rem(lhs as int, rhs as int) == 0, + ensures + i64::MIN as int <= rust_div(lhs as int, rhs as int) <= i64::MAX as int, +{ + lemma_exact_rust_div_fits( + lhs as int, + rhs as int, + i64::MIN as int, + i64::MAX as int, + ); +} + +pub proof fn lemma_checked_div_matches_rust_i64(lhs: i64, rhs: i64, quotient: i64) + requires + rhs != 0, + !(lhs == i64::MIN && rhs == -1), + rust_rem(lhs as int, rhs as int) == 0, + i64::checked_div(lhs, rhs) == Some(quotient), + ensures + quotient as int == rust_div(lhs as int, rhs as int), +{ + let mathematical_quotient = rust_div(lhs as int, rhs as int); + lemma_rust_div_fits_i64(lhs, rhs); + assert(i64::MIN as int <= mathematical_quotient <= i64::MAX as int); + assert(quotient == mathematical_quotient as i64); +} + +pub proof fn lemma_remainder_matches_rust_i64(lhs: i64, rhs: i64) + requires + rhs != 0, + !(lhs == i64::MIN && rhs == -1), + ensures + ::obeys_rem_spec(), + ::rem_req(lhs, rhs), + ::rem_spec(lhs, rhs) as int == rust_rem(lhs as int, rhs as int), +{ + assert(::obeys_rem_spec()); + assert(::rem_req(lhs, rhs)); + reveal(rust_rem); +} + +pub proof fn lemma_remainder_matches_rust_i128(lhs: i128, rhs: i128) + requires + rhs != 0, + !(lhs == i128::MIN && rhs == -1), + ensures + ::obeys_rem_spec(), + ::rem_req(lhs, rhs), + ::rem_spec(lhs, rhs) as int == rust_rem(lhs as int, rhs as int), +{ + assert(::obeys_rem_spec()); + assert(::rem_req(lhs, rhs)); + reveal(rust_rem); +} + +pub proof fn lemma_remainder_matches_rust_u64(lhs: u64, rhs: u64) + requires + rhs != 0, + ensures + ::obeys_rem_spec(), + ::rem_req(lhs, rhs), + rust_rem(lhs as int, rhs as int) == 0 ==> + ::rem_spec(lhs, rhs) == 0, + ::rem_spec(lhs, rhs) != 0 ==> + rust_rem(lhs as int, rhs as int) != 0, +{ + assert(::obeys_rem_spec()); + assert(::rem_req(lhs, rhs)); + reveal(rust_rem); + if rust_rem(lhs as int, rhs as int) == 0 { + if lhs == 0 { + lemma_div_of0(rhs as int); + } else { + assert(lhs > 0); + } + assert((lhs as int) % (rhs as int) == 0); + assert(::rem_spec(lhs, rhs) + == ((lhs as int) % (rhs as int)) as u64); + } +} + +pub proof fn lemma_number_primitive_division_facts(lhs: &Number, rhs: &Number) + ensures + match (lhs, rhs) { + (Number::Int(lhs), Number::Int(rhs)) => + *rhs != 0 && !(*lhs == i64::MIN && *rhs == -1) ==> + ::obeys_rem_spec() + && ::rem_req(*lhs, *rhs) + && ::rem_spec(*lhs, *rhs) as int + == rust_rem(*lhs as int, *rhs as int), + (Number::UInt(lhs), Number::UInt(rhs)) => + *rhs != 0 ==> + ::obeys_rem_spec() + && ::rem_req(*lhs, *rhs) + && (rust_rem(*lhs as int, *rhs as int) == 0 ==> + ::rem_spec(*lhs, *rhs) == 0) + && (::rem_spec(*lhs, *rhs) != 0 ==> + rust_rem(*lhs as int, *rhs as int) != 0), + (Number::Int(lhs), Number::UInt(rhs)) => + *rhs != 0 ==> + *rhs as i128 > 0 + && ::obeys_rem_spec() + && ::rem_req(*lhs as i128, *rhs as i128) + && ::rem_spec(*lhs as i128, *rhs as i128) as int + == rust_rem(*lhs as int, *rhs as int) + && (rust_rem(*lhs as int, *rhs as int) == 0 ==> + i128::MIN as int <= rust_div(*lhs as int, *rhs as int) + <= i128::MAX as int), + (Number::UInt(lhs), Number::Int(rhs)) => + *rhs != 0 ==> + *lhs as i128 >= 0 + && *rhs as i128 != 0 + && rust_div(*lhs as int, *rhs as int) + == (*lhs as int) / (*rhs as int) + && ::obeys_rem_spec() + && ::rem_req(*lhs as i128, *rhs as i128) + && (rust_rem(*lhs as int, *rhs as int) == 0 ==> + ::rem_spec(*lhs as i128, *rhs as i128) == 0) + && (::rem_spec(*lhs as i128, *rhs as i128) != 0 ==> + rust_rem(*lhs as int, *rhs as int) != 0) + && (rust_rem(*lhs as int, *rhs as int) == 0 ==> + i128::MIN as int <= rust_div(*lhs as int, *rhs as int) + <= i128::MAX as int), + _ => true, + }, +{ + match (lhs, rhs) { + (Number::Int(lhs), Number::Int(rhs)) => { + if *rhs != 0 && !(*lhs == i64::MIN && *rhs == -1) { + lemma_remainder_matches_rust_i64(*lhs, *rhs); + } + }, + (Number::UInt(lhs), Number::UInt(rhs)) => { + if *rhs != 0 { + lemma_remainder_matches_rust_u64(*lhs, *rhs); + } + }, + (Number::Int(lhs), Number::UInt(rhs)) => { + if *rhs != 0 { + lemma_remainder_matches_rust_i128(*lhs as i128, *rhs as i128); + if rust_rem(*lhs as int, *rhs as int) == 0 { + lemma_rust_div_fits_i128(*lhs as i128, *rhs as i128); + } + } + }, + (Number::UInt(lhs), Number::Int(rhs)) => { + if *rhs != 0 { + lemma_nonnegative_div_matches_rust(*lhs as i128, *rhs as i128); + lemma_nonnegative_remainder_matches_rust(*lhs as i128, *rhs as i128); + if rust_rem(*lhs as int, *rhs as int) == 0 { + lemma_rust_div_fits_i128(*lhs as i128, *rhs as i128); + } + } + }, + _ => {}, + } +} + +pub proof fn lemma_rust_div_fits_i128(lhs: i128, rhs: i128) + requires + rhs != 0, + !(lhs == i128::MIN && rhs == -1), + rust_rem(lhs as int, rhs as int) == 0, + ensures + i128::MIN as int <= rust_div(lhs as int, rhs as int) <= i128::MAX as int, +{ + lemma_exact_rust_div_fits( + lhs as int, + rhs as int, + i128::MIN as int, + i128::MAX as int, + ); +} + +pub proof fn lemma_nonnegative_div_matches_rust(lhs: i128, rhs: i128) + requires + lhs >= 0, + rhs != 0, + ensures + rust_div(lhs as int, rhs as int) == (lhs as int) / (rhs as int), +{ + reveal(rust_div); + if lhs == 0 { + lemma_div_of0(rhs as int); + } else { + assert(lhs > 0); + } +} + +pub proof fn lemma_nonnegative_remainder_matches_rust(lhs: i128, rhs: i128) + requires + lhs >= 0, + rhs != 0, + ensures + ::obeys_rem_spec(), + ::rem_req(lhs, rhs), + rust_rem(lhs as int, rhs as int) == 0 ==> + ::rem_spec(lhs, rhs) == 0, + ::rem_spec(lhs, rhs) != 0 ==> + rust_rem(lhs as int, rhs as int) != 0, +{ + assert(::obeys_rem_spec()); + assert(::rem_req(lhs, rhs)); + reveal(rust_rem); + if rust_rem(lhs as int, rhs as int) == 0 { + if lhs == 0 { + lemma_div_of0(rhs as int); + } else { + assert(lhs > 0); + } + assert((lhs as int) % (rhs as int) == 0); + assert(::rem_spec(lhs, rhs) + == ((lhs as int) % (rhs as int)) as i128); + } +} + +} diff --git a/src/verify/number_specs.rs b/src/verify/number_specs.rs new file mode 100644 index 000000000..32cb66be0 --- /dev/null +++ b/src/verify/number_specs.rs @@ -0,0 +1,186 @@ +// This file contains specifications for `Number` and its methods. +// +// 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 +)] + +use vstd::prelude::*; + +verus! { + +use crate::number::*; +use super::bigint_assumptions::*; +use super::f64_assumptions::*; +use vstd::float::*; +use vstd::std_specs::cmp::PartialEqSpec; + +pub assume_specification[ ::clone ](n: &Number) -> (res: Number) + ensures + res@ == n@, +; + +pub enum NumberView { + Integer(int), + Float(f64), +} + +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 { + let value_as_u64 = ieee_float_cast::(value); + if ieee_float_cast::(value_as_u64).eq_spec(&value) { + Some(value_as_u64 as int) + } + else { + None + } + } + else { + let value_as_i64 = ieee_float_cast::(value); + if ieee_float_cast::(value_as_i64).eq_spec(&value) { + Some(ieee_float_cast::(value) as int) + } + else { + None + } + } +} + +pub open spec fn normalize_float(value: f64) -> NumberView +{ + match float_to_small_int(value) { + Some(n) => NumberView::Integer(n), + None => NumberView::Float(value), + } +} + +impl NumberView { + pub open spec fn is_zero(&self) -> bool + { + match *self { + Self::Integer(n) => n == 0, + Self::Float(f) => f.eq_spec(&0.0f64), + } + } + + 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] super::bigint_assumptions::spec_bigint_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, + } + } + + pub open spec fn add_ensures(self: Self, rhs: Self, result: Self) -> bool + { + match (self, rhs) { + (NumberView::Integer(lhs), NumberView::Integer(rhs)) => + result matches NumberView::Integer(sum) && sum == lhs + rhs, + _ => exists|a: f64, b: f64| { + &&& self.to_f64_lossy_ensures(a) + &&& rhs.to_f64_lossy_ensures(b) + &&& match float_to_small_int(a + b) { + Some(sum) => result == NumberView::Integer(sum), + None => result == NumberView::Float(a + b), + } + }, + } + } + + pub open spec fn sub_ensures(self: Self, rhs: Self, result: Self) -> bool + { + match (self, rhs) { + (NumberView::Integer(lhs), NumberView::Integer(rhs)) => + result matches NumberView::Integer(diff) && diff == lhs - rhs, + _ => exists|a: f64, b: f64| { + &&& self.to_f64_lossy_ensures(a) + &&& rhs.to_f64_lossy_ensures(b) + &&& match float_to_small_int(a - b) { + Some(diff) => result == NumberView::Integer(diff), + None => result == NumberView::Float(a - b) + } + }, + } + } + + pub open spec fn mul_ensures(self: Self, rhs: Self, result: Self) -> bool + { + match (self, rhs) { + (NumberView::Integer(lhs), NumberView::Integer(rhs)) => + result matches NumberView::Integer(product) && product == lhs * rhs, + _ => exists|a: f64, b: f64| { + &&& self.to_f64_lossy_ensures(a) + &&& rhs.to_f64_lossy_ensures(b) + &&& match float_to_small_int(a * b) { + Some(product) => result == NumberView::Integer(product), + None => result == NumberView::Float(a * b) + } + }, + } + } + + pub open spec fn div_ensures(self: Self, rhs: Self, result: Self) -> bool + { + match (self, rhs) { + (NumberView::Integer(lhs), NumberView::Integer(divisor)) => { + &&& divisor != 0 + &&& if vstd::arithmetic::div_mod::rust_rem(lhs, divisor) == 0 { + result == NumberView::Integer( + vstd::arithmetic::div_mod::rust_div(lhs, divisor), + ) + } else { + exists|a: f64, b: f64| { + &&& self.to_f64_lossy_ensures(a) + &&& rhs.to_f64_lossy_ensures(b) + &&& result == NumberView::Float(a / b) + } + } + }, + _ => { + &&& !rhs.is_zero() + &&& exists|a: f64, b: f64| { + &&& self.to_f64_lossy_ensures(a) + &&& rhs.to_f64_lossy_ensures(b) + &&& result == NumberView::Float(a / b) + } + }, + } + } + +} + +} // end verus! diff --git a/src/verify/utils.rs b/src/verify/utils.rs new file mode 100644 index 000000000..0c6cad858 --- /dev/null +++ b/src/verify/utils.rs @@ -0,0 +1,39 @@ +use std::format; +use std::string::String; + +use vstd::prelude::*; + +verus! { + +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExAnyhowError(anyhow::Error); + +pub assume_specification[ + anyhow::Error::msg:: +](message: M) -> (error: anyhow::Error); + +// The `anyhow!` macro expands to `must_use(format_err(format_args!(..)))`, so +// each of those pieces needs a specification. None of them promises anything +// about the resulting error, which is all the callers rely on. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExFormatArguments<'a>(core::fmt::Arguments<'a>); + +pub assume_specification<'a>[ + core::fmt::Arguments::<'a>::from_str +](message: &'static str) -> (args: core::fmt::Arguments<'a>); + +pub assume_specification<'a>[ + anyhow::__private::format_err +](args: core::fmt::Arguments<'a>) -> (error: anyhow::Error); + +pub assume_specification[ + anyhow::__private::must_use +](error: anyhow::Error) -> (result: anyhow::Error); + +// vstd doesn't specify `to_ascii_uppercase`, and callers don't rely on its +// result, so this promises nothing. +pub assume_specification[ ::to_ascii_uppercase ](s: &str) -> (res: String); + +} // end verus!