1	# Power-of-two capacities and masks, by bit-width induction.
2	import Base
3	import ./word_encoding.bend as WordEncoding
4	import ./word_arithmetic.bend as WordArithmetic
5	
6	def power(+width: Nat,depth: Nat) -> Word(width):
7	  match width:
8	    case 0n:
9	      WNil{}
10	    case 1n+rest:
11	      match depth:
12	        case 0n:
13	          WCon{True{},Word.zero(rest)}
14	        case 1n+previous:
15	          WCon{False{},power(rest,previous)}
16	
17	def mask(+width: Nat,depth: Nat) -> Word(width):
18	  match width:
19	    case 0n:
20	      WNil{}
21	    case 1n+rest:
22	      match depth:
23	        case 0n:
24	          Word.zero(1n+rest)
25	        case 1n+previous:
26	          WCon{True{},mask(rest,previous)}
27	
28	law put_into_zero:
29	  for +width: Nat
30	  for +bit: Bool
31	  {Word.shl.put(width,bit,Word.zero(width)) == Bool.pick(Word(width),bit,power(width,0n),Word.zero(width)) : Word(width)}
32	
33	def put_into_zero(width,bit):
34	  match width:
35	    case 0n:
36	      match bit:
37	        case False{}: {==}
38	        case True{}: {==}
39	    case 1n+ +rest:
40	      match bit:
41	        case False{}:
42	          %put_into_zero(rest,False{}) : {WCon{False{},Word.shl.put(rest,False{},Word.zero(rest))} == WCon{False{},_} : Word(1n+rest)}
43	          {==}
44	        case True{}:
45	          %put_into_zero(rest,False{}) : {WCon{True{},Word.shl.put(rest,False{},Word.zero(rest))} == WCon{True{},_} : Word(1n+rest)}
46	          {==}
47	
48	law shift_power:
49	  for +width: Nat
50	  for +depth: Nat
51	  {Word.shl(width,power(width,depth)) == power(width,1n+depth) : Word(width)}
52	
53	def shift_power(width,depth):
54	  match width:
55	    case 0n: {==}
56	    case 1n+ +rest:
57	      match depth:
58	        case 0n:
59	          %put_into_zero(rest,True{}) : {WCon{False{},Word.shl.put(rest,True{},Word.zero(rest))} == WCon{False{},_} : Word(1n+rest)}
60	          {==}
61	        case 1n+ +previous:
62	          %shift_power(rest,previous) : {WCon{False{},Word.shl.put(rest,False{},power(rest,previous))} == WCon{False{},_} : Word(1n+rest)}
63	          Equal.cong(Word(rest),Word(1n+rest),w => WCon{False{},w},Word.shl.put(rest,False{},power(rest,previous)),Word.shl(rest,power(rest,
64	                previous)),Equal.sym(Word(rest),Word.shl(rest,power(rest,previous)),Word.shl.put(rest,False{},power(rest,previous)),
65	              WordArithmetic.shift_put(rest,power(rest,previous))))
66	
67	law native_power:
68	  for +depth: Nat
69	  {U32.shln(1,depth) == U32{power(32n,depth)} : U32}
70	
71	def native_power(depth):
72	  match depth:
73	    case 0n: {==}
74	    case 1n+ +previous:
75	      %Equal.sym(U32,U32.shln(1,previous),U32{power(32n,previous)},native_power(previous)) : {U32.shl(_) == U32{power(32n,1n+previous)} : U32}
76	      Equal.cong(Word(32n),U32,w => U32{w},Word.shl(32n,power(32n,previous)),power(32n,1n+previous),shift_power(32n,previous))
77	
78	law subtract_one:
79	  for +width: Nat
80	  for +word: Word(width)
81	  {Word.sub(width,word,power(width,0n)) == Word.adc(width,word,Word.zero(width),True{},False{}) : Word(width)}
82	
83	def subtract_one(width,word):
84	  match width:
85	    case 0n: {==}
86	    case 1n+rest:
87	      match word:
88	        case WCon{False{},tail}: {==}
89	        case WCon{True{},tail}: {==}
90	
91	law zero_subtract_zero:
92	  for +width: Nat
93	  {Word.adc(width,Word.zero(width),Word.zero(width),True{},True{}) == Word.zero(width) : Word(width)}
94	
95	def zero_subtract_zero(width):
96	  match width:
97	    case 0n: {==}
98	    case 1n+ +rest:
99	      %zero_subtract_zero(rest) : {WCon{False{},Word.adc(rest,Word.zero(rest),Word.zero(rest),True{},True{})} == WCon{False{},_} : Word(1n+rest)}
100	      {==}
101	
102	law decrement_power:
103	  for +width: Nat
104	  for +depth: Nat
105	  {Word.adc(width,power(width,depth),Word.zero(width),True{},False{}) == mask(width,depth) : Word(width)}
106	
107	def decrement_power(width,depth):
108	  match width:
109	    case 0n: {==}
110	    case 1n+ +rest:
111	      match depth:
112	        case 0n:
113	          %zero_subtract_zero(rest) : {WCon{False{},Word.adc(rest,Word.zero(rest),Word.zero(rest),True{},True{})} == WCon{False{},_} : Word(1n+rest)}
114	          {==}
115	        case 1n+ +previous:
116	          %decrement_power(rest,previous) : {WCon{True{},Word.adc(rest,power(rest,previous),Word.zero(rest),True{},False{})} == WCon{True{},
117	              _} : Word(1n+rest)}
118	          {==}
119	
120	law mask_preserves_bounded:
121	  for +width: Nat
122	  for +depth: Nat
123	  for +word: Word(width)
124	  for bound: {Cmp.is_lt(Word.cmp(width,word,power(width,depth))) == True{} : Bool}
125	  {Word.and(width,word,mask(width,depth)) == word : Word(width)}
126	
127	def mask_preserves_bounded(width,depth,word,bound):
128	  match width:
129	    case 0n:
130	      match word:
131	        case WNil{}: {==}
132	    case 1n+ +rest:
133	      match depth:
134	        case 0n:
135	          %Equal.sym(Word(1n+rest),word,Word.zero(1n+rest),WordEncoding.below_one_zero(rest,word,bound)) : {Word.and(1n+rest,_,
136	              Word.zero(1n+rest)) == _ : Word(1n+rest)}
137	          WordEncoding.and_zero(1n+rest,Word.zero(1n+rest))
138	        case 1n+ +previous:
139	          match word:
140	            case WCon{False{},+tail}:
141	              %mask_preserves_bounded(rest,previous,tail,Equal.trans(Bool,Cmp.is_lt(Word.cmp(rest,tail,power(rest,previous))),
142	                  Cmp.is_lt(Word.cmp.fin(False{},False{},Word.cmp(rest,tail,power(rest,previous)))),True{},Equal.sym(Bool,
143	                    Cmp.is_lt(Word.cmp.fin(False{},False{},Word.cmp(rest,tail,power(rest,previous)))),Cmp.is_lt(Word.cmp(rest,tail,power(rest,
144	                      previous))),WordEncoding.finish_lt_zero(False{},Word.cmp(rest,tail,power(rest,previous)))),bound)) : {WCon{False{},
145	                  Word.and(rest,tail,mask(rest,previous))} == WCon{False{},_} : Word(1n+rest)}
146	              {==}
147	            case WCon{True{},+tail}:
148	              %mask_preserves_bounded(rest,previous,tail,Equal.trans(Bool,Cmp.is_lt(Word.cmp(rest,tail,power(rest,previous))),
149	                  Cmp.is_lt(Word.cmp.fin(True{},False{},Word.cmp(rest,tail,power(rest,previous)))),True{},Equal.sym(Bool,
150	                    Cmp.is_lt(Word.cmp.fin(True{},False{},Word.cmp(rest,tail,power(rest,previous)))),Cmp.is_lt(Word.cmp(rest,tail,power(rest,
151	                      previous))),WordEncoding.finish_lt_zero(True{},Word.cmp(rest,tail,power(rest,previous)))),bound)) : {WCon{True{},
152	                  Word.and(rest,tail,mask(rest,previous))} == WCon{True{},_} : Word(1n+rest)}
153	              {==}
154	
155	def native_word_mask(+depth: Nat,+word: Word(32n),bound: {Cmp.is_lt(Word.cmp(32n,word,power(32n,
156	        depth))) == True{} : Bool}) -> {U32.and(U32{word},U32.sub(U32{power(32n,depth)},1)) == U32{word} : U32}:
157	  %Equal.sym(Word(32n),Word.sub(32n,power(32n,depth),power(32n,0n)),mask(32n,depth),Equal.trans(Word(32n),Word.sub(32n,power(32n,depth),
158	        power(32n,0n)),Word.adc(32n,power(32n,depth),Word.zero(32n),True{},False{}),mask(32n,depth),subtract_one(32n,power(32n,depth)),
159	      decrement_power(32n,depth))) : {U32{Word.and(32n,word,_)} == U32{word} : U32}
160	  Equal.cong(Word(32n),U32,w => U32{w},Word.and(32n,word,mask(32n,depth)),word,mask_preserves_bounded(32n,depth,word,bound))
161	
162	law native_mask_preserves_bounded:
163	  for +depth: Nat
164	  for +index: U32
165	  {U32.is_lt(index,U32.shln(1,depth)) == True{} : Bool} -> {U32.and(index,U32.sub(U32.shln(1,depth),1)) == index : U32}
166	
167	def native_mask_preserves_bounded(depth,index):
168	  match index:
169	    case U32{+word}:
170	      %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.is_lt(U32{word},
171	          _) == True{} : Bool} -> {U32.and(U32{word},U32.sub(_,1)) == U32{word} : U32}
172	      bound => native_word_mask(depth,word,bound)
173	
174	law compare_zero:
175	  for +width: Nat
176	  {Word.cmp(width,Word.zero(width),Word.zero(width)) == EQ{} : Cmp}
177	
178	def compare_zero(width):
179	  match width:
180	    case 0n: {==}
181	    case 1n+ +rest:
182	      %compare_zero(rest) : {Word.cmp.fin(False{},False{},Word.cmp(rest,Word.zero(rest),Word.zero(rest))) == Word.cmp.fin(False{},False{},_) : Cmp}
183	      {==}
184	
185	law positive_power:
186	  for +width: Nat
187	  for +depth: Nat
188	  for fits: {Nat.is_lt(depth,width) == True{} : Bool}
189	  {Word.cmp(width,Word.zero(width),power(width,depth)) == LT{} : Cmp}
190	
191	def positive_power(width,depth,fits):
192	  match width:
193	    case 0n:
194	      match depth:
195	        case 0n: Empty.absurd({Word.cmp(0n,WNil{},power(0n,0n)) == LT{} : Cmp},WordEncoding.false_true(fits))
196	        case 1n+rest: Empty.absurd({Word.cmp(0n,WNil{},power(0n,1n+rest)) == LT{} : Cmp},WordEncoding.false_true(fits))
197	    case 1n+ +rest:
198	      match depth:
199	        case 0n:
200	          %compare_zero(rest) : {Word.cmp.fin(False{},True{},Word.cmp(rest,Word.zero(rest),Word.zero(rest))) == Word.cmp.fin(False{},True{},_) : Cmp}
201	          {==}
202	        case 1n+ +previous:
203	          %positive_power(rest,previous,fits) : {Word.cmp.fin(False{},False{},Word.cmp(rest,Word.zero(rest),power(rest,
204	                  previous))) == Word.cmp.fin(False{},False{},_) : Cmp}
205	          {==}
206	
207	law compare_equal_low_bits:
208	  for +comparison: Cmp
209	  {Word.cmp.fin(False{},False{},comparison) == comparison : Cmp}
210	
211	def compare_equal_low_bits(comparison):
212	  match comparison:
213	    case LT{}: {==}
214	    case EQ{}: {==}
215	    case GT{}: {==}
216	
217	law power_monotone:
218	  for +width: Nat
219	  for +lower: Nat
220	  for +upper: Nat
221	  for fits: {Nat.is_lt(upper,width) == True{} : Bool}
222	  for ordered: {Nat.is_le(lower,upper) == True{} : Bool}
223	  {Cmp.is_le(Word.cmp(width,power(width,lower),power(width,upper))) == True{} : Bool}
224	
225	def power_monotone(width,lower,upper,fits,ordered):
226	  match width:
227	    case 0n: {==}
228	    case 1n+ +rest:
229	      match lower upper:
230	        case 0n 0n:
231	          %compare_zero(rest) : {Cmp.is_le(Word.cmp.fin(True{},True{},Word.cmp(rest,Word.zero(rest),
232	                  Word.zero(rest)))) == Cmp.is_le(Word.cmp.fin(True{},True{},_)) : Bool}
233	          {==}
234	        case 0n 1n+ +previous:
235	          %positive_power(rest,previous,fits) : {Cmp.is_le(Word.cmp.fin(True{},False{},Word.cmp(rest,Word.zero(rest),power(rest,
236	                  previous)))) == Cmp.is_le(Word.cmp.fin(True{},False{},_)) : Bool}
237	          {==}
238	        case 1n+previous 0n:
239	          Empty.absurd({Cmp.is_le(Word.cmp(1n+rest,power(1n+rest,1n+previous),power(1n+rest,0n))) == True{} : Bool},WordEncoding.false_true(ordered))
240	        case 1n+ +low 1n+ +high:
241	          %Equal.sym(Cmp,Word.cmp.fin(False{},False{},Word.cmp(rest,power(rest,low),power(rest,high))),Word.cmp(rest,power(rest,low),power(rest,
242	                high)),compare_equal_low_bits(Word.cmp(rest,power(rest,low),power(rest,high)))) : {Cmp.is_le(_) == True{} : Bool}
243	          power_monotone(rest,low,high,fits,ordered)
244	
245	law power_value:
246	  for +width: Nat
247	  for +depth: Nat
248	  for fits: {Nat.is_lt(depth,width) == True{} : Bool}
249	  {Word.to_nat(width,power(width,depth)) == WordEncoding.shift(depth,1n) : Nat}
250	
251	def power_value(width,depth,fits):
252	  match width:
253	    case 0n:
254	      match depth:
255	        case 0n: Empty.absurd({0n == WordEncoding.shift(0n,1n) : Nat},WordEncoding.false_true(fits))
256	        case 1n+rest: Empty.absurd({0n == WordEncoding.shift(1n+rest,1n) : Nat},WordEncoding.false_true(fits))
257	    case 1n+ +rest:
258	      match depth:
259	        case 0n:
260	          %WordEncoding.zero_nat(rest) : {1n+Nat.double(Word.to_nat(rest,Word.zero(rest))) == 1n+Nat.double(_) : Nat}
261	          {==}
262	        case 1n+ +previous:
263	          %power_value(rest,previous,fits) : {Nat.double(Word.to_nat(rest,power(rest,previous))) == Nat.double(_) : Nat}
264	          {==}
265	
266	law pad_zero:
267	  for +width: Nat
268	  {Word.shr.pad(width,Word.zero(width)) == Word.zero(1n+width) : Word(1n+width)}
269	
270	def pad_zero(width):
271	  match width:
272	    case 0n: {==}
273	    case 1n+ +rest:
274	      %pad_zero(rest) : {WCon{False{},Word.shr.pad(rest,Word.zero(rest))} == WCon{False{},_} : Word(2n+rest)}
275	      {==}
276	
277	law pad_power:
278	  for +width: Nat
279	  for +depth: Nat
280	  for fits: {Nat.is_lt(depth,width) == True{} : Bool}
281	  {Word.shr.pad(width,power(width,depth)) == power(1n+width,depth) : Word(1n+width)}
282	
283	def pad_power(width,depth,fits):
284	  match width:
285	    case 0n:
286	      match depth:
287	        case 0n: Empty.absurd({Word.shr.pad(0n,power(0n,0n)) == power(1n,0n) : Word(1n)},WordEncoding.false_true(fits))
288	        case 1n+rest: Empty.absurd({Word.shr.pad(0n,power(0n,1n+rest)) == power(1n,1n+rest) : Word(1n)},WordEncoding.false_true(fits))
289	    case 1n+ +rest:
290	      match depth:
291	        case 0n:
292	          %pad_zero(rest) : {WCon{True{},Word.shr.pad(rest,Word.zero(rest))} == WCon{True{},_} : Word(2n+rest)}
293	          {==}
294	        case 1n+ +previous:
295	          %pad_power(rest,previous,fits) : {WCon{False{},Word.shr.pad(rest,power(rest,previous))} == WCon{False{},_} : Word(2n+rest)}
296	          {==}
297	
298	law native_half_power:
299	  for +depth: Nat
300	  for fits: {Nat.is_lt(depth,31n) == True{} : Bool}
301	  {U32.shr(U32.shln(1,1n+depth)) == U32.shln(1,depth) : U32}
302	
303	def native_half_power(depth,fits):
304	  %Equal.sym(U32,U32.shln(1,1n+depth),U32{power(32n,1n+depth)},native_power(1n+depth)) : {U32.shr(_) == U32.shln(1,depth) : U32}
305	  %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.shr(U32{power(32n,1n+depth)}) == _ : U32}
306	  Equal.cong(Word(32n),U32,w => U32{w},Word.shr.pad(31n,power(31n,depth)),power(32n,depth),pad_power(31n,depth,fits))
307	
308	law native_power_bound:
309	  for +depth: Nat
310	  for bound: {Nat.is_le(depth,31n) == True{} : Bool}
311	  {U32.is_le(U32.shln(1,depth),2147483648) == True{} : Bool}
312	
313	def native_power_bound(depth,bound):
314	  %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.is_le(_,2147483648) == True{} : Bool}
315	  power_monotone(32n,depth,31n,{==},bound)
316	
317	def native_allocatable(+depth: Nat,bound: {Nat.is_le(depth,30n) == True{} : Bool}) ->
318	  {U32.is_le(U32.shln(1,depth),1073741824) == True{} : Bool}:
319	  %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.is_le(_,1073741824) == True{} : Bool}
320	  power_monotone(32n,depth,30n,{==},bound)
321	
322	def positive_double(value: Nat,positive: {Nat.is_lt(0n,Nat.double(value)) == True{} : Bool}) -> {Nat.is_lt(0n,value) == True{} : Bool}:
323	  match value:
324	    case 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
325	    case 1n+rest: {==}
326	
327	# A nonempty checked owner cannot have a power-of-two capacity truncated to
328	# zero. This recovers the full machine-depth bound from its existing guard.
329	def nonempty_power_depth(+width: Nat,+depth: Nat,positive: {Nat.is_lt(0n,Word.to_nat(width,power(width,depth))) == True{} : Bool}) ->
330	  {Nat.is_lt(depth,width) == True{} : Bool}:
331	  match width:
332	    case 0n: Empty.absurd({Nat.is_lt(depth,0n) == True{} : Bool},WordEncoding.false_true(positive))
333	    case 1n+ +rest:
334	      match depth:
335	        case 0n: {==}
336	        case 1n+ +previous:
337	          nonempty_power_depth(rest,previous,positive_double(Word.to_nat(rest,power(rest,previous)),positive))
338	
339	def native_nonempty_depth(+depth: Nat,positive: {Nat.is_lt(0n,U32.to_nat(U32.shln(1,depth))) == True{} : Bool}) ->
340	  {Nat.is_lt(depth,32n) == True{} : Bool}:
341	  nonempty_power_depth(32n,depth,
342	    %native_power(depth) : {Nat.is_lt(0n,U32.to_nat(_)) == True{} : Bool} positive)