module Realization.Nvidia.SM86.LinearStepSM86

import Accelerator.SM86.Control
import Accelerator.SM86.Immediate
import Accelerator.SM86.Instruction
import Accelerator.SM86.InstructionEncoding
import Accelerator.SM86.Operands
import Accelerator.SM86.Types
import Std.Natural

-- The SM86 realization of Learning.Checked.LinearStep for outputs 2, inputs
-- 2: one thread of one block does the whole step in the semantic program's
-- exact operation order (fused multiply-adds first element innermost,
-- subtraction as addition of a negation, the loss as 0.5 x a fused sum of
-- squares, the update as fma(dW, -eta, W)); every other lane exits at once.
--
-- Preconditions (Realization contract):
--   outputs = 2, inputs = 2 (the register plan is for this shape);
--   one launch of one block, block width 32 (a single warp);
--   the parameter block carries, at the offsets below, the 64-bit addresses
--   of W (row-major, 16 bytes), x (8 bytes), t (8 bytes) and the 44-byte
--   output record (y 8, loss 4, dW 16, W' 16), and eta at 0x190;
--   the arena regions those addresses name are disjoint and 4-aligned.
--
-- Numerical contract: identical to the semantic program's (fused, ordered);
-- reproducibility: bitwise on any SM86 device for this realization, which
-- uses no reduction across lanes and no approximate unit.

def linearStepSM86Identity : Bytes = b"linear-step-sm86-outputs2-inputs2-v1"

def linearStepSM86Outputs : Nat = 2
def linearStepSM86Inputs : Nat = 2
def linearStepSM86BlockWidth : Nat = 32
def linearStepSM86OutputRecordBytes : Nat = 44

-- parameter-block offsets (bytes into c[0])
def linearStepSM86WeightsOffset : Nat = 352
def linearStepSM86InputOffset : Nat = 360
def linearStepSM86TargetOffset : Nat = 368
def linearStepSM86OutputOffset : Nat = 376
def linearStepSM86LearningRateOffset : Nat = 400

def lsR = (lambda unrestricted index : Nat . (sm86Register (nat-to-byte index)))
def lsU = sm86Unsigned32FromNaturalTruncated

-- Controls.  Fixed-latency forms: stall 15 with no scoreboard use, the
-- over-stall control the momentum realization proved on the 3070 for a
-- dependent FFMA chain.  Variable-latency forms (S2R, LDG) name a write
-- barrier and their first consumer waits on it: S2R on SB0, waited by the
-- ISETP; every LDG on SB1, waited by the first FFMA.  Without the waits the
-- consumers read the registers' previous contents -- the RTX 3090 returned a
-- record of zeros for the first version of this program (2026-09-22), and
-- SM86.Scoreboard now refuses it at the checker.
def lsControlWith =
  (lambda unrestricted write : (family SM86Barrier) . (lambda unrestricted wait : Nat .
    (constructor SM86Control SM86ControlValue
      (byte 15)
      (constructor SM86YieldMode SM86Continue)
      write
      (constructor SM86Barrier SM86BarrierNone)
      (nat-to-byte wait)
      (byte 0))))

def lsControl : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86BarrierNone) 0)
def lsControlSetSB0 : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86Barrier0) 0)
def lsControlSetSB1 : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86Barrier1) 0)
def lsControlWaitSB0 : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86BarrierNone) 1)
def lsControlWaitSB1 : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86BarrierNone) 2)

def lsNext =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (lambda unrestricted tail : (family SM86Program) .
      (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail)))

def lsConstant =
  (lambda unrestricted destination : Nat . (lambda unrestricted offset : Nat .
    (constructor SM86InstructionBody SM86MoveConstant (lsR destination) (byte 0) (lsU offset) lsControl)))

def lsLoad =
  (lambda unrestricted destination : Nat . (lambda unrestricted address : Nat . (lambda unrestricted offset : Nat .
    (constructor SM86InstructionBody SM86LoadGlobal (lsR destination) (lsR address) (lsU offset) lsControlSetSB1))))

def lsStore =
  (lambda unrestricted address : Nat . (lambda unrestricted value : Nat . (lambda unrestricted offset : Nat .
    (constructor SM86InstructionBody SM86StoreGlobal (lsR address) (lsR value) (lsU offset) lsControl))))

def lsZero =
  (lambda unrestricted destination : Nat .
    (constructor SM86InstructionBody SM86MoveImmediate (lsR destination) sm86Unsigned32Zero lsControl))

def lsFusedWith =
  (lambda unrestricted control : (family SM86Control) .
  (lambda unrestricted destination : Nat . (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (lambda unrestricted addend : Nat .
    (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd (lsR destination) (lsR left) (lsR right) (lsR addend) control))))))

