proofs/math/u64/u64.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as U64
15 imports
import Base import ../../../spec/math/u64.bend as SU import ../../../src/math/u64.bend as U import ../../lib/lemmas/src/wide.bend as W import ../../lib/lemmas/spec/numeric.bend as S import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/u32.bend as U3 import ../../lib/u32alg.bend as A import ../../lib/lemmas/proofs/numeric.bend as NUM import ../../lib/lemmas/proofs/addition.bend as AD import ../../lib/lemmas/proofs/modular_addition.bend as MA import ../../lib/lemmas/proofs/word_addition.bend as WA import ../../lib/word.bend as WD import ../../lib/u32div.bend as UD
Definitions
def bits source · line 20 · raw
@a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Word(64n)
def order_eq source · line 25 · raw
@+c:Cmp -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.order(c, EQ{}) == c : Cmp}
def fin_order source · line 34 · raw
@+x:Bool -> @+y:Bool -> @+c:Cmp -> @+d:Cmp -> {Word.cmp.fin(x, y, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.order(c, d)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.order(c, Word.cmp.fin(x, y, d)) : Cmp}
def cmp_join source · line 44 · raw
@+n:Nat -> @+m:Nat -> @+a1:Word(n) -> @+b1:Word(m) -> @+a2:Word(n) -> @+b2:Word(m) -> {Word.cmp(Nat.add(n, m), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.join(n, m, a1, b1), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.join(n, m, a2, b2)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.order(Word.cmp(m, b1, b2), Word.cmp(n, a1, a2)) : Cmp}Comparing two joined words is comparing the high parts, then the low parts.
def u32_cmp source · line 52 · raw
@+x:Word(32n) -> @+y:Word(32n) -> {U32.cmp(U32{x}, U32{y}) == Word.cmp(32n, x, y) : Cmp}
def cmp_pack source · line 55 · raw
@+alo:U32 -> @+ahi:U32 -> @+blo:U32 -> @+bhi:U32 -> {Word.cmp(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.pack(alo, ahi), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.pack(blo, bhi)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.order(U32.cmp(ahi, bhi), U32.cmp(alo, blo)) : Cmp}
def ge_fin_zero source · line 60 · raw
@+c:Cmp -> @+x:Bool -> @+h:{Cmp.is_ge(c) == True{} : Bool} -> {Cmp.is_ge(Word.cmp.fin(x, False{}, c)) == True{} : Bool}
def ge_zero source · line 72 · raw
@+n:Nat -> @+w:Word(n) -> {Cmp.is_ge(Word.cmp(n, w, Word.zero(n))) == True{} : Bool}Nothing compares below zero.
def ge_order source · line 79 · raw
@+c:Cmp -> @+d:Cmp -> @+h:{Cmp.is_ge(d) == True{} : Bool} -> {Cmp.is_ge(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.order(c, d)) == Cmp.is_ge(c) : Bool}
def threshold source · line 88 · raw
{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.sign_threshold(63n) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.join(32n, 32n, Word.zero(32n), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.sign_threshold(31n)) : Word(64n)}
def threshold_u32 source · line 91 · raw
{2147483648 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.sign_threshold(31n)} : U32}
def negative_pack source · line 95 · raw
@+lo:U32 -> @+hi:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.negative(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.pack(lo, hi)) == U32.is_ge(hi, 2147483648) : Bool}The sign of the 64-bit word is the top bit of the high limb.
def le_sign_spec source · line 103 · raw
@+alo:U32 -> @+ahi:U32 -> @+blo:U32 -> @+bhi:U32 -> @+na:Bool -> @+nb:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.le_sign(alo, ahi, blo, bhi, na, nb) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.order(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.pack(alo, ahi), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.pack(blo, bhi), na, nb) : Bool}
def le_signed source · line 117 · raw
@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.le_signed(a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.order(bits(a), bits(b), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.negative(bits(a)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.negative(bits(b))) : Bool}THEOREM: le_signed is the specification's signed 64-bit order.
def eq_order source · line 126 · raw
@+c:Cmp -> @+d:Cmp -> {Cmp.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.order(c, d)) == Bool.and(Cmp.is_eq(d), Cmp.is_eq(c)) : Bool}
def zero_pack source · line 147 · raw
{Word.zero(64n) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.pack(0, 0) : Word(64n)}
def is_zero source · line 151 · raw
@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.is_zero(a) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.zero(bits(a)) : Bool}THEOREM: is_zero is the specification's zero test.
def val source · line 160 · raw
@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat
def val_pack source · line 163 · raw
@+lo:U32 -> @+hi:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.pack(lo, hi)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32div.v(lo), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32div.v(hi))) : Nat}
def carry32 source · line 166 · raw
@+x:U32 -> @+y:U32 -> Bool
def add_cons source · line 171 · raw
@+x:U32 -> @+y:U32 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32div.v(U32.add(x, y)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(carry32(x, y)))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32div.v(x), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32div.v(y)) : Nat}
def add_lt1 source · line 179 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> {U32.is_lt(U32.add(x, y), x) == carry32(x, y) : Bool}
def add_lt source · line 184 · raw
@+x:U32 -> @+y:U32 -> {U32.is_lt(U32.add(x, y), x) == carry32(x, y) : Bool}the low-limb wrap test is the low-limb carry
def carry_v source · line 187 · raw
@+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32div.v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.carry(c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(c) : Nat}
def add_hi source · line 194 · raw
@ahi:U32 -> @bhi:U32 -> @c:Bool -> U32
def add_over source · line 197 · raw
@a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat
def add_value source · line 203 · raw
@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.add(val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.add(a, b)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(64n, add_over(a, b))) == Nat.add(val(a), val(b)) : Nat}the sum loses exactly 2^64 times the high carries
def add source · line 223 · raw
@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {bits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.add(a, b)) == Word.add(64n, bits(a), bits(b)) : Word(64n)}THEOREM: add is 64-bit wrapping addition.
def inc_zero32 source · line 232 · raw
@+x:Word(32n) -> {U32.is_zero(U32{Word.inc(32n, x)}) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.ones(32n, x) : Bool}
def add_carry source · line 235 · raw
@+xw:Word(32n) -> @+c:Bool -> {U32.add(U32{xw}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.carry(c)) == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.incif(32n, c, xw)} : U32}
def neg source · line 243 · raw
@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {bits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.neg(a)) == Word.inc(64n, Word.not(64n, bits(a))) : Word(64n)}THEOREM: neg is two's-complement negation.