module Runtime.ArenaCertificate

import Std.Natural

-- A placement certificate for a static arena: not a byte total but the
-- actual placement.  Every resident names its offset, extent and alignment;
-- the certificate holds when each resident is aligned, non-empty and inside
-- the arena, and every pair of residents is disjoint.  Residents here are
-- all live for the whole program, so disjointness is the whole aliasing
-- rule; lifetimes and happens-before come later, with the event graph.  The
-- checker decides the certificate on a concrete plan by normalization.

family ArenaResident : Type 0
constructor ArenaResidentValue
field unrestricted arenaResidentIdentity : Bytes
field unrestricted arenaResidentOffset : Nat
field unrestricted arenaResidentExtent : Nat
field unrestricted arenaResidentAlignment : Nat
end-family

family ArenaResidents : Type 0
constructor ArenaResidentsEnd
constructor ArenaResidentsNext
field unrestricted arenaResidentsHead : (family ArenaResident)
recursive unrestricted arenaResidentsTail
end-family

-- the schedule's events and the pending ranges (below)
family ArenaEvent : Type 0
constructor ArenaHostWrite
field unrestricted arenaHostWriteOffset : Nat
field unrestricted arenaHostWriteExtent : Nat
constructor ArenaHostRead
field unrestricted arenaHostReadOffset : Nat
field unrestricted arenaHostReadExtent : Nat
constructor ArenaAwait
field unrestricted arenaAwaitGeneration : Nat
constructor ArenaObserve
field unrestricted arenaObserveGeneration : Nat
end-family

family ArenaEvents : Type 0
constructor ArenaEventsEnd
constructor ArenaEventsNext
field unrestricted arenaEventsHead : (family ArenaEvent)
recursive unrestricted arenaEventsTail
end-family

-- the pending host writes, as [start, stop)
family ArenaRanges : Type 0
constructor ArenaRangesNone
constructor ArenaRangesNext
field unrestricted arenaRangeStart : Nat
field unrestricted arenaRangeStop : Nat
recursive unrestricted arenaRangesTail
end-family

def arenaResidentOffsetOf =
  (lambda unrestricted resident : (family ArenaResident) .
    (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
      (branch ArenaResidentValue identity offset extent alignment . offset)))

def arenaResidentEndOf =
  (lambda unrestricted resident : (family ArenaResident) .
    (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
      (branch ArenaResidentValue identity offset extent alignment . (naturalAdd offset extent))))

-- offset mod alignment = 0, extent > 0, alignment > 0, offset + extent <= arena
def arenaResidentValid =
  (lambda unrestricted arenaExtent : Nat .
    (lambda unrestricted resident : (family ArenaResident) .
      (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
        (branch ArenaResidentValue identity offset extent alignment .
          (naturalAnd
            (naturalIsZero (naturalIsZero alignment))
            (naturalAnd
              (naturalIsZero (nat-modulo offset alignment))
              (naturalAnd
                (naturalIsZero (naturalIsZero extent))
                (naturalLessOrEqual (naturalAdd offset extent) arenaExtent))))))))

-- [a, a+n) and [b, b+m) are disjoint when one ends before the other begins.
def arenaDisjoint =
  (lambda unrestricted left : (family ArenaResident) .
    (lambda unrestricted right : (family ArenaResident) .
      (naturalOr
        (naturalLessOrEqual (arenaResidentEndOf left) (arenaResidentOffsetOf right))
        (naturalLessOrEqual (arenaResidentEndOf right) (arenaResidentOffsetOf left)))))

def arenaDisjointFromAll =
  (lambda unrestricted resident : (family ArenaResident) .
    (lambda unrestricted others : (family ArenaResidents) .
      (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) others
        (branch ArenaResidentsEnd . 1)
        (branch ArenaResidentsNext head tail induction .
          (naturalAnd (arenaDisjoint resident head) induction)))))

-- 1 when the placement is certified, 0 otherwise.
def arenaCertificate =
  (lambda unrestricted arenaExtent : Nat .
    (lambda unrestricted residents : (family ArenaResidents) .
      (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) residents
        (branch ArenaResidentsEnd . 1)
        (branch ArenaResidentsNext head tail induction .
          (naturalAnd (arenaResidentValid arenaExtent head)
            (naturalAnd (arenaDisjointFromAll head tail) induction))))))

