~/bend-docscommunity

proofs/math/typed/w64div.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64div.bend as W64div

17 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/u32.bend as U
import ../../lib/u32div.bend as UD
import ../../lib/word.bend as WD
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ../u64/u64div.bend as PD
import ./w64mul.bend as WM
import ./u32.bend as U32P
import ./shrn.bend as SR

Definitions

def v source · line 27 · raw

@+x:U32 -> Nat

def lo_dig source · line 32 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+lo:U32 -> @+c16:U32 -> @+m16:U32 -> @+h16:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(c16) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one) : Nat} -> @+hm16:{m16 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 16n)} : U32} -> @+nz16:{U32.is_zero(c16) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(lo) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.div(lo, c16))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(lo, m16))) : Nat}

def k256 source · line 47 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {256n == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one) : Nat}

def add_twice source · line 57 · raw

@+a:Nat -> @+x:Nat -> @+b:Nat -> @+c:Nat -> @+hb:{Nat.add(a, x) == b : Nat} -> @+hc:{Nat.add(a, b) == c : Nat} -> {c == Nat.add(Nat.add(a, a), x) : Nat}

c == (a + a) + x when a + x == b and a + b == c

def oct source · line 63 · raw

@+one:Nat -> @+e:Nat -> @+l1:Nat -> @+l2:Nat -> @+l3:Nat -> @+l4:Nat -> @+l5:Nat -> @+l6:Nat -> @+l7:Nat -> @+l8:Nat -> @+h1:{l1 == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(e, one) : Nat} -> @+h2:{Nat.add(l1, l1) == l2 : Nat} -> @+h3:{Nat.add(l1, l2) == l3 : Nat} -> @+h4:{Nat.add(l1, l3) == l4 : Nat} -> @+h5:{Nat.add(l1, l4) == l5 : Nat} -> @+h6:{Nat.add(l1, l5) == l6 : Nat} -> @+h7:{Nat.add(l1, l6) == l7 : Nat} -> @+h8:{Nat.add(l1, l7) == l8 : Nat} -> {l8 == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(3n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(e, one)) : Nat}

eight steps of a: L_i == i * a, so L8 == 2^3 * a

def k8192 source · line 77 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {8192n == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(13n, one) : Nat}

def k65536 source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {65536n == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one) : Nat}

def mstep source · line 86 · raw

@+dp:Nat -> @+x:Nat -> @+b:Nat -> @+g:Nat -> {Nat.mod(Nat.add(Nat.mul(Nat.mod(x, 1n+dp), b), g), 1n+dp) == Nat.mod(Nat.add(Nat.mul(x, b), g), 1n+dp) : Nat}

def x2_eq source · line 93 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:Nat -> @+g1:Nat -> @+g2:Nat -> {Nat.add(Nat.mul(Nat.add(Nat.mul(h, 65536n), g1), 65536n), g2) == Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, g1), g2), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, h)) : Nat}

def d1g source · line 106 · raw

@+lo:U32 -> @+c16:U32 -> Nat

def d2g source · line 109 · raw

@+lo:U32 -> @+m16:U32 -> Nat

def mod32g source · line 112 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> @+c16:U32 -> @+m16:U32 -> U32

def dig1_eq source · line 116 · raw

@+lo:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.dig1(lo) == d1g(lo, 65536) : Nat}

the high digit is a shift, U32.shrn(lo, 16), the word U32.div(lo, 2^16)

def impl_mod source · line 119 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mod32(a, d) == mod32g(a, d, 65536, 65535) : U32}

def mod_inner source · line 123 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk:{k == 32n : Nat} -> @+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> @+c16:U32 -> @+p16:{c16 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> @+m16:U32 -> @+pm16:{m16 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 16n)} : U32} -> @+nd:Nat -> @+hnd:{v(d) == nd : Nat} -> {v(mod32g(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{lo, hi}, d, c16, m16)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{lo, hi}), v(d)) : Nat}

