module Accelerator.SM86.Operands

import Accelerator.SM86.Control
import Accelerator.SM86.Immediate
import Accelerator.SM86.Instruction
import Accelerator.SM86.Types
import Std.List
import Std.Natural

-- The registers each instruction reads and writes, and the register demand
-- of a program: one owner for both the scoreboard pass (SM86.Scoreboard) and
-- the register count a launch declares.  A 64-bit address or value occupies
-- the named register and the next; the tensor core's A, C and D fragments
-- are four registers from the named one and its B fragment two; LDSM writes
-- one, two or four.  RZ (255) is not a register: it reads zero, absorbs
-- writes, and a fragment based at it names nothing.
--
-- The demand: the highest register named, plus one, plus TWO the hardware
-- reserves, rounded up to the allocation granule of eight.  Found on an RTX
-- 3070 (2026-09-23): the generated linear step at 2 x 6, 6 x 2 and 4 x 4 --
-- every shape whose declared count left exactly one register above the
-- highest named -- hung on the card with the GPU at 100 %, deterministically,
-- while every shape with two or more to spare ran; declaring the two
-- reserved registers made all three run.  The machine model cannot see it.

-- ---- one elimination per instruction ----
-- The schedule tools (SM86.Scoreboard's two passes,
-- Realization.Nvidia.SM86.StallCompaction) used to eliminate every
-- instruction body five or more times -- reads, writes, predicate writes,
-- latency class, fixed latency -- one 37-branch case split each.  The
-- summary answers them all in one split: each field below is the same
-- branch body the corresponding function above uses, tupled, so every
-- field is definitionally the old answer and a pass walks each
-- instruction's body once instead of five times.
family SM86OpSummary : Type 0
constructor SM86OpSummaryValue
field unrestricted sm86OpSummaryReads : (family StdList Nat)
field unrestricted sm86OpSummaryWrites : (family StdList Nat)
field unrestricted sm86OpSummaryPredicateWrites : (family StdList Nat)
field unrestricted sm86OpSummaryWaitKeys : (family StdList Nat)
field unrestricted sm86OpSummarySetKeys : (family StdList Nat)
field unrestricted sm86OpSummaryStall : Nat
field unrestricted sm86OpSummaryLatency : Nat
field unrestricted sm86OpSummaryVariable : Nat
-- sm86MinimumStall's
field unrestricted sm86OpSummaryMinimumStall : Nat
field unrestricted sm86OpSummaryControl : (family SM86Control)
end-family

def sm86RegisterZero : Nat = 255
def sm86RegisterGranule : Nat = 8
def sm86ReservedRegisters : Nat = 2

-- The most registers a launch can declare under the rule above: the
-- largest multiple of the granule in the 255 registers a thread has (R0 ..
-- R254; RZ is not one).  A register index is a byte, so a generator that
-- numbers registers past it does not fail -- its indices wrap onto registers
-- already in use; a generator states its span and is admitted against this.
def sm86RegisterLimit : Nat = 248

-- 1 when a program naming registers below `span` fits the register file
-- with the reserved two
def sm86RegisterSpanAdmitted =
  (lambda unrestricted span : Nat .
    (naturalLessOrEqual (naturalAdd span sm86ReservedRegisters) sm86RegisterLimit))

def sm86RegisterIndex =
  (lambda unrestricted register : (family SM86Register) .
    (eliminate SM86Register (lambda unrestricted current : (family SM86Register) . Nat) register
      (branch SM86RegisterValue index . (byte-to-nat index))))

def sm86NoRegisters : (family StdList Nat) = (constructor StdList StdListEmpty Nat)

-- `count` consecutive registers from `register`, prepended; none from RZ
def sm86RegisterRun =
  (lambda unrestricted register : (family SM86Register) .
    (lambda unrestricted count : Nat .
      (lambda unrestricted rest : (family StdList Nat) .
        (let unrestricted index = (sm86RegisterIndex register) in
        (nat-eliminate
          (lambda unrestricted current : Nat . (family StdList Nat))
          rest
          (lambda unrestricted named : Nat . (lambda unrestricted ignored : (family StdList Nat) .
            (nat-eliminate
              (lambda unrestricted current : Nat . (family StdList Nat))
              rest
              (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdList Nat) .
                (constructor StdList StdListCons Nat
                  (nat-add index (nat-subtract (nat-subtract count 1) predecessor))
                  induction)))
              count)))
          (nat-add (nat-less-than index sm86RegisterZero) (nat-less-than sm86RegisterZero index)))))))

def sm86One = (lambda unrestricted register : (family SM86Register) . (lambda unrestricted rest : (family StdList Nat) . (sm86RegisterRun register 1 rest)))
def sm86Pair = (lambda unrestricted register : (family SM86Register) . (lambda unrestricted rest : (family StdList Nat) . (sm86RegisterRun register 2 rest)))
def sm86Quad = (lambda unrestricted register : (family SM86Register) . (lambda unrestricted rest : (family StdList Nat) . (sm86RegisterRun register 4 rest)))

