proofs/math/natural/bits.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as Bits

7 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/natural.bend as M
import ./arith.bend as R

Definitions

def half_eq source · line 17 · raw

@+n:Nat -> {n == Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)) : Nat}

n == 2 (n / 2) + n mod 2

def add_succ_nle source · line 22 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.add(a, 1n+b), a) == False{} : Bool}

a + (1 + b) <= a is false

def half_lt source · line 30 · raw

@+np:Nat -> {Nat.is_lt(Nat.div(1n+np, 2n), 1n+np) == True{} : Bool}

n / 2 < n for n > 0

def half_rem source · line 38 · raw

@+n:Nat -> {Nat.is_lt(Nat.mod(n, 2n), 2n) == True{} : Bool}

n mod 2 <= 1

def go_acc source · line 43 · raw

@fuel:Nat -> @+n:Nat -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bit_length_go(fuel, n, 1n+k) == 1n+0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bit_length_go(fuel, n, k) : Nat}

def go_zero source · line 52 · raw

@+fuel:Nat -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bit_length_go(fuel, 0n, k) == k : Nat}

def half_fuel source · line 60 · raw

@+np:Nat -> @+f:Nat -> @+hf:{Nat.is_le(np, f) == True{} : Bool} -> {Nat.is_le(Nat.div(1n+np, 2n), f) == True{} : Bool}

the halved argument stays within the fuel

def half_bound source · line 64 · raw

@+np:Nat -> {Nat.is_lt(1n+np, Nat.double(1n+Nat.div(1n+np, 2n))) == True{} : Bool}

2 h + r < 2 (1 + h) for r < 2

def lt_go source · line 70 · raw

@fuel:Nat -> @+n:Nat -> @+hf:{Nat.is_le(n, fuel) == True{} : Bool} -> {Nat.is_lt(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bit_length_go(fuel, n, 0n))) == True{} : Bool}

def bit_length_lt source · line 86 · raw

@+n:Nat -> {Nat.is_lt(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bit_length(n))) == True{} : Bool}

n < 2^bit_length(n) (Mathlib Nat.lt_size_self)

def le_step source · line 90 · raw

@+np:Nat -> @+h:Nat -> @+x:Nat -> @+e:{1n+np == Nat.add(Nat.double(h), Nat.mod(1n+np, 2n)) : Nat} -> @+ih:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(x), Nat.max(1n, Nat.double(h))) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(x), 1n+np) == True{} : Bool}

the lower bound, as 2^L <= max(1, 2 n)

def le_go source · line 97 · raw

@fuel:Nat -> @+n:Nat -> @+hf:{Nat.is_le(n, fuel) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bit_length_go(fuel, n, 0n)), Nat.max(1n, Nat.double(n))) == True{} : Bool}

def bit_length_le source · line 113 · raw

@+np:Nat -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bit_length(1n+np)), Nat.double(1n+np)) == True{} : Bool}

2^bit_length(n) <= 2 n for n > 0, i.e. 2^(bit_length(n) - 1) <= n (Mathlib Nat.size_le)

def bit_length_zero source · line 116 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bit_length(0n) == 0n : Nat}