1	# Machine operations -> unbounded Nat, with explicit no-overflow obligations.
2	import Base
3	import ./word_arithmetic.bend as WordArithmetic
4	import ./word_multiplication.bend as Multiplication
5	import ./word_subtraction.bend as Subtraction
6	import ./nat_to_u32_bounds.bend as Bounds
7	import ./natural_addition.bend as Addition
8	import ./nat_order.bend as Order
9	import ./u32_comparison.bend as Comparison
10	import ./row_major_index.bend as RowMajor
11	
12	def 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	
19	def 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	
27	def 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	
32	def 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	
37	def 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	
46	def 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	
49	def 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.
53	def 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	
64	def 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	
70	def 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	
75	def 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	
79	def 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	
86	def 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	
101	def 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	
114	def 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	
120	def 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	
126	def 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	
133	def 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	
146	def 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	
151	def 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	
155	def 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.
161	def 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	
172	def 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	
179	def 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	
184	def 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	
189	def 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.
196	def 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)))
200	def 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	
205	def 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	
212	def 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	
216	def 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	
221	def 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.
228	def 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.
248	def 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)))
265	def 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)))