def sm86SharedMatrixRegisters =
  (lambda unrestricted count : (family SM86SharedMatrixCount) .
    (eliminate SM86SharedMatrixCount (lambda unrestricted current : (family SM86SharedMatrixCount) . Nat) count
      (branch SM86SharedMatrix1 . 1)
      (branch SM86SharedMatrix2 . 2)
      (branch SM86SharedMatrix4 . 4)))

def sm86ReadRegisters =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody
      (lambda unrestricted current : (family SM86InstructionBody) . (family StdList Nat))
      body
      (branch SM86MoveConstant destination bank offset control . sm86NoRegisters)
      (branch SM86SpecialToRegister destination source control . sm86NoRegisters)
      (branch SM86MoveImmediate destination immediate control . sm86NoRegisters)
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (sm86One left (sm86One addend sm86NoRegisters)))
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (sm86One left (sm86One addend sm86NoRegisters)))
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (sm86One left (sm86Pair right sm86NoRegisters)))
      (branch SM86IntegerAddThreeImmediate destination left immediate control . (sm86One left sm86NoRegisters))
      (branch SM86IntegerAddThreeRegister destination left right control . (sm86One left (sm86One right sm86NoRegisters)))
      (branch SM86ShiftRightImmediate destination source amount control . (sm86One source sm86NoRegisters))
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (sm86One left (sm86One right sm86NoRegisters)))
      (branch SM86IntegerToFloat destination source control . (sm86One source sm86NoRegisters))
      (branch SM86FloatAdd destination left right control . (sm86One left (sm86One right sm86NoRegisters)))
      (branch SM86FloatMultiply destination left right control . (sm86One left (sm86One right sm86NoRegisters)))
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (sm86One left (sm86One right (sm86One addend sm86NoRegisters))))
      (branch SM86MultiFunctionUnitApproximation destination source operation control . (sm86One source sm86NoRegisters))
      (branch SM86FloatMinimumOrMaximum destination left right mode control . (sm86One left (sm86One right sm86NoRegisters)))
      (branch SM86FloatNegate destination source control . (sm86One source sm86NoRegisters))
      (branch SM86FloatPairToPackedHalfPair destination high low control . (sm86One high (sm86One low sm86NoRegisters)))
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (sm86One high (sm86One low sm86NoRegisters)))
      (branch SM86HalfToFloat destination source selector control . (sm86One source sm86NoRegisters))
      (branch SM86BFloat16ToFloat destination source selector control . (sm86One source sm86NoRegisters))
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
        (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))))
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
        (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))))
      (branch SM86LoadGlobal destination address offset control . (sm86Pair address sm86NoRegisters))
      (branch SM86LoadGlobalWide destination address offset control . (sm86Pair address sm86NoRegisters))
      (branch SM86WarpShuffle destination source lane segment mode control . (sm86One source sm86NoRegisters))
      (branch SM86LoadShared destination address offset control . (sm86One address sm86NoRegisters))
      (branch SM86LoadSharedMatrix destination address offset count transpose control . (sm86One address sm86NoRegisters))
      (branch SM86StoreShared address value offset control . (sm86One address (sm86One value sm86NoRegisters)))
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (sm86One address (sm86Pair source sm86NoRegisters)))
      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
      (branch SM86BarrierSynchronize control . sm86NoRegisters)
      (branch SM86StoreGlobal address value offset control . (sm86Pair address (sm86One value sm86NoRegisters)))
      (branch SM86StoreGlobalWide address value offset control . (sm86Pair address (sm86Pair value sm86NoRegisters)))
      (branch SM86StoreGlobal64 address value offset control . (sm86Pair address (sm86Pair value sm86NoRegisters)))
      (branch SM86ReduceGlobalAddFloat32 address value offset control . (sm86Pair address (sm86One value sm86NoRegisters)))
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86One source sm86NoRegisters))
      (branch SM86Branch offset descriptor control . sm86NoRegisters)
      (branch SM86Exit control . sm86NoRegisters)))

