Verify Number with Verus (#774)

feat(verus): Verification of `number`

Signed-off-by: Jay Lorch <jaylorch@gmail.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Author: jaylorch

.dir-locals.el

@@ -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<Number> {
+    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.

.github/skills/verus-verification/SKILL.md

@@ -35,8 +35,8 @@ jobs:
       shell: bash
       run: |
         set -euxo pipefail
-        asset_url=https://github.com/verus-lang/verus/releases/download/release%2F0.2026.08.09.92f466f/verus-0.2026.08.09.92f466f-x86-linux.zip
-        asset_sha256=2f5a41c553f424aacdd732339e9d125563716a0b003c27730f75d6f81a282cef
+        asset_url=https://github.com/verus-lang/verus/releases/download/release%2F0.2026.08.23.fbbbbcf/verus-0.2026.08.23.fbbbbcf-x86-linux.zip
+        asset_sha256=b65483714e6bf2ae72bfe7c7199e1c608495a941306b979260e9ed585d5899c9
         test -n "$asset_url"
         curl -fsSL "$asset_url" -o verus.zip
 
@@ -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

.github/workflows/verus.yml

@@ -54,3 +54,6 @@ bindings/ruby/bin/
 bindings/java/.classpath
 bindings/java/.project
 bindings/java/.settings/
+
+# Emacs backup files
+*~