module PartitionedRegression.Build.NativeHost import PartitionedRegression.NativeHost import PartitionedRegression.Build.ScalarEvaluation import Checkpoint.Envelope import Checkpoint.NativeEnvelope import Compiler.Planning.RegionFrame import Data.Bytes import Hardware.Nvidia.SM86.Command.WholeProgramPlan import Model.Word64 import Platform.Linux.Nvidia.DeviceBinding import Platform.Linux.Nvidia.LinearStep import Platform.Linux.Nvidia.ProgramPlan import Platform.Linux.Nvidia.PlanHost import Platform.Linux.Nvidia.PlanHostRequest import Platform.RunPod.Nvidia.SM86 import Realization.Nvidia.SM86.LinearStepSM86 import Runtime.NativeFilePlan import Runtime.NativeLaunchRecipeLoad import Runtime.NativePhysicalEmbeddedArtifact import Runtime.NativePhysicalNativeELF import Runtime.NativePhysicalProgram import Runtime.NativePhysicalProgramComposer import Runtime.NativeRegionFrame import Runtime.RegionFrame import Runtime.SocketAddress import Std.Foundation import Std.Natural -- The numerical policy is shared by both roles and survives checkpoints. -- Parameters, sample-weighted combination and update use binary64. Each local -- sample rounds W to binary32, evaluates the checked SM86 gradient, then -- widens that value exactly. This is a declared mixed-precision learner, -- not a claim that arbitrary inputs equal the pure binary64 reference. def pgRun : Bytes = b"partitioned-squared-error-native-v1" def pgSchema : Bytes = b"f32-local-gradient-f64-update-with-u64-mass" def pgCheckpointContract = (constructor CheckpointEnvelopeContract CheckpointEnvelopeContractValue b"scalar-parameter-updates-batches-epoch/v1" b"sample-mass-squared-error;rate=1/4;f32-gradient-f64-update" b"fixed-repeated-batch:x=1,1,2;y=0" b"initial-natural-weight=3" (naturalMultiply 4 peerWordBytes) (naturalMultiply 3 peerWordBytes) 1) def pgIdentity = (lambda unrestricted name : Bytes . (bytes-append name (phZeros (naturalSaturatingSubtract nativePhysicalEmbeddedIdentityLength (bytes-length name))))) def pgHostIdentity = (pgIdentity b"partitioned-regression-sm86-host-v1") def pgProgramIdentity = (pgIdentity b"partitioned-regression-sm86-program") def pgQMDIdentity = (pgIdentity b"partitioned-regression-sm86-qmd") def pgPushIdentity = (pgIdentity b"partitioned-regression-sm86-push") def pgRingIdentity = (pgIdentity b"partitioned-regression-sm86-ring") def pgIdentities = (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . (eliminate NativePhysicalEmbeddedComponentKind (lambda unrestricted current : (family NativePhysicalEmbeddedComponentKind) . Bytes) kind (branch NativePhysicalEmbeddedHostELF . pgHostIdentity) (branch NativePhysicalEmbeddedProgramTable . pgProgramIdentity) (branch NativePhysicalEmbeddedQMDTable . pgQMDIdentity) (branch NativePhysicalEmbeddedPushbuffer . pgPushIdentity) (branch NativePhysicalEmbeddedGPFIFO . pgRingIdentity))) def pgPlan = regressionScalarPlan -- A gradient evaluation uploads the current parameter and one sample, issues -- the checked kernel, awaits its own retired fence, and consumes device -- readback. No host equation supplies the gradient. The program is the same -- for x=1 and x=2; samples are runtime state, not prerecorded output bytes. def pgGradient = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted entry : Nat . (lambda unrestricted data : Nat . (lambda unrestricted inputOffset : Nat . (lambda unrestricted targetOffset : Nat . (lambda unrestricted outputOffset : Nat . (lambda unrestricted counter : Nat . (lambda unrestricted scratch : Nat . (lambda unrestricted weight : Nat . (lambda unrestricted destination : Nat . (lambda unrestricted sample : Nat . (nlsEvaluateScalar b"peer-arithmetic" layout entry data inputOffset targetOffset outputOffset counter scratch (constructor NvidiaLinearScalarInput NvidiaLinearScalarBinary64 (frameNativeLoad weight)) (constructor NvidiaLinearScalarInput NvidiaLinearScalarNatural sample) (constructor NvidiaLinearScalarInput NvidiaLinearScalarNatural 0) (constructor NvidiaLinearScalarResult NvidiaLinearScalarGradient) destination)))))))))))) -- One participant holds x=1; the other holds x=1 and x=2. A second GPU -- issue computes the second contribution. Both gradients participate in the -- next shared parameter; a repeated issue counter is private to each channel. def pgContribution = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted entry : Nat . (lambda unrestricted data : Nat . (lambda unrestricted inputOffset : Nat . (lambda unrestricted targetOffset : Nat . (lambda unrestricted outputOffset : Nat . (lambda unrestricted counter : Nat . (lambda unrestricted scratch : Nat . (lambda unrestricted second : Nat . (lambda unrestricted worker : Nat . (lambda unrestricted weight : Nat . (lambda unrestricted destination : Nat . (pgGradient layout entry data inputOffset targetOffset outputOffset counter scratch weight destination 1 (peerByRole worker peerEnd (pgGradient layout entry data inputOffset targetOffset outputOffset counter scratch weight second 2 (peerBinary peerAdd destination destination second peerEnd)))))))))))))))) -- Retain the final device record and both timestamped semaphore releases, -- followed by the completed issue count. This is a bounded raw artifact for -- the existing device-run evidence path, separate from the training wire -- format. It is created exclusively and never used as learning input. def pgReadback = (nlsScalarReadback (peerArgument 5)) -- A bound GPU session and authenticated recipe expansion. The peer protocol -- occupies slots 0..2 and state after phStateExtent; relocation reserves the -- NVIDIA result slots without moving either layout's state addresses. def pgPrelude = (lambda unrestricted device : (family NvidiaDeviceBinding) . (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted recipes : (family NvidiaPlanHostRecipeFills) . (lambda unrestricted program : Bytes . (lambda unrestricted qmd : Bytes . (lambda unrestricted push : Bytes . (lambda unrestricted ring : Bytes . (nlsSessionPrelude pgIdentities b"partitioned-peer" device layout recipes program qmd push ring peerEnd)))))))) -- argv: [previous checkpoint or unused], candidate, committed generation, -- containing directory, exclusive device-readback file. Socket address and -- exact card binding are admitted deployment inputs to compilation. Prediction -- uses the identical numerical checkpoint contract in a fresh process. def partitionedDeviceArtifact = (lambda unrestricted profile : (family RunPodSM86TargetProfile) . (lambda unrestricted device : (family NvidiaDeviceBinding) . (lambda unrestricted worker : Nat . (lambda unrestricted address : (family IPv4Address) . (lambda unrestricted port : Nat . (lambda unrestricted resume : Nat . (lambda unrestricted steps : Nat . (eliminate NvidiaLinearStepPlan (lambda unrestricted p : (family NvidiaLinearStepPlan) . Bytes) (pgPlan profile) (branch NvidiaLinearStepPlanValue layout component recipes data inputOffset targetOffset outputOffset dataBytes admitted . (nat-eliminate (lambda unrestricted ok : Nat . Bytes) b"" (lambda unrestricted previous : Nat . (lambda unrestricted ignored : Bytes . (peerLayoutsFor pgRun pgSchema phStateExtent (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (eliminate StdResult (lambda unrestricted r : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) . Bytes) (planNativeCheckpoint pgCheckpointContract (frameAlign (peerEndpointEnd (peerWorkEnd work))) peerWordBytes (naturalMultiply 2 peerWordBytes) 1048576) (branch StdFailure error . b"") (branch StdSuccess checkpoint . (eliminate StdResult (lambda unrestricted r : (family StdResult (family SocketAddressFailure) Bytes) . Bytes) (linuxIPv4SocketAddress address port) (branch StdFailure error . b"") (branch StdSuccess socketAddress . (let unrestricted counter = (frameAlign (nativeCheckpointEnd checkpoint)) in (let unrestricted scratch = (naturalAdd counter peerWordBytes) in (let unrestricted second = (naturalAdd scratch peerWordBytes) in (let unrestricted extent = (naturalAdd second peerWordBytes) in (let unrestricted destination = (naturalSelect worker (framePayloadAt contribution) (framePayloadAt updated)) in (let unrestricted program = (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramProgramRecipe)) in (let unrestricted qmd = (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramQMDRecipe)) in (let unrestricted push = (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramPushbufferRecipe)) in (let unrestricted ring = (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramGPFIFORecipe)) in (let unrestricted entry = (nvidiaPlanHostTableWord (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramGPFIFO)) 0) in (nlsWithPrivateSlots peerEndpointSlots (pgPrelude device layout recipes program qmd push ring) (lambda unrestricted prepare : (family NativePhysicalCommands) . (nlsWithPrivateSlots peerEndpointSlots (pgContribution layout entry data inputOffset targetOffset outputOffset counter scratch second worker (framePayloadAt initial) destination) (lambda unrestricted local : (family NativePhysicalCommands) . (nlsWithPrivateSlots peerEndpointSlots (pgReadback layout data outputOffset counter (phTelemetry 3 b"partitioned-peer:device-updates-retired" (phRelease peerEnd))) (lambda unrestricted finish : (family NativePhysicalCommands) . (nlsEmbedHost pgIdentities (nativePhysicalGenerateNativeELFBytesDirect (peerProgram (naturalAdd peerEndpointSlots phSlots) extent (peerCheckpointStart checkpoint initial resume (peerStore counter (phImm 0) (prSplice prepare (peerNativeSetup worker socketAddress (peerWorkEnd work) (peerImmediateTransmission work (peerUpdatesWith (prSplice local) (nativeLaunchRecipeSlotValue peerConnectionSlot) worker 0 steps (frameNativeLoad (peerCheckpointEpochAt checkpoint)) (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint)) initial contribution updated acknowledged work (prSplice finish (peerCheckpointFinish checkpoint initial worker steps (nativeLaunchRecipeSlotValue peerConnectionSlot))))))))))) program qmd push ring))))))))))))))))))))))))))))) (naturalAnd admitted (naturalAnd (nvidiaDeviceBindingAdmitted device) (naturalAnd (naturalEqual (bytes-length (nvidiaDeviceBindingUUID device)) 16) (naturalAnd (naturalLessOrEqual worker 1) (naturalAnd (naturalLessOrEqual resume 1) (naturalAnd (naturalNonzero steps) (naturalLessOrEqual steps regionFrameWordLimit))))))))))))))))) def partitionedDevicePredictionArtifact = (checkpointPredictionArtifactFor pgCheckpointContract)