def sm86WriteRegisters =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody
      (lambda unrestricted current : (family SM86InstructionBody) . (family StdList Nat))
      body
      (branch SM86MoveConstant destination bank offset control . (sm86One destination sm86NoRegisters))
      (branch SM86SpecialToRegister destination source control . (sm86One destination sm86NoRegisters))
      (branch SM86MoveImmediate destination immediate control . (sm86One destination sm86NoRegisters))
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (sm86One destination sm86NoRegisters))
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (sm86One destination sm86NoRegisters))
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (sm86Pair destination sm86NoRegisters))
      (branch SM86IntegerAddThreeImmediate destination left immediate control . (sm86One destination sm86NoRegisters))
      (branch SM86IntegerAddThreeRegister destination left right control . (sm86One destination sm86NoRegisters))
      (branch SM86ShiftRightImmediate destination source amount control . (sm86One destination sm86NoRegisters))
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (sm86One destination sm86NoRegisters))
      (branch SM86IntegerToFloat destination source control . (sm86One destination sm86NoRegisters))
      (branch SM86FloatAdd destination left right control . (sm86One destination sm86NoRegisters))
      (branch SM86FloatMultiply destination left right control . (sm86One destination sm86NoRegisters))
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (sm86One destination sm86NoRegisters))
      (branch SM86MultiFunctionUnitApproximation destination source operation control . (sm86One destination sm86NoRegisters))
      (branch SM86FloatMinimumOrMaximum destination left right mode control . (sm86One destination sm86NoRegisters))
      (branch SM86FloatNegate destination source control . (sm86One destination sm86NoRegisters))
      (branch SM86FloatPairToPackedHalfPair destination high low control . (sm86One destination sm86NoRegisters))
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (sm86One destination sm86NoRegisters))
      (branch SM86HalfToFloat destination source selector control . (sm86One destination sm86NoRegisters))
      (branch SM86BFloat16ToFloat destination source selector control . (sm86One destination sm86NoRegisters))
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86Quad destination sm86NoRegisters))
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86Quad destination sm86NoRegisters))
      (branch SM86LoadGlobal destination address offset control . (sm86One destination sm86NoRegisters))
      (branch SM86LoadGlobalWide destination address offset control . (sm86Pair destination sm86NoRegisters))
      (branch SM86WarpShuffle destination source lane segment mode control . (sm86One destination sm86NoRegisters))
      (branch SM86LoadShared destination address offset control . (sm86One destination sm86NoRegisters))
      (branch SM86LoadSharedMatrix destination address offset count transpose control .
        (sm86RegisterRun destination (sm86SharedMatrixRegisters count) sm86NoRegisters))
      (branch SM86StoreShared address value offset control . sm86NoRegisters)
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . sm86NoRegisters)
      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
      (branch SM86BarrierSynchronize control . sm86NoRegisters)
      (branch SM86StoreGlobal address value offset control . sm86NoRegisters)
      (branch SM86StoreGlobalWide address value offset control . sm86NoRegisters)
      (branch SM86StoreGlobal64 address value offset control . sm86NoRegisters)
      (branch SM86ReduceGlobalAddFloat32 address value offset control . sm86NoRegisters)
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . sm86NoRegisters)
      (branch SM86Branch offset descriptor control . sm86NoRegisters)
      (branch SM86Exit control . sm86NoRegisters)))

def sm86InstructionBodyOf =
  (lambda unrestricted instruction : (family SM86Instruction) .
    (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . (family SM86InstructionBody)) instruction
      (branch SM86InstructionValue guard body . body)))

-- one past the highest of the values, or start if that is higher
def sm86SpanOf =
  (lambda unrestricted values : (family StdList Nat) . (lambda unrestricted start : Nat .
    (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) values
      (branch StdListEmpty . start)
      (branch StdListCons head tail induction . (naturalSelect (naturalLess induction (succ head)) (succ head) induction)))))

-- one past the highest register the program names (0 for none)
def sm86RegisterSpan =
  (lambda unrestricted program : (family SM86Program) .
    (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . Nat) program
      (branch SM86ProgramEnd . 0)
      (branch SM86ProgramNext head tail induction .
        (sm86SpanOf (sm86ReadRegisters (sm86InstructionBodyOf head))
          (sm86SpanOf (sm86WriteRegisters (sm86InstructionBodyOf head)) induction)))))

-- the register count a launch of the program must declare
def sm86RegisterDemand =
  (lambda unrestricted program : (family SM86Program) .
    (naturalMultiply sm86RegisterGranule
      (naturalDivideUnchecked
        (naturalAdd (naturalAdd (sm86RegisterSpan program) sm86ReservedRegisters) (naturalSaturatingSubtract sm86RegisterGranule 1))
        sm86RegisterGranule)))

-- ---- control words, predicates as hazard keys, fixed latency ----

-- an instruction body's control word
def sm86BodyControlOf =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody
      (lambda unrestricted current : (family SM86InstructionBody) . (family SM86Control))
      body
      (branch SM86MoveConstant destination bank offset control . control)
      (branch SM86SpecialToRegister destination source control . control)
      (branch SM86MoveImmediate destination immediate control . control)
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . control)
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . control)
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . control)
      (branch SM86IntegerAddThreeImmediate destination left immediate control . control)
      (branch SM86IntegerAddThreeRegister destination left right control . control)
      (branch SM86ShiftRightImmediate destination source amount control . control)
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . control)
      (branch SM86IntegerToFloat destination source control . control)
      (branch SM86FloatAdd destination left right control . control)
      (branch SM86FloatMultiply destination left right control . control)
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . control)
      (branch SM86MultiFunctionUnitApproximation destination source operation control . control)
      (branch SM86FloatMinimumOrMaximum destination left right mode control . control)
      (branch SM86FloatNegate destination source control . control)
      (branch SM86FloatPairToPackedHalfPair destination high low control . control)
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . control)
      (branch SM86HalfToFloat destination source selector control . control)
      (branch SM86BFloat16ToFloat destination source selector control . control)
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . control)
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . control)
      (branch SM86LoadGlobal destination address offset control . control)
      (branch SM86LoadGlobalWide destination address offset control . control)
      (branch SM86WarpShuffle destination source lane segment mode control . control)
      (branch SM86LoadShared destination address offset control . control)
      (branch SM86LoadSharedMatrix destination address offset count transpose control . control)
      (branch SM86StoreShared address value offset control . control)
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . control)
      (branch SM86CommitAsyncGroup control . control)
      (branch SM86WaitAsyncGroups count control . control)
      (branch SM86BarrierSynchronize control . control)
      (branch SM86StoreGlobal address value offset control . control)
      (branch SM86StoreGlobalWide address value offset control . control)
      (branch SM86StoreGlobal64 address value offset control . control)
      (branch SM86ReduceGlobalAddFloat32 address value offset control . control)
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . control)
      (branch SM86Branch offset descriptor control . control)
      (branch SM86Exit control . control)))

