~/bend-docscommunity

PROOF.bend checks

raw source on the hub · import 0x340691c4c9cfde2764a3ed46e48d644a/PROOF.bend as PROOF

wordlib: the proofs of LAWS.bend. Each word law is an induction on the width: the head bit follows from a Bool lemma, the tail from the self-call.

5 imports
import Base
import ./LAWS.bend as Laws
import ./word.bend as W
import ./nat.bend as N
import ./ac.bend as A

Definitions

def bool_xor_comm source · line 14 · raw

@a:Bool -> @b:Bool -> {Bool.xor(a, b) == Bool.xor(b, a) : Bool}

def bool_xor_assoc source · line 25 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {Bool.xor(a, Bool.xor(b, c)) == Bool.xor(Bool.xor(a, b), c) : Bool}

def bool_and_comm source · line 44 · raw

@a:Bool -> @b:Bool -> {Bool.and(a, b) == Bool.and(b, a) : Bool}

def bool_and_assoc source · line 55 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}

def bool_or_comm source · line 74 · raw

@a:Bool -> @b:Bool -> {Bool.or(a, b) == Bool.or(b, a) : Bool}

def bool_or_assoc source · line 85 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}

def bool_not_and source · line 104 · raw

@a:Bool -> @b:Bool -> {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}

def scale_dbl source · line 275 · raw

@K:Bool -> @+P:Nat -> {Nat.double(0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K, P)) == 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K, Nat.double(P)) : Nat}

def adc_step source · line 284 · raw

@+S:Nat -> @+k:Nat -> @+a0:Nat -> @+b0:Nat -> @+c:Nat -> @+R:Nat -> @+K:Bool -> @+P:Nat -> @+A0:Nat -> @+B0:Nat -> @ih:{Nat.add(R, 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K, P)) == Nat.add(A0, Nat.add(B0, k)) : Nat} -> @fa:{Nat.add(S, Nat.double(k)) == Nat.add(a0, Nat.add(b0, c)) : Nat} -> {Nat.add(Nat.add(S, Nat.double(R)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K, Nat.double(P))) == Nat.add(Nat.add(a0, Nat.double(A0)), Nat.add(Nat.add(b0, Nat.double(B0)), c)) : Nat}

one bit of the adder, over Nats: S and k are the sum and carry bits, a0 b0 c the input bits, R the tail sum, K its carry, P = 2^p

def no_wrap.eq source · line 424 · raw

@+d:Nat -> @+G:Nat -> @+P:Nat -> @e:{1n+Nat.add(Nat.add(d, P), G) == P : Nat} -> {Nat.add(1n+Nat.add(d, G), P) == Nat.add(0n, P) : Nat}

a value below P plus a full P cannot fit below P

def no_wrap source · line 428 · raw

@+d:Nat -> @+G:Nat -> @+P:Nat -> @e:{1n+Nat.add(Nat.add(d, P), G) == P : Nat} -> Empty

def wrap_exact.sub source · line 431 · raw

@+R:Nat -> @+d:Nat -> @+G:Nat -> @+P:Nat -> @e:{Nat.add(R, 0n) == Nat.add(d, P) : Nat} -> @bound:{1n+Nat.add(R, G) == P : Nat} -> {1n+Nat.add(Nat.add(d, P), G) == P : Nat}

def wrap_exact source · line 437 · raw

@K:Bool -> @+R:Nat -> @+d:Nat -> @+P:Nat -> @+G:Nat -> @e:{Nat.add(R, 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K, P)) == Nat.add(d, P) : Nat} -> @bound:{1n+Nat.add(R, G) == P : Nat} -> {R == d : Nat}

R + K*P == d + P with R below P forces the carry and R == d

def sub_eq.rest source · line 444 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+d:Nat -> @h:{Word.to_nat(n, a) == Nat.add(Word.to_nat(n, b), d) : Nat} -> {Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, Word.not(n, b)), 1n)) == Nat.add(d, 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)) : Nat}

def sub_eq source · line 451 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+d:Nat -> @h:{Word.to_nat(n, a) == Nat.add(Word.to_nat(n, b), d) : Nat} -> {Nat.add(Word.to_nat(n, Word.sub(n, a, b)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, a, Word.not(n, b), True{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n))) == Nat.add(d, 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)) : Nat}

def uniq.shuffle source · line 468 · raw

@+X:Nat -> @+M:Nat -> @+Y:Nat -> @+M2:Nat -> @+P:Nat -> @e:{Nat.add(X, Nat.add(P, M)) == Nat.add(Y, Nat.add(P, M2)) : Nat} -> {Nat.add(Nat.add(X, M), P) == Nat.add(Nat.add(Y, M2), P) : Nat}

X + k*P == Y + j*P with X, Y below P forces X == Y

def uniq.lift source · line 473 · raw

@+X:Nat -> @+Y:Nat -> @+M:Nat -> @+P:Nat -> @e:{Nat.add(X, 0n) == Nat.add(Y, Nat.add(P, M)) : Nat} -> {Nat.add(X, 0n) == Nat.add(Nat.add(Y, M), P) : Nat}

def uniq source · line 477 · raw

