module Runtime.RegionFrame

import Runtime.RegionTransfer
import Learning.Transition
import Representation.Partition
import Data.Bytes
import Data.SHA256
import Data.SHA256Digest
import Model.Parameter
import Model.Word64
import Std.Foundation
import Std.List
import Std.Natural

family RegionFrameFailure : Type 0
constructor RegionFrameBounds
constructor RegionFrameWrongHeader
constructor RegionFrameWrongExtent
constructor RegionFrameWrongDigest
constructor RegionFrameHashUnavailable
constructor RegionFrameWrongPhase

end-family

-- A scheduled receive already knows every identity and extent. It must compare
-- this canonical header before receiving the body into its admitted staging
-- region. No length, address, allocation or route is taken from peer bytes.
-- Version 1: magic/version, payload extent, four length-prefixed identities,
-- epoch, state version, operation, sender, receiver, interval begin/end. Words
-- are unsigned little-endian 64-bit. The trailer hashes header AND payload.
-- SHA-256 detects corruption; it does not authenticate an untrusted peer.
def regionFrameMagic =
  (bytes-append b"ALPXFER" (bytes 1))

def regionFrameWordLimit : Nat =
  18446744073709551615

def regionFrameDigestBytes : Nat =
  32

def regionFrameWord =
  (lambda unrestricted n : Nat . (dataBytesWord64LE (modelWord64FromNaturalTruncated n)))

def regionFrameSuccess =
  (lambda unrestricted value : Bytes .
    (constructor StdResult StdSuccess (family RegionFrameFailure) Bytes value))

def regionFrameFailure =
  (lambda unrestricted code : (family RegionFrameFailure) .
    (constructor StdResult StdFailure (family RegionFrameFailure) Bytes code))

-- Delaying the continuation makes bounds checks precede copying and hashing
-- in a strict native realization, as well as in the lazy checker.
def regionFrameRequire =
  (lambda unrestricted flag : Nat .
    (lambda unrestricted code : (family RegionFrameFailure) .
      (lambda unrestricted next : (pi unrestricted unit : Nat . (family StdResult (family RegionFrameFailure) Bytes)) .
        (nat-eliminate
          (lambda unrestricted n : Nat . (family StdResult (family RegionFrameFailure) Bytes))
          (regionFrameFailure code)
          (lambda unrestricted p : Nat .
            (lambda unrestricted ignored : (family StdResult (family RegionFrameFailure) Bytes) .
              (next 0)))
          flag))))

def regionFrameThen =
  (lambda unrestricted result : (family StdResult (family RegionFrameFailure) Bytes) .
    (lambda unrestricted next : (pi unrestricted value : Bytes . (family StdResult (family RegionFrameFailure) Bytes)) .
      (eliminate
        StdResult
        (lambda unrestricted current : (family StdResult (family RegionFrameFailure) Bytes) .
          (family StdResult (family RegionFrameFailure) Bytes))
        result
        (branch StdFailure code . (regionFrameFailure code))
        (branch StdSuccess value . (next value)))))

-- Check by subtraction before concatenation. In particular no sum of lengths
-- may wrap and turn an oversized header into a seemingly small allocation.
def regionFrameJoinWithin =
  (lambda unrestricted chunks : (family StdList Bytes) .
    (eliminate
      StdList
      (lambda unrestricted current : (family StdList Bytes) .
        (pi unrestricted budget : Nat . (family StdResult (family RegionFrameFailure) Bytes)))
      chunks
      (branch StdListEmpty . (lambda unrestricted budget : Nat . (regionFrameSuccess b"")))
      (branch
        StdListCons
        head
        tail
        induction
        .
        (lambda unrestricted budget : Nat .
          (regionFrameRequire
            (naturalLessOrEqual (bytes-length head) budget)
            (constructor RegionFrameFailure RegionFrameBounds)
            (lambda unrestricted delayed : Nat .
              (regionFrameThen
                (induction (naturalSaturatingSubtract budget (bytes-length head)))
                (lambda unrestricted rest : Bytes . (regionFrameSuccess (bytes-append head rest))))))))))

def regionFrameChunk =
  (lambda unrestricted value : Bytes .
    (lambda unrestricted tail : (family StdList Bytes) .
      (constructor StdList StdListCons Bytes value tail)))

