module Runtime.NativeResourcePlan

import Runtime.NativePhysicalMemory
import Runtime.NativePhysicalProgram
import Execution.ResourceGraph
import Compiler.Planning.Resources
import Model.Parameter
import Model.Word64
import Std.Foundation
import Std.List
import Std.Natural

-- Deployment facts and existing allocations are separate from the program.
-- This context admits only the interpreter's owned mapping. Image/stack,
-- syscall-created mappings and target buffers require their own derived leases.
family NativeResourceContext : Type 0
constructor NativeResourceContextOf
field unrestricted nativeResourceSchedule : (family ResourceSchedule)
field unrestricted nativeResourceAllocationIdentity : Bytes
field unrestricted nativeResourceEndpoint : Nat
field unrestricted nativeResourceDomain : Nat
field unrestricted nativeResourceMappingQuantum : Nat
field unrestricted nativeResourceEntryBudget : Nat
field unrestricted nativeResourcePairBudget : Nat

end-family

family NativeResourceFailure : Type 0
constructor NativeResourceMemoryFailed
field unrestricted nativeResourceMemoryFailure : (family NativePhysicalMemoryFailure)
constructor NativeResourceAdmissionFailed
field unrestricted nativeResourceAdmissionFailure : (family ResourceFailure)

end-family

def nativePhysicalProgramMemory =
  (lambda unrestricted program : (family NativePhysicalProgram) .
    (eliminate
      NativePhysicalProgram
      (lambda unrestricted current : (family NativePhysicalProgram) .
        (family StdResult (family NativePhysicalMemoryFailure) (family NativePhysicalMemoryLayout)))
      program
      (branch
        NativePhysicalProgramValue
        state
        slots
        commands
        expected
        identity
        fallbacks
        .
        (planNativePhysicalMemory (modelWord64Natural state) (modelWord64Natural slots)))))

-- Charge one owned allocation, rounded independently of its neighbors. An
-- alias is not an allocation; target inventories omit it before this step.
def nativeMemoryLease =
  (lambda unrestricted identity : Bytes .
    (lambda unrestricted endpoint : Nat .
      (lambda unrestricted domain : Nat .
        (lambda unrestricted quantum : Nat .
          (lambda unrestricted extent : Nat .
            (eliminate
              StdResult
              (lambda unrestricted current : (family StdResult (family NativePhysicalMemoryFailure) Nat) .
                (family StdResult (family NativePhysicalMemoryFailure) (family ResourceLease)))
              (nativeMemoryMappedBytes quantum extent)
              (branch
                StdFailure
                error
                .
                (constructor
                  StdResult
                  StdFailure
                  (family NativePhysicalMemoryFailure)
                  (family ResourceLease)
                  error))
              (branch
                StdSuccess
                bytes
                .
                (constructor
                  StdResult
                  StdSuccess
                  (family NativePhysicalMemoryFailure)
                  (family ResourceLease)
                  (constructor
                    ResourceLease
                    ResourceLeaseOf
                    identity
                    endpoint
                    domain
                    (constructor ResourceUnit ResourceMemoryBytes)
                    bytes
                    0
                    1)))))))))

def nativeResourceContextAddLeases =
  (lambda unrestricted context : (family NativeResourceContext) .
    (lambda unrestricted additional : (family StdList (family ResourceLease)) .
      (eliminate
        NativeResourceContext
        (lambda unrestricted current : (family NativeResourceContext) .
          (family NativeResourceContext))
        context
        (branch
          NativeResourceContextOf
          schedule
          identity
          endpoint
          domain
          quantum
          entries
          pairs
          .
          (constructor
            NativeResourceContext
            NativeResourceContextOf
            (constructor
              ResourceSchedule
              ResourceScheduleOf
              (resourceScheduleGraph schedule)
              (resourceSchedulePlacements schedule)
              (stdListAppend (family ResourceLease) additional (resourceScheduleLeases schedule)))
            identity
            endpoint
            domain
            quantum
            entries
            pairs)))))

-- One allocation is charged once, including holes/alignment and result/scratch
-- storage. Frame and checkpoint residents are already inside the state extent:
-- summing them again would double-charge the same physical pages.
-- The conservative [0,1) epoch is the whole cooperating execution, not host time.
def nativePhysicalInterpreterLease =
  (lambda unrestricted identity : Bytes .
    (lambda unrestricted endpoint : Nat .
      (lambda unrestricted domain : Nat .
        (lambda unrestricted quantum : Nat .
          (lambda unrestricted program : (family NativePhysicalProgram) .
            (stdResultBind
              (family NativePhysicalMemoryFailure)
              (family NativePhysicalMemoryLayout)
              (family ResourceLease)
              (nativePhysicalProgramMemory program)
              (lambda unrestricted layout : (family NativePhysicalMemoryLayout) .
                (nativeMemoryLease
                  identity
                  endpoint
                  domain
                  quantum
                  (nativePhysicalMemoryBytes layout)))))))))

