AlphaGitHub
Source/Packages

Runtime.NativeObservedJournal

packages/execution/src/Runtime/NativeObservedJournal.alpha

253 lines11 declarations11.2 KiBSHA-256 7226d59e4359
Download exact fileView at revision426597bda5753d86c4

def · lines 44–56

nativeObservedJournalAdmission

Full file
44def nativeObservedJournalAdmission =
45  (lambda unrestricted applicationBytes : Nat .
46    (lambda unrestricted applicationSlots : Nat .
47      (lambda unrestricted pathAt : Nat .
48        (lambda unrestricted fileSlot : Nat .
49          (lambda unrestricted directorySlot : Nat .
50            (naturalAnd
51              (telemetryRangeFits pathAt nativeObservedJournalBytes applicationBytes)
52              (naturalAnd
53                (naturalLess fileSlot applicationSlots)
54                (naturalAnd
55                  (naturalLess directorySlot applicationSlots)
56                  (naturalIsZero (naturalEqual fileSlot directorySlot))))))))))

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.