1	# Mixed-radix NCHW indexing and its required bounds, on unbounded Nat.
2	import Base
3	import ./nat_order.bend as Order
4	import ./nat_to_u32_bounds.bend as Bounds
5	import ./natural_addition.bend as Addition
6	import ./nat_division.bend as Division
7	import ./word_encoding.bend as WordEncoding
8	import ./boolean_logic.bend as Boolean
9	
10	def multiply_zero_right(+value: Nat) -> {Nat.mul(value,0n) == 0n : Nat}:
11	  match value:
12	    case 0n: {==}
13	    case 1n+rest: multiply_zero_right(rest)
14	
15	def add_swap(+a: Nat,+b: Nat,+tail: Nat) -> {Nat.add(a,Nat.add(b,tail)) == Nat.add(b,Nat.add(a,tail)) : Nat}:
16	  Equal.trans(Nat,Nat.add(a,Nat.add(b,tail)),Nat.add(Nat.add(a,b),tail),Nat.add(b,Nat.add(a,tail)),
17	    Equal.sym(Nat,Nat.add(Nat.add(a,b),tail),Nat.add(a,Nat.add(b,tail)),Addition.associative(a,b,tail)),
18	    Equal.trans(Nat,Nat.add(Nat.add(a,b),tail),Nat.add(Nat.add(b,a),tail),Nat.add(b,Nat.add(a,tail)),
19	      Equal.cong(Nat,Nat,n => Nat.add(n,tail),Nat.add(a,b),Nat.add(b,a),Order.commutative(a,b)),Addition.associative(b,a,tail)))
20	
21	def multiply_successor_right(+a: Nat,+b: Nat) -> {Nat.mul(a,1n+b) == Nat.add(a,Nat.mul(a,b)) : Nat}:
22	  match a:
23	    case 0n: {==}
24	    case 1n+ +rest:
25	      %Equal.sym(Nat,Nat.mul(rest,1n+b),Nat.add(rest,Nat.mul(rest,b)),multiply_successor_right(rest,b)) :
26	        {1n+Nat.add(b,_) == 1n+Nat.add(rest,Nat.add(b,Nat.mul(rest,b))) : Nat}
27	      Equal.cong(Nat,Nat,n => 1n+n,Nat.add(b,Nat.add(rest,Nat.mul(rest,b))),Nat.add(rest,Nat.add(b,Nat.mul(rest,b))),add_swap(b,rest,Nat.mul(rest,b)))
28	
29	def multiply_commutative(+a: Nat,+b: Nat) -> {Nat.mul(a,b) == Nat.mul(b,a) : Nat}:
30	  match a:
31	    case 0n: Equal.sym(Nat,Nat.mul(b,0n),0n,multiply_zero_right(b))
32	    case 1n+ +rest:
33	      %Equal.sym(Nat,Nat.mul(b,1n+rest),Nat.add(b,Nat.mul(b,rest)),multiply_successor_right(b,rest)) : {Nat.add(b,Nat.mul(rest,b)) == _ : Nat}
34	      Equal.cong(Nat,Nat,n => Nat.add(b,n),Nat.mul(rest,b),Nat.mul(b,rest),multiply_commutative(rest,b))
35	
36	def subtract_common_prefix(+prefix: Nat,+a: Nat,+b: Nat) -> {Nat.sub(Nat.add(prefix,a),Nat.add(prefix,b)) == Nat.sub(a,b) : Nat}:
37	  match prefix:
38	    case 0n: {==}
39	    case 1n+rest: subtract_common_prefix(rest,a,b)
40	
41	def subtract_products(+a: Nat,+b: Nat,+factor: Nat) -> {Nat.sub(Nat.mul(a,factor),Nat.mul(b,factor)) == Nat.mul(Nat.sub(a,b),factor) : Nat}:
42	  match a b:
43	    case 0n 0n: {==}
44	    case 0n 1n+b: Order.zero_subtract(Nat.mul(1n+b,factor))
45	    case 1n+ +a 0n:
46	      %Equal.sym(Nat,Nat.sub(1n+a,0n),1n+a,Order.subtract_zero(1n+a)) :
47	        {Nat.sub(Nat.mul(1n+a,factor),0n) == Nat.mul(_,factor) : Nat}
48	      Order.subtract_zero(Nat.mul(1n+a,factor))
49	    case 1n+ +a 1n+ +b:
50	      %Equal.sym(Nat,Nat.sub(Nat.add(factor,Nat.mul(a,factor)),Nat.add(factor,Nat.mul(b,factor))),Nat.sub(Nat.mul(a,factor),Nat.mul(b,factor)),
51	        subtract_common_prefix(factor,Nat.mul(a,factor),Nat.mul(b,factor))) : {_ == Nat.mul(Nat.sub(a,b),factor) : Nat}
52	      subtract_products(a,b,factor)
53	
54	def left_factor_positive(+left: Nat,+right: Nat,positive: {Nat.is_lt(0n,Nat.mul(left,right)) == True{} : Bool}) -> {Nat.is_lt(0n,left) == True{} : Bool}:
55	  match left:
56	    case 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
57	    case 1n+rest: {==}
58	
59	def distrib(+a: Nat,+b: Nat,+c: Nat) -> {Nat.mul(Nat.add(a,b),c) == Nat.add(Nat.mul(a,c),Nat.mul(b,c)) : Nat}:
60	  match a:
61	    case 0n:
62	      {==}
63	    case 1n+ +p:
64	      %Equal.sym(Nat,Nat.add(Nat.add(c,Nat.mul(p,c)),Nat.mul(b,c)),Nat.add(c,Nat.add(Nat.mul(p,c),Nat.mul(b,c))),Addition.associative(c,
65	          Nat.mul(p,c),Nat.mul(b,c))) : {Nat.add(c,Nat.mul(Nat.add(p,b),c)) == _ : Nat}
66	      %distrib(p,b,c) : {Nat.add(c,Nat.mul(Nat.add(p,b),c)) == Nat.add(c,_) : Nat}
67	      {==}
68	
69	def assoc(+a: Nat,+b: Nat,+c: Nat) -> {Nat.mul(Nat.mul(a,b),c) == Nat.mul(a,Nat.mul(b,c)) : Nat}:
70	  match a:
71	    case 0n:
72	      {==}
73	    case 1n+ +p:
74	      %Equal.sym(Nat,Nat.mul(Nat.add(b,Nat.mul(p,b)),c),Nat.add(Nat.mul(b,c),Nat.mul(Nat.mul(p,b),c)),distrib(b,Nat.mul(p,b),
75	          c)) : {_ == Nat.add(Nat.mul(b,c),Nat.mul(p,Nat.mul(b,c))) : Nat}
76	      %assoc(p,b,c) : {Nat.add(Nat.mul(b,c),Nat.mul(Nat.mul(p,b),c)) == Nat.add(Nat.mul(b,c),_) : Nat}
77	      {==}
78	
79	def right_distrib(+factor: Nat,+left: Nat,+right: Nat) ->
80	  {Nat.mul(factor,Nat.add(left,right)) == Nat.add(Nat.mul(factor,left),Nat.mul(factor,right)) : Nat}:
81	  %Equal.sym(Nat,Nat.mul(factor,Nat.add(left,right)),Nat.mul(Nat.add(left,right),factor),multiply_commutative(factor,Nat.add(left,right))) :
82	    {_ == Nat.add(Nat.mul(factor,left),Nat.mul(factor,right)) : Nat}
83	  %multiply_commutative(left,factor) : {Nat.mul(Nat.add(left,right),factor) == Nat.add(_,Nat.mul(factor,right)) : Nat}
84	  %multiply_commutative(right,factor) : {Nat.mul(Nat.add(left,right),factor) == Nat.add(Nat.mul(left,factor),_) : Nat}
85	  distrib(left,right,factor)
86	
87	def mul_le(+a: Nat,+b: Nat,+c: Nat,h: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(Nat.mul(a,c),Nat.mul(b,c)) == True{} : Bool}:
88	  match a b:
89	    case 0n 0n:
90	      {==}
91	    case 0n 1n+b:
92	      Order.zero_le(Nat.mul(1n+b,c))
93	    case 1n+a 0n:
94	      Empty.absurd({Nat.is_le(Nat.mul(1n+a,c),0n) == True{} : Bool},WordEncoding.false_true(h))
95	    case 1n+ +a 1n+ +b:
96	      %Order.commutative(Nat.mul(a,c),c) : {Nat.is_le(_,Nat.add(c,Nat.mul(b,c))) == True{} : Bool}
97	      %Order.commutative(Nat.mul(b,c),c) : {Nat.is_le(Nat.add(Nat.mul(a,c),c),_) == True{} : Bool}
98	      Order.add_le(Nat.mul(a,c),Nat.mul(b,c),c,mul_le(a,b,c,h))
99	
100	def radix(+a: Nat,+limit: Nat,+b: Nat,+width: Nat,ab: {Nat.is_lt(a,limit) == True{} : Bool},bw: {Nat.is_lt(b,
101	      width) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.mul(a,width),b),Nat.mul(limit,width)) == True{} : Bool}:
102	  Bounds.nat_trans(Nat.add(Nat.mul(a,width),b),Nat.mul(1n+a,width),Nat.mul(limit,width),
103	    %Order.commutative(b,Nat.mul(a,width)) : {Nat.is_lt(_,Nat.add(width,Nat.mul(a,width))) == True{} : Bool}
104	    Order.add_lt(b,width,Nat.mul(a,width),bw),
105	    mul_le(1n+a,limit,width,Order.strict_follow(a,limit,ab)))
106	
107	def cancel_multiply_lt(+left: Nat,+right: Nat,+factor: Nat,ordered: {Nat.is_lt(Nat.mul(left,factor),Nat.mul(right,factor)) == True{} : Bool}) ->
108	  {Nat.is_lt(left,right) == True{} : Bool}:
109	  match left right:
110	    case 0n 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(ordered))
111	    case 0n 1n+right: {==}
112	    case 1n+ +left 0n:
113	      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(Nat.mul(1n+left,factor),0n),True{},
114	        Equal.sym(Bool,Nat.is_lt(Nat.mul(1n+left,factor),0n),False{},Division.lt_zero(Nat.mul(1n+left,factor))),ordered)))
115	    case 1n+ +left 1n+ +right:
116	      cancel_multiply_lt(left,right,factor,Order.cancel_offset_lt(factor,Nat.mul(left,factor),Nat.mul(right,factor),ordered))
117	
118	def row_inside(+row: Nat,+rows: Nat,+width: Nat,+column: Nat,inside: {Nat.is_lt(Nat.add(Nat.mul(row,width),column),Nat.mul(rows,width)) == True{} : Bool}) ->
119	  {Nat.is_lt(row,rows) == True{} : Bool}:
120	  cancel_multiply_lt(row,rows,width,Order.le_lt_trans(Nat.mul(row,width),Nat.add(Nat.mul(row,width),column),Nat.mul(rows,width),Order.le_add(Nat.mul(row,width),column),inside))
121	
122	def multiply_lt(+left: Nat,+right: Nat,+factor: Nat,ordered: {Nat.is_lt(left,right) == True{} : Bool},positive: {Nat.is_lt(0n,factor) == True{} : Bool}) ->
123	  {Nat.is_lt(Nat.mul(left,factor),Nat.mul(right,factor)) == True{} : Bool}:
124	  %Addition.zero_right(Nat.mul(left,factor)) : {Nat.is_lt(_,Nat.mul(right,factor)) == True{} : Bool}
125	  radix(left,right,0n,factor,ordered,positive)
126	
127	def cancel_multiply_le(+left: Nat,+right: Nat,+factor: Nat,+positive: {Nat.is_lt(0n,factor) == True{} : Bool},
128	  ordered: {Nat.is_le(Nat.mul(left,factor),Nat.mul(right,factor)) == True{} : Bool}) -> {Nat.is_le(left,right) == True{} : Bool}:
129	  match left right:
130	    case 0n right: Order.zero_le(right)
131	    case 1n+ +left 0n:
132	      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(
133	        %Order.zero_below(Nat.mul(1n+left,factor),ordered) : {Nat.is_lt(0n,_) == True{} : Bool}
134	        Order.product_positive(1n+left,factor,{==},positive)))
135	    case 1n+ +left 1n+ +right:
136	      cancel_multiply_le(left,right,factor,positive,Order.cancel_offset_le(factor,Nat.mul(left,factor),Nat.mul(right,factor),ordered))
137	
138	def same_remainder_le(+left: Nat,+right: Nat,+factor: Nat,+remainder: Nat,+positive: {Nat.is_lt(0n,factor) == True{} : Bool}) ->
139	  {Nat.is_le(Nat.add(Nat.mul(left,factor),remainder),Nat.add(Nat.mul(right,factor),remainder)) == Nat.is_le(left,right) : Bool}:
140	  Boolean.equivalent(Nat.is_le(Nat.add(Nat.mul(left,factor),remainder),Nat.add(Nat.mul(right,factor),remainder)),Nat.is_le(left,right),
141	    ordered => cancel_multiply_le(left,right,factor,positive,Order.cancel_offset_le(remainder,Nat.mul(left,factor),Nat.mul(right,factor),
142	      %Order.commutative(Nat.mul(left,factor),remainder) : {Nat.is_le(_,Nat.add(remainder,Nat.mul(right,factor))) == True{} : Bool}
143	      %Order.commutative(Nat.mul(right,factor),remainder) : {Nat.is_le(Nat.add(Nat.mul(left,factor),remainder),_) == True{} : Bool} ordered)),
144	    ordered => Order.add_le(Nat.mul(left,factor),Nat.mul(right,factor),remainder,mul_le(left,right,factor,ordered)))
145	
146	def same_remainder_lt(+left: Nat,+right: Nat,+factor: Nat,+remainder: Nat,+positive: {Nat.is_lt(0n,factor) == True{} : Bool}) ->
147	  {Nat.is_lt(Nat.add(Nat.mul(left,factor),remainder),Nat.add(Nat.mul(right,factor),remainder)) == Nat.is_lt(left,right) : Bool}:
148	  Boolean.equivalent(Nat.is_lt(Nat.add(Nat.mul(left,factor),remainder),Nat.add(Nat.mul(right,factor),remainder)),Nat.is_lt(left,right),
149	    ordered => cancel_multiply_lt(left,right,factor,Order.cancel_offset_lt(remainder,Nat.mul(left,factor),Nat.mul(right,factor),
150	      %Order.commutative(Nat.mul(left,factor),remainder) : {Nat.is_lt(_,Nat.add(remainder,Nat.mul(right,factor))) == True{} : Bool}
151	      %Order.commutative(Nat.mul(right,factor),remainder) : {Nat.is_lt(Nat.add(Nat.mul(left,factor),remainder),_) == True{} : Bool} ordered)),
152	    ordered => Order.add_lt(Nat.mul(left,factor),Nat.mul(right,factor),remainder,multiply_lt(left,right,factor,ordered,positive)))
153	
154	def index(+input_channel_index: Nat,+height: Nat,+width: Nat,+iy: Nat,+ix: Nat) -> Nat:
155	  Nat.add(Nat.mul(input_channel_index,Nat.mul(height,width)),Nat.add(Nat.mul(iy,width),ix))
156	
157	def expanded(+input_channel_index: Nat,+height: Nat,+width: Nat,+iy: Nat,+ix: Nat) -> {Nat.add(Nat.add(Nat.mul(Nat.mul(input_channel_index,height),width),Nat.mul(iy,width)),
158	    ix) == index(input_channel_index,height,width,iy,ix) : Nat}:
159	  %assoc(input_channel_index,height,width) : {Nat.add(Nat.add(Nat.mul(Nat.mul(input_channel_index,height),width),Nat.mul(iy,width)),ix) == Nat.add(_,Nat.add(Nat.mul(iy,width),
160	        ix)) : Nat}
161	  Addition.associative(Nat.mul(Nat.mul(input_channel_index,height),width),Nat.mul(iy,width),ix)
162	
163	def mixed(+input_channel_index: Nat,+height: Nat,+width: Nat,+iy: Nat,+ix: Nat) -> {Nat.add(Nat.mul(Nat.add(Nat.mul(input_channel_index,height),iy),width),ix) == index(input_channel_index,height,
164	    width,iy,ix) : Nat}:
165	  %Equal.sym(Nat,Nat.mul(Nat.add(Nat.mul(input_channel_index,height),iy),width),Nat.add(Nat.mul(Nat.mul(input_channel_index,height),width),Nat.mul(iy,width)),distrib(Nat.mul(input_channel_index,
166	        height),iy,width)) : {Nat.add(_,ix) == index(input_channel_index,height,width,iy,ix) : Nat}
167	  expanded(input_channel_index,height,width,iy,ix)
168	
169	law in_bounds:
170	  for +input_channel_index: Nat
171	  for +input_channel_count: Nat
172	  for +height: Nat
173	  for +width: Nat
174	  for +iy: Nat
175	  for +ix: Nat
176	  for channel: {Nat.is_lt(input_channel_index,input_channel_count) == True{} : Bool}
177	  for row: {Nat.is_lt(iy,height) == True{} : Bool}
178	  for col: {Nat.is_lt(ix,width) == True{} : Bool}
179	  {Nat.is_lt(index(input_channel_index,height,width,iy,ix),Nat.mul(input_channel_count,Nat.mul(height,width))) == True{} : Bool}
180	def in_bounds(input_channel_index,input_channel_count,height,width,iy,ix,channel,row,col):
181	  %mixed(input_channel_index,height,width,iy,ix) : {Nat.is_lt(_,Nat.mul(input_channel_count,Nat.mul(height,width))) == True{} : Bool}
182	  %assoc(input_channel_count,height,width) : {Nat.is_lt(Nat.add(Nat.mul(Nat.add(Nat.mul(input_channel_index,height),iy),width),ix),_) == True{} : Bool}
183	  radix(Nat.add(Nat.mul(input_channel_index,height),iy),Nat.mul(input_channel_count,height),ix,width,radix(input_channel_index,input_channel_count,iy,height,channel,row),col)
184	
185	def product_covers(+a: Nat,+b: Nat,positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.is_le(a,Nat.mul(a,b)) == True{} : Bool}:
186	  match a b:
187	    case 0n 0n:
188	      {==}
189	    case 0n 1n+b:
190	      {==}
191	    case 1n+a 0n:
192	      Empty.absurd({Nat.is_le(1n+a,Nat.mul(1n+a,0n)) == True{} : Bool},WordEncoding.false_true(positive))
193	    case 1n+ +a 1n+ +b:
194	      Order.transitive(a,Nat.mul(a,1n+b),Nat.add(b,Nat.mul(a,1n+b)),product_covers(a,1n+b,{==}),
195	        %Order.commutative(Nat.mul(a,1n+b),b) : {Nat.is_le(Nat.mul(a,1n+b),_) == True{} : Bool}
196	        Order.le_add(Nat.mul(a,1n+b),b))
197	
198	def row_product(+input_channel_index: Nat,+input_channel_count: Nat,+height: Nat,+width: Nat,+cap: Nat,channel: {Nat.is_lt(input_channel_index,input_channel_count) == True{} : Bool},positive: {Nat.is_lt(0n,
199	      width) == True{} : Bool},bound: {Nat.is_le(Nat.mul(input_channel_count,Nat.mul(height,width)),cap) == True{} : Bool}) -> {Nat.is_le(Nat.mul(input_channel_index,height),
200	    cap) == True{} : Bool}:
201	  Order.transitive(Nat.mul(input_channel_index,height),Nat.mul(input_channel_count,height),cap,mul_le(input_channel_index,input_channel_count,height,Bounds.strict_le(input_channel_index,input_channel_count,channel)),
202	    Order.transitive(Nat.mul(input_channel_count,height),Nat.mul(input_channel_count,Nat.mul(height,width)),cap,
203	      %assoc(input_channel_count,height,width) : {Nat.is_le(Nat.mul(input_channel_count,height),_) == True{} : Bool}
204	      product_covers(Nat.mul(input_channel_count,height),width,positive),bound))