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)))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.