Lemmas on 64-bit words for the contracts

Lemmas on the 64-bit words, unsigned and signed, that the contracts of the model need and Lean core lacks, under their names in the namespaces of Lean core: their bits, masks and shifts, their lowest set bit, the arithmetic of longs that does not overflow, and the branch-free minimum, distance and absolute value of longs. The lemmas on vectors, arrays, lists, ranges, natural numbers and integers are in Ratpoints.Proof.Containers.

Main statements

• UInt64.eq_of_getLsbD_eq: two words are equal when their bits are.
• UInt64.getLsbD_allOnes_shiftLeft, UInt64.getLsbD_allOnes_shiftRight: the bits of the masks.
• UInt64.getLsbD_and_sub_one, UInt64.toNat_and_sub_one_lt: for x ≠ 0, x &&& (x - 1) is x with its lowest set bit cleared, and smaller than x.
• UInt64.getLsbD_fold_or_one_shiftLeft, UInt64.getLsbD_fold_or_one_shiftLeft_comp: the bits of a word set one at a time, at their own positions or at the positions that a function gives.
• UInt64.getLsbD_shiftRight_or_shiftLeft: the 64 bits from position r on of the 128 bits of two words, for 0 < r < 64.
• UInt64.getLsbD_shiftLeft_ofNat, UInt64.getLsbD_shiftRight_ofNat, UInt64.getLsbD_toUInt64_shiftLeft: the bits of a word and of a Boolean shifted by an amount below 64.
• UInt64.getLsbD_foldl_and: the bits of a word and-ed in turn with the words of a list.
• UInt64.two_pow_ctz_mul_shiftRight_ofNat, UInt64.shiftRight_ctz_ofNat_mod_two: a number 0 < b < 2 ^ 64 is 2 ^ t times the odd number b >>> t, for the position t of the lowest set bit of the word b.
• Int64.toInt_shiftRight_ofNat, Int64.shiftRight_63: the arithmetic shift of a long by k < 64, and the mask x >>> 63, -1 for a negative x and 0 otherwise.
• Int64.toNatClampNeg_add_and_shiftRight_63, Int64.toNatClampNeg_xor_shiftRight_63_sub: for d = m - n, n + (d &&& d >>> 63) and (d ^^^ d >>> 63) - d >>> 63 are the smaller and the distance of two non-negative longs.
• Int64.two_pow_ctz_mul_toNatClampNeg_shiftRight, Int64.toNatClampNeg_shiftRight_ctz_mod_two: a positive long x is 2 ^ t times the odd number x >>> t, for the position t of the lowest set bit of the word x read as unsigned.
• Int64.toNatClampNeg_ite_neg: the absolute value of a long other than -2 ^ 63.
• Int64.minValue_lt_ofInt, Int64.ofNat_pos: the word of an integer |a| < 2 ^ 63 is not -2 ^ 63, and that of a natural number 0 < n < 2 ^ 63 is positive.
• Int64.toInt_add_of_lt, Int64.toInt_sub_of_lt, Int64.toInt_neg_of_lt, Int64.toInt_mul_of_lt: the sums, differences, negations and products of longs that do not overflow.
• Int64.toInt_and_one, Int64.toInt_shiftRight_one, Int64.toInt_one_shiftLeft: the lowest bit, the half and the powers of 2 of longs, for the midpoints of the bisection of the Sturm step.
• Int64.toInt_and_ofNat_two_pow_sub_one: a long and-ed with the mask 2 ^ k - 1 is its Euclidean remainder modulo 2 ^ k.
• UInt64.toNat_shift_words_of_lt, UInt64.toNat_shift_words_of_le: the two words of a 128-bit number shifted right by 0 < s < 64 and by 64 ≤ s ≤ 127.

Implementation notes

The file uses Lean core only, so that the grind calls of the proofs see only the lemmas of core, untouched by the updates of Mathlib.

Words

theorem Nat.mod_add_carry {x y : Nat} (hx : x < 2 ^ 64) (hy : y < 2 ^ 64) : (x + y) % 2 ^ 64 + (if (x + y) % 2 ^ 64 < y then 1 else 0) * 2 ^ 64 = x + y

