Native Montgomery arithmetic over eight 32-bit limbs

Raw word operations for prime moduli below 2 ^ 255, represented as eight 32-bit limbs carried in the low halves of UInt64 words (Limbs8). This is the multi-limb sibling of Montgomery/Native32.lean: every operation is a straight-line chain of @[inline] word helpers, and each helper comes with an existential toNat specification that names its outputs as fresh naturals. The definitions themselves live in the zero-import module Montgomery/Native64x8Defs; this module states and proves everything about them.

The limb helpers (adcLo/adcCo, sbbLo/sbbBo, macLo/macHi, montM) are combined by the two telescoping lemmas carry_chain_sum and borrow_chain_sum, which turn an eight-step carry or borrow chain into a single identity between recomposed values. Every correctness statement is generic in the modulus limbs; concrete fields supply their constants through the Mont64x8Field class of Montgomery/Native64x8Field.

Conditional subtraction, addition, subtraction and negation are proved correct here. The CIOS multiplication round mulRound is defined in Montgomery/Native64x8Defs; its state invariant is proved in the sibling module that builds the field carrier.

Main results

• condSub_toNat, add_toNat, sub_toNat, neg_toNat — correctness of the raw operations
• addLimbs_toNat, subLimbs_spec — the underlying carry/borrow chains

Word-level specifications

theorem Montgomery.Native64x8.adc_spec (x y c : UInt64) (hx : x.toNat < 2 ^ 32) (hy : y.toNat < 2 ^ 32) (hc : c.toNat ≤ 1) : ∃ (s : ℕ) (co : ℕ), (adcLo x y c).toNat = s ∧ (adcCo x y c).toNat = co ∧ s + 2 ^ 32 * co = x.toNat + y.toNat + c.toNat ∧ co ≤ 1 ∧ s < 2 ^ 32

Add-with-carry, existential form: the low limb and the carry-out are named as fresh naturals together with their defining equations, so that a chain of them is a linear system over plain variables.

theorem Montgomery.Native64x8.adc_spec_wide (x y c : UInt64) (hx : x.toNat < 2 ^ 33) (hy : y.toNat < 2 ^ 32) (hc : c.toNat ≤ 1) : ∃ (s : ℕ) (co : ℕ), (adcLo x y c).toNat = s ∧ (adcCo x y c).toNat = co ∧ s + 2 ^ 32 * co = x.toNat + y.toNat + c.toNat ∧ co ≤ 2 ∧ s < 2 ^ 32

Add-with-carry when the first summand is one bit wider than a limb.

theorem Montgomery.Native64x8.sbb_spec (x y b : UInt64) (hx : x.toNat < 2 ^ 32) (hy : y.toNat < 2 ^ 32) (hb : b.toNat ≤ 1) : ∃ (m : ℕ) (bo : ℕ), (sbbLo x y b).toNat = m ∧ (sbbBo x y b).toNat = bo ∧ m + y.toNat + b.toNat = x.toNat + 2 ^ 32 * bo ∧ bo ≤ 1 ∧ m < 2 ^ 32

Subtract-with-borrow, existential form.

theorem Montgomery.Native64x8.mac_spec (t x y c : UInt64) (ht : t.toNat < 2 ^ 32) (hx : x.toNat < 2 ^ 32) (hy : y.toNat < 2 ^ 32) (hc : c.toNat < 2 ^ 32) : ∃ (lo : ℕ) (hi : ℕ), (macLo t x y c).toNat = lo ∧ (macHi t x y c).toNat = hi ∧ lo + 2 ^ 32 * hi = t.toNat + x.toNat * y.toNat + c.toNat ∧ hi < 2 ^ 32 ∧ lo < 2 ^ 32

Multiply-accumulate, existential form. The accumulator, both factors and the carry-in all fit in 32 bits, so t + x * y + c cannot overflow a 64-bit word.

theorem Montgomery.Native64x8.montM_toNat (s negInv : UInt64) (hs : s.toNat < 2 ^ 32) (hn : negInv.toNat < 2 ^ 32) : (montM s negInv).toNat = s.toNat * negInv.toNat % 2 ^ 32

The Montgomery multiplier agrees with its natural-number specification.

theorem Montgomery.Native64x8.adcLo_lt (x y c : UInt64) : (adcLo x y c).toNat < 2 ^ 32

theorem Montgomery.Native64x8.sbbLo_lt (x y b : UInt64) : (sbbLo x y b).toNat < 2 ^ 32

theorem Montgomery.Native64x8.macLo_lt (t x y c : UInt64) : (macLo t x y c).toNat < 2 ^ 32

theorem Montgomery.Native64x8.montM_lt (s negInv : UInt64) : (montM s negInv).toNat < 2 ^ 32

Eight-limb values

theorem Montgomery.Native64x8.Limbs8.zero_bounded : zero.Bounded

theorem Montgomery.Native64x8.Limbs8.zero_toNat : zero.toNat = 0

