Verify Number with Verus

[Jay Lorch (jaylorch)]

This PR adds specifications for Number functions and proves that the implementation satisfies them. Some of these specs are self-contained, but most of them refer to specifications described in verify/number_specs.rs. In these specs, a Number is abstracted as a NumberView, which has two variants: Integer and Float.

This PR adds needed assumptions about libraries it depends on, notably BigNum assumptions in verify/bignum_assumptions.rs, f64 assumptions in verify/f64_assumptions.rs, and assumptions about numeric types in verify/num_assumptions.rs.

Most of this code was written by AI (GPT 5.6 Sol, Claude Opus 4.8, and Claude Opus 5), with Jay Lorch (@jaylorch) auditing (and occasionally rewriting) the specifications.

This PR doesn't involve any changes to executable code. However, in the course of generating these proofs, AI found four bugs that necessitated changing the code. Those fixes have already been committed to the Regorus repo:

• e8482f5 (two fixes)
• e468255
• 839510d

To avoid having a dependency on the vstd library in non-verification builds, this PR adds a verus-shim crate with procedural macros. These simple procedural macros simply ignore any #[verus_verify] and #[verus_spec] attributes and expand proof! and proof_decl! blocks into nothing.

[Copilot]

Pull request overview

Adds Verus specification/proof infrastructure around Number (and related f64/BigInt assumptions) while keeping ordinary (non-verification) builds compiling by introducing a no-op verus-shim proc-macro crate. This fits Regorus’ security-critical goal of strengthening numeric correctness guarantees without changing runtime semantics.

Changes:

• Introduces regorus-verus-shim (proc-macro) to strip #[verus_verify]/#[verus_spec] and erase proof! blocks when feature = "verus" is disabled.
• Adds src/verify/ modules with Verus specs/axioms/lemmas for Number, f64, primitive numeric APIs, and num_bigint::BigInt, plus a small executable f64 test.
• Wires verification module into the crate (cfg-gated) and bumps the Verus toolchain/vstd pins (including lockfile updates).

Reviewed changes

Copilot reviewed 16 out of 22 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
verus-shim/src/lib.rs	No-op proc-macros for Verus attributes and proof!/proof_decl!.
verus-shim/Cargo.toml	Declares the shim proc-macro crate (license metadata needs alignment).
src/verify/utils.rs	Verus assumptions/specs to support anyhow!/formatting and str::to_ascii_uppercase.
src/verify/number_specs.rs	Defines NumberView model and specs (e.g., add_ensures, div_ensures).
src/verify/number_proofs.rs	Lemmas bridging Rust division/remainder behavior to Verus models.
src/verify/num_assumptions.rs	Assumptions/specs for primitive numeric operations used in proofs.
src/verify/mod.rs	Module wiring for verification components (cfg-gated).
src/verify/f64_tests.rs	Runtime test justifying a key f64 casting axiom.
src/verify/f64_assumptions.rs	Axioms/assumptions for IEEE-like f64 behavior used by Number proofs.
src/verify/bigint_proofs.rs	Proof helper for BigInt::bits-related reasoning.
src/verify/bigint_assumptions.rs	Large set of assumptions/specs for num_bigint::BigInt.
src/number.rs	Annotates Number implementation with Verus specs/proofs; adds a few runtime tests.
src/lib.rs	Adjusts crate-level attributes/cfg for verification-only unstable features and lints.
Cargo.toml	Adds shim crate dependency; updates pinned vstd version.
Cargo.lock	Updates lockfile for new shim crate and updated Verus-related deps.
bindings/wasm/Cargo.lock	Lockfile update to include shim + updated Verus deps.
bindings/python/Cargo.lock	Lockfile update to include shim + updated Verus deps.
bindings/java/Cargo.lock	Lockfile update to include shim + updated Verus deps.
bindings/ffi/Cargo.lock	Lockfile update to include shim + updated Verus deps.
.gitignore	Ignores Emacs backup files.
.github/workflows/verus.yml	Updates Verus release artifact URL/SHA.
.github/skills/verus-verification/SKILL.md	Adds guidance doc for Verus verification work in this repo.