The sum x + y of two numbers below 2 ^ 64, its low word (x + y) % 2 ^ 64 and the carry 1 exactly when the low word is below y.

theorem Nat.toNat_toUInt64_mod_sixty_four {n : Nat} (hn : n < 64) : n.toUInt64.toNat % 64 = n

A shift amount n < 64 is its own reduction modulo 64, which the shifts of words take.

theorem UInt64.getLsbD_allOnes (t : Nat) : (~~~0).toBitVec.getLsbD t = decide (t < 64)

theorem UInt64.getLsbD_allOnes_shiftLeft (n : UInt64) (t : Nat) : (~~~0 <<< n).toBitVec.getLsbD t = (decide (t < 64) && decide (n.toNat % 64 ≤ t))

theorem UInt64.getLsbD_allOnes_shiftRight (n : UInt64) (t : Nat) : (~~~0 >>> n).toBitVec.getLsbD t = decide (n.toNat % 64 + t < 64)

theorem UInt64.and_one_eq_zero_iff (x : UInt64) : x &&& 1 = 0 ↔ x.toBitVec.getLsbD 0 = false

theorem UInt64.toNat_ctz_lt {x : UInt64} (hx : x ≠ 0) : x.toBitVec.ctz.toNat < 64

theorem UInt64.getLsbD_ctz {x : UInt64} (hx : x ≠ 0) : x.toBitVec.getLsbD x.toBitVec.ctz.toNat = true

theorem UInt64.ne_ctz_of_and_one_eq_zero {w a : UInt64} {t : Nat} (hw : w ≠ 0) (ha : a.toBitVec = w.toBitVec >>> t) (h : a &&& 1 = 0) : t ≠ w.toBitVec.ctz.toNat

theorem UInt64.eq_ctz_of_and_one_ne_zero {w a : UInt64} {t : Nat} (ha : a.toBitVec = w.toBitVec >>> t) (ht : t ≤ w.toBitVec.ctz.toNat) (h : ¬a &&& 1 = 0) : t = w.toBitVec.ctz.toNat

theorem UInt64.getLsbD_and_sub_one {x : UInt64} (hx : x ≠ 0) (t : Nat) : (x &&& x - 1).toBitVec.getLsbD t = (x.toBitVec.getLsbD t && t != x.toBitVec.ctz.toNat)

x &&& (x - 1) is x with its lowest set bit cleared, since x - 1 = ~~~(-x) agrees with x above that bit and has the bit clear.

theorem UInt64.toNat_and_sub_one_lt {x : UInt64} (hx : x ≠ 0) : (x &&& x - 1).toNat < x.toNat

theorem UInt64.eq_of_getLsbD_eq {x y : UInt64} (h : ∀ (t : Nat), x.toBitVec.getLsbD t = y.toBitVec.getLsbD t) : x = y

Two words are equal when their bits are.

theorem UInt64.getLsbD_one_shiftLeft {t : Nat} (ht : t < 64) (s : Nat) : (1 <<< t.toUInt64).toBitVec.getLsbD s = decide (s = t)

theorem UInt64.getLsbD_fold_or_one_shiftLeft_comp (c : Nat → Bool) (f : Nat → Nat) {k : Nat} (hf : ∀ (i : Nat), i < k → f i < 64) (t : Nat) : (k.fold (fun (i : Nat) (x : i < k) (w : UInt64) => if c i = true then w ||| 1 <<< (f i).toUInt64 else w) 0).toBitVec.getLsbD t = decide (∃ (i : Nat), i < k ∧ c i = true ∧ f i = t)

The bits f i for the i < k for which c i holds, set one after the other in the word 0, for f i < 64.

theorem UInt64.getLsbD_fold_or_one_shiftLeft (c : Nat → Bool) {k : Nat} (hk : k ≤ 64) (t : Nat) : (k.fold (fun (i : Nat) (x : i < k) (w : UInt64) => if c i = true then w ||| 1 <<< i.toUInt64 else w) 0).toBitVec.getLsbD t = (decide (t < k) && c t)

