proofs/lib/u32div.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as U32div

13 imports

import Base
import ./lemmas/spec/numeric.bend as S
import ./nat.bend as N
import ./logic.bend as L
import ./u32.bend as U
import ./u32alg.bend as A
import ./lemmas/proofs/nat_algebra.bend as NA
import ./lemmas/proofs/natural_products.bend as PR
import ./lemmas/proofs/division_bounds.bend as DB
import ./lemmas/proofs/division_quotient.bend as DQ
import ./lemmas/proofs/natural_division.bend as ND
import ./lemmas/proofs/word_comparison.bend as WC
import ./word.bend as WD

Definitions

def v source · line 23 · raw

@+x:U32 -> Nat

def dq source · line 26 · raw

@-m:Nat -> @r:Pair(Word(m), U32) -> Word(m)

def dr source · line 30 · raw

@-m:Nat -> @r:Pair(Word(m), U32) -> U32

def inv source · line 35 · raw

@+m:Nat -> @+a:Word(m) -> @+bn:Nat -> @r:Pair(Word(m), U32) -> Type

the long-division invariant of a partial result r for the prefix a

def digit_one source · line 41 · raw

@+q:Nat -> @+bn:Nat -> @+r:Nat -> @+a:Nat -> @+d:Nat -> @+h:{Nat.add(bn, d) == Nat.add(a, Nat.double(r)) : Nat} -> {Nat.add(Nat.mul(1n+Nat.double(q), bn), d) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}

a subtracting digit: (1 + 2q) b + d == a + 2 (q b + r) when b + d == a + 2 r

def digit_zero source · line 52 · raw

@+q:Nat -> @+bn:Nat -> @+r:Nat -> @+a:Nat -> {Nat.add(Nat.mul(Nat.double(q), bn), Nat.add(a, Nat.double(r))) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}

a zero digit: 2q b + (a + 2 r) == a + 2 (q b + r)

def vw source · line 61 · raw

@+w:Word(32n) -> {v(U32{w}) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.uw(32n, w) : Nat}

def vb source · line 64 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> {Nat.is_lt(v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}

def sub32 source · line 70 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+b:U32 -> @+d:Nat -> @+e:{Nat.add(v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == Nat.add(d, v(b)) : Nat} -> @+hd:{Nat.is_lt(d, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {v(U32.sub(x, b)) == d : Nat}

def fin_true source · line 81 · raw

@+p:Nat -> @+q:Word(p) -> @+s:U32 -> @+b:U32 -> @+a0:Bool -> @+hi:Word(p) -> @+r:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+he:{Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, q), v(b)), r) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, hi) : Nat} -> @+hr:{Nat.is_lt(r, v(b)) == True{} : Bool} -> @+hts:{Nat.add(v(s), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(a0), Nat.double(r)) : Nat} -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, True{}))

def fin_ge source · line 102 · raw

@+p:Nat -> @+q:Word(p) -> @+s:U32 -> @+b:U32 -> @+a0:Bool -> @+hi:Word(p) -> @+r:Nat -> @+he:{Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, q), v(b)), r) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, hi) : Nat} -> @+hr:{Nat.is_lt(r, v(b)) == True{} : Bool} -> @+hs:{v(s) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(a0), Nat.double(r)) : Nat} -> @+hge:{Nat.is_ge(v(s), v(b)) == True{} : Bool} -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, True{}))

def fin_lt source · line 119 · raw

@+p:Nat -> @+q:Word(p) -> @+s:U32 -> @+b:U32 -> @+a0:Bool -> @+hi:Word(p) -> @+r:Nat -> @+he:{Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, q), v(b)), r) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, hi) : Nat} -> @+hs:{v(s) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(a0), Nat.double(r)) : Nat} -> @+hge:{Nat.is_ge(v(s), v(b)) == False{} : Bool} -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, False{}))

def fin_false source · line 129 · raw

@+p:Nat -> @+q:Word(p) -> @+s:U32 -> @+b:U32 -> @+a0:Bool -> @+hi:Word(p) -> @+r:Nat -> @+he:{Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, q), v(b)), r) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, hi) : Nat} -> @+hr:{Nat.is_lt(r, v(b)) == True{} : Bool} -> @+hs:{v(s) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(a0), Nat.double(r)) : Nat} -> @+g:Bool -> @+hg:{U32.is_ge(s, b) == g : Bool} -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, g))

def shl_ts source · line 136 · raw