Comments suppressed due to low confidence (1)

src/number.rs:196

• This proof! { ... } invocation is used as a standalone statement but is missing a trailing semicolon, which can cause a Rust parse error in non-Verus builds (the shim expands to empty, but the parser still requires statement termination).

        proof! { axiom_f64_ops_deterministic(); }

[Jay Lorch (jaylorch)]

Deep-review skill finding — High: packaging/publishing is broken

Source: repository-local deep-review skill, posted by GitHub Copilot. This is not a finding authored by Anand Krishnamoorthi (@anakrish).

Cargo.toml:152 makes the publishable regorus crate depend on regorus-verus-shim = { path = "verus-shim", version = "0.0.0" }, while verus-shim/Cargo.toml:11 declares publish = false. During package preparation Cargo must resolve the version from crates.io, where it does not exist, so cargo package/cargo publish fails.

Suggested fix: keep the shim out of shipped builds by cfg-gating verification annotations/proof blocks, or make the shim publishable and publish it before regorus.

Ah, good point. Before we do this, I should talk with Anand Krishnamoorthi (@anakrish) about alternatives, such as taking a dependency on the vstd crate instead.

[Anand Krishnamoorthi (anakrish)]

Automated Verus proof audit — summary and traceability concern

Source: automated formal-analysis review performed by GitHub Copilot. This comment is not authored by Anand Krishnamoorthi (@anakrish).

The audit found substantial real proof value: 57 bodies are verified for arithmetic safety; integer add/sub/mul, exact division/modulo (including MIN / -1), power construction, and the pow10_bigint loop invariant have meaningful contracts. Executable Verus/non-Verus parity also appears clean.

However, the PR does not make the proof boundary discoverable. src/verify/mod.rs has no proof index; unproven axioms and proved lemmas look identical at call sites; uninterpreted terms read like exact mathematics; and eight functions are silently outside verification. A reviewer must reconstruct Verus internals to determine what is proved versus trusted.

Please add a short proof map covering: method → plain-English theorem → body-proved/external/trusted status → axioms relied upon → relevant lemma. Also mark opaque clauses as TRUSTED and meaningful body properties as PROVED near their contracts.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — High: to_f64_lossy_ensures does not constrain the returned float

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

In src/verify/number_specs.rs:106-123, the integer case permits an existential BigInt witness whose view and spec_to_f64 are uninterpreted. For NumberView::Integer(3), the third disjunct can therefore witness essentially any returned f; nothing establishes f == 3.0. This weakness propagates into as_f64, mixed float/integer arithmetic, inexact division, comparisons, and negative powers.

This is specifically the representation-leaking existential anti-pattern described by the repository's Verus guidance. Please relate BigInt to_f64 to its mathematical view, or specify to_f64_lossy over the concrete Number variant so the returned value is fixed.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — High: float-to-integer contracts certify saturated wrong answers

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

The contracts at src/number.rs:489-650 model Rust's saturating casts rather than the expected exact conversion property. Concrete examples:

• Float(2^64).as_u64() returns Some(u64::MAX) instead of None.
• Float(2^63).as_i64() returns Some(i64::MAX) instead of None.
• Equivalent failures occur at 2^128/2^127 for u128/i128.

Because MAX as f64 rounds to the next power of two, both the <= MAX as f64 guard and round-trip check pass. The proof consequently blesses the bug instead of detecting it. Please specify that the returned integer has the same mathematical value as the float; verification should then expose the required strict upper-bound fix.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — High: Ord proves determinism, not ordering correctness

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

At src/number.rs:455-465, the integer branch states result == n1.cmp_spec(&n2), but cmp_spec for Verus mathematical int is uninterpreted here. The implementation and postcondition agree only through the same opaque symbol, so no theorem such as n1 < n2 ⇒ Less is established.