The bits i < k for which c i holds, set one after the other in the word 0: the case f i = i of UInt64.getLsbD_fold_or_one_shiftLeft_comp.

theorem UInt64.getLsbD_or_one_shiftLeft (x : UInt64) {n : Nat} (hn : n < 64) (t : Nat) : (x ||| 1 <<< ofNat n).toBitVec.getLsbD t = (x.toBitVec.getLsbD t || decide (t = n))

theorem UInt64.getLsbD_shiftLeft_ofNat (x : UInt64) {n : Nat} (hn : n < 64) (t : Nat) : (x <<< ofNat n).toBitVec.getLsbD t = (decide (t < 64) && decide (n ≤ t) && x.toBitVec.getLsbD (t - n))

theorem UInt64.getLsbD_shiftRight_ofNat (x : UInt64) {n : Nat} (hn : n < 64) (t : Nat) : (x >>> ofNat n).toBitVec.getLsbD t = x.toBitVec.getLsbD (n + t)

theorem UInt64.getLsbD_toUInt64_shiftLeft (v : Bool) {n : Nat} (hn : n < 64) (t : Nat) : (v.toUInt64 <<< ofNat n).toBitVec.getLsbD t = (v && decide (t = n))

The bits of a Boolean shifted to the position n < 64, as RP_INIT_BIT sets a bit.

theorem UInt64.getLsbD_shiftRight_or_shiftLeft {r : Nat} (hr0 : r ≠ 0) (hr : r < 64) (x y : UInt64) (t : Nat) : (x >>> r.toUInt64 ||| y <<< (64 - r).toUInt64).toBitVec.getLsbD t = (decide (t < 64) && if r + t < 64 then x.toBitVec.getLsbD (r + t) else y.toBitVec.getLsbD (r + t - 64))

For 0 < r < 64, the word made of the bits of x from r on and the lowest r bits of y above them: the 64 bits from position r on of the 128 bits of x followed by y.

theorem UInt64.getLsbD_foldl_and {α : Type u} (f : α → UInt64) (l : List α) (init : UInt64) (t : Nat) : (List.foldl (fun (acc : UInt64) (a : α) => acc &&& f a) init l).toBitVec.getLsbD t = (init.toBitVec.getLsbD t && l.all fun (a : α) => (f a).toBitVec.getLsbD t)

The bits of a word and-ed in turn with the words f a of the entries a of a list.

theorem UInt64.ofNat_ne_zero_of_lt {b : Nat} (hb0 : 0 < b) (hb : b < size) : ofNat b ≠ 0

theorem UInt64.two_pow_ctz_mul_shiftRight_ofNat {b : Nat} (hb0 : 0 < b) (hb : b < size) : 2 ^ (ofNat b).toBitVec.ctz.toNat * b >>> (ofNat b).toBitVec.ctz.toNat = b

For 0 < b < 2 ^ 64, b is 2 ^ t times b >>> t, for the position t of the lowest set bit of the word b, since the bits of b below it are clear.

theorem UInt64.shiftRight_ctz_ofNat_mod_two {b : Nat} (hb0 : 0 < b) (hb : b < size) : b >>> (ofNat b).toBitVec.ctz.toNat % 2 = 1

For 0 < b < 2 ^ 64, b >>> t is odd, for the position t of the lowest set bit of the word b.

theorem UInt64.toNat_shiftRight_32 (x : UInt64) : (x >>> 32).toNat = x.toNat / 2 ^ 32

theorem UInt64.toNat_and_0xffffffff (x : UInt64) : (x &&& 4294967295).toNat = x.toNat % 2 ^ 32

theorem UInt64.and_not_eq_zero_iff (w m : UInt64) : w &&& ~~~m = 0 ↔ ∀ (t : Nat), w.toBitVec.getLsbD t = true → m.toBitVec.getLsbD t = true

