module Runtime.NativePhysicalMemory

import Data.Bytes
import Model.Parameter
import Model.Word64
import Std.Foundation
import Std.Natural

-- The interpreter's allocation contains program state, result words, then
-- repeat and wait state. Both native hosts implement this same layout.
-- Keep this ABI independent of the program/target owners so admission, memory
-- reservations and machine emitters share one calculation.
family NativePhysicalMemoryLayout : Type 0
constructor NativePhysicalMemoryLayoutOf
field unrestricted nativePhysicalMemoryStateBytes : Nat
field unrestricted nativePhysicalMemorySlotBytes : Nat
field unrestricted nativePhysicalMemoryScratchOffset : Nat
field unrestricted nativePhysicalMemoryAllocationBytes : Nat

end-family

family NativePhysicalMemoryFailure : Type 0
constructor NativePhysicalMemoryEmpty
constructor NativePhysicalMemoryOverflow
constructor NativePhysicalMemoryPageInvalid

end-family

def nativePhysicalMemoryWordLimit =
  18446744073709551615

def nativePhysicalMemoryWordBytes =
  (bytes-length (dataBytesWord64LE (modelWord64FromNaturalTruncated 0)))

-- The ISA shift implementing multiplication by one ABI word; checked below.
def nativePhysicalMemoryWordShift =
  3

def nativePhysicalMemoryIterationOffset =
  0

def nativePhysicalMemoryCountOffset =
  (naturalAdd nativePhysicalMemoryIterationOffset nativePhysicalMemoryWordBytes)

def nativePhysicalMemoryBodyOffset =
  (naturalAdd nativePhysicalMemoryCountOffset nativePhysicalMemoryWordBytes)

def nativePhysicalMemoryBodyCountOffset =
  (naturalAdd nativePhysicalMemoryBodyOffset nativePhysicalMemoryWordBytes)

def nativePhysicalMemoryWaitSecondsOffset =
  (naturalAdd nativePhysicalMemoryBodyCountOffset nativePhysicalMemoryWordBytes)

def nativePhysicalMemoryWaitNanosOffset =
  (naturalAdd nativePhysicalMemoryWaitSecondsOffset nativePhysicalMemoryWordBytes)

def nativePhysicalMemoryScratchBytes =
  (naturalAdd nativePhysicalMemoryWaitNanosOffset nativePhysicalMemoryWordBytes)

def nativePhysicalMemoryAdmitted =
  (lambda unrestricted state : Nat .
    (lambda unrestricted slots : Nat .
      (naturalAnd
        (naturalNonzero state)
        (naturalAnd
          (naturalLessOrEqual
            state
            (naturalSaturatingSubtract
              nativePhysicalMemoryWordLimit
              nativePhysicalMemoryScratchBytes))
          (naturalLessOrEqual
            slots
            (naturalDivideUnchecked
              (naturalSaturatingSubtract
                (naturalSaturatingSubtract
                  nativePhysicalMemoryWordLimit
                  nativePhysicalMemoryScratchBytes)
                state)
              nativePhysicalMemoryWordBytes))))))

