module Runtime.NativePeerEndpoint

import Compiler.Planning.RegionFrame
import Runtime.NativeRegionFrame
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativeMemoryPlan
import Runtime.NativeSocketPlan
import Runtime.SocketAddress
import Runtime.WordDigest
import Std.List
import Data.Bytes
import Std.Natural

-- ---- edges ----
-- A participant's sessions are its incident edges, in ascending peer order.
-- Each edge has one IPv4 address. The lower role of an edge binds and listens
-- on it; the higher role connects to it. Every edge owns a listener slot and
-- a connection slot, so a peer's descriptor is a static slot, never a
-- runtime lookup, and the protocol layer can name it by peer role.
--
-- Establishment order: copy every address, bind and listen on every edge to
-- a higher peer, announce those ports (two bytes each, big-endian, edge
-- order), then establish edges in order: connect to each lower peer, accept
-- each higher peer and close that listener. Launching participants in role
-- order, each after the previous announced, therefore never connects to an
-- absent listener, and no participant accepts before it has finished its own
-- connects. A star (role 0 listens for every other role) and a two-role pair
-- are instances; with one edge this is exactly the earlier two-role setup.
-- Fixed membership: the addresses are compiled in, and a missing or late
-- peer exhausts the bounded accept/connect budgets and aborts.
family NativePeerEdge : Type 0
constructor NativePeerEdgeOf
field unrestricted nativePeerEdgePeer : Nat
field unrestricted nativePeerEdgeAddress : Bytes

end-family

-- Endpoint policy shared by learning compositions: a participant's incident
-- edges (two-role pairs are the one-edge case). It owns their result slots,
-- bounded establishment/IO and listener reporting; it does not define a
-- learning equation, membership authentication or device fallback.
def nativePeerWordBytes : Nat =
  digestAddressBytes

def nativePeerIOWithBudget =
  (lambda unrestricted timeout : (family NativePhysicalOperand) .
    (lambda unrestricted attempts : (family NativePhysicalOperand) .
      (lambda unrestricted descriptor : (family NativePhysicalOperand) .
        (lambda unrestricted send : Nat .
          (lambda unrestricted layout : (family RegionFrameLayout) .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nat-eliminate
                (lambda unrestricted n : Nat . (family NativePhysicalCommands))
                (nativeFrameReceive layout descriptor timeout attempts 0 tail)
                (lambda unrestricted n : Nat .
                  (lambda unrestricted ignored : (family NativePhysicalCommands) .
                    (nativeFrameSend layout descriptor timeout attempts 0 tail)))
                send)))))))

-- These are explicit fixed-membership policy defaults, not measured device
-- latency bounds. A caller waiting for durable publication chooses its own
-- larger admitted budget through nativePeerIOWithBudget.
def nativePeerIOAttempts : Nat =
  4096

def nativePeerIO =
  (nativePeerIOWithBudget
    (nativeLaunchRecipeImmediate 1000)
    (nativeLaunchRecipeImmediate nativePeerIOAttempts))

def nativePeerScratchSlot : Nat =
  0

def nativePeerListenerSlot =
  (naturalAdd nativePeerScratchSlot 1)

def nativePeerConnectionSlot =
  (naturalAdd nativePeerListenerSlot 1)

def nativePeerEndpointSlots =
  (naturalAdd nativePeerConnectionSlot 1)

def nativePeerEndpointLengthAt =
  (lambda unrestricted base : Nat . (naturalAdd base linuxIPv4SocketAddressBytes))

def nativePeerEndpointEnd =
  (lambda unrestricted base : Nat .
    (naturalAdd (nativePeerEndpointLengthAt base) nativePeerWordBytes))

def nativePeerPortWrite =
  (lambda unrestricted base : Nat .
    (lambda unrestricted tail : (family NativePhysicalCommands) .
      (nativeLaunchRecipeCommand
        (nativeSocketSystemCall
          1
          (nativeLaunchRecipeArguments
            (nativeLaunchRecipeImmediate 1)
            (frameNativeState (naturalAdd base linuxIPv4PortAt))
            (nativeLaunchRecipeImmediate linuxIPv4PortBytes)
            (nativeLaunchRecipeImmediate 0))
          (nativeLaunchRecipeStore nativePeerScratchSlot))
        b"peer-listening-port"
        (nativeLaunchRecipeAssertEqual
          (nativeLaunchRecipeSlotValue nativePeerScratchSlot)
          (nativeLaunchRecipeImmediate linuxIPv4PortBytes)
          b"peer-listening-port-count"
          tail))))

