Large source region · 2,401 lines
module Accelerator.SM86.InstructionEncoding
import Accelerator.SM86.FieldEncoding
import Accelerator.SM86.Immediate
import Accelerator.SM86.Instruction
import Accelerator.SM86.NumericSemantics
import Accelerator.SM86.Types
import Std.Byte
import Std.Natural
import Accelerator.SM86.Control
family SM86InstructionEncodingResult : Type 0
constructor SM86InstructionEncodingSucceeded
field unrestricted sm86InstructionEncodedBytes : Bytes
field unrestricted sm86InstructionEncodingTelemetry : (family SM86FieldEncodingTelemetry)
constructor SM86InstructionEncodingFieldFailed
field unrestricted sm86InstructionFieldError : (family SM86EncodingErrorCode)
field unrestricted sm86InstructionFieldPosition : Nat
field unrestricted sm86InstructionFieldWidth : Nat
field unrestricted sm86InstructionFieldDetail : Nat
field unrestricted sm86InstructionFieldTelemetry : (family SM86FieldEncodingTelemetry)
constructor SM86InstructionEncodingUnsupported
field unrestricted sm86UnsupportedInstructionOrdinal : Nat
end-family
family SM86ProgramEncodingTelemetry : Type 0
constructor SM86ProgramEncodingTelemetryValue
field unrestricted sm86ProgramTelemetryInstructions : Nat
field unrestricted sm86ProgramTelemetryBytes : Nat
field unrestricted sm86ProgramTelemetryFields : Nat
field unrestricted sm86ProgramTelemetryBits : Nat
field unrestricted sm86ProgramTelemetryHighestExclusiveBit : Nat
end-family
family SM86ProgramEncodingResult : Type 0
constructor SM86ProgramEncodingSucceeded
field unrestricted sm86ProgramEncodedBytes : Bytes
field unrestricted sm86ProgramEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
constructor SM86ProgramEncodingFailed
field unrestricted sm86ProgramFailureInstructionIndex : Nat
field unrestricted sm86ProgramFailure : (family SM86InstructionEncodingResult)
field unrestricted sm86ProgramFailureTelemetry : (family SM86ProgramEncodingTelemetry)
end-family
-- One Ampere instruction contains 128 bits, including its control fields.
def sm86InstructionBytes : Nat = 16
def sm86InstructionNaturalOne =
(succ zero)
def sm86InstructionNaturalTwo =
(byte-to-nat (byte 2))
def sm86InstructionNaturalThree =
(byte-to-nat (byte 3))
def sm86InstructionNaturalFive =
(byte-to-nat (byte 5))
def sm86InstructionNaturalEight =
(byte-to-nat (byte 8))
def sm86InstructionNaturalSixteen =
(byte-to-nat (byte 16))
def sm86InstructionNaturalTwentyFour =
(byte-to-nat (byte 24))
def sm86InstructionNaturalThirtyTwo =
(byte-to-nat (byte 32))
def sm86InstructionNaturalThirtyEight =
(byte-to-nat (byte 38))
def sm86InstructionNaturalForty =
(byte-to-nat (byte 40))
def sm86InstructionNaturalFiftyFour =
(byte-to-nat (byte 54))
def sm86InstructionNaturalFiftyThree =
(byte-to-nat (byte 53))
def sm86InstructionNaturalFiftyEight =
(byte-to-nat (byte 58))
def sm86InstructionNaturalSixty =
(byte-to-nat (byte 60))
def sm86InstructionNaturalSixtyOne =
(byte-to-nat (byte 61))
def sm86InstructionNaturalSixtyThree =
(byte-to-nat (byte 63))
def sm86InstructionNaturalSixtyFour =
(byte-to-nat (byte 64))
def sm86InstructionNaturalSeventyTwo =
(byte-to-nat (byte 72))
def sm86InstructionNaturalSeventyEight =
(byte-to-nat (byte 78))
def sm86InstructionNaturalEighty =
(byte-to-nat (byte 80))
def sm86InstructionNaturalEightyOne =
(byte-to-nat (byte 81))
def sm86InstructionNaturalEightyFour =
(byte-to-nat (byte 84))
def sm86InstructionNaturalThirteen =
(byte-to-nat (byte 13))
def sm86Opcode =
(lambda unrestricted high : Byte .
(lambda unrestricted low : Byte .
(naturalAdd
(naturalMultiply (byte-to-nat high) byteNaturalTwoHundredFiftySix)
(byte-to-nat low))))
def sm86OpcodeMoveConstant =
(sm86Opcode (byte 10) (byte 2))
def sm86OpcodeMoveImmediate =
(sm86Opcode (byte 8) (byte 2))
def sm86OpcodeSpecialToRegister =
(sm86Opcode (byte 9) (byte 25))
def sm86OpcodeIntegerMultiplyAddImmediate =
(sm86Opcode (byte 8) (byte 36))
def sm86OpcodeIntegerMultiplyAddConstant =
(sm86Opcode (byte 10) (byte 36))
def sm86OpcodeIntegerMultiplyAddWideConstant =
(sm86Opcode (byte 6) (byte 37))
def sm86OpcodeIntegerAddThreeImmediate =
(sm86Opcode (byte 8) (byte 16))
def sm86OpcodeIntegerAddThreeRegister =
(sm86Opcode (byte 2) (byte 16))
def sm86OpcodeShiftRightImmediate =
(sm86Opcode (byte 8) (byte 25))
def sm86OpcodeLogicThreeInputTruthTable =
(sm86Opcode (byte 2) (byte 18))
def sm86OpcodeIntegerToFloat =
(sm86Opcode (byte 2) (byte 69))
def sm86OpcodeFloatPairToPackedHalfPair =
(sm86Opcode (byte 2) (byte 62))
def sm86OpcodeHalfToFloat =
(sm86Opcode (byte 2) (byte 48))
def sm86OpcodeTensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 =
(sm86Opcode (byte 2) (byte 60))
-- PRMT with an immediate selector (the bfloat16 widening)
def sm86OpcodePermuteImmediate =
(sm86Opcode (byte 8) (byte 22))
def sm86OpcodeFloatMinimumOrMaximum =
(sm86Opcode (byte 2) (byte 9))
def sm86OpcodeFloatAdd =
(sm86Opcode (byte 2) (byte 33))
def sm86OpcodeFloatMultiply =
(sm86Opcode (byte 2) (byte 32))
def sm86OpcodeFloatFusedMultiplyAdd =
(sm86Opcode (byte 2) (byte 35))
def sm86OpcodeMultiFunctionUnitApproximation =
(sm86Opcode (byte 3) (byte 8))
def sm86OpcodeFloatNegate =
(sm86Opcode (byte 2) (byte 33))
def sm86OpcodeLoadGlobal =
(sm86Opcode (byte 9) (byte 129))
def sm86OpcodeWarpShuffle =
(sm86Opcode (byte 15) (byte 137))
def sm86OpcodeLoadShared =
(sm86Opcode (byte 9) (byte 132))
def sm86OpcodeLoadSharedMatrix =
(sm86Opcode (byte 8) (byte 59))
def sm86OpcodeStoreShared =
(sm86Opcode (byte 3) (byte 136))
def sm86OpcodeBarrierSynchronize =
(sm86Opcode (byte 11) (byte 29))
def sm86OpcodeLoadGlobalToShared =
(sm86Opcode (byte 15) (byte 174))
def sm86OpcodeCommitAsyncGroup =
(sm86Opcode (byte 9) (byte 175))
def sm86OpcodeWaitAsyncGroups =
(sm86Opcode (byte 9) (byte 26))
def sm86OpcodeStoreGlobal =
(sm86Opcode (byte 9) (byte 134))
def sm86OpcodeReduceGlobalAddFloat32 =
(sm86Opcode (byte 9) (byte 142))
def sm86OpcodePredicateGreaterThanImmediate =
(sm86Opcode (byte 8) (byte 12))
def sm86OpcodeExit =
(sm86Opcode (byte 9) (byte 77))
def sm86OpcodeBranch =
(sm86Opcode (byte 9) (byte 71))
def sm86RegisterNatural =
(lambda unrestricted register : (family SM86Register) .
(eliminate
SM86Register
(lambda unrestricted current : (family SM86Register) . Nat)
register
(branch SM86RegisterValue value . (byte-to-nat value))))
def sm86Unsigned32Natural =
(lambda unrestricted value : (family SM86Unsigned32) .
(eliminate
SM86Unsigned32
(lambda unrestricted current : (family SM86Unsigned32) . Nat)
value
(branch
SM86Unsigned32Value
byte0
byte1
byte2
byte3
.
(naturalAdd
(byte-to-nat byte0)
(naturalMultiply
byteNaturalTwoHundredFiftySix
(naturalAdd
(byte-to-nat byte1)
(naturalMultiply
byteNaturalTwoHundredFiftySix
(naturalAdd
(byte-to-nat byte2)
(naturalMultiply byteNaturalTwoHundredFiftySix (byte-to-nat byte3))))))))))
def sm86Unsigned32BytesNatural =
(lambda unrestricted byte0 : Byte .
(lambda unrestricted byte1 : Byte .
(lambda unrestricted byte2 : Byte .
(lambda unrestricted byte3 : Byte .
(sm86Unsigned32Natural
(constructor SM86Unsigned32 SM86Unsigned32Value byte0 byte1 byte2 byte3))))))
def sm86InstructionField =
(lambda unrestricted position : Nat .
(lambda unrestricted width : Nat .
(lambda unrestricted value : Nat .
(constructor SM86EncodedField SM86EncodedFieldValue position width value))))
def sm86InstructionFieldsEmpty =
(constructor SM86EncodedFieldList SM86EncodedFieldListEmpty)
def sm86InstructionFieldsCons =
(lambda unrestricted field : (family SM86EncodedField) .
(lambda unrestricted tail : (family SM86EncodedFieldList) .
(constructor SM86EncodedFieldList SM86EncodedFieldListCons field tail)))
def sm86InstructionOneField =
(lambda unrestricted position : Nat .
(lambda unrestricted width : Nat .
(lambda unrestricted value : Nat .
(sm86InstructionFieldsCons
(sm86InstructionField position width value)
sm86InstructionFieldsEmpty))))
def sm86InstructionPrependField =
(lambda unrestricted position : Nat .
(lambda unrestricted width : Nat .
(lambda unrestricted value : Nat .
(lambda unrestricted tail : (family SM86EncodedFieldList) .
(sm86InstructionFieldsCons (sm86InstructionField position width value) tail)))))
-- Fixed32 operands retain their four-byte representation through field packing.
def sm86InstructionWord32Field =
(lambda unrestricted position : Nat .
(lambda unrestricted value : (family SM86Unsigned32) .
(constructor SM86EncodedField SM86EncodedFieldWord32Value position value)))
def sm86InstructionOneWord32Field =
(lambda unrestricted position : Nat .
(lambda unrestricted value : (family SM86Unsigned32) .
(sm86InstructionFieldsCons
(sm86InstructionWord32Field position value)
sm86InstructionFieldsEmpty)))
def sm86InstructionPrependWord32Field =
(lambda unrestricted position : Nat .
(lambda unrestricted value : (family SM86Unsigned32) .
(lambda unrestricted tail : (family SM86EncodedFieldList) .
(sm86InstructionFieldsCons (sm86InstructionWord32Field position value) tail))))
def sm86InstructionWord24Field =
(lambda unrestricted position : Nat .
(lambda unrestricted byte0 : Byte .
(lambda unrestricted byte1 : Byte .
(lambda unrestricted byte2 : Byte .
(constructor SM86EncodedField SM86EncodedFieldWord24Value position byte0 byte1 byte2)))))
def sm86InstructionOneWord24Field =
(lambda unrestricted position : Nat .
(lambda unrestricted byte0 : Byte .
(lambda unrestricted byte1 : Byte .
(lambda unrestricted byte2 : Byte .
(sm86InstructionFieldsCons
(sm86InstructionWord24Field position byte0 byte1 byte2)
sm86InstructionFieldsEmpty)))))
def sm86InstructionPrependWord24Field =
(lambda unrestricted position : Nat .
(lambda unrestricted byte0 : Byte .
(lambda unrestricted byte1 : Byte .
(lambda unrestricted byte2 : Byte .
(lambda unrestricted tail : (family SM86EncodedFieldList) .
(sm86InstructionFieldsCons (sm86InstructionWord24Field position byte0 byte1 byte2) tail))))))
def sm86InstructionUnsupported =
(lambda unrestricted ordinal : Nat .
(constructor SM86InstructionEncodingResult SM86InstructionEncodingUnsupported ordinal))
def sm86InstructionFieldFailure =
(lambda unrestricted error : (family SM86EncodingErrorCode) .
(lambda unrestricted position : Nat .
(lambda unrestricted width : Nat .
(lambda unrestricted detail : Nat .
(lambda unrestricted telemetry : (family SM86FieldEncodingTelemetry) .
(constructor
SM86InstructionEncodingResult
SM86InstructionEncodingFieldFailed
error
position
width
detail
telemetry))))))
def sm86InstructionContinueFields =
(lambda unrestricted operands : (family SM86EncodedFieldList) .
(lambda unrestricted header : (family SM86FieldEncodingResult) .
(eliminate
SM86FieldEncodingResult
(lambda unrestricted current : (family SM86FieldEncodingResult) .
(family SM86InstructionEncodingResult))
header
(branch
SM86FieldEncodingSucceeded
headerBytes
headerTelemetry
.
(eliminate
SM86FieldEncodingResult
(lambda unrestricted current : (family SM86FieldEncodingResult) .
(family SM86InstructionEncodingResult))
(sm86EncodeFieldListFrom operands headerBytes)
(branch
SM86FieldEncodingSucceeded
complete
operandTelemetry
.
(constructor
SM86InstructionEncodingResult
SM86InstructionEncodingSucceeded
complete
(sm86MergeFieldTelemetry headerTelemetry operandTelemetry)))
(branch
SM86FieldEncodingFailed
error
position
width
detail
telemetry
.
(sm86InstructionFieldFailure
error
position
width
detail
(sm86MergeFieldTelemetry headerTelemetry telemetry)))))
(branch
SM86FieldEncodingFailed
error
position
width
detail
telemetry
.
(sm86InstructionFieldFailure error position width detail telemetry)))))
def sm86EncodeInstructionFields =
(lambda unrestricted opcode : Nat .
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted control : (family SM86Control) .
(lambda unrestricted operands : (family SM86EncodedFieldList) .
(sm86InstructionContinueFields
operands
(sm86EncodeInstructionHeader opcode guard control))))))
def sm86SpecialRegisterNatural =
(lambda unrestricted special : (family SM86SpecialRegister) .
(eliminate
SM86SpecialRegister
(lambda unrestricted current : (family SM86SpecialRegister) . Nat)
special
(branch SM86CooperativeThreadArrayIdX . (byte-to-nat (byte 37)))
(branch SM86CooperativeThreadArrayIdY . (byte-to-nat (byte 38)))
(branch SM86CooperativeThreadArrayIdZ . (byte-to-nat (byte 39)))
(branch SM86ThreadIdX . (byte-to-nat (byte 33)))
(branch SM86ClockLow . (byte-to-nat (byte 80)))
(branch SM86GlobalTimerLow . (byte-to-nat (byte 82)))
(branch SM86GlobalTimerHigh . (byte-to-nat (byte 83)))))
def sm86ShuffleModeNatural =
(lambda unrestricted mode : (family SM86ShuffleMode) .
(eliminate
SM86ShuffleMode
(lambda unrestricted current : (family SM86ShuffleMode) . Nat)
mode
(branch SM86ShuffleIndex . zero)
(branch SM86ShuffleUp . (succ zero))
(branch SM86ShuffleDown . (byte-to-nat (byte 2)))
(branch SM86ShuffleButterfly . (byte-to-nat (byte 3)))))
def sm86EncodeMoveConstant =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted bank : Byte .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeMoveConstant
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyEight
sm86InstructionNaturalSixteen
(sm86Unsigned32Natural offset)
(sm86InstructionPrependField
sm86InstructionNaturalFiftyFour
sm86InstructionNaturalFive
(byte-to-nat bank)
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
zero
(sm86InstructionOneField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 15)))))))))))))
def sm86EncodeMoveImmediate =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted immediate : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeMoveImmediate
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependWord32Field
sm86InstructionNaturalThirtyTwo
immediate
(sm86InstructionOneField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 15))))))))))
def sm86EncodeSpecialToRegister =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted special : (family SM86SpecialRegister) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeSpecialToRegister
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionOneField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(sm86SpecialRegisterNatural special))))))))
def sm86EncodeIntegerMultiplyAddImmediate =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted immediate : (family SM86Unsigned32) .
(lambda unrestricted addend : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeIntegerMultiplyAddImmediate
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependWord32Field
sm86InstructionNaturalThirtyTwo
immediate
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(sm86RegisterNatural addend)
(sm86InstructionOneWord24Field
sm86InstructionNaturalSeventyTwo
(byte 2)
(byte 142)
(byte 7)))))))))))))
def sm86EncodeIntegerMultiplyAddConstant =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted bank : Byte .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted addend : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeIntegerMultiplyAddConstant
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyEight
sm86InstructionNaturalSixteen
(sm86Unsigned32Natural offset)
(sm86InstructionPrependField
sm86InstructionNaturalFiftyFour
sm86InstructionNaturalFive
(byte-to-nat bank)
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(sm86RegisterNatural addend)
(sm86InstructionOneWord24Field
sm86InstructionNaturalSeventyTwo
(byte 2)
(byte 142)
(byte 7)))))))))))))))
def sm86EncodeIntegerMultiplyAddWideConstant =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted right : (family SM86Register) .
(lambda unrestricted bank : Byte .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(nat-eliminate
(lambda unrestricted destinationIsZero : Nat .
(family SM86InstructionEncodingResult))
(sm86EncodeInstructionFields
sm86OpcodeIntegerMultiplyAddWideConstant
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyEight
sm86InstructionNaturalSixteen
(sm86Unsigned32Natural offset)
(sm86InstructionPrependField
sm86InstructionNaturalFiftyFour
sm86InstructionNaturalFive
(byte-to-nat bank)
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(sm86RegisterNatural right)
(sm86InstructionOneWord24Field
sm86InstructionNaturalSeventyTwo
(byte 0)
(byte 142)
(byte 7))))))))
(lambda unrestricted invalidPredecessor : Nat .
(lambda unrestricted invalidInduction : (family SM86InstructionEncodingResult) .
(sm86InstructionUnsupported (byte-to-nat (byte 6)))))
(byte-equal (nat-to-byte (sm86RegisterNatural destination)) (byte 255))))))))))
def sm86EncodeIntegerAdd3Immediate =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted immediate : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeIntegerAddThreeImmediate
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependWord32Field
sm86InstructionNaturalThirtyTwo
immediate
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(byte-to-nat (byte 255))
(sm86InstructionPrependField
sm86InstructionNaturalEightyOne
sm86InstructionNaturalThree
(byte-to-nat (byte 7))
(sm86InstructionOneField
sm86InstructionNaturalEightyFour
sm86InstructionNaturalThree
(byte-to-nat (byte 7))))))))))))))
def sm86EncodeIntegerAdd3Register =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted right : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeIntegerAddThreeRegister
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural right)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 255)
(byte 224)
(byte 255)
(byte 7))))))))))))
def sm86EncodeShiftRightImmediate =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted amount : Byte .
(lambda unrestricted control : (family SM86Control) .
(nat-eliminate
(lambda unrestricted amountInvalid : Nat . (family SM86InstructionEncodingResult))
(sm86EncodeInstructionFields
sm86OpcodeShiftRightImmediate
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(byte-to-nat (byte 255))
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalThirtyTwo
(byte-to-nat amount)
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionOneWord24Field
sm86InstructionNaturalSeventyTwo
(byte 22)
(byte 1)
(byte 0)))))))
(lambda unrestricted invalidPredecessor : Nat .
(lambda unrestricted invalidInduction : (family SM86InstructionEncodingResult) .
(sm86InstructionUnsupported (byte-to-nat (byte 9)))))
(nat-less-than (byte-to-nat (byte 31)) (byte-to-nat amount))))))))
def sm86EncodeLogic3 =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted right : (family SM86Register) .
(lambda unrestricted truthTable : Byte .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeLogicThreeInputTruthTable
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural right)
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(byte-to-nat (byte 255))
(sm86InstructionPrependField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat truthTable)
(sm86InstructionOneField
sm86InstructionNaturalEighty
sm86InstructionNaturalSixteen
(sm86Unsigned32BytesNatural (byte 142) (byte 7) (byte 0) (byte 0)))))))))))))))
def sm86EncodeFloatMultiply =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted right : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeFloatMultiply
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural right)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 0)
(byte 0)
(byte 64)
(byte 0))))))))))))
def sm86EncodeIntegerToFloat =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeIntegerToFloat
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionPrependField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 20))
(sm86InstructionOneField
sm86InstructionNaturalEighty
sm86InstructionNaturalEight
(byte-to-nat (byte 32)))))))))))
def sm86HalfSelectorNatural =
(lambda unrestricted selector : (family SM86HalfSelector) .
(eliminate
SM86HalfSelector
(lambda unrestricted current : (family SM86HalfSelector) . Nat)
selector
(branch SM86LowHalf . zero)
(branch SM86HighHalf . sm86InstructionNaturalOne)))
def sm86EncodeFloat32PairToHalf2 =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted sourceHigh : (family SM86Register) .
(lambda unrestricted sourceLow : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeFloatPairToPackedHalfPair
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural sourceHigh)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural sourceLow)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 255)
(byte 0)
(byte 0)
(byte 0))))))))))))
def sm86EncodeHalfToFloat =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted selector : (family SM86HalfSelector) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeHalfToFloat
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(byte-to-nat (byte 255))
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionPrependField
sm86InstructionNaturalSixty
sm86InstructionNaturalOne
(sm86HalfSelectorNatural selector)
(sm86InstructionPrependField
sm86InstructionNaturalSixtyOne
sm86InstructionNaturalOne
sm86InstructionNaturalOne
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 0)
(byte 65)
(byte 0)
(byte 0))))))))))))))
-- F2FP.BF16.PACK_AB: F2FP.PACK_AB with bit 76 set (the bfloat16 result;
-- ptxas's encoding for sm_86 and sm_121, 2026-09-25)
def sm86EncodeFloat32PairToBFloat16Pair =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted sourceHigh : (family SM86Register) .
(lambda unrestricted sourceLow : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeFloatPairToPackedHalfPair
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural sourceHigh)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural sourceLow)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 255)
(byte 16)
(byte 0)
(byte 0))))))))))))
-- PRMT Rd, Ra, selector, RZ: the result's bytes, high to low, are Ra's
-- bytes 1, 0 (H0) or 3, 2 (H1) then two of RZ's
def sm86BFloat16WidenSelector =
(lambda unrestricted selector : (family SM86HalfSelector) .
(eliminate
SM86HalfSelector
(lambda unrestricted current : (family SM86HalfSelector) . (family SM86Unsigned32))
selector
(branch SM86LowHalf . (constructor SM86Unsigned32 SM86Unsigned32Value (byte 68) (byte 16) (byte 0) (byte 0)))
(branch SM86HighHalf . (constructor SM86Unsigned32 SM86Unsigned32Value (byte 68) (byte 50) (byte 0) (byte 0)))))
def sm86EncodeBFloat16ToFloat =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted selector : (family SM86HalfSelector) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodePermuteImmediate
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionPrependWord32Field
sm86InstructionNaturalThirtyTwo
(sm86BFloat16WidenSelector selector)
(sm86InstructionOneField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(byte-to-nat (byte 255))))))))))))
-- HMMA.16816.F32.BF16: the binary16 tile product's encoding with bit 82 set
def sm86EncodeHMMA16816F32BF16 =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted fragmentA : (family SM86Register) .
(lambda unrestricted fragmentB : (family SM86Register) .
(lambda unrestricted accumulator : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeTensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural fragmentA)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural fragmentB)
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(sm86RegisterNatural accumulator)
(sm86InstructionPrependField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 24))
(sm86InstructionOneField
sm86InstructionNaturalEighty
sm86InstructionNaturalEight
(byte-to-nat (byte 4)))))))))))))))
def sm86EncodeHMMA16816F32F16 =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted fragmentA : (family SM86Register) .
(lambda unrestricted fragmentB : (family SM86Register) .
(lambda unrestricted accumulator : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeTensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural fragmentA)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural fragmentB)
(sm86InstructionPrependField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(sm86RegisterNatural accumulator)
(sm86InstructionOneField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 24))))))))))))))
def sm86EncodeFloatAdd =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted right : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeFloatAdd
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionOneField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural right))))))))))
def sm86EncodeFloatFusedMultiplyAdd =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted right : (family SM86Register) .
(lambda unrestricted addend : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeFloatFusedMultiplyAdd
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural right)
(sm86InstructionOneField
sm86InstructionNaturalSixtyFour
sm86InstructionNaturalEight
(sm86RegisterNatural addend))))))))))))
def sm86EncodeMultiFunction =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted operation : (family SM86MultiFunction) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeMultiFunctionUnitApproximation
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionOneField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat (sm86MultiFunctionSelector operation)))))))))))
def sm86FloatExtremumDescriptorNatural =
(lambda unrestricted extremum : (family SM86FloatExtremum) .
(eliminate
SM86FloatExtremum
(lambda unrestricted current : (family SM86FloatExtremum) . Nat)
extremum
(branch SM86FloatMinimum . (sm86Unsigned32BytesNatural (byte 0) (byte 0) (byte 128) (byte 3)))
(branch SM86FloatMaximum . (sm86Unsigned32BytesNatural (byte 0) (byte 0) (byte 128) (byte 7)))))
-- Keep the public Natural descriptor; encoding consumes its bounded sibling.
def sm86FloatExtremumDescriptorWord32 =
(lambda unrestricted extremum : (family SM86FloatExtremum) .
(eliminate
SM86FloatExtremum
(lambda unrestricted current : (family SM86FloatExtremum) . (family SM86Unsigned32))
extremum
(branch
SM86FloatMinimum
.
(constructor SM86Unsigned32 SM86Unsigned32Value (byte 0) (byte 0) (byte 128) (byte 3)))
(branch
SM86FloatMaximum
.
(constructor SM86Unsigned32 SM86Unsigned32Value (byte 0) (byte 0) (byte 128) (byte 7)))))
def sm86EncodeFloatExtremum =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted left : (family SM86Register) .
(lambda unrestricted right : (family SM86Register) .
(lambda unrestricted extremum : (family SM86FloatExtremum) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeFloatMinimumOrMaximum
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural left)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural right)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(sm86FloatExtremumDescriptorWord32 extremum))))))))))))
def sm86EncodeFloatNegate =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeFloatNegate
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 255))
(sm86InstructionPrependField
sm86InstructionNaturalSixtyThree
sm86InstructionNaturalOne
sm86InstructionNaturalOne
(sm86InstructionOneField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalOne
sm86InstructionNaturalOne))))))))))
def sm86EncodeLoadGlobal =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeLoadGlobal
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 4))
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 0)
(byte 25)
(byte 30)
(byte 12)))))))))))))
def sm86EncodeLoadGlobalWide =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeLoadGlobal
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 4))
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 0)
(byte 29)
(byte 30)
(byte 12)))))))))))))
def sm86EncodeShuffle =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted lane : Byte .
(lambda unrestricted segment : (family SM86Unsigned32) .
(lambda unrestricted mode : (family SM86ShuffleMode) .
(lambda unrestricted control : (family SM86Control) .
(nat-eliminate
(lambda unrestricted laneInvalid : Nat . (family SM86InstructionEncodingResult))
(sm86EncodeInstructionFields
sm86OpcodeWarpShuffle
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalThirteen
(sm86Unsigned32Natural segment)
(sm86InstructionPrependField
sm86InstructionNaturalFiftyThree
sm86InstructionNaturalFive
(byte-to-nat lane)
(sm86InstructionPrependField
sm86InstructionNaturalFiftyEight
sm86InstructionNaturalTwo
(sm86ShuffleModeNatural mode)
(sm86InstructionOneField
sm86InstructionNaturalEightyOne
sm86InstructionNaturalThree
(byte-to-nat (byte 7)))))))))
(lambda unrestricted invalidPredecessor : Nat .
(lambda unrestricted invalidInduction : (family SM86InstructionEncodingResult) .
(sm86InstructionUnsupported (byte-to-nat (byte 20)))))
(nat-less-than (byte-to-nat (byte 31)) (byte-to-nat lane))))))))))
def sm86EncodeLoadShared =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeLoadShared
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionOneField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 72))))))))))))
def sm86SharedMatrixCountNatural =
(lambda unrestricted count : (family SM86SharedMatrixCount) .
(eliminate
SM86SharedMatrixCount
(lambda unrestricted current : (family SM86SharedMatrixCount) . Nat)
count
(branch SM86SharedMatrix1 . zero)
(branch SM86SharedMatrix2 . sm86InstructionNaturalOne)
(branch SM86SharedMatrix4 . sm86InstructionNaturalTwo)))
def sm86SharedMatrixTransposeNatural =
(lambda unrestricted transpose : (family SM86SharedMatrixTranspose) .
(eliminate
SM86SharedMatrixTranspose
(lambda unrestricted current : (family SM86SharedMatrixTranspose) . Nat)
transpose
(branch SM86SharedMatrixNotTransposed . zero)
(branch SM86SharedMatrixTransposed . sm86InstructionNaturalOne)))
def sm86EncodeLoadSharedMatrix =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted destination : (family SM86Register) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted count : (family SM86SharedMatrixCount) .
(lambda unrestricted transpose : (family SM86SharedMatrixTranspose) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeLoadSharedMatrix
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalSixteen
sm86InstructionNaturalEight
(sm86RegisterNatural destination)
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionPrependField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalTwo
(sm86SharedMatrixCountNatural count)
(sm86InstructionOneField
sm86InstructionNaturalSeventyEight
sm86InstructionNaturalOne
(sm86SharedMatrixTransposeNatural transpose))))))))))))))
def sm86EncodeStoreShared =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted value : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeStoreShared
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural value)
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionOneField
sm86InstructionNaturalSeventyTwo
sm86InstructionNaturalEight
(byte-to-nat (byte 72))))))))))))
-- LDGSTS.E.BYPASS.128 [address + offset], [source.64 + sourceOffset], as
-- ptxas encodes cp.async.cg ... 16 for sm_86 (nvdisasm -hex on the DGX
-- Spark, 2026-09-26; research p4-hmma/cp_async*.cu): the shared address
-- register at 16, the global pair at 24, the global offset at 32 (signed 12
-- bits in the silicon; this encoder admits 0..0x7ff, bit 43 clear), the
-- shared offset at 44 (20 bits), and bits 64..95 0x0b901c44: BYPASS (bit 81
-- clear), the global-memory descriptor UR4 with its enable (0x44) -- the
-- descriptor LDG's bits 32..39 name too. The compiler's native encoder
-- (RuntimeMachine) is its twin.
def sm86EncodeLoadGlobalToShared =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted sourceOffset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeLoadGlobalToShared
guard
control
(sm86InstructionPrependField sm86InstructionNaturalSixteen sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField sm86InstructionNaturalTwentyFour sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionPrependField sm86InstructionNaturalThirtyTwo (byte-to-nat (byte 11))
(sm86Unsigned32Natural sourceOffset)
(sm86InstructionPrependField (byte-to-nat (byte 44)) (byte-to-nat (byte 20))
(sm86Unsigned32Natural offset)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor SM86Unsigned32 SM86Unsigned32Value (byte 68) (byte 28) (byte 144) (byte 11))))))))))))))
-- LDGDEPBAR: no operand; its control's write barrier (SB0) counts the group.
def sm86EncodeCommitAsyncGroup =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields sm86OpcodeCommitAsyncGroup guard control sm86InstructionFieldsEmpty)))
-- DEPBAR.LE SB0, count: the count at 38 (6 bits), the scoreboard at 44 (SB0),
-- bit 47 the LE form (ptxas's cp.async.wait_group, as above).
def sm86EncodeWaitAsyncGroups =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted count : Byte .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeWaitAsyncGroups
guard
control
(sm86InstructionPrependField sm86InstructionNaturalThirtyEight (byte-to-nat (byte 6)) (byte-to-nat count)
(sm86InstructionPrependField (byte-to-nat (byte 47)) sm86InstructionNaturalOne 1
sm86InstructionFieldsEmpty))))))
-- BAR.SYNC.DEFER_BLOCKING 0x0: bit 80 set, as ptxas encodes bar.sync for
-- sm_86 and sm_121 (read off nvdisasm -hex on the DGX Spark, 2026-09-26:
-- high word 0x...0001_0000); without it nvdisasm reads plain BAR.SYNC. The
-- compiler's native encoder (RuntimeMachine) is its twin.
def sm86EncodeBarrierSynchronize =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeBarrierSynchronize
guard
control
(sm86InstructionPrependField sm86InstructionNaturalEighty sm86InstructionNaturalOne 1
sm86InstructionFieldsEmpty))))
def sm86EncodeStoreGlobal =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted value : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeStoreGlobal
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural value)
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 4)
(byte 25)
(byte 16)
(byte 12))))))))))))
def sm86EncodeStoreGlobalWide =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted value : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeStoreGlobal
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural value)
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 4)
(byte 29)
(byte 16)
(byte 12))))))))))))
-- STG.E.64: the register pair [value, value+1] to [address + offset]. The
-- descriptor word differs from the 32-bit store only in the size code (byte
-- 25 -> 27; the 128-bit store is 29), the same three codes the wide-memory
-- descriptors carry. An mma.m16n8k16 fp32 accumulator fragment hands each
-- thread PAIRS of adjacent columns, so a row-major epilogue needs exactly this
-- width: a 128-bit store there overlaps the neighbouring thread and lands on an
-- 8-byte-aligned address, which the SM faults instead of executing.
def sm86EncodeStoreGlobal64 =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted value : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeStoreGlobal
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural value)
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 4)
(byte 27)
(byte 16)
(byte 12))))))))))))
def sm86EncodeReduceGlobalAddFloat32 =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted address : (family SM86Register) .
(lambda unrestricted value : (family SM86Register) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeReduceGlobalAddFloat32
guard
control
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural address)
(sm86InstructionPrependField
sm86InstructionNaturalThirtyTwo
sm86InstructionNaturalEight
(sm86RegisterNatural value)
(sm86InstructionPrependField
sm86InstructionNaturalForty
sm86InstructionNaturalTwentyFour
(sm86Unsigned32Natural offset)
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 132)
(byte 231)
(byte 16)
(byte 12))))))))))))
def sm86EncodePredicateGreater =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted predicate : (family SM86Predicate) .
(lambda unrestricted source : (family SM86Register) .
(lambda unrestricted immediate : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(app
(lambda unrestricted predicateControl : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodePredicateGreaterThanImmediate
guard
predicateControl
(sm86InstructionPrependField
sm86InstructionNaturalTwentyFour
sm86InstructionNaturalEight
(sm86RegisterNatural source)
(sm86InstructionPrependWord32Field
sm86InstructionNaturalThirtyTwo
immediate
(sm86InstructionPrependWord32Field
sm86InstructionNaturalSixtyFour
(constructor
SM86Unsigned32
SM86Unsigned32Value
(byte 112)
(byte 64)
(byte 240)
(byte 3))
(sm86InstructionOneField
sm86InstructionNaturalEightyOne
sm86InstructionNaturalThree
(byte-to-nat (sm86PredicateNumber predicate))))))))
(eliminate
SM86Control
(lambda unrestricted current : (family SM86Control) . (family SM86Control))
control
(branch
SM86ControlValue
stall
yieldMode
writeBarrier
readBarrier
waitMask
reuseMask
.
(constructor
SM86Control
SM86ControlValue
(byte 15)
yieldMode
writeBarrier
readBarrier
waitMask
reuseMask)))))))))
def sm86EncodeExit =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeExit
guard
control
(sm86InstructionOneWord32Field
sm86InstructionNaturalSixtyFour
(constructor SM86Unsigned32 SM86Unsigned32Value (byte 0) (byte 0) (byte 128) (byte 3))))))
-- BRA (relative branch, opcode 0x947): the loop back-edge. Field layout mirrors the golden
-- reference (offset@32(32) = relative BYTE offset from PC+16, descriptor@64(32) = 0x03800000 for a
-- forward branch, 0x0383ffff for a backward branch). The guard predicate (@12) and negate bit (@15)
-- and the control word (@105) are laid down by the shared instruction header, so `@!P0 BRA` reuses the
-- SAME predicate machinery as every predicated instruction. This is a real field-packing encoder (a
-- COMPONENT), never a golden-byte substitute; nvdisasm-verified on the SM86 profile.
def sm86EncodeBranch =
(lambda unrestricted guard : (family SM86InstructionGuard) .
(lambda unrestricted offset : (family SM86Unsigned32) .
(lambda unrestricted descriptor : (family SM86Unsigned32) .
(lambda unrestricted control : (family SM86Control) .
(sm86EncodeInstructionFields
sm86OpcodeBranch
guard
control
(sm86InstructionPrependWord32Field
sm86InstructionNaturalThirtyTwo
offset
(sm86InstructionOneWord32Field sm86InstructionNaturalSixtyFour descriptor)))))))
def sm86EncodeInstruction =
(lambda unrestricted instruction : (family SM86Instruction) .
(eliminate
SM86Instruction
(lambda unrestricted current : (family SM86Instruction) .
(family SM86InstructionEncodingResult))
instruction
(branch
SM86InstructionValue
guard
body
.
(eliminate
SM86InstructionBody
(lambda unrestricted current : (family SM86InstructionBody) .
(family SM86InstructionEncodingResult))
body
(branch
SM86MoveConstant
destination
bank
offset
control
.
(sm86EncodeMoveConstant guard destination bank offset control))
(branch
SM86SpecialToRegister
destination
special
control
.
(sm86EncodeSpecialToRegister guard destination special control))
(branch
SM86MoveImmediate
destination
immediate
control
.
(sm86EncodeMoveImmediate guard destination immediate control))
(branch
SM86IntegerMultiplyAddConstant
destination
left
bank
offset
addend
control
.
(sm86EncodeIntegerMultiplyAddConstant guard destination left bank offset addend control))
(branch
SM86IntegerMultiplyAddImmediate
destination
left
immediate
addend
control
.
(sm86EncodeIntegerMultiplyAddImmediate guard destination left immediate addend control))
(branch
SM86IntegerMultiplyAddWideConstant
destination
left
right
bank
offset
control
.
(sm86EncodeIntegerMultiplyAddWideConstant
guard
destination
left
right
bank
offset
control))
(branch
SM86IntegerAddThreeImmediate
destination
left
immediate
control
.
(sm86EncodeIntegerAdd3Immediate guard destination left immediate control))
(branch
SM86IntegerAddThreeRegister
destination
left
right
control
.
(sm86EncodeIntegerAdd3Register guard destination left right control))
(branch
SM86ShiftRightImmediate
destination
source
amount
control
.
(sm86EncodeShiftRightImmediate guard destination source amount control))
(branch
SM86LogicThreeInputTruthTable
destination
left
right
truthTable
control
.
(sm86EncodeLogic3 guard destination left right truthTable control))
(branch
SM86IntegerToFloat
destination
source
control
.
(sm86EncodeIntegerToFloat guard destination source control))
(branch
SM86FloatAdd
destination
left
right
control
.
(sm86EncodeFloatAdd guard destination left right control))
(branch
SM86FloatMultiply
destination
left
right
control
.
(sm86EncodeFloatMultiply guard destination left right control))
(branch
SM86FloatFusedMultiplyAdd
destination
left
right
addend
control
.
(sm86EncodeFloatFusedMultiplyAdd guard destination left right addend control))
(branch
SM86MultiFunctionUnitApproximation
destination
source
operation
control
.
(sm86EncodeMultiFunction guard destination source operation control))
(branch
SM86FloatMinimumOrMaximum
destination
left
right
extremum
control
.
(sm86EncodeFloatExtremum guard destination left right extremum control))
(branch
SM86FloatNegate
destination
source
control
.
(sm86EncodeFloatNegate guard destination source control))
(branch
SM86FloatPairToPackedHalfPair
destination
sourceHigh
sourceLow
control
.
(sm86EncodeFloat32PairToHalf2 guard destination sourceHigh sourceLow control))
(branch
SM86FloatPairToPackedBFloat16Pair
destination
sourceHigh
sourceLow
control
.
(sm86EncodeFloat32PairToBFloat16Pair guard destination sourceHigh sourceLow control))
(branch
SM86HalfToFloat
destination
source
selector
control
.
(sm86EncodeHalfToFloat guard destination source selector control))
(branch
SM86BFloat16ToFloat
destination
source
selector
control
.
(sm86EncodeBFloat16ToFloat guard destination source selector control))
(branch
SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32
destination
fragmentA
fragmentB
accumulator
control
.
(sm86EncodeHMMA16816F32F16 guard destination fragmentA fragmentB accumulator control))
(branch
SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32
destination
fragmentA
fragmentB
accumulator
control
.
(sm86EncodeHMMA16816F32BF16 guard destination fragmentA fragmentB accumulator control))
(branch
SM86LoadGlobal
destination
address
offset
control
.
(sm86EncodeLoadGlobal guard destination address offset control))
(branch
SM86LoadGlobalWide
destination
address
offset
control
.
(sm86EncodeLoadGlobalWide guard destination address offset control))
(branch
SM86WarpShuffle
destination
source
lane
segment
mode
control
.
(sm86EncodeShuffle guard destination source lane segment mode control))
(branch
SM86LoadShared
destination
address
offset
control
.
(sm86EncodeLoadShared guard destination address offset control))
(branch
SM86LoadSharedMatrix
destination
address
offset
count
transpose
control
.
(sm86EncodeLoadSharedMatrix guard destination address offset count transpose control))
(branch
SM86StoreShared
address
value
offset
control
.
(sm86EncodeStoreShared guard address value offset control))
(branch
SM86LoadGlobalToShared
address
offset
source
sourceOffset
control
.
(sm86EncodeLoadGlobalToShared guard address offset source sourceOffset control))
(branch SM86CommitAsyncGroup control . (sm86EncodeCommitAsyncGroup guard control))
(branch SM86WaitAsyncGroups count control . (sm86EncodeWaitAsyncGroups guard count control))
(branch SM86BarrierSynchronize control . (sm86EncodeBarrierSynchronize guard control))
(branch
SM86StoreGlobal
address
value
offset
control
.
(sm86EncodeStoreGlobal guard address value offset control))
(branch
SM86StoreGlobalWide
address
value
offset
control
.
(sm86EncodeStoreGlobalWide guard address value offset control))
(branch
SM86StoreGlobal64
address
value
offset
control
.
(sm86EncodeStoreGlobal64 guard address value offset control))
(branch
SM86ReduceGlobalAddFloat32
address
value
offset
control
.
(sm86EncodeReduceGlobalAddFloat32 guard address value offset control))
(branch
SM86PredicateGreaterThanImmediate
predicate
source
immediate
control
.
(sm86EncodePredicateGreater guard predicate source immediate control))
(branch
SM86Branch
offset
descriptor
control
.
(sm86EncodeBranch guard offset descriptor control))
(branch SM86Exit control . (sm86EncodeExit guard control))))))
def sm86ProgramTelemetryZero =
(constructor
SM86ProgramEncodingTelemetry
SM86ProgramEncodingTelemetryValue
zero
zero
zero
zero
zero)
def sm86ProgramTelemetryInstruction =
(lambda unrestricted fieldTelemetry : (family SM86FieldEncodingTelemetry) .
(eliminate
SM86FieldEncodingTelemetry
(lambda unrestricted current : (family SM86FieldEncodingTelemetry) .
(family SM86ProgramEncodingTelemetry))
fieldTelemetry
(branch
SM86FieldEncodingTelemetryValue
fields
bits
outputBytes
highest
.
(constructor
SM86ProgramEncodingTelemetry
SM86ProgramEncodingTelemetryValue
(succ zero)
outputBytes
fields
bits
highest))))
def sm86MergeProgramTelemetry =
(lambda unrestricted left : (family SM86ProgramEncodingTelemetry) .
(lambda unrestricted right : (family SM86ProgramEncodingTelemetry) .
(eliminate
SM86ProgramEncodingTelemetry
(lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
(family SM86ProgramEncodingTelemetry))
left
(branch
SM86ProgramEncodingTelemetryValue
leftInstructions
leftBytes
leftFields
leftBits
leftHighest
.
(eliminate
SM86ProgramEncodingTelemetry
(lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
(family SM86ProgramEncodingTelemetry))
right
(branch
SM86ProgramEncodingTelemetryValue
rightInstructions
rightBytes
rightFields
rightBits
rightHighest
.
(constructor
SM86ProgramEncodingTelemetry
SM86ProgramEncodingTelemetryValue
(naturalAdd leftInstructions rightInstructions)
(naturalAdd leftBytes rightBytes)
(naturalAdd leftFields rightFields)
(naturalAdd leftBits rightBits)
(sm86NaturalMaximum leftHighest rightHighest))))))))
def sm86EncodeProgramFromIndex =
(lambda unrestricted program : (family SM86Program) .
(eliminate
SM86Program
(lambda unrestricted current : (family SM86Program) .
(pi unrestricted instructionIndex : Nat . (family SM86ProgramEncodingResult)))
program
(branch
SM86ProgramEnd
.
(lambda unrestricted instructionIndex : Nat .
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingSucceeded
b""
sm86ProgramTelemetryZero)))
(branch
SM86ProgramNext
head
tail
ih_tail
.
(lambda unrestricted instructionIndex : Nat .
(eliminate
SM86InstructionEncodingResult
(lambda unrestricted current : (family SM86InstructionEncodingResult) .
(family SM86ProgramEncodingResult))
(sm86EncodeInstruction head)
(branch
SM86InstructionEncodingSucceeded
headBytes
headTelemetry
.
(eliminate
SM86ProgramEncodingResult
(lambda unrestricted current : (family SM86ProgramEncodingResult) .
(family SM86ProgramEncodingResult))
(ih_tail (succ instructionIndex))
(branch
SM86ProgramEncodingSucceeded
tailBytes
tailTelemetry
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingSucceeded
(bytes-append headBytes tailBytes)
(sm86MergeProgramTelemetry
(sm86ProgramTelemetryInstruction headTelemetry)
tailTelemetry)))
(branch
SM86ProgramEncodingFailed
failureIndex
failure
failureTelemetry
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingFailed
failureIndex
failure
(sm86MergeProgramTelemetry
(sm86ProgramTelemetryInstruction headTelemetry)
failureTelemetry)))))
(branch
SM86InstructionEncodingFieldFailed
error
position
width
detail
fieldTelemetry
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingFailed
instructionIndex
(constructor
SM86InstructionEncodingResult
SM86InstructionEncodingFieldFailed
error
position
width
detail
fieldTelemetry)
(sm86ProgramTelemetryInstruction fieldTelemetry)))
(branch
SM86InstructionEncodingUnsupported
ordinal
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingFailed
instructionIndex
(constructor
SM86InstructionEncodingResult
SM86InstructionEncodingUnsupported
ordinal)
sm86ProgramTelemetryZero)))))))
def sm86EncodeProgram =
(lambda unrestricted program : (family SM86Program) .
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingSucceeded
(compiler-native-encode (family SM86Program) program)
sm86ProgramTelemetryZero))
-- Encode structural repetition without first expanding the repeated program.
-- This is the physical-program analogue of a bytes builder: the segment is
-- validated and encoded once, while its already-checked image is retained as
-- a shared chunk until the final build. Large unrolled schedules therefore
-- remain linear in their output size instead of repeatedly normalizing the
-- same instruction terms.
def sm86RepeatedProgramBytesBuilder =
(lambda unrestricted payload : Bytes .
(lambda unrestricted count : Nat .
(nat-eliminate
(lambda unrestricted current : Nat . BytesBuilder)
(bytes-builder-empty)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : BytesBuilder .
(bytes-builder-append (bytes-builder-chunk payload) induction)))
count)))
def sm86ScaleProgramTelemetry =
(lambda unrestricted telemetry : (family SM86ProgramEncodingTelemetry) .
(lambda unrestricted count : Nat .
(eliminate
SM86ProgramEncodingTelemetry
(lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
(family SM86ProgramEncodingTelemetry))
telemetry
(branch
SM86ProgramEncodingTelemetryValue
instructions
outputBytes
fields
bits
highest
.
(constructor
SM86ProgramEncodingTelemetry
SM86ProgramEncodingTelemetryValue
(naturalMultiply instructions count)
(naturalMultiply outputBytes count)
(naturalMultiply fields count)
(naturalMultiply bits count)
highest)))))
def sm86ProgramEncodingAppend =
(lambda unrestricted left : (family SM86ProgramEncodingResult) .
(lambda unrestricted right : (family SM86ProgramEncodingResult) .
(eliminate
SM86ProgramEncodingResult
(lambda unrestricted current : (family SM86ProgramEncodingResult) .
(family SM86ProgramEncodingResult))
left
(branch
SM86ProgramEncodingSucceeded
leftBytes
leftTelemetry
.
(eliminate
SM86ProgramEncodingResult
(lambda unrestricted current : (family SM86ProgramEncodingResult) .
(family SM86ProgramEncodingResult))
right
(branch
SM86ProgramEncodingSucceeded
rightBytes
rightTelemetry
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingSucceeded
(bytes-builder-build
(bytes-builder-append
(bytes-builder-chunk leftBytes)
(bytes-builder-chunk rightBytes)))
(sm86MergeProgramTelemetry leftTelemetry rightTelemetry)))
(branch
SM86ProgramEncodingFailed
rightFailureIndex
rightFailure
rightFailureTelemetry
.
(eliminate
SM86ProgramEncodingTelemetry
(lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
(family SM86ProgramEncodingResult))
leftTelemetry
(branch
SM86ProgramEncodingTelemetryValue
leftInstructions
leftOutputBytes
leftFields
leftBits
leftHighest
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingFailed
(naturalAdd leftInstructions rightFailureIndex)
rightFailure
(sm86MergeProgramTelemetry leftTelemetry rightFailureTelemetry)))))))
(branch
SM86ProgramEncodingFailed
leftFailureIndex
leftFailure
leftFailureTelemetry
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingFailed
leftFailureIndex
leftFailure
leftFailureTelemetry)))))
def sm86EncodeProgramRepeated =
(lambda unrestricted segment : (family SM86Program) .
(lambda unrestricted count : Nat .
(nat-eliminate
(lambda unrestricted nonzero : Nat . (family SM86ProgramEncodingResult))
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingSucceeded
b""
sm86ProgramTelemetryZero)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family SM86ProgramEncodingResult) .
(eliminate
SM86ProgramEncodingResult
(lambda unrestricted current : (family SM86ProgramEncodingResult) .
(family SM86ProgramEncodingResult))
(sm86EncodeProgram segment)
(branch
SM86ProgramEncodingSucceeded
segmentBytes
segmentTelemetry
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingSucceeded
(bytes-builder-build (sm86RepeatedProgramBytesBuilder segmentBytes count))
(sm86ScaleProgramTelemetry segmentTelemetry count)))
(branch
SM86ProgramEncodingFailed
failureIndex
failure
failureTelemetry
.
(constructor
SM86ProgramEncodingResult
SM86ProgramEncodingFailed
failureIndex
failure
failureTelemetry)))))
(naturalNonzero count))))
def sm86InstructionEncodingStableCode =
(lambda unrestricted result : (family SM86InstructionEncodingResult) .
(eliminate
SM86InstructionEncodingResult
(lambda unrestricted current : (family SM86InstructionEncodingResult) . Bytes)
result
(branch
SM86InstructionEncodingSucceeded
encoded
telemetry
.
b"ALPHA-SM86-INS-000")
(branch
SM86InstructionEncodingFieldFailed
error
position
width
detail
telemetry
.
(sm86EncodingErrorStableCode error))
(branch
SM86InstructionEncodingUnsupported
ordinal
.
b"ALPHA-SM86-INS-001")))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.