Fraction: Q68.60 fixed-point numbers for Solana finance

A fixed-point number with 60 fractional bits, modelled here at the spec layer with an unbounded Nat underlying representation (so omega works without ceremony). A future Fraction128 companion will refine this to the u128-bounded on-chain shape used by Kamino and other DeFi protocols (Kamino's U68F60).

A Fraction f represents the real number f.bits / 2^60.

This module is Layer 1 in the long-term Solanalib stack: a numeric foundation that every domain primitive (interest curves, exchange rates, slippage, vesting fractions, …) sits on top of. The conscious choice to use Nat rather than u128 at this layer follows the seL4 / CompCert pattern — prove mathematical properties on the abstract model, refine to the bounded representation separately.

Main definitions

• Fraction — a fixed-point number, conceptually bits / 2^60.
• Fraction.zero, Fraction.one — the additive and multiplicative units.
• Fraction.fromNat / Fraction.toFloor — integer/fraction conversions.
• Fraction.add, Fraction.mul — arithmetic at the fixed-point scale.

Main statements (this commit)

A minimal kit:

• add_zero, zero_add, add_comm — Fraction.add is a commutative monoid.
• mul_one, one_mul — Fraction.one is the multiplicative identity.

Multiplication is approximately associative — the truncating division by scale after each multiplication introduces a rounding error of at most one ULP. A bound on that error is deferred to a follow-up file.

Conventions

The "scale" exponent (60) is exposed as Fraction.scaleBits so future refinements that need a different precision (e.g. Q.32, Q.96) can be parameterised cleanly.

structure Solanalib.Fraction : Type

A fixed-point number with scaleBits fractional bits, where scaleBits = 60 to match the U68F60 convention common in Solana DeFi.

Fraction.mk b represents the real number b / 2^60.

• bits : LamportsUnchecked

  The underlying integer encoding: bits = realValue * 2^60.

theorem Solanalib.Fraction.ext_iff {x y : Fraction} : x = y ↔ x.bits = y.bits

theorem Solanalib.Fraction.ext {x y : Fraction} (bits : x.bits = y.bits) : x = y

def Solanalib.instReprFraction.repr : Fraction → LamportsUnchecked → Std.Format

Equations

• Solanalib.instReprFraction.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "bits" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.bits)).group) " }"

@[implicit_reducible]

instance Solanalib.instReprFraction : Repr Fraction

Equations

• Solanalib.instReprFraction = { reprPrec := Solanalib.instReprFraction.repr }

@[implicit_reducible]

instance Solanalib.instDecidableEqFraction : DecidableEq Fraction

Equations

• Solanalib.instDecidableEqFraction = Solanalib.instDecidableEqFraction.decEq

def Solanalib.instDecidableEqFraction.decEq (x✝ x✝¹ : Fraction) : Decidable (x✝ = x✝¹)

Equations

