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)))))))))))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.