Coppelius.Build.RTX3070

1module Coppelius.Build.RTX3070
2
3import Accelerator.SM86.Capability
4import Coppelius.Build.SM86Compat
5import Coppelius.Learner
6import Coppelius.SM86Capability
7import Coppelius.TrainingRun
8import Model.Parameter
9import Model.Word64
10import Platform.RunPod.Nvidia.SM86
11import Representation.BuildRequest
12import Representation.BuildPlan
13import Std.Natural
14import Std.Physical
15import Std.Word
16import Coppelius.Build.NativeHost
17import Platform.Linux.Nvidia.Compatibility
18
19-- R5's one physical target.  The exact self-contained ELF completed fresh
20-- initialization and fresh-process continuation on this device on 2026-09-17.
21-- Marketing identity remains evidence; capability admission stays generic.
22family CoppeliusRTX3070Binding : Type 0
23constructor CoppeliusRTX3070BindingValue
24field unrestricted coppeliusRTX3070SemanticBinding : (family CoppeliusSM86BuildBinding)
25field unrestricted coppeliusRTX3070TargetProfile : (family RunPodSM86TargetProfile)
26field unrestricted coppeliusRTX3070ObservedCapabilities : (family SM86DeviceCapabilities)
27field unrestricted coppeliusRTX3070Admission : (family SM86CapabilityAdmission)
28field unrestricted coppeliusRTX3070Plan : (family SystemTargetBuildPlan)
29
30end-family
31
32def coppeliusRTX3070TargetIdentity : Bytes =
33  runPodRTX3070TargetIdentity
34
35def coppeliusRTX3070QualificationIdentity : Bytes =
36  b"coppelius-rtx3070-target-profile-v1"
37
38def coppeliusRTX3070TotalVideoMemory : StdU64 =
39  (runPodSM86TotalVideoMemory runPodRTX3070TargetProfile)
40
41def coppeliusRTX3070Capabilities : (family SM86DeviceCapabilities) =
42  (record
43    SM86DeviceCapabilities
44    (sm86CapabilityComputeMajor = 8)
45    (sm86CapabilityComputeMinor = 6)
46    (sm86CapabilityTotalVideoMemoryBytes = coppeliusRTX3070TotalVideoMemory)
47    (sm86CapabilityAvailableVideoMemoryBytes
48      =
49      (stdByteCountValue coppeliusSM86CompatMinimumVideoMemory))
50    (sm86CapabilityMappedAddressEnd = (stdDeviceAddressValue coppeliusSM86CompatMappedAddressEnd))
51    (sm86CapabilityMaximumGridX
52      =
53      (stdU32ToNatural (stdGridDimensionValue coppeliusSM86CompatMaximumGridX)))
54    (sm86CapabilityUVMSupported = 1)
55    (sm86CapabilityResourceManagerSupported = 1)
56    (sm86CapabilityQMDSupported = 1)
57    (sm86CapabilityPushbufferSupported = 1)
58    (sm86CapabilityGPFIFOSupported = 1)
59    (sm86CapabilityDeviceTimestampsSupported = 1)
60    (sm86CapabilityHostFallbacks = 0))
61
62def coppeliusRTX3070CapabilityAdmission : (family SM86CapabilityAdmission) =
63  (coppeliusSM86CompatAdmit coppeliusRTX3070Capabilities)
64
65def coppeliusRTX3070CapabilityAccepted : Nat =
66  (sm86CapabilityAdmissionAccepted coppeliusRTX3070CapabilityAdmission)
67
68-- the compatibility contract: what the artifact demands of the card
69-- against what the RTX 3070 profile supplies (Platform.Linux.Nvidia.
70-- Compatibility); the first demand not met, by name (empty = admitted)
71def coppeliusRTX3070CompatibilityRefusal : Bytes =
72  (nvidiaCompatibilityRefusal (coppeliusCompatDemands runPodSM86QMDArchitecture) runPodRTX3070Supplies)
73
74def coppeliusRTX3070ExactTargetAccepted : Nat =
75  (naturalAnd (naturalIsZero (bytes-length coppeliusRTX3070CompatibilityRefusal))
76  (naturalAnd
77    (runPodSM86TargetMatches
78      runPodRTX3070TargetProfile
79      runPodRTX3070ProductIdentity
80      coppeliusRTX3070Capabilities)
81    coppeliusRTX3070CapabilityAccepted))
82
83def coppeliusRTX3070BuildPlanEntries =
84  (coppeliusSM86BuildPlanEntries
85    coppeliusRTX3070TargetIdentity
86    coppeliusRTX3070QualificationIdentity
87    b"coppelius-rtx3070-sm86.elf"
88    b"systems/coppelius/evidence/2026-09-17-alpha-owned-self-contained-training-elf.md"
89    b"r6-qualification-pending")
90
91def coppeliusRTX3070BuildPlan : (family SystemTargetBuildPlan) =
92  (record
93    SystemTargetBuildPlan
94    (systemTargetBuildPlanIdentity = b"coppelius-rtx3070-build-plan-v1")
95    (systemTargetBuildPlanCapabilityAccepted = coppeliusRTX3070ExactTargetAccepted)
96    (systemTargetBuildPlanEntries = coppeliusRTX3070BuildPlanEntries))
97
98def coppeliusRTX3070BuildRequest : (family SystemTargetBuildRequest) =
99  (record
100    SystemTargetBuildRequest
101    (buildRequestSystemIdentity = b"coppelius")
102    (buildRequestLearnerIdentity = coppeliusLearnerIdentity)
103    (buildRequestTargetIdentity = coppeliusRTX3070TargetIdentity)
104    (buildRequestAdmissionAccepted = coppeliusRTX3070ExactTargetAccepted)
105    (buildRequestScheduleIdentity = b"sm86-qmd-pushbuffer-gpfifo-v1")
106    (buildRequestMemoryIdentity = b"coppelius-sm86-static-arena-1280-mib")
107    (buildRequestProtocolIdentity = b"alpha-text-artifact-request-v1")
108    (buildRequestCheckpointIdentity = coppeliusRawCheckpointSchemaIdentity)
109    (buildRequestOutputFilename = b"coppelius-rtx3070-sm86.elf")
110    (buildRequestArtifactRoot = b"systems/coppelius/src/Coppelius/Build/RTX3070Artifact.alpha")
111    (buildRequestArtifactExpression = b"artifact"))
112
113def coppeliusRTX3070Binding : (family CoppeliusRTX3070Binding) =
114  (record
115    CoppeliusRTX3070Binding
116    (coppeliusRTX3070SemanticBinding = coppeliusSM86BuildBinding)
117    (coppeliusRTX3070TargetProfile = runPodRTX3070TargetProfile)
118    (coppeliusRTX3070ObservedCapabilities = coppeliusRTX3070Capabilities)
119    (coppeliusRTX3070Admission = coppeliusRTX3070CapabilityAdmission)
120    (coppeliusRTX3070Plan = coppeliusRTX3070BuildPlan))