bend-kit-lemmas

Releases (2):
  0.1.1.0  0x917f5ed79ae87f89944206ae34045b4e  indexed  https://jend.leeeet.dev/files.txt?path=bend-kit-lemmas@0.1.1.0
  0.1.0.0  0xeaee3c88886bfae971db9dcf3cde0759  unindexed  https://jend.leeeet.dev/files.txt?path=bend-kit-lemmas@0.1.0.0

Definitions (45):
  Lemmas.pow2 (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=pow2)
   # 2^n, by the doubling that Word.to_nat uses.
   def pow2(n: Nat) -> Nat:
  Lemmas.bit (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=bit)
   # The value of a word whose low bit is x and whose upper bits have value t.
   def bit(x: Bool, t: Nat) -> Nat:
  Lemmas.to_nat_con (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=to_nat_con)
   law to_nat_con:
     for -p: Nat
     for x: Bool
     for -t: Word(p)
     {bit(x, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{x, t}) : Nat}
  Lemmas.cmp_bit (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=cmp_bit)
   law cmp_bit:
     for a: Nat
     for b: Nat
     for x: Bool
     for y: Bool
     {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(bit(x, a), bit(y, b)) : Cmp}
  Lemmas.word_cmp_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_cmp_nat)
   # Comparing two words compares their values.
   law word_cmp_nat:
     for n: Nat
     for a: Word(n)
     for b: Word(n)
     {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
  Lemmas.u32_cmp_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_cmp_nat)
   law u32_cmp_nat:
     for a: U32
     for b: U32
     {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
  Lemmas.u32_is_lt_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_is_lt_nat)
   law u32_is_lt_nat:
     for a: U32
     for b: U32
     {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
  Lemmas.u32_is_le_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_is_le_nat)
   law u32_is_le_nat:
     for a: U32
     for b: U32
     {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
  Lemmas.u32_is_eq_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_is_eq_nat)
   law u32_is_eq_nat:
     for a: U32
     for b: U32
     {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
  Lemmas.odd_lt_double (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=odd_lt_double)
   law odd_lt_double:
     for a: Nat
     for b: Nat
     for h: MNat.lt(a, b)
     MNat.lt(1n+Nat.double(a), Nat.double(b))
  Lemmas.word_to_nat_lt (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_to_nat_lt)
   # A word of n bits has a value below 2^n.
   law word_to_nat_lt:
     for n: Nat
     for w: Word(n)
     MNat.lt(Word.to_nat(n, w), pow2(n))
  Lemmas.u32_to_nat_word (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_to_nat_word)
   law u32_to_nat_word:
     for -x: Word(32n)
     {Word.to_nat(32n, x) == U32.to_nat(U32{x}) : Nat}
  Lemmas.u32_to_nat_lt (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_to_nat_lt)
   law u32_to_nat_lt:
     for a: U32
     MNat.lt(U32.to_nat(a), pow2(32n))
  Lemmas.double_inj (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=double_inj)
   law double_inj:
     for a: Nat
     for b: Nat
     for h: {Nat.double(a) == Nat.double(b) : Nat}
     {a == b : Nat}
  Lemmas.double_ne_odd (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=double_ne_odd)
   law double_ne_odd:
     for a: Nat
     for b: Nat
     for h: {Nat.double(a) == 1n+Nat.double(b) : Nat}
     Empty
  Lemmas.word_to_nat_inj (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_to_nat_inj)
   # Two words with the same value are the same word.
   law word_to_nat_inj:
     for n: Nat
     for a: Word(n)
     for b: Word(n)
     for h: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
     {a == b : Word(n)}
  Lemmas.u32_to_nat_inj (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_to_nat_inj)
   law u32_to_nat_inj:
     for a: U32
     for b: U32
     for h: {U32.to_nat(a) == U32.to_nat(b) : Nat}
     {a == b : U32}
  Lemmas.b2n (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=b2n)
   def b2n(b: Bool) -> Nat:
  Lemmas.scale (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=scale)
   # m when q is set, else 0.
   def scale(q: Bool, m: Nat) -> Nat:
  Lemmas.maj (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=maj)
   # The carry out of a full adder: set when two or three of the bits are set.
   def maj(x: Bool, y: Bool, c: Bool) -> Bool:
  Lemmas.carry (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=carry)
   # The carry out of Word.adc(n, a, b, False{}, c): the bit that a + b + c overflows into.
   def carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
  Lemmas.scale_double (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=scale_double)
   law scale_double:
     for q: Bool
     for -m: Nat
     {Nat.double(scale(q, m)) == scale(q, Nat.double(m)) : Nat}
  Lemmas.adc_step (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=adc_step)
   # One bit of the adder: s + 2k is the sum c + x + y of the three input bits.
   law adc_step:
     for +s: Nat
     for +x: Nat
     for +y: Nat
     for +c: Nat
     for +k: Nat
     for +r: Nat
     for +q: Bool
     for +m: Nat
     for +a: Nat
     …
  Lemmas.word_adc_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_adc_nat)
   # The adder is exact: the word sum plus the carry-out weight 2^n is c + a + b.
   law word_adc_nat:
     for n: Nat
     for a: Word(n)
     for b: Word(n)
     for 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}
  Lemmas.lt_rw (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=lt_rw)
   # Moves a strict upper bound across an equation without a conversion check.
   law lt_rw:
     for -a: Nat
     for -b: Nat
     for -c: Nat
     for e: {a == b : Nat}
     for h: MNat.lt(b, c)
     MNat.lt(a, c)
  Lemmas.add_no_carry (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=add_no_carry)
   law add_no_carry:
     for q: Bool
     for +r: Nat
     for +m: Nat
     for +s: Nat
     for e: {Nat.add(r, scale(q, m)) == s : Nat}
     for h: MNat.lt(s, m)
     {r == s : Nat}
  Lemmas.add_mod_carry (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=add_mod_carry)
   law add_mod_carry:
     for q: Bool
     for +r: Nat
     for +m: Nat
     for +s: Nat
     for e: {Nat.add(r, scale(q, m)) == s : Nat}
     for h: MNat.lt(r, m)
     {r == Nat.mod(s, m) : Nat}
  Lemmas.word_add_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_add_nat)
   # Addition without overflow is exact.
   law word_add_nat:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     for h: MNat.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}
  Lemmas.word_add_mod (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_add_mod)
   # Addition wraps modulo 2^n.
   law word_add_mod:
     for +n: Nat
     for +a: Word(n)
     for +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}
  Lemmas.u32_add_word (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_add_word)
   law u32_add_word:
     for -x: Word(32n)
     for -y: Word(32n)
     {Word.to_nat(32n, Word.add(32n, x, y)) == U32.to_nat(U32.add(U32{x}, U32{y})) : Nat}
  Lemmas.u32_add_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_add_nat)
   law u32_add_nat:
     for a: U32
     for b: U32
     for h: MNat.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}
  Lemmas.u32_add_mod (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_add_mod)
   law u32_add_mod:
     for a: U32
     for b: U32
     {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n)) : Nat}
  Lemmas.word_not_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_not_nat)
   # The bitwise complement of w has value 2^n - 1 - w.
   law word_not_nat:
     for n: Nat
     for w: Word(n)
     {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == pow2(n) : Nat}
  Lemmas.word_sub_not (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_sub_not)
   # Subtraction is addition of the complement with a carry in.
   law word_sub_not:
     for n: Nat
     for a: Word(n)
     for b: Word(n)
     for +c: Bool
     {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}
  Lemmas.sub_arith (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=sub_arith)
   law sub_arith:
     for +a: Nat
     for +b: Nat
     for +nb: Nat
     for +m: Nat
     for h: MNat.le(b, a)
     for hn: {1n+Nat.add(nb, b) == m : Nat}
     {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), m) : Nat}
  Lemmas.sub_fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=sub_fin)
   law sub_fin:
     for q: Bool
     for +r: Nat
     for +d: Nat
     for +m: Nat
     for e: {Nat.add(r, scale(q, m)) == Nat.add(d, m) : Nat}
     for h: MNat.lt(r, m)
     {r == d : Nat}
  Lemmas.word_sub_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_sub_nat)
   # Subtraction without wrap is exact.
   law word_sub_nat:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     for h: MNat.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}
  Lemmas.u32_sub_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_sub_nat)
   law u32_sub_nat:
     for a: U32
     for b: U32
     for h: MNat.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}
  Lemmas.lt_of_double_lt (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=lt_of_double_lt)
   law lt_of_double_lt:
     for a: Nat
     for b: Nat
     for h: MNat.lt(Nat.double(a), Nat.double(b))
     MNat.lt(a, b)
  Lemmas.word_inc_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=word_inc_nat)
   # Incrementing without overflow adds one.
   law word_inc_nat:
     for n: Nat
     for w: Word(n)
     for h: MNat.lt(1n+Word.to_nat(n, w), pow2(n))
     {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}
  Lemmas.u32_inc_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_inc_nat)
   law u32_inc_nat:
     for a: U32
     for h: MNat.lt(1n+U32.to_nat(a), pow2(32n))
     {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}
  Lemmas.u32_to_from_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_to_from_nat)
   law u32_to_from_nat:
     for k: Nat
     for +h: MNat.lt(k, pow2(32n))
     {U32.to_nat(U32.from_nat(k)) == k : Nat}
  Lemmas.u32_from_to_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_from_to_nat)
   law u32_from_to_nat:
     for +a: U32
     {U32.from_nat(U32.to_nat(a)) == a : U32}
  Lemmas.and_le_sub (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=and_le_sub)
   law and_le_sub:
     for c: Bool
     for +a: Nat
     for +b: Nat
     for +l: Nat
     for -s: Nat
     for +hc: {Nat.is_le(a, l) == c : Bool}
     for hs: MNat.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}
  Lemmas.u32_fits_nat (https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_fits_nat)
   # The overflow-safe bounds check n <= len and i <= len - n holds exactly when i + n <= len.
   law u32_fits_nat:
     for +len: U32
     for +i: U32
     for +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}