-- the body with another control word
def sm86BodyWithControl =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (lambda unrestricted replacement : (family SM86Control) .
      (eliminate SM86InstructionBody
        (lambda unrestricted current : (family SM86InstructionBody) . (family SM86InstructionBody))
        body
      (branch SM86MoveConstant destination bank offset control . (constructor SM86InstructionBody SM86MoveConstant destination bank offset replacement))
      (branch SM86SpecialToRegister destination source control . (constructor SM86InstructionBody SM86SpecialToRegister destination source replacement))
      (branch SM86MoveImmediate destination immediate control . (constructor SM86InstructionBody SM86MoveImmediate destination immediate replacement))
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddConstant destination left bank offset addend replacement))
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate destination left immediate addend replacement))
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant destination left right bank offset replacement))
      (branch SM86IntegerAddThreeImmediate destination left immediate control . (constructor SM86InstructionBody SM86IntegerAddThreeImmediate destination left immediate replacement))
      (branch SM86IntegerAddThreeRegister destination left right control . (constructor SM86InstructionBody SM86IntegerAddThreeRegister destination left right replacement))
      (branch SM86ShiftRightImmediate destination source amount control . (constructor SM86InstructionBody SM86ShiftRightImmediate destination source amount replacement))
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (constructor SM86InstructionBody SM86LogicThreeInputTruthTable destination left right truthTable replacement))
      (branch SM86IntegerToFloat destination source control . (constructor SM86InstructionBody SM86IntegerToFloat destination source replacement))
      (branch SM86FloatAdd destination left right control . (constructor SM86InstructionBody SM86FloatAdd destination left right replacement))
      (branch SM86FloatMultiply destination left right control . (constructor SM86InstructionBody SM86FloatMultiply destination left right replacement))
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd destination left right addend replacement))
      (branch SM86MultiFunctionUnitApproximation destination source operation control . (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation destination source operation replacement))
      (branch SM86FloatMinimumOrMaximum destination left right mode control . (constructor SM86InstructionBody SM86FloatMinimumOrMaximum destination left right mode replacement))
      (branch SM86FloatNegate destination source control . (constructor SM86InstructionBody SM86FloatNegate destination source replacement))
      (branch SM86FloatPairToPackedHalfPair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedHalfPair destination high low replacement))
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedBFloat16Pair destination high low replacement))
      (branch SM86HalfToFloat destination source selector control . (constructor SM86InstructionBody SM86HalfToFloat destination source selector replacement))
      (branch SM86BFloat16ToFloat destination source selector control . (constructor SM86InstructionBody SM86BFloat16ToFloat destination source selector replacement))
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator replacement))
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator replacement))
      (branch SM86LoadGlobal destination address offset control . (constructor SM86InstructionBody SM86LoadGlobal destination address offset replacement))
      (branch SM86LoadGlobalWide destination address offset control . (constructor SM86InstructionBody SM86LoadGlobalWide destination address offset replacement))
      (branch SM86WarpShuffle destination source lane segment mode control . (constructor SM86InstructionBody SM86WarpShuffle destination source lane segment mode replacement))
      (branch SM86LoadShared destination address offset control . (constructor SM86InstructionBody SM86LoadShared destination address offset replacement))
      (branch SM86LoadSharedMatrix destination address offset count transpose control . (constructor SM86InstructionBody SM86LoadSharedMatrix destination address offset count transpose replacement))
      (branch SM86StoreShared address value offset control . (constructor SM86InstructionBody SM86StoreShared address value offset replacement))
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (constructor SM86InstructionBody SM86LoadGlobalToShared address offset source sourceOffset replacement))
      (branch SM86CommitAsyncGroup control . (constructor SM86InstructionBody SM86CommitAsyncGroup replacement))
      (branch SM86WaitAsyncGroups count control . (constructor SM86InstructionBody SM86WaitAsyncGroups count replacement))
      (branch SM86BarrierSynchronize control . (constructor SM86InstructionBody SM86BarrierSynchronize replacement))
      (branch SM86StoreGlobal address value offset control . (constructor SM86InstructionBody SM86StoreGlobal address value offset replacement))
      (branch SM86StoreGlobalWide address value offset control . (constructor SM86InstructionBody SM86StoreGlobalWide address value offset replacement))
      (branch SM86StoreGlobal64 address value offset control . (constructor SM86InstructionBody SM86StoreGlobal64 address value offset replacement))
      (branch SM86ReduceGlobalAddFloat32 address value offset control . (constructor SM86InstructionBody SM86ReduceGlobalAddFloat32 address value offset replacement))
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate predicate source immediate replacement))
      (branch SM86Branch offset descriptor control . (constructor SM86InstructionBody SM86Branch offset descriptor replacement))
      (branch SM86Exit control . (constructor SM86InstructionBody SM86Exit replacement)))))

