1module Runtime.CyclicRecordOffset
2
3import Std.Foundation
4import Std.Natural
5
6-- A deterministic record traversal needs no mutable cursor beyond the count
7-- of completed updates. This defines an offset, not a shuffled sampler. The
8-- entire file fits Linux's signed offset range; additions cannot wrap the
9-- persisted unsigned counter. Rejection carries no usable offset.
10family CyclicRecordOffset : Type 0
11constructor CyclicRecordOffsetRejected
12constructor CyclicRecordOffsetAccepted
13field unrestricted cyclicRecordByteOffset : Nat
14end-family
15
16def cyclicRecordWordMaximum : Nat = 18446744073709551615
17def cyclicRecordFileMaximum : Nat = 9223372036854775807
18def cyclicRecordOffset = (lambda unrestricted completed : Nat . (lambda unrestricted iteration : Nat .
19 (lambda unrestricted count : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted within : Nat .
20 (eliminate StdBool (lambda unrestricted current : (family StdBool) . (family CyclicRecordOffset))
21 (stdBoolFromNatural (naturalAnd (naturalLess 0 count)
22 (naturalAnd (naturalLess 0 extent) (naturalAnd (naturalLess within extent)
23 (naturalAnd (naturalLessOrEqual (naturalAdd completed iteration) cyclicRecordWordMaximum)
24 (naturalLessOrEqual (naturalMultiply count extent) cyclicRecordFileMaximum))))))
25 (branch StdTrue . (constructor CyclicRecordOffset CyclicRecordOffsetAccepted
26 (naturalAdd within (naturalMultiply extent (naturalModuloUnchecked (naturalAdd completed iteration) count)))))
27 (branch StdFalse . (constructor CyclicRecordOffset CyclicRecordOffsetRejected))))))))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.