[Anand Krishnamoorthi (anakrish)]

Summary

Make Number equality and ordering exact and coherent.

• compare mixed floats and integers from exact binary64 components rather than converting the integer operand to f64
• keep comparison hot paths allocation-free for primitive and integer-only pairs; borrow stored BigInts and use at most one binary64-bounded temporary for integral float/BigInt comparison
• define one total order shared by Eq and Ord, including deterministic defensive handling if a non-finite Number reaches the internal type
• preserve numeric signed-zero behavior (-0.0 == 0)
• add public-boundary and in-crate regression coverage for transitivity, sets, object keys, sorting, min/max, large integers, signed zero, and the non-finite tail
• replace the lossy Verus comparison model with an exact scaled-integer model
• make every NaN representation one CEL-compatible equality class while keeping signed infinities distinct
• body-verify Ord, PartialEq, NaN dispatch, and the integer/BigInt comparison dispatch, leaving only unsupported native float comparison helpers as narrow trusted boundaries

Security impact

The previous lossy comparison could make a float at 2^63 compare equal to both exact integers 2^63 and 2^63 + 1. It could also make out-of-range BigInt values compare equal to infinity. That violated equality transitivity and allowed distinct set elements or object keys to be silently merged.

This PR fixes comparison semantics only. It is rebased onto main after #845 and preserves its finite-arithmetic error paths and strengthened Verus contracts; the diff does not change numeric ingress, arithmetic overflow/promotion, formatting, or compiled-blob validation.

Ordering contract

This is an internal Eq/Ord contract:

• finite integers and floats follow exact mathematical ordering

• -0.0, 0.0, and integer zero remain equal

• the complete internal order is:

  -∞ < negative finite numbers < (-0.0 = +0.0 = integer 0) < positive finite numbers < +∞ < NaN

  Every NaN sign and payload compares equal to every other NaN, matching CEL equality. NaN remains distinct from infinities and finite values.

Language frontends that require different NaN operator semantics should implement those operators separately rather than expose this internal storage order.

Verification model

The Verus model specifies exact finite scaled-integer comparison and a terminal NaN equality class. Ord, PartialEq, NaN dispatch, integer comparisons, and BigInt/primitive comparisons are body-verified. Four narrow external_body helpers retain exact postconditions for operations this Verus toolchain cannot connect to the binary64 bit model: guarded float-to-integer casts, FloatCore::integer_decode with BigInt shifts, and native non-NaN float comparisons. No global axiom assumes the final comparison correspondence.

Verification

• cargo test - 344 passed, 2 ignored, plus all integration suites passed
• cargo test --test gate_cmp_exactness
• cargo test --test gate_promotion
• RVM differential comparison fixture, including equality/order, sets, object keys, and sort/min/max
• units.parse and units.parse_bytes fixtures
• cargo test --no-default-features --tests --no-run
• focused Verus number verification: 73 verified, 0 errors
• focused Verus comparison proofs: 16 verified, 0 errors
• full Verus verification: 105 verified, 0 errors
• Rust 1.95 cargo clippy --all-targets --all-features -- -Dwarnings
• formatting and diff checks

[Copilot]

🟡 Changes recommended

Regression coverage still needs genuinely out-of-f64-range integers and compiled RVM execution.

2 open issues

• Use an out-of-range integer to test BigInt-to-infinity collisions · New
• Cover equality and sorting regressions in compiled RVM tests · New

What changed in this PR

Makes numeric equality and ordering exact and consistent, preventing distinct numbers from merging in sets and object keys.

Changes:

• Replaces lossy mixed-number comparisons with exact integer scaling.
• Preserves signed-zero equality and defines deterministic non-finite ordering.
• Adds regression tests and updates the Verus comparison model.

File	Description
tests/​interpreter/​cases/​builtins/​units/​parse.yaml	Preserves exact large-integer expectations.
tests/​interpreter/​cases/​builtins/​units/​parse_bytes.yaml	Preserves exact large-integer expectations.
tests/​gate_cmp_exactness.rs	Adds public-boundary comparison regressions.
src/​verify/​number_specs.rs	Models exact numeric ordering.
src/​number.rs	Implements exact comparisons and internal tests.

_{Review effort: Balanced}

[Copilot]

🔵 Needs a closer look

Security-critical comparison semantics and newly trusted Verus boundaries require final human validation.

No open issues 🎉

2 resolved since last review

• Cover equality and sorting regressions in compiled RVM tests
• Use an out-of-range integer to test BigInt-to-infinity collisions

_{Review effort: Balanced}

[Copilot]

🔵 Needs a closer look

Security-critical comparison changes and expanded trusted Verus boundaries warrant final human validation.

No open issues 🎉

_{Review effort: Balanced}

[Jay Lorch (jaylorch)]

I stopped reviewing around line #489, after finding many problems and bugs. I think it would be useful to fix those and apply similar fixes to the rest of the PR before I continue reviewing.

[Jay Lorch (jaylorch)]

I stopped reviewing around line #489, after finding many problems and bugs. I think it would be useful to fix those and apply similar fixes to the rest of the PR before I continue reviewing.

[Anand Krishnamoorthi (anakrish)]

Addressed all current review threads in b500d31.

Highlights: exponent 2047 and sign-bit handling are explicit; scaled comparison now uses a common exponent; the 2^64 boundary has the exact reviewed literal as a regression test; Ord, PartialEq, and all integer/BigInt dispatch helpers are now body-verified. Only unsupported float operations remain narrow external_body boundaries. Local Verus results are 73/0 focused and 103/0 full; the PR Verus check is green.

Jay Lorch (@jaylorch), please re-review these changes and continue beyond the original line 489 when convenient.

[Anand Krishnamoorthi (anakrish)]

Addressed the latest review round in e922093.

The internal order is now -∞ < finite values < +∞ < NaN, with signed/integer zero merged and every NaN sign/payload in one CEL-compatible equality class. cmp_float, Ord, PartialEq, NaN dispatch, and integer/BigInt dispatch remain body-verified. Proof-only material moved to number_proofs.rs; no global comparator correspondence axioms remain. Four native float helpers retain exact local contracts after primitive-assumption attempts left comparison postconditions unproved.

Local verification: Number 73/0, comparison proofs 16/0, full Verus 105/0; Number 10/10, comparison 6/6, arithmetic 3/3, RVM fixture passed; Rust 1.95 strict Clippy, formatting, and diff checks passed.

Jay Lorch (@jaylorch), please re-review when convenient.

[Jay Lorch (jaylorch)]

Getting close! There are now a few extraneous spec functions that don't need to be there.

There are still a few external_body functions, which is unfortunate, but we can just plan to fix those in a later PR. It seems like the agent isn't quite up to the task, and it will require some human assistance.

[Jay Lorch (jaylorch)]

We should try to get rid of the external_body instances in a later PR, but for now this looks good. Thanks!

[Anand Krishnamoorthi (anakrish)]

Thanks for the thorough review Jay Lorch (@jaylorch). Much appreciated.