def sm86ControlStallOf =
  (lambda unrestricted control : (family SM86Control) .
    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . Nat) control
      (branch SM86ControlValue stall yield write read wait reuse . (byte-to-nat stall))))

def sm86ControlWithStall =
  (lambda unrestricted control : (family SM86Control) . (lambda unrestricted stall : Nat .
    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family SM86Control)) control
      (branch SM86ControlValue old yield write read wait reuse .
        (constructor SM86Control SM86ControlValue (nat-to-byte stall) yield write read wait reuse)))))

-- A predicate as a hazard key beside the registers: 256 + its index (P0 ..
-- P6; PT, which reads true and absorbs writes, is none).
def sm86PredicateKeys =
  (lambda unrestricted predicate : (family SM86Predicate) .
    (eliminate SM86Predicate (lambda unrestricted current : (family SM86Predicate) . (family StdList Nat)) predicate
      (branch SM86Predicate0 . (constructor StdList StdListCons Nat 256 sm86NoRegisters))
      (branch SM86Predicate1 . (constructor StdList StdListCons Nat 257 sm86NoRegisters))
      (branch SM86Predicate2 . (constructor StdList StdListCons Nat 258 sm86NoRegisters))
      (branch SM86Predicate3 . (constructor StdList StdListCons Nat 259 sm86NoRegisters))
      (branch SM86Predicate4 . (constructor StdList StdListCons Nat 260 sm86NoRegisters))
      (branch SM86Predicate5 . (constructor StdList StdListCons Nat 261 sm86NoRegisters))
      (branch SM86Predicate6 . (constructor StdList StdListCons Nat 262 sm86NoRegisters))
      (branch SM86PredicateTrue . sm86NoRegisters)))

-- the predicate an instruction's guard reads
def sm86GuardKeys =
  (lambda unrestricted instruction : (family SM86Instruction) .
    (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . (family StdList Nat)) instruction
      (branch SM86InstructionValue guard body .
        (eliminate SM86InstructionGuard (lambda unrestricted current : (family SM86InstructionGuard) . (family StdList Nat)) guard
          (branch SM86InstructionAlways . sm86NoRegisters)
          (branch SM86InstructionWhen predicate . (sm86PredicateKeys predicate))
          (branch SM86InstructionWhenNot predicate . (sm86PredicateKeys predicate))))))

-- the predicate a body writes
def sm86PredicateWriteKeys =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . (family StdList Nat)) body
      (branch SM86MoveConstant destination bank offset control . sm86NoRegisters)
      (branch SM86SpecialToRegister destination source control . sm86NoRegisters)
      (branch SM86MoveImmediate destination immediate control . sm86NoRegisters)
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . sm86NoRegisters)
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . sm86NoRegisters)
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . sm86NoRegisters)
      (branch SM86IntegerAddThreeImmediate destination left immediate control . sm86NoRegisters)
      (branch SM86IntegerAddThreeRegister destination left right control . sm86NoRegisters)
      (branch SM86ShiftRightImmediate destination source amount control . sm86NoRegisters)
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . sm86NoRegisters)
      (branch SM86IntegerToFloat destination source control . sm86NoRegisters)
      (branch SM86FloatAdd destination left right control . sm86NoRegisters)
      (branch SM86FloatMultiply destination left right control . sm86NoRegisters)
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . sm86NoRegisters)
      (branch SM86MultiFunctionUnitApproximation destination source operation control . sm86NoRegisters)
      (branch SM86FloatMinimumOrMaximum destination left right mode control . sm86NoRegisters)
      (branch SM86FloatNegate destination source control . sm86NoRegisters)
      (branch SM86FloatPairToPackedHalfPair destination high low control . sm86NoRegisters)
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . sm86NoRegisters)
      (branch SM86HalfToFloat destination source selector control . sm86NoRegisters)
      (branch SM86BFloat16ToFloat destination source selector control . sm86NoRegisters)
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . sm86NoRegisters)
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . sm86NoRegisters)
      (branch SM86LoadGlobal destination address offset control . sm86NoRegisters)
      (branch SM86LoadGlobalWide destination address offset control . sm86NoRegisters)
      (branch SM86WarpShuffle destination source lane segment mode control . sm86NoRegisters)
      (branch SM86LoadShared destination address offset control . sm86NoRegisters)
      (branch SM86LoadSharedMatrix destination address offset count transpose control . sm86NoRegisters)
      (branch SM86StoreShared address value offset control . sm86NoRegisters)
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . sm86NoRegisters)
      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
      (branch SM86BarrierSynchronize control . sm86NoRegisters)
      (branch SM86StoreGlobal address value offset control . sm86NoRegisters)
      (branch SM86StoreGlobalWide address value offset control . sm86NoRegisters)
      (branch SM86StoreGlobal64 address value offset control . sm86NoRegisters)
      (branch SM86ReduceGlobalAddFloat32 address value offset control . sm86NoRegisters)
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86PredicateKeys predicate))
      (branch SM86Branch offset descriptor control . sm86NoRegisters)
      (branch SM86Exit control . sm86NoRegisters)))