The contracts also expose an Eq/Ord law violation for NaN: Float(NaN) != Float(NaN), while cmp maps partial_cmp(None) to Equal. Please write the ordering explicitly (<, >, otherwise Equal) and document or resolve the NaN law violation, since Number ordering affects sets and objects.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — High: several float specifications only rename opaque behavior

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

In src/verify/f64_assumptions.rs:105-171, spec_f64_fract, abs, floor, ceil, round, and is_sign_positive are uninterpreted functions paired with assumptions saying the runtime function returns that uninterpreted value. f64::eq_spec is likewise never tied to IEEE equality.

As a result, contracts for is_zero, is_integer, float_to_small_int, abs, floor, ceil, round, and is_positive do not establish their apparent mathematical properties. Please connect these symbols to vstd's IEEE/bit-level models, and clearly label any remaining uninterpreted clauses as trusted/opaque rather than proved semantics.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — Medium: totality contracts omit resource failure

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

The contracts for lsh, rsh, two_pow, and ten_pow assert successful results across their full machine-integer domains, but Verus assumes allocation succeeds. Policy-reachable bits.lsh(1, 4294967295) can request roughly 512 MiB, two_pow(i32::MIN) constructs roughly 256 MiB, and extreme ten_pow inputs are much larger. The new two_pow(i32::MIN) unit test itself performs that allocation.

Please state the allocation assumption explicitly, avoid executing the extreme allocation in a unit test, and consider enforcing a shift/exponent resource bound consistent with the repository's resource-limit invariant.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — Medium: bitwise contracts are uninterpreted

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

src/verify/bigint_assumptions.rs:45-79 introduces uninterpreted spec_bigint_bitand, bitor, and bitxor; the Number::{and,or,xor} contracts then state only that results equal those opaque functions. They do not establish two's-complement semantics or even basic identities such as a & a == a.

Please give these operations falsifiable semantics, at minimum by proving agreement with primitive signed/unsigned bitwise operations over representable ranges and documenting the extension to arbitrary BigInts.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — Medium: the trusted axiom set has no consistency/vacuity guard

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

The verification relies on 22 axioms and 121 assume_specification declarations. A single inconsistent axiom would allow every obligation to verify vacuously while CI remains green. Most axioms also lack a nearby truth justification, and axiom_f64_ops_deterministic bundles many unrelated claims, including behavior vstd deliberately leaves unspecified.

Please document the justification and dependents of each axiom, split broad axioms to the facts actually required, remove unused assumptions, and add an expected-failure consistency probe that calls the trusted axioms and verifies that assert(false) remains unprovable after Verus/vstd upgrades.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — Medium: eight functions are silently outside verification

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

Verification is opt-in, leaving Debug::fmt, Serialize::serialize, FromStr::from_str, PartialOrd::partial_cmp, bigint_to_scientific, parse_scientific_bigint, split_scientific_parts, and scientific_parts_to_bigint external by default with no visible marker. FromStr handles untrusted policy text, and PartialOrd participates in collection ordering, so this omission is material.

Please annotate each intentionally unverified function explicitly as external with a reason, and list it in the proposed proof index. This prevents future reviewers from mistaking absence of annotations for verified coverage.

[Anand Krishnamoorthi (anakrish)]

Automated formal-review finding — Medium/Low: trait-level guarantees are disabled without explanation

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

src/verify/number_specs.rs:203-287 sets nine obeys_*_spec() switches to false for seven From impls, PartialEq, and Ord. Monomorphic call sites can still use local postconditions, but verified generic code receives no trait-level guarantee. This distinction is documented for only one switch and is otherwise difficult to discover.

Please explain each disabled trait contract and state in the proof map that these guarantees apply only to statically resolved Number calls, not generic verified consumers.

[Jay Lorch (jaylorch)]

Automated Verus proof audit — summary and traceability concern