def regionFrameName =
  (lambda unrestricted value : Bytes .
    (lambda unrestricted tail : (family StdList Bytes) .
      (regionFrameChunk (regionFrameWord (bytes-length value)) (regionFrameChunk value tail))))

def regionFrameNumber =
  (lambda unrestricted value : Nat .
    (lambda unrestricted tail : (family StdList Bytes) .
      (regionFrameChunk (regionFrameWord value) tail)))

-- The fixed route suffix is shared by encoding and offset derivation. Runtime
-- round patching therefore follows this schema, not copied byte constants.
def regionFrameRoute =
  (lambda unrestricted operation : Nat .
    (lambda unrestricted sender : Nat .
      (lambda unrestricted receiver : Nat .
        (lambda unrestricted begin : Nat .
          (lambda unrestricted end : Nat .
            (bytes-append
              (regionFrameWord operation)
              (bytes-append
                (regionFrameWord sender)
                (bytes-append
                  (regionFrameWord receiver)
                  (bytes-append (regionFrameWord begin) (regionFrameWord end))))))))))

def regionFrameVersionFromEnd =
  (bytes-length (bytes-append (regionFrameWord 0) (regionFrameRoute 0 0 0 0 0)))

def regionFrameEpochFromEnd =
  (naturalAdd (bytes-length (regionFrameWord 0)) regionFrameVersionFromEnd)

def regionFrameHeader =
  (lambda unrestricted identity : (family RegionTransferIdentity) .
    (lambda unrestricted payloadBytes : Nat .
      (lambda unrestricted headerBudget : Nat .
        (eliminate
          RegionTransferIdentity
          (lambda unrestricted current : (family RegionTransferIdentity) .
            (family StdResult (family RegionFrameFailure) Bytes))
          identity
          (branch
            RegionTransferIdentityOf
            composition
            run
            region
            representation
            round
            operation
            sender
            receiver
            interval
            .
            (eliminate
              LearningRound
              (lambda unrestricted current : (family LearningRound) .
                (family StdResult (family RegionFrameFailure) Bytes))
              round
              (branch
                LearningRoundOf
                epoch
                version
                .
                (regionFrameRequire
                  (naturalAnd
                    (naturalLessOrEqual headerBudget regionFrameWordLimit)
                    (naturalAnd
                      (naturalLessOrEqual payloadBytes regionFrameWordLimit)
                      (naturalAnd
                        (naturalLessOrEqual epoch regionFrameWordLimit)
                        (naturalAnd
                          (naturalLessOrEqual version regionFrameWordLimit)
                          (naturalAnd
                            (naturalLessOrEqual operation regionFrameWordLimit)
                            (naturalAnd
                              (naturalLessOrEqual sender regionFrameWordLimit)
                              (naturalAnd
                                (naturalLessOrEqual receiver regionFrameWordLimit)
                                (naturalAnd
                                  (naturalLessOrEqual (intervalEnd interval) regionFrameWordLimit)
                                  (naturalLessOrEqual
                                    (intervalBegin interval)
                                    (intervalEnd interval))))))))))
                  (constructor RegionFrameFailure RegionFrameBounds)
                  (lambda unrestricted delayed : Nat .
                    (regionFrameJoinWithin
                      (regionFrameChunk
                        regionFrameMagic
                        (regionFrameNumber
                          payloadBytes
                          (regionFrameName
                            composition
                            (regionFrameName
                              run
                              (regionFrameName
                                region
                                (regionFrameName
                                  representation
                                  (regionFrameNumber
                                    epoch
                                    (regionFrameNumber
                                      version
                                      (regionFrameChunk
                                        (regionFrameRoute
                                        operation
                                        sender
                                        receiver
                                        (intervalBegin interval)
                                        (intervalEnd interval))
                                        (constructor StdList StdListEmpty Bytes))))))))))
                      headerBudget))))))))))

def regionFrameHash =
  (lambda unrestricted bytes : Bytes .
    (eliminate
      SHA256Result
      (lambda unrestricted current : (family SHA256Result) .
        (family StdResult (family RegionFrameFailure) Bytes))
      (sha256Bytes bytes)
      (branch SHA256Succeeded digest . (regionFrameSuccess (sha256DigestToBytes digest)))
      (branch
        SHA256Failed
        code
        .
        (regionFrameFailure (constructor RegionFrameFailure RegionFrameHashUnavailable)))))