theorem Montgomery.Native64x8.Limbs8.one_bounded : one.Bounded

theorem Montgomery.Native64x8.Limbs8.one_toNat : one.toNat = 1

theorem Montgomery.Native64x8.Limbs8.ofNat_bounded (n : ℕ) : (ofNat n).Bounded

theorem Montgomery.Native64x8.Limbs8.ofNat_toNat (n : ℕ) : (ofNat n).toNat = n % 2 ^ 256

theorem Montgomery.Native64x8.sum8_lt {a0 a1 a2 a3 a4 a5 a6 a7 : ℕ} (h0 : a0 < 2 ^ 32) (h1 : a1 < 2 ^ 32) (h2 : a2 < 2 ^ 32) (h3 : a3 < 2 ^ 32) (h4 : a4 < 2 ^ 32) (h5 : a5 < 2 ^ 32) (h6 : a6 < 2 ^ 32) (h7 : a7 < 2 ^ 32) : a0 + 2 ^ 32 * a1 + 2 ^ 64 * a2 + 2 ^ 96 * a3 + 2 ^ 128 * a4 + 2 ^ 160 * a5 + 2 ^ 192 * a6 + 2 ^ 224 * a7 < 2 ^ 256

A recomposed value with 32-bit limbs stays below 2 ^ 256.

theorem Montgomery.Native64x8.Limbs8.ext_of_toNat {x y : Limbs8} (hx : x.Bounded) (hy : y.Bounded) (h : x.toNat = y.toNat) : x = y

Bounded limb vectors are determined by their value.

theorem Montgomery.Native64x8.Limbs8.toNat_lt {x : Limbs8} (hx : x.Bounded) : x.toNat < 2 ^ 256

A bounded eight-limb value is below 2 ^ 256.

Chain lemmas

Telescoping identities for an eight-step carry or borrow chain. They are stated over plain naturals and the y slots are arbitrary, so carry_chain_sum serves both the add-with-carry chains and the multiply-accumulate chains of CIOS, where yᵢ is a limb product.

theorem Montgomery.Native64x8.carry_chain_sum {x0 x1 x2 x3 x4 x5 x6 x7 y0 y1 y2 y3 y4 y5 y6 y7 s0 s1 s2 s3 s4 s5 s6 s7 cin c0 c1 c2 c3 c4 c5 c6 c7 : ℕ} (e0 : s0 + 2 ^ 32 * c0 = x0 + y0 + cin) (e1 : s1 + 2 ^ 32 * c1 = x1 + y1 + c0) (e2 : s2 + 2 ^ 32 * c2 = x2 + y2 + c1) (e3 : s3 + 2 ^ 32 * c3 = x3 + y3 + c2) (e4 : s4 + 2 ^ 32 * c4 = x4 + y4 + c3) (e5 : s5 + 2 ^ 32 * c5 = x5 + y5 + c4) (e6 : s6 + 2 ^ 32 * c6 = x6 + y6 + c5) (e7 : s7 + 2 ^ 32 * c7 = x7 + y7 + c6) : s0 + 2 ^ 32 * s1 + 2 ^ 64 * s2 + 2 ^ 96 * s3 + 2 ^ 128 * s4 + 2 ^ 160 * s5 + 2 ^ 192 * s6 + 2 ^ 224 * s7 + 2 ^ 256 * c7 = x0 + 2 ^ 32 * x1 + 2 ^ 64 * x2 + 2 ^ 96 * x3 + 2 ^ 128 * x4 + 2 ^ 160 * x5 + 2 ^ 192 * x6 + 2 ^ 224 * x7 + (y0 + 2 ^ 32 * y1 + 2 ^ 64 * y2 + 2 ^ 96 * y3 + 2 ^ 128 * y4 + 2 ^ 160 * y5 + 2 ^ 192 * y6 + 2 ^ 224 * y7) + cin

Weighted telescoping of an eight-step carry chain.

theorem Montgomery.Native64x8.borrow_chain_sum {x0 x1 x2 x3 x4 x5 x6 x7 y0 y1 y2 y3 y4 y5 y6 y7 m0 m1 m2 m3 m4 m5 m6 m7 bin b0 b1 b2 b3 b4 b5 b6 b7 : ℕ} (e0 : m0 + y0 + bin = x0 + 2 ^ 32 * b0) (e1 : m1 + y1 + b0 = x1 + 2 ^ 32 * b1) (e2 : m2 + y2 + b1 = x2 + 2 ^ 32 * b2) (e3 : m3 + y3 + b2 = x3 + 2 ^ 32 * b3) (e4 : m4 + y4 + b3 = x4 + 2 ^ 32 * b4) (e5 : m5 + y5 + b4 = x5 + 2 ^ 32 * b5) (e6 : m6 + y6 + b5 = x6 + 2 ^ 32 * b6) (e7 : m7 + y7 + b6 = x7 + 2 ^ 32 * b7) : m0 + 2 ^ 32 * m1 + 2 ^ 64 * m2 + 2 ^ 96 * m3 + 2 ^ 128 * m4 + 2 ^ 160 * m5 + 2 ^ 192 * m6 + 2 ^ 224 * m7 + (y0 + 2 ^ 32 * y1 + 2 ^ 64 * y2 + 2 ^ 96 * y3 + 2 ^ 128 * y4 + 2 ^ 160 * y5 + 2 ^ 192 * y6 + 2 ^ 224 * y7) + bin = x0 + 2 ^ 32 * x1 + 2 ^ 64 * x2 + 2 ^ 96 * x3 + 2 ^ 128 * x4 + 2 ^ 160 * x5 + 2 ^ 192 * x6 + 2 ^ 224 * x7 + 2 ^ 256 * b7