Source: automated formal-analysis review performed by GitHub Copilot. This comment is not authored by Anand Krishnamoorthi (@anakrish).

The audit found substantial real proof value: 57 bodies are verified for arithmetic safety; integer add/sub/mul, exact division/modulo (including MIN / -1), power construction, and the pow10_bigint loop invariant have meaningful contracts. Executable Verus/non-Verus parity also appears clean.

However, the PR does not make the proof boundary discoverable. src/verify/mod.rs has no proof index; unproven axioms and proved lemmas look identical at call sites; uninterpreted terms read like exact mathematics; and eight functions are silently outside verification. A reviewer must reconstruct Verus internals to determine what is proved versus trusted.

Please add a short proof map covering: method → plain-English theorem → body-proved/external/trusted status → axioms relied upon → relevant lemma. Also mark opaque clauses as TRUSTED and meaningful body properties as PROVED near their contracts.

This PR is just an intermediate step in the verification of the project. It is not intended to be the end of the verification process. Soon, we'll be verifying higher-level functions, whose correctness depends on the functions in Number. At that point, the Number specs will not constitute the highest level of the trusted spec.

So I suggest deferring the job of marking the trust boundary until proof work is further along. It will certainly move.

[Jay Lorch (jaylorch)]

Automated formal-review finding — High: to_f64_lossy_ensures does not constrain the returned float

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

In src/verify/number_specs.rs:106-123, the integer case permits an existential BigInt witness whose view and spec_to_f64 are uninterpreted. For NumberView::Integer(3), the third disjunct can therefore witness essentially any returned f; nothing establishes f == 3.0. This weakness propagates into as_f64, mixed float/integer arithmetic, inexact division, comparisons, and negative powers.

This is specifically the representation-leaking existential anti-pattern described by the repository's Verus guidance. Please relate BigInt to_f64 to its mathematical view, or specify to_f64_lossy over the concrete Number variant so the returned value is fixed.

Even before verification the function had the name to_f64_lossy. So it shouldn't be surprising that the result isn't guaranteed to match precisely (e.g., 3 becoming exactly 3.0) and isn't guaranteed to be deterministic (e.g., the result of converting 3 may depend on whether it's currently stored as an unsigned integer, a signed integer, or a big integer). For this reason, the correct spec seems to be a non-deterministic one.

[Jay Lorch (jaylorch)]

Automated formal-review finding — High: float-to-integer contracts certify saturated wrong answers

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

The contracts at src/number.rs:489-650 model Rust's saturating casts rather than the expected exact conversion property. Concrete examples:

• Float(2^64).as_u64() returns Some(u64::MAX) instead of None.
• Float(2^63).as_i64() returns Some(i64::MAX) instead of None.
• Equivalent failures occur at 2^128/2^127 for u128/i128.

Because MAX as f64 rounds to the next power of two, both the <= MAX as f64 guard and round-trip check pass. The proof consequently blesses the bug instead of detecting it. Please specify that the returned integer has the same mathematical value as the float; verification should then expose the required strict upper-bound fix.

It's not clear whether the behavior you observe is a bug or not. I agree that if you convert 18446744073709551616.0 (which equals 2^64) to a float and then call to_u64() you get u64::MAX, but this is true for even slightly bigger numbers because the precision of an f64 isn't sufficient to represent all the bits. The specification given now is at least a correct description of what the function does.

[Jay Lorch (jaylorch)]

Automated formal-review finding — High: Ord proves determinism, not ordering correctness

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

At src/number.rs:455-465, the integer branch states result == n1.cmp_spec(&n2), but cmp_spec for Verus mathematical int is uninterpreted here. The implementation and postcondition agree only through the same opaque symbol, so no theorem such as n1 < n2 ⇒ Less is established.

