~/bend-docscommunity

src/u32.bend fails

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/u32.bend as MU32

3 imports
import Base
import ./nat.bend as Nat
import ./class.bend as C

Laws

law cmp_bits unverifiedits file does not pass the checker (fails)source · line 24 · raw

@x:Bool -> @y:Bool -> @a:Nat -> @b:Nat -> {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(Nat.add(bit(x), Nat.double(a)), Nat.add(bit(y), Nat.double(b))) : Cmp}

comparing bit + 2*rest compares the rests first, then the bits, which is what Word.cmp.fin does

law Word.cmp_nat unverifiedits file does not pass the checker (fails)source · line 66 · raw

@+n:Nat -> @a:Word(n) -> @b:Word(n) -> {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}

law cmp_nat unverifiedits file does not pass the checker (fails)source · line 93 · raw

@a:U32 -> @b:U32 -> {Nat.cmp(U32.to_nat(a), U32.to_nat(b)) == U32.cmp(a, b) : Cmp}

law is_lt_nat unverifiedits file does not pass the checker (fails)source · line 108 · raw

@+a:U32 -> @+b:U32 -> @-c:Bool -> @e:{U32.is_lt(a, b) == c : Bool} -> {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == c : Bool}

a result of U32.is_lt is the same result of Nat.is_lt on the numbers

law min_le_r.go unverifiedits file does not pass the checker (fails)source · line 123 · raw

@+a:U32 -> @+b:U32 -> @c:Bool -> @e:{U32.is_lt(a, b) == c : Bool} -> LE(Bool.pick(U32, c, a, b), b)

law min_le_r unverifiedits file does not pass the checker (fails)source · line 138 · raw

@+a:U32 -> @+b:U32 -> LE(U32.min(a, b), b)

min(a, b) <= b

law le_max_r.go unverifiedits file does not pass the checker (fails)source · line 146 · raw

@+a:U32 -> @+b:U32 -> @c:Bool -> @e:{U32.is_lt(a, b) == c : Bool} -> LE(b, Bool.pick(U32, c, b, a))

law le_max_r unverifiedits file does not pass the checker (fails)source · line 161 · raw

@+a:U32 -> @+b:U32 -> LE(b, U32.max(a, b))

b <= max(a, b)

law clamp_le_hi unverifiedits file does not pass the checker (fails)source · line 170 · raw

@+x:U32 -> @+lo:U32 -> @+hi:U32 -> LE(U32.clamp(x, lo, hi), hi)

clamp(x, lo, hi) <= hi, even when lo > hi

law lo_le_clamp.go unverifiedits file does not pass the checker (fails)source · line 179 · raw

@+lo:U32 -> @+m:U32 -> @+hi:U32 -> @lm:LE(lo, m) -> @lh:LE(lo, hi) -> @c:Bool -> LE(lo, Bool.pick(U32, c, m, hi))

law lo_le_clamp unverifiedits file does not pass the checker (fails)source · line 196 · raw

@+x:U32 -> @+lo:U32 -> @+hi:U32 -> @lh:LE(lo, hi) -> LE(lo, U32.clamp(x, lo, hi))

lo <= clamp(x, lo, hi) when lo <= hi

law Word.sub_add unverifiedits file does not pass the checker (fails)source · line 215 · raw

@+n:Nat -> @a:Word(n) -> @+b:Word(n) -> @c:Bool -> {a == Word.adc(n, Word.adc(n, a, b, False{}, c), b, True{}, Bool.not(c)) : Word(n)}

(a + b + c) - b, with carry not(c), is a. Each case passes the carry out of its bit.

law Word.sub_add.arm unverifiedits file does not pass the checker (fails)source · line 223 · raw

@-p:Nat -> @-h:Bool -> @-at:Word(p) -> @-bt:Word(p) -> @-k:Bool -> @e:{at == Word.adc(p, Word.adc(p, at, bt, False{}, k), bt, True{}, Bool.not(k)) : Word(p)} -> {WCon{h, at} == WCon{h, Word.adc(p, Word.adc(p, at, bt, False{}, k), bt, True{}, Bool.not(k))} : Word(1n+p)}

one bit: the bit is kept, and e is the law for the rest at the carry k

law Word.add_sub unverifiedits file does not pass the checker (fails)source · line 261 · raw

@+n:Nat -> @a:Word(n) -> @+b:Word(n) -> @c:Bool -> {a == Word.adc(n, Word.adc(n, a, b, True{}, c), b, False{}, Bool.not(c)) : Word(n)}

(a - b) + b, with carry not(c), is a

law Word.add_sub.arm unverifiedits file does not pass the checker (fails)source · line 269 · raw

@-p:Nat -> @-h:Bool -> @-at:Word(p) -> @-bt:Word(p) -> @-k:Bool -> @e:{at == Word.adc(p, Word.adc(p, at, bt, True{}, k), bt, False{}, Bool.not(k)) : Word(p)} -> {WCon{h, at} == WCon{h, Word.adc(p, Word.adc(p, at, bt, True{}, k), bt, False{}, Bool.not(k))} : Word(1n+p)}

one bit: the bit is kept, and e is the law for the rest at the carry k

law sub_add unverifiedits file does not pass the checker (fails)source · line 307 · raw

@a:U32 -> @b:U32 -> {a == U32.sub(U32.add(a, b), b) : U32}

subtracting b undoes adding b, with wraparound

law add_sub unverifiedits file does not pass the checker (fails)source · line 318 · raw

@a:U32 -> @b:U32 -> {a == U32.add(U32.sub(a, b), b) : U32}

adding b undoes subtracting b, with wraparound

Definitions

def bit source · line 15 · raw

@b:Bool -> Nat

def LE source · line 104 · raw

@a:U32 -> @b:U32 -> Data

a <= b on U32

def group source · line 329 · raw

0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Group<U32>

wrapping + and - as a C.Group