-- ASSUMED, and stated as an assumption: the cycles after issue before a
-- fixed-latency form's destination (register or predicate) may be read --
-- 6 for every such form, above the 4 published for Ampere's FP32 and
-- integer pipes.  Variable-latency forms (loads, S2R, SHFL, MUFU, HMMA)
-- deliver through a scoreboard barrier instead, and forms with no
-- destination deliver nothing (0).  A program accepted under this table
-- that a card computes wrongly refutes it: silicon runs of stall-compacted
-- programs are its evidence.
def sm86FixedLatencyCycles : Nat = 6

-- HMMA.16816.F32: a fixed-latency result, as ptxas schedules it for sm_86
-- (no scoreboard; a dependent HMMA 24 cycles after its producer, a store
-- of the result 23 -- nvdisasm -hex of a dependent mma.sync chain on the
-- DGX Spark, 2026-09-26; sm_121's is 29, Accelerator.SM121.Lowering's
-- tensor class).  Its sources are read at issue.  An HMMA that declares a
-- write barrier is ordered by it instead (the older products do).
def sm86TensorLatencyCycles : Nat = 24

-- 1 when a control word declares a write barrier
def sm86ControlWritesBarrier =
  (lambda unrestricted control : (family SM86Control) .
    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . Nat) control
      (branch SM86ControlValue stall yield write read wait reuse .
        (eliminate SM86Barrier (lambda unrestricted current : (family SM86Barrier) . Nat) write
          (branch SM86Barrier0 . 1) (branch SM86Barrier1 . 1) (branch SM86Barrier2 . 1) (branch SM86Barrier3 . 1)
          (branch SM86Barrier4 . 1) (branch SM86Barrier5 . 1) (branch SM86Barrier6 . 1) (branch SM86BarrierNone . 0)))))

def sm86FixedLatency =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . Nat) body
      (branch SM86MoveConstant destination bank offset control . sm86FixedLatencyCycles)
      (branch SM86SpecialToRegister destination source control . 0)
      (branch SM86MoveImmediate destination immediate control . sm86FixedLatencyCycles)
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . sm86FixedLatencyCycles)
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . sm86FixedLatencyCycles)
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . sm86FixedLatencyCycles)
      (branch SM86IntegerAddThreeImmediate destination left immediate control . sm86FixedLatencyCycles)
      (branch SM86IntegerAddThreeRegister destination left right control . sm86FixedLatencyCycles)
      (branch SM86ShiftRightImmediate destination source amount control . sm86FixedLatencyCycles)
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . sm86FixedLatencyCycles)
      (branch SM86IntegerToFloat destination source control . sm86FixedLatencyCycles)
      (branch SM86FloatAdd destination left right control . sm86FixedLatencyCycles)
      (branch SM86FloatMultiply destination left right control . sm86FixedLatencyCycles)
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . sm86FixedLatencyCycles)
      (branch SM86MultiFunctionUnitApproximation destination source operation control . 0)
      (branch SM86FloatMinimumOrMaximum destination left right mode control . sm86FixedLatencyCycles)
      (branch SM86FloatNegate destination source control . sm86FixedLatencyCycles)
      (branch SM86FloatPairToPackedHalfPair destination high low control . sm86FixedLatencyCycles)
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . sm86FixedLatencyCycles)
      (branch SM86HalfToFloat destination source selector control . sm86FixedLatencyCycles)
      (branch SM86BFloat16ToFloat destination source selector control . sm86FixedLatencyCycles)
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
        (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles))
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
        (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles))
      (branch SM86LoadGlobal destination address offset control . 0)
      (branch SM86LoadGlobalWide destination address offset control . 0)
      (branch SM86WarpShuffle destination source lane segment mode control . 0)
      (branch SM86LoadShared destination address offset control . 0)
      (branch SM86LoadSharedMatrix destination address offset count transpose control . 0)
      (branch SM86StoreShared address value offset control . 0)
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 0)
      (branch SM86CommitAsyncGroup control . 0)
      (branch SM86WaitAsyncGroups count control . 0)
      (branch SM86BarrierSynchronize control . 0)
      (branch SM86StoreGlobal address value offset control . 0)
      (branch SM86StoreGlobalWide address value offset control . 0)
      (branch SM86StoreGlobal64 address value offset control . 0)
      (branch SM86ReduceGlobalAddFloat32 address value offset control . 0)
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . sm86FixedLatencyCycles)
      (branch SM86Branch offset descriptor control . 0)
      (branch SM86Exit control . 0)))