def nativePeerEdgePeerOf =
  (lambda unrestricted edge : (family NativePeerEdge) .
    (eliminate
      NativePeerEdge
      (lambda unrestricted current : (family NativePeerEdge) . Nat)
      edge
      (branch NativePeerEdgeOf peer address . peer)))

def nativePeerEdgeAddressOf =
  (lambda unrestricted edge : (family NativePeerEdge) .
    (eliminate
      NativePeerEdge
      (lambda unrestricted current : (family NativePeerEdge) . Bytes)
      edge
      (branch NativePeerEdgeOf peer address . address)))

def nativePeerEdgeListenerSlot =
  (lambda unrestricted index : Nat . (naturalAdd nativePeerListenerSlot (naturalMultiply 2 index)))

def nativePeerEdgeConnectionSlot =
  (lambda unrestricted index : Nat .
    (naturalAdd nativePeerConnectionSlot (naturalMultiply 2 index)))

def nativePeerEdgeSlots =
  (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
    (nativePeerEdgeListenerSlot (stdListLength (family NativePeerEdge) edges)))

-- One address entry: the socket address followed by its socklen word.
def nativePeerEdgeEntryBytes =
  (nativePeerEndpointEnd 0)

def nativePeerEdgeAddressAt =
  (lambda unrestricted base : Nat .
    (lambda unrestricted index : Nat .
      (naturalAdd base (naturalMultiply index nativePeerEdgeEntryBytes))))

def nativePeerEdgesEnd =
  (lambda unrestricted base : Nat .
    (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
      (nativePeerEdgeAddressAt base (stdListLength (family NativePeerEdge) edges))))

-- Edges in order with their positions, for folds that need the slot index.
def nativePeerEdgesFold =
  (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
    (lambda unrestricted step : (pi unrestricted index : Nat . (pi unrestricted edge : (family NativePeerEdge) . (pi unrestricted rest : (family NativePhysicalCommands) . (family NativePhysicalCommands)))) .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (stdListFold
          (family NativePeerEdge)
          (pi unrestricted index : Nat . (family NativePhysicalCommands))
          (lambda unrestricted edge : (family NativePeerEdge) .
            (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
              (lambda unrestricted index : Nat . (step index edge (next (succ index))))))
          (lambda unrestricted index : Nat . tail)
          edges
          0))))

def nativePeerEdgeListens =
  (lambda unrestricted role : Nat .
    (lambda unrestricted edge : (family NativePeerEdge) .
      (naturalLess role (nativePeerEdgePeerOf edge))))

def nativePeerEdgeWhenListening =
  (lambda unrestricted role : Nat .
    (lambda unrestricted edge : (family NativePeerEdge) .
      (lambda unrestricted listening : (family NativePhysicalCommands) .
        (lambda unrestricted connecting : (family NativePhysicalCommands) .
          (nat-eliminate
            (lambda unrestricted current : Nat . (family NativePhysicalCommands))
            connecting
            (lambda unrestricted previous : Nat .
              (lambda unrestricted ignored : (family NativePhysicalCommands) . listening))
            (nativePeerEdgeListens role edge))))))

def nativePeerEdgeListen =
  (lambda unrestricted at : Nat .
    (lambda unrestricted index : Nat .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (nativeSocketOpenIPv4
          (nativePeerEdgeListenerSlot index)
          nativePeerScratchSlot
          (nativeSocketBindListener
            (nativeLaunchRecipeSlotValue (nativePeerEdgeListenerSlot index))
            (frameNativeState at)
            (nativeLaunchRecipeImmediate 1)
            nativePeerScratchSlot
            (nativeMemoryStoreWord64
              b"peer-state"
              (nativePeerEndpointLengthAt at)
              (nativeLaunchRecipeImmediate linuxIPv4SocketAddressBytes)
              (nativeSocketRequireZero
                (nativeSocketLocalAddress
                  (nativeLaunchRecipeSlotValue (nativePeerEdgeListenerSlot index))
                  (frameNativeState at)
                  (frameNativeState (nativePeerEndpointLengthAt at))
                  (nativeLaunchRecipeStore nativePeerScratchSlot))
                nativePeerScratchSlot
                b"peer-local-address"
                (nativeLaunchRecipeAssertEqual
                  (frameNativeLoad (nativePeerEndpointLengthAt at))
                  (nativeLaunchRecipeImmediate linuxIPv4SocketAddressBytes)
                  b"peer-local-address-extent"
                  tail))))))))

