Realization.Nvidia.SM86.LinearStepSM86

1module Realization.Nvidia.SM86.LinearStepSM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.Operands
8import Accelerator.SM86.Types
9import Std.Natural
10
11-- The SM86 realization of Learning.Checked.LinearStep for outputs 2, inputs
12-- 2: one thread of one block does the whole step in the semantic program's
13-- exact operation order (fused multiply-adds first element innermost,
14-- subtraction as addition of a negation, the loss as 0.5 x a fused sum of
15-- squares, the update as fma(dW, -eta, W)); every other lane exits at once.
16--
17-- Preconditions (Realization contract):
18--   outputs = 2, inputs = 2 (the register plan is for this shape);
19--   one launch of one block, block width 32 (a single warp);
20--   the parameter block carries, at the offsets below, the 64-bit addresses
21--   of W (row-major, 16 bytes), x (8 bytes), t (8 bytes) and the 44-byte
22--   output record (y 8, loss 4, dW 16, W' 16), and eta at 0x190;
23--   the arena regions those addresses name are disjoint and 4-aligned.
24--
25-- Numerical contract: identical to the semantic program's (fused, ordered);
26-- reproducibility: bitwise on any SM86 device for this realization, which
27-- uses no reduction across lanes and no approximate unit.
28
29def linearStepSM86Identity : Bytes = b"linear-step-sm86-outputs2-inputs2-v1"
30
31def linearStepSM86Outputs : Nat = 2
32def linearStepSM86Inputs : Nat = 2
33def linearStepSM86BlockWidth : Nat = 32
34def linearStepSM86OutputRecordBytes : Nat = 44
35
36-- parameter-block offsets (bytes into c[0])
37def linearStepSM86WeightsOffset : Nat = 352
38def linearStepSM86InputOffset : Nat = 360
39def linearStepSM86TargetOffset : Nat = 368
40def linearStepSM86OutputOffset : Nat = 376
41def linearStepSM86LearningRateOffset : Nat = 400
42
43def lsR = (lambda unrestricted index : Nat . (sm86Register (nat-to-byte index)))
44def lsU = sm86Unsigned32FromNaturalTruncated
45
46-- Controls.  Fixed-latency forms: stall 15 with no scoreboard use, the
47-- over-stall control the momentum realization proved on the 3070 for a
48-- dependent FFMA chain.  Variable-latency forms (S2R, LDG) name a write
49-- barrier and their first consumer waits on it: S2R on SB0, waited by the
50-- ISETP; every LDG on SB1, waited by the first FFMA.  Without the waits the
51-- consumers read the registers' previous contents -- the RTX 3090 returned a
52-- record of zeros for the first version of this program (2026-09-22), and
53-- SM86.Scoreboard now refuses it at the checker.
54def lsControlWith =
55  (lambda unrestricted write : (family SM86Barrier) . (lambda unrestricted wait : Nat .
56    (constructor SM86Control SM86ControlValue
57      (byte 15)
58      (constructor SM86YieldMode SM86Continue)
59      write
60      (constructor SM86Barrier SM86BarrierNone)
61      (nat-to-byte wait)
62      (byte 0))))
63
64def lsControl : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86BarrierNone) 0)
65def lsControlSetSB0 : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86Barrier0) 0)
66def lsControlSetSB1 : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86Barrier1) 0)
67def lsControlWaitSB0 : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86BarrierNone) 1)
68def lsControlWaitSB1 : (family SM86Control) = (lsControlWith (constructor SM86Barrier SM86BarrierNone) 2)
69
70def lsNext =
71  (lambda unrestricted body : (family SM86InstructionBody) .
72    (lambda unrestricted tail : (family SM86Program) .
73      (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail)))
74
75def lsConstant =
76  (lambda unrestricted destination : Nat . (lambda unrestricted offset : Nat .
77    (constructor SM86InstructionBody SM86MoveConstant (lsR destination) (byte 0) (lsU offset) lsControl)))
78
79def lsLoad =
80  (lambda unrestricted destination : Nat . (lambda unrestricted address : Nat . (lambda unrestricted offset : Nat .
81    (constructor SM86InstructionBody SM86LoadGlobal (lsR destination) (lsR address) (lsU offset) lsControlSetSB1))))
82
83def lsStore =
84  (lambda unrestricted address : Nat . (lambda unrestricted value : Nat . (lambda unrestricted offset : Nat .
85    (constructor SM86InstructionBody SM86StoreGlobal (lsR address) (lsR value) (lsU offset) lsControl))))
86
87def lsZero =
88  (lambda unrestricted destination : Nat .
89    (constructor SM86InstructionBody SM86MoveImmediate (lsR destination) sm86Unsigned32Zero lsControl))
90
91def lsFusedWith =
92  (lambda unrestricted control : (family SM86Control) .
93  (lambda unrestricted destination : Nat . (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (lambda unrestricted addend : Nat .
94    (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd (lsR destination) (lsR left) (lsR right) (lsR addend) control))))))
95
96def lsFused = (lsFusedWith lsControl)
97
98def lsMultiply =
99  (lambda unrestricted destination : Nat . (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
100    (constructor SM86InstructionBody SM86FloatMultiply (lsR destination) (lsR left) (lsR right) lsControl))))
101
102def lsAdd =
103  (lambda unrestricted destination : Nat . (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
104    (constructor SM86InstructionBody SM86FloatAdd (lsR destination) (lsR left) (lsR right) lsControl))))
105
106def lsNegate =
107  (lambda unrestricted destination : Nat . (lambda unrestricted source : Nat .
108    (constructor SM86InstructionBody SM86FloatNegate (lsR destination) (lsR source) lsControl)))
109
110-- ---- the program, for any shape ----
111-- Registers, for outputs m and inputs k: R0 tid; R2:R3 &W; R4:R5 &x; R6:R7
112-- &t; R8:R9 &out; R10 eta; then x (k), t (m), W (m x k), y (m), d (m), loss,
113-- 0.5, dW (m x k), -eta, W' (m x k), consecutively from R12 -- for 2 x 2:
114-- R12,R13 x; R14,R15 t; R16..R19 W; R20,R21 y; R22,R23 d; R24 loss; R25 0.5;
115-- R26..R29 dW; R30 -eta; R31..R34 W', the plan the RTX 3090 ran.  The
116-- program is generated from the shape; every loop below is unrolled, in the
117-- semantic program's order (fma chains first element innermost).
118def lsBase : Nat = 12
119def lsRegX = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted j : Nat . (naturalAdd lsBase j))))
120def lsRegT = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (naturalAdd lsBase (naturalAdd k i)))))
121def lsRegW =
122  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
123    (naturalAdd lsBase (naturalAdd k (naturalAdd m (naturalAdd (naturalMultiply i k) j))))))))
124def lsRegY = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (naturalAdd (lsRegW k m m 0) i))))
125def lsRegD = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (naturalAdd (lsRegY k m m) i))))
126def lsRegLoss = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lsRegD k m m)))
127def lsRegHalf = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (naturalAdd (lsRegLoss k m) 1)))
128def lsRegDW =
129  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
130    (naturalAdd (lsRegHalf k m) (naturalAdd 1 (naturalAdd (naturalMultiply i k) j)))))))
131def lsRegNegEta = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lsRegDW k m m 0)))
132def lsRegWp =
133  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
134    (naturalAdd (lsRegNegEta k m) (naturalAdd 1 (naturalAdd (naturalMultiply i k) j)))))))
135-- one past the last register the allocation names (the end of W'):
136-- 15 + k + 3m + 3mk
137def linearStepSM86RegisterSpanFor =
138  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat . (lsRegWp k m m 0)))
139-- The shapes the generator realizes: at least one output and one input, and
140-- the allocation within the register file (Accelerator.SM86.Operands).
141-- Past it the byte register indices would wrap -- a 9 x 9 step would name
142-- R293 as R37, on top of W -- so every artifact gates on this.  240 shapes,
143-- 38 x 1 .. 1 x 57 (Proof.LinearStepRegisterPlan).
144def linearStepSM86ShapeAdmitted =
145  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
146    (naturalAnd (naturalNonzero m) (naturalAnd (naturalNonzero k) (sm86RegisterSpanAdmitted (linearStepSM86RegisterSpanFor m k))))))
147-- the output record: y (4m), loss (4), dW (4mk), W' (4mk)
148def linearStepSM86OutputRecordBytesFor =
149  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
150    (naturalAdd (naturalMultiply 4 m) (naturalAdd 4 (naturalMultiply 8 (naturalMultiply m k))))))
151def lsLossOffset = (lambda unrestricted m : Nat . (naturalMultiply 4 m))
152def lsGradientOffset = (lambda unrestricted m : Nat . (lambda unrestricted k : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
153  (naturalAdd (naturalMultiply 4 m) (naturalAdd 4 (naturalMultiply 4 (naturalAdd (naturalMultiply i k) j))))))))
154def lsUpdatedOffset = (lambda unrestricted m : Nat . (lambda unrestricted k : Nat . (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
155  (naturalAdd (lsGradientOffset m k i j) (naturalMultiply 4 (naturalMultiply m k)))))))
156
157-- an unrolled loop: body 0 (body 1 (... body (count-1) tail))
158def lsFor =
159  (lambda unrestricted count : Nat .
160    (lambda unrestricted body : (pi unrestricted index : Nat . (pi unrestricted rest : (family SM86Program) . (family SM86Program))) .
161      (lambda unrestricted tail : (family SM86Program) .
162        (nat-eliminate
163          (lambda unrestricted current : Nat . (family SM86Program))
164          tail
165          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SM86Program) .
166            (body (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) predecessor) induction)))
167          count))))
168
169-- the first fused multiply-add waits on the loads' barrier
170def lsFirstFusedControl =
171  (lambda unrestricted i : Nat . (lambda unrestricted j : Nat .
172    (nat-eliminate
173      (lambda unrestricted current : Nat . (family SM86Control))
174      lsControl
175      (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family SM86Control) . lsControlWaitSB1))
176      (naturalAnd (naturalIsZero i) (naturalIsZero j)))))
177
178-- The program as named blocks and named loop bodies, each prepending its
179-- instructions to what follows, so a statement about the program is a
180-- statement about its parts (Proof.LinearStepGeneratorForall): the
181-- prologue, the loads, y, d, the loss, dW, W', Exit.
182
183-- tid, the lane guard, the nine parameter words (4 addresses, eta)
184def lsPrologue =
185  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
186    (lsNext (constructor SM86InstructionBody SM86SpecialToRegister (lsR 0) (constructor SM86SpecialRegister SM86ThreadIdX) lsControlSetSB0)
187    (lsNext (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate (constructor SM86Predicate SM86Predicate0) (lsR 0) sm86Unsigned32Zero lsControlWaitSB0)
188    (constructor SM86Program SM86ProgramNext (sm86PredicatedInstruction (constructor SM86Predicate SM86Predicate0) (constructor SM86InstructionBody SM86Exit lsControl))
189    (lsNext (lsConstant 2 352)
190    (lsNext (lsConstant 3 356)
191    (lsNext (lsConstant 4 360)
192    (lsNext (lsConstant 5 364)
193    (lsNext (lsConstant 6 368)
194    (lsNext (lsConstant 7 372)
195    (lsNext (lsConstant 8 376)
196    (lsNext (lsConstant 9 380)
197    (lsNext (lsConstant 10 400)
198      tail)))))))))))))))
199
200-- the loads: x (k), t (m), W (m rows of k)
201def lsLoadXBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
202  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) . (lsNext (lsLoad (lsRegX k m j) 4 (naturalMultiply 4 j)) rest)))))
203def lsLoadTBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
204  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsNext (lsLoad (lsRegT k m i) 6 (naturalMultiply 4 i)) rest)))))
205def lsLoadWRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
206  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
207    (lsNext (lsLoad (lsRegW k m i j) 2 (naturalMultiply 4 (naturalAdd (naturalMultiply i k) j))) rest))))))
208def lsLoadWBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
209  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsLoadWRow k m i) rest)))))
210def lsLoads =
211  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
212    (lsFor k (lsLoadXBody k m) (lsFor m (lsLoadTBody k m) (lsFor m (lsLoadWBody k m) tail))))))
213
214-- y_i = fma(W_i(k-1), x_(k-1), ... fma(W_i0, x_0, +0.0)), then stored
215def lsOutputRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
216  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
217    (lsNext (lsFusedWith (lsFirstFusedControl i j) (lsRegY k m i) (lsRegW k m i j) (lsRegX k m j) (lsRegY k m i)) rest))))))
218def lsOutputBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
219  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) .
220    (lsNext (lsZero (lsRegY k m i)) (lsFor k (lsOutputRow k m i) rest))))))
221def lsStoreYBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
222  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsNext (lsStore 8 (lsRegY k m i) (naturalMultiply 4 i)) rest)))))
223def lsOutputs =
224  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
225    (lsFor m (lsOutputBody k m) (lsFor m (lsStoreYBody k m) tail)))))
226
227-- d_i = y_i + (-t_i)
228def lsResidualBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
229  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) .
230    (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))))))
231def lsResiduals =
232  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
233    (lsFor m (lsResidualBody k m) tail))))
234
235-- loss = 0.5 x fma(d_(m-1), d_(m-1), ... fma(d_0, d_0, +0.0)), then stored
236def lsLossBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
237  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) .
238    (lsNext (lsFused (lsRegLoss k m) (lsRegD k m i) (lsRegD k m i) (lsRegLoss k m)) rest)))))
239def lsLossTail = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
240  (lsNext (constructor SM86InstructionBody SM86MoveImmediate (lsR (lsRegHalf k m)) (lsU 1056964608) lsControl)
241  (lsNext (lsMultiply (lsRegLoss k m) (lsRegHalf k m) (lsRegLoss k m))
242  (lsNext (lsStore 8 (lsRegLoss k m) (lsLossOffset m))
243    tail))))))
244def lsLoss =
245  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
246    (lsNext (lsZero (lsRegLoss k m)) (lsFor m (lsLossBody k m) (lsLossTail k m tail))))))
247
248-- dW_ij = d_i x x_j, then stored
249def lsGradientRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
250  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
251    (lsNext (lsMultiply (lsRegDW k m i j) (lsRegD k m i) (lsRegX k m j)) rest))))))
252def lsStoreGradientRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
253  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
254    (lsNext (lsStore 8 (lsRegDW k m i j) (lsGradientOffset m k i j)) rest))))))
255def lsGradientBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
256  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsGradientRow k m i) rest)))))
257def lsStoreGradientBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
258  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsStoreGradientRow k m i) rest)))))
259def lsGradient =
260  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
261    (lsFor m (lsGradientBody k m) (lsFor m (lsStoreGradientBody k m) tail)))))
262
263-- W'_ij = fma(dW_ij, -eta, W_ij), then stored
264def lsUpdateRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
265  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
266    (lsNext (lsFused (lsRegWp k m i j) (lsRegDW k m i j) (lsRegNegEta k m) (lsRegW k m i j)) rest))))))
267def lsStoreUpdateRow = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted i : Nat .
268  (lambda unrestricted j : Nat . (lambda unrestricted rest : (family SM86Program) .
269    (lsNext (lsStore 8 (lsRegWp k m i j) (lsUpdatedOffset m k i j)) rest))))))
270def lsUpdateBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
271  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsUpdateRow k m i) rest)))))
272def lsStoreUpdateBody = (lambda unrestricted k : Nat . (lambda unrestricted m : Nat .
273  (lambda unrestricted i : Nat . (lambda unrestricted rest : (family SM86Program) . (lsFor k (lsStoreUpdateRow k m i) rest)))))
274def lsUpdate =
275  (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
276    (lsNext (lsNegate (lsRegNegEta k m) 10) (lsFor m (lsUpdateBody k m) (lsFor m (lsStoreUpdateBody k m) tail))))))
277
278def lsExit : (family SM86Program) =
279  (lsNext (constructor SM86InstructionBody SM86Exit lsControl) (constructor SM86Program SM86ProgramEnd))
280
281def linearStepSM86ProgramFor =
282  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
283    (lsPrologue k m (lsLoads k m (lsOutputs k m (lsResiduals k m (lsLoss k m (lsGradient k m (lsUpdate k m lsExit)))))))))
284
285-- 3 + 9 + (k + m + mk) loads, m + mk + m, 2m, 1 + m + 3, mk + mk, 1 + mk + mk, exit
286def linearStepSM86InstructionCountFor =
287  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
288    (naturalAdd 18 (naturalAdd k (naturalAdd (naturalMultiply 6 m) (naturalMultiply 6 (naturalMultiply m k)))))))
289
290-- the 2 x 2 program the plan, the proofs and the RTX 3090 record name
291def linearStepSM86Program : (family SM86Program) = (linearStepSM86ProgramFor linearStepSM86Outputs linearStepSM86Inputs)
292
293def linearStepSM86InstructionCount : Nat = 56
294
295-- the register count a launch declares: derived from the program
296-- (Accelerator.SM86.Operands -- the highest register named, plus the two the
297-- hardware reserves, in granules of eight; 40 for 2 x 2)
298def linearStepSM86RegistersFor =
299  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
300    (sm86RegisterDemand (linearStepSM86ProgramFor m k))))
301
302def linearStepSM86Registers : Nat = (linearStepSM86RegistersFor linearStepSM86Outputs linearStepSM86Inputs)
303
304-- The register plan, 1 when it holds for the shape: an admitted shape's
305-- program names exactly the registers below its allocation's span (so its
306-- derived register count is the allocation's, and no index wrapped).  The
307-- program sits under the admitted branch's binder, not in an argument of
308-- naturalSelect: for an open shape the admission can be undecided, and the
309-- checker's weak head of a stuck select quotes (and so evaluates) every
310-- argument it captured -- here a program generated for an open shape, about
311-- 40 s per cell, where the binder keeps it unevaluated.
312def linearStepSM86RegisterPlanHolds =
313  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
314    (nat-eliminate
315      (lambda unrestricted admitted : Nat . Nat)
316      1
317      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
318        (naturalEqual (sm86RegisterSpan (linearStepSM86ProgramFor m k)) (linearStepSM86RegisterSpanFor m k))))
319      (linearStepSM86ShapeAdmitted m k))))
320
321-- The machine bytes, by the compiler's encoder, for any shape and for the
322-- checked 2 x 2.
323def linearStepSM86MachineBytesFor =
324  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
325    (eliminate SM86ProgramEncodingResult
326      (lambda unrestricted current : (family SM86ProgramEncodingResult) . Bytes)
327      (sm86EncodeProgram (linearStepSM86ProgramFor m k))
328      (branch SM86ProgramEncodingSucceeded bytes telemetry . bytes)
329      (branch SM86ProgramEncodingFailed index failure telemetry . b""))))
330
331def linearStepSM86EncodedFor =
332  (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
333    (eliminate SM86ProgramEncodingResult
334      (lambda unrestricted current : (family SM86ProgramEncodingResult) . Nat)
335      (sm86EncodeProgram (linearStepSM86ProgramFor m k))
336      (branch SM86ProgramEncodingSucceeded bytes telemetry . 1)
337      (branch SM86ProgramEncodingFailed index failure telemetry . zero))))
338
339def linearStepSM86MachineBytes : Bytes =
340  (eliminate SM86ProgramEncodingResult
341    (lambda unrestricted current : (family SM86ProgramEncodingResult) . Bytes)
342    (sm86EncodeProgram linearStepSM86Program)
343    (branch SM86ProgramEncodingSucceeded bytes telemetry . bytes)
344    (branch SM86ProgramEncodingFailed index failure telemetry . b""))
345
346-- 1 when the encoder accepted every instruction (a build-time fact: the
347-- encoder runs at build, so Proof.CheckedLinearStepArtifact gates the
348-- artifact on it and the build refuses an unencodable instruction).
349def linearStepSM86Encoded : Nat =
350  (eliminate SM86ProgramEncodingResult
351    (lambda unrestricted current : (family SM86ProgramEncodingResult) . Nat)
352    (sm86EncodeProgram linearStepSM86Program)
353    (branch SM86ProgramEncodingSucceeded bytes telemetry . 1)
354    (branch SM86ProgramEncodingFailed index failure telemetry . zero))