module Platform.AArch64.WordDigest

import Compiler.MachineAArch64
import Compiler.MachineAArch64Assembly
import Model.Config
import Platform.AArch64.RoutineEmitter
import Runtime.WordDigest
import Std.Natural

-- AAPCS64 emitter for shared word digest and ALPHATEL sealing. Arguments occupy
-- x0..x5; all other values fit in caller-saved x6..x14. x16 is exclusively an
-- address scratch and x17 an immediate scratch; x18 and callee-saved registers
-- are untouched. The interpreter also retains image state in x12..x14 across
-- inline calls. The shared algorithm saves/restores those registers through
-- its R13/R14/R15 roles; this custom runtime requirement is stronger than
-- AAPCS64 and those saves must not be removed as redundant.
-- Form addresses before loads/stores so the clock field at byte 13 is handled
-- as an unaligned access, without truncating an A64 scaled displacement.
def digestAArch64JumpIf =
  (lambda unrestricted condition : (family WordDigestCondition) .
    (lambda unrestricted name : Bytes .
      (lambda unrestricted rest : (family AArch64Assembly) .
        (constructor
          AArch64Assembly
          AArch64AssemblyBranchIf
          (eliminate
            WordDigestCondition
            (lambda unrestricted current : (family WordDigestCondition) . (family AArch64Condition))
            condition
            (branch WordDigestBelow . (constructor AArch64Condition AArch64CarryClear))
            (branch WordDigestNotZero . (constructor AArch64Condition AArch64NotEqual))
            (branch WordDigestZero . (constructor AArch64Condition AArch64Equal))
            (branch WordDigestNegative . (constructor AArch64Condition AArch64Minus)))
          name
          rest))))

def aarch64WordDigestBackendFor =
  (lambda unrestricted return : (pi unrestricted tail : (family AArch64Assembly) . (family AArch64Assembly)) .
    (constructor
      WordDigestBackend
      WordDigestBackendValue
      (family AArch64Assembly)
      (family AArch64Register)
      ahrLoad32
      ahrLoad64
      ahrLoad8
      ahrStore32
      ahrStore64
      ahrStore8
      ahrMov
      ahrAdd
      ahrAnd
      ahrOr
      ahrXor
      ahrShl
      ahrShr
      ahrMovImm
      ahrAddImm
      ahrAndImm
      ahrCmpImm
      ahrMulImm
      ahrLabel
      digestAArch64JumpIf
      return
      ahrEnd
      ahrX6
      ahrX7
      ahrX3
      ahrX2
      ahrX1
      ahrX0
      ahrX8
      ahrX4
      ahrX5
      ahrX9
      ahrX10
      ahrX11
      ahrX12
      ahrX13
      ahrX14))

-- The existing seal has a void result, so keep its emission unchanged. Raw
-- digest returns a byte count: the abstract RAX lives in x6, whereas AAPCS64
-- and NativePhysicalRuntime consume the return value in x0.
def aarch64WordDigestBackend =
  (aarch64WordDigestBackendFor ahrReturn)

def aarch64WordDigestReturn =
  (lambda unrestricted tail : (family AArch64Assembly) . (ahrMov ahrX0 ahrX6 (ahrReturn tail)))

def aarch64WordDigestAssembly : (family AArch64Assembly) =
  (wordDigestAssemblyFor
    (family AArch64Assembly)
    (family AArch64Register)
    (aarch64WordDigestBackendFor aarch64WordDigestReturn))

def aarch64WordDigestRoutine : Bytes =
  (aarch64RoutineBytes aarch64WordDigestAssembly)

-- Select the same byte-padding algorithm with AAPCS64 register assignments.
-- Refusal returns directly in x0; successful padding retains x0/x2/x5 for
-- block compression and never touches the interpreter's x12..x14 state.
def aarch64ByteDigestAssembly : (family AArch64Assembly) =
  (constructor
    AArch64Assembly
    AArch64AssemblyBranch
    b"byte-digest-entry"
    (ahrLabel
      b"byte-digest-refused"
      (ahrMovImm
        ahrX0
        0
        (ahrReturn
          (ahrLabel
            b"byte-digest-entry"
            (wordDigestBytePaddingFor
              (family AArch64Assembly)
              (family AArch64Register)
              (aarch64WordDigestBackendFor aarch64WordDigestReturn)
              ahrX1
              aarch64WordDigestAssembly))))))

def aarch64ByteDigestRoutine : Bytes =
  (aarch64RoutineBytes aarch64ByteDigestAssembly)

def aarch64WordDigestContinueAssembly =
  (wordDigestContinueAssemblyFor
    (family AArch64Assembly)
    (family AArch64Register)
    (aarch64WordDigestBackendFor aarch64WordDigestReturn))

def aarch64WordDigestContinueRoutine : Bytes =
  (aarch64RoutineBytes aarch64WordDigestContinueAssembly)

def aarch64ByteDigestStreamStartAssembly =
  (wordDigestStreamStartFor
    (family AArch64Assembly)
    (family AArch64Register)
    (aarch64WordDigestBackendFor aarch64WordDigestReturn))

def aarch64ByteDigestStreamStartRoutine : Bytes =
  (aarch64RoutineBytes aarch64ByteDigestStreamStartAssembly)

def aarch64ByteDigestStreamFinishAssembly =
  (constructor
    AArch64Assembly
    AArch64AssemblyBranch
    b"byte-digest-entry"
    (ahrLabel
      b"byte-digest-refused"
      (ahrMovImm
        ahrX0
        0
        (ahrReturn
          (ahrLabel
            b"byte-digest-entry"
            (wordDigestStreamFinishFor
              (family AArch64Assembly)
              (family AArch64Register)
              (aarch64WordDigestBackendFor aarch64WordDigestReturn)))))))

def aarch64ByteDigestStreamFinishRoutine : Bytes =
  (aarch64RoutineBytes aarch64ByteDigestStreamFinishAssembly)