proofs/word_encoding.bend checks

law double_add proved

Also proved in bend-mathlib as nat.double_add: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.double_add.

source · line 22 · raw

@+a:Nat -> @+b:Nat -> {Nat.double(Nat.add(a, b)) == Nat.add(Nat.double(a), Nat.double(b)) : Nat}

law zero_nat provedsource · line 35 · raw

@+n:Nat -> {Word.to_nat(n, Word.zero(n)) == 0n : Nat}

law finish_lt_zero provedsource · line 47 · raw

@+b:Bool -> @+c:Cmp -> {Cmp.is_lt(Word.cmp.fin(b, False{}, c)) == Cmp.is_lt(c) : Bool}

law compare_high_only provedsource · line 67 · raw

@+n:Nat -> @+m:Nat -> @+w:Word(n) -> @+top:Word(m) -> @+other:Word(m) -> {Cmp.is_lt(Word.cmp(Nat.add(n, m), concat(n, m, w, top), concat(n, m, Word.zero(n), other))) == Cmp.is_lt(Word.cmp(m, top, other)) : Bool}

law nonnegative provedsource · line 88 · raw

@+n:Nat -> @+w:Word(n) -> {Cmp.is_lt(Word.cmp(n, w, Word.zero(n))) == False{} : Bool}

law finish_one provedsource · line 116 · raw

@+b:Bool -> @+c:Cmp -> @nonneg:{Cmp.is_lt(c) == False{} : Bool} -> {Cmp.is_lt(Word.cmp.fin(b, True{}, c)) == Cmp.is_eq(Word.cmp.fin(b, False{}, c)) : Bool}

law less_one_is_zero provedsource · line 137 · raw

@+n:Nat -> @+w:Word(1n+n) -> {Cmp.is_lt(Word.cmp(1n+n, w, WCon{True{}, Word.zero(n)})) == Cmp.is_eq(Word.cmp(1n+n, w, Word.zero(1n+n))) : Bool}

law join_prepend provedsource · line 167 · raw

@+n:Nat -> @+m:Nat -> @+b:Bool -> @+parts:Split<n, m> -> {WCon{b, join(n, m, parts)} == join(1n+n, m, prepend(n, m, b, parts)) : Word(1n+Nat.add(n, m))}

law recover provedsource · line 178 · raw

@+n:Nat -> @+m:Nat -> @+w:Word(Nat.add(n, m)) -> {join(n, m, split(n, m, w)) == w : Word(Nat.add(n, m))}

law cmp_eq provedsource · line 195 · raw

@+c:Cmp -> @yes:{Cmp.is_eq(c) == True{} : Bool} -> {c == EQ{} : Cmp}

law finish_eq_parts provedsource · line 209 · raw

@+b:Bool -> @+c:Cmp -> @eq:{Word.cmp.fin(b, False{}, c) == EQ{} : Cmp} -> Pair({b == False{} : Bool}, {c == EQ{} : Cmp})

law zero_reflect provedsource · line 230 · raw

@+n:Nat -> @+w:Word(n) -> @eq:{Word.cmp(n, w, Word.zero(n)) == EQ{} : Cmp} -> {w == Word.zero(n) : Word(n)}

law below_one_zero provedsource · line 254 · raw

@+n:Nat -> @+w:Word(1n+n) -> @below:{Cmp.is_lt(Word.cmp(1n+n, w, WCon{True{}, Word.zero(n)})) == True{} : Bool} -> {w == Word.zero(1n+n) : Word(1n+n)}

law and_zero provedsource · line 265 · raw

@+n:Nat -> @+w:Word(n) -> {Word.and(n, w, Word.zero(n)) == Word.zero(n) : Word(n)}

law upper_zero provedsource · line 285 · raw

@+n:Nat -> @+m:Nat -> @+low:Word(n) -> @+high:Word(1n+m) -> @bound:{Cmp.is_lt(Word.cmp(Nat.add(n, 1n+m), concat(n, 1n+m, low, high), concat(n, 1n+m, Word.zero(n), WCon{True{}, Word.zero(m)}))) == True{} : Bool} -> {high == Word.zero(1n+m) : Word(1n+m)}

type Split source · line 147 · raw

@-n:Nat -> @-m:Nat -> Data

• Parts

  @-n:Nat -> @-m:Nat -> @low:Word(n) -> @high:Word(m) -> Split<n, m>

def concat source · line 4 · raw

@+n:Nat -> @+m:Nat -> @w:Word(n) -> @tail:Word(m) -> Word(Nat.add(n, m))

def shift source · line 15 · raw

@n:Nat -> @x:Nat -> Nat

def truth source · line 105 · raw

@b:Bool -> Type

def false_true source · line 112 · raw

@e:{False{} == True{} : Bool} -> Empty

def join source · line 150 · raw

@+n:Nat -> @+m:Nat -> @parts:Split<n, m> -> Word(Nat.add(n, m))

def prepend source · line 154 · raw

@-n:Nat -> @-m:Nat -> @b:Bool -> @parts:Split<n, m> -> Split<1n+n, m>

def split source · line 158 · raw

@+n:Nat -> @+m:Nat -> @w:Word(Nat.add(n, m)) -> Split<n, m>

def zero_step source · line 236 · raw

@+p:Nat -> @+b:Bool -> @+rest:Word(p) -> @proof:Pair({b == False{} : Bool}, {Word.cmp(p, rest, Word.zero(p)) == EQ{} : Cmp}) -> @ih:(@_:{Word.cmp(p, rest, Word.zero(p)) == EQ{} : Cmp} -> {rest == Word.zero(p) : Word(p)}) -> {WCon{b, rest} == Word.zero(1n+p) : Word(1n+p)}