AlphaGitHub
Source/Packages

Runtime.DeviceArenaCertificate

packages/execution/src/Runtime/DeviceArenaCertificate.alpha

1,800 lines133 declarations66.8 KiBSHA-256 74ef7fffbf20
Download exact fileView at revisionf5034773ad4bb52133

def · lines 167–176

deviceArenaAddModulo

Full file
a + b modulo 2^64; both arms are evaluated, so neither may overflow
167def deviceArenaAddModulo =
168  (lambda unrestricted a : Nat .
169    (lambda unrestricted b : Nat .
170      (let unrestricted room =
171        (naturalSaturatingSubtract deviceArenaWordMaximum a)
172        in
173        (naturalSelect
174          (naturalLess room b)
175          (naturalSaturatingSubtract (naturalSaturatingSubtract b room) 1)
176          (naturalAdd a (naturalSelect (naturalLess room b) room b))))))

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.