~/bend-docscommunity

proofs/math/u64/u64div.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as U64div

19 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/u32alg.bend as A
import ../../lib/u32.bend as U3
import ../../lib/lemmas/proofs/division_quotient.bend as DQ
import ../../lib/word.bend as WD
import ../../lib/arith.bend as AR
import ../../lib/u32div.bend as UD
import ./u64.bend as P
import ../../lib/lemmas/types/model.bend as T
import ../../lib/lemmas/proofs/modular_addition.bend as MA
import ../../lib/lemmas/proofs/modular_negation.bend as MN
import ../../lib/lemmas/proofs/negation_magnitude.bend as NM
import ../../lib/lemmas/proofs/word_value.bend as WV

Definitions

def dm_e2 source · line 28 · raw

@+a:U32 -> @+b:U32 -> @h:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.dm_type(a, b) -> {Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.div(a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.mod(a, b))) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(a) : Nat}

def dm_l2 source · line 32 · raw

@+a:U32 -> @+b:U32 -> @h:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.dm_type(a, b) -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.mod(a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(b)) == True{} : Bool}

def dm_e source · line 36 · raw

@+a:U32 -> @+b:U32 -> @+hb:{U32.is_zero(b) == False{} : Bool} -> {Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.div(a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.mod(a, b))) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(a) : Nat}

def dm_l source · line 39 · raw

@+a:U32 -> @+b:U32 -> @+hb:{U32.is_zero(b) == False{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.mod(a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(b)) == True{} : Bool}

def mul32 source · line 42 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+h:{Nat.is_lt(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(y)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.mul(x, y)) == Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(y)) : Nat}

def add32 source · line 49 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+h:{Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(y)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.add(x, y)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(y)) : Nat}

def hp32 source · line 56 · raw

@+k:Nat -> @x:U32 -> Nat

def and32w source · line 61 · raw

@+k:Nat -> @+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(x, U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)})), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, hp32(k, x))) : Nat}

def and32 source · line 68 · raw

@+k:Nat -> @+x:U32 -> @+m:U32 -> @+hm:{m == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)} : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(x, m)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, hp32(k, x))) : Nat}

def and32_ltw source · line 71 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(x, U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)})), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one)) == True{} : Bool}

def and32_lt source · line 77 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+m:U32 -> @+hm:{m == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)} : U32} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(x, m)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one)) == True{} : Bool}

def pow32 source · line 80 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:U32 -> @+hc:{c == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, k)} : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(c) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one) : Nat}

def le32 source · line 84 · raw

@+a:U32 -> @+b:U32 -> @+h:{U32.is_le(a, b) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(a), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(b)) == True{} : Bool}

def g_fin source · line 89 · raw

@+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+c20:U32 -> @+c8:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def g_t3 source · line 92 · raw

@+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+t1:U32 -> @+t2:U32 -> @+c20:U32 -> @+c8:U32 -> @+m8:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def g_t2 source · line 95 · raw

@+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+t1:U32 -> @+c20:U32 -> @+c12:U32 -> @+c8:U32 -> @+m12:U32 -> @+m8:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def gdiv source · line 98 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> @+c20:U32 -> @+c12:U32 -> @+c8:U32 -> @+m12:U32 -> @+m8:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def impl source · line 102 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.div_small(a, d) == gdiv(a, d, 1048576, 4096, 256, 4095, 255) : 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64}

def expand source · line 110 · raw

@+h:Nat -> @+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(12n, Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(12n, h), a)), b)), c) == Nat.add(Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(20n, a), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, b)), c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, h)) : Nat}

2^8 (2^12 (2^12 h + a) + b) + c == ((2^20 a + 2^8 b) + c) + 2^32 h

def lt_eq source · line 123 · raw

@+a:Nat -> @+b:Nat -> @+k:Nat -> @+e:{a == b : Nat} -> @+h:{Nat.is_lt(a, k) == True{} : Bool} -> {Nat.is_lt(b, k) == True{} : Bool}

a value equation rewritten into a bound

def mul_pow source · line 127 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+j:Nat -> @+c:Nat -> @+kv:Nat -> @+hk:{kv == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, one) : Nat} -> {Nat.mul(c, kv) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, c) : Nat}

a scaled product c*k with v(k) == 2^j, as 2^j c

def mulp32 source · line 131 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+j:Nat -> @+x:U32 -> @+k:U32 -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(k) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, one) : Nat} -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.mul(x, k)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x)) : Nat}

v(x * k) == 2^j v(x) when v(k) == 2^j and 2^j v(x) < 2^32

def addv32 source · line 136 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+a:Nat -> @+b:Nat -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x) == a : Nat} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(y) == b : Nat} -> @+h:{Nat.is_lt(Nat.add(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.add(x, y)) == Nat.add(a, b) : Nat}

v(x + y) == a + b when v(x) == a, v(y) == b and a + b < 2^32

def lo_eq source · line 142 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+lo:U32 -> @+c20:U32 -> @+c8:U32 -> @+m12:U32 -> @+m8:U32 -> @+h20:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(c20) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(20n, one) : Nat} -> @+h8:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(c8) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one) : Nat} -> @+hm12:{m12 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 12n)} : U32} -> @+hm8:{m8 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 8n)} : U32} -> @+nz20:{U32.is_zero(c20) == False{} : Bool} -> @+nz8:{U32.is_zero(c8) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(lo) == Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(20n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.div(lo, c20))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(U32.div(lo, c8), m12)))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(lo, m8))) : Nat}

