module Compiler.Planning.RegionFrame

import Runtime.RegionTransfer
import Runtime.RegionFrame
import Runtime.WordDigest
import Runtime.ArenaCertificate
import Data.SHA256
import Data.SHA256Padding
import Model.Parameter
import Model.Word64
import Std.Foundation
import Std.Natural

-- One content region is reused for SHA padding AFTER the trailer has been
-- received separately. Padding can never overwrite the transmitted digest.
family RegionFrameLayout : Type 0
constructor RegionFrameLayoutOf
field unrestricted frameLayoutHeader : Bytes
field unrestricted frameLayoutPayloadBytes : Nat
field unrestricted frameLayoutBase : Nat
field unrestricted frameLayoutPadding : Bytes

end-family

family RegionFrameLayoutFailure : Type 0
constructor RegionFrameLayoutHeaderRejected
constructor RegionFrameLayoutPaddingRejected
constructor RegionFrameLayoutBoundsRejected

end-family

def frameHeader =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (eliminate
      RegionFrameLayout
      (lambda unrestricted current : (family RegionFrameLayout) . Bytes)
      layout
      (branch RegionFrameLayoutOf header payload base padding . header)))

def framePayloadBytes =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (eliminate
      RegionFrameLayout
      (lambda unrestricted current : (family RegionFrameLayout) . Nat)
      layout
      (branch RegionFrameLayoutOf header payload base padding . payload)))

def frameBase =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (eliminate
      RegionFrameLayout
      (lambda unrestricted current : (family RegionFrameLayout) . Nat)
      layout
      (branch RegionFrameLayoutOf header payload base padding . base)))

def framePadding =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (eliminate
      RegionFrameLayout
      (lambda unrestricted current : (family RegionFrameLayout) . Bytes)
      layout
      (branch RegionFrameLayoutOf header payload base padding . padding)))

def frameAlign =
  (lambda unrestricted extent : Nat .
    (naturalMultiply
      digestWorkAlignment
      (naturalDivideUnchecked
        (naturalAdd extent (naturalSaturatingSubtract digestWorkAlignment 1))
        digestWorkAlignment)))

def frameContentBytes =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (bytes-length (frameHeader layout)) (framePayloadBytes layout)))

def framePaddedBytes =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameContentBytes layout) (bytes-length (framePadding layout))))

def frameBlockCount =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalDivideUnchecked (framePaddedBytes layout) digestBlockBytes))

def frameExpectedRelative =
  (lambda unrestricted layout : (family RegionFrameLayout) . (framePaddedBytes layout))

def frameReceivedRelative =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameExpectedRelative layout) (bytes-length (frameHeader layout))))

def frameComputedRelative =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameReceivedRelative layout) regionFrameDigestBytes))

def frameWorkRelative =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (frameAlign (naturalAdd (frameComputedRelative layout) regionFrameDigestBytes)))

def framePhaseRelative =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameWorkRelative layout) digestWorkBytes))

def frameStorageBytes =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (framePhaseRelative layout) digestAddressBytes))

def frameHeaderAt =
  (lambda unrestricted layout : (family RegionFrameLayout) . (frameBase layout))

def framePayloadAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameBase layout) (bytes-length (frameHeader layout))))

def framePaddingAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameBase layout) (frameContentBytes layout)))

def frameExpectedAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameBase layout) (frameExpectedRelative layout)))

-- These are offsets in a locally constructed, admitted canonical header.
-- Peer-provided lengths never participate in their derivation.
def frameExpectedVersionAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd
      (frameExpectedAt layout)
      (naturalSaturatingSubtract (bytes-length (frameHeader layout)) regionFrameVersionFromEnd)))

def frameExpectedEpochAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd
      (frameExpectedAt layout)
      (naturalSaturatingSubtract (bytes-length (frameHeader layout)) regionFrameEpochFromEnd)))

def frameReceivedAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameBase layout) (frameReceivedRelative layout)))

def frameComputedAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameBase layout) (frameComputedRelative layout)))

def frameWorkAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameBase layout) (frameWorkRelative layout)))

def framePhaseAt =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameBase layout) (framePhaseRelative layout)))

def frameEnd =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (naturalAdd (frameBase layout) (frameStorageBytes layout)))

