module Platform.Linux.Nvidia.LinearStep import Accelerator.SM86.Instruction import Platform.Linux.Nvidia.ProgramPlan import Accelerator.SM86.InstructionEncoding import Accelerator.SM86.Types import Compiler.Planning.VA import Hardware.Nvidia.SM86.Command.WholeProgramPlan import Model.Config import Model.Parameter import Model.Word64 import Platform.Linux.Nvidia.PlanHost import Platform.Linux.Nvidia.DeviceBinding import Platform.Linux.Nvidia.PlanHostRequest import Platform.Linux.Nvidia.ResourcePlan import Runtime.NativePhysicalMemory import Runtime.NativeResourcePlan import Execution.ResourceGraph import Std.Foundation import Std.List import Realization.Nvidia.SM86.LinearStepPlanSM86 import Realization.Nvidia.SM86.LinearStepSM86 import Runtime.ArenaCertificate import Runtime.NativePhysicalEmbeddedArtifact import Runtime.NativePhysicalProgram import Runtime.NativeFloatPlan import Runtime.NativeFilePlan import Data.Bytes import Runtime.NativeLaunchRecipeLoad import Runtime.NativePhysicalProgramComposer import Std.Natural import Std.Numeric.Profile -- A shape-derived, reusable scalar/vector linear-step placement. The same -- checked kernel can evaluate gradients from runtime data repeatedly. System -- semantics choose samples and combine gradients; this target owns memory, -- launch tables, submission retirement and readback. All buffers are explicit: -- host-visible system memory for this small realization, video memory for the -- separate direct-RM USERD allocation. The system-memory ring and data use -- the admitted direct mappings. This is a declared route, not a runtime retry. family NvidiaLinearStepPlan : Type 0 constructor NvidiaLinearStepPlanValue field unrestricted nlsLayout : (family NvidiaPlanHostLayout) field unrestricted nlsComponents : (pi unrestricted component : (family NvidiaWholeProgramComponent) . Bytes) field unrestricted nlsRecipes : (family NvidiaPlanHostRecipeFills) field unrestricted nlsDataHost : Nat field unrestricted nlsInputOffset : Nat field unrestricted nlsTargetOffset : Nat field unrestricted nlsOutputOffset : Nat field unrestricted nlsDataBytes : Nat field unrestricted nlsAdmitted : Nat end-family -- Scalar evaluation chooses a semantic result field, never an unchecked byte -- offset. These cases apply to the admitted 1-output, 1-input specialization. family NvidiaLinearScalarResult : Type 0 constructor NvidiaLinearScalarPrediction constructor NvidiaLinearScalarLoss constructor NvidiaLinearScalarGradient constructor NvidiaLinearScalarUpdatedWeight end-family family NvidiaLinearScalarInput : Type 0 constructor NvidiaLinearScalarNatural field unrestricted nlsNaturalValue : Nat constructor NvidiaLinearScalarBinary64 field unrestricted nlsBinary64Value : (family NativePhysicalOperand) end-family def nlsScalarResultOffset = (lambda unrestricted result : (family NvidiaLinearScalarResult) . (eliminate NvidiaLinearScalarResult (lambda unrestricted current : (family NvidiaLinearScalarResult) . Nat) result (branch NvidiaLinearScalarPrediction . 0) (branch NvidiaLinearScalarLoss . (lsLossOffset 1)) (branch NvidiaLinearScalarGradient . (lsGradientOffset 1 1 0 0)) (branch NvidiaLinearScalarUpdatedWeight . (lsUpdatedOffset 1 1 0 0)))) -- A runtime input is rounded once to binary32. A natural input first uses the -- explicit binary64 conversion, preserving the host arithmetic contract. The -- temporary is private and must not alias another input's still-live state. def nlsUploadScalar = (lambda unrestricted error : Bytes . (lambda unrestricted input : (family NvidiaLinearScalarInput) . (lambda unrestricted scratch : Nat . (lambda unrestricted destination : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NvidiaLinearScalarInput (lambda unrestricted current : (family NvidiaLinearScalarInput) . (family NativePhysicalCommands)) input (branch NvidiaLinearScalarNatural value . (nativeFloat64Natural error scratch value (nativeNumericConvert error (constructor StdNumericConversion StdNumericRoundBinary64) scratch (phLoad scratch) (phCopyStateToMapped scratch destination (linearStepPlanInputBytesFor 1) tail)))) (branch NvidiaLinearScalarBinary64 value . (nativeNumericConvert error (constructor StdNumericConversion StdNumericRoundBinary64) scratch value (phCopyStateToMapped scratch destination (linearStepPlanInputBytesFor 1) tail))))))))) -- Upload all runtime operands, submit one checked scalar kernel, wait for its -- own fence, then widen the selected device result. No host expression computes -- that result. The caller supplies the matching scalar plan and disjoint state; -- its fresh-channel counter is independent of checkpointed learner versions. def nlsEvaluateScalar = (lambda unrestricted error : Bytes . (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 : (family NvidiaLinearScalarInput) . (lambda unrestricted input : (family NvidiaLinearScalarInput) . (lambda unrestricted target : (family NvidiaLinearScalarInput) . (lambda unrestricted result : (family NvidiaLinearScalarResult) . (lambda unrestricted destination : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nlsUploadScalar error weight scratch data (nlsUploadScalar error input scratch (naturalAdd data inputOffset) (nlsUploadScalar error target scratch (naturalAdd data targetOffset) (prReissueCounted layout counter 0 entry (phCopyMappedToState (naturalAdd data (naturalAdd outputOffset (nlsScalarResultOffset result))) scratch (linearStepPlanInputBytesFor 1) (nativeNumericConvert error (constructor StdNumericConversion StdNumericWidenBinary32) destination (phLoad scratch) tail))))))))))))))))))))) -- Learning rate is a runtime scalar in the launch's typed parameter block. -- A zero rate asks this realization for a gradient without changing W. The -- output still contains y, loss, gradient and proposed W; callers select only -- the fields their learning transition needs. def nvidiaLinearStepPlan = (lambda unrestricted m : Nat . (lambda unrestricted k : Nat . (lambda unrestricted learningRate : Nat . (lambda unrestricted architecture : (family ModelWord32) . (lambda unrestricted computeClass : (family ModelWord32) . (lambda unrestricted spaVersion : (family ModelWord32) . (lambda unrestricted qmdBytes : Nat . (lambda unrestricted product : Bytes . (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted availableVideo : Nat . (let unrestricted inputOffset = (linearStepPlanWeightsBytesFor m k) in (let unrestricted targetOffset = (naturalAdd inputOffset (linearStepPlanInputBytesFor k)) in (let unrestricted outputOffset = (naturalAdd targetOffset (linearStepPlanTargetBytesFor m)) in (let unrestricted dataBytes = (naturalAdd outputOffset (linearStepSM86OutputRecordBytesFor m k)) in (eliminate NvidiaProgramPlan (lambda unrestricted value : (family NvidiaProgramPlan) . (family NvidiaLinearStepPlan)) (nvidiaProgramPlan (linearStepPlanRegionsForProgram (linearStepSM86ProgramFor m k)) (lambda unrestricted programGPU : Nat . (lambda unrestricted dataGPU : Nat . (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleOne (constructor NvidiaLaunchTemplate NvidiaLaunchTemplateValue linearStepSM86Identity (constructor NvidiaLaunchKernel NvidiaLaunchKernelValue (phWord programGPU) 1 1 1 1 1 linearStepPlanParameterBytes) (linearStepPlanParametersAt dataGPU (naturalAdd dataGPU inputOffset) (naturalAdd dataGPU targetOffset) (naturalAdd dataGPU outputOffset) learningRate))))) linearStepPlanSubmissions dataBytes (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory) architecture computeClass spaVersion qmdBytes product abi availableVideo) (branch NvidiaProgramPlanValue layout component recipes dataHost dataGPU extent admitted . (constructor NvidiaLinearStepPlan NvidiaLinearStepPlanValue layout component recipes dataHost inputOffset targetOffset outputOffset extent (naturalAnd (linearStepSM86ShapeAdmitted m k) admitted)))))))))))))))))) -- Keep the complete last scalar result, timestamped semaphore and fresh-channel -- issue count as separate device evidence. The destination is exclusive. The -- record is never a learning input or an implied whole-run timing measurement. def nlsScalarReadback = (lambda unrestricted path : (family NativePhysicalOperand) . (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted data : Nat . (lambda unrestricted outputOffset : Nat . (lambda unrestricted counter : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeFileOpen path nativeFileCandidateFlags prSlotResult prSlotStatus b"device-readback-open" (nativeFileWrite (phSlot prSlotResult) (phImm (naturalAdd data outputOffset)) (linearStepSM86OutputRecordBytesFor 1 1) (phImm 0) prSlotStatus b"device-readback-output" (nativeFileWrite (phSlot prSlotResult) (phImm (prSemaphoreHost layout)) prSemaphoreStride (phImm (linearStepSM86OutputRecordBytesFor 1 1)) prSlotStatus b"device-readback-fence" (nativeFileWrite (phSlot prSlotResult) (phState counter) (bytes-length (dataBytesWord64LE (modelWord64FromNaturalTruncated 0))) (phImm (naturalAdd (linearStepSM86OutputRecordBytesFor 1 1) prSemaphoreStride)) prSlotStatus b"device-readback-issues" (nativeFileClose (phSlot prSlotResult) prSlotStatus b"device-readback-close" tail)))))))))))