def nativePeerEdgeEstablish =
  (lambda unrestricted role : Nat .
    (lambda unrestricted base : Nat .
      (lambda unrestricted index : Nat .
        (lambda unrestricted edge : (family NativePeerEdge) .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (nativePeerEdgeWhenListening
              role
              edge
              (nativeSocketAcceptChecked
                (nativeLaunchRecipeSlotValue (nativePeerEdgeListenerSlot index))
                (nativeLaunchRecipeImmediate 30000)
                (nativeLaunchRecipeImmediate 64)
                (nativePeerEdgeConnectionSlot index)
                nativePeerScratchSlot
                (nativeSocketCloseChecked
                  (nativeLaunchRecipeSlotValue (nativePeerEdgeListenerSlot index))
                  nativePeerScratchSlot
                  tail))
              (nativeSocketOpenIPv4
                (nativePeerEdgeConnectionSlot index)
                nativePeerScratchSlot
                (nativeSocketConnectChecked
                  (nativeLaunchRecipeSlotValue (nativePeerEdgeConnectionSlot index))
                  (frameNativeState (nativePeerEdgeAddressAt base index))
                  (nativeLaunchRecipeImmediate 5000)
                  (nativeLaunchRecipeImmediate 64)
                  nativePeerScratchSlot
                  tail))))))))

def nativePeerEdgeSetup =
  (lambda unrestricted role : Nat .
    (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
      (lambda unrestricted base : Nat .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativePeerEdgesFold
            edges
            (lambda unrestricted index : Nat .
              (lambda unrestricted edge : (family NativePeerEdge) .
                (lambda unrestricted rest : (family NativePhysicalCommands) .
                  (frameNativeCopy
                    (nativePeerEdgeAddressAt base index)
                    (nativePeerEdgeAddressOf edge)
                    rest))))
            (nativePeerEdgesFold
              edges
              (lambda unrestricted index : Nat .
                (lambda unrestricted edge : (family NativePeerEdge) .
                  (lambda unrestricted rest : (family NativePhysicalCommands) .
                    (nativePeerEdgeWhenListening
                      role
                      edge
                      (nativePeerEdgeListen (nativePeerEdgeAddressAt base index) index rest)
                      rest))))
              (nativePeerEdgesFold
                edges
                (lambda unrestricted index : Nat .
                  (lambda unrestricted edge : (family NativePeerEdge) .
                    (lambda unrestricted rest : (family NativePhysicalCommands) .
                      (nativePeerEdgeWhenListening
                        role
                        edge
                        (nativePeerPortWrite (nativePeerEdgeAddressAt base index) rest)
                        rest))))
                (nativePeerEdgesFold
                  edges
                  (lambda unrestricted index : Nat .
                    (lambda unrestricted edge : (family NativePeerEdge) .
                      (lambda unrestricted rest : (family NativePhysicalCommands) .
                        (nativePeerEdgeEstablish role base index edge rest))))
                  tail))))))))

-- The connection slot of the edge to `peer`, or the scratch slot (which no
-- edge owns) when the participant has no such edge; admission of the caller's
-- topology must refuse that case before commands are generated.
def nativePeerEdgeConnectionTo =
  (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
    (lambda unrestricted peer : Nat .
      (stdListFold
        (family NativePeerEdge)
        (pi unrestricted index : Nat . Nat)
        (lambda unrestricted edge : (family NativePeerEdge) .
          (lambda unrestricted next : (pi unrestricted index : Nat . Nat) .
            (lambda unrestricted index : Nat .
              (naturalSelect
                (naturalEqual (nativePeerEdgePeerOf edge) peer)
                (nativePeerEdgeConnectionSlot index)
                (next (succ index))))))
        (lambda unrestricted index : Nat . nativePeerScratchSlot)
        edges
        0)))