theorem UInt64.getLsbD_or_shiftLeft (x : UInt64) {s : Nat} (hs : s < 64) (t : Nat) : (x ||| x <<< ofNat s).toBitVec.getLsbD t = (x.toBitVec.getLsbD t || decide (t < 64) && decide (s ≤ t) && x.toBitVec.getLsbD (t - s))

theorem UInt64.getLsbD_or_shiftLeft_of_dvd {x : UInt64} {g : Nat → Bool} {s P : Nat} (hPs : P ∣ s) (hs : s < 64) (hx : ∀ (t : Nat), x.toBitVec.getLsbD t = (decide (t < s) && g (t % P))) (t : Nat) : (x ||| x <<< ofNat s).toBitVec.getLsbD t = (decide (t < min (2 * s) 64) && g (t % P))

One doubling of a pattern g of period P ∣ s, s < 64, that fills the bits below s: the pattern then fills the bits below min (2 s) 64.

theorem UInt64.shiftRight_and_one_beq_zero (x : UInt64) {j : Nat} (hj : j < 64) : (x >>> ofNat j &&& 1 == 0) = !x.toBitVec.getLsbD j

theorem UInt64.getLsbD_getElem!_set!_or_one_shiftLeft {seen : Array UInt64} (hs : seen.size = 2) {K K0 : Nat} (hK : K < 128) : (seen.set! (K0 / 64) (seen[K0 / 64]! ||| 1 <<< ofNat (K0 % 64)))[K / 64]!.toBitVec.getLsbD (K % 64) = (seen[K / 64]!.toBitVec.getLsbD (K % 64) || decide (K = K0))

Setting bit K₀ of the 128 bits of the two words seen sets the bit K < 128 exactly when K = K₀, and keeps the others.

theorem UInt64.toNat_shiftRight_toUInt64 (x : UInt64) {s : Nat} (hs : s < 64) : (x >>> s.toUInt64).toNat = x.toNat / 2 ^ s

theorem UInt64.toNat_shift_words_of_lt (hi lo : UInt64) {s : Nat} (hs0 : 0 < s) (hs : s < 64) : (hi >>> s.toUInt64).toNat * 2 ^ 64 + (lo >>> s.toUInt64 ||| hi <<< (64 - s).toUInt64).toNat = (hi.toNat * 2 ^ 64 + lo.toNat) / 2 ^ s

The two words of a 128-bit number hi 2 ^ 64 + lo shifted right by 0 < s < 64.

theorem UInt64.toNat_shift_words_of_le (hi lo : UInt64) {s : Nat} (hs0 : 64 ≤ s) (hs : s ≤ 127) : (hi >>> (s - 64).toUInt64).toNat = (hi.toNat * 2 ^ 64 + lo.toNat) / 2 ^ s

The two words of a 128-bit number hi 2 ^ 64 + lo shifted right by 64 ≤ s ≤ 127.

theorem UInt64.two_pow_ctz_dvd {w : UInt64} : 2 ^ w.toBitVec.ctz.toNat ∣ w.toNat

A word is divisible by 2 ^ t for the position t of its lowest set bit (t = 64 for the word 0).

theorem UInt64.toNat_one_shiftLeft_sub_one {s : Nat} (hs : s < 64) : (1 <<< s.toUInt64 - 1).toNat = 2 ^ s - 1

The mask (1 <<< s) - 1 of the low s < 64 bits of a word, 2 ^ s - 1.

theorem UInt64.toInt_toInt64_of_lt {t : UInt64} (ht : t.toNat < 2 ^ 63) : t.toInt64.toInt = ↑t.toNat

theorem UInt64.toInt_toInt64_one_shiftLeft_sub_one {s : Nat} (hs : s < 64) : (1 <<< s.toUInt64 - 1).toInt64.toInt = 2 ^ s - 1

The mask (1 <<< s) - 1 of the low s < 64 bits of a word read as a long, 2 ^ s - 1.

Signed words

theorem Nat.toNat_toUInt64_toInt64 {B : Nat} (hB : B < 2 ^ 63) : B.toInt64.toUInt64.toNat = B

