module Platform.Linux.Nvidia.ProgramPlan import Accelerator.SM86.Instruction 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 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 -- One shared native session plan for target-owned programs. Model-specific -- parameter/data layouts supply typed regions and launch declarations; this -- owner derives backing, placement, tables, recipes and admission. The data -- backing is explicit, so persistent learner state can use video memory. -- Current code-region admission is SM86. A new architecture must provide its -- own established extent/placement semantics, not reuse a guessed capacity. family NvidiaProgramPlan : Type 0 constructor NvidiaProgramPlanValue field unrestricted nvidiaProgramLayout : (family NvidiaPlanHostLayout) field unrestricted nvidiaProgramComponents : (pi unrestricted component : (family NvidiaWholeProgramComponent) . Bytes) field unrestricted nvidiaProgramRecipes : (family NvidiaPlanHostRecipeFills) field unrestricted nvidiaProgramDataHost : Nat field unrestricted nvidiaProgramDataGPU : Nat field unrestricted nvidiaProgramDataBytes : Nat field unrestricted nvidiaProgramAdmitted : Nat end-family -- Append a relocated device fragment only after successful admission. Result -- slots are private to the device session; state addresses already come from -- the caller's combined layout. A failed relocation produces no executable. def nlsWithPrivateSlots = (lambda unrestricted slotsBefore : Nat . (lambda unrestricted commands : (family NativePhysicalCommands) . (lambda unrestricted emit : (pi unrestricted relocated : (family NativePhysicalCommands) . Bytes) . (eliminate NativePhysicalProgramComposeCommandsResult (lambda unrestricted r : (family NativePhysicalProgramComposeCommandsResult) . Bytes) (nativePhysicalProgramComposeRelocateCommands commands (phWord 0) (phWord slotsBefore) (phWord 0)) (branch NativePhysicalProgramComposeCommandsRelocated relocated count operations operands checks . (emit relocated)) (branch NativePhysicalProgramComposeCommandsRejected error count operations operands checks . b""))))) def nlsExtent = (lambda unrestricted bytes : Nat . (nvidiaPlanHostRoundUp bytes nvidiaPlanHostMappingUnit)) def nlsAfter = (lambda unrestricted base : Nat . (lambda unrestricted bytes : Nat . (vaPlaceAfter base bytes nvidiaPlanHostMappingAlignment))) def nlsBuffer = (lambda unrestricted name : Bytes . (lambda unrestricted gpu : Nat . (lambda unrestricted host : Nat . (lambda unrestricted bytes : Nat . (lambda unrestricted memory : (family NvidiaPlanHostMemory) . (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue name gpu host (nlsExtent bytes) memory)))))) def nlsRecipe = (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . (lambda unrestricted tail : (family NvidiaPlanHostRecipeFills) . (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext host extent kind tail))))) def nlsHostExtras = (phResident b"recipe-staging" nvidiaPlanHostStaging nvidiaPlanHostStagingExtent (constructor ArenaResidents ArenaResidentsEnd)) -- This anonymous mapping is created by nlsSessionPrelude below. Its timestamp -- and recipe views share one allocation; account for it once alongside the -- target session and the actual interpreter program before emitting bytes. def nlsResourceContext = (lambda unrestricted context : (family NvidiaResourceContext) . (stdResultBind (family NativePhysicalMemoryFailure) (family ResourceLease) (family NvidiaResourceContext) (nvidiaResourceHostLease context b"/control/recipe-staging" nvidiaPlanHostStagingExtent) (lambda unrestricted lease : (family ResourceLease) . (constructor StdResult StdSuccess (family NativePhysicalMemoryFailure) (family NvidiaResourceContext) (nvidiaResourceWithNative context (nativeResourceContextAddLeases (nvidiaResourceNative context) (constructor StdList StdListCons (family ResourceLease) lease (constructor StdList StdListEmpty (family ResourceLease))))))))) def nlsGenerateResourceELF = (lambda unrestricted context : (family NvidiaResourceContext) . (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativePhysicalMemoryFailure) (family NvidiaResourceContext)) . Bytes) (nlsResourceContext context) (branch StdFailure reason . b"") (branch StdSuccess withStaging . (nvidiaPlanHostGenerateResourceELF withStaging layout program)))))) -- Session setup owns the native driver, executable verification and recipe -- expansion. Identities belong to the compiled composition; the device path -- never learns the caller's model, learner, endpoint or checkpoint layout. def nlsSessionPrelude = (lambda unrestricted identity : (pi unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . Bytes) . (lambda unrestricted label : Bytes . (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 . (lambda unrestricted tail : (family NativePhysicalCommands) . (prFenceRegister (phPipeCreate (phTelemetryOpen (phTelemetry 1 (bytes-append label b":begin") (prEnvelope (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedHostELF)) (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedProgramTable)) (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedQMDTable)) (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedPushbuffer)) (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO)) (bytes-length program) (bytes-length qmd) (bytes-length push) (bytes-length ring) (phPreludeOn device (constructor NvidiaPlanHostMode NvidiaPlanHostStrict) layout (nativeLaunchRecipeStagingCommands nvidiaPlanHostStaging nvidiaPlanHostStagingExtent prSlotStatus phIdentity (prRecipeFills recipes (phTelemetry 2 (bytes-append label b":channel-ready") tail))))))))))))))))))) -- The compiler's typed envelope builder places and seals the five reachable -- components. Neither the caller nor this plan joins executable bytes itself. -- The schedule owns each ring entry and its semaphore ordinal. The caller -- selects an admitted ordinal and owns one initialized fresh-channel counter; -- prReissueCounted serializes retirement before any successor touches memory. def nvidiaProgramIssue = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted component : (pi unrestricted kind : (family NvidiaWholeProgramComponent) . Bytes) . (lambda unrestricted counter : Nat . (lambda unrestricted ordinal : Nat . (prReissueCounted layout counter ordinal (nvidiaPlanHostTableWord (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramGPFIFO)) ordinal)))))) def nlsEmbedHost = (lambda unrestricted identity : (pi unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . Bytes) . (lambda unrestricted host : Bytes . (lambda unrestricted program : Bytes . (lambda unrestricted qmd : Bytes . (lambda unrestricted push : Bytes . (lambda unrestricted ring : Bytes . (nativePhysicalEmbeddedBuildResultBytes (nativePhysicalEmbeddedBuild (nativePhysicalEmbeddedPayloadInMemory (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedHostELF)) host) (nativePhysicalEmbeddedPayloadInMemory (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedProgramTable)) program) (nativePhysicalEmbeddedPayloadInMemory (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedQMDTable)) qmd) (nativePhysicalEmbeddedPayloadInMemory (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedPushbuffer)) push) (nativePhysicalEmbeddedPayloadInMemory (identity (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO)) ring))))))))) -- Placement is derived before the launch parameters are specialized. Program -- capacity, QMDs, semaphores and pushbuffer size come from that same schedule. -- The initial ring recipe must fit the channel's admitted entry count. A -- runtime may reissue an entry after retirement; a larger static schedule -- instead needs a different channel plan, not an oversized startup recipe. def nvidiaProgramSubmissionsAdmitted = (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) . (let unrestricted count = (nvidiaSubmissionScheduleCount submissions) in (naturalAnd (naturalNonzero count) (naturalLessOrEqual count nvidiaPlanHostDirectGPFIFOEntries)))) def nvidiaProgramPlan = (lambda unrestricted regions : (family NvidiaDeviceRegions) . (lambda unrestricted launchesAt : (pi unrestricted programGPU : Nat . (pi unrestricted dataGPU : Nat . (family NvidiaLaunchSchedule))) . (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) . (lambda unrestricted dataBytes : Nat . (lambda unrestricted dataMemory : (family NvidiaPlanHostMemory) . (lambda unrestricted architecture : (family ModelWord32) . (lambda unrestricted computeClass : (family ModelWord32) . (lambda unrestricted spaVersion : (family ModelWord32) . (lambda unrestricted qmdSlotBytes : Nat . (lambda unrestricted product : Bytes . (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted availableVideo : Nat . (let unrestricted dataGPU = (nlsAfter phUVMChannelRangeBase phUVMChannelRangeExtent) in (let unrestricted dataHost = (nlsAfter phDoorHost nvidiaPlanHostMappingUnit) in (let unrestricted programGPU = (nlsAfter dataGPU (nlsExtent dataBytes)) in (let unrestricted programHost = (nlsAfter dataHost (nlsExtent dataBytes)) in (let unrestricted launches = (launchesAt programGPU dataGPU) in (let unrestricted launchCount = (nvidiaLaunchScheduleCount launches) in (let unrestricted submissionCount = (nvidiaSubmissionScheduleCount submissions) in (let unrestricted referenceCount = (nvidiaSubmissionScheduleReferenceCount submissions) in (let unrestricted programBytes = (nvidiaSM86ProgramCapacity regions launches) in (let unrestricted qmdBytes = (naturalMultiply qmdSlotBytes launchCount) in (let unrestricted pushBytes = (nvidiaSubmissionScheduleEncodedBytes submissions) in (let unrestricted semBytes = (nvidiaSubmissionSemaphoreExtent submissions prSemaphoreStride launchCount) in (let unrestricted ringBytes = (naturalMultiply nvidiaPlanHostDirectGPFIFOEntries 8) in (let unrestricted qmdGPU = (nlsAfter programGPU (nlsExtent programBytes)) in (let unrestricted qmdHost = (nlsAfter programHost (nlsExtent programBytes)) in (let unrestricted pushGPU = (nlsAfter qmdGPU (nlsExtent qmdBytes)) in (let unrestricted pushHost = (nlsAfter qmdHost (nlsExtent qmdBytes)) in (let unrestricted semGPU = (nlsAfter pushGPU (nlsExtent pushBytes)) in (let unrestricted semHost = (nlsAfter pushHost (nlsExtent pushBytes)) in (let unrestricted ringGPU = (nlsAfter semGPU (nlsExtent semBytes)) in (let unrestricted ringHost = (nlsAfter semHost (nlsExtent semBytes)) in (let unrestricted userdHost = (nlsAfter ringHost (nlsExtent ringBytes)) in (let unrestricted userdGPU = (nlsAfter ringGPU (nlsExtent ringBytes)) in (let unrestricted errorHost = (nlsAfter userdHost nvidiaPlanHostUSERDBytes) in (let unrestricted system = (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory) in (let unrestricted video = (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) in (let unrestricted layout = (constructor NvidiaPlanHostLayout NvidiaPlanHostLayoutValue (nlsBuffer b"gpfifo" ringGPU ringHost ringBytes system) (nlsBuffer b"push" pushGPU pushHost pushBytes system) (nlsBuffer b"semaphores" semGPU semHost semBytes system) (nlsBuffer b"program" programGPU programHost programBytes system) (nlsBuffer b"qmd" qmdGPU qmdHost qmdBytes system) (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue b"userd" userdGPU userdHost nvidiaPlanHostUSERDBytes video) (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext (nlsBuffer b"data" dataGPU dataHost dataBytes dataMemory) (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd)) abi (constructor NvidiaPlanHostLifecycle NvidiaPlanHostDirectRM nvidiaPlanHostDirectGPFIFOEntries) product errorHost) in (let unrestricted component = (lambda unrestricted selected : (family NvidiaWholeProgramComponent) . (compiler-native-encode (family NvidiaWholeProgramPlan) (constructor NvidiaWholeProgramPlan NvidiaWholeProgramPlanValue selected architecture computeClass spaVersion (phWord programGPU) (phWord qmdGPU) (phWord pushGPU) (phWord semGPU) nvidiaCodeRegionAlignment programBytes regions launches launchCount qmdBytes submissions submissionCount referenceCount))) in (let unrestricted recipes = (nlsRecipe programHost programBytes (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedProgramTable) (nlsRecipe qmdHost qmdBytes (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedQMDTable) (nlsRecipe pushHost pushBytes (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedPushbuffer) (nlsRecipe ringHost -- The allocation holds the cyclic ring; the recipe -- contains only this schedule's initial entries. -- The loader requires its exact expanded extent. (naturalMultiply submissionCount 8) (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO) (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsEnd))))) in (let unrestricted admitted = (naturalAnd (nvidiaSM86RegionsAdmitted regions) (naturalAnd (naturalNonzero launchCount) (naturalAnd (nvidiaProgramSubmissionsAdmitted submissions) (naturalAnd (nvidiaPlanHostLayoutAdmitted layout) (naturalAnd (nvidiaPlanHostLayoutCertified layout nlsHostExtras) (naturalAnd (prRecipesAdmitted layout recipes) (naturalAnd (naturalLessOrEqual (nvidiaPlanHostVideoAllocationBytes layout) availableVideo) (naturalAnd (naturalLessOrEqual (bytes-length (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramProgram))) programBytes) (naturalAnd (naturalEqual (bytes-length (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramQMD))) qmdBytes) (naturalEqual (bytes-length (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramPushbuffer))) pushBytes)))))))))) in (constructor NvidiaProgramPlan NvidiaProgramPlanValue layout component recipes dataHost dataGPU dataBytes admitted))))))))))))))))))))))))))))))))))))))))))) -- Select every compiler-derived recipe once before embedding its closure. def nlsWithProgramRecipes = (lambda unrestricted component : (pi unrestricted selected : (family NvidiaWholeProgramComponent) . Bytes) . (lambda unrestricted emit : (pi unrestricted program : Bytes . (pi unrestricted qmd : Bytes . (pi unrestricted push : Bytes . (pi unrestricted ring : Bytes . Bytes)))) . (emit (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramProgramRecipe)) (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramQMDRecipe)) (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramPushbufferRecipe)) (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramGPFIFORecipe)))))