• Solanalib.instDecidableEqFraction.decEq { bits := a } { bits := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Solanalib.Fraction.scaleBits : LamportsUnchecked

The number of fractional bits in the representation.

Equations

• Solanalib.Fraction.scaleBits = 60

def Solanalib.Fraction.scale : LamportsUnchecked

The scale factor: 2^scaleBits = 2^60. Every operation that preserves the fixed-point invariant divides intermediate products by this constant.

Equations

• Solanalib.Fraction.scale = 2 ^ Solanalib.Fraction.scaleBits

theorem Solanalib.Fraction.scale_pos : 0 < scale

scale > 0 — useful for division-cancellation lemmas.

def Solanalib.Fraction.zero : Fraction

The additive identity.

Equations

• Solanalib.Fraction.zero = { bits := 0 }

def Solanalib.Fraction.one : Fraction

The multiplicative identity: encoding of 1.0.

Equations

• Solanalib.Fraction.one = { bits := Solanalib.Fraction.scale }

def Solanalib.Fraction.fromNat (n : LamportsUnchecked) : Fraction

Convert an integer n to its fixed-point encoding n * 2^60.

Equations

• Solanalib.Fraction.fromNat n = { bits := n * Solanalib.Fraction.scale }

def Solanalib.Fraction.toFloor (f : Fraction) : LamportsUnchecked

Project a fraction to its integer floor: bits / 2^60.

Equations

• f.toFloor = f.bits / Solanalib.Fraction.scale

def Solanalib.Fraction.add (a b : Fraction) : Fraction

Addition: just sum the bits. The fixed-point scale is preserved because both operands share it.

Equations

• a.add b = { bits := a.bits + b.bits }

def Solanalib.Fraction.sub (a b : Fraction) (_h : b.bits ≤ a.bits) : Fraction

Subtraction with an explicit underflow precondition: b ≤ a (on the underlying bit encoding). Returns ⟨a.bits − b.bits⟩. The precondition is mandatory: matches the dependent-type discipline used throughout Solanalib (compare Account.debit).

Equations

• a.sub b _h = { bits := a.bits - b.bits }

def Solanalib.Fraction.mul (a b : Fraction) : Fraction

Multiplication: (a.bits * b.bits) / scale. The division corrects the doubled scale that would otherwise result from bits * bits. This operation truncates — see the file docstring on associativity.

Equations

• a.mul b = { bits := a.bits * b.bits / Solanalib.Fraction.scale }

def Solanalib.Fraction.div (a b : Fraction) (_h : b.bits ≠ 0) : Fraction

Division with an explicit non-zero precondition on the divisor. Returns ⟨a.bits * scale / b.bits⟩ — the multiplication by scale corrects the lost-scale that would otherwise result from bits / bits.

Like every truncating division in Fraction, this rounds toward zero. A rounded-up companion (divCeil) is a future refinement.

Equations

• a.div b _h = { bits := a.bits * Solanalib.Fraction.scale / b.bits }

Order

Fraction inherits its order from the underlying Nat encoding: a ≤ b ↔ a.bits ≤ b.bits. Comparisons are decidable and omega-friendly once unfolded via the iff lemmas.

@[implicit_reducible]

instance Solanalib.Fraction.instLE : LE Fraction

Equations

• Solanalib.Fraction.instLE = { le := fun (a b : Solanalib.Fraction) => a.bits ≤ b.bits }

@[implicit_reducible]

instance Solanalib.Fraction.instLT : LT Fraction

Equations

• Solanalib.Fraction.instLT = { lt := fun (a b : Solanalib.Fraction) => a.bits < b.bits }

@[implicit_reducible]

instance Solanalib.Fraction.instDecidableLe (a b : Fraction) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = a.bits.decLe b.bits

@[implicit_reducible]

instance Solanalib.Fraction.instDecidableLt (a b : Fraction) : Decidable (a < b)

Equations

• a.instDecidableLt b = a.bits.decLt b.bits

@[simp]

theorem Solanalib.Fraction.le_iff_bits_le (a b : Fraction) : a ≤ b ↔ a.bits ≤ b.bits

@[simp]

theorem Solanalib.Fraction.lt_iff_bits_lt (a b : Fraction) : a < b ↔ a.bits < b.bits

Theorems

@[simp]

theorem Solanalib.Fraction.add_bits (a b : Fraction) : (a.add b).bits = a.bits + b.bits

@[simp]

theorem Solanalib.Fraction.sub_bits (a b : Fraction) (h : b.bits ≤ a.bits) : (a.sub b h).bits = a.bits - b.bits

@[simp]

theorem Solanalib.Fraction.mul_bits (a b : Fraction) : (a.mul b).bits = a.bits * b.bits / scale

@[simp]

theorem Solanalib.Fraction.div_bits (a b : Fraction) (h : b.bits ≠ 0) : (a.div b h).bits = a.bits * scale / b.bits

@[simp]

theorem Solanalib.Fraction.zero_bits : zero.bits = 0

@[simp]

theorem Solanalib.Fraction.one_bits : one.bits = scale

@[simp]

theorem Solanalib.Fraction.fromNat_bits (n : LamportsUnchecked) : (fromNat n).bits = n * scale

@[simp]

theorem Solanalib.Fraction.toFloor_def (f : Fraction) : f.toFloor = f.bits / scale

theorem Solanalib.Fraction.one_bits_ne_zero : one.bits ≠ 0

one.bits ≠ 0: useful for discharging div's precondition when the divisor is one.

theorem Solanalib.Fraction.add_zero (a : Fraction) : a.add zero = a

theorem Solanalib.Fraction.zero_add (a : Fraction) : zero.add a = a

theorem Solanalib.Fraction.add_comm (a b : Fraction) : a.add b = b.add a

theorem Solanalib.Fraction.mul_one (a : Fraction) : a.mul one = a

theorem Solanalib.Fraction.one_mul (a : Fraction) : one.mul a = a

Order theorems

theorem Solanalib.Fraction.zero_le (a : Fraction) : zero ≤ a

theorem Solanalib.Fraction.le_refl (a : Fraction) : a ≤ a

theorem Solanalib.Fraction.le_trans {a b c : Fraction} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c

theorem Solanalib.Fraction.le_antisymm {a b : Fraction} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

Round-trip theorems

theorem Solanalib.Fraction.toFloor_fromNat (n : LamportsUnchecked) : (fromNat n).toFloor = n

Integer round-trip: fromNat n |>.toFloor = n. The fixed-point encoding preserves integer values exactly.

theorem Solanalib.Fraction.sub_add (a b : Fraction) (h : b.bits ≤ a.bits) : (a.sub b h).add b = a

sub followed by add cancels (within its precondition).

theorem Solanalib.Fraction.div_one (a : Fraction) : a.div one one_bits_ne_zero = a

Division by one is identity.

Bridging to Lamports

Lamports (= UInt64) and Fraction (= Q68.60) are the two numeric foundations Solana programs juggle: integer lamport counts and fractional ratios. The lift ofLamports is exact (no precision loss — Lamports fit comfortably in the 68 integer bits). The reverse projection toLamports? returns Option because the Fraction's integer floor can exceed u64::MAX.

def Solanalib.Fraction.ofLamports (l : Lamports) : Fraction

Lift a Lamports (u64) to its exact Fraction encoding.

Equations

• Solanalib.Fraction.ofLamports l = Solanalib.Fraction.fromNat l.toNat

def Solanalib.Fraction.toLamports? (f : Fraction) : Option Lamports

Project a Fraction to Lamports by taking the integer floor. Returns none if the floor exceeds u64::MAX.

Equations

• f.toLamports? = if h : f.toFloor < UInt64.size then some (UInt64.ofNatLT f.toFloor h) else none

theorem Solanalib.Fraction.toFloor_ofLamports (l : Lamports) : (ofLamports l).toFloor = l.toNat

Round-trip: (ofLamports l).toFloor = l.toNat. The Q68.60 lift preserves the integer value exactly.