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).
144def linearStepSM86ShapeAdmitted =
145 (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
146 (naturalAnd (naturalNonzero m) (naturalAnd (naturalNonzero k) (sm86RegisterSpanAdmitted (linearStepSM86RegisterSpanFor m k))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.