def lsFused = (lsFusedWith lsControl)

def lsMultiply =
  (lambda unrestricted destination : Nat . (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
    (constructor SM86InstructionBody SM86FloatMultiply (lsR destination) (lsR left) (lsR right) lsControl))))

def lsAdd =
  (lambda unrestricted destination : Nat . (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
    (constructor SM86InstructionBody SM86FloatAdd (lsR destination) (lsR left) (lsR right) lsControl))))

def lsNegate =
  (lambda unrestricted destination : Nat . (lambda unrestricted source : Nat .
    (constructor SM86InstructionBody SM86FloatNegate (lsR destination) (lsR source) lsControl)))

-- ---- the program, for any shape ----
-- Registers, for outputs m and inputs k: R0 tid; R2:R3 &W; R4:R5 &x; R6:R7
-- &t; R8:R9 &out; R10 eta; then x (k), t (m), W (m x k), y (m), d (m), loss,
-- 0.5, dW (m x k), -eta, W' (m x k), consecutively from R12 -- for 2 x 2:
-- R12,R13 x; R14,R15 t; R16..R19 W; R20,R21 y; R22,R23 d; R24 loss; R25 0.5;
-- R26..R29 dW; R30 -eta; R31..R34 W', the plan the RTX 3090 ran.  The
-- program is generated from the shape; every loop below is unrolled, in the
-- semantic program's order (fma chains first element innermost).
def lsBase : Nat = 12
def lsRegX = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted j : Nat . (naturalAdd lsBase j))))
def lsRegT = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (naturalAdd lsBase (naturalAdd k i)))))
def lsRegW =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
    (naturalAdd lsBase (naturalAdd k (naturalAdd m (naturalAdd (naturalMultiply i k) j))))))))
def lsRegY = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (naturalAdd (lsRegW k m m 0) i))))
def lsRegD = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (naturalAdd (lsRegY k m m) i))))
def lsRegLoss = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lsRegD k m m)))
def lsRegHalf = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (naturalAdd (lsRegLoss k m) 1)))
def lsRegDW =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
    (naturalAdd (lsRegHalf k m) (naturalAdd 1 (naturalAdd (naturalMultiply i k) j)))))))
def lsRegNegEta = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lsRegDW k m m 0)))
def lsRegWp =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
    (naturalAdd (lsRegNegEta k m) (naturalAdd 1 (naturalAdd (naturalMultiply i k) j)))))))
-- one past the last register the allocation names (the end of W'):
-- 15 + k + 3m + 3mk
def linearStepSM86RegisterSpanFor =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat . (lsRegWp k m m 0)))
-- The shapes the generator realizes: at least one output and one input, and
-- the allocation within the register file (Accelerator.SM86.Operands).
-- Past it the byte register indices would wrap -- a 9 x 9 step would name
-- R293 as R37, on top of W -- so every artifact gates on this.  240 shapes,
-- 38 x 1 .. 1 x 57 (Proof.LinearStepRegisterPlan).
def linearStepSM86ShapeAdmitted =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
    (naturalAnd (naturalNonzero m) (naturalAnd (naturalNonzero k) (sm86RegisterSpanAdmitted (linearStepSM86RegisterSpanFor m k))))))
-- the output record: y (4m), loss (4), dW (4mk), W' (4mk)
def linearStepSM86OutputRecordBytesFor =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
    (naturalAdd (naturalMultiply 4 m) (naturalAdd 4 (naturalMultiply 8 (naturalMultiply m k))))))
def lsLossOffset = (lambda unrestricted m : Nat . (naturalMultiply 4 m))
def lsGradientOffset = (lambda unrestricted m : Nat . (lambda unrestricted k : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
  (naturalAdd (naturalMultiply 4 m) (naturalAdd 4 (naturalMultiply 4 (naturalAdd (naturalMultiply i k) j))))))))
def lsUpdatedOffset = (lambda unrestricted m : Nat . (lambda unrestricted k : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
  (naturalAdd (lsGradientOffset m k i j) (naturalMultiply 4 (naturalMultiply m k)))))))

-- an unrolled loop: body 0 (body 1 (... body (count-1) tail))
def lsFor =
  (lambda unrestricted count : Nat .
    (lambda unrestricted body : (pi unrestricted index : Nat . (pi unrestricted rest : (family SM86Program) . (family SM86Program))) .
      (lambda unrestricted tail : (family SM86Program) .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family SM86Program))
          tail
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SM86Program) .
            (body (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) predecessor) induction)))
          count))))

-- the first fused multiply-add waits on the loads' barrier
def lsFirstFusedControl =
  (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family SM86Control))
      lsControl
      (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family SM86Control) . lsControlWaitSB1))
      (naturalAnd (naturalIsZero i) (naturalIsZero j)))))

