Basic Bignum Definitions

This file contains the fundamental definitions for bignums in Lean, ported from s2n-bignum/common/bignum.ml

Main Definitions

• bigdigit n i - Extracts the i-th 64-bit digit from natural number n
• highdigits n i - Returns the high part: n DIV (2^(64*i))
• lowdigits n i - Returns the low part: n MOD (2^(64*i))

References

Source: s2n-bignum/common/bignum.ml (lines 11-77)

def Bignum.bigdigit (n i : Nat) : Nat

Extract the i-th 64-bit digit from a natural number n.

This corresponds to HOL Light's definition:

let bigdigit = new_definition
 `bigdigit n i = (n DIV (2 EXP (64 * i))) MOD (2 EXP 64)`;;

Source: s2n-bignum/common/bignum.ml:11-12

Equations

• Bignum.bigdigit n i = n / 2 ^ (64 * i) % 2 ^ 64

def Bignum.highdigits (n i : Nat) : Nat

Extract the high digits of n starting from position i. Essentially n DIV (2^(64*i)).

This corresponds to HOL Light's definition:

let highdigits = new_definition
 `highdigits n i = n DIV (2 EXP (64 * i))`;;

Source: s2n-bignum/common/bignum.ml:73-74

Equations

• Bignum.highdigits n i = n / 2 ^ (64 * i)

def Bignum.lowdigits (n i : Nat) : Nat

Extract the low digits of n up to position i. Essentially n MOD (2^(64*i)).

This corresponds to HOL Light's definition:

let lowdigits = new_definition
 `lowdigits n i = n MOD (2 EXP (64 * i))`;;

Source: s2n-bignum/common/bignum.ml:76-77

Equations

• Bignum.lowdigits n i = n % 2 ^ (64 * i)

theorem Bignum.bigdigit_bound (n i : Nat) : bigdigit n i < 2 ^ 64

A bigdigit is always less than 2^64.

Corresponds to HOL Light theorem:

let BIGDIGIT_BOUND = prove
 (`!n i. bigdigit n i < 2 EXP 64`, ...);;

Source: s2n-bignum/common/bignum.ml:24-27

theorem Bignum.bigdigit_zero (i : Nat) : bigdigit 0 i = 0

bigdigit of 0 is always 0.

Corresponds to HOL Light theorem:

let BIGDIGIT_0 = prove
 (`!i. bigdigit 0 i = 0`, ...);;

Source: s2n-bignum/common/bignum.ml:33-35

theorem Bignum.lowdigits_zero (n : Nat) : lowdigits n 0 = 0

lowdigits of 0 is always 0.

Corresponds to HOL Light theorem:

let LOWDIGITS_0 = prove
 (`!n. lowdigits n 0 = 0`, ...);;

Source: s2n-bignum/common/bignum.ml:121-123

theorem Bignum.highdigits_zero (n : Nat) : highdigits n 0 = n

highdigits of n at position 0 is n itself.

Corresponds to HOL Light theorem:

let HIGHDIGITS_0 = prove
 (`!n. highdigits n 0 = n`, ...);;

Source: s2n-bignum/common/bignum.ml:109-111

theorem Bignum.lowdigits_bound (n i : Nat) : lowdigits n i < 2 ^ (64 * i)

lowdigits is always bounded by 2^(64*i).

Corresponds to HOL Light theorem:

let LOWDIGITS_BOUND = prove
 (`!n i. lowdigits n i < 2 EXP (64 * i)`, ...);;

Source: s2n-bignum/common/bignum.ml:139-141