Publication owns the frame and checkpoint scratch arenas. A shard's bytes
must lie entirely within its owner's captured state payload, past the
capture prefix, never in a header or digest workspace that publication
itself overwrites. Offsets are relative to the owner's state.
323def nativePublicationSourceWithin =
324 (lambda unrestricted start : Nat .
325 (lambda unrestricted count : Nat .
326 (lambda unrestricted base : Nat .
327 (lambda unrestricted size : Nat .
328 (naturalAnd
329 (naturalLessOrEqual (naturalAdd base nativeRegionCaptureBytes) start)
330 (naturalLessOrEqual (naturalAdd start count) (naturalAdd base size)))))))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.