proofs/word_multiplication.bend
stelliferous@0.0.3.0 · 199 lines · 0 definitions
1import Base
2import stelliferous@0.0.3.0/proofs/row_major_index.bend as RowMajor
3import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
4import stelliferous@0.0.3.0/proofs/word_arithmetic.bend as WordArithmetic
5import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
6
7def truncate(n: Nat,w: Word(1n+n)) -> Word(n):
8 match n:
9 case 0n:
10 WNil{}
11 case 1n+p:
12 WCon{b,t} = w
13 WCon{b,truncate(p,t)}
14
15def truncate_zero(+n: Nat) -> {truncate(n,Word.zero(1n+n)) == Word.zero(n) : Word(n)}:
16 match n:
17 case 0n:
18 {==}
19 case 1n+ +p:
20 %truncate_zero(p) : {WCon{False{},truncate(p,Word.zero(1n+p))} == WCon{False{},_} : Word(1n+p)}
21 {==}
22
23def truncate_inc(+n: Nat,+w: Word(1n+n)) -> {truncate(n,Word.inc(1n+n,w)) == Word.inc(n,truncate(n,w)) : Word(n)}:
24 match n:
25 case 0n:
26 {==}
27 case 1n+ +p:
28 match w:
29 case WCon{False{},t}:
30 {==}
31 case WCon{True{},+t}:
32 %truncate_inc(p,t) : {WCon{False{},truncate(p,Word.inc(1n+p,t))} == WCon{False{},_} : Word(1n+p)}
33 {==}
34
35def truncate_encode(+a: Nat,+n: Nat) -> {truncate(n,WordArithmetic.encode(a,1n+n)) == WordArithmetic.encode(a,n) : Word(n)}:
36 match a:
37 case 0n:
38 truncate_zero(n)
39 case 1n+ +p:
40 %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))),
41 truncate_inc(n,WordArithmetic.encode(p,1n+n))) : {_ == Word.inc(n,WordArithmetic.encode(p,n)) : Word(n)}
42 %truncate_encode(p,n) : {Word.inc(n,truncate(n,WordArithmetic.encode(p,1n+n))) == Word.inc(n,_) : Word(n)}
43 {==}
44
45def put(+n: Nat,+b: Bool,+w: Word(n)) -> {Word.shl.put(n,b,w) == truncate(n,WCon{b,w}) : Word(n)}:
46 match n:
47 case 0n:
48 {==}
49 case 1n+ +p:
50 WCon{+c,+t} = w
51 %put(p,c,t) : {WCon{b,Word.shl.put(p,c,t)} == WCon{b,_} : Word(1n+p)}
52 {==}
53
54def shift(+n: Nat,+w: Word(1n+n)) -> {Word.shl(1n+n,w) == WCon{False{},truncate(n,w)} : Word(1n+n)}:
55 WCon{+b,+t} = w
56 %put(n,b,t) : {WCon{False{},Word.shl.put(n,b,t)} == WCon{False{},_} : Word(1n+n)}
57 {==}
58
59def encoded_double(+a: Nat,+n: Nat) -> {WordArithmetic.encode(Nat.double(a),1n+n) == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}:
60 %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,
61 1n+n)) : {_ == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}
62 %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,
63 WordArithmetic.encode(a,1n+n))) : {_ == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}
64 %truncate_encode(a,n) : {WCon{False{},truncate(n,WordArithmetic.encode(a,1n+n))} == WCon{False{},_} : Word(1n+n)}
65 {==}
66
67law word_roundtrip:
68 for +n: Nat
69 for +w: Word(n)
70 {WordArithmetic.encode(Word.to_nat(n,w),n) == w : Word(n)}
71def word_roundtrip(n,w):
72 match n:
73 case 0n:
74 WNil{} = w
75 {==}
76 case 1n+ +p:
77 match w:
78 case WCon{False{},+t}:
79 %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)},
80 encoded_double(Word.to_nat(p,t),p)) : {_ == WCon{False{},t} : Word(1n+p)}
81 %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)}
82 {==}
83 case WCon{True{},+t}:
84 %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)},
85 encoded_double(Word.to_nat(p,t),p)) : {Word.inc(1n+p,_) == WCon{True{},t} : Word(1n+p)}
86 %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)}
87 {==}
88
89def double_mul(+a: Nat,+b: Nat) -> {Nat.mul(Nat.double(a),b) == Nat.mul(a,Nat.double(b)) : Nat}:
90 match a:
91 case 0n:
92 {==}
93 case 1n+ +p:
94 %Addition.double(b) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == Nat.add(_,Nat.mul(p,Nat.double(b))) : Nat}
95 %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,
96 Nat.double(b)))) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == _ : Nat}
97 %double_mul(p,b) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == Nat.add(b,Nat.add(b,_)) : Nat}
98 {==}
99
100law multiply_go:
101 for +m: Nat
102 for +n: Nat
103 for +w: Word(m)
104 for +b: Nat
105 for +acc: Nat
106 {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)),
107 n) : Word(n)}
108def multiply_go(m,n,w,b,acc):
109 match m:
110 case 0n:
111 %Equal.sym(Nat,Nat.add(acc,0n),acc,Addition.zero_right(acc)) : {WordArithmetic.encode(acc,n) == WordArithmetic.encode(_,n) : Word(n)}
112 {==}
113 case 1n+ +p:
114 match w:
115 case WCon{False{},+t}:
116 %WordArithmetic.encode_double(b,n) : {Word.mul.go(n,p,t,_,WordArithmetic.encode(acc,n)) == WordArithmetic.encode(Nat.add(acc,
117 Nat.mul(Nat.double(Word.to_nat(p,t)),b)),n) : Word(n)}
118 %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),
119 b)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),WordArithmetic.encode(acc,n)) == WordArithmetic.encode(Nat.add(acc,
120 _),n) : Word(n)}
121 multiply_go(p,n,t,Nat.double(b),acc)
122 case WCon{True{},+t}:
123 %WordArithmetic.encode_double(b,n) : {Word.mul.go(n,p,t,_,Word.add(n,WordArithmetic.encode(acc,n),WordArithmetic.encode(b,
124 n))) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,Nat.mul(Nat.double(Word.to_nat(p,t)),b))),n) : Word(n)}
125 %Equal.sym(Word(n),Word.add(n,WordArithmetic.encode(acc,n),WordArithmetic.encode(b,n)),WordArithmetic.encode(Nat.add(acc,b),n),
126 WordArithmetic.encode_add(acc,b,n)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),
127 _) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,Nat.mul(Nat.double(Word.to_nat(p,t)),b))),n) : Word(n)}
128 %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),
129 b)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),WordArithmetic.encode(Nat.add(acc,b),
130 n)) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,_)),n) : Word(n)}
131 %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),
132 WordArithmetic.encode(Nat.add(acc,b),n)) == WordArithmetic.encode(_,n) : Word(n)}
133 multiply_go(p,n,t,Nat.double(b),Nat.add(acc,b))
134
135def 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)}:
136 %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)}
137 multiply_go(n,n,a,Word.to_nat(n,b),0n)
138
139def native_multiply(+a: U32,+b: U32) -> {U32.mul(a,b) == U32.from_nat(Nat.mul(U32.to_nat(a),U32.to_nat(b))) : U32}:
140 match a b:
141 case U32{+x} U32{+y}:
142 %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),
143 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,
144 y)} == _ : U32}
145 %multiply(32n,x,y) : {U32{Word.mul(32n,x,y)} == U32{_} : U32}
146 {==}
147
148def 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),
149 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}:
150 %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),
151 U32.to_nat(b)) : Nat}
152 Bounds.roundtrip(Nat.mul(U32.to_nat(a),U32.to_nat(b)),cap,cap_ok,h)
153
154# Encoding respects products even when the natural operands exceed a word.
155def encoded_product_roundtrip(+value: Nat,remaining: Nat,+width: Nat) ->
156 {WordArithmetic.encode(Nat.mul(Word.to_nat(width,WordArithmetic.encode(value,width)),remaining),width) == WordArithmetic.encode(Nat.mul(value,remaining),width) : Word(width)}:
157 match remaining:
158 case 0n:
159 Equal.cong(Nat,Word(width),n => WordArithmetic.encode(n,width),Nat.mul(Word.to_nat(width,WordArithmetic.encode(value,width)),0n),Nat.mul(value,0n),
160 Equal.trans(Nat,Nat.mul(Word.to_nat(width,WordArithmetic.encode(value,width)),0n),0n,Nat.mul(value,0n),RowMajor.multiply_zero_right(Word.to_nat(width,WordArithmetic.encode(value,width))),Equal.sym(Nat,Nat.mul(value,0n),0n,RowMajor.multiply_zero_right(value))))
161 case 1n+ +rest:
162 +decoded = Word.to_nat(width,WordArithmetic.encode(value,width))
163 %Equal.sym(Nat,Nat.mul(decoded,1n+rest),Nat.add(decoded,Nat.mul(decoded,rest)),RowMajor.multiply_successor_right(decoded,rest)) :
164 {WordArithmetic.encode(_,width) == WordArithmetic.encode(Nat.mul(value,1n+rest),width) : Word(width)}
165 %Equal.sym(Nat,Nat.mul(value,1n+rest),Nat.add(value,Nat.mul(value,rest)),RowMajor.multiply_successor_right(value,rest)) :
166 {WordArithmetic.encode(Nat.add(decoded,Nat.mul(decoded,rest)),width) == WordArithmetic.encode(_,width) : Word(width)}
167 %WordArithmetic.encode_add(decoded,Nat.mul(decoded,rest),width) :
168 {_ == WordArithmetic.encode(Nat.add(value,Nat.mul(value,rest)),width) : Word(width)}
169 %WordArithmetic.encode_add(value,Nat.mul(value,rest),width) :
170 {Word.add(width,WordArithmetic.encode(decoded,width),WordArithmetic.encode(Nat.mul(decoded,rest),width)) == _ : Word(width)}
171 %Equal.sym(Word(width),WordArithmetic.encode(decoded,width),WordArithmetic.encode(value,width),word_roundtrip(width,WordArithmetic.encode(value,width))) :
172 {Word.add(width,_,WordArithmetic.encode(Nat.mul(decoded,rest),width)) == Word.add(width,WordArithmetic.encode(value,width),WordArithmetic.encode(Nat.mul(value,rest),width)) : Word(width)}
173 %Equal.sym(Word(width),WordArithmetic.encode(Nat.mul(decoded,rest),width),WordArithmetic.encode(Nat.mul(value,rest),width),encoded_product_roundtrip(value,rest,width)) :
174 {Word.add(width,WordArithmetic.encode(value,width),_) == Word.add(width,WordArithmetic.encode(value,width),WordArithmetic.encode(Nat.mul(value,rest),width)) : Word(width)}
175 {==}
176
177def encoded_multiply(+left: Nat,+right: Nat,+width: Nat) ->
178 {Word.mul(width,WordArithmetic.encode(left,width),WordArithmetic.encode(right,width)) == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}:
179 +a = Word.to_nat(width,WordArithmetic.encode(left,width))
180 +b = Word.to_nat(width,WordArithmetic.encode(right,width))
181 %Equal.sym(Word(width),Word.mul(width,WordArithmetic.encode(left,width),WordArithmetic.encode(right,width)),WordArithmetic.encode(Nat.mul(a,b),width),multiply(width,WordArithmetic.encode(left,width),WordArithmetic.encode(right,width))) :
182 {_ == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}
183 %Equal.sym(Word(width),WordArithmetic.encode(Nat.mul(a,b),width),WordArithmetic.encode(Nat.mul(left,b),width),encoded_product_roundtrip(left,b,width)) :
184 {_ == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}
185 %Equal.sym(Nat,Nat.mul(left,b),Nat.mul(b,left),RowMajor.multiply_commutative(left,b)) :
186 {WordArithmetic.encode(_,width) == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}
187 %Equal.sym(Word(width),WordArithmetic.encode(Nat.mul(b,left),width),WordArithmetic.encode(Nat.mul(right,left),width),encoded_product_roundtrip(right,left,width)) :
188 {_ == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}
189 Equal.cong(Nat,Word(width),n => WordArithmetic.encode(n,width),Nat.mul(right,left),Nat.mul(left,right),RowMajor.multiply_commutative(right,left))
190
191def native_encoded_multiply(+left: Nat,+right: Nat) ->
192 {(U32.from_nat(left) * U32.from_nat(right) : U32) == U32.from_nat(Nat.mul(left,right)) : U32}:
193 %Equal.sym(U32,U32.from_nat(left),U32{WordArithmetic.encode(left,32n)},WordArithmetic.native_encoding(left)) :
194 {(_ * U32.from_nat(right) : U32) == U32.from_nat(Nat.mul(left,right)) : U32}
195 %Equal.sym(U32,U32.from_nat(right),U32{WordArithmetic.encode(right,32n)},WordArithmetic.native_encoding(right)) :
196 {(U32{WordArithmetic.encode(left,32n)} * _ : U32) == U32.from_nat(Nat.mul(left,right)) : U32}
197 %Equal.sym(U32,U32.from_nat(Nat.mul(left,right)),U32{WordArithmetic.encode(Nat.mul(left,right),32n)},WordArithmetic.native_encoding(Nat.mul(left,right))) :
198 {U32{Word.mul(32n,WordArithmetic.encode(left,32n),WordArithmetic.encode(right,32n))} == _ : U32}
199 Equal.cong(Word(32n),U32,word => U32{word},Word.mul(32n,WordArithmetic.encode(left,32n),WordArithmetic.encode(right,32n)),WordArithmetic.encode(Nat.mul(left,right),32n),encoded_multiply(left,right,32n))