Coppelius.Build.SM86Compat

1module Coppelius.Build.SM86Compat
2
3import Accelerator.SM86.Capability
4import Coppelius.ArenaPlan
5import Coppelius.LaunchPolicy
6import Coppelius.Learner
7import Coppelius.SM86Capability
8import Coppelius.System
9import Coppelius.TrainingRun
10import Representation.BuildPlan
11
12-- This is the semantic system-to-target binding.  It names only the generic
13-- SM86 capability profile; a physical card witness is supplied separately.
14family CoppeliusSM86BuildBinding : Type 0
15constructor CoppeliusSM86BuildBindingValue
16field unrestricted coppeliusBuildSystem : (family CoppeliusSystemConfiguration)
17field unrestricted coppeliusBuildLearning : (family CoppeliusLearningSemantics)
18field unrestricted coppeliusBuildRequirements : (family SM86CapabilityRequirements)
19field unrestricted coppeliusBuildArena : (family CoppeliusArenaPlan)
20field unrestricted coppeliusBuildLaunch : (family CoppeliusLaunchPolicy)
21field unrestricted coppeliusBuildCheckpoint : (family CoppeliusCheckpointTransportSchema)
22
23end-family
24
25def coppeliusSM86BuildBinding : (family CoppeliusSM86BuildBinding) =
26  (record
27    CoppeliusSM86BuildBinding
28    (coppeliusBuildSystem = coppeliusSystem)
29    (coppeliusBuildLearning = coppeliusLearningSemantics)
30    (coppeliusBuildRequirements = coppeliusSM86CompatCapabilityRequirements)
31    (coppeliusBuildArena = coppeliusSM86CompatArenaPlan)
32    (coppeliusBuildLaunch = coppeliusSM86CompatLaunchPolicy)
33    (coppeliusBuildCheckpoint = coppeliusCheckpointSchema))
34
35-- Target products supply only their identity, output name and evidence lane.
36-- Everything else is shared by the system-to-SM86 binding.
37def coppeliusSM86BuildPlanEntries =
38  (lambda unrestricted targetIdentity : Bytes .
39    (lambda unrestricted capabilityEvidence : Bytes .
40      (lambda unrestricted finalELF : Bytes .
41        (lambda unrestricted evidencePath : Bytes .
42          (lambda unrestricted physicalLane : Bytes .
43            (buildPlanCons
44              b"system"
45              b"coppelius"
46              (buildPlanCons
47                b"model"
48                b"dense-transformer-60m"
49                (buildPlanCons
50                  b"objective"
51                  coppeliusObjectiveIdentity
52                  (buildPlanCons
53                    b"learner"
54                    coppeliusLearnerIdentity
55                    (buildPlanCons
56                      b"target"
57                      targetIdentity
58                      (buildPlanCons
59                        b"requirements"
60                        coppeliusSM86CompatProfileIdentity
61                        (buildPlanCons
62                          b"capability-evidence"
63                          capabilityEvidence
64                          (buildPlanCons
65                            b"schedule"
66                            b"sm86-qmd-pushbuffer-gpfifo-v1"
67                            (buildPlanCons
68                              b"memory"
69                              b"coppelius-sm86-static-arena-1280-mib"
70                              (buildPlanCons
71                                b"host-emitter"
72                                b"alpha-x86_64-host-emitter"
73                                (buildPlanCons
74                                  b"final-host-elf"
75                                  finalELF
76                                  (buildPlanCons
77                                    b"device-image"
78                                    b"embedded-sm86-program-table"
79                                    (buildPlanCons
80                                      b"qmd"
81                                      b"embedded-sm86-qmd-table"
82                                      (buildPlanCons
83                                        b"pushbuffer"
84                                        b"embedded-sm86-pushbuffer"
85                                        (buildPlanCons
86                                        b"gpfifo"
87                                        b"embedded-sm86-gpfifo"
88                                        (buildPlanCons
89                                        b"checkpoint"
90                                        coppeliusRawCheckpointSchemaIdentity
91                                        (buildPlanCons
92                                        b"evidence"
93                                        evidencePath
94                                        (buildPlanCons b"physical-lane" physicalLane buildPlanEmpty)))))))))))))))))))))))