bend-osdev-word64
Releases (2)
Definitions (425)
PROOF_div.bend
- def wd.bt
- def wd.bv
- def wd.bl
- def wd.topthe top bit of a word, below 2
- def wd.nz
- def wd.wvthe value of a word one bit longer
- def wd.etaa pair is its two parts
- def wd.p1
- def wd.p2
- def wr.d0
- def wr.d1
- def wr.d2
- def wr.d3
- def wr.d4
- def wd.k
- def wr.d5
- def wr.d6
- def wr.d7
- def wd.sel
- def wd.st
- def wr.d8
- def wr.d9
- def wd.bs
- def wd.bits
- def wr.d10
- def wd.dz2
- def wd.dz
PROOF_mul.bend
- def wu.ve
- def wu.lt
- def wv.g
- def wv.ve
- def wv.lt64
- def wn.sub0
- def wn.le0
- def wn.ft
- def wn.tf
- def wn.ge_lt
- def wm.fn
- def wr.m0
- def wm.hl
- def wr.m1
- def wr.m2
- def wr.m3
- def wm.s3
- def wm.low2lo + 2^h hi < 2^n for lo, hi < 2^h
- def wm.plx, y < 2^h: x y < 2^n
- def wr.m4
- def wr.m5
- def wr.m6
- def wr.m7
- def wr.m8
- def wr.m9
- def wm.k
- def wr.m10
- def wr.m11
- def wr.m12
- def wr.m13
- def wq.k
PROOF_text.bend
- def wu.ve
- def wu.lt
- def wv.g
- def wv.ve
- def wv.lt64
- def wn.sub0
- def wn.le0
- def wn.ft
- def wn.tf
- def wn.ge_lt
- def wm.fn
- def wsd.pw
- def wsd.pwv
- def wr.t0
- def wr.t1
- def wsd.mulpw
- def wsd.mul16
- def wsd.mlea c < b c: a < b
- def wsd.mlc.go
- def wsd.mlc
- def wsd.knx < 2^h 10: x < 2^n (for 10 <= 2^h)
- def wr.t2
- def wr.t3
- def wr.t4
- def wr.t5
- def wsd.k1
- def wsd.k210 d + m = v < 2^h 10: d < 2^h
- def wsd.k3q < 2^h: the shift of q by h is 2^h q
- def wsd.fst
- def wsd.snd
- def wsh.q
- def wsh.r
- def wsd.v
- def wsd.d
- def wsd.m
- def wsd.q
- def wsd.step
- def wr.t6
- def wr.t7
- def wr.t8
- def wr.t9
- def wsd.alg