module Runtime.RegionTransfer

import Learning.Transition
import Representation.Partition
import Std.Foundation
import Std.Natural

-- Logical identity, before choosing transport or encoding. A matching byte
-- count alone cannot authorize a receive. Digests and authentication belong
-- to the wire boundary; process pointers never belong in a logical message.
family RegionTransferIdentity : Type 0
constructor RegionTransferIdentityOf
field unrestricted transferComposition : Bytes
field unrestricted transferRun : Bytes
field unrestricted transferRegion : Bytes
field unrestricted transferRepresentation : Bytes
field unrestricted transferRound : (family LearningRound)
field unrestricted transferOperation : Nat
field unrestricted transferSender : Nat
field unrestricted transferReceiver : Nat
field unrestricted transferInterval : (family LogicalInterval)

end-family

family TransferPhase : Type 0
constructor TransferDeclared
constructor TransferSourceReading
constructor TransferSourceReleased
constructor TransferPayloadReceived
constructor TransferDestinationVisible
constructor TransferConsumed
constructor TransferAborted

end-family

family TransferEvent : Type 0
constructor TransferBeginRead
constructor TransferFinishRead
constructor TransferValidatePayload
constructor TransferEstablishVisibility
constructor TransferConsume
constructor TransferAbort

end-family

family TransferFailure : Type 0
constructor TransferIdentityMismatch
constructor TransferPayloadSizeMismatch
constructor TransferIllegalPhase

end-family