def lo_l1 source · line 177 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+lo:U32 -> @+c20:U32 -> @+h20:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(c20) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(20n, one) : Nat} -> @+nz20:{U32.is_zero(c20) == False{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.div(lo, c20)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(12n, one)) == True{} : Bool}

the top digit of the low limb is below 2^12

def tval source · line 185 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+j:Nat -> @+x:U32 -> @+k:U32 -> @+y:U32 -> @+dn:Nat -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(k) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, one) : Nat} -> @+hy:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(y), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, one)) == True{} : Bool} -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x), dn) == True{} : Bool} -> @+hjk:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, dn), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.add(U32.mul(x, k), y)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(x)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(y)) : Nat}

one digit of the long division: t = x * 2^j + y with x < d, y < 2^j

def gval source · line 192 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+c20:U32 -> @+c12:U32 -> @+c8:U32 -> @+m12:U32 -> @+m8:U32 -> @+hd0:{U32.is_zero(d) == False{} : Bool} -> @+hle:{U32.is_le(d, c20) == True{} : Bool} -> @+p20:{c20 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 20n)} : U32} -> @+p12:{c12 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 12n)} : U32} -> @+p8:{c8 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 8n)} : U32} -> @+hm12:{m12 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 12n)} : U32} -> @+hm8:{m8 == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 8n)} : U32} -> @+nz20:{U32.is_zero(c20) == False{} : Bool} -> @+nz8:{U32.is_zero(c8) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.val(gdiv(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{lo, hi}, d, c20, c12, c8, m12, m8)) == Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.val(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{lo, hi}), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(d)) : Nat}

def div_value source · line 274 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> @+hd0:{U32.is_zero(d) == False{} : Bool} -> @+hle:{U32.is_le(d, 1048576) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.val(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.div_small(a, d)) == Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.val(a), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(d)) : Nat}

THEOREM: div_small is Nat division of the 64-bit value, for 0 < d <= 2^20.

def from_u source · line 281 · raw

@+n:Nat -> @+w:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.from_nat(n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(n, w)) == w : Word(n)}

def div_bits source · line 286 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> @+hd0:{U32.is_zero(d) == False{} : Bool} -> @+hle:{U32.is_le(d, 1048576) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.div_small(a, d)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned_quotient(64n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bits(a), d) : Word(64n)}

THEOREM: div_small is the specification's unsigned 64-bit quotient.

def neg_quot source · line 295 · raw

@+n:Nat -> @+w:Word(n) -> @+d:U32 -> @+hnz:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.is_zero(n, w) == False{} : Bool} -> {Word.inc(n, Word.not(n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned_quotient(n, Word.inc(n, Word.not(n, w)), d))) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.negative_quotient(n, w, d) : Word(n)}

negate, divide the magnitude, negate back: the specification's quotient of a negative word, at every width

def is_zero_eq source · line 319 · raw

@+n:Nat -> @+w:Word(n) -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.is_zero(n, w) == True{} : Bool} -> {w == Word.zero(n) : Word(n)}

def nz_g source · line 328 · raw

@+w:Word(64n) -> @+z:Bool -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.is_zero(64n, w) == z : Bool} -> @+hn:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.negative(w) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.is_zero(64n, w) == False{} : Bool}

def nz_neg source · line 336 · raw

@+w:Word(64n) -> @+hn:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.negative(w) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.is_zero(64n, w) == False{} : Bool}

a negative word is nonzero

def qs source · line 339 · raw

@w:Word(64n) -> @neg:Bool -> @+d:U32 -> Word(64n)

def signed_g source · line 342 · raw

@+lo:U32 -> @+hi:U32 -> @+d:U32 -> @+hd0:{U32.is_zero(d) == False{} : Bool} -> @+hle:{U32.is_le(d, 1048576) == True{} : Bool} -> @+g:Bool -> @+hg:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.negative(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.pack(lo, hi)) == g : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.div_sign(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{lo, hi}, d, g)) == qs(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.pack(lo, hi), g, d) : Word(64n)}

def div_signed source · line 358 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+d:U32 -> @+hd0:{U32.is_zero(d) == False{} : Bool} -> @+hle:{U32.is_le(d, 1048576) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.div_small_signed(a, d)) == qs(0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bits(a), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.negative(0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bits(a)), d) : Word(64n)}

THEOREM: div_small_signed is the specification's signed quotient (truncating toward zero), for 0 < d <= 2^20.

def qs_spec source · line 364 · raw

@+w:Word(64n) -> @+neg:Bool -> {qs(w, neg, 1000000) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.quotient_signed(w, neg) : Word(64n)}

def milliseconds source · line 372 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.I64{0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.div_small_signed(a, 1000000))} == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.milliseconds(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.I64{0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bits(a)}) : 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64}

THEOREM: dividing by 10^6 is the specification's nanoseconds-to-milliseconds.