-- The program as named blocks and named loop bodies, each prepending its
-- instructions to what follows, so a statement about the program is a
-- statement about its parts (Proof.LinearStepGeneratorForall): the
-- prologue, the loads, y, d, the loss, dW, W', Exit.

-- tid, the lane guard, the nine parameter words (4 addresses, eta)
def lsPrologue =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
    (lsNext (constructor SM86InstructionBody SM86SpecialToRegister (lsR 0) (constructor SM86SpecialRegister SM86ThreadIdX) lsControlSetSB0)
    (lsNext (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate (constructor SM86Predicate SM86Predicate0) (lsR 0) sm86Unsigned32Zero lsControlWaitSB0)
    (constructor SM86Program SM86ProgramNext (sm86PredicatedInstruction (constructor SM86Predicate SM86Predicate0) (constructor SM86InstructionBody SM86Exit lsControl))
    (lsNext (lsConstant 2 352)
    (lsNext (lsConstant 3 356)
    (lsNext (lsConstant 4 360)
    (lsNext (lsConstant 5 364)
    (lsNext (lsConstant 6 368)
    (lsNext (lsConstant 7 372)
    (lsNext (lsConstant 8 376)
    (lsNext (lsConstant 9 380)
    (lsNext (lsConstant 10 400)
      tail)))))))))))))))

-- the loads: x (k), t (m), W (m rows of k)
def lsLoadXBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) . (lsNext (lsLoad (lsRegX k m j) 4 (naturalMultiply 4 j)) rest)))))
def lsLoadTBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsNext (lsLoad (lsRegT k m i) 6 (naturalMultiply 4 i)) rest)))))
def lsLoadWRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsLoad (lsRegW k m i j) 2 (naturalMultiply 4 (naturalAdd (naturalMultiply i k) j))) rest))))))
def lsLoadWBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsLoadWRow k m i) rest)))))
def lsLoads =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
    (lsFor k (lsLoadXBody k m) (lsFor m (lsLoadTBody k m) (lsFor m (lsLoadWBody k m) tail))))))

-- y_i = fma(W_i(k-1), x_(k-1), ... fma(W_i0, x_0, +0.0)), then stored
def lsOutputRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsFusedWith (lsFirstFusedControl i j) (lsRegY k m i) (lsRegW k m i j) (lsRegX k m j) (lsRegY k m i)) rest))))))
def lsOutputBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsZero (lsRegY k m i)) (lsFor k (lsOutputRow k m i) rest))))))
def lsStoreYBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsNext (lsStore 8 (lsRegY k m i) (naturalMultiply 4 i)) rest)))))
def lsOutputs =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
    (lsFor m (lsOutputBody k m) (lsFor m (lsStoreYBody k m) tail)))))

-- d_i = y_i + (-t_i)
def lsResidualBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsNegate (lsRegD k m i) (lsRegT k m i)) (lsNext (lsAdd (lsRegD k m i) (lsRegY k m i) (lsRegD k m i)) rest))))))
def lsResiduals =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
    (lsFor m (lsResidualBody k m) tail))))

-- loss = 0.5 x fma(d_(m-1), d_(m-1), ... fma(d_0, d_0, +0.0)), then stored
def lsLossBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsFused (lsRegLoss k m) (lsRegD k m i) (lsRegD k m i) (lsRegLoss k m)) rest)))))
def lsLossTail = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
  (lsNext (constructor SM86InstructionBody SM86MoveImmediate (lsR (lsRegHalf k m)) (lsU 1056964608) lsControl)
  (lsNext (lsMultiply (lsRegLoss k m) (lsRegHalf k m) (lsRegLoss k m))
  (lsNext (lsStore 8 (lsRegLoss k m) (lsLossOffset m))
    tail))))))
def lsLoss =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
    (lsNext (lsZero (lsRegLoss k m)) (lsFor m (lsLossBody k m) (lsLossTail k m tail))))))

-- dW_ij = d_i x x_j, then stored
def lsGradientRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsMultiply (lsRegDW k m i j) (lsRegD k m i) (lsRegX k m j)) rest))))))
def lsStoreGradientRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsStore 8 (lsRegDW k m i j) (lsGradientOffset m k i j)) rest))))))
def lsGradientBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsGradientRow k m i) rest)))))
def lsStoreGradientBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsStoreGradientRow k m i) rest)))))
def lsGradient =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
    (lsFor m (lsGradientBody k m) (lsFor m (lsStoreGradientBody k m) tail)))))

-- W'_ij = fma(dW_ij, -eta, W_ij), then stored
def lsUpdateRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsFused (lsRegWp k m i j) (lsRegDW k m i j) (lsRegNegEta k m) (lsRegW k m i j)) rest))))))
def lsStoreUpdateRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
    (lsNext (lsStore 8 (lsRegWp k m i j) (lsUpdatedOffset m k i j)) rest))))))
def lsUpdateBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsUpdateRow k m i) rest)))))
def lsStoreUpdateBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsStoreUpdateRow k m i) rest)))))
def lsUpdate =
  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
    (lsNext (lsNegate (lsRegNegEta k m) 10) (lsFor m (lsUpdateBody k m) (lsFor m (lsStoreUpdateBody k m) tail))))))

def lsExit : (family SM86Program) =
  (lsNext (constructor SM86InstructionBody SM86Exit lsControl) (constructor SM86Program SM86ProgramEnd))

def linearStepSM86ProgramFor =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
    (lsPrologue k m (lsLoads k m (lsOutputs k m (lsResiduals k m (lsLoss k m (lsGradient k m (lsUpdate k m lsExit)))))))))

-- 3 + 9 + (k + m + mk) loads, m + mk + m, 2m, 1 + m + 3, mk + mk, 1 + mk + mk, exit
def linearStepSM86InstructionCountFor =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
    (naturalAdd 18 (naturalAdd k (naturalAdd (naturalMultiply 6 m) (naturalMultiply 6 (naturalMultiply m k)))))))

-- the 2 x 2 program the plan, the proofs and the RTX 3090 record name
def linearStepSM86Program : (family SM86Program) = (linearStepSM86ProgramFor linearStepSM86Outputs linearStepSM86Inputs)

def linearStepSM86InstructionCount : Nat = 56

-- the register count a launch declares: derived from the program
-- (Accelerator.SM86.Operands -- the highest register named, plus the two the
-- hardware reserves, in granules of eight; 40 for 2 x 2)
def linearStepSM86RegistersFor =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
    (sm86RegisterDemand (linearStepSM86ProgramFor m k))))

def linearStepSM86Registers : Nat = (linearStepSM86RegistersFor linearStepSM86Outputs linearStepSM86Inputs)

-- The register plan, 1 when it holds for the shape: an admitted shape's
-- program names exactly the registers below its allocation's span (so its
-- derived register count is the allocation's, and no index wrapped).  The
-- program sits under the admitted branch's binder, not in an argument of
-- naturalSelect: for an open shape the admission can be undecided, and the
-- checker's weak head of a stuck select quotes (and so evaluates) every
-- argument it captured -- here a program generated for an open shape, about
-- 40 s per cell, where the binder keeps it unevaluated.
def linearStepSM86RegisterPlanHolds =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
    (nat-eliminate
      (lambda unrestricted admitted : Nat . Nat)
      1
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
        (naturalEqual (sm86RegisterSpan (linearStepSM86ProgramFor m k)) (linearStepSM86RegisterSpanFor m k))))
      (linearStepSM86ShapeAdmitted m k))))

-- The machine bytes, by the compiler's encoder, for any shape and for the
-- checked 2 x 2.
def linearStepSM86MachineBytesFor =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
    (eliminate SM86ProgramEncodingResult
      (lambda unrestricted current : (family SM86ProgramEncodingResult) . Bytes)
      (sm86EncodeProgram (linearStepSM86ProgramFor m k))
      (branch SM86ProgramEncodingSucceeded bytes telemetry . bytes)
      (branch SM86ProgramEncodingFailed index failure telemetry . b""))))

def linearStepSM86EncodedFor =
  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
    (eliminate SM86ProgramEncodingResult
      (lambda unrestricted current : (family SM86ProgramEncodingResult) . Nat)
      (sm86EncodeProgram (linearStepSM86ProgramFor m k))
      (branch SM86ProgramEncodingSucceeded bytes telemetry . 1)
      (branch SM86ProgramEncodingFailed index failure telemetry . zero))))

def linearStepSM86MachineBytes : Bytes =
  (eliminate SM86ProgramEncodingResult
    (lambda unrestricted current : (family SM86ProgramEncodingResult) . Bytes)
    (sm86EncodeProgram linearStepSM86Program)
    (branch SM86ProgramEncodingSucceeded bytes telemetry . bytes)
    (branch SM86ProgramEncodingFailed index failure telemetry . b""))

-- 1 when the encoder accepted every instruction (a build-time fact: the
-- encoder runs at build, so Proof.CheckedLinearStepArtifact gates the
-- artifact on it and the build refuses an unencodable instruction).
def linearStepSM86Encoded : Nat =
  (eliminate SM86ProgramEncodingResult
    (lambda unrestricted current : (family SM86ProgramEncodingResult) . Nat)
    (sm86EncodeProgram linearStepSM86Program)
    (branch SM86ProgramEncodingSucceeded bytes telemetry . 1)
    (branch SM86ProgramEncodingFailed index failure telemetry . zero))