bend-osdev-word64

Releases (2):
  0.1.1.0  0xea9c6e6209a3ac3fb21596f70f09f650  indexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-word64@0.1.1.0
  0.1.0.0  0x44cf1401f78136bfc15c4c5be1cd20f0  unindexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-word64@0.1.0.0

Definitions (425, 1 to 100 shown):
  LAWS.add_wraps (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=add_wraps)
   law add_wraps:
     {W.W64.add(W.W64.max(), W.W64.one()) == W.W64.zero() : W.W64}
  LAWS.sub_wraps (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=sub_wraps)
   law sub_wraps:
     {W.W64.sub(W.W64.zero(), W.W64.one()) == W.W64.max() : W.W64}
  LAWS.hi_of_parts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=hi_of_parts)
   law hi_of_parts:
     {W.W64.hi(W.W64.from_parts(3735928559, 3405691582)) == 3735928559 : U32}
  LAWS.lo_of_parts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=lo_of_parts)
   law lo_of_parts:
     {W.W64.lo(W.W64.from_parts(3735928559, 3405691582)) == 3405691582 : U32}
  LAWS.shl_crosses_halves (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=shl_crosses_halves)
   law shl_crosses_halves:
     {W.W64.shl(W.W64.one(), 32n) == W.W64.from_parts(1, 0) : W.W64}
  LAWS.shr_crosses_halves (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=shr_crosses_halves)
   law shr_crosses_halves:
     {W.W64.shr(W.W64.from_parts(1, 0), 1n) == W.W64.from_parts(0, 2147483648) : W.W64}
  LAWS.mul_of_max_halves (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=mul_of_max_halves)
   # (2^32 - 1)^2 = 2^64 - 2^33 + 1
   law mul_of_max_halves:
     {W.W64.mul(W.W64.from_u32(4294967295), W.W64.from_u32(4294967295)) == W.W64.from_parts(4294967294, 1) : W.W64}
  LAWS.show_max (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=show_max)
   law show_max:
     {W.W64.show(W.W64.max()) == "18446744073709551615" : String}
  LAWS.show_hex_parts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=show_hex_parts)
   law show_hex_parts:
     {W.W64.show_hex(W.W64.from_parts(3735928559, 3405691582)) == "deadbeefcafebabe" : String}
  LAWS.show_hex_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=show_hex_zero)
   law show_hex_zero:
     {W.W64.show_hex(W.W64.zero()) == "0000000000000000" : String}
  LAWS.lo_from_u32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=lo_from_u32)
   # For every 32-bit a: from_u32 then lo gives a back.
   law lo_from_u32:
     for a: U32
     {W.W64.lo(W.W64.from_u32(a)) == a : U32}
  LAWS.hi_from_parts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=hi_from_parts)
   # For every pair of halves: splitting the joined word gives them back.
   law hi_from_parts:
     for h: U32
     for l: U32
     {W.W64.hi(W.W64.from_parts(h, l)) == h : U32}
  LAWS.lo_from_parts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=lo_from_parts)
   law lo_from_parts:
     for h: U32
     for l: U32
     {W.W64.lo(W.W64.from_parts(h, l)) == l : U32}
  LAWS.from_parts_zero_hi (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=from_parts_zero_hi)
   # Interface laws: a word whose high half is 0 is the word of its low half,
   # and the word of halves 0 and 0 is zero.
   law from_parts_zero_hi:
     for a: U32
     {W.W64.from_parts(0, a) == W.W64.from_u32(a) : W.W64}
  LAWS.from_parts_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=from_parts_zero)
   law from_parts_zero:
     {W.W64.from_parts(0, 0) == W.W64.zero() : W.W64}
  LAWS.parts_of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=parts_of)
   # Interface law: a word is its two halves joined (for every word). Other
   # packages' proofs use this instead of looking inside W64.
   law parts_of:
     for v: W.W64
     {W.W64.from_parts(W.W64.hi(v), W.W64.lo(v)) == v : W.W64}
  LAWS.to_nat_parts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=to_nat_parts)
   # The value of a word (for every word): lo + hi * 2^32, the weight 2^32 being
   # 32 doublings (U32Nat.dbl, from bend-osdev-u32).
   law to_nat_parts:
     for +h: U32
     for +l: U32
     {W.W64.to_nat(W.W64.from_parts(h, l)) == Nat.add(U32.to_nat(l), U.U32Nat.dbl(32n, U32.to_nat(h))) : Nat}
  LAWS.value_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=value_eq)
   # Two words with the same value are the same word.
   law value_eq:
     for +a: W.W64
     for +b: W.W64
     for e: {W.W64.to_nat(a) == W.W64.to_nat(b) : Nat}
     {a == b : W.W64}
  LAWS.cmp_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=cmp_value)
   # Comparison is the order of the values (for every pair of words).
   law cmp_value:
     for +a: W.W64
     for +b: W.W64
     {W.W64.cmp(a, b) == Nat.cmp(W.W64.to_nat(a), W.W64.to_nat(b)) : Cmp}
  LAWS.lt_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=lt_value)
   law lt_value:
     for +a: W.W64
     for +b: W.W64
     {W.W64.is_lt(a, b) == Nat.is_lt(W.W64.to_nat(a), W.W64.to_nat(b)) : Bool}
  LAWS.le_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=le_value)
   law le_value:
     for +a: W.W64
     for +b: W.W64
     {W.W64.is_le(a, b) == Nat.is_le(W.W64.to_nat(a), W.W64.to_nat(b)) : Bool}
  LAWS.eq_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=eq_value)
   law eq_value:
     for +a: W.W64
     for +b: W.W64
     {W.W64.is_eq(a, b) == Nat.is_eq(W.W64.to_nat(a), W.W64.to_nat(b)) : Bool}
  LAWS.cmp_hi_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=cmp_hi_lt)
   # Comparison is by the high halves, then the low halves (for dependents
   # that order words through W64.hi and W64.lo).
   law cmp_hi_lt:
     for +a: W.W64
     for +b: W.W64
     for h: {U32.cmp(W.W64.hi(a), W.W64.hi(b)) == LT{} : Cmp}
     {W.W64.cmp(a, b) == LT{} : Cmp}
  LAWS.cmp_hi_gt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=cmp_hi_gt)
   law cmp_hi_gt:
     for +a: W.W64
     for +b: W.W64
     for h: {U32.cmp(W.W64.hi(a), W.W64.hi(b)) == GT{} : Cmp}
     {W.W64.cmp(a, b) == GT{} : Cmp}
  LAWS.cmp_hi_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=cmp_hi_eq)
   law cmp_hi_eq:
     for +a: W.W64
     for +b: W.W64
     for h: {U32.cmp(W.W64.hi(a), W.W64.hi(b)) == EQ{} : Cmp}
     {W.W64.cmp(a, b) == U32.cmp(W.W64.lo(a), W.W64.lo(b)) : Cmp}
  LAWS.add_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=add_wrap)
   # Addition, for every pair of words: the sum of the values, less 2^64 when
   # it wraps, which is exactly when the result is below the first operand;
   # and with the sum no more than a word's value, it does not wrap.
   law add_wrap:
     for +a: W.W64
     for +b: W.W64
     {Nat.add(W.W64.to_nat(W.W64.add(a, b)), U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(W.W64.add(a, b), a)))) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
  LAWS.add_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=add_value)
   law add_value:
     for +a: W.W64
     for +b: W.W64
     for +c: W.W64
     for h: {Nat.is_le(Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)), W.W64.to_nat(c)) == True{} : Bool}
     {W.W64.to_nat(W.W64.add(a, b)) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
  LAWS.sub_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=sub_wrap)
   # Subtraction, for every pair of words: the difference plus the subtrahend
   # is the minuend, plus 2^64 when the subtrahend is the larger; when it is
   # not, the difference is the Nat difference.
   law sub_wrap:
     for +a: W.W64
     for +b: W.W64
     {Nat.add(W.W64.to_nat(W.W64.sub(a, b)), W.W64.to_nat(b)) == Nat.add(W.W64.to_nat(a), U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(a, b)))) : Nat}
  LAWS.sub_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=sub_value)
   law sub_value:
     for +a: W.W64
     for +b: W.W64
     for h: {Nat.is_le(W.W64.to_nat(b), W.W64.to_nat(a)) == True{} : Bool}
     {W.W64.to_nat(W.W64.sub(a, b)) == Nat.sub(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
  LAWS.shl_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=shl_value)
   # Shifts, as Nat facts. A shift left by k < 64 multiplies the value by 2^k
   # when the result is no more than a word's value; a shift right by k < 64
   # is the floor of the value divided by 2^k (2^k times it is at most the
   # value, and 2^k times one more is above it); by 64 or more, both give 0.
   law shl_value:
     for +a: W.W64
     for +k: Nat
     for +c: W.W64
     for hk: {Nat.is_lt(k, 64n) == True{} : Bool}
     for +h: {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(a)), W.W64.to_nat(c)) == True{} : Bool}
     {W.W64.to_nat(W.W64.shl(a, k)) == U.U32Nat.dbl(k, W.W64.to_nat(a)) : Nat}
  LAWS.shr_value_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=shr_value_le)
   law shr_value_le:
     for +a: W.W64
     for +k: Nat
     for hk: {Nat.is_lt(k, 64n) == True{} : Bool}
     {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64.shr(a, k))), W.W64.to_nat(a)) == True{} : Bool}
  LAWS.shr_value_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=shr_value_lt)
   law shr_value_lt:
     for +a: W.W64
     for +k: Nat
     for hk: {Nat.is_lt(k, 64n) == True{} : Bool}
     {Nat.is_lt(W.W64.to_nat(a), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64.shr(a, k)))) == True{} : Bool}
  LAWS.shl_big (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=shl_big)
   law shl_big:
     for +a: W.W64
     for +k: Nat
     for +h: {Nat.is_le(64n, k) == True{} : Bool}
     {W.W64.shl(a, k) == W.W64.zero() : W.W64}
  LAWS.shr_big (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&name=shr_big)
   law shr_big:
     for +a: W.W64
     for +k: Nat
     for +h: {Nat.is_le(64n, k) == True{} : Bool}
     {W.W64.shr(a, k) == W.W64.zero() : W.W64}
  LAWSBits.and_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_bits.bend&name=and_comm)
   # The bits: and, or and xor commute; and + or is the sum of the values, and
   # so is xor + 2 and; with no bit in common (and is 0), or is the sum; not is
   # the subtraction from 2^64 - 1.
   law and_comm:
     for +a: W.W64
     for +b: W.W64
     {W.W64.and(a, b) == W.W64.and(b, a) : W.W64}
  LAWSBits.or_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_bits.bend&name=or_comm)
   law or_comm:
     for +a: W.W64
     for +b: W.W64
     {W.W64.or(a, b) == W.W64.or(b, a) : W.W64}
  LAWSBits.xor_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_bits.bend&name=xor_comm)
   law xor_comm:
     for +a: W.W64
     for +b: W.W64
     {W.W64.xor(a, b) == W.W64.xor(b, a) : W.W64}
  LAWSBits.and_or (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_bits.bend&name=and_or)
   law and_or:
     for +a: W.W64
     for +b: W.W64
     {Nat.add(W.W64.to_nat(W.W64.and(a, b)), W.W64.to_nat(W.W64.or(a, b))) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
  LAWSBits.xor_and (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_bits.bend&name=xor_and)
   law xor_and:
     for +a: W.W64
     for +b: W.W64
     {Nat.add(W.W64.to_nat(W.W64.xor(a, b)), Nat.double(W.W64.to_nat(W.W64.and(a, b)))) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
  LAWSBits.or_disjoint (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_bits.bend&name=or_disjoint)
   law or_disjoint:
     for +a: W.W64
     for +b: W.W64
     for h: {W.W64.and(a, b) == W.W64.zero() : W.W64}
     {W.W64.to_nat(W.W64.or(a, b)) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
  LAWSBits.not_sub (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_bits.bend&name=not_sub)
   law not_sub:
     for +a: W.W64
     {W.W64.not(a) == W.W64.sub(W.W64.max(), a) : W.W64}
  LAWSBits.shl_one_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_bits.bend&name=shl_one_wrap)
   # A shift left by one bit: twice the value, less 2^64 for the top bit (bit
   # 31 of the high half) going out.
   law shl_one_wrap:
     for +a: W.W64
     {Nat.add(W.W64.to_nat(W.W64.shl(a, 1n)), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(W.W64.hi(a), 31n)))) == Nat.double(W.W64.to_nat(a)) : Nat}
  LAWSDiv.divmod_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_div.bend&name=divmod_value)
   # Division (shift and subtract, 64 steps): for b not 0, the quotient and the
   # remainder are the Nat ones, a = q b + r with r < b; by 0, the quotient is 0
   # and the remainder a.
   law divmod_value:
     for +a: W.W64
     for +b: W.W64
     for h: {W.W64.is_zero(b) == False{} : Bool}
     {Nat.add(Nat.mul(W.W64.to_nat(W.W64.div(a, b)), W.W64.to_nat(b)), W.W64.to_nat(W.W64.mod(a, b))) == W.W64.to_nat(a) : Nat}
  LAWSDiv.mod_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_div.bend&name=mod_lt)
   law mod_lt:
     for +a: W.W64
     for +b: W.W64
     for h: {W.W64.is_zero(b) == False{} : Bool}
     {Nat.is_lt(W.W64.to_nat(W.W64.mod(a, b)), W.W64.to_nat(b)) == True{} : Bool}
  LAWSDiv.div_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_div.bend&name=div_zero)
   law div_zero:
     for +a: W.W64
     {W.W64.div(a, W.W64.zero()) == W.W64.zero() : W.W64}
  LAWSDiv.mod_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_div.bend&name=mod_zero)
   law mod_zero:
     for +a: W.W64
     {W.W64.mod(a, W.W64.zero()) == a : W.W64}
  LAWSMul.mulhi_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_mul.bend&name=mulhi_value)
   # Multiplication. W64.mulhi(a, b) is the high 32 bits of the product of two
   # 32-bit words: with the low 32 bits (U32.mul), the whole product. W64.mul
   # is the product modulo 2^64: its value is the low 64 bits of the product of
   # the values (U32Nat.low, from bend-osdev-u32), what wraps is 2^64 times the
   # rest, and with the product no more than a word's value nothing wraps.
   law mulhi_value:
     for +a: U32
     for +b: U32
     {Nat.add(U32.to_nat(U32.mul(a, b)), U.U32Nat.dbl(32n, U32.to_nat(W.W64.mulhi(a, b)))) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWSMul.mul_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_mul.bend&name=mul_wrap)
   law mul_wrap:
     for +a: W.W64
     for +b: W.W64
     {Nat.add(W.W64.to_nat(W.W64.mul(a, b)), U.U32Nat.dbl(64n, U.U32Nat.high(64n, Nat.mul(W.W64.to_nat(a), W.W64.to_nat(b))))) == Nat.mul(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
  LAWSMul.mul_low (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_mul.bend&name=mul_low)
   law mul_low:
     for +a: W.W64
     for +b: W.W64
     {W.W64.to_nat(W.W64.mul(a, b)) == U.U32Nat.low(64n, Nat.mul(W.W64.to_nat(a), W.W64.to_nat(b))) : Nat}
  LAWSMul.mul_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_mul.bend&name=mul_value)
   law mul_value:
     for +a: W.W64
     for +b: W.W64
     for +c: W.W64
     for h: {Nat.is_le(Nat.mul(W.W64.to_nat(a), W.W64.to_nat(b)), W.W64.to_nat(c)) == True{} : Bool}
     {W.W64.to_nat(W.W64.mul(a, b)) == Nat.mul(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
  LAWSText.show_reads (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/LAWS_text.bend&name=show_reads)
   # Decimal text: the digits of W64.show(a), read back one by one (Base's
   # Nat.read.go, the reader without Nat.read's 2^48 gate), are the value.
   law show_reads:
     for +a: W.W64
     {Nat.read.go(W.W64.show(a), 0n) == Some{W.W64.to_nat(a)} : Maybe<&2, Nat>}
  PROOF.wp.pick_lex (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wp.pick_lex)
   def wp.pick_lex(c: Cmp, -al: U32, -bl: U32) -> {W.W64.cmp.pick(c, al, bl) == P.wv.lex(c, U32.cmp(al, bl)) : Cmp}:
  PROOF.wp.of_halves (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wp.of_halves)
   def wp.of_halves(p: Word(32n) & Word(32n)) -> W.W64:
  PROOF.wp.add_split.fin (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wp.add_split.fin)
   def wp.add_split.fin(-ahw: Word(32n), -alw: Word(32n), -bhw: Word(32n), -blw: Word(32n), cb: Bool) -> {W.W64{U32.add(U32{Word.add(32n, ahw, bhw)}, W.W64.bit(cb)), U32{Word.add(32n, alw, blw)}} == W.W64{U32{Word.add(32n, Word.add(32n, ahw, bhw), P.wv.bitw(32n, cb))}, U32{Word.add(32n, alw, blw)}} : W.W64}:
  PROOF.wp.add_split.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wp.add_split.go)
   def wp.add_split.go(+ahw: Word(32n), +alw: Word(32n), +bhw: Word(32n), +blw: Word(32n), cb: Bool, e: {Cmp.is_lt(Word.cmp(32n, Word.add(32n, alw, blw), alw)) == cb : Bool}) -> {W.W64.add(W.W64{U32{ahw}, U32{alw}}, W.W64{U32{bhw}, U32{blw}}) == W.W64{U32{P.wv.addhi(32n, ahw, alw, bhw, blw)}, U32{Word.add(32n, alw, blw)}} : W.W64}:
  PROOF.wp.add_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wp.add_split)
   def wp.add_split(+ahw: Word(32n), +alw: Word(32n), +bhw: Word(32n), +blw: Word(32n)) -> {W.W64.add(W.W64{U32{ahw}, U32{alw}}, W.W64{U32{bhw}, U32{blw}}) == W.W64{U32{P.wv.addhi(32n, ahw, alw, bhw, blw)}, U32{Word.add(32n, alw, blw)}} : W.W64}:
  PROOF.wp.sub_split.fin (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wp.sub_split.fin)
   def wp.sub_split.fin(-ahw: Word(32n), -alw: Word(32n), -bhw: Word(32n), -blw: Word(32n), cb: Bool) -> {W.W64{U32.sub(U32{Word.sub(32n, ahw, bhw)}, W.W64.bit(cb)), U32{Word.sub(32n, alw, blw)}} == W.W64{U32{Word.sub(32n, Word.sub(32n, ahw, bhw), P.wv.bitw(32n, cb))}, U32{Word.sub(32n, alw, blw)}} : W.W64}:
  PROOF.wp.sub_split.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wp.sub_split.go)
   def wp.sub_split.go(+ahw: Word(32n), +alw: Word(32n), +bhw: Word(32n), +blw: Word(32n), cb: Bool, e: {Cmp.is_lt(Word.cmp(32n, alw, blw)) == cb : Bool}) -> {W.W64.sub(W.W64{U32{ahw}, U32{alw}}, W.W64{U32{bhw}, U32{blw}}) == W.W64{U32{P.wv.subhi(32n, ahw, alw, bhw, blw)}, U32{Word.sub(32n, alw, blw)}} : W.W64}:
  PROOF.wp.sub_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wp.sub_split)
   def wp.sub_split(+ahw: Word(32n), +alw: Word(32n), +bhw: Word(32n), +blw: Word(32n)) -> {W.W64.sub(W.W64{U32{ahw}, U32{alw}}, W.W64{U32{bhw}, U32{blw}}) == W.W64{U32{P.wv.subhi(32n, ahw, alw, bhw, blw)}, U32{Word.sub(32n, alw, blw)}} : W.W64}:
  PROOF.wq.shln (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shln)
   def wq.shln(+w: Word(32n), k: Nat) -> {U32.shln(U32{w}, k) == U32{PS.ws.shl(32n, k, w)} : U32}:
  PROOF.wq.shrn (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shrn)
   def wq.shrn(+w: Word(32n), k: Nat) -> {U32.shrn(U32{w}, k) == U32{PS.ws.shr(32n, k, w)} : U32}:
  PROOF.wq.shl.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shl.go)
   def wq.shl.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: Word(32n), +chw: Word(32n), +clw: Word(32n), ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, hk: {Nat.is_lt(k, 64n) == True{} : Bool}, +h: {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{chw}, U32{clw}})) == True{} : Bool}) -> {W.W64.to_nat(W.W64.shl.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}})) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}:
  PROOF.wq.shr_le.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shr_le.go)
   def wq.shr_le.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: Word(32n), ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64.shr.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}}))), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}:
  PROOF.wq.shr_lt.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shr_lt.go)
   def wq.shr_lt.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: Word(32n), ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64.shr.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}})))) == True{} : Bool}:
  PROOF.wq.shlbig.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shlbig.go)
   def wq.shlbig.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, -a: W.W64, ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, +h: {Nat.is_le(64n, k) == True{} : Bool}) -> {W.W64.shl.pick(z, l32, l64, k, a) == W.W64.zero() : W.W64}:
  PROOF.wq.shrbig.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shrbig.go)
   def wq.shrbig.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, -a: W.W64, ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, +h: {Nat.is_le(64n, k) == True{} : Bool}) -> {W.W64.shr.pick(z, l32, l64, k, a) == W.W64.zero() : W.W64}:
  PROOFBits.wu.ve (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wu.ve)
   def wu.ve(+w: Word(32n)) -> {Word.to_nat(32n, w) == U32.to_nat(U32{w}) : Nat}:
  PROOFBits.wu.lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wu.lt)
   def wu.lt(+x: U32) -> {Nat.is_lt(U32.to_nat(x), U.U32Nat.dbl(32n, 1n)) == True{} : Bool}:
  PROOFBits.wv.g (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wv.g)
   def wv.g(+n: Nat, +m: Nat, +h: Word(n), +l: Word(n), e: {Nat.add(n, n) == m : Nat}) -> {Nat.is_lt(P.wv.V(n, h, l), U.U32Nat.dbl(m, 1n)) == True{} : Bool}:
  PROOFBits.wv.ve (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wv.ve)
   def wv.ve(+h: Word(32n), +l: Word(32n)) -> {P.wv.V(32n, h, l) == W.W64.to_nat(W.W64{U32{h}, U32{l}}) : Nat}:
  PROOFBits.wv.lt64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wv.lt64)
   def wv.lt64(+x: W.W64) -> {Nat.is_lt(W.W64.to_nat(x), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}:
  PROOFBits.wn.sub0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wn.sub0)
   def wn.sub0(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}:
  PROOFBits.wn.le0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wn.le0)
   def wn.le0(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
  PROOFBits.wn.ft (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wn.ft)
   def wn.ft(e: {False{} == True{} : Bool}) -> Empty:
  PROOFBits.wn.tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wn.tf)
   def wn.tf(e: {True{} == False{} : Bool}) -> Empty:
  PROOFBits.wn.ge_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wn.ge_lt)
   def wn.ge_lt(c: Cmp) -> {Cmp.is_ge(c) == Bool.not(Cmp.is_lt(c)) : Bool}:
  PROOFBits.wm.fn (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wm.fn)
   def wm.fn(+h: Nat, +n: Nat, +x: Nat, +en: {Nat.add(h, h) == n : Nat}) -> {U.U32Nat.dbl(n, x) == U.U32Nat.dbl(h, U.U32Nat.dbl(h, x)) : Nat}:
  PROOFBits.wr.b0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wr.b0)
   def wr.b0(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x2, U.U32Nat.dbl(32n, x3))) == Nat.add(Nat.add(x0, x2), U.U32Nat.dbl(32n, Nat.add(x1, x3))) : Nat}:
  PROOFBits.wr.b1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wr.b1)
   def wr.b1(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, x1), U.U32Nat.dbl(32n, Nat.add(x2, x3))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(x1, U.U32Nat.dbl(32n, x3))) : Nat}:
  PROOFBits.wr.b2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wr.b2)
   def wr.b2(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.double(Nat.add(x2, U.U32Nat.dbl(32n, x3)))) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}:
  PROOFBits.wb.lts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wb.lts)
   def wb.lts(x: Nat, y: Nat) -> {Nat.is_lt(x, 1n+y) == Nat.is_le(x, y) : Bool}:
  PROOFBits.wb.mlt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wb.mlt)
   # nothing is above the mask of all n bits
   def wb.mlt(+n: Nat, +w: Word(n)) -> {Cmp.is_lt(Word.cmp(n, U.U32Word.mask(n, n), w)) == False{} : Bool}:
  PROOFBits.wb.maxlt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wb.maxlt)
   def wb.maxlt(+x: U32) -> {U32.is_lt(4294967295, x) == False{} : Bool}:
  PROOFBits.wb.sub0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wb.sub0)
   def wb.sub0(+x: U32) -> {U32.sub(x, 0) == x : U32}:
  PROOFBits.wr.b3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wr.b3)
   def wr.b3(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, Nat.add(x1, x2))), U.U32Nat.dbl(64n, x3)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}:
  PROOFBits.wr.b4 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wr.b4)
   def wr.b4(+x0: Nat, +x1: Nat) -> {Nat.add(Nat.double(x0), U.U32Nat.dbl(32n, Nat.double(x1))) == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}:
  PROOFBits.wr.b5 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wr.b5)
   def wr.b5(+x0: Nat, +x1: Nat, +x2: Nat) -> {Nat.add(Nat.add(x0, x1), U.U32Nat.dbl(32n, Nat.add(x2, 0n))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), x1) : Nat}:
  PROOFBits.wb.or_bit (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wb.or_bit)
   def wb.or_bit(+x: W.W64, +c: U32, +hc: {Nat.is_lt(U32.to_nat(c), U.U32Nat.dbl(1n, 1n)) == True{} : Bool}) -> {W.W64.to_nat(W.W64.or(W.W64.shl(x, 1n), W.W64.from_u32(c))) == Nat.add(W.W64.to_nat(W.W64.shl(x, 1n)), U32.to_nat(c)) : Nat}:
  PROOFDiv.wu.ve (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wu.ve)
   def wu.ve(+w: Word(32n)) -> {Word.to_nat(32n, w) == U32.to_nat(U32{w}) : Nat}:
  PROOFDiv.wu.lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wu.lt)
   def wu.lt(+x: U32) -> {Nat.is_lt(U32.to_nat(x), U.U32Nat.dbl(32n, 1n)) == True{} : Bool}:
  PROOFDiv.wv.g (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wv.g)
   def wv.g(+n: Nat, +m: Nat, +h: Word(n), +l: Word(n), e: {Nat.add(n, n) == m : Nat}) -> {Nat.is_lt(P.wv.V(n, h, l), U.U32Nat.dbl(m, 1n)) == True{} : Bool}:
  PROOFDiv.wv.ve (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wv.ve)
   def wv.ve(+h: Word(32n), +l: Word(32n)) -> {P.wv.V(32n, h, l) == W.W64.to_nat(W.W64{U32{h}, U32{l}}) : Nat}:
  PROOFDiv.wv.lt64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wv.lt64)
   def wv.lt64(+x: W.W64) -> {Nat.is_lt(W.W64.to_nat(x), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}:
  PROOFDiv.wn.sub0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wn.sub0)
   def wn.sub0(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}:
  PROOFDiv.wn.le0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wn.le0)
   def wn.le0(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
  PROOFDiv.wn.ft (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wn.ft)
   def wn.ft(e: {False{} == True{} : Bool}) -> Empty:
  PROOFDiv.wn.tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wn.tf)
   def wn.tf(e: {True{} == False{} : Bool}) -> Empty:
  PROOFDiv.wn.ge_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wn.ge_lt)
   def wn.ge_lt(c: Cmp) -> {Cmp.is_ge(c) == Bool.not(Cmp.is_lt(c)) : Bool}:
  PROOFDiv.wm.fn (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wm.fn)
   def wm.fn(+h: Nat, +n: Nat, +x: Nat, +en: {Nat.add(h, h) == n : Nat}) -> {U.U32Nat.dbl(n, x) == U.U32Nat.dbl(h, U.U32Nat.dbl(h, x)) : Nat}:
  PROOFDiv.wd.lt2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wd.lt2)
   def wd.lt2(x: Nat, h: {Nat.is_lt(x, U.U32Nat.dbl(1n, 1n)) == True{} : Bool}) -> {Nat.is_le(x, 1n) == True{} : Bool}:
More: https://jend.leeeet.dev/packages/bend-osdev-word64.txt?definitions_offset=100