-- The fewest cycles an instruction must stall before the next issues, from
-- its own issue rather than a result: 1, except BAR.SYNC.DEFER_BLOCKING
-- (6) and an HMMA ordered by its fixed latency (8).  ptxas always gives
-- the barrier 6 (sm_86 and sm_121, every bar.sync read off nvdisasm -hex on
-- the DGX Spark, 2026-09-26).  With 1 the GB10 let a warp's
-- shared-matrix load right after the barrier read, now and then, what
-- another warp had stored before it: the tiled product's last k-step (its
-- loads follow the barrier directly) read the buffer's previous tile.
def sm86BarrierSynchronizeStall : Nat = 6
-- ptxas gives DEPBAR.LE SB0, n (cp.async.wait_group) 4 on sm_86 and sm_121
-- (every wait read off nvdisasm -hex on the DGX Spark, 2026-09-26, research
-- p4-hmma/cp_async*.cu); the realization keeps it.
def sm86WaitAsyncGroupsStall : Nat = 4
-- ptxas never issues an HMMA.16816 within 8 cycles of the one before on
-- sm_86 (16 on sm_121: the tensor pipe's rate); the model asks every
-- instruction after an HMMA to wait 8, which is stricter (ptxas fills the gap
-- with other work) and puts a product's dependent, however few products
-- apart, past sm86TensorLatencyCycles.
def sm86TensorIssueStall : Nat = 8
def sm86MinimumStall =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . Nat) body
      (branch SM86MoveConstant destination bank offset control . 1)
      (branch SM86SpecialToRegister destination source control . 1)
      (branch SM86MoveImmediate destination immediate control . 1)
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . 1)
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . 1)
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . 1)
      (branch SM86IntegerAddThreeImmediate destination left immediate control . 1)
      (branch SM86IntegerAddThreeRegister destination left right control . 1)
      (branch SM86ShiftRightImmediate destination source amount control . 1)
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . 1)
      (branch SM86IntegerToFloat destination source control . 1)
      (branch SM86FloatAdd destination left right control . 1)
      (branch SM86FloatMultiply destination left right control . 1)
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . 1)
      (branch SM86MultiFunctionUnitApproximation destination source operation control . 1)
      (branch SM86FloatMinimumOrMaximum destination left right mode control . 1)
      (branch SM86FloatNegate destination source control . 1)
      (branch SM86FloatPairToPackedHalfPair destination high low control . 1)
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . 1)
      (branch SM86HalfToFloat destination source selector control . 1)
      (branch SM86BFloat16ToFloat destination source selector control . 1)
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
        (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall))
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
        (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall))
      (branch SM86LoadGlobal destination address offset control . 1)
      (branch SM86LoadGlobalWide destination address offset control . 1)
      (branch SM86WarpShuffle destination source lane segment mode control . 1)
      (branch SM86LoadShared destination address offset control . 1)
      (branch SM86LoadSharedMatrix destination address offset count transpose control . 1)
      (branch SM86StoreShared address value offset control . 1)
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 1)
      (branch SM86CommitAsyncGroup control . 1)
      (branch SM86WaitAsyncGroups count control . sm86WaitAsyncGroupsStall)
      (branch SM86BarrierSynchronize control . sm86BarrierSynchronizeStall)
      (branch SM86StoreGlobal address value offset control . 1)
      (branch SM86StoreGlobalWide address value offset control . 1)
      (branch SM86StoreGlobal64 address value offset control . 1)
      (branch SM86ReduceGlobalAddFloat32 address value offset control . 1)
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . 1)
      (branch SM86Branch offset descriptor control . 1)
      (branch SM86Exit control . 1)))

-- A scoreboard barrier as a hazard key: 300 + its number (SB0 .. SB5).  An
-- instruction that sets one (write or read barrier) makes it pending
-- sm86BarrierSetCycles after issue -- ASSUMED, like the table above: a
-- waiter issued sooner could miss it -- and an instruction whose wait mask
-- names it reads it.
def sm86BarrierSetCycles : Nat = 2

def sm86BarrierKeys =
  (lambda unrestricted barrier : (family SM86Barrier) .
    (eliminate SM86Barrier (lambda unrestricted current : (family SM86Barrier) . (family StdList Nat)) barrier
      (branch SM86Barrier0 . (constructor StdList StdListCons Nat 300 sm86NoRegisters))
      (branch SM86Barrier1 . (constructor StdList StdListCons Nat 301 sm86NoRegisters))
      (branch SM86Barrier2 . (constructor StdList StdListCons Nat 302 sm86NoRegisters))
      (branch SM86Barrier3 . (constructor StdList StdListCons Nat 303 sm86NoRegisters))
      (branch SM86Barrier4 . (constructor StdList StdListCons Nat 304 sm86NoRegisters))
      (branch SM86Barrier5 . (constructor StdList StdListCons Nat 305 sm86NoRegisters))
      (branch SM86Barrier6 . (constructor StdList StdListCons Nat 306 sm86NoRegisters))
      (branch SM86BarrierNone . sm86NoRegisters)))