def planNativePhysicalMemory =
  (lambda unrestricted state : Nat .
    (lambda unrestricted slots : Nat .
      (eliminate
        StdBool
        (lambda unrestricted flag : (family StdBool) .
          (family
            StdResult
            (family NativePhysicalMemoryFailure)
            (family NativePhysicalMemoryLayout)))
        (stdBoolFromNatural (naturalNonzero state))
        (branch
          StdTrue
          .
          (eliminate
            StdBool
            (lambda unrestricted flag : (family StdBool) .
              (family
                StdResult
                (family NativePhysicalMemoryFailure)
                (family NativePhysicalMemoryLayout)))
            (stdBoolFromNatural (nativePhysicalMemoryAdmitted state slots))
            (branch
              StdTrue
              .
              (let unrestricted slotBytes =
                (naturalMultiply slots nativePhysicalMemoryWordBytes)
                in
                (let unrestricted scratch =
                  (naturalAdd state slotBytes)
                  in
                  (constructor
                    StdResult
                    StdSuccess
                    (family NativePhysicalMemoryFailure)
                    (family NativePhysicalMemoryLayout)
                    (constructor
                      NativePhysicalMemoryLayout
                      NativePhysicalMemoryLayoutOf
                      state
                      slotBytes
                      scratch
                      (naturalAdd scratch nativePhysicalMemoryScratchBytes))))))
            (branch
              StdFalse
              .
              (constructor
                StdResult
                StdFailure
                (family NativePhysicalMemoryFailure)
                (family NativePhysicalMemoryLayout)
                (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow)))))
        (branch
          StdFalse
          .
          (constructor
            StdResult
            StdFailure
            (family NativePhysicalMemoryFailure)
            (family NativePhysicalMemoryLayout)
            (constructor NativePhysicalMemoryFailure NativePhysicalMemoryEmpty))))))

def nativePhysicalMemoryBytes =
  (lambda unrestricted layout : (family NativePhysicalMemoryLayout) .
    (eliminate
      NativePhysicalMemoryLayout
      (lambda unrestricted current : (family NativePhysicalMemoryLayout) . Nat)
      layout
      (branch NativePhysicalMemoryLayoutOf state slots scratch bytes . bytes)))

-- Mapping granularity is a platform/deployment fact, never guessed from a
-- neighboring host. This accepts a positive declared quantum; its provenance
-- and agreement with the actual OS mapping remain the target's responsibility.
def nativeMemoryMappedBytes =
  (lambda unrestricted quantum : Nat .
    (lambda unrestricted bytes : Nat .
      (eliminate
        StdBool
        (lambda unrestricted flag : (family StdBool) .
          (family StdResult (family NativePhysicalMemoryFailure) Nat))
        (stdBoolFromNatural
          (naturalAnd
            (naturalNonzero quantum)
            (naturalAnd
              (naturalLessOrEqual quantum nativePhysicalMemoryWordLimit)
              (naturalAnd
                (naturalNonzero bytes)
                (naturalLessOrEqual bytes nativePhysicalMemoryWordLimit)))))
        (branch
          StdTrue
          .
          (let unrestricted pages =
            (naturalAdd (naturalDivideUnchecked (naturalSaturatingSubtract bytes 1) quantum) 1)
            in
            (eliminate
              StdBool
              (lambda unrestricted flag : (family StdBool) .
                (family StdResult (family NativePhysicalMemoryFailure) Nat))
              (stdBoolFromNatural
                (naturalLessOrEqual
                  pages
                  (naturalDivideUnchecked nativePhysicalMemoryWordLimit quantum)))
              (branch
                StdTrue
                .
                (constructor
                  StdResult
                  StdSuccess
                  (family NativePhysicalMemoryFailure)
                  Nat
                  (naturalMultiply pages quantum)))
              (branch
                StdFalse
                .
                (constructor
                  StdResult
                  StdFailure
                  (family NativePhysicalMemoryFailure)
                  Nat
                  (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow))))))
        (branch
          StdFalse
          .
          (constructor
            StdResult
            StdFailure
            (family NativePhysicalMemoryFailure)
            Nat
            (constructor NativePhysicalMemoryFailure NativePhysicalMemoryPageInvalid))))))

def nativePhysicalMemoryMappedBytes =
  (lambda unrestricted quantum : Nat .
    (lambda unrestricted layout : (family NativePhysicalMemoryLayout) .
      (nativeMemoryMappedBytes quantum (nativePhysicalMemoryBytes layout))))

def nativePhysicalMemoryWordShiftLaw :
  (equal Nat (naturalPowerOfTwo nativePhysicalMemoryWordShift) nativePhysicalMemoryWordBytes) =
  (refl Nat 8)