module Platform.Linux.Nvidia.Compatibility import Hardware.Nvidia.SM86.Command.WholeProgramPlan import Platform.Linux.Nvidia.PlanHost import Std.List import Std.Natural -- The compatibility contract (docs/PRD-ALPHA-REMAINING.md item 5, [12]): -- what an artifact assumes of the card and the driver, set against what a -- device profile states the card supplies, each supply with the kind of -- evidence behind it. -- -- * a DEMAND is the plan's: an ABI it was built against (the driver -- branch whose ioctl layouts the host encodes), a feature it uses (the -- instruction set, unified memory, the compute class), or a resource it -- needs (registers per thread, threads and shared memory per block, -- video memory) -- with the amount, derived from the plan, and whether -- the supply must be exactly that (an ABI, an instruction set) or at -- least that (a resource); -- * a SUPPLY is the profile's, named as the demand is, with its amount -- and its evidence: an ARCHITECTURAL constraint (what the architecture -- defines, named by its source), a MEASUREMENT (what a qualified run on -- that card recorded, named by the record), or a VALIDATED MODEL (what -- a model the gates hold to the card says, named by the model). -- -- Admission takes the demands in order; the first with no supply of its -- name, or a supply that does not meet it, refuses the pairing BY NAME -- (nvidiaCompatibilityRefusal is that name; empty = admitted). A profile -- that drops a supply is refused at the demand that needed it -- (scripts/ci/compatibility-contract.sh). family NvidiaEvidence : Type 0 constructor NvidiaEvidenceArchitectural field unrestricted nvidiaEvidenceArchitecturalSource : Bytes constructor NvidiaEvidenceMeasured field unrestricted nvidiaEvidenceMeasuredRecord : Bytes constructor NvidiaEvidenceModelled field unrestricted nvidiaEvidenceModel : Bytes end-family family NvidiaDemandKind : Type 0 constructor NvidiaDemandABI constructor NvidiaDemandFeature constructor NvidiaDemandResource end-family -- a demand's comparison: the supply exactly the amount, or at least it family NvidiaDemandBound : Type 0 constructor NvidiaDemandExactly constructor NvidiaDemandAtLeast end-family family NvidiaDemand : Type 0 constructor NvidiaDemandValue field unrestricted nvidiaDemandName : Bytes field unrestricted nvidiaDemandKind : (family NvidiaDemandKind) field unrestricted nvidiaDemandBound : (family NvidiaDemandBound) field unrestricted nvidiaDemandAmount : Nat end-family family NvidiaSupply : Type 0 constructor NvidiaSupplyValue field unrestricted nvidiaSupplyName : Bytes field unrestricted nvidiaSupplyAmount : Nat field unrestricted nvidiaSupplyEvidence : (family NvidiaEvidence) end-family def nvidiaDemand = (lambda unrestricted name : Bytes . (lambda unrestricted kind : (family NvidiaDemandKind) . (lambda unrestricted bound : (family NvidiaDemandBound) . (lambda unrestricted amount : Nat . (lambda unrestricted rest : (family StdList (family NvidiaDemand)) . (constructor StdList StdListCons (family NvidiaDemand) (constructor NvidiaDemand NvidiaDemandValue name kind bound amount) rest)))))) def nvidiaSupply = (lambda unrestricted name : Bytes . (lambda unrestricted amount : Nat . (lambda unrestricted evidence : (family NvidiaEvidence) . (lambda unrestricted rest : (family StdList (family NvidiaSupply)) . (constructor StdList StdListCons (family NvidiaSupply) (constructor NvidiaSupply NvidiaSupplyValue name amount evidence) rest))))) def nvidiaNoDemands : (family StdList (family NvidiaDemand)) = (constructor StdList StdListEmpty (family NvidiaDemand)) def nvidiaNoSupplies : (family StdList (family NvidiaSupply)) = (constructor StdList StdListEmpty (family NvidiaSupply)) -- whether a supply meets a demand of the same name (0 when the names differ) def nvidiaSupplyMeets = (lambda unrestricted demand : (family NvidiaDemand) . (lambda unrestricted supply : (family NvidiaSupply) . (eliminate NvidiaDemand (lambda unrestricted current : (family NvidiaDemand) . Nat) demand (branch NvidiaDemandValue name kind bound amount . (eliminate NvidiaSupply (lambda unrestricted current : (family NvidiaSupply) . Nat) supply (branch NvidiaSupplyValue supplied available evidence . (naturalAnd (bytes-equal name supplied) (eliminate NvidiaDemandBound (lambda unrestricted current : (family NvidiaDemandBound) . Nat) bound (branch NvidiaDemandExactly . (naturalEqual available amount)) (branch NvidiaDemandAtLeast . (naturalLessOrEqual amount available)))))))))) def nvidiaDemandMet = (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) . (lambda unrestricted demand : (family NvidiaDemand) . (stdListFold (family NvidiaSupply) Nat (lambda unrestricted supply : (family NvidiaSupply) . (lambda unrestricted rest : Nat . (naturalOr (nvidiaSupplyMeets demand supply) rest))) 0 supplies))) def nvidiaDemandName = (lambda unrestricted demand : (family NvidiaDemand) . (eliminate NvidiaDemand (lambda unrestricted current : (family NvidiaDemand) . Bytes) demand (branch NvidiaDemandValue name kind bound amount . name))) -- the first demand the supplies do not meet, by name; empty when all are met def nvidiaCompatibilityRefusal = (lambda unrestricted demands : (family StdList (family NvidiaDemand)) . (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) . (stdListFold (family NvidiaDemand) Bytes (lambda unrestricted demand : (family NvidiaDemand) . (lambda unrestricted later : Bytes . (nat-eliminate (lambda unrestricted met : Nat . Bytes) (nvidiaDemandName demand) (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . later)) (nvidiaDemandMet supplies demand)))) b"" demands))) -- 1 when admitted def nvidiaCompatibilityAdmitted = (lambda unrestricted demands : (family StdList (family NvidiaDemand)) . (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) . (naturalIsZero (bytes-length (nvidiaCompatibilityRefusal demands supplies))))) -- ---- what a request host demands ---- -- the driver branch its ioctl layouts are for (the host also refuses -- another branch by name at run time: PlanHost.phRootAndDriverBranch), the -- compute class it allocates, and unified memory when its lifecycle is UVM def nvidiaHostDemands = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted rest : (family StdList (family NvidiaDemand)) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family StdList (family NvidiaDemand))) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . (family StdList (family NvidiaDemand))) abi (branch NvidiaPlanHostABIValue mapIoctl nvos46Size dmaOffset status channelClass computeClass usermodeClass engineType driverBranch scheduleParams userdMemory channelFlags directDMAFlags . (nvidiaDemand b"driver-branch" (constructor NvidiaDemandKind NvidiaDemandABI) (constructor NvidiaDemandBound NvidiaDemandExactly) driverBranch (nvidiaDemand b"compute-class" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandExactly) computeClass (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family StdList (family NvidiaDemand))) lifecycle (branch NvidiaPlanHostDirectRM . rest) (branch NvidiaPlanHostUVM base extent . (nvidiaDemand b"unified-memory" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandAtLeast) 1 rest))))))))))) -- ---- what a plan's kernels demand ---- -- the most registers, threads and shared bytes any of its device regions -- declares, per thread and per block def nvidiaRegionsMaximum = (lambda unrestricted field : (pi unrestricted region : (family NvidiaDeviceRegion) . Nat) . (lambda unrestricted regions : (family NvidiaDeviceRegions) . (eliminate NvidiaDeviceRegions (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions (branch NvidiaDeviceRegionsEnd . 0) (branch NvidiaDeviceRegionsNext head tail induction . (naturalSelect (naturalLess induction (field head)) (field head) induction))))) def nvidiaRegionRegisters = (lambda unrestricted region : (family NvidiaDeviceRegion) . (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region (branch NvidiaDeviceRegionValue identity material registers blockX shared . registers) (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . registers) (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . registers))) def nvidiaRegionThreads = (lambda unrestricted region : (family NvidiaDeviceRegion) . (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region (branch NvidiaDeviceRegionValue identity material registers blockX shared . blockX) (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . blockX) (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . blockX))) def nvidiaRegionShared = (lambda unrestricted region : (family NvidiaDeviceRegion) . (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region (branch NvidiaDeviceRegionValue identity material registers blockX shared . shared) (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . shared) (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . shared))) -- a plan's demands: its instruction set (10 x major + minor), its kernels' -- resources, the video memory its arena occupies, then the host's def nvidiaPlanDemands = (lambda unrestricted instructionSet : Nat . (lambda unrestricted regions : (family NvidiaDeviceRegions) . (lambda unrestricted videoMemory : Nat . (lambda unrestricted rest : (family StdList (family NvidiaDemand)) . (nvidiaDemand b"instruction-set" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandExactly) instructionSet (nvidiaDemand b"registers-per-thread" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionRegisters regions) (nvidiaDemand b"threads-per-block" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionThreads regions) (nvidiaDemand b"shared-bytes-per-block" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionShared regions) (nvidiaDemand b"video-memory-bytes" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) videoMemory rest))))))))) -- a little-endian word of text (a driver version's first four bytes) def nvidiaCompatibilityTextWord = (lambda unrestricted text : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . Nat) 0 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat . (naturalAdd (byte-to-nat head) (naturalMultiply 256 induction))))) text)) -- the instruction set a QMD architecture word names (0x86: 8.6, as 86) def nvidiaInstructionSetOf = (lambda unrestricted architecture : Nat . (naturalAdd (naturalMultiply 10 (naturalDivideUnchecked architecture 16)) (naturalModuloUnchecked architecture 16))) -- a profile with one supply dropped (what the contract's refusals are -- stated against) def nvidiaSuppliesWithout = (lambda unrestricted name : Bytes . (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) . (stdListFold (family NvidiaSupply) (family StdList (family NvidiaSupply)) (lambda unrestricted supply : (family NvidiaSupply) . (lambda unrestricted rest : (family StdList (family NvidiaSupply)) . (eliminate NvidiaSupply (lambda unrestricted current : (family NvidiaSupply) . (family StdList (family NvidiaSupply))) supply (branch NvidiaSupplyValue supplied amount evidence . (nat-eliminate (lambda unrestricted same : Nat . (family StdList (family NvidiaSupply))) (constructor StdList StdListCons (family NvidiaSupply) supply rest) (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family StdList (family NvidiaSupply)) . rest)) (bytes-equal name supplied)))))) nvidiaNoSupplies supplies)))