AlphaGitHub
Source/Packages

Compiler.NormalizationBudget

packages/compiler/src/Compiler/NormalizationBudget.alpha

775 lines53 declarations32.9 KiBSHA-256 582a37dd050a
Download exact fileView at revisionf5034773ad4bb52133

def · lines 192–210

normalizationBudgetValid

Full file
Both operands are at most limit. Their sum cannot wrap to limit: that 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))))))))

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.