~/bend-docscommunity

lemmas.bend checks

raw source on the hub · import bend-kit-lemmas@0.1.0.0/lemmas.bend as Lemmas

Proved laws that relate Word and U32 arithmetic to Nat. Source: https://github.com/paymog/bend-kit/tree/main/lemmas

2 imports
import Base
import bend-mathlib@0.7.2.0/nat.bend as MNat

Laws

law to_nat_con provedsource · line 21 · raw

@-p:Nat -> @x:Bool -> @-t:Word(p) -> {bit(x, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{x, t}) : Nat}

law cmp_bit provedsource · line 34 · raw

@a:Nat -> @b:Nat -> @x:Bool -> @y:Bool -> {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(bit(x, a), bit(y, b)) : Cmp}

law word_cmp_nat provedsource · line 85 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}

Comparing two words compares their values.

law u32_cmp_nat provedsource · line 108 · raw

@a:U32 -> @b:U32 -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}

law u32_is_lt_nat provedsource · line 118 · raw

@a:U32 -> @b:U32 -> {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}

law u32_is_le_nat provedsource · line 127 · raw

@a:U32 -> @b:U32 -> {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}

law u32_is_eq_nat provedsource · line 136 · raw

@a:U32 -> @b:U32 -> {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}

law odd_lt_double provedsource · line 145 · raw

@a:Nat -> @b:Nat -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(a, b) -> 0x449abff091641d732d7b9f0780df40ae/nat.lt(1n+Nat.double(a), Nat.double(b))

law word_to_nat_lt provedsource · line 163 · raw

@n:Nat -> @w:Word(n) -> 0x449abff091641d732d7b9f0780df40ae/nat.lt(Word.to_nat(n, w), pow2(n))

A word of n bits has a value below 2^n.

law u32_to_nat_word provedsource · line 179 · raw

@-x:Word(32n) -> {Word.to_nat(32n, x) == U32.to_nat(U32{x}) : Nat}

law u32_to_nat_lt provedsource · line 186 · raw

@a:U32 -> 0x449abff091641d732d7b9f0780df40ae/nat.lt(U32.to_nat(a), pow2(32n))

law double_inj provedsource · line 197 · raw

@a:Nat -> @b:Nat -> @h:{Nat.double(a) == Nat.double(b) : Nat} -> {a == b : Nat}

law double_ne_odd provedsource · line 216 · raw

@a:Nat -> @b:Nat -> @h:{Nat.double(a) == 1n+Nat.double(b) : Nat} -> Empty

law word_to_nat_inj provedsource · line 235 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @h:{Word.to_nat(n, a) == Word.to_nat(n, b) : Nat} -> {a == b : Word(n)}

Two words with the same value are the same word.

law u32_to_nat_inj provedsource · line 265 · raw

@a:U32 -> @b:U32 -> @h:{U32.to_nat(a) == U32.to_nat(b) : Nat} -> {a == b : U32}

law scale_double provedsource · line 313 · raw

@q:Bool -> @-m:Nat -> {Nat.double(scale(q, m)) == scale(q, Nat.double(m)) : Nat}

law adc_step provedsource · line 326 · raw

@+s:Nat -> @+x:Nat -> @+y:Nat -> @+c:Nat -> @+k:Nat -> @+r:Nat -> @+q:Bool -> @+m:Nat -> @+a:Nat -> @+b:Nat -> @ih:{Nat.add(r, scale(q, m)) == Nat.add(k, Nat.add(a, b)) : Nat} -> @fa:{Nat.add(c, Nat.add(x, y)) == Nat.add(s, Nat.double(k)) : Nat} -> {Nat.add(Nat.add(s, Nat.double(r)), scale(q, Nat.double(m))) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}

One bit of the adder: s + 2k is the sum c + x + y of the three input bits.

law word_adc_nat provedsource · line 356 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @c:Bool -> {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), scale(carry(n, a, b, c), pow2(n))) == Nat.add(b2n(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}

The adder is exact: the word sum plus the carry-out weight 2^n is c + a + b.

law lt_rw provedsource · line 409 · raw

@-a:Nat -> @-b:Nat -> @-c:Nat -> @e:{a == b : Nat} -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(b, c) -> 0x449abff091641d732d7b9f0780df40ae/nat.lt(a, c)

Moves a strict upper bound across an equation without a conversion check.

law add_no_carry provedsource · line 421 · raw

@q:Bool -> @+r:Nat -> @+m:Nat -> @+s:Nat -> @e:{Nat.add(r, scale(q, m)) == s : Nat} -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(s, m) -> {r == s : Nat}

law add_mod_carry provedsource · line 438 · raw

@q:Bool -> @+r:Nat -> @+m:Nat -> @+s:Nat -> @e:{Nat.add(r, scale(q, m)) == s : Nat} -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(r, m) -> {r == Nat.mod(s, m) : Nat}

law word_add_nat provedsource · line 460 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)) -> {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}