def admitNativePhysicalResources =
  (lambda unrestricted context : (family NativeResourceContext) .
    (lambda unrestricted program : (family NativePhysicalProgram) .
      (eliminate
        NativeResourceContext
        (lambda unrestricted current : (family NativeResourceContext) .
          (family StdResult (family NativeResourceFailure) (family ResourceSchedule)))
        context
        (branch
          NativeResourceContextOf
          schedule
          identity
          endpoint
          domain
          quantum
          entries
          pairs
          .
          (eliminate
            StdResult
            (lambda unrestricted current : (family StdResult (family NativePhysicalMemoryFailure) (family ResourceLease)) .
              (family StdResult (family NativeResourceFailure) (family ResourceSchedule)))
            (nativePhysicalInterpreterLease identity endpoint domain quantum program)
            (branch
              StdFailure
              reason
              .
              (constructor
                StdResult
                StdFailure
                (family NativeResourceFailure)
                (family ResourceSchedule)
                (constructor NativeResourceFailure NativeResourceMemoryFailed reason)))
            (branch
              StdSuccess
              lease
              .
              (eliminate
                StdResult
                (lambda unrestricted current : (family StdResult (family ResourceFailure) (family ResourceSchedule)) .
                  (family StdResult (family NativeResourceFailure) (family ResourceSchedule)))
                (admitResourceSchedule
                  entries
                  pairs
                  (constructor
                    ResourceSchedule
                    ResourceScheduleOf
                    (resourceScheduleGraph schedule)
                    (resourceSchedulePlacements schedule)
                    (constructor
                      StdList
                      StdListCons
                      (family ResourceLease)
                      lease
                      (resourceScheduleLeases schedule))))
                (branch
                  StdFailure
                  reason
                  .
                  (constructor
                    StdResult
                    StdFailure
                    (family NativeResourceFailure)
                    (family ResourceSchedule)
                    (constructor NativeResourceFailure NativeResourceAdmissionFailed reason)))
                (branch
                  StdSuccess
                  admitted
                  .
                  (constructor
                    StdResult
                    StdSuccess
                    (family NativeResourceFailure)
                    (family ResourceSchedule)
                    admitted)))))))))

def nativePhysicalResourcesAdmitted =
  (lambda unrestricted context : (family NativeResourceContext) .
    (lambda unrestricted program : (family NativePhysicalProgram) .
      (stdBoolToNatural
        (stdResultIsSuccess
          (family NativeResourceFailure)
          (family ResourceSchedule)
          (admitNativePhysicalResources context program)))))

-- One native host process reserving `budget` bytes for its interpreter
-- mapping: the context a single-participant host pairing admits against.
-- `kind` names the executor (for example b"x86-64-native" or
-- b"aarch64-native"); it is evidence naming the target, not a capability the
-- admission checks.
def nativeSingleHostResources =
  (lambda unrestricted name : Bytes .
    (lambda unrestricted kind : Bytes .
      (lambda unrestricted budget : Nat .
        (constructor
          NativeResourceContext
          NativeResourceContextOf
          (constructor
            ResourceSchedule
            ResourceScheduleOf
            (constructor
              ResourceGraph
              ResourceGraphOf
              (constructor
                StdList
                StdListCons
                (family ResourceEndpoint)
                (constructor
                  ResourceEndpoint
                  ResourceEndpointOf
                  0
                  name
                  kind
                  (constructor
                    StdList
                    StdListCons
                    Bytes
                    b"native-interpreter"
                    (constructor StdList StdListEmpty Bytes))
                  (constructor StdList StdListCons Nat 0 (constructor StdList StdListEmpty Nat)))
                (constructor StdList StdListEmpty (family ResourceEndpoint)))
              (constructor
                StdList
                StdListCons
                (family ResourceDomain)
                (constructor
                  ResourceDomain
                  ResourceCapacityDomain
                  0
                  (bytes-append name b"-interpreter-reservation")
                  (constructor ResourceUnit ResourceMemoryBytes)
                  (constructor
                    ResourceFact
                    ResourceEstablished
                    budget
                    b"qualification-process-reservation"))
                (constructor StdList StdListEmpty (family ResourceDomain)))
              (constructor StdList StdListEmpty (family ResourceLink)))
            (constructor StdList StdListEmpty (family ResourcePlacement))
            (constructor StdList StdListEmpty (family ResourceLease)))
          (bytes-append name b"-interpreter")
          0
          0
          4096
          16
          256))))