@+X:Nat -> @+Y:Nat -> @+P:Nat -> @+GX:Nat -> @+GY:Nat -> @+k:Nat -> @+j:Nat -> @e:{Nat.add(X, Nat.mul(k, P)) == Nat.add(Y, Nat.mul(j, P)) : Nat} -> @bX:{1n+Nat.add(X, GX) == P : Nat} -> @bY:{1n+Nat.add(Y, GY) == P : Nat} -> {X == Y : Nat}

def uniq.conv source · line 495 · raw

@+X:Nat -> @+Y:Nat -> @+L:Nat -> @+L2:Nat -> @+R:Nat -> @+R2:Nat -> @e:{Nat.add(X, L) == Nat.add(Y, R) : Nat} -> @hl:{L == L2 : Nat} -> @hr:{R == R2 : Nat} -> {Nat.add(X, L2) == Nat.add(Y, R2) : Nat}

def assoc.cases source · line 499 · raw

@J2:Bool -> @J1:Bool -> @K2:Bool -> @K1:Bool -> @+Y:Nat -> @+X:Nat -> @+P:Nat -> @+GY:Nat -> @+GX:Nat -> @e:{Nat.add(Y, Nat.add(0x340691c4c9cfde2764a3ed46e48d644a/word.scale(J2, P), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(J1, P))) == Nat.add(X, Nat.add(0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K2, P), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K1, P))) : Nat} -> @bY:{1n+Nat.add(Y, GY) == P : Nat} -> @bX:{1n+Nat.add(X, GX) == P : Nat} -> {Y == X : Nat}

def assoc.r source · line 568 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+c:Word(n) -> {Nat.add(Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), Nat.add(0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, Word.add(n, a, b), c, False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, a, b, False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat}

(a + b) + c, by value: X + 2^n*(K2 + K1) == A + (B + C)

def assoc.l source · line 576 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+c:Word(n) -> {Nat.add(Word.to_nat(n, Word.add(n, a, Word.add(n, b, c))), Nat.add(0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, a, Word.add(n, b, c), False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, b, c, False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)))) == Nat.add(Word.to_nat(n, a), Nat.add(Word.to_nat(n, b), Word.to_nat(n, c))) : Nat}

a + (b + c), by value: Y + 2^n*(J2 + J1) == A + (B + C)

def assoc.eq source · line 583 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+c:Word(n) -> {Nat.add(Word.to_nat(n, Word.add(n, a, Word.add(n, b, c))), Nat.add(0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, a, Word.add(n, b, c), False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, b, c, False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)))) == Nat.add(Word.to_nat(n, Word.add(n, Word.add(n, a, b), c)), Nat.add(0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, Word.add(n, a, b), c, False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, a, b, False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n)))) : Nat}

def no_carry.sub source · line 596 · raw

@+R:Nat -> @+S:Nat -> @+P:Nat -> @+g:Nat -> @e:{Nat.add(R, P) == S : Nat} -> @h:{1n+Nat.add(S, g) == P : Nat} -> {1n+Nat.add(Nat.add(R, P), g) == P : Nat}

def no_carry source · line 601 · raw

@K:Bool -> @+R:Nat -> @+S:Nat -> @+P:Nat -> @+g:Nat -> @e:{Nat.add(R, 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K, P)) == S : Nat} -> @h:{1n+Nat.add(S, g) == P : Nat} -> {R == S : Nat}

R + K*P == S with S below P rules the carry out

def add_eq source · line 608 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Nat.add(Word.to_nat(n, Word.add(n, a, b)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(0x340691c4c9cfde2764a3ed46e48d644a/word.carry(n, a, b, False{}), 0x340691c4c9cfde2764a3ed46e48d644a/word.pow2(n))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}

def shl_step source · line 620 · raw

@+c:Nat -> @+R:Nat -> @+K:Bool -> @+P:Nat -> @+bb:Nat -> @+T:Nat -> @ih:{Nat.add(R, 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K, P)) == Nat.add(bb, Nat.double(T)) : Nat} -> {Nat.add(Nat.add(c, Nat.double(R)), 0x340691c4c9cfde2764a3ed46e48d644a/word.scale(K, Nat.double(P))) == Nat.add(c, Nat.double(Nat.add(bb, Nat.double(T)))) : Nat}

one step of shl.put over Nats: c the bit shifted in, R the tail, K the bit shifted out, P = 2^p, bb and T the input's head and tail

def cmp_bits_00 source · line 690 · raw

@+x:Nat -> @+y:Nat -> {Word.cmp.fin(False{}, False{}, Nat.cmp(x, y)) == Nat.cmp(Nat.double(x), Nat.double(y)) : Cmp}

def cmp_bits_01 source · line 701 · raw

@+x:Nat -> @+y:Nat -> {Word.cmp.fin(False{}, True{}, Nat.cmp(x, y)) == Nat.cmp(Nat.double(x), 1n+Nat.double(y)) : Cmp}

def cmp_bits_10 source · line 712 · raw

@+x:Nat -> @+y:Nat -> {Word.cmp.fin(True{}, False{}, Nat.cmp(x, y)) == Nat.cmp(1n+Nat.double(x), Nat.double(y)) : Cmp}

def cmp_bits_11 source · line 723 · raw

@+x:Nat -> @+y:Nat -> {Word.cmp.fin(True{}, True{}, Nat.cmp(x, y)) == Nat.cmp(1n+Nat.double(x), 1n+Nat.double(y)) : Cmp}