theorem Int64.toInt_shiftRight_ofNat (x : Int64) {k : Nat} (hk : k < 64) : (x >>> ofNat k).toInt = x.toInt >>> k

The arithmetic shift >>> of a long by k < 64 is the shift of its value, the floor of its quotient by 2 ^ k.

theorem Int64.shiftRight_63 (x : Int64) : x >>> 63 = if x < 0 then -1 else 0

The mask x >>> 63 of a long is -1 for a negative one and 0 otherwise.

theorem Int64.and_shiftRight_63 (x : Int64) : x &&& x >>> 63 = if x < 0 then x else 0

theorem Int64.xor_shiftRight_63_sub (x : Int64) : (x ^^^ x >>> 63) - x >>> 63 = if x < 0 then -x else x

theorem Int64.sub_lt_zero_iff_of_nonneg {a b : Int64} (ha : 0 ≤ a) (hb : 0 ≤ b) : a - b < 0 ↔ a < b

theorem Int64.toNatClampNeg_add_and_shiftRight_63 {m n : Int64} (hm : 0 ≤ m) (hn : 0 ≤ n) : (n + (m - n &&& (m - n) >>> 63)).toNatClampNeg = min m.toNatClampNeg n.toNatClampNeg

n + (d &&& d >>> 63) for d = m - n is the smaller of two non-negative longs m and n, without a branch.

theorem Int64.toNatClampNeg_xor_shiftRight_63_sub {m n : Int64} (hm : 0 ≤ m) (hn : 0 ≤ n) : ((m - n ^^^ (m - n) >>> 63) - (m - n) >>> 63).toNatClampNeg = if m.toNatClampNeg < n.toNatClampNeg then n.toNatClampNeg - m.toNatClampNeg else m.toNatClampNeg - n.toNatClampNeg

(d ^^^ d >>> 63) - d >>> 63 for d = m - n is the distance of two non-negative longs m and n, without a branch.

theorem Int64.xor_shiftRight_63_sub_pos {m n : Int64} (hm : 0 ≤ m) (hn : 0 ≤ n) (h : m ≠ n) : 0 < (m - n ^^^ (m - n) >>> 63) - (m - n) >>> 63

theorem Int64.toNatClampNeg_shiftRight_ofNat {x : Int64} (hx : 0 ≤ x) {k : Nat} (hk : k < 64) : (x >>> ofNat k).toNatClampNeg = x.toNatClampNeg >>> k

theorem Int64.toUInt64_eq_ofNat_toNatClampNeg {x : Int64} (hx : 0 ≤ x) : x.toUInt64 = UInt64.ofNat x.toNatClampNeg

theorem Int64.toUInt64_ne_zero_of_pos {x : Int64} (hx : 0 < x) : x.toUInt64 ≠ 0

theorem Int64.two_pow_ctz_mul_toNatClampNeg_shiftRight {x : Int64} (hx : 0 < x) : 2 ^ x.toUInt64.toBitVec.ctz.toNat * (x >>> ofNat x.toUInt64.toBitVec.ctz.toNat).toNatClampNeg = x.toNatClampNeg

A positive long x is 2 ^ t times x >>> t, for the position t of the lowest set bit of the word x read as unsigned.

theorem Int64.toNatClampNeg_shiftRight_ctz_mod_two {x : Int64} (hx : 0 < x) : (x >>> ofNat x.toUInt64.toBitVec.ctz.toNat).toNatClampNeg % 2 = 1

A positive long x shifted right by the position of the lowest set bit of the word x read as unsigned is odd.

theorem Int64.and_one_beq_zero_iff {x : Int64} (hx : 0 ≤ x) : (x &&& 1 == 0) = true ↔ x.toNatClampNeg % 2 = 0

theorem Int64.toNatClampNeg_eq_natAbs {x : Int64} (hx : 0 ≤ x) : x.toNatClampNeg = x.toInt.natAbs

theorem Int64.toNatClampNeg_ite_neg {x : Int64} (h : minValue < x) : (if x < 0 then -x else x).toNatClampNeg = x.toInt.natAbs