Addition without overflow is exact.

law word_add_mod provedsource · line 472 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)) : Nat}

Addition wraps modulo 2^n.

law u32_add_word provedsource · line 484 · raw

@-x:Word(32n) -> @-y:Word(32n) -> {Word.to_nat(32n, Word.add(32n, x, y)) == U32.to_nat(U32.add(U32{x}, U32{y})) : Nat}

law u32_add_nat provedsource · line 492 · raw

@a:U32 -> @b:U32 -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n)) -> {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}

law u32_add_mod provedsource · line 504 · raw

@a:U32 -> @b:U32 -> {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n)) : Nat}

law word_not_nat provedsource · line 521 · raw

@n:Nat -> @w:Word(n) -> {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == pow2(n) : Nat}

The bitwise complement of w has value 2^n - 1 - w.

law word_sub_not provedsource · line 543 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @+c:Bool -> {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}

Subtraction is addition of the complement with a carry in.

law sub_arith provedsource · line 567 · raw

@+a:Nat -> @+b:Nat -> @+nb:Nat -> @+m:Nat -> @h:0x449abff091641d732d7b9f0780df40ae/nat.le(b, a) -> @hn:{1n+Nat.add(nb, b) == m : Nat} -> {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), m) : Nat}

law sub_fin provedsource · line 584 · raw

@q:Bool -> @+r:Nat -> @+d:Nat -> @+m:Nat -> @e:{Nat.add(r, scale(q, m)) == Nat.add(d, m) : Nat} -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(r, m) -> {r == d : Nat}

law word_sub_nat provedsource · line 604 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @h:0x449abff091641d732d7b9f0780df40ae/nat.le(Word.to_nat(n, b), Word.to_nat(n, a)) -> {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}

Subtraction without wrap is exact.

law u32_sub_nat provedsource · line 628 · raw

@a:U32 -> @b:U32 -> @h:0x449abff091641d732d7b9f0780df40ae/nat.le(U32.to_nat(b), U32.to_nat(a)) -> {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}

law lt_of_double_lt provedsource · line 639 · raw

@a:Nat -> @b:Nat -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(Nat.double(a), Nat.double(b)) -> 0x449abff091641d732d7b9f0780df40ae/nat.lt(a, b)

law word_inc_nat provedsource · line 657 · raw

@n:Nat -> @w:Word(n) -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(1n+Word.to_nat(n, w), pow2(n)) -> {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}

Incrementing without overflow adds one.

law u32_inc_nat provedsource · line 676 · raw

@a:U32 -> @h:0x449abff091641d732d7b9f0780df40ae/nat.lt(1n+U32.to_nat(a), pow2(32n)) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}

law u32_to_from_nat provedsource · line 686 · raw

@k:Nat -> @+h:0x449abff091641d732d7b9f0780df40ae/nat.lt(k, pow2(32n)) -> {U32.to_nat(U32.from_nat(k)) == k : Nat}

law u32_from_to_nat provedsource · line 702 · raw

@+a:U32 -> {U32.from_nat(U32.to_nat(a)) == a : U32}

law and_le_sub provedsource · line 709 · raw

@c:Bool -> @+a:Nat -> @+b:Nat -> @+l:Nat -> @-s:Nat -> @+hc:{Nat.is_le(a, l) == c : Bool} -> @hs:(@_:0x449abff091641d732d7b9f0780df40ae/nat.le(a, l) -> {s == Nat.sub(l, a) : Nat}) -> {Bool.and(c, Nat.is_le(b, s)) == Nat.is_le(Nat.add(a, b), l) : Bool}

law u32_fits_nat provedsource · line 733 · raw

@+len:U32 -> @+i:U32 -> @+n:U32 -> {Bool.and(U32.is_le(n, len), U32.is_le(i, U32.sub(len, n))) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool}

The overflow-safe bounds check n <= len and i <= len - n holds exactly when i + n <= len.

Definitions

def pow2 source · line 6 · raw

@n:Nat -> Nat

2^n, by the doubling that Word.to_nat uses.

def bit source · line 14 · raw

@x:Bool -> @t:Nat -> Nat

The value of a word whose low bit is x and whose upper bits have value t.

def b2n source · line 276 · raw

@b:Bool -> Nat

def scale source · line 284 · raw

@q:Bool -> @m:Nat -> Nat

m when q is set, else 0.

def maj source · line 292 · raw

@x:Bool -> @y:Bool -> @c:Bool -> Bool

The carry out of a full adder: set when two or three of the bits are set.

def carry source · line 304 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @c:Bool -> Bool

The carry out of Word.adc(n, a, b, False{}, c): the bit that a + b + c overflows into.