module Realization.Nvidia.SM86.Transpose.FP16SM86 import Accelerator.SM86.Control import Accelerator.SM86.Immediate import Accelerator.SM86.Instruction import Accelerator.SM86.InstructionEncoding import Accelerator.SM86.Program import Accelerator.SM86.Types import Compiler.AST import Compiler.ApplicationBuilder import Data.SHA256Digest import Std.Natural family GroupedTransposeGeometry : Type 0 constructor GroupedTransposeGeometryValue field unrestricted groupedTransposeGroups : Nat field unrestricted groupedTransposeRows : Nat field unrestricted groupedTransposeColumns : Nat end-family family GroupedTransposeGrid : Type 0 constructor GroupedTransposeGridValue field unrestricted groupedTransposeGridX : Nat field unrestricted groupedTransposeGridY : Nat field unrestricted groupedTransposeGridZ : Nat end-family family GroupedTransposeABI : Type 0 constructor GroupedTransposeABIValue field unrestricted groupedTransposeABIConstantBank : Byte field unrestricted groupedTransposeABIOutputPointerOffset : Nat field unrestricted groupedTransposeABIInputPointerOffset : Nat field unrestricted groupedTransposeABIPointerAlignment : Nat field unrestricted groupedTransposeABIElementBytes : Nat field unrestricted groupedTransposeABIPackedWordBytes : Nat field unrestricted groupedTransposeABIBlockX : Nat field unrestricted groupedTransposeABITileRows : Nat field unrestricted groupedTransposeABITileColumns : Nat end-family family GroupedTransposeResourcePolicy : Type 0 constructor GroupedTransposeResourcePolicyValue field unrestricted groupedTransposeResourceRegisters : Nat field unrestricted groupedTransposeResourceSharedBytes : Nat field unrestricted groupedTransposeResourceGlobalLoads : Nat field unrestricted groupedTransposeResourceGlobalStores : Nat field unrestricted groupedTransposeResourceHostFallbackCalls : Nat field unrestricted groupedTransposeResourceHostStagingTransfers : Nat field unrestricted groupedTransposeResourceHostCallbacks : Nat field unrestricted groupedTransposeResourceApplicationBuilderNativeOnly : Nat end-family family GroupedTransposeDifferentialReceipt : Type 0 constructor GroupedTransposeDifferentialReceiptValue field unrestricted groupedTransposeDifferentialReferenceBytes : Nat field unrestricted groupedTransposeDifferentialCandidateBytes : Nat field unrestricted groupedTransposeDifferentialReferenceIdentity : Bytes field unrestricted groupedTransposeDifferentialCandidateIdentity : Bytes field unrestricted groupedTransposeDifferentialEncodingTelemetry : (family SM86ProgramEncodingTelemetry) field unrestricted groupedTransposeDifferentialIdentityTelemetry : (family SHA256DigestTelemetry) field unrestricted groupedTransposeDifferentialRuns : Nat end-family family GroupedTransposeFailureCode : Type 0 constructor GroupedTransposeNoError constructor GroupedTransposeGroupsZero constructor GroupedTransposeGroupsOutOfRange constructor GroupedTransposeDimensionZero constructor GroupedTransposeDimensionNotTileMultiple constructor GroupedTransposeSourceOffsetOverflow constructor GroupedTransposeTensorExtentOverflow constructor GroupedTransposeInstructionCountMismatch constructor GroupedTransposeEncodingFailed constructor GroupedTransposeEncodedByteCountMismatch constructor GroupedTransposeIdentityFailed constructor GroupedTransposeIdentityLengthInvalid constructor GroupedTransposeApplicationBuilderRejected constructor GroupedTransposeHostFallbackObserved constructor GroupedTransposeHostStagingObserved constructor GroupedTransposeHostCallbackObserved constructor GroupedTransposeDifferentialEncodingFailed constructor GroupedTransposeDifferentialEncodedByteCountMismatch constructor GroupedTransposeDifferentialImageMismatch constructor GroupedTransposeDifferentialIdentityFailed constructor GroupedTransposeDifferentialIdentityMismatch end-family family GroupedTransposeTelemetry : Type 0 constructor GroupedTransposeTelemetryValue field unrestricted groupedTransposeTelemetryGroups : Nat field unrestricted groupedTransposeTelemetryRows : Nat field unrestricted groupedTransposeTelemetryColumns : Nat field unrestricted groupedTransposeTelemetryGridX : Nat field unrestricted groupedTransposeTelemetryGridY : Nat field unrestricted groupedTransposeTelemetryGridZ : Nat field unrestricted groupedTransposeTelemetryInstructions : Nat field unrestricted groupedTransposeTelemetryEncodedBytes : Nat field unrestricted groupedTransposeTelemetryGlobalLoads : Nat field unrestricted groupedTransposeTelemetryGlobalStores : Nat field unrestricted groupedTransposeTelemetryRegisters : Nat field unrestricted groupedTransposeTelemetrySharedBytes : Nat field unrestricted groupedTransposeTelemetryHostFallbackCalls : Nat field unrestricted groupedTransposeTelemetryHostStagingTransfers : Nat field unrestricted groupedTransposeTelemetryHostCallbacks : Nat field unrestricted groupedTransposeTelemetryApplicationBuilderNativeOnly : Nat field unrestricted groupedTransposeTelemetryABI : (family GroupedTransposeABI) field unrestricted groupedTransposeTelemetryResourcePolicy : (family GroupedTransposeResourcePolicy) field unrestricted groupedTransposeTelemetryDifferentialRuns : Nat field unrestricted groupedTransposeTelemetryCompositionWitness : (family Term) end-family family GroupedTransposeValidationResult : Type 0 constructor GroupedTransposeGeometryValidated field unrestricted groupedTransposeValidatedGrid : (family GroupedTransposeGrid) constructor GroupedTransposeGeometryRejected field unrestricted groupedTransposeGeometryFailure : (family GroupedTransposeFailureCode) end-family family GroupedTransposeBuildResult : Type 0 constructor GroupedTransposeBuildSucceeded field unrestricted groupedTransposeEncodedBytes : Bytes field unrestricted groupedTransposeImageIdentity : Bytes field unrestricted groupedTransposeBuildABI : (family GroupedTransposeABI) field unrestricted groupedTransposeBuildResourcePolicy : (family GroupedTransposeResourcePolicy) field unrestricted groupedTransposeBuildDifferentialReceipt : (family GroupedTransposeDifferentialReceipt) field unrestricted groupedTransposeEncodingTelemetry : (family SM86ProgramEncodingTelemetry) field unrestricted groupedTransposeIdentityTelemetry : (family SHA256DigestTelemetry) field unrestricted groupedTransposeBuildTelemetry : (family GroupedTransposeTelemetry) constructor GroupedTransposeContractFailed field unrestricted groupedTransposeContractFailure : (family GroupedTransposeFailureCode) field unrestricted groupedTransposeContractTelemetry : (family GroupedTransposeTelemetry) constructor GroupedTransposeImageEncodingFailed field unrestricted groupedTransposeEncodingFailure : (family GroupedTransposeFailureCode) field unrestricted groupedTransposeFailedEncoding : (family SM86ProgramEncodingResult) field unrestricted groupedTransposeEncodingFailureTelemetry : (family GroupedTransposeTelemetry) constructor GroupedTransposeImageIdentityFailed field unrestricted groupedTransposeIdentityFailure : (family GroupedTransposeFailureCode) field unrestricted groupedTransposeFailedIdentity : (family SHA256HexResult) field unrestricted groupedTransposeIdentityFailureTelemetry : (family GroupedTransposeTelemetry) end-family def groupedTransposeOne : Nat = (succ zero) def groupedTransposeN2 : Nat = (byte-to-nat (byte 2)) def groupedTransposeN4 : Nat = (byte-to-nat (byte 4)) def groupedTransposeN10 : Nat = (byte-to-nat (byte 10)) def groupedTransposeN16 : Nat = (byte-to-nat (byte 16)) def groupedTransposeN22 : Nat = (byte-to-nat (byte 22)) def groupedTransposeN32 : Nat = (byte-to-nat (byte 32)) def groupedTransposeN62 : Nat = (byte-to-nat (byte 62)) def groupedTransposeN64 : Nat = (byte-to-nat (byte 64)) def groupedTransposeN160 : Nat = (byte-to-nat (byte 160)) def groupedTransposeN256 : Nat = (succ (byte-to-nat (byte 255))) def groupedTransposeInstructionCount : Nat = (byte-to-nat (byte 183)) def groupedTransposeRegisterCount : Nat = groupedTransposeN32 def groupedTransposeSharedBytes : Nat = zero def groupedTransposeEncodedByteCount : Nat = (naturalMultiply groupedTransposeInstructionCount groupedTransposeN16) def groupedTransposeBase256 : Nat = (succ (byte-to-nat (byte 255))) def groupedTransposeMaximumGroups : Nat = (naturalPredecessor (naturalPowerOfTwo groupedTransposeN16)) def groupedTransposeMaximumOffset24 : Nat = (naturalPredecessor (naturalPowerOfTwo (byte-to-nat (byte 24)))) def groupedTransposeMaximumWord32 : Nat = (naturalPredecessor (naturalPowerOfTwo groupedTransposeN32)) def groupedTransposeHostFallbackCalls : Nat = zero def groupedTransposeHostStagingTransfers : Nat = zero def groupedTransposeHostCallbacks : Nat = zero def groupedTransposeDifferentialRuns : Nat = groupedTransposeN2 def groupedTransposePointerAlignment : Nat = groupedTransposeN4 def groupedTransposeElementBytes : Nat = groupedTransposeN2 def groupedTransposePackedWordBytes : Nat = groupedTransposeN4 -- CB0 contains the destination pointer before the source pointer. Keep the -- launch ABI with the realization so consumers do not restate slot numbers. def groupedTransposeOutputArgument : Nat = 0 def groupedTransposeInputArgument : Nat = 1 def groupedTransposeArgumentCount : Nat = groupedTransposeN2 def groupedTransposeOutputPointerOffset : Nat = (naturalAdd (byte-to-nat (byte 96)) groupedTransposeN256) def groupedTransposeInputPointerOffset : Nat = (naturalAdd (byte-to-nat (byte 104)) groupedTransposeN256) def groupedTransposeApplicationWitness : (family Term) = (Compiler.ApplicationBuilder/app2 (constructor Term Variable b"grouped-transpose") (constructor Term NaturalLiteral groupedTransposeN32) (constructor Term NaturalLiteral groupedTransposeInstructionCount)) def groupedTransposeABI : (family GroupedTransposeABI) = (constructor GroupedTransposeABI GroupedTransposeABIValue (byte 0) groupedTransposeOutputPointerOffset groupedTransposeInputPointerOffset groupedTransposePointerAlignment groupedTransposeElementBytes groupedTransposePackedWordBytes groupedTransposeN32 groupedTransposeN32 groupedTransposeN32) def groupedTransposeResourcePolicy : (family GroupedTransposeResourcePolicy) = (constructor GroupedTransposeResourcePolicy GroupedTransposeResourcePolicyValue groupedTransposeRegisterCount groupedTransposeSharedBytes groupedTransposeN32 groupedTransposeN32 groupedTransposeHostFallbackCalls groupedTransposeHostStagingTransfers groupedTransposeHostCallbacks applicationBuilderNativeOnly) def groupedTransposeFailureStableCode : (pi unrestricted code : (family GroupedTransposeFailureCode) . Bytes) = (lambda unrestricted code : (family GroupedTransposeFailureCode) . (eliminate GroupedTransposeFailureCode (lambda unrestricted current : (family GroupedTransposeFailureCode) . Bytes) code (branch GroupedTransposeNoError . b"ALPHA-TR-000") (branch GroupedTransposeGroupsZero . b"ALPHA-TR-001") (branch GroupedTransposeGroupsOutOfRange . b"ALPHA-TR-002") (branch GroupedTransposeDimensionZero . b"ALPHA-TR-003") (branch GroupedTransposeDimensionNotTileMultiple . b"ALPHA-TR-004") (branch GroupedTransposeSourceOffsetOverflow . b"ALPHA-TR-005") (branch GroupedTransposeTensorExtentOverflow . b"ALPHA-TR-006") (branch GroupedTransposeInstructionCountMismatch . b"ALPHA-TR-007") (branch GroupedTransposeEncodingFailed . b"ALPHA-TR-008") (branch GroupedTransposeEncodedByteCountMismatch . b"ALPHA-TR-009") (branch GroupedTransposeIdentityFailed . b"ALPHA-TR-010") (branch GroupedTransposeIdentityLengthInvalid . b"ALPHA-TR-011") (branch GroupedTransposeApplicationBuilderRejected . b"ALPHA-TR-012") (branch GroupedTransposeHostFallbackObserved . b"ALPHA-TR-013") (branch GroupedTransposeHostStagingObserved . b"ALPHA-TR-014") (branch GroupedTransposeHostCallbackObserved . b"ALPHA-TR-015") (branch GroupedTransposeDifferentialEncodingFailed . b"ALPHA-TR-016") (branch GroupedTransposeDifferentialEncodedByteCountMismatch . b"ALPHA-TR-017") (branch GroupedTransposeDifferentialImageMismatch . b"ALPHA-TR-018") (branch GroupedTransposeDifferentialIdentityFailed . b"ALPHA-TR-019") (branch GroupedTransposeDifferentialIdentityMismatch . b"ALPHA-TR-020"))) def groupedTransposeNaturalByte = (lambda unrestricted value : Nat . (nat-to-byte (naturalModuloUnchecked value groupedTransposeBase256))) def groupedTransposeNaturalQuotient256 = (lambda unrestricted value : Nat . (naturalDivideUnchecked value groupedTransposeBase256)) def groupedTransposeUnsigned32FromNatural = (lambda unrestricted value : Nat . (Accelerator.SM86.Immediate/sm86Unsigned32 (groupedTransposeNaturalByte value) (groupedTransposeNaturalByte (groupedTransposeNaturalQuotient256 value)) (groupedTransposeNaturalByte (groupedTransposeNaturalQuotient256 (groupedTransposeNaturalQuotient256 value))) (groupedTransposeNaturalByte (groupedTransposeNaturalQuotient256 (groupedTransposeNaturalQuotient256 (groupedTransposeNaturalQuotient256 value)))))) def groupedTransposeU0 = (groupedTransposeUnsigned32FromNatural zero) def groupedTransposeU4 = (groupedTransposeUnsigned32FromNatural groupedTransposeN4) def groupedTransposeU16 = (groupedTransposeUnsigned32FromNatural groupedTransposeN16) def groupedTransposeU65535 = (groupedTransposeUnsigned32FromNatural groupedTransposeMaximumGroups) def groupedTransposeConstantBase = (groupedTransposeUnsigned32FromNatural (byte-to-nat (byte 40))) def groupedTransposeInputPointer = (groupedTransposeUnsigned32FromNatural groupedTransposeInputPointerOffset) def groupedTransposeOutputPointer = (groupedTransposeUnsigned32FromNatural groupedTransposeOutputPointerOffset) def groupedTransposeR = (lambda unrestricted value : Byte . (sm86Register value)) def groupedTransposeR0 = (groupedTransposeR (byte 0)) def groupedTransposeR1 = (groupedTransposeR (byte 1)) def groupedTransposeR2 = (groupedTransposeR (byte 2)) def groupedTransposeR3 = (groupedTransposeR (byte 3)) def groupedTransposeR4 = (groupedTransposeR (byte 4)) def groupedTransposeR5 = (groupedTransposeR (byte 5)) def groupedTransposeR6 = (groupedTransposeR (byte 6)) def groupedTransposeR8 = (groupedTransposeR (byte 8)) def groupedTransposeR10 = (groupedTransposeR (byte 10)) def groupedTransposeR12 = (groupedTransposeR (byte 12)) def groupedTransposeR13 = (groupedTransposeR (byte 13)) def groupedTransposeR14 = (groupedTransposeR (byte 14)) def groupedTransposeR15 = (groupedTransposeR (byte 15)) def groupedTransposeR16 = (groupedTransposeR (byte 16)) def groupedTransposeR17 = (groupedTransposeR (byte 17)) def groupedTransposeR18 = (groupedTransposeR (byte 18)) def groupedTransposeR19 = (groupedTransposeR (byte 19)) def groupedTransposeR20 = (groupedTransposeR (byte 20)) def groupedTransposeR22 = (groupedTransposeR (byte 22)) def groupedTransposeR24 = (groupedTransposeR (byte 24)) def groupedTransposeSet0 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0)) def groupedTransposeWait0 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0)) def groupedTransposeNext = (lambda unrestricted body : (family SM86InstructionBody) . (lambda unrestricted tail : (family SM86Program) . (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail))) def validateGroupedTransposeGeometry = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (eliminate GroupedTransposeGeometry (lambda unrestricted current : (family GroupedTransposeGeometry) . (family GroupedTransposeValidationResult)) geometry (branch GroupedTransposeGeometryValue groups rows columns . (nat-eliminate (lambda unrestricted groupsPositive : Nat . (family GroupedTransposeValidationResult)) (constructor GroupedTransposeValidationResult GroupedTransposeGeometryRejected (constructor GroupedTransposeFailureCode GroupedTransposeGroupsZero)) (lambda unrestricted groupsPred : Nat . (lambda unrestricted groupsInd : (family GroupedTransposeValidationResult) . (nat-eliminate (lambda unrestricted groupsBounded : Nat . (family GroupedTransposeValidationResult)) (constructor GroupedTransposeValidationResult GroupedTransposeGeometryRejected (constructor GroupedTransposeFailureCode GroupedTransposeGroupsOutOfRange)) (lambda unrestricted groupsBoundPred : Nat . (lambda unrestricted groupsBoundInd : (family GroupedTransposeValidationResult) . (nat-eliminate (lambda unrestricted dimensionsPositive : Nat . (family GroupedTransposeValidationResult)) (constructor GroupedTransposeValidationResult GroupedTransposeGeometryRejected (constructor GroupedTransposeFailureCode GroupedTransposeDimensionZero)) (lambda unrestricted dimensionsPred : Nat . (lambda unrestricted dimensionsInd : (family GroupedTransposeValidationResult) . (nat-eliminate (lambda unrestricted tileExact : Nat . (family GroupedTransposeValidationResult)) (constructor GroupedTransposeValidationResult GroupedTransposeGeometryRejected (constructor GroupedTransposeFailureCode GroupedTransposeDimensionNotTileMultiple)) (lambda unrestricted tilePred : Nat . (lambda unrestricted tileInd : (family GroupedTransposeValidationResult) . (nat-eliminate (lambda unrestricted sourceOffsetBounded : Nat . (family GroupedTransposeValidationResult)) (constructor GroupedTransposeValidationResult GroupedTransposeGeometryRejected (constructor GroupedTransposeFailureCode GroupedTransposeSourceOffsetOverflow)) (lambda unrestricted sourcePred : Nat . (lambda unrestricted sourceInd : (family GroupedTransposeValidationResult) . (nat-eliminate (lambda unrestricted extentBounded : Nat . (family GroupedTransposeValidationResult)) (constructor GroupedTransposeValidationResult GroupedTransposeGeometryRejected (constructor GroupedTransposeFailureCode GroupedTransposeTensorExtentOverflow)) (lambda unrestricted extentPred : Nat . (lambda unrestricted extentInd : (family GroupedTransposeValidationResult) . (constructor GroupedTransposeValidationResult GroupedTransposeGeometryValidated (constructor GroupedTransposeGrid GroupedTransposeGridValue (naturalDivideUnchecked columns groupedTransposeN32) (naturalDivideUnchecked rows groupedTransposeN32) groups)))) (naturalFitsWord32 (naturalDivideUnchecked (naturalMultiply groups (naturalMultiply rows columns)) groupedTransposeN2))))) (naturalBelowTwoPower (byte-to-nat (byte 24)) (naturalMultiply groupedTransposeN62 columns))))) (naturalAnd (naturalIsZero (naturalModuloUnchecked rows groupedTransposeN32)) (naturalIsZero (naturalModuloUnchecked columns groupedTransposeN32)))))) (naturalAnd (naturalNonzero rows) (naturalNonzero columns))))) (naturalBelowTwoPower groupedTransposeN16 groups)))) (naturalNonzero groups))))) def groupedTransposeGrid = validateGroupedTransposeGeometry def groupedTransposePrefix = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (eliminate GroupedTransposeGeometry (lambda unrestricted current : (family GroupedTransposeGeometry) . (family SM86Program)) geometry (branch GroupedTransposeGeometryValue groups rows columns . (groupedTransposeNext (constructor SM86InstructionBody SM86MoveConstant groupedTransposeR1 (byte 0) groupedTransposeConstantBase sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86SpecialToRegister groupedTransposeR2 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86MoveImmediate groupedTransposeR3 groupedTransposeU4 groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86SpecialToRegister groupedTransposeR4 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate groupedTransposeR4 groupedTransposeR4 groupedTransposeU0 groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86SpecialToRegister groupedTransposeR5 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdZ) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate groupedTransposeR5 groupedTransposeR5 groupedTransposeU0 groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86SpecialToRegister groupedTransposeR0 (constructor SM86SpecialRegister SM86ThreadIdX) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate groupedTransposeR0 groupedTransposeR0 groupedTransposeU0 groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86MoveImmediate groupedTransposeR6 groupedTransposeU65535 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR8 groupedTransposeR5 (groupedTransposeUnsigned32FromNatural (naturalDivideUnchecked (naturalMultiply rows columns) groupedTransposeN2)) sm86ZeroRegister sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR8 groupedTransposeR4 (groupedTransposeUnsigned32FromNatural (naturalMultiply groupedTransposeN16 columns)) groupedTransposeR8 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR8 groupedTransposeR2 groupedTransposeU16 groupedTransposeR8 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR8 groupedTransposeR0 (groupedTransposeUnsigned32FromNatural groupedTransposeOne) groupedTransposeR8 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant groupedTransposeR10 groupedTransposeR8 groupedTransposeR3 (byte 0) groupedTransposeInputPointer sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR20 groupedTransposeR5 (groupedTransposeUnsigned32FromNatural (naturalDivideUnchecked (naturalMultiply rows columns) groupedTransposeN2)) sm86ZeroRegister sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR20 groupedTransposeR2 (groupedTransposeUnsigned32FromNatural (naturalMultiply groupedTransposeN16 rows)) groupedTransposeR20 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR20 groupedTransposeR0 (groupedTransposeUnsigned32FromNatural rows) groupedTransposeR20 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR20 groupedTransposeR4 groupedTransposeU16 groupedTransposeR20 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant groupedTransposeR22 groupedTransposeR20 groupedTransposeR3 (byte 0) groupedTransposeOutputPointer sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate groupedTransposeR20 groupedTransposeR20 (groupedTransposeUnsigned32FromNatural (naturalDivideUnchecked rows groupedTransposeN2)) sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant groupedTransposeR24 groupedTransposeR20 groupedTransposeR3 (byte 0) groupedTransposeOutputPointer sm86SafeControl) (constructor SM86Program SM86ProgramEnd)))))))))))))))))))))))))) def groupedTransposeRowPair = (lambda unrestricted pairIndex : Nat . (lambda unrestricted columns : Nat . (lambda unrestricted tail : (family SM86Program) . (groupedTransposeNext (constructor SM86InstructionBody SM86LoadGlobal groupedTransposeR12 groupedTransposeR10 (groupedTransposeUnsigned32FromNatural (naturalMultiply pairIndex (naturalMultiply groupedTransposeN4 columns))) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86LogicThreeInputTruthTable groupedTransposeR14 groupedTransposeR12 groupedTransposeR6 (byte 192) groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86ShiftRightImmediate groupedTransposeR15 groupedTransposeR12 (byte 16) sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86LoadGlobal groupedTransposeR13 groupedTransposeR10 (groupedTransposeUnsigned32FromNatural (naturalMultiply (succ (naturalMultiply pairIndex groupedTransposeN2)) (naturalMultiply groupedTransposeN2 columns))) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86LogicThreeInputTruthTable groupedTransposeR16 groupedTransposeR13 groupedTransposeR6 (byte 192) groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86ShiftRightImmediate groupedTransposeR17 groupedTransposeR13 (byte 16) sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR18 groupedTransposeR16 (groupedTransposeUnsigned32FromNatural (naturalPowerOfTwo groupedTransposeN16)) groupedTransposeR14 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR19 groupedTransposeR17 (groupedTransposeUnsigned32FromNatural (naturalPowerOfTwo groupedTransposeN16)) groupedTransposeR15 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86StoreGlobal groupedTransposeR22 groupedTransposeR18 (groupedTransposeUnsigned32FromNatural (naturalMultiply pairIndex groupedTransposeN4)) sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86StoreGlobal groupedTransposeR24 groupedTransposeR19 (groupedTransposeUnsigned32FromNatural (naturalMultiply pairIndex groupedTransposeN4)) sm86SafeControl) tail))))))))))))) def groupedTransposeRows = (lambda unrestricted count : Nat . (lambda unrestricted columns : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family SM86Program)) (constructor SM86Program SM86ProgramEnd) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SM86Program) . (groupedTransposeRowPair predecessor columns induction))) count))) def emitGroupedTransposeFP16SM86 = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (eliminate GroupedTransposeGeometry (lambda unrestricted current : (family GroupedTransposeGeometry) . (family SM86Program)) geometry (branch GroupedTransposeGeometryValue groups rows columns . (sm86ProgramAppend (groupedTransposePrefix geometry) (sm86ProgramAppend (groupedTransposeRows groupedTransposeN16 columns) (groupedTransposeNext (constructor SM86InstructionBody SM86Exit sm86SafeControl) (constructor SM86Program SM86ProgramEnd))))))) def groupedTransposeTelemetryFor = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (lambda unrestricted instructions : Nat . (lambda unrestricted encodedBytes : Nat . (eliminate GroupedTransposeGeometry (lambda unrestricted current : (family GroupedTransposeGeometry) . (family GroupedTransposeTelemetry)) geometry (branch GroupedTransposeGeometryValue groups rows columns . (constructor GroupedTransposeTelemetry GroupedTransposeTelemetryValue groups rows columns (naturalDivideUnchecked columns groupedTransposeN32) (naturalDivideUnchecked rows groupedTransposeN32) groups instructions encodedBytes groupedTransposeN32 groupedTransposeN32 groupedTransposeRegisterCount groupedTransposeSharedBytes groupedTransposeHostFallbackCalls groupedTransposeHostStagingTransfers groupedTransposeHostCallbacks applicationBuilderNativeOnly groupedTransposeABI groupedTransposeResourcePolicy groupedTransposeDifferentialRuns groupedTransposeApplicationWitness)))))) def groupedTransposeEmptyTelemetry = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (groupedTransposeTelemetryFor geometry zero zero)) def groupedTransposeObservedTelemetry = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (lambda unrestricted instructions : Nat . (lambda unrestricted encodedBytes : Nat . (groupedTransposeTelemetryFor geometry instructions encodedBytes)))) def groupedTransposeContractFailureFor = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (lambda unrestricted instructions : Nat . (lambda unrestricted encodedBytes : Nat . (lambda unrestricted failure : (family GroupedTransposeFailureCode) . (constructor GroupedTransposeBuildResult GroupedTransposeContractFailed failure (groupedTransposeObservedTelemetry geometry instructions encodedBytes)))))) def groupedTransposeEncodingFailureFor = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (lambda unrestricted instructions : Nat . (lambda unrestricted encodedBytes : Nat . (lambda unrestricted failure : (family GroupedTransposeFailureCode) . (lambda unrestricted encoding : (family SM86ProgramEncodingResult) . (constructor GroupedTransposeBuildResult GroupedTransposeImageEncodingFailed failure encoding (groupedTransposeObservedTelemetry geometry instructions encodedBytes))))))) def groupedTransposeIdentityFailureFor = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (lambda unrestricted instructions : Nat . (lambda unrestricted encodedBytes : Nat . (lambda unrestricted failure : (family GroupedTransposeFailureCode) . (lambda unrestricted identityResult : (family SHA256HexResult) . (constructor GroupedTransposeBuildResult GroupedTransposeImageIdentityFailed failure identityResult (groupedTransposeObservedTelemetry geometry instructions encodedBytes))))))) def groupedTransposeDifferentialIdentity = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (lambda unrestricted count : Nat . (lambda unrestricted bytes : Bytes . (lambda unrestricted identity : Bytes . (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) . (lambda unrestricted identityTelemetry : (family SHA256DigestTelemetry) . (lambda unrestricted candidateBytes : Bytes . (lambda unrestricted candidateEncodingTelemetry : (family SM86ProgramEncodingTelemetry) . (lambda unrestricted candidateIdentityResult : (family SHA256HexResult) . (eliminate SHA256HexResult (lambda unrestricted current : (family SHA256HexResult) . (family GroupedTransposeBuildResult)) candidateIdentityResult (branch SHA256HexSucceeded candidateIdentity candidateIdentityTelemetry . (nat-eliminate (lambda unrestricted identityLengthExact : Nat . (family GroupedTransposeBuildResult)) (groupedTransposeIdentityFailureFor geometry count (bytes-length candidateBytes) (constructor GroupedTransposeFailureCode GroupedTransposeIdentityLengthInvalid) candidateIdentityResult) (lambda unrestricted identityLengthPred : Nat . (lambda unrestricted identityLengthInd : (family GroupedTransposeBuildResult) . (nat-eliminate (lambda unrestricted identityExact : Nat . (family GroupedTransposeBuildResult)) (groupedTransposeContractFailureFor geometry count (bytes-length candidateBytes) (constructor GroupedTransposeFailureCode GroupedTransposeDifferentialIdentityMismatch)) (lambda unrestricted identityPred : Nat . (lambda unrestricted identityInd : (family GroupedTransposeBuildResult) . (constructor GroupedTransposeBuildResult GroupedTransposeBuildSucceeded bytes identity groupedTransposeABI groupedTransposeResourcePolicy (constructor GroupedTransposeDifferentialReceipt GroupedTransposeDifferentialReceiptValue (bytes-length bytes) (bytes-length candidateBytes) identity candidateIdentity candidateEncodingTelemetry candidateIdentityTelemetry groupedTransposeDifferentialRuns) encodingTelemetry identityTelemetry (groupedTransposeObservedTelemetry geometry count (bytes-length bytes))))) (bytes-equal identity candidateIdentity)))) (naturalEqual (bytes-length candidateIdentity) groupedTransposeN64))) (branch SHA256HexFailed error ordinal candidateIdentityTelemetry . (groupedTransposeIdentityFailureFor geometry count (bytes-length candidateBytes) (constructor GroupedTransposeFailureCode GroupedTransposeDifferentialIdentityFailed) candidateIdentityResult)))))))))))) def groupedTransposeDifferentialEncoding = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (lambda unrestricted count : Nat . (lambda unrestricted bytes : Bytes . (lambda unrestricted identity : Bytes . (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) . (lambda unrestricted identityTelemetry : (family SHA256DigestTelemetry) . (lambda unrestricted candidateEncoding : (family SM86ProgramEncodingResult) . (eliminate SM86ProgramEncodingResult (lambda unrestricted current : (family SM86ProgramEncodingResult) . (family GroupedTransposeBuildResult)) candidateEncoding (branch SM86ProgramEncodingSucceeded candidateBytes candidateTelemetry . (nat-eliminate (lambda unrestricted candidateLengthExact : Nat . (family GroupedTransposeBuildResult)) (groupedTransposeContractFailureFor geometry count (bytes-length candidateBytes) (constructor GroupedTransposeFailureCode GroupedTransposeDifferentialEncodedByteCountMismatch)) (lambda unrestricted candidateLengthPred : Nat . (lambda unrestricted candidateLengthInd : (family GroupedTransposeBuildResult) . (nat-eliminate (lambda unrestricted imageExact : Nat . (family GroupedTransposeBuildResult)) (groupedTransposeContractFailureFor geometry count (bytes-length candidateBytes) (constructor GroupedTransposeFailureCode GroupedTransposeDifferentialImageMismatch)) (lambda unrestricted imagePred : Nat . (lambda unrestricted imageInd : (family GroupedTransposeBuildResult) . (groupedTransposeDifferentialIdentity geometry count bytes identity encodingTelemetry identityTelemetry candidateBytes candidateTelemetry (sha256Hex candidateBytes)))) (bytes-equal bytes candidateBytes)))) (naturalEqual (bytes-length candidateBytes) groupedTransposeEncodedByteCount))) (branch SM86ProgramEncodingFailed index failure candidateTelemetry . (groupedTransposeEncodingFailureFor geometry count (bytes-length bytes) (constructor GroupedTransposeFailureCode GroupedTransposeDifferentialEncodingFailed) candidateEncoding)))))))))) def groupedTransposeFinalizeNative = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (lambda unrestricted program : (family SM86Program) . (lambda unrestricted count : Nat . (lambda unrestricted bytes : Bytes . (lambda unrestricted identity : Bytes . (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) . (lambda unrestricted identityTelemetry : (family SHA256DigestTelemetry) . (nat-eliminate (lambda unrestricted builderNative : Nat . (family GroupedTransposeBuildResult)) (groupedTransposeContractFailureFor geometry count (bytes-length bytes) (constructor GroupedTransposeFailureCode GroupedTransposeApplicationBuilderRejected)) (lambda unrestricted builderPred : Nat . (lambda unrestricted builderInd : (family GroupedTransposeBuildResult) . (nat-eliminate (lambda unrestricted fallbackFree : Nat . (family GroupedTransposeBuildResult)) (groupedTransposeContractFailureFor geometry count (bytes-length bytes) (constructor GroupedTransposeFailureCode GroupedTransposeHostFallbackObserved)) (lambda unrestricted fallbackPred : Nat . (lambda unrestricted fallbackInd : (family GroupedTransposeBuildResult) . (nat-eliminate (lambda unrestricted stagingFree : Nat . (family GroupedTransposeBuildResult)) (groupedTransposeContractFailureFor geometry count (bytes-length bytes) (constructor GroupedTransposeFailureCode GroupedTransposeHostStagingObserved)) (lambda unrestricted stagingPred : Nat . (lambda unrestricted stagingInd : (family GroupedTransposeBuildResult) . (nat-eliminate (lambda unrestricted callbackFree : Nat . (family GroupedTransposeBuildResult)) (groupedTransposeContractFailureFor geometry count (bytes-length bytes) (constructor GroupedTransposeFailureCode GroupedTransposeHostCallbackObserved)) (lambda unrestricted callbackPred : Nat . (lambda unrestricted callbackInd : (family GroupedTransposeBuildResult) . (groupedTransposeDifferentialEncoding geometry count bytes identity encodingTelemetry identityTelemetry (sm86EncodeProgram program)))) (naturalEqual groupedTransposeHostCallbacks zero)))) (naturalEqual groupedTransposeHostStagingTransfers zero)))) (naturalEqual groupedTransposeHostFallbackCalls zero)))) applicationBuilderNativeOnly)))))))) def groupedTransposeBuildEncoded = (lambda unrestricted geometry : (family GroupedTransposeGeometry) . (eliminate GroupedTransposeValidationResult (lambda unrestricted current : (family GroupedTransposeValidationResult) . (family GroupedTransposeBuildResult)) (validateGroupedTransposeGeometry geometry) (branch GroupedTransposeGeometryValidated grid . (app (lambda unrestricted program : (family SM86Program) . (app (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted countExact : Nat . (family GroupedTransposeBuildResult)) (constructor GroupedTransposeBuildResult GroupedTransposeContractFailed (constructor GroupedTransposeFailureCode GroupedTransposeInstructionCountMismatch) (groupedTransposeTelemetryFor geometry count zero)) (lambda unrestricted countPred : Nat . (lambda unrestricted countInd : (family GroupedTransposeBuildResult) . (app (lambda unrestricted encoding : (family SM86ProgramEncodingResult) . (eliminate SM86ProgramEncodingResult (lambda unrestricted current : (family SM86ProgramEncodingResult) . (family GroupedTransposeBuildResult)) encoding (branch SM86ProgramEncodingSucceeded bytes encodingTelemetry . (nat-eliminate (lambda unrestricted bytesExact : Nat . (family GroupedTransposeBuildResult)) (constructor GroupedTransposeBuildResult GroupedTransposeContractFailed (constructor GroupedTransposeFailureCode GroupedTransposeEncodedByteCountMismatch) (groupedTransposeTelemetryFor geometry count (bytes-length bytes))) (lambda unrestricted bytesPred : Nat . (lambda unrestricted bytesInd : (family GroupedTransposeBuildResult) . (app (lambda unrestricted identityResult : (family SHA256HexResult) . (eliminate SHA256HexResult (lambda unrestricted current : (family SHA256HexResult) . (family GroupedTransposeBuildResult)) identityResult (branch SHA256HexSucceeded identity identityTelemetry . (nat-eliminate (lambda unrestricted identityExact : Nat . (family GroupedTransposeBuildResult)) (constructor GroupedTransposeBuildResult GroupedTransposeImageIdentityFailed (constructor GroupedTransposeFailureCode GroupedTransposeIdentityLengthInvalid) identityResult (groupedTransposeTelemetryFor geometry count (bytes-length bytes))) (lambda unrestricted identityPred : Nat . (lambda unrestricted identityInd : (family GroupedTransposeBuildResult) . (groupedTransposeFinalizeNative geometry program count bytes identity encodingTelemetry identityTelemetry))) (naturalEqual (bytes-length identity) groupedTransposeN64))) (branch SHA256HexFailed error ordinal identityTelemetry . (constructor GroupedTransposeBuildResult GroupedTransposeImageIdentityFailed (constructor GroupedTransposeFailureCode GroupedTransposeIdentityFailed) identityResult (groupedTransposeTelemetryFor geometry count (bytes-length bytes)))))) (sha256Hex bytes)))) (naturalEqual (bytes-length bytes) groupedTransposeEncodedByteCount))) (branch SM86ProgramEncodingFailed index failure encodingTelemetry . (constructor GroupedTransposeBuildResult GroupedTransposeImageEncodingFailed (constructor GroupedTransposeFailureCode GroupedTransposeEncodingFailed) encoding (groupedTransposeTelemetryFor geometry count zero))))) (sm86EncodeProgram program)))) (naturalEqual count groupedTransposeInstructionCount))) (sm86ProgramCount program))) (emitGroupedTransposeFP16SM86 geometry))) (branch GroupedTransposeGeometryRejected failure . (constructor GroupedTransposeBuildResult GroupedTransposeContractFailed failure (groupedTransposeEmptyTelemetry geometry))))) -- Coppelius uses a deliberately small tiled transpose realization for dense -- backward operands. A CTA owns a pair of input rows and one 128-column tile; -- every one of its 64 threads owns two adjacent columns. The two source packed -- words are unpacked and then repacked as two adjacent-row destination words. -- This makes every global access 32-bit while preserving each FP16 payload -- bit-for-bit, without making the block width grow with the matrix width. -- -- Launch contract for rows x columns: -- grid = (rows / 2, columns / tile, groups) -- block = (tile / 2, 1, 1) (coppeliusFP16TransposeBlockThreads) -- c[0][0x160] = output pointer, c[0][0x168] = input pointer -- Rows must be even and columns must be a multiple of 128. Every Coppelius -- activation and weight geometry satisfies that contract, including the -- 1408-wide feed-forward and 12288-wide vocabulary matrices. def coppeliusFP16TransposeInstructionCount : Nat = (byte-to-nat (byte 31)) def coppeliusFP16TransposeRegisterCount : Nat = (byte-to-nat (byte 27)) def coppeliusFP16TransposeTiledProgram = (lambda unrestricted tileColumns : Nat . (app (lambda unrestricted halfTileColumns : Nat . (lambda unrestricted groups : Nat . (lambda unrestricted rows : Nat . (lambda unrestricted columns : Nat . (app (lambda unrestricted halfRows : Nat . (app (lambda unrestricted halfColumns : Nat . (app (lambda unrestricted groupWords : Nat . (groupedTransposeNext (constructor SM86InstructionBody SM86SpecialToRegister groupedTransposeR0 (constructor SM86SpecialRegister SM86ThreadIdX) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR4 groupedTransposeR0 (groupedTransposeUnsigned32FromNatural groupedTransposeN2) sm86ZeroRegister groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86SpecialToRegister groupedTransposeR1 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR14 groupedTransposeR1 (groupedTransposeUnsigned32FromNatural columns) sm86ZeroRegister groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86SpecialToRegister groupedTransposeR2 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86SpecialToRegister (groupedTransposeR (byte 26)) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdZ) groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR5 (groupedTransposeR (byte 26)) (groupedTransposeUnsigned32FromNatural groupWords) sm86ZeroRegister groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86MoveImmediate groupedTransposeR3 groupedTransposeU4 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR14 groupedTransposeR5 (groupedTransposeUnsigned32FromNatural groupedTransposeOne) groupedTransposeR14 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR14 groupedTransposeR2 (groupedTransposeUnsigned32FromNatural halfTileColumns) groupedTransposeR14 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR14 groupedTransposeR0 (groupedTransposeUnsigned32FromNatural groupedTransposeOne) groupedTransposeR14 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate groupedTransposeR15 groupedTransposeR14 (groupedTransposeUnsigned32FromNatural halfColumns) sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant groupedTransposeR6 groupedTransposeR14 groupedTransposeR3 (byte 0) groupedTransposeInputPointer sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant groupedTransposeR8 groupedTransposeR15 groupedTransposeR3 (byte 0) groupedTransposeInputPointer sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR4 groupedTransposeR2 (groupedTransposeUnsigned32FromNatural tileColumns) groupedTransposeR4 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR16 groupedTransposeR4 (groupedTransposeUnsigned32FromNatural halfRows) groupedTransposeR1 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate groupedTransposeR16 groupedTransposeR5 (groupedTransposeUnsigned32FromNatural groupedTransposeOne) groupedTransposeR16 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerAddThreeImmediate groupedTransposeR17 groupedTransposeR16 (groupedTransposeUnsigned32FromNatural halfRows) sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant groupedTransposeR10 groupedTransposeR16 groupedTransposeR3 (byte 0) groupedTransposeOutputPointer sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant groupedTransposeR12 groupedTransposeR17 groupedTransposeR3 (byte 0) groupedTransposeOutputPointer sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86LoadGlobal groupedTransposeR18 groupedTransposeR6 groupedTransposeU0 groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86HalfToFloat groupedTransposeR20 groupedTransposeR18 (constructor SM86HalfSelector SM86LowHalf) groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86HalfToFloat groupedTransposeR22 groupedTransposeR18 (constructor SM86HalfSelector SM86HighHalf) sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86LoadGlobal groupedTransposeR19 groupedTransposeR8 groupedTransposeU0 groupedTransposeSet0) (groupedTransposeNext (constructor SM86InstructionBody SM86HalfToFloat (groupedTransposeR (byte 21)) groupedTransposeR19 (constructor SM86HalfSelector SM86LowHalf) groupedTransposeWait0) (groupedTransposeNext (constructor SM86InstructionBody SM86HalfToFloat (groupedTransposeR (byte 23)) groupedTransposeR19 (constructor SM86HalfSelector SM86HighHalf) sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86FloatPairToPackedHalfPair groupedTransposeR24 (groupedTransposeR (byte 21)) groupedTransposeR20 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86FloatPairToPackedHalfPair (groupedTransposeR (byte 25)) (groupedTransposeR (byte 23)) groupedTransposeR22 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86StoreGlobal groupedTransposeR10 groupedTransposeR24 groupedTransposeU0 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86StoreGlobal groupedTransposeR12 (groupedTransposeR (byte 25)) groupedTransposeU0 sm86SafeControl) (groupedTransposeNext (constructor SM86InstructionBody SM86Exit sm86SafeControl) (constructor SM86Program SM86ProgramEnd))))))))))))))))))))))))))))))))) (naturalDivideUnchecked (naturalMultiply rows columns) groupedTransposeN2))) (naturalDivideUnchecked columns groupedTransposeN2))) (naturalDivideUnchecked rows groupedTransposeN2)))))) (naturalDivideUnchecked tileColumns groupedTransposeN2))) def coppeliusFP16TransposeProgram = (lambda unrestricted groups : Nat . (lambda unrestricted rows : Nat . (lambda unrestricted columns : Nat . (coppeliusFP16TransposeTiledProgram 128 groups rows columns)))) def coppeliusFP16Transpose64TileProgram = (lambda unrestricted groups : Nat . (lambda unrestricted rows : Nat . (lambda unrestricted columns : Nat . (coppeliusFP16TransposeTiledProgram 64 groups rows columns)))) -- The block a tile needs: a thread per packed word of the tile's row pair -- (two columns), so tileColumns / 2 threads. A wider block's extra threads -- address words past the tile -- the next row's -- and store past the -- group's output, over the next group's (the 64-column tile run with the -- 128-column tile's 64 threads raced the next head's blocks). def coppeliusFP16TransposeBlockThreads = (lambda unrestricted tileColumns : Nat . (naturalDivideUnchecked tileColumns 2)) def coppeliusFP16Transpose1024x512Program : (family SM86Program) = (coppeliusFP16TransposeProgram 1 1024 512) def coppeliusFP16Transpose512x512Program : (family SM86Program) = (coppeliusFP16TransposeProgram 1 512 512)