1module Compiler.NormalizationBudget
2
3import Model.Config
4import Model.Word32
5import Std.Word
6import Std.Natural
7import Compiler.NaturalMagnitude
8import Compiler.IntegerLiteral
9import Data.Bytes
10
11-- Fixed-width work accounting. An exhausted charge preserves the last valid
12-- state; it never wraps, partially charges, or supplies an admissible residual.
13family NormalizationBudget : Type 0
14constructor NormalizationBudgetValue
15field unrestricted normalizationWorkLimit : (family ModelWord32)
16field unrestricted normalizationWorkRemaining : (family ModelWord32)
17field unrestricted normalizationWorkUsed : (family ModelWord32)
18
19end-family
20
21family NormalizationCostResult : Type 0
22constructor NormalizationCostWord
23field unrestricted normalizationCost : (family ModelWord32)
24constructor NormalizationCostTooLarge
25constructor NormalizationCostInvalid
26
27end-family
28
29family NormalizationChargeResult : Type 0
30constructor NormalizationCharged
31field unrestricted normalizationUpdatedBudget : (family NormalizationBudget)
32constructor NormalizationChargeExhausted
33field unrestricted normalizationUnchangedBudget : (family NormalizationBudget)
34field unrestricted normalizationRejectedCharge : (family ModelWord32)
35constructor NormalizationChargeInvalid
36
37end-family
38
39-- Internal payload traversal state. Stopped blocks skip their remaining work.
40family NormalizationPayloadState : Type 0
41constructor NormalizationPayloadActive
42field unrestricted normalizationPayloadRemaining : Bytes
43field unrestricted normalizationPayloadBudget : (family NormalizationBudget)
44constructor NormalizationPayloadStopped
45field unrestricted normalizationPayloadResult : (family NormalizationChargeResult)
46
47end-family
48
49-- Bounded admission for unary metadata operations. The cursor grows only as
50-- far as the available budget; the requested natural is never eliminated.
51family NormalizationNaturalState : Type 0
52constructor NormalizationNaturalActive
53field unrestricted normalizationNaturalCursor : Nat
54field unrestricted normalizationNaturalBudget : (family NormalizationBudget)
55constructor NormalizationNaturalStopped
56field unrestricted normalizationNaturalResult : (family NormalizationChargeResult)
57
58end-family
59
60-- Magnitudes are decimal digits in little-endian order. Conversion visits at
61-- most ten admitted digits, never the represented natural value.
62def normalizationCostDecimalText =
63 (lambda unrestricted digits : Bytes .
64 (bytes-eliminate
65 (lambda unrestricted current : Bytes . Bytes)
66 b""
67 (lambda unrestricted head : Byte .
68 (lambda unrestricted tail : Bytes .
69 (lambda unrestricted induction : Bytes .
70 (bytes-append
71 induction
72 (bytes
73 (nat-to-byte (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat (byte 48)))))))))
74 digits))
75
76def finishNormalizationCostWord =
77 (lambda unrestricted result : (family IntegerLiteralResult) .
78 (eliminate
79 IntegerLiteralResult
80 (lambda unrestricted current : (family IntegerLiteralResult) .
81 (family NormalizationCostResult))
82 result
83 (branch
84 IntegerLiteralWord
85 width
86 sign
87 bytesLE
88 .
89 (eliminate
90 DataBytesWord32ExactDecodeResult
91 (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) .
92 (family NormalizationCostResult))
93 (Std.Word/stdU32DecodeLEExact bytesLE)
94 (branch
95 DataBytesWord32ExactlyDecoded
96 word
97 telemetry
98 .
99 (constructor NormalizationCostResult NormalizationCostWord word))
100 (branch
101 DataBytesWord32ExactDecodeFailed
102 error
103 telemetry
104 .
105 (constructor NormalizationCostResult NormalizationCostInvalid))))
106 (branch
107 IntegerLiteralFailed
108 failure
109 .
110 (eliminate
111 IntegerLiteralFailure
112 (lambda unrestricted current : (family IntegerLiteralFailure) .
113 (family NormalizationCostResult))
114 failure
115 (branch
116 IntegerLiteralMissingDigits
117 .
118 (constructor NormalizationCostResult NormalizationCostInvalid))
119 (branch
120 IntegerLiteralBadDigit
121 .
122 (constructor NormalizationCostResult NormalizationCostInvalid))
123 (branch
124 IntegerLiteralBadSeparator
125 .
126 (constructor NormalizationCostResult NormalizationCostInvalid))
127 (branch
128 IntegerLiteralOutOfRange
129 .
130 (constructor NormalizationCostResult NormalizationCostTooLarge))))))
131
132def normalizationCostFromMagnitude =
133 (lambda unrestricted digits : Bytes .
134 (eliminate
135 NaturalMagnitudeResult
136 (lambda unrestricted current : (family NaturalMagnitudeResult) .
137 (family NormalizationCostResult))
138 (Compiler.NaturalMagnitude/magnitudeDecodeCanonical digits)
139 (branch
140 NaturalMagnitudeAccepted
141 canonical
142 .
143 (app
144 (nat-eliminate
145 (lambda unrestricted tooLong : Nat .
146 (pi unrestricted force : Nat . (family NormalizationCostResult)))
147 (lambda unrestricted force : Nat .
148 (app
149 (nat-eliminate
150 (lambda unrestricted empty : Nat .
151 (pi unrestricted force : Nat . (family NormalizationCostResult)))
152 (lambda unrestricted force : Nat .
153 (finishNormalizationCostWord
154 (Compiler.IntegerLiteral/integerLiteralParse
155 (constructor IntegerLiteralRadix IntegerLiteralDecimal)
156 (constructor IntegerLiteralKind IntegerLiteralUnsigned)
157 (constructor IntegerLiteralSign IntegerLiteralPositive)
158 (constructor IntegerLiteralWidth IntegerLiteralWidth32)
159 (normalizationCostDecimalText canonical))))
160 (lambda unrestricted predecessor : Nat .
161 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationCostResult)) .
162 (lambda unrestricted force : Nat .
163 (constructor
164 NormalizationCostResult
165 NormalizationCostWord
166 Model.Word32/modelWord32Zero))))
167 (bytes-equal canonical b""))
168 zero))
169 (lambda unrestricted predecessor : Nat .
170 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationCostResult)) .
171 (lambda unrestricted force : Nat .
172 (constructor NormalizationCostResult NormalizationCostTooLarge))))
173 (nat-less-than (byte-to-nat (byte 10)) (bytes-length canonical)))
174 zero))
175 (branch
176 NaturalMagnitudeRejected
177 failure
178 .
179 (constructor NormalizationCostResult NormalizationCostInvalid))))
180
181def normalizationBudget =
182 (lambda unrestricted limit : (family ModelWord32) .
183 (constructor
184 NormalizationBudget
185 NormalizationBudgetValue
186 limit
187 limit
188 Model.Word32/modelWord32Zero))
189
190-- Both operands are at most limit. Their sum cannot wrap to limit: that
191-- would require limit + 2^32 <= 2*limit, impossible for a U32 limit.
192def normalizationBudgetValid =
193 (lambda unrestricted budget : (family NormalizationBudget) .
194 (eliminate
195 NormalizationBudget
196 (lambda unrestricted current : (family NormalizationBudget) . Nat)
197 budget
198 (branch
199 NormalizationBudgetValue
200 limit
201 remaining
202 used
203 .
204 (Std.Natural/naturalAnd
205 (Std.Natural/naturalIsZero (Std.Word/stdU32LessThan limit remaining))
206 (Std.Natural/naturalAnd
207 (Std.Natural/naturalIsZero (Std.Word/stdU32LessThan limit used))
208 (bytes-equal
209 (Std.Word/stdU32EncodeLE limit)
210 (Std.Word/stdU32EncodeLE (Std.Word/stdU32AddWrapping remaining used))))))))
211
212def chargeValidNormalizationBudget =
213 (lambda unrestricted amount : (family ModelWord32) .
214 (lambda unrestricted budget : (family NormalizationBudget) .
215 (eliminate
216 NormalizationBudget
217 (lambda unrestricted current : (family NormalizationBudget) .
218 (family NormalizationChargeResult))
219 budget
220 (branch
221 NormalizationBudgetValue
222 limit
223 remaining
224 used
225 .
226 (app
227 (nat-eliminate
228 (lambda unrestricted insufficient : Nat .
229 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
230 (lambda unrestricted force : Nat .
231 (constructor
232 NormalizationChargeResult
233 NormalizationCharged
234 (constructor
235 NormalizationBudget
236 NormalizationBudgetValue
237 limit
238 (Std.Word/stdU32SubtractWrapping remaining amount)
239 (Std.Word/stdU32AddWrapping used amount))))
240 (lambda unrestricted predecessor : Nat .
241 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
242 (lambda unrestricted force : Nat .
243 (constructor
244 NormalizationChargeResult
245 NormalizationChargeExhausted
246 budget
247 amount))))
248 (Std.Word/stdU32LessThan remaining amount))
249 zero)))))
250
251def chargeNormalizationBudgetGeneral =
252 (lambda unrestricted amount : (family ModelWord32) .
253 (lambda unrestricted budget : (family NormalizationBudget) .
254 (app
255 (nat-eliminate
256 (lambda unrestricted valid : Nat .
257 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
258 (lambda unrestricted force : Nat .
259 (constructor NormalizationChargeResult NormalizationChargeInvalid))
260 (lambda unrestricted predecessor : Nat .
261 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
262 (lambda unrestricted force : Nat . (chargeValidNormalizationBudget amount budget))))
263 (normalizationBudgetValid budget))
264 zero)))
265
266def normalizationWordOne =
267 (constructor ModelWord32 ModelWord32Value (byte 1) (byte 0) (byte 0) (byte 0))
268
269def normalizationBytePredecessor =
270 (lambda unrestricted value : Byte .
271 (nat-to-byte
272 (nat-eliminate
273 (lambda unrestricted current : Nat . Nat)
274 (byte-to-nat (byte 255))
275 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . predecessor))
276 (byte-to-nat value))))
277
278def normalizationWordChoose =
279 (lambda unrestricted condition : Nat .
280 (lambda unrestricted selected : (pi unrestricted force : Nat . (family ModelWord32)) .
281 (lambda unrestricted fallback : (pi unrestricted force : Nat . (family ModelWord32)) .
282 (app
283 (nat-eliminate
284 (lambda unrestricted current : Nat .
285 (pi unrestricted force : Nat . (family ModelWord32)))
286 fallback
287 (lambda unrestricted predecessor : Nat .
288 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family ModelWord32)) .
289 selected))
290 condition)
291 zero))))
292
293-- Called only after proving remaining > 0. Borrow visits at most four bytes;
294-- it never runs bitwise XOR to subtract a single unit.
295def normalizationWordPredecessor =
296 (lambda unrestricted word : (family ModelWord32) .
297 (eliminate
298 ModelWord32
299 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
300 word
301 (branch
302 ModelWord32Value
303 b0
304 b1
305 b2
306 b3
307 .
308 (normalizationWordChoose
309 (byte-equal b0 (byte 0))
310 (lambda unrestricted force : Nat .
311 (normalizationWordChoose
312 (byte-equal b1 (byte 0))
313 (lambda unrestricted force : Nat .
314 (normalizationWordChoose
315 (byte-equal b2 (byte 0))
316 (lambda unrestricted force : Nat .
317 (constructor
318 ModelWord32
319 ModelWord32Value
320 (byte 255)
321 (byte 255)
322 (byte 255)
323 (normalizationBytePredecessor b3)))
324 (lambda unrestricted force : Nat .
325 (constructor
326 ModelWord32
327 ModelWord32Value
328 (byte 255)
329 (byte 255)
330 (normalizationBytePredecessor b2)
331 b3))))
332 (lambda unrestricted force : Nat .
333 (constructor
334 ModelWord32
335 ModelWord32Value
336 (byte 255)
337 (normalizationBytePredecessor b1)
338 b2
339 b3))))
340 (lambda unrestricted force : Nat .
341 (constructor ModelWord32 ModelWord32Value (normalizationBytePredecessor b0) b1 b2 b3))))))
342
343def chargeNormalizationBudgetOneValid =
344 (lambda unrestricted budget : (family NormalizationBudget) .
345 (eliminate
346 NormalizationBudget
347 (lambda unrestricted current : (family NormalizationBudget) .
348 (family NormalizationChargeResult))
349 budget
350 (branch
351 NormalizationBudgetValue
352 limit
353 remaining
354 used
355 .
356 (app
357 (nat-eliminate
358 (lambda unrestricted empty : Nat .
359 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
360 (lambda unrestricted force : Nat .
361 (constructor
362 NormalizationChargeResult
363 NormalizationCharged
364 (constructor
365 NormalizationBudget
366 NormalizationBudgetValue
367 limit
368 (normalizationWordPredecessor remaining)
369 (Std.Word/stdU32AddWrapping used normalizationWordOne))))
370 (lambda unrestricted predecessor : Nat .
371 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
372 (lambda unrestricted force : Nat .
373 (constructor
374 NormalizationChargeResult
375 NormalizationChargeExhausted
376 budget
377 normalizationWordOne))))
378 (Std.Word/stdU32IsZero remaining))
379 zero))))
380
381def chargeNormalizationBudgetOne =
382 (lambda unrestricted budget : (family NormalizationBudget) .
383 (app
384 (nat-eliminate
385 (lambda unrestricted valid : Nat .
386 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
387 (lambda unrestricted force : Nat .
388 (constructor NormalizationChargeResult NormalizationChargeInvalid))
389 (lambda unrestricted predecessor : Nat .
390 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
391 (lambda unrestricted force : Nat . (chargeNormalizationBudgetOneValid budget))))
392 (normalizationBudgetValid budget))
393 zero))
394
395def chargeNormalizationBudget =
396 (lambda unrestricted amount : (family ModelWord32) .
397 (lambda unrestricted budget : (family NormalizationBudget) .
398 (app
399 (nat-eliminate
400 (lambda unrestricted one : Nat .
401 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
402 (lambda unrestricted force : Nat . (chargeNormalizationBudgetGeneral amount budget))
403 (lambda unrestricted predecessor : Nat .
404 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
405 (lambda unrestricted force : Nat . (chargeNormalizationBudgetOne budget))))
406 (bytes-equal (Std.Word/stdU32EncodeLE amount) (bytes 1 0 0 0)))
407 zero)))
408
409-- Charge one byte at a time without folding over the entire payload.
410def stepNormalizationPayload =
411 (lambda unrestricted state : (family NormalizationPayloadState) .
412 (eliminate
413 NormalizationPayloadState
414 (lambda unrestricted current : (family NormalizationPayloadState) .
415 (family NormalizationPayloadState))
416 state
417 (branch
418 NormalizationPayloadActive
419 payload
420 budget
421 .
422 (app
423 (nat-eliminate
424 (lambda unrestricted nonempty : Nat .
425 (pi unrestricted force : Nat . (family NormalizationPayloadState)))
426 (lambda unrestricted force : Nat .
427 (constructor
428 NormalizationPayloadState
429 NormalizationPayloadStopped
430 (constructor NormalizationChargeResult NormalizationCharged budget)))
431 (lambda unrestricted predecessor : Nat .
432 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationPayloadState)) .
433 (lambda unrestricted force : Nat .
434 (eliminate
435 NormalizationChargeResult
436 (lambda unrestricted result : (family NormalizationChargeResult) .
437 (family NormalizationPayloadState))
438 (chargeNormalizationBudgetOne budget)
439 (branch
440 NormalizationCharged
441 next
442 .
443 (constructor
444 NormalizationPayloadState
445 NormalizationPayloadActive
446 (bytes-tail payload)
447 next))
448 (branch
449 NormalizationChargeExhausted
450 unchanged
451 amount
452 .
453 (constructor
454 NormalizationPayloadState
455 NormalizationPayloadStopped
456 (constructor
457 NormalizationChargeResult
458 NormalizationChargeExhausted
459 unchanged
460 amount)))
461 (branch
462 NormalizationChargeInvalid
463 .
464 (constructor
465 NormalizationPayloadState
466 NormalizationPayloadStopped
467 (constructor NormalizationChargeResult NormalizationChargeInvalid)))))))
468 (nat-less-than zero (bytes-length payload)))
469 zero))
470 (branch NormalizationPayloadStopped result . state)))
471
472def repeatNormalizationPayloadSmall =
473 (lambda unrestricted count : Nat .
474 (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
475 (lambda unrestricted state : (family NormalizationPayloadState) .
476 (eliminate
477 NormalizationPayloadState
478 (lambda unrestricted current : (family NormalizationPayloadState) .
479 (family NormalizationPayloadState))
480 state
481 (branch
482 NormalizationPayloadActive
483 payload
484 budget
485 .
486 (nat-eliminate
487 (lambda unrestricted index : Nat . (family NormalizationPayloadState))
488 state
489 (lambda unrestricted predecessor : Nat .
490 (lambda unrestricted induction : (family NormalizationPayloadState) .
491 (step induction)))
492 count))
493 (branch NormalizationPayloadStopped result . state)))))
494
495-- Exactly four little-endian budget bytes build base-256 iteration blocks.
496-- Each block checks Stopped before entering; no unary budget conversion occurs.
497def iterateNormalizationPayload =
498 (lambda unrestricted digits : Bytes .
499 (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
500 (lambda unrestricted seed : (family NormalizationPayloadState) .
501 (app
502 (bytes-eliminate
503 (lambda unrestricted remaining : Bytes .
504 (pi unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
505 (pi unrestricted seed : (family NormalizationPayloadState) .
506 (family NormalizationPayloadState))))
507 (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
508 (lambda unrestricted seed : (family NormalizationPayloadState) . seed))
509 (lambda unrestricted head : Byte .
510 (lambda unrestricted tail : Bytes .
511 (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) . (pi unrestricted seed : (family NormalizationPayloadState) . (family NormalizationPayloadState))) .
512 (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
513 (lambda unrestricted seed : (family NormalizationPayloadState) .
514 (continue
515 (lambda unrestricted state : (family NormalizationPayloadState) .
516 (repeatNormalizationPayloadSmall
517 (succ (byte-to-nat (byte 255)))
518 step
519 state))
520 (repeatNormalizationPayloadSmall (byte-to-nat head) step seed)))))))
521 digits)
522 step
523 seed))))
524
525def finishNormalizationPayload =
526 (lambda unrestricted state : (family NormalizationPayloadState) .
527 (eliminate
528 NormalizationPayloadState
529 (lambda unrestricted current : (family NormalizationPayloadState) .
530 (family NormalizationChargeResult))
531 state
532 (branch
533 NormalizationPayloadActive
534 payload
535 budget
536 .
537 (app
538 (nat-eliminate
539 (lambda unrestricted nonempty : Nat .
540 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
541 (lambda unrestricted force : Nat .
542 (constructor NormalizationChargeResult NormalizationCharged budget))
543 (lambda unrestricted predecessor : Nat .
544 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
545 (lambda unrestricted force : Nat .
546 (constructor
547 NormalizationChargeResult
548 NormalizationChargeExhausted
549 budget
550 normalizationWordOne))))
551 (nat-less-than zero (bytes-length payload)))
552 zero))
553 (branch NormalizationPayloadStopped result . result)))
554
555-- A sequence of checked unit charges; exhaustion retains the last valid budget.
556-- This bounds traversed payload by the remaining budget, including U32_MAX.
557def chargeNormalizationBytes =
558 (lambda unrestricted payload : Bytes .
559 (lambda unrestricted budget : (family NormalizationBudget) .
560 (app
561 (nat-eliminate
562 (lambda unrestricted valid : Nat .
563 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
564 (lambda unrestricted force : Nat .
565 (constructor NormalizationChargeResult NormalizationChargeInvalid))
566 (lambda unrestricted predecessor : Nat .
567 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
568 (lambda unrestricted force : Nat .
569 (eliminate
570 NormalizationBudget
571 (lambda unrestricted current : (family NormalizationBudget) .
572 (family NormalizationChargeResult))
573 budget
574 (branch
575 NormalizationBudgetValue
576 limit
577 remaining
578 used
579 .
580 (finishNormalizationPayload
581 (iterateNormalizationPayload
582 (Std.Word/stdU32EncodeLE remaining)
583 stepNormalizationPayload
584 (constructor
585 NormalizationPayloadState
586 NormalizationPayloadActive
587 payload
588 budget))))))))
589 (normalizationBudgetValid budget))
590 zero)))
591
592def stepNormalizationNatural =
593 (lambda unrestricted target : Nat .
594 (lambda unrestricted state : (family NormalizationNaturalState) .
595 (eliminate
596 NormalizationNaturalState
597 (lambda unrestricted current : (family NormalizationNaturalState) .
598 (family NormalizationNaturalState))
599 state
600 (branch
601 NormalizationNaturalActive
602 cursor
603 budget
604 .
605 (app
606 (nat-eliminate
607 (lambda unrestricted nonempty : Nat .
608 (pi unrestricted force : Nat . (family NormalizationNaturalState)))
609 (lambda unrestricted force : Nat .
610 (constructor
611 NormalizationNaturalState
612 NormalizationNaturalStopped
613 (constructor NormalizationChargeResult NormalizationCharged budget)))
614 (lambda unrestricted predecessor : Nat .
615 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationNaturalState)) .
616 (lambda unrestricted force : Nat .
617 (eliminate
618 NormalizationChargeResult
619 (lambda unrestricted result : (family NormalizationChargeResult) .
620 (family NormalizationNaturalState))
621 (chargeNormalizationBudgetOne budget)
622 (branch
623 NormalizationCharged
624 next
625 .
626 (constructor
627 NormalizationNaturalState
628 NormalizationNaturalActive
629 (succ cursor)
630 next))
631 (branch
632 NormalizationChargeExhausted
633 unchanged
634 amount
635 .
636 (constructor
637 NormalizationNaturalState
638 NormalizationNaturalStopped
639 (constructor
640 NormalizationChargeResult
641 NormalizationChargeExhausted
642 unchanged
643 amount)))
644 (branch
645 NormalizationChargeInvalid
646 .
647 (constructor
648 NormalizationNaturalState
649 NormalizationNaturalStopped
650 (constructor NormalizationChargeResult NormalizationChargeInvalid)))))))
651 (nat-less-than cursor target))
652 zero))
653 (branch NormalizationNaturalStopped result . state))))
654
655def repeatNormalizationNaturalSmall =
656 (lambda unrestricted count : Nat .
657 (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
658 (lambda unrestricted state : (family NormalizationNaturalState) .
659 (eliminate
660 NormalizationNaturalState
661 (lambda unrestricted current : (family NormalizationNaturalState) .
662 (family NormalizationNaturalState))
663 state
664 (branch
665 NormalizationNaturalActive
666 cursor
667 budget
668 .
669 (nat-eliminate
670 (lambda unrestricted index : Nat . (family NormalizationNaturalState))
671 state
672 (lambda unrestricted predecessor : Nat .
673 (lambda unrestricted induction : (family NormalizationNaturalState) .
674 (step induction)))
675 count))
676 (branch NormalizationNaturalStopped result . state)))))
677
678-- Exactly four little-endian budget bytes build base-256 iteration blocks.
679-- Each block checks Stopped before entering; no unary budget conversion occurs.
680def iterateNormalizationNatural =
681 (lambda unrestricted digits : Bytes .
682 (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
683 (lambda unrestricted seed : (family NormalizationNaturalState) .
684 (app
685 (bytes-eliminate
686 (lambda unrestricted remaining : Bytes .
687 (pi unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
688 (pi unrestricted seed : (family NormalizationNaturalState) .
689 (family NormalizationNaturalState))))
690 (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
691 (lambda unrestricted seed : (family NormalizationNaturalState) . seed))
692 (lambda unrestricted head : Byte .
693 (lambda unrestricted tail : Bytes .
694 (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) . (pi unrestricted seed : (family NormalizationNaturalState) . (family NormalizationNaturalState))) .
695 (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
696 (lambda unrestricted seed : (family NormalizationNaturalState) .
697 (continue
698 (lambda unrestricted state : (family NormalizationNaturalState) .
699 (repeatNormalizationNaturalSmall
700 (succ (byte-to-nat (byte 255)))
701 step
702 state))
703 (repeatNormalizationNaturalSmall (byte-to-nat head) step seed)))))))
704 digits)
705 step
706 seed))))
707
708def finishNormalizationNatural =
709 (lambda unrestricted target : Nat .
710 (lambda unrestricted state : (family NormalizationNaturalState) .
711 (eliminate
712 NormalizationNaturalState
713 (lambda unrestricted current : (family NormalizationNaturalState) .
714 (family NormalizationChargeResult))
715 state
716 (branch
717 NormalizationNaturalActive
718 cursor
719 budget
720 .
721 (app
722 (nat-eliminate
723 (lambda unrestricted nonempty : Nat .
724 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
725 (lambda unrestricted force : Nat .
726 (constructor NormalizationChargeResult NormalizationCharged budget))
727 (lambda unrestricted predecessor : Nat .
728 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
729 (lambda unrestricted force : Nat .
730 (constructor
731 NormalizationChargeResult
732 NormalizationChargeExhausted
733 budget
734 normalizationWordOne))))
735 (nat-less-than cursor target))
736 zero))
737 (branch NormalizationNaturalStopped result . result))))
738
739-- A sequence of checked unit charges; exhaustion retains the last valid budget.
740-- This bounds the natural cursor by the remaining budget, including U32_MAX.
741def chargeNormalizationNatural =
742 (lambda unrestricted target : Nat .
743 (lambda unrestricted budget : (family NormalizationBudget) .
744 (app
745 (nat-eliminate
746 (lambda unrestricted valid : Nat .
747 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
748 (lambda unrestricted force : Nat .
749 (constructor NormalizationChargeResult NormalizationChargeInvalid))
750 (lambda unrestricted predecessor : Nat .
751 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
752 (lambda unrestricted force : Nat .
753 (eliminate
754 NormalizationBudget
755 (lambda unrestricted current : (family NormalizationBudget) .
756 (family NormalizationChargeResult))
757 budget
758 (branch
759 NormalizationBudgetValue
760 limit
761 remaining
762 used
763 .
764 (finishNormalizationNatural
765 target
766 (iterateNormalizationNatural
767 (Std.Word/stdU32EncodeLE remaining)
768 (stepNormalizationNatural target)
769 (constructor
770 NormalizationNaturalState
771 NormalizationNaturalActive
772 zero
773 budget))))))))
774 (normalizationBudgetValid budget))
775 zero)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.