module Coppelius.Build.SM86Compat

import Accelerator.SM86.Capability
import Coppelius.ArenaPlan
import Coppelius.LaunchPolicy
import Coppelius.Learner
import Coppelius.SM86Capability
import Coppelius.System
import Coppelius.TrainingRun
import Representation.BuildPlan

-- This is the semantic system-to-target binding.  It names only the generic
-- SM86 capability profile; a physical card witness is supplied separately.
family CoppeliusSM86BuildBinding : Type 0
constructor CoppeliusSM86BuildBindingValue
field unrestricted coppeliusBuildSystem : (family CoppeliusSystemConfiguration)
field unrestricted coppeliusBuildLearning : (family CoppeliusLearningSemantics)
field unrestricted coppeliusBuildRequirements : (family SM86CapabilityRequirements)
field unrestricted coppeliusBuildArena : (family CoppeliusArenaPlan)
field unrestricted coppeliusBuildLaunch : (family CoppeliusLaunchPolicy)
field unrestricted coppeliusBuildCheckpoint : (family CoppeliusCheckpointTransportSchema)

end-family

def coppeliusSM86BuildBinding : (family CoppeliusSM86BuildBinding) =
  (record
    CoppeliusSM86BuildBinding
    (coppeliusBuildSystem = coppeliusSystem)
    (coppeliusBuildLearning = coppeliusLearningSemantics)
    (coppeliusBuildRequirements = coppeliusSM86CompatCapabilityRequirements)
    (coppeliusBuildArena = coppeliusSM86CompatArenaPlan)
    (coppeliusBuildLaunch = coppeliusSM86CompatLaunchPolicy)
    (coppeliusBuildCheckpoint = coppeliusCheckpointSchema))

-- Target products supply only their identity, output name and evidence lane.
-- Everything else is shared by the system-to-SM86 binding.
def coppeliusSM86BuildPlanEntries =
  (lambda unrestricted targetIdentity : Bytes .
    (lambda unrestricted capabilityEvidence : Bytes .
      (lambda unrestricted finalELF : Bytes .
        (lambda unrestricted evidencePath : Bytes .
          (lambda unrestricted physicalLane : Bytes .
            (buildPlanCons
              b"system"
              b"coppelius"
              (buildPlanCons
                b"model"
                b"dense-transformer-60m"
                (buildPlanCons
                  b"objective"
                  coppeliusObjectiveIdentity
                  (buildPlanCons
                    b"learner"
                    coppeliusLearnerIdentity
                    (buildPlanCons
                      b"target"
                      targetIdentity
                      (buildPlanCons
                        b"requirements"
                        coppeliusSM86CompatProfileIdentity
                        (buildPlanCons
                          b"capability-evidence"
                          capabilityEvidence
                          (buildPlanCons
                            b"schedule"
                            b"sm86-qmd-pushbuffer-gpfifo-v1"
                            (buildPlanCons
                              b"memory"
                              b"coppelius-sm86-static-arena-1280-mib"
                              (buildPlanCons
                                b"host-emitter"
                                b"alpha-x86_64-host-emitter"
                                (buildPlanCons
                                  b"final-host-elf"
                                  finalELF
                                  (buildPlanCons
                                    b"device-image"
                                    b"embedded-sm86-program-table"
                                    (buildPlanCons
                                      b"qmd"
                                      b"embedded-sm86-qmd-table"
                                      (buildPlanCons
                                        b"pushbuffer"
                                        b"embedded-sm86-pushbuffer"
                                        (buildPlanCons
                                        b"gpfifo"
                                        b"embedded-sm86-gpfifo"
                                        (buildPlanCons
                                        b"checkpoint"
                                        coppeliusRawCheckpointSchemaIdentity
                                        (buildPlanCons
                                        b"evidence"
                                        evidencePath
                                        (buildPlanCons b"physical-lane" physicalLane buildPlanEmpty)))))))))))))))))))))))