def encodeRegionFrame =
  (lambda unrestricted identity : (family RegionTransferIdentity) .
    (lambda unrestricted headerBudget : Nat .
      (lambda unrestricted payloadBudget : Nat .
        (lambda unrestricted payload : Bytes .
          (regionFrameRequire
            (naturalLessOrEqual (bytes-length payload) payloadBudget)
            (constructor RegionFrameFailure RegionFrameBounds)
            (lambda unrestricted delayed : Nat .
              (regionFrameThen
                (regionFrameHeader identity (bytes-length payload) headerBudget)
                (lambda unrestricted header : Bytes .
                  (regionFrameRequire
                    (naturalAnd
                      (naturalLessOrEqual
                        (bytes-length header)
                        (naturalSaturatingSubtract regionFrameWordLimit regionFrameDigestBytes))
                      (naturalLessOrEqual
                        (bytes-length payload)
                        (naturalSaturatingSubtract
                          (naturalSaturatingSubtract regionFrameWordLimit regionFrameDigestBytes)
                          (bytes-length header))))
                    (constructor RegionFrameFailure RegionFrameBounds)
                    (lambda unrestricted delayed : Nat .
                      (let unrestricted content =
                        (bytes-append header payload)
                        in
                        (regionFrameThen
                          (regionFrameHash content)
                          (lambda unrestricted digest : Bytes .
                            (regionFrameSuccess (bytes-append content digest)))))))))))))))

-- This decoder is for a bounded scheduled frame, not a discovery protocol.
-- It rejects trailing bytes as well as truncation and binds the digest to the
-- complete scope. Native framing reads the expected header and body extents
-- separately; this pure boundary validates the completed immutable bytes.
def decodeRegionFrame =
  (lambda unrestricted identity : (family RegionTransferIdentity) .
    (lambda unrestricted expectedBytes : Nat .
      (lambda unrestricted headerBudget : Nat .
        (lambda unrestricted frame : Bytes .
          (regionFrameThen
            (regionFrameHeader identity expectedBytes headerBudget)
            (lambda unrestricted header : Bytes .
              (regionFrameRequire
                (naturalAnd
                  (naturalLessOrEqual regionFrameDigestBytes (bytes-length frame))
                  (naturalAnd
                    (naturalLessOrEqual
                      (bytes-length header)
                      (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes))
                    (naturalEqual
                      expectedBytes
                      (naturalSaturatingSubtract
                        (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes)
                        (bytes-length header)))))
                (constructor RegionFrameFailure RegionFrameWrongExtent)
                (lambda unrestricted delayed : Nat .
                  (regionFrameRequire
                    (bytes-equal header (dataBytesTakeValidated (bytes-length header) frame))
                    (constructor RegionFrameFailure RegionFrameWrongHeader)
                    (lambda unrestricted delayed : Nat .
                      (let unrestricted contentBytes =
                        (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes)
                        in
                        (regionFrameThen
                          (regionFrameHash (dataBytesTakeValidated contentBytes frame))
                          (lambda unrestricted digest : Bytes .
                            (regionFrameRequire
                              (bytes-equal digest (dataBytesDropValidated contentBytes frame))
                              (constructor RegionFrameFailure RegionFrameWrongDigest)
                              (lambda unrestricted delayed : Nat .
                                (regionFrameSuccess
                                  (dataBytesTakeValidated
                                    expectedBytes
                                    (dataBytesDropValidated (bytes-length header) frame))))))))))))))))))

def receiveRegionFrame =
  (lambda unrestricted identity : (family RegionTransferIdentity) .
    (lambda unrestricted expectedBytes : Nat .
      (lambda unrestricted headerBudget : Nat .
        (lambda unrestricted phase : (family TransferPhase) .
          (lambda unrestricted frame : Bytes .
            (regionFrameRequire
              (naturalEqual (transferPhaseCode phase) 2)
              (constructor RegionFrameFailure RegionFrameWrongPhase)
              (lambda unrestricted delayed : Nat .
                (decodeRegionFrame identity expectedBytes headerBudget frame))))))))