TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Kernels.LimbArray.Shift.Proof

Limb arrays: value semantics of the shifts #

The shifts of Shift.Runtime build each result limb from two source limbs, so their toNat statements are proved bit by bit: shiftLeftLimb_testBit and shiftRightLimb_testBit read one bit of a result limb as one bit of the source value, and Nat.eq_of_testBit_eq turns those readings into toNat_shiftLeft and toNat_shiftRight.

toNat_roundShiftRightEven then combines the shift with the guard-and-sticky form of nearest-even rounding from FloatLib.Numerics.ShiftRightJam.Proof. The guard bit, sticky test, and quotient parity determine whether to increment the truncated quotient.

Machine-word shift bits #

source
theorem FloatLib.Numerics.LimbArray.uint32_shiftRight_testBit (x : UInt32) (r n : ℕ) (hr : r < 32) :
(x >>> UInt32.ofNat r).toNat.testBit n = x.toNat.testBit (r + n)

A bit of a right-shifted limb, for shift counts below 32.

source
theorem FloatLib.Numerics.LimbArray.uint32_shiftLeft_testBit (x : UInt32) (r n : ℕ) (hr : r < 32) :
(x <<< UInt32.ofNat r).toNat.testBit n = (decide (n < 32) && (decide (r ≤ n) && x.toNat.testBit (n - r)))

A bit of a left-shifted limb, for shift counts below 32.

Left shift #

source
theorem FloatLib.Numerics.LimbArray.shiftLeftLimb_testBit (v : LimbArray) (q r i m : ℕ) (hr : r < 32) (hm : m < 32) :
(v.shiftLeftLimb q r i).toNat.testBit m = (decide (32 * q + r ≤ 32 * i + m) && v.toNat.testBit (32 * i + m - (32 * q + r)))

One bit of a result limb of the left shift is the corresponding bit of the source value.

source
@[simp]
theorem FloatLib.Numerics.LimbArray.size_shiftLeft (v : LimbArray) (k : ℕ) :
(v.shiftLeft k).size = v.size + k / 32 + 1

A left shift by k bits adds k / 32 + 1 limbs.

source
theorem FloatLib.Numerics.LimbArray.limb_shiftLeft (v : LimbArray) (k i : ℕ) :
(v.shiftLeft k).limb i = if i < v.size + k / 32 + 1 then v.shiftLeftLimb (k / 32) (k % 32) i else 0

Each limb of a left shift is the corresponding shiftLeftLimb value inside the new size and zero above it.

source
@[simp]
theorem FloatLib.Numerics.LimbArray.toNat_shiftLeft (v : LimbArray) (k : ℕ) :
(v.shiftLeft k).toNat = v.toNat * 2 ^ k

The left shift multiplies the value by 2^k.

Right shift #

source
theorem FloatLib.Numerics.LimbArray.shiftRightLimb_testBit (v : LimbArray) (q r i m : ℕ) (hr : r < 32) (hm : m < 32) :
(v.shiftRightLimb q r i).toNat.testBit m = v.toNat.testBit (32 * i + m + (32 * q + r))

One bit of a result limb of the right shift is the corresponding bit of the source value.

source
@[simp]
theorem FloatLib.Numerics.LimbArray.size_shiftRight (v : LimbArray) (k : ℕ) :
(v.shiftRight k).size = v.size

A right shift keeps the limb count.

source
theorem FloatLib.Numerics.LimbArray.limb_shiftRight (v : LimbArray) (k i : ℕ) :
(v.shiftRight k).limb i = if i < v.size then v.shiftRightLimb (k / 32) (k % 32) i else 0

Each limb of a right shift is the corresponding shiftRightLimb value inside the size and zero above it.

source
@[simp]
theorem FloatLib.Numerics.LimbArray.toNat_shiftRight (v : LimbArray) (k : ℕ) :
(v.shiftRight k).toNat = v.toNat / 2 ^ k

The right shift divides the value by 2^k.

Nearest-even rounding #

source
@[simp]
theorem FloatLib.Numerics.LimbArray.size_roundShiftRightEven (v : LimbArray) (shift : ℕ) :
(v.roundShiftRightEven shift).size = v.size

Rounding a right shift keeps the limb count of the shifted array.

source
@[simp]
theorem FloatLib.Numerics.LimbArray.toNat_roundShiftRightEven (v : LimbArray) (shift : ℕ) :
(v.roundShiftRightEven shift).toNat = Numerics.roundShiftRightEven v.toNat shift

The limb rounder agrees with the width-generic nearest-even shift.