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")))