proofs/word_multiplication.bend
stelliferous@0.0.2.0 · 151 lines · 13 definitions
1import Base
2import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
3import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
4import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
5
6def truncate(n: Nat,w: Word(1n+n)) -> Word(n):
7 match n:
8 case 0n:
9 WNil{}
10 case 1n+p:
11 WCon{b,t} = w
12 WCon{b,truncate(p,t)}
13
14def truncate_zero(+n: Nat) -> {truncate(n,Word.zero(1n+n)) == Word.zero(n) : Word(n)}:
15 match n:
16 case 0n:
17 {==}
18 case 1n+ +p:
19 %truncate_zero(p) : {WCon{False{},truncate(p,Word.zero(1n+p))} == WCon{False{},_} : Word(1n+p)}
20 {==}
21
22def truncate_inc(+n: Nat,+w: Word(1n+n)) -> {truncate(n,Word.inc(1n+n,w)) == Word.inc(n,truncate(n,w)) : Word(n)}:
23 match n:
24 case 0n:
25 {==}
26 case 1n+ +p:
27 match w:
28 case WCon{False{},t}:
29 {==}
30 case WCon{True{},+t}:
31 %truncate_inc(p,t) : {WCon{False{},truncate(p,Word.inc(1n+p,t))} == WCon{False{},_} : Word(1n+p)}
32 {==}
33
34def truncate_encode(+a: Nat,+n: Nat) -> {truncate(n,WordArithmetic.encode(a,1n+n)) == WordArithmetic.encode(a,n) : Word(n)}:
35 match a:
36 case 0n:
37 truncate_zero(n)
38 case 1n+ +p:
39 %Equal.sym(Word(n),truncate(n,Word.inc(1n+n,WordArithmetic.encode(p,1n+n))),Word.inc(n,truncate(n,WordArithmetic.encode(p,1n+n))),
40 truncate_inc(n,WordArithmetic.encode(p,1n+n))) : {_ == Word.inc(n,WordArithmetic.encode(p,n)) : Word(n)}
41 %truncate_encode(p,n) : {Word.inc(n,truncate(n,WordArithmetic.encode(p,1n+n))) == Word.inc(n,_) : Word(n)}
42 {==}
43
44def put(+n: Nat,+b: Bool,+w: Word(n)) -> {Word.shl.put(n,b,w) == truncate(n,WCon{b,w}) : Word(n)}:
45 match n:
46 case 0n:
47 {==}
48 case 1n+ +p:
49 WCon{+c,+t} = w
50 %put(p,c,t) : {WCon{b,Word.shl.put(p,c,t)} == WCon{b,_} : Word(1n+p)}
51 {==}
52
53def shift(+n: Nat,+w: Word(1n+n)) -> {Word.shl(1n+n,w) == WCon{False{},truncate(n,w)} : Word(1n+n)}:
54 WCon{+b,+t} = w
55 %put(n,b,t) : {WCon{False{},Word.shl.put(n,b,t)} == WCon{False{},_} : Word(1n+n)}
56 {==}
57
58def encoded_double(+a: Nat,+n: Nat) -> {WordArithmetic.encode(Nat.double(a),1n+n) == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}:
59 %Equal.sym(Word(1n+n),WordArithmetic.encode(Nat.double(a),1n+n),Word.shl(1n+n,WordArithmetic.encode(a,1n+n)),WordArithmetic.encode_double(a,
60 1n+n)) : {_ == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}
61 %Equal.sym(Word(1n+n),Word.shl(1n+n,WordArithmetic.encode(a,1n+n)),WCon{False{},truncate(n,WordArithmetic.encode(a,1n+n))},shift(n,
62 WordArithmetic.encode(a,1n+n))) : {_ == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}
63 %truncate_encode(a,n) : {WCon{False{},truncate(n,WordArithmetic.encode(a,1n+n))} == WCon{False{},_} : Word(1n+n)}
64 {==}
65
66law word_roundtrip:
67 for +n: Nat
68 for +w: Word(n)
69 {WordArithmetic.encode(Word.to_nat(n,w),n) == w : Word(n)}
70def word_roundtrip(n,w):
71 match n:
72 case 0n:
73 WNil{} = w
74 {==}
75 case 1n+ +p:
76 match w:
77 case WCon{False{},+t}:
78 %Equal.sym(Word(1n+p),WordArithmetic.encode(Nat.double(Word.to_nat(p,t)),1n+p),WCon{False{},WordArithmetic.encode(Word.to_nat(p,t),p)},
79 encoded_double(Word.to_nat(p,t),p)) : {_ == WCon{False{},t} : Word(1n+p)}
80 %Equal.sym(Word(p),WordArithmetic.encode(Word.to_nat(p,t),p),t,word_roundtrip(p,t)) : {WCon{False{},_} == WCon{False{},t} : Word(1n+p)}
81 {==}
82 case WCon{True{},+t}:
83 %Equal.sym(Word(1n+p),WordArithmetic.encode(Nat.double(Word.to_nat(p,t)),1n+p),WCon{False{},WordArithmetic.encode(Word.to_nat(p,t),p)},
84 encoded_double(Word.to_nat(p,t),p)) : {Word.inc(1n+p,_) == WCon{True{},t} : Word(1n+p)}
85 %Equal.sym(Word(p),WordArithmetic.encode(Word.to_nat(p,t),p),t,word_roundtrip(p,t)) : {WCon{True{},_} == WCon{True{},t} : Word(1n+p)}
86 {==}
87
88def double_mul(+a: Nat,+b: Nat) -> {Nat.mul(Nat.double(a),b) == Nat.mul(a,Nat.double(b)) : Nat}:
89 match a:
90 case 0n:
91 {==}
92 case 1n+ +p:
93 %Addition.double(b) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == Nat.add(_,Nat.mul(p,Nat.double(b))) : Nat}
94 %Equal.sym(Nat,Nat.add(Nat.add(b,b),Nat.mul(p,Nat.double(b))),Nat.add(b,Nat.add(b,Nat.mul(p,Nat.double(b)))),Addition.associative(b,b,Nat.mul(p,
95 Nat.double(b)))) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == _ : Nat}
96 %double_mul(p,b) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == Nat.add(b,Nat.add(b,_)) : Nat}
97 {==}
98
99law multiply_go:
100 for +m: Nat
101 for +n: Nat
102 for +w: Word(m)
103 for +b: Nat
104 for +acc: Nat
105 {Word.mul.go(n,m,w,WordArithmetic.encode(b,n),WordArithmetic.encode(acc,n)) == WordArithmetic.encode(Nat.add(acc,Nat.mul(Word.to_nat(m,w),b)),
106 n) : Word(n)}
107def multiply_go(m,n,w,b,acc):
108 match m:
109 case 0n:
110 %Equal.sym(Nat,Nat.add(acc,0n),acc,Addition.zero_right(acc)) : {WordArithmetic.encode(acc,n) == WordArithmetic.encode(_,n) : Word(n)}
111 {==}
112 case 1n+ +p:
113 match w:
114 case WCon{False{},+t}:
115 %WordArithmetic.encode_double(b,n) : {Word.mul.go(n,p,t,_,WordArithmetic.encode(acc,n)) == WordArithmetic.encode(Nat.add(acc,
116 Nat.mul(Nat.double(Word.to_nat(p,t)),b)),n) : Word(n)}
117 %Equal.sym(Nat,Nat.mul(Nat.double(Word.to_nat(p,t)),b),Nat.mul(Word.to_nat(p,t),Nat.double(b)),double_mul(Word.to_nat(p,t),
118 b)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),WordArithmetic.encode(acc,n)) == WordArithmetic.encode(Nat.add(acc,
119 _),n) : Word(n)}
120 multiply_go(p,n,t,Nat.double(b),acc)
121 case WCon{True{},+t}:
122 %WordArithmetic.encode_double(b,n) : {Word.mul.go(n,p,t,_,Word.add(n,WordArithmetic.encode(acc,n),WordArithmetic.encode(b,
123 n))) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,Nat.mul(Nat.double(Word.to_nat(p,t)),b))),n) : Word(n)}
124 %Equal.sym(Word(n),Word.add(n,WordArithmetic.encode(acc,n),WordArithmetic.encode(b,n)),WordArithmetic.encode(Nat.add(acc,b),n),
125 WordArithmetic.encode_add(acc,b,n)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),
126 _) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,Nat.mul(Nat.double(Word.to_nat(p,t)),b))),n) : Word(n)}
127 %Equal.sym(Nat,Nat.mul(Nat.double(Word.to_nat(p,t)),b),Nat.mul(Word.to_nat(p,t),Nat.double(b)),double_mul(Word.to_nat(p,t),
128 b)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),WordArithmetic.encode(Nat.add(acc,b),
129 n)) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,_)),n) : Word(n)}
130 %Addition.associative(acc,b,Nat.mul(Word.to_nat(p,t),Nat.double(b))) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),
131 WordArithmetic.encode(Nat.add(acc,b),n)) == WordArithmetic.encode(_,n) : Word(n)}
132 multiply_go(p,n,t,Nat.double(b),Nat.add(acc,b))
133
134def multiply(+n: Nat,+a: Word(n),+b: Word(n)) -> {Word.mul(n,a,b) == WordArithmetic.encode(Nat.mul(Word.to_nat(n,a),Word.to_nat(n,b)),n) : Word(n)}:
135 %word_roundtrip(n,b) : {Word.mul.go(n,n,a,_,Word.zero(n)) == WordArithmetic.encode(Nat.mul(Word.to_nat(n,a),Word.to_nat(n,b)),n) : Word(n)}
136 multiply_go(n,n,a,Word.to_nat(n,b),0n)
137
138def native_multiply(+a: U32,+b: U32) -> {U32.mul(a,b) == U32.from_nat(Nat.mul(U32.to_nat(a),U32.to_nat(b))) : U32}:
139 match a b:
140 case U32{+x} U32{+y}:
141 %Equal.sym(U32,U32.from_nat(Nat.mul(Word.to_nat(32n,x),Word.to_nat(32n,y))),U32{WordArithmetic.encode(Nat.mul(Word.to_nat(32n,x),
142 Word.to_nat(32n,y)),32n)},WordArithmetic.native_encoding(Nat.mul(Word.to_nat(32n,x),Word.to_nat(32n,y)))) : {U32{Word.mul(32n,x,
143 y)} == _ : U32}
144 %multiply(32n,x,y) : {U32{Word.mul(32n,x,y)} == U32{_} : U32}
145 {==}
146
147def bounded_multiply(+a: U32,+b: U32,+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},h: {Nat.is_le(Nat.mul(U32.to_nat(a),
148 U32.to_nat(b)),U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32.mul(a,b)) == Nat.mul(U32.to_nat(a),U32.to_nat(b)) : Nat}:
149 %Equal.sym(U32,U32.mul(a,b),U32.from_nat(Nat.mul(U32.to_nat(a),U32.to_nat(b))),native_multiply(a,b)) : {U32.to_nat(_) == Nat.mul(U32.to_nat(a),
150 U32.to_nat(b)) : Nat}
151 Bounds.roundtrip(Nat.mul(U32.to_nat(a),U32.to_nat(b)),cap,cap_ok,h)