-- the barriers a control word sets
def sm86ControlSetKeys =
  (lambda unrestricted control : (family SM86Control) .
    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family StdList Nat)) control
      (branch SM86ControlValue stall yield write read wait reuse .
        (stdListAppend Nat (sm86BarrierKeys write) (sm86BarrierKeys read)))))

-- the barriers a control word's wait mask names (bit b: SB b)
def sm86ControlWaitKeys =
  (lambda unrestricted control : (family SM86Control) .
    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family StdList Nat)) control
      (branch SM86ControlValue stall yield write read wait reuse .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family StdList Nat))
          sm86NoRegisters
          (lambda unrestricted bit : Nat . (lambda unrestricted induction : (family StdList Nat) .
            (nat-eliminate
              (lambda unrestricted current : Nat . (family StdList Nat))
              induction
              (lambda unrestricted set : Nat . (lambda unrestricted ignored : (family StdList Nat) .
                (constructor StdList StdListCons Nat (naturalAdd 300 bit) induction)))
              (nat-modulo (nat-divide (byte-to-nat wait) (naturalPowerOfTwo bit)) 2))))
          6))))


def sm86OpSummaryMake =
  (lambda unrestricted reads : (family StdList Nat) .
    (lambda unrestricted writes : (family StdList Nat) .
      (lambda unrestricted predicateWrites : (family StdList Nat) .
        (lambda unrestricted variable : Nat .
          (lambda unrestricted latency : Nat .
            (lambda unrestricted minimum : Nat .
            (lambda unrestricted control : (family SM86Control) .
              (constructor SM86OpSummary SM86OpSummaryValue
                reads writes predicateWrites
                (sm86ControlWaitKeys control) (sm86ControlSetKeys control)
                (sm86ControlStallOf control) latency variable minimum control))))))))

def sm86OpSummaryOfBody =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody
      (lambda unrestricted current : (family SM86InstructionBody) . (family SM86OpSummary))
      body
      (branch SM86MoveConstant destination bank offset control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86SpecialToRegister destination source control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
      (branch SM86MoveImmediate destination immediate control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (sm86OpSummaryMake (sm86One left (sm86One addend sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (sm86OpSummaryMake (sm86One left (sm86One addend sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (sm86OpSummaryMake (sm86One left (sm86Pair right sm86NoRegisters)) (sm86Pair destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86IntegerAddThreeImmediate destination left immediate control . (sm86OpSummaryMake (sm86One left sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86IntegerAddThreeRegister destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86ShiftRightImmediate destination source amount control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86IntegerToFloat destination source control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86FloatAdd destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86FloatMultiply destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (sm86OpSummaryMake (sm86One left (sm86One right (sm86One addend sm86NoRegisters))) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86MultiFunctionUnitApproximation destination source operation control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
      (branch SM86FloatMinimumOrMaximum destination left right mode control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86FloatNegate destination source control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86FloatPairToPackedHalfPair destination high low control . (sm86OpSummaryMake (sm86One high (sm86One low sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (sm86OpSummaryMake (sm86One high (sm86One low sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86HalfToFloat destination source selector control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86BFloat16ToFloat destination source selector control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86OpSummaryMake (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))) (sm86Quad destination sm86NoRegisters) sm86NoRegisters 0 (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles) (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall) control))
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86OpSummaryMake (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))) (sm86Quad destination sm86NoRegisters) sm86NoRegisters 0 (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles) (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall) control))
      (branch SM86LoadGlobal destination address offset control . (sm86OpSummaryMake (sm86Pair address sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
      (branch SM86LoadGlobalWide destination address offset control . (sm86OpSummaryMake (sm86Pair address sm86NoRegisters) (sm86Pair destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
      (branch SM86WarpShuffle destination source lane segment mode control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
      (branch SM86LoadShared destination address offset control . (sm86OpSummaryMake (sm86One address sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
      (branch SM86LoadSharedMatrix destination address offset count transpose control . (sm86OpSummaryMake (sm86One address sm86NoRegisters) (sm86RegisterRun destination (sm86SharedMatrixRegisters count) sm86NoRegisters) sm86NoRegisters 1 0 1 control))
      (branch SM86StoreShared address value offset control . (sm86OpSummaryMake (sm86One address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (sm86OpSummaryMake (sm86One address (sm86Pair source sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
      (branch SM86CommitAsyncGroup control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))
      (branch SM86WaitAsyncGroups count control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 sm86WaitAsyncGroupsStall control))
      (branch SM86BarrierSynchronize control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 sm86BarrierSynchronizeStall control))
      (branch SM86StoreGlobal address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
      (branch SM86StoreGlobalWide address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86Pair value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
      (branch SM86StoreGlobal64 address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86Pair value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
      (branch SM86ReduceGlobalAddFloat32 address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) sm86NoRegisters (sm86PredicateKeys predicate) 0 sm86FixedLatencyCycles 1 control))
      (branch SM86Branch offset descriptor control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))
      (branch SM86Exit control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))))