module Runtime.CyclicRecordOffset

import Std.Foundation
import Std.Natural

-- A deterministic record traversal needs no mutable cursor beyond the count
-- of completed updates. This defines an offset, not a shuffled sampler. The
-- entire file fits Linux's signed offset range; additions cannot wrap the
-- persisted unsigned counter. Rejection carries no usable offset.
family CyclicRecordOffset : Type 0
constructor CyclicRecordOffsetRejected
constructor CyclicRecordOffsetAccepted
field unrestricted cyclicRecordByteOffset : Nat
end-family

def cyclicRecordWordMaximum : Nat = 18446744073709551615
def cyclicRecordFileMaximum : Nat = 9223372036854775807
def cyclicRecordOffset = (lambda unrestricted completed : Nat . (lambda unrestricted iteration : Nat .
  (lambda unrestricted count : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted within : Nat .
    (eliminate StdBool (lambda unrestricted current : (family StdBool) . (family CyclicRecordOffset))
      (stdBoolFromNatural (naturalAnd (naturalLess 0 count)
        (naturalAnd (naturalLess 0 extent) (naturalAnd (naturalLess within extent)
          (naturalAnd (naturalLessOrEqual (naturalAdd completed iteration) cyclicRecordWordMaximum)
            (naturalLessOrEqual (naturalMultiply count extent) cyclicRecordFileMaximum))))))
      (branch StdTrue . (constructor CyclicRecordOffset CyclicRecordOffsetAccepted
        (naturalAdd within (naturalMultiply extent (naturalModuloUnchecked (naturalAdd completed iteration) count)))))
      (branch StdFalse . (constructor CyclicRecordOffset CyclicRecordOffsetRejected))))))))