module Runtime.NativeRegionFrame

import Compiler.Planning.RegionFrame
import Runtime.RegionFrame
import Runtime.NativeSocketPlan
import Runtime.NativeMemoryPlan
import Runtime.NativeMemoryRoutine
import Runtime.NativeWordArithmetic
import Runtime.NativeWordDigest
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad
import Model.Word64
import Std.Natural

-- Endpoint-local ownership: validated means verified bytes in host staging.
-- It is not GPU visibility. Device upload/fences belong to the target session.
-- A layout is initialized once. Completed rounds advance explicitly; replacing
-- a live session with another epoch remains the caller's admission obligation.
family NativeFramePhase : Type 0
constructor NativeFrameUnissued
constructor NativeFrameActive
constructor NativeFrameValidated
constructor NativeFrameConsumed
constructor NativeFrameSent

end-family

-- Rearming cannot accept an arbitrary phase such as Active or Validated.
family NativeFrameTerminal : Type 0
constructor NativeFrameSendComplete
constructor NativeFrameConsumeComplete

end-family

def nativeFramePhaseCode =
  (lambda unrestricted phase : (family NativeFramePhase) .
    (eliminate
      NativeFramePhase
      (lambda unrestricted p : (family NativeFramePhase) . Nat)
      phase
      (branch NativeFrameUnissued . 0)
      (branch NativeFrameActive . 1)
      (branch NativeFrameValidated . 2)
      (branch NativeFrameConsumed . 3)
      (branch NativeFrameSent . 4)))

def frameNativeState =
  nativeMemoryState

def frameNativeLoad =
  nativeMemoryLoad

def frameNativeCopy =
  nativeMemoryCopyPayload

def frameNativePhase =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted phase : (family NativeFramePhase) .
      (nativeLaunchRecipeCommand
        (constructor
          NativePhysicalOperation
          NativePhysicalStoreWord64
          (frameNativeState (framePhaseAt layout))
          (nativeLaunchRecipeImmediate (nativeFramePhaseCode phase)))
        b"frame-phase")))

def frameNativeRequirePhase =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted phase : (family NativeFramePhase) .
      (nativeLaunchRecipeAssertEqual
        (frameNativeLoad (framePhaseAt layout))
        (nativeLaunchRecipeImmediate (nativeFramePhaseCode phase))
        b"frame-phase-mismatch")))

def nativeFrameInitialize =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted tail : (family NativePhysicalCommands) .
      (frameNativeCopy
        (frameExpectedAt layout)
        (frameHeader layout)
        (frameNativePhase layout (constructor NativeFramePhase NativeFrameUnissued) tail))))

-- Resume initializes a fresh slot from admitted runtime state. It does not
-- authorize reinitializing a live slot or choosing a peer-supplied epoch.
def nativeFrameInitializeRound =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted epoch : (family NativePhysicalOperand) .
      (lambda unrestricted version : (family NativePhysicalOperand) .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativeFrameInitialize
            layout
            (nativeLaunchRecipeCommand
              (constructor
                NativePhysicalOperation
                NativePhysicalStoreWord64
                (frameNativeState (frameExpectedEpochAt layout))
                epoch)
              b"frame-initialize-epoch"
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalStoreWord64
                  (frameNativeState (frameExpectedVersionAt layout))
                  version)
                b"frame-initialize-version"
                tail)))))))

def nativeFrameAdvance =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted terminal : (family NativeFrameTerminal) .
      (lambda unrestricted slot : Nat .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (frameNativeRequirePhase
            layout
            (eliminate
              NativeFrameTerminal
              (lambda unrestricted current : (family NativeFrameTerminal) .
                (family NativeFramePhase))
              terminal
              (branch NativeFrameSendComplete . (constructor NativeFramePhase NativeFrameSent))
              (branch
                NativeFrameConsumeComplete
                .
                (constructor NativeFramePhase NativeFrameConsumed)))
            (nativeCheckedWordAdd
              (frameNativeState (frameExpectedVersionAt layout))
              (frameNativeLoad (frameExpectedVersionAt layout))
              (nativeLaunchRecipeImmediate 1)
              slot
              b"frame-version-overflow"
              (frameNativePhase layout (constructor NativeFramePhase NativeFrameUnissued) tail)))))))

-- Copy the current expected header, including its runtime round. Recopying
-- the static layout header here would silently retransmit the first version.
def frameNativeCopyHeader =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted slot : Nat .
      (nativeMemoryCopyOperands
        (frameNativeState (frameHeaderAt layout))
        (frameNativeState (frameExpectedAt layout))
        (bytes-length (frameHeader layout))
        slot
        b"frame-header-copy")))

def frameNativeCompare =
  nativeMemoryCompareRegions