@+p:Nat -> @+q:Word(p) -> @+b:U32 -> @+t:Bool -> @+s:Word(32n) -> @+a0:Bool -> @+hi:Word(p) -> @+r:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+he:{Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, q), v(b)), r) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, hi) : Nat} -> @+hr:{Nat.is_lt(r, v(b)) == True{} : Bool} -> @+hts:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.uw(32n, s), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.bo(t, one))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(a0), Nat.double(r)) : Nat} -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, U32{s}, b, Bool.or(t, U32.is_ge(U32{s}, b))))

def shl_ok source · line 144 · raw

@+p:Nat -> @+q:Word(p) -> @+b:U32 -> @ts:Pair(Bool, Word(32n)) -> @+a0:Bool -> @+hi:Word(p) -> @+r:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+he:{Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, q), v(b)), r) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, hi) : Nat} -> @+hr:{Nat.is_lt(r, v(b)) == True{} : Bool} -> @hts:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.uw(32n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.ow(32n, ts)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.bo(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.ob(32n, ts), one))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(a0), Nat.double(r)) : Nat} -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.shl(p, q, b, ts))

def rec_ok source · line 149 · raw

@+p:Nat -> @+a0:Bool -> @+b:U32 -> @+hi:Word(p) -> @qr:Pair(Word(p), U32) -> @ih:inv(p, hi, v(b), qr) -> @+one:Nat -> @+h1:{one == 1n : Nat} -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.rec(p, a0, b, qr))

def go_ok source · line 161 · raw

@+m:Nat -> @+a:Word(m) -> @+b:U32 -> @+hb:{Nat.is_lt(0n, v(b)) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> inv(m, a, v(b), U32.divmod.go(m, a, b))

the invariant holds for every prefix of the dividend

def pos_nat source · line 170 · raw

@+x:Nat -> @+h:{Cmp.is_eq(Nat.cmp(x, 0n)) == False{} : Bool} -> {Nat.is_lt(0n, x) == True{} : Bool}

def pos source · line 177 · raw

@+b:U32 -> @+hb:{U32.is_zero(b) == False{} : Bool} -> {Nat.is_lt(0n, v(b)) == True{} : Bool}

def dm_fin source · line 180 · raw

@+aw:Word(32n) -> @+b:U32 -> @qr:Pair(Word(32n), U32) -> @h:inv(32n, aw, v(b), qr) -> Pair({Nat.add(Nat.mul(v(U32.div.fin(qr)), v(b)), v(U32.mod.fin(qr))) == v(U32{aw}) : Nat}, {Nat.is_lt(v(U32.mod.fin(qr)), v(b)) == True{} : Bool})

def dm_if source · line 189 · raw

@+aw:Word(32n) -> @+b:U32 -> @+z:Bool -> @+hz:{z == False{} : Bool} -> @+hb:{Nat.is_lt(0n, v(b)) == True{} : Bool} -> Pair({Nat.add(Nat.mul(v(U32.div.if(aw, b, z)), v(b)), v(U32.mod.if(aw, b, z))) == v(U32{aw}) : Nat}, {Nat.is_lt(v(U32.mod.if(aw, b, z)), v(b)) == True{} : Bool})

def div_mod source · line 197 · raw

@+a:U32 -> @+b:U32 -> @+hb:{U32.is_zero(b) == False{} : Bool} -> Pair({Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))) == v(a) : Nat}, {Nat.is_lt(v(U32.mod(a, b)), v(b)) == True{} : Bool})

THEOREM: div and mod are Euclidean division by any nonzero divisor.

def mod_identify source · line 202 · raw

@+q:Nat -> @+d:Nat -> @+r:Nat -> @+bound:{Nat.is_lt(r, d) == True{} : Bool} -> {Nat.mod(Nat.add(Nat.mul(q, d), r), d) == r : Nat}

def dm_type source · line 209 · raw

@+a:U32 -> @+b:U32 -> Type

def div_of source · line 212 · raw

@+a:U32 -> @+b:U32 -> @h:dm_type(a, b) -> {v(U32.div(a, b)) == Nat.div(v(a), v(b)) : Nat}

def mod_of source · line 217 · raw

@+a:U32 -> @+b:U32 -> @h:dm_type(a, b) -> {v(U32.mod(a, b)) == Nat.mod(v(a), v(b)) : Nat}

def div_nat source · line 223 · raw

@+a:U32 -> @+b:U32 -> @+hb:{U32.is_zero(b) == False{} : Bool} -> {v(U32.div(a, b)) == Nat.div(v(a), v(b)) : Nat}

THEOREM: div is Nat division.

def mod_nat source · line 227 · raw

@+a:U32 -> @+b:U32 -> @+hb:{U32.is_zero(b) == False{} : Bool} -> {v(U32.mod(a, b)) == Nat.mod(v(a), v(b)) : Nat}

THEOREM: mod is Nat remainder.