-- ---- the schedule over the arena ----
-- What the certificate sees of a host's schedule over its host-visible
-- arena: the host writes a range, reads a range, awaits a submission by its
-- generation (the submissions issued once it is written; the host goes on
-- only when that one has completed), or observes an awaited submission (a
-- timestamp of it).  The device's work is ordered with the host's by those
-- waits alone, so the certificate decides that the order the host relies on
-- is the order it has:
--   * generations strictly increase, so every wait awaits work its own
--     submit issued -- a completion of an earlier generation cannot satisfy
--     it -- and the last is the plan's count: every submission awaited;
--   * a host write is pending until a submission consumes it; a host write
--     over a pending range would overwrite staging no submission has read,
--     and none may be pending at the end;
--   * a host read of a pending range would read back the host's own
--     staging, not a submission's result;
--   * an observation names an awaited generation.
-- Ranges of no bytes touch nothing.

def arenaRangesNone : (family ArenaRanges) = (constructor ArenaRanges ArenaRangesNone)

-- 1 when [start, stop) meets a range of the list
def arenaRangesMeet =
  (lambda unrestricted start : Nat .
    (lambda unrestricted stop : Nat .
      (lambda unrestricted ranges : (family ArenaRanges) .
        (eliminate ArenaRanges (lambda unrestricted current : (family ArenaRanges) . Nat) ranges
          (branch ArenaRangesNone . 0)
          (branch ArenaRangesNext otherStart otherStop tail induction .
            (naturalOr (naturalAnd (naturalLess start otherStop) (naturalLess otherStart stop)) induction))))))

def arenaRangesEmpty =
  (lambda unrestricted ranges : (family ArenaRanges) .
    (eliminate ArenaRanges (lambda unrestricted current : (family ArenaRanges) . Nat) ranges
      (branch ArenaRangesNone . 1)
      (branch ArenaRangesNext start stop tail induction . 0)))

-- The first event that breaks the order, counted from 1 (one past the last
-- when the end does: a submission never awaited, or a write never
-- consumed), or 0 when none does.  The walk carries the first hazard found
-- and makes one recursive call per event (a choice between two
-- continuations would be evaluated on both sides by the build's evaluator).
def arenaScheduleHazard =
  (lambda unrestricted count : Nat .
    (lambda unrestricted events : (family ArenaEvents) .
      (app (app (app (app
        (eliminate ArenaEvents
          (lambda unrestricted current : (family ArenaEvents) .
            (pi unrestricted index : Nat . (pi unrestricted last : Nat . (pi unrestricted pending : (family ArenaRanges) . (pi unrestricted hazard : Nat . Nat)))))
          events
          (branch ArenaEventsEnd .
            (lambda unrestricted index : Nat . (lambda unrestricted last : Nat . (lambda unrestricted pending : (family ArenaRanges) . (lambda unrestricted hazard : Nat .
              (naturalSelect hazard hazard
                (naturalSelect (naturalAnd (naturalEqual last count) (arenaRangesEmpty pending)) 0 index)))))))
          (branch ArenaEventsNext event rest induction .
            (lambda unrestricted index : Nat . (lambda unrestricted last : Nat . (lambda unrestricted pending : (family ArenaRanges) . (lambda unrestricted hazard : Nat .
              (let unrestricted found = (lambda unrestricted failed : Nat . (naturalSelect hazard hazard (naturalSelect failed index 0)))
                in (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) event
                  (branch ArenaHostWrite offset extent .
                    (let unrestricted meets = (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending))
                      in (induction (succ index) last
                           (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
                             pending
                             (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) .
                               (constructor ArenaRanges ArenaRangesNext offset (naturalAdd offset extent) pending)))
                             (naturalAnd (naturalNonzero extent) (naturalIsZero meets)))
                           (found meets))))
                  (branch ArenaHostRead offset extent .
                    (induction (succ index) last pending
                      (found (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending)))))
                  (branch ArenaAwait generation .
                    (let unrestricted fresh = (naturalLess last generation)
                      in (induction (succ index) (naturalSelect fresh generation last)
                           (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
                             pending
                             (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) . arenaRangesNone))
                             fresh)
                           (found (naturalIsZero fresh)))))
                  (branch ArenaObserve generation .
                    (induction (succ index) last pending
                      (found (naturalIsZero (naturalAnd (naturalNonzero generation) (naturalLessOrEqual generation last))))))))))))))
        1) 0) arenaRangesNone) 0)))

-- 1 when the schedule keeps the order, 0 otherwise.
def arenaScheduleCertificate =
  (lambda unrestricted count : Nat .
    (lambda unrestricted events : (family ArenaEvents) .
      (naturalIsZero (arenaScheduleHazard count events))))