def frameNativeHash =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted slot : Nat .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (frameNativeCopy
          (framePaddingAt layout)
          (framePadding layout)
          (nativeLaunchRecipeCommand
            (constructor
              NativePhysicalOperation
              NativePhysicalMachineRoutine
              nativeWordDigestRoutine
              (constructor
                NativePhysicalArguments
                NativePhysicalArgumentsValue
                (frameNativeState (frameHeaderAt layout))
                (nativeLaunchRecipeImmediate (frameBlockCount layout))
                (frameNativeState (frameComputedAt layout))
                (nativeLaunchRecipeImmediate 0)
                (nativeLaunchRecipeImmediate 0)
                (frameNativeState (frameWorkAt layout)))
              (nativeLaunchRecipeStore slot))
            b"frame-hash"
            (nativeLaunchRecipeAssertEqual
              (nativeLaunchRecipeSlotValue slot)
              (nativeLaunchRecipeImmediate regionFrameDigestBytes)
              b"frame-hash-count"
              tail))))))

def frameNativeIO =
  (lambda unrestricted send : Nat .
    (lambda unrestricted descriptor : (family NativePhysicalOperand) .
      (lambda unrestricted offset : Nat .
        (lambda unrestricted extent : Nat .
          (lambda unrestricted timeout : (family NativePhysicalOperand) .
            (lambda unrestricted attempts : (family NativePhysicalOperand) .
              (lambda unrestricted slot : Nat .
                (lambda unrestricted tail : (family NativePhysicalCommands) .
                  (nativeLaunchRecipeCommand
                    (nat-eliminate
                      (lambda unrestricted n : Nat . (family NativePhysicalOperation))
                      (nativeSocketRead
                        descriptor
                        (frameNativeState offset)
                        (nativeLaunchRecipeImmediate extent)
                        timeout
                        attempts
                        (nativeLaunchRecipeStore slot))
                      (lambda unrestricted n : Nat .
                        (lambda unrestricted ignored : (family NativePhysicalOperation) .
                          (nativeSocketWrite
                            descriptor
                            (frameNativeState offset)
                            (nativeLaunchRecipeImmediate extent)
                            timeout
                            attempts
                            (nativeLaunchRecipeStore slot))))
                      send)
                    b"frame-stream"
                    (nativeLaunchRecipeAssertEqual
                      (nativeLaunchRecipeSlotValue slot)
                      (nativeLaunchRecipeImmediate extent)
                      b"frame-stream-count"
                      tail))))))))))

-- Read/compare the locally known header before any body read. The trailer
-- has its own region, so digest padding cannot destroy the peer's claim.
-- Every failure is fatal to this stream; partial bytes are never consumed.
def nativeFrameReceive =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted descriptor : (family NativePhysicalOperand) .
      (lambda unrestricted timeout : (family NativePhysicalOperand) .
        (lambda unrestricted attempts : (family NativePhysicalOperand) .
          (lambda unrestricted slot : Nat .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (frameNativeRequirePhase
                layout
                (constructor NativeFramePhase NativeFrameUnissued)
                (frameNativePhase
                  layout
                  (constructor NativeFramePhase NativeFrameActive)
                  (frameNativeIO
                    0
                    descriptor
                    (frameHeaderAt layout)
                    (bytes-length (frameHeader layout))
                    timeout
                    attempts
                    slot
                    (frameNativeCompare
                      (frameHeaderAt layout)
                      (frameExpectedAt layout)
                      (bytes-length (frameHeader layout))
                      slot
                      b"frame-header-mismatch"
                      (frameNativeIO
                        0
                        descriptor
                        (framePayloadAt layout)
                        (framePayloadBytes layout)
                        timeout
                        attempts
                        slot
                        (frameNativeIO
                          0
                          descriptor
                          (frameReceivedAt layout)
                          regionFrameDigestBytes
                          timeout
                          attempts
                          slot
                          (frameNativeHash
                            layout
                            slot
                            (frameNativeCompare
                              (frameComputedAt layout)
                              (frameReceivedAt layout)
                              regionFrameDigestBytes
                              slot
                              b"frame-digest-mismatch"
                              (frameNativePhase
                                layout
                                (constructor NativeFramePhase NativeFrameValidated)
                                tail)))))))))))))))

-- The producer owns the payload and may fill it before this fragment. A
-- complete socket write releases this local source; it is not a peer ACK.
def nativeFrameSend =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted descriptor : (family NativePhysicalOperand) .
      (lambda unrestricted timeout : (family NativePhysicalOperand) .
        (lambda unrestricted attempts : (family NativePhysicalOperand) .
          (lambda unrestricted slot : Nat .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (frameNativeRequirePhase
                layout
                (constructor NativeFramePhase NativeFrameUnissued)
                (frameNativePhase
                  layout
                  (constructor NativeFramePhase NativeFrameActive)
                  (frameNativeCopyHeader
                    layout
                    slot
                    (frameNativeHash
                      layout
                      slot
                      (frameNativeIO
                        1
                        descriptor
                        (frameHeaderAt layout)
                        (frameContentBytes layout)
                        timeout
                        attempts
                        slot
                        (frameNativeIO
                          1
                          descriptor
                          (frameComputedAt layout)
                          regionFrameDigestBytes
                          timeout
                          attempts
                          slot
                          (frameNativePhase
                            layout
                            (constructor NativeFramePhase NativeFrameSent)
                            tail)))))))))))))

def nativeFrameConsume =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (lambda unrestricted tail : (family NativePhysicalCommands) .
      (frameNativeRequirePhase
        layout
        (constructor NativeFramePhase NativeFrameValidated)
        (frameNativePhase layout (constructor NativeFramePhase NativeFrameConsumed) tail))))