def regionTransferIdentityEqual =
  (lambda unrestricted expected : (family RegionTransferIdentity) .
    (lambda unrestricted actual : (family RegionTransferIdentity) .
      (eliminate
        RegionTransferIdentity
        (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
        expected
        (branch
          RegionTransferIdentityOf
          expectedComposition
          expectedRun
          expectedRegion
          expectedRepresentation
          expectedRound
          expectedOperation
          expectedSender
          expectedReceiver
          expectedInterval
          .
          (eliminate
            RegionTransferIdentity
            (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
            actual
            (branch
              RegionTransferIdentityOf
              actualComposition
              actualRun
              actualRegion
              actualRepresentation
              actualRound
              actualOperation
              actualSender
              actualReceiver
              actualInterval
              .
              (naturalAnd
                (bytes-equal expectedComposition actualComposition)
                (naturalAnd
                  (bytes-equal expectedRun actualRun)
                  (naturalAnd
                    (bytes-equal expectedRegion actualRegion)
                    (naturalAnd
                      (bytes-equal expectedRepresentation actualRepresentation)
                      (naturalAnd
                        (learningRoundEqual expectedRound actualRound)
                        (naturalAnd
                          (naturalEqual expectedOperation actualOperation)
                          (naturalAnd
                            (naturalEqual expectedSender actualSender)
                            (naturalAnd
                              (naturalEqual expectedReceiver actualReceiver)
                              (naturalAnd
                                (naturalEqual
                                  (intervalBegin expectedInterval)
                                  (intervalBegin actualInterval))
                                (naturalEqual
                                  (intervalEnd expectedInterval)
                                  (intervalEnd actualInterval)))))))))))))))))

def transferPhaseCode =
  (lambda unrestricted phase : (family TransferPhase) .
    (eliminate
      TransferPhase
      (lambda unrestricted current : (family TransferPhase) . Nat)
      phase
      (branch TransferDeclared . 0)
      (branch TransferSourceReading . 1)
      (branch TransferSourceReleased . 2)
      (branch TransferPayloadReceived . 3)
      (branch TransferDestinationVisible . 4)
      (branch TransferConsumed . 5)
      (branch TransferAborted . 6)))

def transferRequirePhase =
  (lambda unrestricted expected : Nat .
    (lambda unrestricted next : (family TransferPhase) .
      (lambda unrestricted actual : (family TransferPhase) .
        (nat-eliminate
          (lambda unrestricted flag : Nat .
            (family StdResult (family TransferFailure) (family TransferPhase)))
          (constructor
            StdResult
            StdFailure
            (family TransferFailure)
            (family TransferPhase)
            (constructor TransferFailure TransferIllegalPhase))
          (lambda unrestricted previous : Nat .
            (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
              (constructor
                StdResult
                StdSuccess
                (family TransferFailure)
                (family TransferPhase)
                next)))
          (naturalEqual expected (transferPhaseCode actual))))))

-- These are protocol states, not claims of physical DMA completion. A native
-- realization must obtain events from its actual transport and visibility
-- primitives. One edge's state has one execution owner.
def advanceTransferPhase =
  (lambda unrestricted phase : (family TransferPhase) .
    (lambda unrestricted event : (family TransferEvent) .
      (eliminate
        TransferEvent
        (lambda unrestricted current : (family TransferEvent) .
          (family StdResult (family TransferFailure) (family TransferPhase)))
        event
        (branch
          TransferBeginRead
          .
          (transferRequirePhase 0 (constructor TransferPhase TransferSourceReading) phase))
        (branch
          TransferFinishRead
          .
          (transferRequirePhase 1 (constructor TransferPhase TransferSourceReleased) phase))
        (branch
          TransferValidatePayload
          .
          (transferRequirePhase 2 (constructor TransferPhase TransferPayloadReceived) phase))
        (branch
          TransferEstablishVisibility
          .
          (transferRequirePhase 3 (constructor TransferPhase TransferDestinationVisible) phase))
        (branch
          TransferConsume
          .
          (transferRequirePhase 4 (constructor TransferPhase TransferConsumed) phase))
        (branch
          TransferAbort
          .
          (nat-eliminate
            (lambda unrestricted flag : Nat .
              (family StdResult (family TransferFailure) (family TransferPhase)))
            (constructor
              StdResult
              StdFailure
              (family TransferFailure)
              (family TransferPhase)
              (constructor TransferFailure TransferIllegalPhase))
            (lambda unrestricted previous : Nat .
              (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
                (constructor
                  StdResult
                  StdSuccess
                  (family TransferFailure)
                  (family TransferPhase)
                  (constructor TransferPhase TransferAborted))))
            (naturalLess (transferPhaseCode phase) 5))))))

-- Aborting does not establish that in-flight DMA has stopped. Teardown must
-- drain those reads before reclaiming resources.
def transferSourceReusable =
  (lambda unrestricted phase : (family TransferPhase) .
    (let unrestricted code =
      (transferPhaseCode phase)
      in
      (naturalAnd (naturalLessOrEqual 2 code) (naturalLessOrEqual code 5))))

def transferDestinationUsable =
  (lambda unrestricted phase : (family TransferPhase) .
    (let unrestricted code =
      (transferPhaseCode phase)
      in
      (naturalAnd (naturalLessOrEqual 4 code) (naturalLessOrEqual code 5))))

def receiveRegionTransfer =
  (lambda unrestricted expected : (family RegionTransferIdentity) .
    (lambda unrestricted actual : (family RegionTransferIdentity) .
      (lambda unrestricted expectedBytes : Nat .
        (lambda unrestricted actualBytes : Nat .
          (lambda unrestricted phase : (family TransferPhase) .
            (nat-eliminate
              (lambda unrestricted flag : Nat .
                (family StdResult (family TransferFailure) (family TransferPhase)))
              (constructor
                StdResult
                StdFailure
                (family TransferFailure)
                (family TransferPhase)
                (constructor TransferFailure TransferIdentityMismatch))
              (lambda unrestricted previous : Nat .
                (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
                  (nat-eliminate
                    (lambda unrestricted flag : Nat .
                      (family StdResult (family TransferFailure) (family TransferPhase)))
                    (constructor
                      StdResult
                      StdFailure
                      (family TransferFailure)
                      (family TransferPhase)
                      (constructor TransferFailure TransferPayloadSizeMismatch))
                    (lambda unrestricted before : Nat .
                      (lambda unrestricted rest : (family StdResult (family TransferFailure) (family TransferPhase)) .
                        (advanceTransferPhase
                          phase
                          (constructor TransferEvent TransferValidatePayload))))
                    (naturalEqual expectedBytes actualBytes))))
              (regionTransferIdentityEqual expected actual)))))))

-- Route projection reads the same identity that the wire header encodes;
-- participant programs must not keep a second, independently chosen route.
def regionTransferSender =
  (lambda unrestricted identity : (family RegionTransferIdentity) .
    (eliminate
      RegionTransferIdentity
      (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
      identity
      (branch
        RegionTransferIdentityOf
        composition
        run
        region
        representation
        round
        operation
        sender
        receiver
        interval
        .
        sender)))

def regionTransferReceiver =
  (lambda unrestricted identity : (family RegionTransferIdentity) .
    (eliminate
      RegionTransferIdentity
      (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
      identity
      (branch
        RegionTransferIdentityOf
        composition
        run
        region
        representation
        round
        operation
        sender
        receiver
        interval
        .
        receiver)))

-- Change only the route of a logical transfer; all scope, version and region
-- fields survive. Used when a single decision is disseminated along a tree.

def regionTransferWithRoute =
(lambda unrestricted identity : (family RegionTransferIdentity) .
(lambda unrestricted sender : Nat .
(lambda unrestricted receiver : Nat .
(eliminate RegionTransferIdentity (lambda unrestricted current : (family RegionTransferIdentity) . (family RegionTransferIdentity)) identity
(branch RegionTransferIdentityOf composition run region representation round operation oldSender oldReceiver interval .
(constructor RegionTransferIdentity RegionTransferIdentityOf composition run region representation round operation sender receiver interval))))))