proofs/row_major_index.bend
stelliferous@0.0.3.0 · 204 lines · 0 definitions
1# Mixed-radix NCHW indexing and its required bounds, on unbounded Nat.
2import Base
3import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
4import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
5import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
6import stelliferous@0.0.3.0/proofs/nat_division.bend as Division
7import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
8import stelliferous@0.0.3.0/proofs/boolean_logic.bend as Boolean
9
10def 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
15def 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
21def 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
29def 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
36def 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
41def 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
54def 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
59def 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
69def 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
79def 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
87def 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
100def 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
107def 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
118def 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
122def 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
127def 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
138def 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
146def 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
154def 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
157def 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
163def 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
169law 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}
180def 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
185def 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
198def 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))