proofs/lib/word.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as MWord
17 imports
import Base import ../../spec/lib/numeric.bend as SNUM 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/addition_bounds.bend as AB import ./lemmas/proofs/word_multiplication.bend as WM import ./lemmas/proofs/word_value.bend as WV import ./lemmas/proofs/negation_magnitude.bend as NM 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/word_addition.bend as WA import ./lemmas/proofs/modular_addition.bend as MA import ./lemmas/src/wide.bend as W
Definitions
def sc source · line 24 · raw
@+n:Nat -> @+k:Nat -> Nat
def uw source · line 27 · raw
@+n:Nat -> @+w:Word(n) -> Nat
def bo source · line 31 · raw
@b:Bool -> @+one:Nat -> Nat
a bit worth one
def bo_bit source · line 38 · raw
@+b:Bool -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {bo(b, one) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b) : Nat}
def lt1 source · line 45 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{Nat.is_lt(x, sc(n, one)) == True{} : Bool} -> {Nat.is_lt(x, sc(n, 1n)) == True{} : Bool}
def lt1r source · line 48 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{Nat.is_lt(x, sc(n, 1n)) == True{} : Bool} -> {Nat.is_lt(x, sc(n, one)) == True{} : Bool}
def wb source · line 52 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+w:Word(n) -> {Nat.is_lt(uw(n, w), sc(n, one)) == True{} : Bool}every n-bit word is below 2^n
def uniq source · line 56 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+r1:Nat -> @+r2:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.add(r1, sc(n, x)) == Nat.add(r2, sc(n, y)) : Nat} -> @+b1:{Nat.is_lt(r1, sc(n, one)) == True{} : Bool} -> @+b2:{Nat.is_lt(r2, sc(n, one)) == True{} : Bool} -> {r1 == r2 : Nat}r1 + 2^n x == r2 + 2^n y with both r below 2^n forces r1 == r2
def add_exact source · line 60 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:Word(n) -> @+b:Word(n) -> @+h:{Nat.is_lt(Nat.add(uw(n, a), uw(n, b)), sc(n, one)) == True{} : Bool} -> {uw(n, Word.add(n, a, b)) == Nat.add(uw(n, a), uw(n, b)) : Nat}addition below 2^n is exact
def mul_exact source · line 64 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:Word(n) -> @+b:Word(n) -> @+h:{Nat.is_lt(Nat.mul(uw(n, a), uw(n, b)), sc(n, one)) == True{} : Bool} -> {uw(n, Word.mul(n, a, b)) == Nat.mul(uw(n, a), uw(n, b)) : Nat}multiplication below 2^n is exact
def sub_wrap source · line 72 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+xw:Word(n) -> @+bw:Word(n) -> @+d:Nat -> @+e:{Nat.add(uw(n, xw), sc(n, one)) == Nat.add(d, uw(n, bw)) : Nat} -> @+hd:{Nat.is_lt(d, sc(n, one)) == True{} : Bool} -> {uw(n, Word.sub(n, xw, bw)) == d : Nat}If x + 2^n == d + b with d < 2^n, the machine difference x - b is d.
def ob source · line 95 · raw
@-n:Nat -> @r:Pair(Bool, Word(n)) -> Bool
def ow source · line 99 · raw
@-n:Nat -> @r:Pair(Bool, Word(n)) -> Word(n)
def shl_con source · line 103 · raw
@+p:Nat -> @+c:Bool -> @+b:Bool -> @+tl:Word(p) -> @r:Pair(Bool, Word(p)) -> @ih:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, ow(p, r)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.scale_binary(p, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(ob(p, r)))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(p, tl))) : Nat} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(1n+p, ow(1n+p, Word.shl.out.con(p, c, r))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.scale_binary(1n+p, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(ob(1n+p, Word.shl.out.con(p, c, r))))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c), Nat.double(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(1n+p, WCon{b, tl}))) : Nat}
def shl_nil source · line 111 · raw
@+c:Bool -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(0n, ow(0n, Word.shl.out(0n, c, WNil{}))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.scale_binary(0n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(ob(0n, Word.shl.out(0n, c, WNil{}))))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c), Nat.double(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(0n, WNil{}))) : Nat}
def shl_out source · line 119 · raw
@+n:Nat -> @+c:Bool -> @+w:Word(n) -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(n, ow(n, Word.shl.out(n, c, w))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.scale_binary(n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(ob(n, Word.shl.out(n, c, w))))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c), Nat.double(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(n, w))) : Nat}the out-shifted bit and word together hold c + 2w
def shl_out1 source · line 127 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:Bool -> @+w:Word(n) -> {Nat.add(uw(n, ow(n, Word.shl.out(n, c, w))), sc(n, bo(ob(n, Word.shl.out(n, c, w)), one))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c), Nat.double(uw(n, w))) : Nat}the same with the out-shifted bit worth one
def add_inner source · line 133 · raw
@+n:Nat -> @+h:Nat -> @+t:Nat -> @+c0:Nat -> @+c1:Nat -> @+c2:Nat -> @+ah:Nat -> @+bh:Nat -> @+f2:{Nat.add(t, sc(n, c1)) == Nat.add(ah, bh) : Nat} -> @+f3:{Nat.add(h, sc(n, c2)) == Nat.add(t, c0) : Nat} -> {Nat.add(h, Nat.add(sc(n, c1), sc(n, c2))) == Nat.add(c0, Nat.add(ah, bh)) : Nat}
def add_alg source · line 144 · raw
@+n:Nat -> @+l:Nat -> @+h:Nat -> @+t:Nat -> @+c0:Nat -> @+c1:Nat -> @+c2:Nat -> @+al:Nat -> @+ah:Nat -> @+bl:Nat -> @+bh:Nat -> @+f1:{Nat.add(l, sc(n, c0)) == Nat.add(al, bl) : Nat} -> @+f2:{Nat.add(t, sc(n, c1)) == Nat.add(ah, bh) : Nat} -> @+f3:{Nat.add(h, sc(n, c2)) == Nat.add(t, c0) : Nat} -> {Nat.add(Nat.add(l, sc(n, h)), sc(n, sc(n, Nat.add(c1, c2)))) == Nat.add(Nat.add(al, sc(n, ah)), Nat.add(bl, sc(n, bh))) : Nat}low limbs l with carry c0, high limbs t = ah + bh (carry c1), then h = t + c0 (carry c2): the two-limb sum loses exactly 2^(2n) (c1 + c2).
def carry_lt source · line 158 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Nat -> @+x:Nat -> @+y:Nat -> @+c:Bool -> @+e:{Nat.add(s, sc(n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c))) == Nat.add(x, y) : Nat} -> @+hy:{Nat.is_lt(y, sc(n, one)) == True{} : Bool} -> {Nat.is_lt(s, x) == c : Bool}the carry out of an addition is the wrap-around test sum < x
def not_join source · line 174 · raw
@+n:Nat -> @+m:Nat -> @+a:Word(n) -> @+b:Word(m) -> {Word.not(Nat.add(n, m), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.join(n, m, a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.join(n, m, Word.not(n, a), Word.not(m, b)) : Word(Nat.add(n, m))}
def ones source · line 182 · raw
@+n:Nat -> @w:Word(n) -> Bool
every bit set
def incif source · line 189 · raw
@+m:Nat -> @c:Bool -> @b:Word(m) -> Word(m)
def inc_join source · line 197 · raw
@+n:Nat -> @+m:Nat -> @+a:Word(n) -> @+b:Word(m) -> {Word.inc(Nat.add(n, m), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.join(n, m, a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.join(n, m, Word.inc(n, a), incif(m, ones(n, a), b)) : Word(Nat.add(n, m))}incrementing a joined word carries into the high part iff the low part is all ones
def eq_fin_tf source · line 206 · raw
@+c:Cmp -> {Cmp.is_eq(Word.cmp.fin(True{}, False{}, c)) == False{} : Bool}
def eq_fin_ff source · line 215 · raw
@+c:Cmp -> {Cmp.is_eq(Word.cmp.fin(False{}, False{}, c)) == Cmp.is_eq(c) : Bool}
def inc_zero source · line 225 · raw
@+n:Nat -> @+x:Word(n) -> {Cmp.is_eq(Word.cmp(n, Word.inc(n, x), Word.zero(n))) == ones(n, x) : Bool}an increment is zero iff it wrapped from all ones
def one_word source · line 234 · raw
@+p:Nat -> Word(1n+p)
def add_one source · line 238 · raw
@+p:Nat -> @+x:Word(1n+p) -> {Word.add(1n+p, x, one_word(p)) == Word.inc(1n+p, x) : Word(1n+p)}adding one is incrementing
def mask source · line 251 · raw
@+n:Nat -> @+k:Nat -> Word(n)
the low k bits set
def hi_part source · line 255 · raw
@+n:Nat -> @+k:Nat -> @+x:Word(n) -> Nat
the bits of x above the low k
def and_false_bv source · line 264 · raw
@+b:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(Bool.and(b, False{})) == 0n : Nat}
def and_zero source · line 271 · raw
@+p:Nat -> @+t:Word(p) -> {uw(p, Word.and(p, t, mask(p, 0n))) == 0n : Nat}
def low0 source · line 279 · raw
@+p:Nat -> @+b:Bool -> @+t:Word(p) -> {uw(1n+p, Word.and(1n+p, WCon{b, t}, mask(1n+p, 0n))) == 0n : Nat}
def mask_split source · line 287 · raw
@+n:Nat -> @+k:Nat -> @+x:Word(n) -> {uw(n, x) == Nat.add(uw(n, Word.and(n, x, mask(n, k))), sc(k, hi_part(n, k, x))) : Nat}x == (x & mask k) + 2^k (bits above k)
def sc_pos source · line 303 · raw
@+k:Nat -> {Nat.is_lt(0n, sc(k, 1n)) == True{} : Bool}
def mask_lt source · line 311 · raw
@+n:Nat -> @+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Word(n) -> {Nat.is_lt(uw(n, Word.and(n, x, mask(n, k))), sc(k, one)) == True{} : Bool}x & mask k is below 2^k
def pw source · line 322 · raw
@+n:Nat -> @+k:Nat -> Word(n)
2^k as an n-bit word
def pw_val source · line 331 · raw
@+n:Nat -> @+k:Nat -> @+hk:{Nat.is_lt(k, n) == True{} : Bool} -> {uw(n, pw(n, k)) == sc(k, 1n) : Nat}
def pwv source · line 341 · raw
@+n:Nat -> @+k:Nat -> @+hk:{Nat.is_lt(k, n) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:Word(n) -> @+hc:{c == pw(n, k) : Word(n)} -> {uw(n, c) == sc(k, one) : Nat}a word known to be 2^k has value 2^k (the word stays a variable)
def inc_exact source · line 346 · raw
@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+w:Word(n) -> @+h:{Nat.is_lt(1n+uw(n, w), sc(n, one)) == True{} : Bool} -> {uw(n, Word.inc(n, w)) == 1n+uw(n, w) : Nat}an increment below 2^n is exact