The absolute value of a long other than -2 ^ 63, whose negation would leave the range.

theorem Int64.toNatClampNeg_eq_one_iff (x : Int64) : x.toNatClampNeg = 1 ↔ x = 1

theorem Int64.minValue_lt_ofInt {a : Int} (ha : a.natAbs < 2 ^ 63) : minValue < ofInt a

theorem Int64.ofNat_pos {n : Nat} (h0 : 0 < n) (h : n < 2 ^ 63) : 0 < ofNat n

theorem Int64.toInt_add_of_lt {a b : Int64} (h1 : -2 ^ 63 ≤ a.toInt + b.toInt) (h2 : a.toInt + b.toInt < 2 ^ 63) : (a + b).toInt = a.toInt + b.toInt

theorem Int64.toInt_sub_of_lt {a b : Int64} (h1 : -2 ^ 63 ≤ a.toInt - b.toInt) (h2 : a.toInt - b.toInt < 2 ^ 63) : (a - b).toInt = a.toInt - b.toInt

theorem Int64.toInt_neg_of_lt {a : Int64} (h : -2 ^ 63 < a.toInt) : (-a).toInt = -a.toInt

theorem Int64.one_shiftLeft_sub_one {k : Nat} (hk : k ≤ 6) : 1 <<< ofNat k - 1 = ofNat (2 ^ k - 1)

The mask (1 <<< k) - 1 of the low k ≤ 6 bits of a long, 2 ^ k - 1.

theorem Int64.toInt_and_ofNat_two_pow_sub_one (x : Int64) {k : Nat} (hk : k < 63) : (x &&& ofNat (2 ^ k - 1)).toInt = x.toInt % 2 ^ k

A long and-ed with the mask 2 ^ k - 1 < 2 ^ 63 is its Euclidean remainder modulo 2 ^ k, also for a negative one, in two's complement.

theorem Int64.toInt_ofNat_two_pow_sub_one {k : Nat} (hk : k < 63) : (ofNat (2 ^ k - 1)).toInt = 2 ^ k - 1

theorem Int64.toInt_mul_of_lt {a b : Int64} (h1 : -2 ^ 63 ≤ a.toInt * b.toInt) (h2 : a.toInt * b.toInt < 2 ^ 63) : (a * b).toInt = a.toInt * b.toInt

The product of two longs that does not overflow.

theorem Int64.toInt_two_mul {x : Int64} (h : x.toInt.natAbs < 2 ^ 62) : (2 * x).toInt = 2 * x.toInt

theorem Int64.toInt_and_one (x : Int64) : (x &&& 1).toInt = x.toInt % 2

The lowest bit x &&& 1 of a long, its remainder modulo 2, also for a negative one.

theorem Int64.toInt_shiftRight_one (x : Int64) : (x >>> 1).toInt = x.toInt / 2

The arithmetic shift x >>> 1 of a long, the floor of its half.

theorem Int64.toInt_one_shiftLeft_ofNat {k : Nat} (hk : k < 63) : (1 <<< ofNat k).toInt = 2 ^ k

The power 1 <<< k of 2 for a shift k < 63.

theorem Int64.toInt_one_shiftLeft {k : Int64} (h0 : 0 ≤ k.toInt) (h : k.toInt < 63) : (1 <<< k).toInt = 2 ^ k.toInt.toNat

The power 1 <<< k of 2 for a long shift 0 ≤ k < 63.

theorem Int64.toInt_div_ofNat {a : Int64} (ha : 0 ≤ a.toInt) {n : Nat} (hn63 : n < 2 ^ 63) : (a / n.toInt64).toInt = a.toInt / ↑n

The quotient of a non-negative long by a natural number n < 2 ^ 63, the floor of the quotient of the values.

theorem Int64.natCast_toNat_toUInt64 {x : Int64} (hx : 0 ≤ x.toInt) : ↑x.toUInt64.toNat = x.toInt

theorem Int64.toInt_add_one_of_lt {e : Int64} (h : e.toInt < 2 ^ 63 - 1) : (e + 1).toInt = e.toInt + 1