def frameLayoutResidents =
  (lambda unrestricted layout : (family RegionFrameLayout) .
    (constructor
      ArenaResidents
      ArenaResidentsNext
      (constructor
        ArenaResident
        ArenaResidentValue
        b"frame-content-and-padding"
        (frameHeaderAt layout)
        (framePaddedBytes layout)
        1)
      (constructor
        ArenaResidents
        ArenaResidentsNext
        (constructor
          ArenaResident
          ArenaResidentValue
          b"frame-expected-header"
          (frameExpectedAt layout)
          (bytes-length (frameHeader layout))
          1)
        (constructor
          ArenaResidents
          ArenaResidentsNext
          (constructor
            ArenaResident
            ArenaResidentValue
            b"frame-received-digest"
            (frameReceivedAt layout)
            regionFrameDigestBytes
            1)
          (constructor
            ArenaResidents
            ArenaResidentsNext
            (constructor
              ArenaResident
              ArenaResidentValue
              b"frame-computed-digest"
              (frameComputedAt layout)
              regionFrameDigestBytes
              1)
            (constructor
              ArenaResidents
              ArenaResidentsNext
              (constructor
                ArenaResident
                ArenaResidentValue
                b"frame-hash-work"
                (frameWorkAt layout)
                digestWorkBytes
                digestWorkAlignment)
              (constructor
                ArenaResidents
                ArenaResidentsNext
                (constructor
                  ArenaResident
                  ArenaResidentValue
                  b"frame-phase"
                  (framePhaseAt layout)
                  digestAddressBytes
                  digestAddressBytes)
                (constructor ArenaResidents ArenaResidentsEnd))))))))

-- Admission compares a derived extent with available capacity; the executable
-- allocates exactly frameEnd. Base alignment makes the shared relative layout
-- independent of an earlier role's placement. Subtraction avoids base overflow.
def frameLayoutFits =
  (lambda unrestricted available : Nat .
    (lambda unrestricted layout : (family RegionFrameLayout) .
      (naturalAnd
        (naturalLessOrEqual available regionFrameWordLimit)
        (naturalAnd
          (naturalIsZero (naturalModuloUnchecked (frameBase layout) digestWorkAlignment))
          (naturalAnd
            (naturalLessOrEqual (frameBase layout) available)
            (naturalLessOrEqual
              (frameStorageBytes layout)
              (naturalSaturatingSubtract available (frameBase layout))))))))

def planRegionFrameLayout =
  (lambda unrestricted identity : (family RegionTransferIdentity) .
    (lambda unrestricted payloadBytes : Nat .
      (lambda unrestricted headerBudget : Nat .
        (lambda unrestricted base : Nat .
          (lambda unrestricted available : Nat .
            (eliminate
              StdResult
              (lambda unrestricted current : (family StdResult (family RegionFrameFailure) Bytes) .
                (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)))
              (regionFrameHeader identity payloadBytes headerBudget)
              (branch
                StdFailure
                code
                .
                (constructor
                  StdResult
                  StdFailure
                  (family RegionFrameLayoutFailure)
                  (family RegionFrameLayout)
                  (constructor RegionFrameLayoutFailure RegionFrameLayoutHeaderRejected)))
              (branch
                StdSuccess
                header
                .
                (nat-eliminate
                  (lambda unrestricted valid : Nat .
                    (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)))
                  (constructor
                    StdResult
                    StdFailure
                    (family RegionFrameLayoutFailure)
                    (family RegionFrameLayout)
                    (constructor RegionFrameLayoutFailure RegionFrameLayoutBoundsRejected))
                  (lambda unrestricted previous : Nat .
                    (lambda unrestricted ignored : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
                      (eliminate
                        StdResult
                        (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) .
                          (family
                            StdResult
                            (family RegionFrameLayoutFailure)
                            (family RegionFrameLayout)))
                        (sha256PaddingSuffix (naturalAdd (bytes-length header) payloadBytes))
                        (branch
                          StdFailure
                          code
                          .
                          (constructor
                            StdResult
                            StdFailure
                            (family RegionFrameLayoutFailure)
                            (family RegionFrameLayout)
                            (constructor RegionFrameLayoutFailure RegionFrameLayoutPaddingRejected)))
                        (branch
                          StdSuccess
                          padding
                          .
                          (let unrestricted layout : (family RegionFrameLayout) =
                            (constructor
                              RegionFrameLayout
                              RegionFrameLayoutOf
                              header
                              payloadBytes
                              base
                              padding)
                            in
                            (nat-eliminate
                              (lambda unrestricted fits : Nat .
                                (family
                                  StdResult
                                  (family RegionFrameLayoutFailure)
                                  (family RegionFrameLayout)))
                              (constructor
                                StdResult
                                StdFailure
                                (family RegionFrameLayoutFailure)
                                (family RegionFrameLayout)
                                (constructor
                                  RegionFrameLayoutFailure
                                  RegionFrameLayoutBoundsRejected))
                              (lambda unrestricted previous : Nat .
                                (lambda unrestricted ignored : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
                                  (constructor
                                    StdResult
                                    StdSuccess
                                    (family RegionFrameLayoutFailure)
                                    (family RegionFrameLayout)
                                    layout)))
                              (frameLayoutFits available layout)))))))
                  (naturalAnd
                    (naturalLessOrEqual
                      (bytes-length header)
                      (modelWord64Natural sha256MaximumInputBytes))
                    (naturalLessOrEqual
                      payloadBytes
                      (naturalSaturatingSubtract
                        (modelWord64Natural sha256MaximumInputBytes)
                        (bytes-length header))))))))))))