The contracts also expose an Eq/Ord law violation for NaN: Float(NaN) != Float(NaN), while cmp maps partial_cmp(None) to Equal. Please write the ordering explicitly (<, >, otherwise Equal) and document or resolve the NaN law violation, since Number ordering affects sets and objects.

Thanks! I didn't realize that cmp_spec for int was undefined, so I shouldn't be using it in specs. I've fixed that.

I don't understand the point you're making about an Eq/Ord law violation for NaN. We use PartialEq, not Eq, on f64, specifically because of the NaN != NaN issue. Could you please give a more specific description?

[Jay Lorch (jaylorch)]

Automated formal-review finding — High: several float specifications only rename opaque behavior

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

In src/verify/f64_assumptions.rs:105-171, spec_f64_fract, abs, floor, ceil, round, and is_sign_positive are uninterpreted functions paired with assumptions saying the runtime function returns that uninterpreted value. f64::eq_spec is likewise never tied to IEEE equality.

As a result, contracts for is_zero, is_integer, float_to_small_int, abs, floor, ceil, round, and is_positive do not establish their apparent mathematical properties. Please connect these symbols to vstd's IEEE/bit-level models, and clearly label any remaining uninterpreted clauses as trusted/opaque rather than proved semantics.

This is a good idea, which should probably wait for this outstanding Verus PR.

Alternatively, I'm starting to wonder if it's a good idea to support floats at all(!) None of the supported operations require floats, and would work fine on rationals. Rational numbers would give us perfect precision.

[Jay Lorch (jaylorch)]

Automated formal-review finding — Medium: totality contracts omit resource failure

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

The contracts for lsh, rsh, two_pow, and ten_pow assert successful results across their full machine-integer domains, but Verus assumes allocation succeeds. Policy-reachable bits.lsh(1, 4294967295) can request roughly 512 MiB, two_pow(i32::MIN) constructs roughly 256 MiB, and extreme ten_pow inputs are much larger. The new two_pow(i32::MIN) unit test itself performs that allocation.

Please state the allocation assumption explicitly, avoid executing the extreme allocation in a unit test, and consider enforcing a shift/exponent resource bound consistent with the repository's resource-limit invariant.

Ah, good point. I've removed the unit test that allocates lots of memory.

As for limiting the allocation by enforcing a resource bound, that's a design decision I leave to Anand Krishnamoorthi (@anakrish).

[Jay Lorch (jaylorch)]

Automated formal-review finding — Medium: bitwise contracts are uninterpreted

Source: automated GitHub Copilot proof audit; not authored by Anand Krishnamoorthi (@anakrish).

src/verify/bigint_assumptions.rs:45-79 introduces uninterpreted spec_bigint_bitand, bitor, and bitxor; the Number::{and,or,xor} contracts then state only that results equal those opaque functions. They do not establish two's-complement semantics or even basic identities such as a & a == a.

Please give these operations falsifiable semantics, at minimum by proving agreement with primitive signed/unsigned bitwise operations over representable ranges and documenting the extension to arbitrary BigInts.

Good idea. Done!

[Anand Krishnamoorthi (anakrish)]

Deep-review skill finding — Medium: the public verus feature disables the unsafe-code prohibition
Source: repository-local deep-review skill, posted by GitHub Copilot. This is not a finding authored by Anand Krishnamoorthi (Anand Krishnamoorthi (@anakrish)).
At src/lib.rs:8, #![cfg_attr(not(feature = "verus"), forbid(unsafe_code))] removes the core crate's documented forbid(unsafe_code) invariant whenever the public Cargo feature is enabled. Cargo cannot enforce the accompanying claim that such a build is never used in production, and all-features/downstream builds can enable it normally.
Suggested fix: keep forbid(unsafe_code) unconditional, or isolate verifier requirements outside the core crate rather than keying the safety guarantee to a public feature.

I'm not sure this will work. I should talk to Anand Krishnamoorthi (Anand Krishnamoorthi (@anakrish)) about how to deal with this.

This can be revisited later in subsequent PRs to see if possible.