-- Edges are admitted when their peers are distinct, strictly ascending,
-- differ from this role, and every address is one IPv4 socket address.
def nativePeerEdgesAdmitted =
  (lambda unrestricted role : Nat .
    (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
      (stdListFold
        (family NativePeerEdge)
        (pi unrestricted floor : Nat . Nat)
        (lambda unrestricted edge : (family NativePeerEdge) .
          (lambda unrestricted next : (pi unrestricted floor : Nat . Nat) .
            (lambda unrestricted floor : Nat .
              (naturalAnd
                (naturalLessOrEqual floor (nativePeerEdgePeerOf edge))
                (naturalAnd
                  (naturalIsZero (naturalEqual role (nativePeerEdgePeerOf edge)))
                  (naturalAnd
                    (naturalEqual
                      (bytes-length (nativePeerEdgeAddressOf edge))
                      linuxIPv4SocketAddressBytes)
                    (next (succ (nativePeerEdgePeerOf edge)))))))))
        (lambda unrestricted floor : Nat . 1)
        edges
        0)))

-- A star centred on role 0: role 0 has an edge to every other role, in
-- order, at `addresses`; every other role has one edge, to role 0, at its
-- one address.
def nativePeerStarEdges =
  (lambda unrestricted role : Nat .
    (lambda unrestricted addresses : (family StdList Bytes) .
      (stdListFold
        Bytes
        (pi unrestricted index : Nat . (family StdList (family NativePeerEdge)))
        (lambda unrestricted address : Bytes .
          (lambda unrestricted next : (pi unrestricted index : Nat . (family StdList (family NativePeerEdge))) .
            (lambda unrestricted index : Nat .
              (constructor
                StdList
                StdListCons
                (family NativePeerEdge)
                (constructor
                  NativePeerEdge
                  NativePeerEdgeOf
                  (naturalSelect (naturalIsZero role) (succ index) 0)
                  address)
                (next (succ index))))))
        (lambda unrestricted index : Nat . (constructor StdList StdListEmpty (family NativePeerEdge)))
        addresses
        0)))

-- A star of `owners` admits owner 0 with one address per other owner and
-- every other owner with exactly one address, all admitted edges.
def nativePeerStarAdmitted =
  (lambda unrestricted owners : Nat .
    (lambda unrestricted role : Nat .
      (lambda unrestricted addresses : (family StdList Bytes) .
        (naturalAnd
          (naturalLess role owners)
          (naturalAnd
            (naturalEqual
              (stdListLength Bytes addresses)
              (naturalSelect (naturalIsZero role) (naturalPredecessor owners) 1))
            (nativePeerEdgesAdmitted role (nativePeerStarEdges role addresses)))))))

-- The two-role pair: role 0 listens for role 1 at `address`, role 1
-- connects to it. Same commands, slots and state as one admitted edge.
def nativePeerEdgesOfPair =
  (lambda unrestricted worker : Nat .
    (lambda unrestricted address : Bytes .
      (constructor
        StdList
        StdListCons
        (family NativePeerEdge)
        (constructor
          NativePeerEdge
          NativePeerEdgeOf
          (naturalSelect (naturalIsZero worker) 1 0)
          address)
        (constructor StdList StdListEmpty (family NativePeerEdge)))))

def nativePeerSetup =
  (lambda unrestricted worker : Nat .
    (lambda unrestricted address : Bytes .
      (lambda unrestricted base : Nat .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativePeerEdgeSetup
            (naturalSelect (naturalIsZero worker) 0 1)
            (nativePeerEdgesOfPair worker address)
            base
            tail)))))

def nativePeerByRole =
  (lambda unrestricted worker : Nat .
    (lambda unrestricted coordinator : (family NativePhysicalCommands) .
      (lambda unrestricted participant : (family NativePhysicalCommands) .
        (nat-eliminate
          (lambda unrestricted role : Nat . (family NativePhysicalCommands))
          coordinator
          (lambda unrestricted previous : Nat .
            (lambda unrestricted ignored : (family NativePhysicalCommands) . participant))
          worker))))