def mod32_value source · line 150 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.Mod32.value(a, d, hd)

Mod32.value: a 64-bit value mod a nonzero U32

def div32_rem source · line 157 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.Div32.rem(a, d, hd)

Div32.rem: div32's remainder is mod32's term

def dstep source · line 163 · raw

@+A:Nat -> @+D:Nat -> @+r:Nat -> @+b:Nat -> @+g:Nat -> @+q2:Nat -> @+r2:Nat -> @+e:{Nat.add(Nat.mul(r, b), g) == Nat.add(Nat.mul(q2, D), r2) : Nat} -> {Nat.add(Nat.mul(Nat.add(Nat.mul(A, D), r), b), g) == Nat.add(Nat.mul(Nat.add(Nat.mul(A, b), q2), D), r2) : Nat}

one digit of long division: (A D + r) b + g == (A b + q2) D + r2 when r b + g == q2 D + r2

def lt_cancel_mul_c source · line 166 · raw

@+a:Nat -> @+b:Nat -> @+d:Nat -> @+h:{Nat.is_lt(Nat.mul(a, d), Nat.mul(b, d)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(a, b) == c : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def lt_cancel_mul source · line 173 · raw

@+a:Nat -> @+b:Nat -> @+d:Nat -> @+h:{Nat.is_lt(Nat.mul(a, d), Nat.mul(b, d)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def div32q_g source · line 176 · raw

@+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+c16:U32 -> @+m16:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def impl_q source · line 179 · raw

@+lo:U32 -> @+hi:U32 -> @+d:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.fst_q(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.div32(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{lo, hi}, d)) == div32q_g(lo, hi, d, 65536, 65535) : 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64}

def bound_lt source · line 186 · raw

@+q:Nat -> @+y:Nat -> @+b:Nat -> @+s:Nat -> @+n:Nat -> @+n2:Nat -> @+hn:{n == n2 : Nat} -> @+hb:{Nat.mul(n, s) == b : Nat} -> @+hqy:{Nat.is_le(q, y) == True{} : Bool} -> @+hyb:{Nat.is_lt(y, b) == True{} : Bool} -> {Nat.is_lt(q, Nat.mul(s, n2)) == True{} : Bool}

Q <= Y < B with B == n * S gives Q < S * n2 for n == n2. The bound stays 2^32 * v(d) with v(d) opaque: 2^32 * (1 + dp) would unfold into 2^32 successors.

def quot_core source · line 191 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk:{k == 32n : Nat} -> @+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> @+c16:U32 -> @+p16:{c16 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> @+m16:U32 -> @+pm16:{m16 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 16n)} : U32} -> @+dp:Nat -> @+hnd:{v(d) == 1n+dp : Nat} -> {Nat.add(U32.to_nat(U32.from_nat(Nat.add(Nat.mul(Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), 1n+dp), 65536n), Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.dig_t(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), 1n+dp), 65536n, d2g(lo, m16)), 1n+dp)))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(32n, v(U32.div(hi, d)))) == Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{lo, hi}), 1n+dp) : Nat}

def quot_inner source · line 227 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk:{k == 32n : Nat} -> @+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> @+c16:U32 -> @+p16:{c16 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> @+m16:U32 -> @+pm16:{m16 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 16n)} : U32} -> @+nd:Nat -> @+hnd:{v(d) == nd : Nat} -> {Nat.add(U32.to_nat(U32.from_nat(Nat.add(Nat.mul(Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), v(d)), 65536n), Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.dig_t(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), v(d)), 65536n, d2g(lo, m16)), v(d))))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(32n, v(U32.div(hi, d)))) == Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{lo, hi}), v(d)) : Nat}

def div32_quot source · line 235 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> @+hd:{U32.is_zero(d) == False{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.Div32.quot(a, d, hd)

Div32.quot: a 64-bit value divided by a nonzero U32