bend-osdev-u32
Releases (1)
-
0.1.0.0 indexed
Definitions (397)
PROOF.bend
- def un.double_mul
- def un.nz
- def un.sz
- def ur.r0
- def ur.r1
- def ur.r2
- def un.dmu.s
- def un.dmu
- def un.dmu.q
- def un.dmu.r
- def ur.r3
- def un.wc
- def ur.r4
- def ur.r5
- def ur.r6
- def ur.r7
- def ur.r8
- def ur.r9
- def ur.r10
- def ur.r11
- def un.low_zero
- def un.high_halfhigh(k, x / 2) = high(k, x) / 2
- def ur.r12
- def un.low_double_low
- def un.odd_d
- def un.odd_d1
- def un.odd_bd
- def un.half_bd
- def un.topc
- def un.top
- def un.putva shift left by one bit, c coming in: twice the value plus c, less 2^n for the bit going out
- def ur.r13
- def un.shlv
- def un.shl_low
- def um.k
- def ur.r14
- def ur.r15
- def ur.r16
- def ur.r17
- def ur.r18
- def ur.r19
- def ur.r20
- def um.go
- def um.e
- def ud.q
- def ud.r
- def un.soWord.shl.out is the bit going out and the shifted word
- def un.ge_lt
- def un.bit_le
- def un.nlt_lenot x < y: y <= x
- def ur.r21
- def ur.r22
- def ur.r23
- def ur.r24
- def ur.r25
- def ur.r26
- def ur.r27
- def ur.r28
- def ur.r29
- def ur.r30
- def ur.r31
- def ud.kr' + g b = 2 r + a, r' < b: the remainder after one step, at a width N
- def ur.r32
- def ur.r33
- def ur.r34
- def ur.r35
- def ur.r36
- def ur.r37
- def ud.fin.t
- def ud.fin.f
- def ud.fin
- def ud.step2
- def ud.step
- def ud.go
- def ud.dq
- def ud.dr
- def ud.nz
- def ud.hb
- def ud.dz2
- def ud.dz
- def ud.p1
- def ud.p2
- def un.band_comm
- def un.bor_comm
- def un.bxor_comm
- def un.bao
- def un.bxa
- def un.band_t
- def un.band_f
- def un.bor_f
- def ur.r38
- def ur.r39
- def ur.r40
- def un.lt1
- def un.dz0
- def un.double_inj
- def un.odd_even
- def un.lt_half
- def un.or_zero
- def ur.r41