proofs/bounded_u32_arithmetic.bend
stelliferous@0.0.3.0 · 281 lines · 0 definitions
1# Machine operations -> unbounded Nat, with explicit no-overflow obligations.
2import Base
3import stelliferous@0.0.3.0/proofs/word_arithmetic.bend as WordArithmetic
4import stelliferous@0.0.3.0/proofs/word_multiplication.bend as Multiplication
5import stelliferous@0.0.3.0/proofs/word_subtraction.bend as Subtraction
6import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
7import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
8import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
9import stelliferous@0.0.3.0/proofs/u32_comparison.bend as Comparison
10import stelliferous@0.0.3.0/proofs/row_major_index.bend as RowMajor
11
12def count_within(+count: U32,+length: Nat,+capacity: U32,+upper: U32,exact: {U32.to_nat(count) == length : Nat},
13 room: {Nat.is_le(length,U32.to_nat(capacity)) == True{} : Bool},capacity_bound: {U32.is_le(capacity,upper) == True{} : Bool}) ->
14 {U32.is_le(count,upper) == True{} : Bool}:
15 %Equal.sym(Bool,U32.is_le(count,upper),Nat.is_le(U32.to_nat(count),U32.to_nat(upper)),Comparison.le(count,upper)) : {_ == True{} : Bool}
16 %Equal.sym(Nat,U32.to_nat(count),length,exact) : {Nat.is_le(_,U32.to_nat(upper)) == True{} : Bool}
17 Order.transitive(length,U32.to_nat(capacity),U32.to_nat(upper),room,Bounds.as_nat_le(capacity,upper,capacity_bound))
18
19def native_roundtrip(+a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
20 match a:
21 case U32{+w}:
22 %Equal.sym(U32,U32.from_nat(Word.to_nat(32n,w)),U32{WordArithmetic.encode(Word.to_nat(32n,w),32n)},
23 WordArithmetic.native_encoding(Word.to_nat(32n,w))) : {_ == U32{w} : U32}
24 %Equal.sym(Word(32n),WordArithmetic.encode(Word.to_nat(32n,w),32n),w,Multiplication.word_roundtrip(32n,w)) : {U32{_} == U32{w} : U32}
25 {==}
26
27def native_add(+a: U32,+b: U32) -> {U32.add(a,b) == U32.from_nat(Nat.add(U32.to_nat(a),U32.to_nat(b))) : U32}:
28 %native_roundtrip(a) : {U32.add(_,b) == U32.from_nat(Nat.add(U32.to_nat(a),U32.to_nat(b))) : U32}
29 %native_roundtrip(b) : {U32.add(U32.from_nat(U32.to_nat(a)),_) == U32.from_nat(Nat.add(U32.to_nat(a),U32.to_nat(b))) : U32}
30 WordArithmetic.native_add(U32.to_nat(a),U32.to_nat(b))
31
32def add_zero(+value: U32) -> {(value + 0 : U32) == value : U32}:
33 %native_roundtrip(value) : {(value + 0 : U32) == _ : U32}
34 %Addition.zero_right(U32.to_nat(value)) : {(value + 0 : U32) == U32.from_nat(_) : U32}
35 native_add(value,0)
36
37def add_commutative(+left: U32,+right: U32) -> {(left + right : U32) == (right + left : U32) : U32}:
38 %Equal.sym(U32,(left + right : U32),U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))),native_add(left,right)) :
39 {_ == (right + left : U32) : U32}
40 %Equal.sym(U32,(right + left : U32),U32.from_nat(Nat.add(U32.to_nat(right),U32.to_nat(left))),native_add(right,left)) :
41 {U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))) == _ : U32}
42 %Order.commutative(U32.to_nat(left),U32.to_nat(right)) :
43 {U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))) == U32.from_nat(_) : U32}
44 {==}
45
46def add_zero_left(+value: U32) -> {(0 + value : U32) == value : U32}:
47 Equal.trans(U32,(0 + value : U32),(value + 0 : U32),value,add_commutative(0,value),add_zero(value))
48
49def multiply_zero_left(+value: U32) -> {(0 * value : U32) == 0 : U32}:
50 Multiplication.native_multiply(0,value)
51
52# These are modular identities, so they require no no-overflow assumption.
53def encoded_add_associative(+a: Nat,+b: Nat,+c: Nat) ->
54 {((U32.from_nat(a) + U32.from_nat(b) : U32) + U32.from_nat(c) : U32) == (U32.from_nat(a) + (U32.from_nat(b) + U32.from_nat(c) : U32) : U32) : U32}:
55 %Equal.sym(U32,(U32.from_nat(a) + U32.from_nat(b) : U32),U32.from_nat(Nat.add(a,b)),WordArithmetic.native_add(a,b)) :
56 {(_ + U32.from_nat(c) : U32) == (U32.from_nat(a) + (U32.from_nat(b) + U32.from_nat(c) : U32) : U32) : U32}
57 %Equal.sym(U32,(U32.from_nat(Nat.add(a,b)) + U32.from_nat(c) : U32),U32.from_nat(Nat.add(Nat.add(a,b),c)),WordArithmetic.native_add(Nat.add(a,b),c)) :
58 {_ == (U32.from_nat(a) + (U32.from_nat(b) + U32.from_nat(c) : U32) : U32) : U32}
59 %Equal.sym(U32,(U32.from_nat(b) + U32.from_nat(c) : U32),U32.from_nat(Nat.add(b,c)),WordArithmetic.native_add(b,c)) : {U32.from_nat(Nat.add(Nat.add(a,b),c)) == (U32.from_nat(a) + _ : U32) : U32}
60 %Equal.sym(U32,(U32.from_nat(a) + U32.from_nat(Nat.add(b,c)) : U32),U32.from_nat(Nat.add(a,Nat.add(b,c))),WordArithmetic.native_add(a,Nat.add(b,c))) : {U32.from_nat(Nat.add(Nat.add(a,b),c)) == _ : U32}
61 %Addition.associative(a,b,c) : {U32.from_nat(Nat.add(Nat.add(a,b),c)) == U32.from_nat(_) : U32}
62 {==}
63
64def add_associative(+a: U32,+b: U32,+c: U32) -> {((a + b : U32) + c : U32) == (a + (b + c : U32) : U32) : U32}:
65 %native_roundtrip(a) : {((_ + b : U32) + c : U32) == (_ + (b + c : U32) : U32) : U32}
66 %native_roundtrip(b) : {((U32.from_nat(U32.to_nat(a)) + _ : U32) + c : U32) == (U32.from_nat(U32.to_nat(a)) + (_ + c : U32) : U32) : U32}
67 %native_roundtrip(c) : {((U32.from_nat(U32.to_nat(a)) + U32.from_nat(U32.to_nat(b)) : U32) + _ : U32) == (U32.from_nat(U32.to_nat(a)) + (U32.from_nat(U32.to_nat(b)) + _ : U32) : U32) : U32}
68 encoded_add_associative(U32.to_nat(a),U32.to_nat(b),U32.to_nat(c))
69
70def subtract_from_sum(+a: U32,+b: U32,+c: U32) -> {((a + b : U32) - c : U32) == (a + (b - c : U32) : U32) : U32}:
71 %Subtraction.add_subtract(b,c) : {((a + _ : U32) - c : U32) == (a + (b - c : U32) : U32) : U32}
72 %add_associative(a,(b - c : U32),c) : {(_ - c : U32) == (a + (b - c : U32) : U32) : U32}
73 Subtraction.subtract_add((a + (b - c : U32) : U32),c)
74
75def subtract_first(+a: U32,+b: U32) -> {((a + b : U32) - a : U32) == b : U32}:
76 %add_commutative(b,a) : {(_ - a : U32) == b : U32}
77 Subtraction.subtract_add(b,a)
78
79def add_after_subtract(+value: U32,+padding: U32,+offset: U32) ->
80 {((value - padding : U32) + offset : U32) == ((value + offset : U32) - padding : U32) : U32}:
81 %Equal.sym(U32,((value - padding : U32) + offset : U32),(offset + (value - padding : U32) : U32),add_commutative((value - padding : U32),offset)) :
82 {_ == ((value + offset : U32) - padding : U32) : U32}
83 %add_commutative(offset,value) : {(offset + (value - padding : U32) : U32) == (_ - padding : U32) : U32}
84 Equal.sym(U32,((offset + value : U32) - padding : U32),(offset + (value - padding : U32) : U32),subtract_from_sum(offset,value,padding))
85
86def subtract_sum(+value: U32,+left: U32,+right: U32) ->
87 {((value - left : U32) - right : U32) == (value - (left + right : U32) : U32) : U32}:
88 +rest = ((value - left : U32) - right : U32)
89 +sum = (left + right : U32)
90 +restored = Equal.trans(U32,(rest + sum : U32),(rest + (right + left : U32) : U32),value,
91 Equal.cong(U32,U32,sum => (rest + sum : U32),sum,(right + left : U32),add_commutative(left,right)),
92 Equal.trans(U32,(rest + (right + left : U32) : U32),((rest + right : U32) + left : U32),value,
93 Equal.sym(U32,((rest + right : U32) + left : U32),(rest + (right + left : U32) : U32),add_associative(rest,right,left)),
94 Equal.trans(U32,((rest + right : U32) + left : U32),((value - left : U32) + left : U32),value,
95 Equal.cong(U32,U32,rest => (rest + left : U32),(rest + right : U32),(value - left : U32),Subtraction.add_subtract((value - left : U32),right)),
96 Subtraction.add_subtract(value,left))))
97 Equal.trans(U32,rest,((rest + sum : U32) - sum : U32),(value - sum : U32),
98 Equal.sym(U32,((rest + sum : U32) - sum : U32),rest,Subtraction.subtract_add(rest,sum)),
99 Equal.cong(U32,U32,value => (value - sum : U32),(rest + sum : U32),value,restored))
100
101def subtract_difference(+value: U32,+tap: U32,+offset: U32) ->
102 {((value - tap : U32) + offset : U32) == (value - (tap - offset : U32) : U32) : U32}:
103 +result = ((value - tap : U32) + offset : U32)
104 +difference = (tap - offset : U32)
105 +restored = Equal.trans(U32,(result + difference : U32),((value - tap : U32) + (offset + difference : U32) : U32),value,
106 add_associative((value - tap : U32),offset,difference),
107 Equal.trans(U32,((value - tap : U32) + (offset + difference : U32) : U32),((value - tap : U32) + tap : U32),value,
108 Equal.cong(U32,U32,tail => ((value - tap : U32) + tail : U32),(offset + difference : U32),tap,
109 Equal.trans(U32,(offset + difference : U32),(difference + offset : U32),tap,add_commutative(offset,difference),Subtraction.add_subtract(tap,offset))),Subtraction.add_subtract(value,tap)))
110 Equal.trans(U32,result,((result + difference : U32) - difference : U32),(value - difference : U32),
111 Equal.sym(U32,((result + difference : U32) - difference : U32),result,Subtraction.subtract_add(result,difference)),
112 Equal.cong(U32,U32,value => (value - difference : U32),(result + difference : U32),value,restored))
113
114def native_subtract(+a: U32,+b: U32,h: {Nat.is_le(U32.to_nat(b),U32.to_nat(a)) == True{} : Bool}) -> {U32.sub(a,
115 b) == U32.from_nat(Nat.sub(U32.to_nat(a),U32.to_nat(b))) : U32}:
116 %native_roundtrip(a) : {U32.sub(_,b) == U32.from_nat(Nat.sub(U32.to_nat(a),U32.to_nat(b))) : U32}
117 %native_roundtrip(b) : {U32.sub(U32.from_nat(U32.to_nat(a)),_) == U32.from_nat(Nat.sub(U32.to_nat(a),U32.to_nat(b))) : U32}
118 Subtraction.encoded_subtract(U32.to_nat(a),U32.to_nat(b),h)
119
120def add(+a: U32,+b: U32,+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},h: {Nat.is_le(Nat.add(U32.to_nat(a),U32.to_nat(b)),
121 U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32.add(a,b)) == Nat.add(U32.to_nat(a),U32.to_nat(b)) : Nat}:
122 %Equal.sym(U32,U32.add(a,b),U32.from_nat(Nat.add(U32.to_nat(a),U32.to_nat(b))),native_add(a,b)) : {U32.to_nat(_) == Nat.add(U32.to_nat(a),
123 U32.to_nat(b)) : Nat}
124 Bounds.roundtrip(Nat.add(U32.to_nat(a),U32.to_nat(b)),cap,cap_ok,h)
125
126def subtract(+a: U32,+b: U32,+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},ordered: {Nat.is_le(U32.to_nat(b),
127 U32.to_nat(a)) == True{} : Bool},h: {Nat.is_le(Nat.sub(U32.to_nat(a),U32.to_nat(b)),
128 U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32.sub(a,b)) == Nat.sub(U32.to_nat(a),U32.to_nat(b)) : Nat}:
129 %Equal.sym(U32,U32.sub(a,b),U32.from_nat(Nat.sub(U32.to_nat(a),U32.to_nat(b))),native_subtract(a,b,
130 ordered)) : {U32.to_nat(_) == Nat.sub(U32.to_nat(a),U32.to_nat(b)) : Nat}
131 Bounds.roundtrip(Nat.sub(U32.to_nat(a),U32.to_nat(b)),cap,cap_ok,h)
132
133def remove_prefix(+value: U32,+base: U32,+local: Nat,+capacity: U32,capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
134 +exact: {U32.to_nat(value) == Nat.add(U32.to_nat(base),local) : Nat},room: {Nat.is_le(U32.to_nat(value),U32.to_nat(capacity)) == True{} : Bool}) ->
135 {U32.to_nat((value - base : U32)) == local : Nat}:
136 +local_room = Order.transitive(local,Nat.add(U32.to_nat(base),local),U32.to_nat(capacity),
137 %Order.commutative(local,U32.to_nat(base)) : {Nat.is_le(local,_) == True{} : Bool} Order.le_add(local,U32.to_nat(base)),
138 %exact : {Nat.is_le(_,U32.to_nat(capacity)) == True{} : Bool} room)
139 Equal.trans(Nat,U32.to_nat((value - base : U32)),Nat.sub(U32.to_nat(value),U32.to_nat(base)),local,
140 subtract(value,base,capacity,capacity_ok,
141 %Equal.sym(Nat,U32.to_nat(value),Nat.add(U32.to_nat(base),local),exact) : {Nat.is_le(U32.to_nat(base),_) == True{} : Bool} Order.le_add(U32.to_nat(base),local),
142 %Equal.sym(Nat,U32.to_nat(value),Nat.add(U32.to_nat(base),local),exact) : {Nat.is_le(Nat.sub(_,U32.to_nat(base)),U32.to_nat(capacity)) == True{} : Bool}
143 %Equal.sym(Nat,Nat.sub(Nat.add(U32.to_nat(base),local),U32.to_nat(base)),local,Order.subtract_shift(U32.to_nat(base),local)) : {Nat.is_le(_,U32.to_nat(capacity)) == True{} : Bool} local_room),
144 %Equal.sym(Nat,U32.to_nat(value),Nat.add(U32.to_nat(base),local),exact) : {Nat.sub(_,U32.to_nat(base)) == local : Nat} Order.subtract_shift(U32.to_nat(base),local))
145
146def subtract_zero(+value: U32) -> {(value - 0 : U32) == value : U32}:
147 Equal.trans(U32,(value - 0 : U32),U32.from_nat(Nat.sub(U32.to_nat(value),0n)),value,native_subtract(value,0,Order.zero_le(U32.to_nat(value))),
148 Equal.trans(U32,U32.from_nat(Nat.sub(U32.to_nat(value),0n)),U32.from_nat(U32.to_nat(value)),value,
149 Equal.cong(Nat,U32,U32.from_nat,Nat.sub(U32.to_nat(value),0n),U32.to_nat(value),Order.subtract_zero(U32.to_nat(value))),native_roundtrip(value)))
150
151def 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),U32.to_nat(b)),
152 U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32.mul(a,b)) == Nat.mul(U32.to_nat(a),U32.to_nat(b)) : Nat}:
153 Multiplication.bounded_multiply(a,b,cap,cap_ok,h)
154
155def from_nat_exact(+count: U32,+length: Nat,exact: {U32.to_nat(count) == length : Nat}) -> {U32.from_nat(length) == count : U32}:
156 %exact : {U32.from_nat(_) == count : U32}
157 native_roundtrip(count)
158
159# Each mixed-radix step is exact when its complete result fits. The product
160# bound is derived here, rather than assumed for an intermediate machine word.
161def multiply_add_exact(+a: U32,+radix: U32,+rest: U32,+capacity: U32,+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
162 +room: {Nat.is_le(Nat.add(Nat.mul(U32.to_nat(a),U32.to_nat(radix)),U32.to_nat(rest)),U32.to_nat(capacity)) == True{} : Bool}) ->
163 {U32.to_nat((a * radix + rest : U32)) == Nat.add(Nat.mul(U32.to_nat(a),U32.to_nat(radix)),U32.to_nat(rest)) : Nat}:
164 +product = Nat.mul(U32.to_nat(a),U32.to_nat(radix))
165 +exact = multiply(a,radix,capacity,capacity_ok,
166 Order.transitive(product,Nat.add(product,U32.to_nat(rest)),U32.to_nat(capacity),Order.le_add(product,U32.to_nat(rest)),room))
167 %exact : {U32.to_nat((a * radix + rest : U32)) == Nat.add(_,U32.to_nat(rest)) : Nat}
168 add((a * radix : U32),rest,capacity,capacity_ok,
169 %Equal.sym(Nat,U32.to_nat((a * radix : U32)),product,exact) : {Nat.is_le(Nat.add(_,U32.to_nat(rest)),U32.to_nat(capacity)) == True{} : Bool}
170 room)
171
172def equal_of_is_eq(+left: U32,+right: U32,equal: {U32.is_eq(left,right) == True{} : Bool}) -> {left == right : U32}:
173 %native_roundtrip(left) : {_ == right : U32}
174 %native_roundtrip(right) : {U32.from_nat(U32.to_nat(left)) == _ : U32}
175 Equal.cong(Nat,U32,value => U32.from_nat(value),U32.to_nat(left),U32.to_nat(right),Order.equal_of_is_eq(U32.to_nat(left),U32.to_nat(right),{
176 %Comparison.eq(left,right) : {_ == True{} : Bool}
177 equal : {Nat.is_eq(U32.to_nat(left),U32.to_nat(right)) == True{} : Bool}}))
178
179def to_nat_injective(+left: U32,+right: U32,equal: {U32.to_nat(left) == U32.to_nat(right) : Nat}) -> {left == right : U32}:
180 %native_roundtrip(left) : {_ == right : U32}
181 %native_roundtrip(right) : {U32.from_nat(U32.to_nat(left)) == _ : U32}
182 Equal.cong(Nat,U32,value => U32.from_nat(value),U32.to_nat(left),U32.to_nat(right),equal)
183
184def word_zero(+value: U32,zero: {U32.is_zero(value) == True{} : Bool}) -> {value == 0 : U32}:
185 to_nat_injective(value,0,Order.equal_of_is_eq(U32.to_nat(value),0n,{
186 %Comparison.eq(value,0) : {_ == True{} : Bool}
187 zero : {Nat.is_eq(U32.to_nat(value),0n) == True{} : Bool}}))
188
189def word_nonzero_positive(+extent: U32,nonzero: {U32.is_zero(extent) == False{} : Bool}) -> {Nat.is_lt(0n,U32.to_nat(extent)) == True{} : Bool}:
190 Order.nonzero_positive(U32.to_nat(extent),{
191 %Comparison.eq(extent,0) : {_ == False{} : Bool}
192 nonzero : {Nat.is_eq(U32.to_nat(extent),0n) == False{} : Bool}})
193
194# Zero channels, rows or width make the actual modular local count zero.
195# These producers need no positive-width or whole-tensor indexing envelope.
196def multiply_one(+word: U32) -> {(word * 1 : U32) == word : U32}:
197 Equal.trans(U32,(word * 1 : U32),U32.from_nat(Nat.mul(U32.to_nat(word),1n)),word,Multiplication.native_multiply(word,1),
198 Equal.trans(U32,U32.from_nat(Nat.mul(U32.to_nat(word),1n)),U32.from_nat(U32.to_nat(word)),word,
199 Equal.cong(Nat,U32,U32.from_nat,Nat.mul(U32.to_nat(word),1n),U32.to_nat(word),Order.times_one(U32.to_nat(word))),native_roundtrip(word)))
200def multiply_zero_right(+value: U32) -> {(value * 0 : U32) == 0 : U32}:
201 Equal.trans(U32,(value * 0 : U32),U32.from_nat(Nat.mul(U32.to_nat(value),0n)),0,
202 Multiplication.native_multiply(value,0),
203 Equal.cong(Nat,U32,U32.from_nat,Nat.mul(U32.to_nat(value),0n),0n,RowMajor.multiply_zero_right(U32.to_nat(value))))
204
205def multiply_commutative(+left: U32,+right: U32) -> {(left * right : U32) == (right * left : U32) : U32}:
206 Equal.trans(U32,(left * right : U32),U32.from_nat(Nat.mul(U32.to_nat(left),U32.to_nat(right))),(right * left : U32),
207 Multiplication.native_multiply(left,right),
208 Equal.trans(U32,U32.from_nat(Nat.mul(U32.to_nat(left),U32.to_nat(right))),U32.from_nat(Nat.mul(U32.to_nat(right),U32.to_nat(left))),(right * left : U32),
209 Equal.cong(Nat,U32,value => U32.from_nat(value),Nat.mul(U32.to_nat(left),U32.to_nat(right)),Nat.mul(U32.to_nat(right),U32.to_nat(left)),RowMajor.multiply_commutative(U32.to_nat(left),U32.to_nat(right))),
210 Equal.sym(U32,(right * left : U32),U32.from_nat(Nat.mul(U32.to_nat(right),U32.to_nat(left))),Multiplication.native_multiply(right,left))))
211
212def equal_reflexive(+word: U32) -> {U32.is_eq(word,word) == True{} : Bool}:
213 %Equal.sym(Bool,U32.is_eq(word,word),Nat.is_eq(U32.to_nat(word),U32.to_nat(word)),Comparison.eq(word,word)) : {_ == True{} : Bool}
214 Order.equal_reflexive(U32.to_nat(word))
215
216def add_zero_subtract(+value: U32,+padding: U32) -> {(value + (0 - padding : U32) : U32) == (value - padding : U32) : U32}:
217 Equal.trans(U32,(value + (0 - padding : U32) : U32),((value + 0 : U32) - padding : U32),(value - padding : U32),
218 Equal.sym(U32,((value + 0 : U32) - padding : U32),(value + (0 - padding : U32) : U32),subtract_from_sum(value,0,padding)),
219 Equal.cong(U32,U32,n => (n - padding : U32),(value + 0 : U32),value,add_zero(value)))
220
221def negate_twice(+value: U32) -> {(0 - (0 - value : U32) : U32) == value : U32}:
222 +zero = Equal.trans(U32,(value + (0 - value : U32) : U32),((0 - value : U32) + value : U32),0,
223 add_commutative(value,(0 - value : U32)),Subtraction.add_subtract(0,value))
224 %zero : {(_ - (0 - value : U32) : U32) == value : U32}
225 Subtraction.subtract_add(value,(0 - value : U32))
226
227# A modular channel counter advances both its tile and source-plane strides.
228def multiply_successor(+index: U32,+stride: U32) ->
229 {((index + 1 : U32) * stride : U32) == (index * stride + stride : U32) : U32}:
230 +a = U32.to_nat(index)
231 +b = U32.to_nat(stride)
232 +left = {
233 %native_roundtrip(index) : {(_ + 1 : U32) == U32.from_nat(1n+a) : U32}
234 %Equal.sym(U32,(U32.from_nat(a) + 1 : U32),(1 + U32.from_nat(a) : U32),add_commutative(U32.from_nat(a),1)) : {_ == U32.from_nat(1n+a) : U32}
235 WordArithmetic.native_add(1n,a) : {(index + 1 : U32) == U32.from_nat(1n+a) : U32}}
236 +right = Equal.trans(U32,(index * stride + stride : U32),(U32.from_nat(Nat.mul(a,b)) + stride : U32),U32.from_nat(Nat.add(Nat.mul(a,b),b)),
237 Equal.cong(U32,U32,value => (value + stride : U32),(index * stride : U32),U32.from_nat(Nat.mul(a,b)),Multiplication.native_multiply(index,stride)),
238 %native_roundtrip(stride) : {(U32.from_nat(Nat.mul(a,b)) + _ : U32) == U32.from_nat(Nat.add(Nat.mul(a,b),b)) : U32}
239 WordArithmetic.native_add(Nat.mul(a,b),b))
240 %Equal.sym(U32,(index * stride + stride : U32),U32.from_nat(Nat.add(Nat.mul(a,b),b)),right) :
241 {((index + 1 : U32) * stride : U32) == _ : U32}
242 %Order.commutative(b,Nat.mul(a,b)) : {((index + 1 : U32) * stride : U32) == U32.from_nat(_) : U32}
243 %Equal.sym(U32,(index + 1 : U32),U32.from_nat(1n+a),left) : {(_ * stride : U32) == U32.from_nat(Nat.mul(1n+a,b)) : U32}
244 %native_roundtrip(stride) : {(U32.from_nat(1n+a) * _ : U32) == U32.from_nat(Nat.mul(1n+a,b)) : U32}
245 Multiplication.native_encoded_multiply(1n+a,b)
246
247# Modular products preserve natural distributivity and associativity.
248def multiply_additive(+left: U32,+right: U32,+factor: U32) ->
249 {((left + right : U32) * factor : U32) == (left * factor + right * factor : U32) : U32}:
250 +a = U32.to_nat(left)
251 +b = U32.to_nat(right)
252 +c = U32.to_nat(factor)
253 +sum = Nat.add(a,b)
254 +products = Nat.add(Nat.mul(a,c),Nat.mul(b,c))
255 +left_exact = {
256 %Equal.sym(U32,(left + right : U32),U32.from_nat(sum),native_add(left,right)) : {(_ * factor : U32) == U32.from_nat(Nat.mul(sum,c)) : U32}
257 %native_roundtrip(factor) : {(U32.from_nat(sum) * _ : U32) == U32.from_nat(Nat.mul(sum,c)) : U32}
258 Multiplication.native_encoded_multiply(sum,c) : {((left + right : U32) * factor : U32) == U32.from_nat(Nat.mul(sum,c)) : U32}}
259 +right_exact = {
260 %Equal.sym(U32,(left * factor : U32),U32.from_nat(Nat.mul(a,c)),Multiplication.native_multiply(left,factor)) : {(_ + right * factor : U32) == U32.from_nat(products) : U32}
261 %Equal.sym(U32,(right * factor : U32),U32.from_nat(Nat.mul(b,c)),Multiplication.native_multiply(right,factor)) : {(U32.from_nat(Nat.mul(a,c)) + _ : U32) == U32.from_nat(products) : U32}
262 WordArithmetic.native_add(Nat.mul(a,c),Nat.mul(b,c)) : {(left * factor + right * factor : U32) == U32.from_nat(products) : U32}}
263 Equal.trans(U32,((left + right : U32) * factor : U32),U32.from_nat(Nat.mul(sum,c)),(left * factor + right * factor : U32),left_exact,
264 Equal.trans(U32,U32.from_nat(Nat.mul(sum,c)),U32.from_nat(products),(left * factor + right * factor : U32),Equal.cong(Nat,U32,U32.from_nat,Nat.mul(sum,c),products,RowMajor.distrib(a,b,c)),Equal.sym(U32,(left * factor + right * factor : U32),U32.from_nat(products),right_exact)))
265def multiply_associative(+left: U32,+middle: U32,+right: U32) ->
266 {(left * middle * right : U32) == (left * (middle * right : U32) : U32) : U32}:
267 +a = U32.to_nat(left)
268 +b = U32.to_nat(middle)
269 +c = U32.to_nat(right)
270 +first = Nat.mul(Nat.mul(a,b),c)
271 +last = Nat.mul(a,Nat.mul(b,c))
272 +left_exact = {
273 %Equal.sym(U32,(left * middle : U32),U32.from_nat(Nat.mul(a,b)),Multiplication.native_multiply(left,middle)) : {(_ * right : U32) == U32.from_nat(first) : U32}
274 %native_roundtrip(right) : {(U32.from_nat(Nat.mul(a,b)) * _ : U32) == U32.from_nat(first) : U32}
275 Multiplication.native_encoded_multiply(Nat.mul(a,b),c) : {(left * middle * right : U32) == U32.from_nat(first) : U32}}
276 +right_exact = {
277 %native_roundtrip(left) : {(_ * (middle * right : U32) : U32) == U32.from_nat(last) : U32}
278 %Equal.sym(U32,(middle * right : U32),U32.from_nat(Nat.mul(b,c)),Multiplication.native_multiply(middle,right)) : {(U32.from_nat(a) * _ : U32) == U32.from_nat(last) : U32}
279 Multiplication.native_encoded_multiply(a,Nat.mul(b,c)) : {(left * (middle * right : U32) : U32) == U32.from_nat(last) : U32}}
280 Equal.trans(U32,(left * middle * right : U32),U32.from_nat(first),(left * (middle * right : U32) : U32),left_exact,
281 Equal.trans(U32,U32.from_nat(first),U32.from_nat(last),(left * (middle * right : U32) : U32),Equal.cong(Nat,U32,U32.from_nat,first,last,RowMajor.assoc(a,b,c)),Equal.sym(U32,(left * (middle * right : U32) : U32),U32.from_nat(last),right_exact)))