Weighted telescoping of an eight-step borrow chain.

Branch lemmas

The situations that a borrow chain can produce, each as a standalone linear problem over a handful of naturals.

Limbwise addition and subtraction

theorem Montgomery.Native64x8.addLimbs_bounded (a b : Limbs8) : (addLimbs a b).Bounded

theorem Montgomery.Native64x8.addLimbs_toNat (a b : Limbs8) (ha : a.Bounded) (hb : b.Bounded) : ∃ c ≤ 1, (addLimbs a b).toNat + 2 ^ 256 * c = a.toNat + b.toNat

The limbwise sum and the discarded top carry recompose the sum of the inputs.

theorem Montgomery.Native64x8.subLimbs_bounded (a b : Limbs8) : (subLimbs a b).Bounded

theorem Montgomery.Native64x8.subLimbs_spec (a b : Limbs8) (ha : a.Bounded) (hb : b.Bounded) : (subBorrow a b).toNat ≤ 1 ∧ (subLimbs a b).toNat + b.toNat = a.toNat + 2 ^ 256 * (subBorrow a b).toNat

The limbwise difference and the final borrow recompose the difference of the inputs.

Conditional subtraction

theorem Montgomery.Native64x8.condSub_bounded (q t : Limbs8) (ht : t.Bounded) : (condSub q t).Bounded

theorem Montgomery.Native64x8.condSub_toNat (q t : Limbs8) (hq : q.Bounded) (ht : t.Bounded) : (condSub q t).toNat = if t.toNat < q.toNat then t.toNat else t.toNat - q.toNat

condSub subtracts the modulus exactly when the input is at least the modulus.

theorem Montgomery.Native64x8.condSub_lt (q t : Limbs8) (hq : q.Bounded) (ht : t.Bounded) (h : t.toNat < 2 * q.toNat) : (condSub q t).toNat < q.toNat

condSub returns a canonical representative for inputs below 2 * q.

Field operations

theorem Montgomery.Native64x8.add_bounded (q a b : Limbs8) : (add q a b).Bounded

theorem Montgomery.Native64x8.sub_bounded (q a b : Limbs8) : (sub q a b).Bounded

theorem Montgomery.Native64x8.neg_bounded (q a : Limbs8) : (neg q a).Bounded

theorem Montgomery.Native64x8.add_toNat (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded) (hq2 : 2 * q.toNat < 2 ^ 256) (haq : a.toNat < q.toNat) (hbq : b.toNat < q.toNat) : (add q a b).toNat = (a.toNat + b.toNat) % q.toNat

Modular addition is correct for canonical inputs of a modulus below 2 ^ 255.

theorem Montgomery.Native64x8.add_lt (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded) (hq2 : 2 * q.toNat < 2 ^ 256) (haq : a.toNat < q.toNat) (hbq : b.toNat < q.toNat) : (add q a b).toNat < q.toNat

theorem Montgomery.Native64x8.sub_toNat (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded) (hq2 : 2 * q.toNat < 2 ^ 256) (haq : a.toNat < q.toNat) (hbq : b.toNat < q.toNat) : (sub q a b).toNat = (a.toNat + (q.toNat - b.toNat)) % q.toNat

Modular subtraction is correct for canonical inputs of a modulus below 2 ^ 255.

theorem Montgomery.Native64x8.sub_lt (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded) (hq2 : 2 * q.toNat < 2 ^ 256) (haq : a.toNat < q.toNat) (hbq : b.toNat < q.toNat) : (sub q a b).toNat < q.toNat

theorem Montgomery.Native64x8.neg_toNat (q a : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hq2 : 2 * q.toNat < 2 ^ 256) (haq : a.toNat < q.toNat) : (neg q a).toNat = (q.toNat - a.toNat) % q.toNat

Modular negation is correct for canonical inputs of a modulus below 2 ^ 255.

theorem Montgomery.Native64x8.neg_lt (q a : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hq2 : 2 * q.toNat < 2 ^ 256) (haq : a.toNat < q.toNat) : (neg q a).toNat < q.toNat