module Realization.Nvidia.SM86.GreedyArgmaxSM86 import Accelerator.SM86.Control import Accelerator.SM86.Immediate import Accelerator.SM86.Instruction import Accelerator.SM86.InstructionEncoding import Accelerator.SM86.Program import Accelerator.SM86.Types import Data.SHA256Digest import Std.Natural import Accelerator.SM86.NumericSemantics family GreedyArgmaxSM86ExecutionContract : Type 0 constructor GreedyArgmaxSM86NativeOnly end-family family GreedyArgmaxSM86FailureCode : Type 0 constructor GreedyArgmaxSM86VocabularyZero constructor GreedyArgmaxSM86VocabularyTooLarge constructor GreedyArgmaxSM86InstructionCountMismatch constructor GreedyArgmaxSM86EncodedInstructionCountMismatch constructor GreedyArgmaxSM86EncodedByteCountMismatch constructor GreedyArgmaxSM86RegisterCountMismatch constructor GreedyArgmaxSM86SharedByteCountMismatch constructor GreedyArgmaxSM86GridCountMismatch constructor GreedyArgmaxSM86ThreadCountMismatch constructor GreedyArgmaxSM86ImageEncodingFailed constructor GreedyArgmaxSM86ImageIdentityFailed constructor GreedyArgmaxSM86ImageIdentityLengthInvalid constructor GreedyArgmaxSM86HostFallbackDetected end-family family GreedyArgmaxSM86Validation : Type 0 constructor GreedyArgmaxSM86ValidationAccepted constructor GreedyArgmaxSM86ValidationRejected field unrestricted greedyArgmaxSM86ValidationFailure : (family GreedyArgmaxSM86FailureCode) end-family family GreedyArgmaxSM86OutputReceipt : Type 0 constructor GreedyArgmaxSM86OutputReceiptValue field unrestricted greedyArgmaxSM86ReceiptTokenOffset : Nat field unrestricted greedyArgmaxSM86ReceiptValidityOffset : Nat field unrestricted greedyArgmaxSM86ReceiptWordBytes : Nat field unrestricted greedyArgmaxSM86ReceiptValidValue : Nat field unrestricted greedyArgmaxSM86ReceiptInvalidValue : Nat end-family family GreedyArgmaxSM86ABI : Type 0 constructor GreedyArgmaxSM86ABIValue field unrestricted greedyArgmaxSM86ABIConstantBank : Nat field unrestricted greedyArgmaxSM86ABIOutputPointerOffset : Nat field unrestricted greedyArgmaxSM86ABILogitsPointerOffset : Nat field unrestricted greedyArgmaxSM86ABILogitElementBytes : Nat field unrestricted greedyArgmaxSM86ABIReceipt : (family GreedyArgmaxSM86OutputReceipt) end-family family GreedyArgmaxSM86Manifest : Type 0 constructor GreedyArgmaxSM86ManifestValue field unrestricted greedyArgmaxSM86ManifestVocabulary : Nat field unrestricted greedyArgmaxSM86ManifestFullSlots : Nat field unrestricted greedyArgmaxSM86ManifestTailLanes : Nat field unrestricted greedyArgmaxSM86ManifestExpectedInstructions : Nat field unrestricted greedyArgmaxSM86ManifestExpectedBytes : Nat field unrestricted greedyArgmaxSM86ManifestRegisters : Nat field unrestricted greedyArgmaxSM86ManifestSharedBytes : Nat field unrestricted greedyArgmaxSM86ManifestGridX : Nat field unrestricted greedyArgmaxSM86ManifestThreadsPerBlock : Nat field unrestricted greedyArgmaxSM86ManifestActiveLogitLoads : Nat field unrestricted greedyArgmaxSM86ManifestActiveFiniteChecks : Nat field unrestricted greedyArgmaxSM86ManifestInactiveFiniteChecks : Nat field unrestricted greedyArgmaxSM86ManifestTailMaskWrites : Nat field unrestricted greedyArgmaxSM86ManifestTieReductionStages : Nat field unrestricted greedyArgmaxSM86ManifestTokenWrites : Nat field unrestricted greedyArgmaxSM86ManifestValidityWrites : Nat field unrestricted greedyArgmaxSM86ManifestHostLogitReads : Nat field unrestricted greedyArgmaxSM86ManifestHostFallbackOperations : Nat field unrestricted greedyArgmaxSM86ManifestABI : (family GreedyArgmaxSM86ABI) end-family family GreedyArgmaxSM86Telemetry : Type 0 constructor GreedyArgmaxSM86TelemetryValue field unrestricted greedyArgmaxSM86TelemetryContract : (family GreedyArgmaxSM86ExecutionContract) field unrestricted greedyArgmaxSM86TelemetryManifest : (family GreedyArgmaxSM86Manifest) field unrestricted greedyArgmaxSM86TelemetryObservedInstructions : Nat field unrestricted greedyArgmaxSM86TelemetryObservedBytes : Nat field unrestricted greedyArgmaxSM86TelemetryEncodingFields : Nat field unrestricted greedyArgmaxSM86TelemetryEncodingBits : Nat field unrestricted greedyArgmaxSM86TelemetryHighestEncodedBit : Nat field unrestricted greedyArgmaxSM86TelemetryIdentityInputBytes : Nat field unrestricted greedyArgmaxSM86TelemetryIdentityOutputBytes : Nat field unrestricted greedyArgmaxSM86TelemetryTailValidationSeparated : Nat field unrestricted greedyArgmaxSM86TelemetryLowestTokenTieBreak : Nat field unrestricted greedyArgmaxSM86TelemetryHostFallbackOperations : Nat end-family family GreedyArgmaxSM86Artifact : Type 0 constructor GreedyArgmaxSM86ArtifactReady field unrestricted greedyArgmaxSM86ArtifactProgram : (family SM86Program) field unrestricted greedyArgmaxSM86ArtifactImage : Bytes field unrestricted greedyArgmaxSM86ArtifactImageSHA256 : Bytes field unrestricted greedyArgmaxSM86ArtifactManifest : (family GreedyArgmaxSM86Manifest) field unrestricted greedyArgmaxSM86ArtifactEncodingTelemetry : (family SM86ProgramEncodingTelemetry) field unrestricted greedyArgmaxSM86ArtifactIdentityTelemetry : (family SHA256DigestTelemetry) field unrestricted greedyArgmaxSM86ArtifactTelemetry : (family GreedyArgmaxSM86Telemetry) constructor GreedyArgmaxSM86ArtifactFailed field unrestricted greedyArgmaxSM86ArtifactFailure : (family GreedyArgmaxSM86FailureCode) field unrestricted greedyArgmaxSM86ArtifactFailureOrdinal : Nat field unrestricted greedyArgmaxSM86ArtifactFailureDetail : Bytes field unrestricted greedyArgmaxSM86ArtifactFailureTelemetry : (family GreedyArgmaxSM86Telemetry) end-family def greedyArgmaxSM86N1 = (succ zero) def greedyArgmaxSM86N2 = (byte-to-nat (byte 2)) def greedyArgmaxSM86N4 = (byte-to-nat (byte 4)) def greedyArgmaxSM86N5 = (byte-to-nat (byte 5)) def greedyArgmaxSM86N7 = (byte-to-nat (byte 7)) def greedyArgmaxSM86N8 = (byte-to-nat (byte 8)) def greedyArgmaxSM86N12 = (byte-to-nat (byte 12)) def greedyArgmaxSM86N16 = (byte-to-nat (byte 16)) def greedyArgmaxSM86N23 = (byte-to-nat (byte 23)) def greedyArgmaxSM86N30 = (byte-to-nat (byte 30)) def greedyArgmaxSM86N31 = (byte-to-nat (byte 31)) def greedyArgmaxSM86N32 = (byte-to-nat (byte 32)) def greedyArgmaxSM86N33 = (byte-to-nat (byte 33)) def greedyArgmaxSM86N64 = (byte-to-nat (byte 64)) def greedyArgmaxSM86N96 = (byte-to-nat (byte 96)) def greedyArgmaxSM86N115 = (byte-to-nat (byte 115)) def greedyArgmaxSM86N251 = (byte-to-nat (byte 251)) def greedyArgmaxSM86N254 = (byte-to-nat (byte 254)) def greedyArgmaxSM86N255 = (byte-to-nat (byte 255)) def greedyArgmaxSM86N256 = (succ greedyArgmaxSM86N255) def greedyArgmaxSM86N277 = (naturalAdd greedyArgmaxSM86N256 (naturalAdd greedyArgmaxSM86N16 greedyArgmaxSM86N5)) def greedyArgmaxSM86N352 = (naturalAdd greedyArgmaxSM86N256 greedyArgmaxSM86N96) def greedyArgmaxSM86N360 = (naturalAdd greedyArgmaxSM86N352 greedyArgmaxSM86N8) def greedyArgmaxSM86N12288 = (naturalMultiply (byte-to-nat (byte 48)) greedyArgmaxSM86N256) def greedyArgmaxSM86N49152 = (naturalMultiply greedyArgmaxSM86N12288 greedyArgmaxSM86N4) def greedyArgmaxSM86N1717 = (naturalAdd (naturalMultiply (byte-to-nat (byte 48)) greedyArgmaxSM86N30) greedyArgmaxSM86N277) def greedyArgmaxSM86N27472 = (naturalMultiply greedyArgmaxSM86N1717 greedyArgmaxSM86N16) def greedyArgmaxSM86N10 = (byte-to-nat (byte 10)) def greedyArgmaxSM86MaximumVocabulary = greedyArgmaxSM86N12288 def greedyArgmaxSM86PromotedVocabulary = greedyArgmaxSM86N12288 def greedyArgmaxSM86PromotedInstructions = greedyArgmaxSM86N1717 def greedyArgmaxSM86PromotedBytes = greedyArgmaxSM86N27472 def greedyArgmaxSM86Registers = greedyArgmaxSM86N32 def greedyArgmaxSM86SharedBytes = greedyArgmaxSM86N96 def greedyArgmaxSM86GridX = greedyArgmaxSM86N1 def greedyArgmaxSM86ThreadsPerBlock = greedyArgmaxSM86N256 def greedyArgmaxSM86InstructionBytes = greedyArgmaxSM86N16 def greedyArgmaxSM86HostLogitReads = zero def greedyArgmaxSM86HostFallbackOperations = zero def greedyArgmaxSM86U0 = sm86Unsigned32Zero def greedyArgmaxSM86U1 = sm86Unsigned32One def greedyArgmaxSM86U4 = (sm86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0)) def greedyArgmaxSM86U7 = (sm86Unsigned32 (byte 7) (byte 0) (byte 0) (byte 0)) def greedyArgmaxSM86U8 = (sm86Unsigned32 (byte 8) (byte 0) (byte 0) (byte 0)) def greedyArgmaxSM86U12 = (sm86Unsigned32 (byte 12) (byte 0) (byte 0) (byte 0)) def greedyArgmaxSM86U31 = (sm86Unsigned32 (byte 31) (byte 0) (byte 0) (byte 0)) def greedyArgmaxSM86U254 = (sm86Unsigned32 (byte 254) (byte 0) (byte 0) (byte 0)) def greedyArgmaxSM86U352 = (sm86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0)) def greedyArgmaxSM86U356 = (sm86Unsigned32 (byte 100) (byte 1) (byte 0) (byte 0)) def greedyArgmaxSM86U360 = (sm86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0)) def greedyArgmaxSM86UFloatZero = greedyArgmaxSM86U0 def greedyArgmaxSM86UFloatOne = (sm86Unsigned32 (byte 0) (byte 0) (byte 128) (byte 63)) def greedyArgmaxSM86UFloatNegativeInfinity = (sm86Unsigned32 (byte 0) (byte 0) (byte 128) (byte 255)) def greedyArgmaxSM86UAbsMask = (sm86Unsigned32 (byte 255) (byte 255) (byte 255) (byte 127)) def greedyArgmaxSM86UByteMask = (sm86Unsigned32 (byte 255) (byte 0) (byte 0) (byte 0)) def greedyArgmaxSM86UMaximumToken = (sm86Unsigned32 (byte 255) (byte 255) (byte 255) (byte 255)) def greedyArgmaxSM86ByteLoopBackOffset = (sm86Unsigned32 (byte 64) (byte 255) (byte 255) (byte 255)) def greedyArgmaxSM86BackwardBranchDescriptor = (sm86Unsigned32 (byte 255) (byte 255) (byte 131) (byte 3)) def greedyArgmaxSM86R0 = (sm86Register (byte 0)) def greedyArgmaxSM86R1 = (sm86Register (byte 1)) def greedyArgmaxSM86R2 = (sm86Register (byte 2)) def greedyArgmaxSM86R3 = (sm86Register (byte 3)) def greedyArgmaxSM86R4 = (sm86Register (byte 4)) def greedyArgmaxSM86R6 = (sm86Register (byte 6)) def greedyArgmaxSM86R7 = (sm86Register (byte 7)) def greedyArgmaxSM86R8 = (sm86Register (byte 8)) def greedyArgmaxSM86R9 = (sm86Register (byte 9)) def greedyArgmaxSM86R10 = (sm86Register (byte 10)) def greedyArgmaxSM86R11 = (sm86Register (byte 11)) def greedyArgmaxSM86R12 = (sm86Register (byte 12)) def greedyArgmaxSM86R13 = (sm86Register (byte 13)) def greedyArgmaxSM86R14 = (sm86Register (byte 14)) def greedyArgmaxSM86R15 = (sm86Register (byte 15)) def greedyArgmaxSM86R16 = (sm86Register (byte 16)) def greedyArgmaxSM86R17 = (sm86Register (byte 17)) def greedyArgmaxSM86R18 = (sm86Register (byte 18)) def greedyArgmaxSM86R19 = (sm86Register (byte 19)) def greedyArgmaxSM86R20 = (sm86Register (byte 20)) def greedyArgmaxSM86R21 = (sm86Register (byte 21)) def greedyArgmaxSM86R22 = (sm86Register (byte 22)) def greedyArgmaxSM86R23 = (sm86Register (byte 23)) def greedyArgmaxSM86R24 = (sm86Register (byte 24)) def greedyArgmaxSM86R25 = (sm86Register (byte 25)) def greedyArgmaxSM86R26 = (sm86Register (byte 26)) def greedyArgmaxSM86R27 = (sm86Register (byte 27)) def greedyArgmaxSM86R28 = (sm86Register (byte 28)) def greedyArgmaxSM86R29 = (sm86Register (byte 29)) def greedyArgmaxSM86P0 : (family SM86Predicate) = (constructor SM86Predicate SM86Predicate0) def greedyArgmaxSM86P1 : (family SM86Predicate) = (constructor SM86Predicate SM86Predicate1) def greedyArgmaxSM86P2 : (family SM86Predicate) = (constructor SM86Predicate SM86Predicate2) def greedyArgmaxSM86P3 : (family SM86Predicate) = (constructor SM86Predicate SM86Predicate3) def greedyArgmaxSM86FloatMaximum : (family SM86FloatExtremum) = (constructor SM86FloatExtremum SM86FloatMaximum) def greedyArgmaxSM86FloatMinimum : (family SM86FloatExtremum) = (constructor SM86FloatExtremum SM86FloatMinimum) def greedyArgmaxSM86ShuffleButterfly : (family SM86ShuffleMode) = (constructor SM86ShuffleMode SM86ShuffleButterfly) def greedyArgmaxSM86Set0 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0)) def greedyArgmaxSM86Set1 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1)) def greedyArgmaxSM86Set2 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2)) def greedyArgmaxSM86Wait0 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0)) def greedyArgmaxSM86Wait1 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier1)) def greedyArgmaxSM86Wait2 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier2)) def greedyArgmaxSM86Next = (lambda unrestricted body : (family SM86InstructionBody) . (lambda unrestricted tail : (family SM86Program) . (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail))) def greedyArgmaxSM86When = (lambda unrestricted predicate : (family SM86Predicate) . (lambda unrestricted body : (family SM86InstructionBody) . (lambda unrestricted tail : (family SM86Program) . (constructor SM86Program SM86ProgramNext (sm86PredicatedInstruction predicate body) tail)))) def greedyArgmaxSM86WhenNot = (lambda unrestricted predicate : (family SM86Predicate) . (lambda unrestricted body : (family SM86InstructionBody) . (lambda unrestricted tail : (family SM86Program) . (constructor SM86Program SM86ProgramNext (sm86NegatedPredicatedInstruction predicate body) tail)))) def greedyArgmaxSM86Unsigned32FromNatural = (lambda unrestricted value : Nat . (app (lambda unrestricted quotient1 : Nat . (app (lambda unrestricted quotient2 : Nat . (app (lambda unrestricted quotient3 : Nat . (sm86Unsigned32 (nat-to-byte (naturalModuloUnchecked value greedyArgmaxSM86N256)) (nat-to-byte (naturalModuloUnchecked quotient1 greedyArgmaxSM86N256)) (nat-to-byte (naturalModuloUnchecked quotient2 greedyArgmaxSM86N256)) (nat-to-byte (naturalModuloUnchecked quotient3 greedyArgmaxSM86N256)))) (naturalDivideUnchecked quotient2 greedyArgmaxSM86N256))) (naturalDivideUnchecked quotient1 greedyArgmaxSM86N256))) (naturalDivideUnchecked value greedyArgmaxSM86N256))) def greedyArgmaxSM86ReceiptValue = (constructor GreedyArgmaxSM86OutputReceipt GreedyArgmaxSM86OutputReceiptValue zero greedyArgmaxSM86N4 greedyArgmaxSM86N4 greedyArgmaxSM86N1 zero) def greedyArgmaxSM86ABIValue = (constructor GreedyArgmaxSM86ABI GreedyArgmaxSM86ABIValue zero greedyArgmaxSM86N352 greedyArgmaxSM86N360 greedyArgmaxSM86N4 greedyArgmaxSM86ReceiptValue) def greedyArgmaxSM86FailureCodeBytes = (lambda unrestricted code : (family GreedyArgmaxSM86FailureCode) . (eliminate GreedyArgmaxSM86FailureCode (lambda unrestricted current : (family GreedyArgmaxSM86FailureCode) . Bytes) code (branch GreedyArgmaxSM86VocabularyZero . b"ALPHA-SM86-GREEDY-001") (branch GreedyArgmaxSM86VocabularyTooLarge . b"ALPHA-SM86-GREEDY-002") (branch GreedyArgmaxSM86InstructionCountMismatch . b"ALPHA-SM86-GREEDY-003") (branch GreedyArgmaxSM86EncodedInstructionCountMismatch . b"ALPHA-SM86-GREEDY-004") (branch GreedyArgmaxSM86EncodedByteCountMismatch . b"ALPHA-SM86-GREEDY-005") (branch GreedyArgmaxSM86RegisterCountMismatch . b"ALPHA-SM86-GREEDY-006") (branch GreedyArgmaxSM86SharedByteCountMismatch . b"ALPHA-SM86-GREEDY-007") (branch GreedyArgmaxSM86GridCountMismatch . b"ALPHA-SM86-GREEDY-008") (branch GreedyArgmaxSM86ThreadCountMismatch . b"ALPHA-SM86-GREEDY-009") (branch GreedyArgmaxSM86ImageEncodingFailed . b"ALPHA-SM86-GREEDY-010") (branch GreedyArgmaxSM86ImageIdentityFailed . b"ALPHA-SM86-GREEDY-011") (branch GreedyArgmaxSM86ImageIdentityLengthInvalid . b"ALPHA-SM86-GREEDY-012") (branch GreedyArgmaxSM86HostFallbackDetected . b"ALPHA-SM86-GREEDY-013"))) def greedyArgmaxSM86ValidateVocabulary = (lambda unrestricted vocabulary : Nat . (nat-eliminate (lambda unrestricted positive : Nat . (family GreedyArgmaxSM86Validation)) (constructor GreedyArgmaxSM86Validation GreedyArgmaxSM86ValidationRejected (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86VocabularyZero)) (lambda unrestricted positivePredecessor : Nat . (lambda unrestricted positiveInduction : (family GreedyArgmaxSM86Validation) . (nat-eliminate (lambda unrestricted bounded : Nat . (family GreedyArgmaxSM86Validation)) (constructor GreedyArgmaxSM86Validation GreedyArgmaxSM86ValidationRejected (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86VocabularyTooLarge)) (lambda unrestricted boundedPredecessor : Nat . (lambda unrestricted boundedInduction : (family GreedyArgmaxSM86Validation) . (constructor GreedyArgmaxSM86Validation GreedyArgmaxSM86ValidationAccepted))) (naturalLessOrEqual vocabulary greedyArgmaxSM86MaximumVocabulary)))) (naturalNonzero vocabulary))) def greedyArgmaxSM86InitialProgram : (family SM86Program) = (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86SpecialToRegister greedyArgmaxSM86R0 (constructor SM86SpecialRegister SM86ThreadIdX) greedyArgmaxSM86Set0) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R4 greedyArgmaxSM86U4 greedyArgmaxSM86Wait0) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R7 greedyArgmaxSM86UFloatNegativeInfinity sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R8 greedyArgmaxSM86UMaximumToken sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R9 greedyArgmaxSM86UAbsMask sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R12 greedyArgmaxSM86UFloatZero sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R11 greedyArgmaxSM86UByteMask sm86SafeControl) sm86ProgramEmpty))))))) def greedyArgmaxSM86ValidateCandidateProgram : (family SM86Program) = (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86ShiftRightImmediate greedyArgmaxSM86R14 greedyArgmaxSM86R10 (byte 23) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable greedyArgmaxSM86R14 greedyArgmaxSM86R14 greedyArgmaxSM86R11 (byte 192) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P1 greedyArgmaxSM86R14 greedyArgmaxSM86U254 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R13 greedyArgmaxSM86UFloatZero sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P1 (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R13 greedyArgmaxSM86UFloatOne sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R12 greedyArgmaxSM86R12 greedyArgmaxSM86R13 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P1 (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R10 greedyArgmaxSM86UFloatNegativeInfinity sm86SafeControl) sm86ProgramEmpty))))))) def greedyArgmaxSM86CandidateProgram : (family SM86Program) = (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatMinimumOrMaximum greedyArgmaxSM86R14 greedyArgmaxSM86R7 greedyArgmaxSM86R10 greedyArgmaxSM86FloatMaximum sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatNegate greedyArgmaxSM86R15 greedyArgmaxSM86R14 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R16 greedyArgmaxSM86R7 greedyArgmaxSM86R15 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable greedyArgmaxSM86R16 greedyArgmaxSM86R16 greedyArgmaxSM86R9 (byte 192) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P2 greedyArgmaxSM86R16 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P2 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R8 greedyArgmaxSM86R3 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R17 greedyArgmaxSM86R10 greedyArgmaxSM86R15 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable greedyArgmaxSM86R17 greedyArgmaxSM86R17 greedyArgmaxSM86R9 (byte 192) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P3 greedyArgmaxSM86R17 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P3 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R3 greedyArgmaxSM86R8 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerToFloat greedyArgmaxSM86R23 greedyArgmaxSM86R8 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerToFloat greedyArgmaxSM86R24 greedyArgmaxSM86R3 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatMinimumOrMaximum greedyArgmaxSM86R25 greedyArgmaxSM86R23 greedyArgmaxSM86R24 greedyArgmaxSM86FloatMinimum sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatNegate greedyArgmaxSM86R26 greedyArgmaxSM86R25 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R27 greedyArgmaxSM86R23 greedyArgmaxSM86R26 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable greedyArgmaxSM86R27 greedyArgmaxSM86R27 greedyArgmaxSM86R9 (byte 192) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P1 greedyArgmaxSM86R27 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P1 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R8 greedyArgmaxSM86R3 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R7 greedyArgmaxSM86R14 greedyArgmaxSM86U0 sm86SafeControl) sm86ProgramEmpty))))))))))))))))))) def greedyArgmaxSM86ByteVocabularyInitialProgram : (family SM86Program) = (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R3 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R4 greedyArgmaxSM86U4 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R7 greedyArgmaxSM86UFloatNegativeInfinity sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R8 greedyArgmaxSM86UMaximumToken sm86SafeControl) sm86ProgramEmpty)))) def greedyArgmaxSM86AscendingCandidateProgram : (family SM86Program) = (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatMinimumOrMaximum greedyArgmaxSM86R14 greedyArgmaxSM86R7 greedyArgmaxSM86R10 greedyArgmaxSM86FloatMaximum sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatNegate greedyArgmaxSM86R15 greedyArgmaxSM86R14 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R16 greedyArgmaxSM86R7 greedyArgmaxSM86R15 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P2 greedyArgmaxSM86R16 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P2 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R8 greedyArgmaxSM86R3 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R7 greedyArgmaxSM86R14 greedyArgmaxSM86U0 sm86SafeControl) sm86ProgramEmpty)))))) -- Bob uses one thread and one native backward branch to scan all 256 byte -- logits. The twelve-instruction loop advances R3 from 0 through 255, so the -- branch offset is -192 bytes from the instruction following BRA. def greedyArgmaxSM86ByteVocabularyLoopProgram : (family SM86Program) = (sm86ProgramAppend (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant greedyArgmaxSM86R24 greedyArgmaxSM86R3 greedyArgmaxSM86R4 (byte 0) greedyArgmaxSM86U360 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LoadGlobal greedyArgmaxSM86R10 greedyArgmaxSM86R24 greedyArgmaxSM86U0 greedyArgmaxSM86Set0) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R10 greedyArgmaxSM86R10 greedyArgmaxSM86U0 greedyArgmaxSM86Wait0) sm86ProgramEmpty))) (sm86ProgramAppend greedyArgmaxSM86AscendingCandidateProgram (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R3 greedyArgmaxSM86R3 greedyArgmaxSM86U1 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P0 greedyArgmaxSM86R3 greedyArgmaxSM86UByteMask sm86SafeControl) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86Branch greedyArgmaxSM86ByteLoopBackOffset greedyArgmaxSM86BackwardBranchDescriptor sm86BranchControl) sm86ProgramEmpty))))) def greedyArgmaxSM86FullSlotProgram = (lambda unrestricted slot : Nat . (app (lambda unrestricted base : Nat . (sm86ProgramAppend (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R3 greedyArgmaxSM86R0 (greedyArgmaxSM86Unsigned32FromNatural base) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant greedyArgmaxSM86R28 greedyArgmaxSM86R3 greedyArgmaxSM86R4 (byte 0) greedyArgmaxSM86U360 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LoadGlobal greedyArgmaxSM86R10 greedyArgmaxSM86R28 greedyArgmaxSM86U0 greedyArgmaxSM86Set0) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R10 greedyArgmaxSM86R10 greedyArgmaxSM86U0 greedyArgmaxSM86Wait0) sm86ProgramEmpty)))) (sm86ProgramAppend greedyArgmaxSM86ValidateCandidateProgram greedyArgmaxSM86CandidateProgram))) (naturalMultiply slot greedyArgmaxSM86N256))) def greedyArgmaxSM86PartialSlotProgram = (lambda unrestricted slot : Nat . (lambda unrestricted lastLane : Nat . (app (lambda unrestricted base : Nat . (sm86ProgramAppend (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P0 greedyArgmaxSM86R0 (greedyArgmaxSM86Unsigned32FromNatural lastLane) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R3 greedyArgmaxSM86R0 (greedyArgmaxSM86Unsigned32FromNatural base) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant greedyArgmaxSM86R28 greedyArgmaxSM86R3 greedyArgmaxSM86R4 (byte 0) greedyArgmaxSM86U360 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R10 greedyArgmaxSM86UFloatZero sm86SafeControl) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86LoadGlobal greedyArgmaxSM86R10 greedyArgmaxSM86R28 greedyArgmaxSM86U0 greedyArgmaxSM86Set0) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R10 greedyArgmaxSM86R10 greedyArgmaxSM86U0 greedyArgmaxSM86Wait0) sm86ProgramEmpty)))))) (sm86ProgramAppend greedyArgmaxSM86ValidateCandidateProgram (greedyArgmaxSM86When greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R10 greedyArgmaxSM86UFloatNegativeInfinity sm86SafeControl) greedyArgmaxSM86CandidateProgram)))) (naturalMultiply slot greedyArgmaxSM86N256)))) def greedyArgmaxSM86FullSlotPrograms = (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family SM86Program)) sm86ProgramEmpty (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SM86Program) . (sm86ProgramAppend induction (greedyArgmaxSM86FullSlotProgram predecessor)))) count)) def greedyArgmaxSM86SlotPrograms = (lambda unrestricted vocabulary : Nat . (app (lambda unrestricted fullSlots : Nat . (app (lambda unrestricted remainder : Nat . (app (lambda unrestricted fullProgram : (family SM86Program) . (nat-eliminate (lambda unrestricted tailLanes : Nat . (family SM86Program)) fullProgram (lambda unrestricted lastLane : Nat . (lambda unrestricted tailInduction : (family SM86Program) . (sm86ProgramAppend fullProgram (greedyArgmaxSM86PartialSlotProgram fullSlots lastLane)))) remainder)) (greedyArgmaxSM86FullSlotPrograms fullSlots))) (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256))) (naturalDivideUnchecked vocabulary greedyArgmaxSM86N256))) def greedyArgmaxSM86PairStage = (lambda unrestricted lane : Byte . (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86WarpShuffle greedyArgmaxSM86R17 greedyArgmaxSM86R7 lane greedyArgmaxSM86U31 greedyArgmaxSM86ShuffleButterfly greedyArgmaxSM86Set0) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86WarpShuffle greedyArgmaxSM86R18 greedyArgmaxSM86R8 lane greedyArgmaxSM86U31 greedyArgmaxSM86ShuffleButterfly greedyArgmaxSM86Set1) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R18 greedyArgmaxSM86R18 greedyArgmaxSM86U0 greedyArgmaxSM86Wait1) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatMinimumOrMaximum greedyArgmaxSM86R19 greedyArgmaxSM86R7 greedyArgmaxSM86R17 greedyArgmaxSM86FloatMaximum greedyArgmaxSM86Wait0) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatNegate greedyArgmaxSM86R20 greedyArgmaxSM86R19 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R21 greedyArgmaxSM86R7 greedyArgmaxSM86R20 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable greedyArgmaxSM86R21 greedyArgmaxSM86R21 greedyArgmaxSM86R9 (byte 192) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P1 greedyArgmaxSM86R21 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R22 greedyArgmaxSM86R17 greedyArgmaxSM86R20 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable greedyArgmaxSM86R22 greedyArgmaxSM86R22 greedyArgmaxSM86R9 (byte 192) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P2 greedyArgmaxSM86R22 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P1 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R8 greedyArgmaxSM86R18 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P2 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R18 greedyArgmaxSM86R8 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerToFloat greedyArgmaxSM86R23 greedyArgmaxSM86R8 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerToFloat greedyArgmaxSM86R24 greedyArgmaxSM86R18 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatMinimumOrMaximum greedyArgmaxSM86R25 greedyArgmaxSM86R23 greedyArgmaxSM86R24 greedyArgmaxSM86FloatMinimum sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatNegate greedyArgmaxSM86R26 greedyArgmaxSM86R25 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R27 greedyArgmaxSM86R23 greedyArgmaxSM86R26 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable greedyArgmaxSM86R27 greedyArgmaxSM86R27 greedyArgmaxSM86R9 (byte 192) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P3 greedyArgmaxSM86R27 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P3 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R8 greedyArgmaxSM86R18 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R7 greedyArgmaxSM86R19 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86WarpShuffle greedyArgmaxSM86R17 greedyArgmaxSM86R12 lane greedyArgmaxSM86U31 greedyArgmaxSM86ShuffleButterfly greedyArgmaxSM86Set2) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R12 greedyArgmaxSM86R12 greedyArgmaxSM86R17 greedyArgmaxSM86Wait2) sm86ProgramEmpty))))))))))))))))))))))))) def greedyArgmaxSM86WarpReduceProgram : (family SM86Program) = (sm86ProgramAppend (greedyArgmaxSM86PairStage (byte 16)) (sm86ProgramAppend (greedyArgmaxSM86PairStage (byte 8)) (sm86ProgramAppend (greedyArgmaxSM86PairStage (byte 4)) (sm86ProgramAppend (greedyArgmaxSM86PairStage (byte 2)) (greedyArgmaxSM86PairStage (byte 1)))))) def greedyArgmaxSM86BlockReduceProgram : (family SM86Program) = (sm86ProgramAppend greedyArgmaxSM86WarpReduceProgram (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R1 greedyArgmaxSM86U31 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86LogicThreeInputTruthTable greedyArgmaxSM86R2 greedyArgmaxSM86R0 greedyArgmaxSM86R1 (byte 192) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P0 greedyArgmaxSM86R2 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86ShiftRightImmediate greedyArgmaxSM86R3 greedyArgmaxSM86R0 (byte 5) sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate greedyArgmaxSM86R4 greedyArgmaxSM86R3 greedyArgmaxSM86U12 sm86ZeroRegister sm86SafeControl) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86StoreShared greedyArgmaxSM86R4 greedyArgmaxSM86R7 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86StoreShared greedyArgmaxSM86R4 greedyArgmaxSM86R8 greedyArgmaxSM86U4 sm86SafeControl) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86StoreShared greedyArgmaxSM86R4 greedyArgmaxSM86R12 greedyArgmaxSM86U8 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R7 greedyArgmaxSM86UFloatNegativeInfinity sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R8 greedyArgmaxSM86UMaximumToken sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R12 greedyArgmaxSM86UFloatZero sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P0 greedyArgmaxSM86R0 greedyArgmaxSM86U7 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate greedyArgmaxSM86R4 greedyArgmaxSM86R0 greedyArgmaxSM86U12 sm86ZeroRegister sm86SafeControl) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86LoadShared greedyArgmaxSM86R7 greedyArgmaxSM86R4 greedyArgmaxSM86U0 greedyArgmaxSM86Set0) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86LoadShared greedyArgmaxSM86R8 greedyArgmaxSM86R4 greedyArgmaxSM86U4 greedyArgmaxSM86Set1) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86LoadShared greedyArgmaxSM86R12 greedyArgmaxSM86R4 greedyArgmaxSM86U8 greedyArgmaxSM86Set2) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R7 greedyArgmaxSM86R7 greedyArgmaxSM86U0 greedyArgmaxSM86Wait0) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86IntegerAddThreeImmediate greedyArgmaxSM86R8 greedyArgmaxSM86R8 greedyArgmaxSM86U0 greedyArgmaxSM86Wait1) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86FloatAdd greedyArgmaxSM86R12 greedyArgmaxSM86R12 greedyArgmaxSM86R13 greedyArgmaxSM86Wait2) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86BarrierSynchronize sm86SafeControl) greedyArgmaxSM86WarpReduceProgram)))))))))))))))))))))) def greedyArgmaxSM86SuffixProgram : (family SM86Program) = (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveConstant greedyArgmaxSM86R28 (byte 0) greedyArgmaxSM86U352 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveConstant greedyArgmaxSM86R29 (byte 0) greedyArgmaxSM86U356 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R27 greedyArgmaxSM86U1 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P1 greedyArgmaxSM86R12 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86When greedyArgmaxSM86P1 (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R27 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate greedyArgmaxSM86P0 greedyArgmaxSM86R0 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86StoreGlobal greedyArgmaxSM86R28 greedyArgmaxSM86R8 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86WhenNot greedyArgmaxSM86P0 (constructor SM86InstructionBody SM86StoreGlobal greedyArgmaxSM86R28 greedyArgmaxSM86R27 greedyArgmaxSM86U4 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) sm86ProgramEmpty))))))))) -- Bob's byte reference schedule has one thread, hence one writer. def greedyArgmaxSM86ByteVocabularySuffixProgram : (family SM86Program) = (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveConstant greedyArgmaxSM86R28 (byte 0) greedyArgmaxSM86U352 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveConstant greedyArgmaxSM86R29 (byte 0) greedyArgmaxSM86U356 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86MoveImmediate greedyArgmaxSM86R27 greedyArgmaxSM86U1 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86StoreGlobal greedyArgmaxSM86R28 greedyArgmaxSM86R8 greedyArgmaxSM86U0 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86StoreGlobal greedyArgmaxSM86R28 greedyArgmaxSM86R27 greedyArgmaxSM86U4 sm86SafeControl) (greedyArgmaxSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) sm86ProgramEmpty)))))) def greedyArgmaxSM86ProgramFor = (lambda unrestricted vocabulary : Nat . (sm86ProgramAppend greedyArgmaxSM86InitialProgram (sm86ProgramAppend (greedyArgmaxSM86SlotPrograms vocabulary) (sm86ProgramAppend greedyArgmaxSM86BlockReduceProgram greedyArgmaxSM86SuffixProgram)))) def greedyArgmaxSM86ByteVocabularyProgram : (family SM86Program) = (sm86ProgramAppend greedyArgmaxSM86ByteVocabularyInitialProgram (sm86ProgramAppend greedyArgmaxSM86ByteVocabularyLoopProgram greedyArgmaxSM86ByteVocabularySuffixProgram)) def greedyArgmaxSM86HasTail = (lambda unrestricted vocabulary : Nat . (naturalNonzero (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256))) def greedyArgmaxSM86ExpectedInstructions = (lambda unrestricted vocabulary : Nat . (naturalAdd greedyArgmaxSM86N277 (naturalAdd (naturalMultiply (naturalDivideUnchecked vocabulary greedyArgmaxSM86N256) greedyArgmaxSM86N30) (naturalMultiply (greedyArgmaxSM86HasTail vocabulary) greedyArgmaxSM86N33)))) def greedyArgmaxSM86TailMaskWrites = (lambda unrestricted vocabulary : Nat . (naturalMultiply (greedyArgmaxSM86HasTail vocabulary) (naturalSaturatingSubtract greedyArgmaxSM86N256 (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256)))) def greedyArgmaxSM86ManifestFor = (lambda unrestricted vocabulary : Nat . (app (lambda unrestricted expectedInstructions : Nat . (constructor GreedyArgmaxSM86Manifest GreedyArgmaxSM86ManifestValue vocabulary (naturalDivideUnchecked vocabulary greedyArgmaxSM86N256) (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256) expectedInstructions (naturalMultiply expectedInstructions greedyArgmaxSM86InstructionBytes) greedyArgmaxSM86Registers greedyArgmaxSM86SharedBytes greedyArgmaxSM86GridX greedyArgmaxSM86ThreadsPerBlock vocabulary vocabulary zero (greedyArgmaxSM86TailMaskWrites vocabulary) greedyArgmaxSM86N10 greedyArgmaxSM86N1 greedyArgmaxSM86N1 greedyArgmaxSM86HostLogitReads greedyArgmaxSM86HostFallbackOperations greedyArgmaxSM86ABIValue)) (greedyArgmaxSM86ExpectedInstructions vocabulary))) def greedyArgmaxSM86TelemetryFor = (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) . (lambda unrestricted observedInstructions : Nat . (lambda unrestricted observedBytes : Nat . (lambda unrestricted fields : Nat . (lambda unrestricted bits : Nat . (lambda unrestricted highest : Nat . (lambda unrestricted identityInput : Nat . (lambda unrestricted identityOutput : Nat . (constructor GreedyArgmaxSM86Telemetry GreedyArgmaxSM86TelemetryValue (constructor GreedyArgmaxSM86ExecutionContract GreedyArgmaxSM86NativeOnly) manifest observedInstructions observedBytes fields bits highest identityInput identityOutput greedyArgmaxSM86N1 greedyArgmaxSM86N1 greedyArgmaxSM86HostFallbackOperations))))))))) def greedyArgmaxSM86EmptyTelemetry = (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) . (lambda unrestricted observedInstructions : Nat . (lambda unrestricted observedBytes : Nat . (greedyArgmaxSM86TelemetryFor manifest observedInstructions observedBytes zero zero zero zero zero)))) def greedyArgmaxSM86Failed = (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) . (lambda unrestricted code : (family GreedyArgmaxSM86FailureCode) . (lambda unrestricted ordinal : Nat . (lambda unrestricted observedInstructions : Nat . (lambda unrestricted observedBytes : Nat . (constructor GreedyArgmaxSM86Artifact GreedyArgmaxSM86ArtifactFailed code ordinal (greedyArgmaxSM86FailureCodeBytes code) (greedyArgmaxSM86EmptyTelemetry manifest observedInstructions observedBytes))))))) def greedyArgmaxSM86BuildIdentity = (lambda unrestricted program : (family SM86Program) . (lambda unrestricted image : Bytes . (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) . (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) . (eliminate SM86ProgramEncodingTelemetry (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) . (family GreedyArgmaxSM86Artifact)) encodingTelemetry (branch SM86ProgramEncodingTelemetryValue instructions encodedBytes fields bits highest . (eliminate SHA256HexResult (lambda unrestricted current : (family SHA256HexResult) . (family GreedyArgmaxSM86Artifact)) (sha256Hex image) (branch SHA256HexSucceeded identity digestTelemetry . (nat-eliminate (lambda unrestricted exactLength : Nat . (family GreedyArgmaxSM86Artifact)) (greedyArgmaxSM86Failed manifest (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86ImageIdentityLengthInvalid) (bytes-length identity) instructions encodedBytes) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family GreedyArgmaxSM86Artifact) . (constructor GreedyArgmaxSM86Artifact GreedyArgmaxSM86ArtifactReady program image identity manifest encodingTelemetry digestTelemetry (greedyArgmaxSM86TelemetryFor manifest instructions encodedBytes fields bits highest (bytes-length image) (bytes-length identity))))) (naturalEqual (bytes-length identity) greedyArgmaxSM86N64))) (branch SHA256HexFailed failure hexFailureOrdinal digestTelemetry . (greedyArgmaxSM86Failed manifest (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86ImageIdentityFailed) zero instructions encodedBytes))))))))) def greedyArgmaxSM86BuildEncoded = (lambda unrestricted program : (family SM86Program) . (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) . (eliminate SM86ProgramEncodingResult (lambda unrestricted current : (family SM86ProgramEncodingResult) . (family GreedyArgmaxSM86Artifact)) (sm86EncodeProgram program) (branch SM86ProgramEncodingSucceeded image telemetry . (eliminate SM86ProgramEncodingTelemetry (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) . (family GreedyArgmaxSM86Artifact)) telemetry (branch SM86ProgramEncodingTelemetryValue instructions encodedBytes fields bits highest . (eliminate GreedyArgmaxSM86Manifest (lambda unrestricted current : (family GreedyArgmaxSM86Manifest) . (family GreedyArgmaxSM86Artifact)) manifest (branch GreedyArgmaxSM86ManifestValue vocabulary fullSlots tailLanes expectedInstructions expectedBytes registers sharedBytes gridX threads activeLoads activeFinite inactiveFinite tailMasks tieStages tokenWrites validityWrites hostReads fallbacks abi . (nat-eliminate (lambda unrestricted instructionsExact : Nat . (family GreedyArgmaxSM86Artifact)) (greedyArgmaxSM86Failed manifest (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86EncodedInstructionCountMismatch) instructions instructions encodedBytes) (lambda unrestricted instructionPredecessor : Nat . (lambda unrestricted instructionInduction : (family GreedyArgmaxSM86Artifact) . (nat-eliminate (lambda unrestricted bytesExact : Nat . (family GreedyArgmaxSM86Artifact)) (greedyArgmaxSM86Failed manifest (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86EncodedByteCountMismatch) encodedBytes instructions encodedBytes) (lambda unrestricted bytePredecessor : Nat . (lambda unrestricted byteInduction : (family GreedyArgmaxSM86Artifact) . (greedyArgmaxSM86BuildIdentity program image manifest telemetry))) (naturalEqual encodedBytes expectedBytes)))) (naturalEqual instructions expectedInstructions))))))) (branch SM86ProgramEncodingFailed instructionIndex failure telemetry . (greedyArgmaxSM86Failed manifest (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86ImageEncodingFailed) instructionIndex (sm86ProgramCount program) zero))))) def greedyArgmaxSM86BuildValidated = (lambda unrestricted vocabulary : Nat . (app (lambda unrestricted program : (family SM86Program) . (app (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) . (eliminate GreedyArgmaxSM86Manifest (lambda unrestricted current : (family GreedyArgmaxSM86Manifest) . (family GreedyArgmaxSM86Artifact)) manifest (branch GreedyArgmaxSM86ManifestValue manifestVocabulary fullSlots tailLanes expectedInstructions expectedBytes registers sharedBytes gridX threads activeLoads activeFinite inactiveFinite tailMasks tieStages tokenWrites validityWrites hostReads fallbacks abi . (nat-eliminate (lambda unrestricted fallbackFree : Nat . (family GreedyArgmaxSM86Artifact)) (greedyArgmaxSM86Failed manifest (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86HostFallbackDetected) fallbacks (sm86ProgramCount program) zero) (lambda unrestricted fallbackPredecessor : Nat . (lambda unrestricted fallbackInduction : (family GreedyArgmaxSM86Artifact) . (nat-eliminate (lambda unrestricted programExact : Nat . (family GreedyArgmaxSM86Artifact)) (greedyArgmaxSM86Failed manifest (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86InstructionCountMismatch) (sm86ProgramCount program) (sm86ProgramCount program) zero) (lambda unrestricted programPredecessor : Nat . (lambda unrestricted programInduction : (family GreedyArgmaxSM86Artifact) . (greedyArgmaxSM86BuildEncoded program manifest))) (naturalEqual (sm86ProgramCount program) expectedInstructions)))) (naturalEqual fallbacks zero))))) (greedyArgmaxSM86ManifestFor vocabulary))) (greedyArgmaxSM86ProgramFor vocabulary))) def greedyArgmaxSM86Build = (lambda unrestricted vocabulary : Nat . (eliminate GreedyArgmaxSM86Validation (lambda unrestricted current : (family GreedyArgmaxSM86Validation) . (family GreedyArgmaxSM86Artifact)) (greedyArgmaxSM86ValidateVocabulary vocabulary) (branch GreedyArgmaxSM86ValidationAccepted . (greedyArgmaxSM86BuildValidated vocabulary)) (branch GreedyArgmaxSM86ValidationRejected failure . (greedyArgmaxSM86Failed (greedyArgmaxSM86ManifestFor vocabulary) failure zero zero zero)))) def greedyArgmaxSM86BuildPromoted = (greedyArgmaxSM86Build greedyArgmaxSM86PromotedVocabulary) def greedyArgmaxSM86ByteVocabularyManifest : (family GreedyArgmaxSM86Manifest) = (app (lambda unrestricted expectedInstructions : Nat . (constructor GreedyArgmaxSM86Manifest GreedyArgmaxSM86ManifestValue greedyArgmaxSM86N256 greedyArgmaxSM86N256 zero expectedInstructions (naturalMultiply expectedInstructions greedyArgmaxSM86InstructionBytes) greedyArgmaxSM86Registers zero greedyArgmaxSM86GridX greedyArgmaxSM86N1 greedyArgmaxSM86N256 zero zero zero zero greedyArgmaxSM86N1 greedyArgmaxSM86N1 greedyArgmaxSM86HostLogitReads greedyArgmaxSM86HostFallbackOperations greedyArgmaxSM86ABIValue)) (sm86ProgramCount greedyArgmaxSM86ByteVocabularyProgram)) def greedyArgmaxSM86BuildByteVocabulary : (family GreedyArgmaxSM86Artifact) = (greedyArgmaxSM86BuildEncoded greedyArgmaxSM86ByteVocabularyProgram greedyArgmaxSM86ByteVocabularyManifest)