pub enum AverInt {
Small(i64),
Big(Box<BigInt>),
}Expand description
Arbitrary-precision integer (mathematical ℤ) with a small-int fast path.
Invariant: Big never holds a value representable as i64 (see module
docs). Always construct/renormalize through this type’s API.
Variants§
Small(i64)
A value that fits i64 — the common, allocation-free case.
Big(Box<BigInt>)
A value outside the i64 range. Boxed to keep the enum small (a
bare BigInt is three machine words; boxing keeps AverInt at two).
Implementations§
Source§impl AverInt
impl AverInt
Sourcepub fn from_bigint(b: BigInt) -> Self
pub fn from_bigint(b: BigInt) -> Self
Renormalize a BigInt to canonical form: demote to Small when it
fits i64, otherwise box it as Big. Every path that produces or
reconstructs a BigInt must funnel through here so the canonical
invariant (a value fitting i64 is always Small) holds — this is
the sole sanctioned way to build a Big, which is why Big’s payload
is private.
Sourcepub fn div_euclid(&self, rhs: &AverInt) -> Option<AverInt>
pub fn div_euclid(&self, rhs: &AverInt) -> Option<AverInt>
Euclidean quotient, matching i64::div_euclid and the Lean/Dafny
Int.ediv model the proofs cite: the unique q with a remainder in
[0, |rhs|). Returns None when rhs == 0. Over ℤ there is no
i64::MIN / -1 overflow edge — it is just i64::MAX + 1, returned as
a Big.
Sourcepub fn rem_euclid(&self, rhs: &AverInt) -> Option<AverInt>
pub fn rem_euclid(&self, rhs: &AverInt) -> Option<AverInt>
Euclidean remainder self - rhs * div_euclid(self, rhs), matching
i64::rem_euclid and the Lean/Dafny Int.emod model. Returns None
when rhs == 0. The result is always non-negative and in [0, |rhs|),
independent of the sign of either operand.
Sourcepub fn div_trunc(&self, rhs: &AverInt) -> Option<AverInt>
pub fn div_trunc(&self, rhs: &AverInt) -> Option<AverInt>
Truncating quotient (rounds toward zero), the semantics of the raw
/ operator. Returns None when rhs == 0. Distinct from
div_euclid for negative operands; provided for the low-level
arithmetic opcodes (Int.div uses the Euclidean form).
Sourcepub fn rem_trunc(&self, rhs: &AverInt) -> Option<AverInt>
pub fn rem_trunc(&self, rhs: &AverInt) -> Option<AverInt>
Truncating remainder (sign follows the dividend), the semantics of the
raw % operator. Returns None when rhs == 0.
Sourcepub fn min_ref(&self, other: &AverInt) -> AverInt
pub fn min_ref(&self, other: &AverInt) -> AverInt
The smaller of self and other (borrowing form, to avoid the
by-value Ord::min/max and keep the small-int clone cheap).
Sourcepub fn to_usize(&self) -> Option<usize>
pub fn to_usize(&self) -> Option<usize>
self as usize if it fits (non-negative and in range), else None.
Sourcepub fn to_f64(&self) -> f64
pub fn to_f64(&self) -> f64
self as f64, lossily. Huge magnitudes saturate to ±∞ (never
NaN), matching the Lean prelude’s Float.ofInt/IEEE coercion. This
is the only intentionally-lossy conversion.
Sourcepub fn from_f64_trunc(f: f64) -> AverInt
pub fn from_f64_trunc(f: f64) -> AverInt
Truncate a finite f64 toward zero into ℤ. The exact mirror of the
VM’s float_to_aver_int (src/types/int.rs): non-finite (NaN/±∞)
maps to 0; an in-i64-range truncated value stays Small; an
out-of-range finite magnitude is represented EXACTLY as a Big via
BigInt::from_f64.
This is the constructor Int.fromFloat and Float.floor/ceil/round
must funnel through — a bare f as i64 cast SATURATES huge finite
floats to i64::MAX/MIN (a silent wrong value), which this avoids.