A sequence of checked unit charges; exhaustion retains the last valid budget.
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)))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.