module Realization.Nvidia.SM86.GELUSM86 import Accelerator.SM86.Control import Accelerator.SM86.Immediate import Accelerator.SM86.Instruction import Accelerator.SM86.InstructionEncoding import Accelerator.SM86.NumericSemantics import Accelerator.SM86.Program import Accelerator.SM86.Types import Data.SHA256Digest import Std.Natural import Std.Byte family GELUSM86ProgramKind : Type 0 constructor GELUSM86Forward constructor GELUSM86Backward end-family family GELUSM86ScalarKind : Type 0 constructor GELUSM86ScaleScalar constructor GELUSM86CubicScalar constructor GELUSM86HalfScalar constructor GELUSM86OneScalar constructor GELUSM86ThreeCubicScalar end-family family GELUSM86ScalarBinding : Type 0 constructor GELUSM86ScalarBindingValue field unrestricted geluSM86ScalarKind : (family GELUSM86ScalarKind) field unrestricted geluSM86ScalarOffset : (family SM86Unsigned32) end-family family GELUSM86ScalarBindings : Type 0 constructor GELUSM86ScalarBindingsEnd constructor GELUSM86ScalarBindingsNext field unrestricted geluSM86ScalarBindingHead : (family GELUSM86ScalarBinding) recursive unrestricted geluSM86ScalarBindingTail end-family family GELUSM86FailureCode : Type 0 constructor GELUSM86ElementCountZero constructor GELUSM86ElementCountMisaligned constructor GELUSM86InstructionCountMismatch constructor GELUSM86EncodingFailed constructor GELUSM86IdentityInvalid end-family family GELUSM86Telemetry : Type 0 constructor GELUSM86TelemetryValue field unrestricted geluSM86TelemetryKind : (family GELUSM86ProgramKind) field unrestricted geluSM86TelemetryExpectedInstructions : Nat field unrestricted geluSM86TelemetryActualInstructions : Nat field unrestricted geluSM86TelemetryRegisters : Nat field unrestricted geluSM86TelemetryElements : Nat field unrestricted geluSM86TelemetryGridX : Nat field unrestricted geluSM86TelemetryBlockX : Nat field unrestricted geluSM86TelemetryScalarBindings : Nat field unrestricted geluSM86TelemetryHostOperations : Nat field unrestricted geluSM86TelemetryEncodedBytes : Nat field unrestricted geluSM86TelemetryEncodedFields : Nat field unrestricted geluSM86TelemetryEncodedBits : Nat constructor GELUSM86TelemetryRejected field unrestricted geluSM86TelemetryFailure : (family GELUSM86FailureCode) field unrestricted geluSM86TelemetryFailureOrdinal : Nat end-family family GELUSM86Plan : Type 0 constructor GELUSM86PlanValue field unrestricted geluSM86PlanKind : (family GELUSM86ProgramKind) field unrestricted geluSM86PlanElements : Nat field unrestricted geluSM86PlanProgram : (family SM86Program) field unrestricted geluSM86PlanScalars : (family GELUSM86ScalarBindings) field unrestricted geluSM86PlanTelemetry : (family GELUSM86Telemetry) end-family family GELUSM86PlanResult : Type 0 constructor GELUSM86PlanReady field unrestricted geluSM86ReadyPlan : (family GELUSM86Plan) constructor GELUSM86PlanFailed field unrestricted geluSM86PlanFailure : (family GELUSM86FailureCode) field unrestricted geluSM86PlanFailureTelemetry : (family GELUSM86Telemetry) end-family family GELUSM86ImageResult : Type 0 constructor GELUSM86ImageReady field unrestricted geluSM86ImageKind : (family GELUSM86ProgramKind) field unrestricted geluSM86ImageBytes : Bytes field unrestricted geluSM86ImageSHA256 : Bytes field unrestricted geluSM86ImageTelemetry : (family GELUSM86Telemetry) constructor GELUSM86ImageFailed field unrestricted geluSM86ImageFailure : (family GELUSM86FailureCode) field unrestricted geluSM86ImageFailureInstruction : Nat field unrestricted geluSM86ImageFailureDetail : Bytes field unrestricted geluSM86ImageFailureTelemetry : (family GELUSM86Telemetry) end-family def geluSM86NaturalFive = (byte-to-nat (byte 5)) def geluSM86NaturalTwentyTwo = (byte-to-nat (byte 22)) def geluSM86NaturalTwentyFour = (byte-to-nat (byte 24)) def geluSM86NaturalThirtyTwo = (byte-to-nat (byte 32)) def geluSM86NaturalThirtyFour = (byte-to-nat (byte 34)) def geluSM86BlockX = byteNaturalTwoHundredFiftySix def geluSM86Unsigned32 = (lambda unrestricted b0 : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b2 : Byte . (lambda unrestricted b3 : Byte . (sm86Unsigned32 b0 b1 b2 b3))))) def geluSM86ImmediateZero = (geluSM86Unsigned32 (byte 0) (byte 0) (byte 0) (byte 0)) def geluSM86ImmediateFour = (geluSM86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0)) def geluSM86ImmediateTwoHundredFiftySix = (geluSM86Unsigned32 (byte 0) (byte 1) (byte 0) (byte 0)) def geluSM86ConstantBase = (geluSM86Unsigned32 (byte 40) (byte 0) (byte 0) (byte 0)) def geluSM86OutputPointer = (geluSM86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0)) def geluSM86InputPointer = (geluSM86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0)) def geluSM86UpstreamPointer = (geluSM86Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0)) def geluSM86ScaleOffset = (geluSM86Unsigned32 (byte 144) (byte 1) (byte 0) (byte 0)) def geluSM86CubicOffset = (geluSM86Unsigned32 (byte 148) (byte 1) (byte 0) (byte 0)) def geluSM86HalfOffset = (geluSM86Unsigned32 (byte 152) (byte 1) (byte 0) (byte 0)) def geluSM86OneOffset = (geluSM86Unsigned32 (byte 156) (byte 1) (byte 0) (byte 0)) def geluSM86ThreeCubicOffset = (geluSM86Unsigned32 (byte 160) (byte 1) (byte 0) (byte 0)) def geluSM86ScalarBindings : (family GELUSM86ScalarBindings) = (constructor GELUSM86ScalarBindings GELUSM86ScalarBindingsNext (constructor GELUSM86ScalarBinding GELUSM86ScalarBindingValue (constructor GELUSM86ScalarKind GELUSM86ScaleScalar) geluSM86ScaleOffset) (constructor GELUSM86ScalarBindings GELUSM86ScalarBindingsNext (constructor GELUSM86ScalarBinding GELUSM86ScalarBindingValue (constructor GELUSM86ScalarKind GELUSM86CubicScalar) geluSM86CubicOffset) (constructor GELUSM86ScalarBindings GELUSM86ScalarBindingsNext (constructor GELUSM86ScalarBinding GELUSM86ScalarBindingValue (constructor GELUSM86ScalarKind GELUSM86HalfScalar) geluSM86HalfOffset) (constructor GELUSM86ScalarBindings GELUSM86ScalarBindingsNext (constructor GELUSM86ScalarBinding GELUSM86ScalarBindingValue (constructor GELUSM86ScalarKind GELUSM86OneScalar) geluSM86OneOffset) (constructor GELUSM86ScalarBindings GELUSM86ScalarBindingsNext (constructor GELUSM86ScalarBinding GELUSM86ScalarBindingValue (constructor GELUSM86ScalarKind GELUSM86ThreeCubicScalar) geluSM86ThreeCubicOffset) (constructor GELUSM86ScalarBindings GELUSM86ScalarBindingsEnd)))))) def geluSM86Register = (lambda unrestricted value : Byte . (sm86Register value)) def geluSM86Instruction = (lambda unrestricted body : (family SM86InstructionBody) . (constructor SM86Instruction SM86InstructionValue (constructor SM86InstructionGuard SM86InstructionAlways) body)) def geluSM86Next = (lambda unrestricted body : (family SM86InstructionBody) . (lambda unrestricted tail : (family SM86Program) . (constructor SM86Program SM86ProgramNext (geluSM86Instruction body) tail))) def geluSM86End = (constructor SM86Program SM86ProgramEnd) def geluSM86SetBarrier0 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0)) def geluSM86SetBarrier1 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1)) def geluSM86SetBarrier2 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2)) def geluSM86SetBarrier3 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier3)) def geluSM86SetBarrier4 = (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier4)) def geluSM86WaitBarrier3 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier3)) def geluSM86WaitBarrier4 = (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier4)) def geluSM86WaitSpecials : (family SM86Control) = (constructor SM86Control SM86ControlValue (byte 7) (constructor SM86YieldMode SM86Continue) (constructor SM86Barrier SM86BarrierNone) (constructor SM86Barrier SM86BarrierNone) (byte 3) (byte 0)) def geluSM86WaitInputs : (family SM86Control) = (constructor SM86Control SM86ControlValue (byte 7) (constructor SM86YieldMode SM86Continue) (constructor SM86Barrier SM86BarrierNone) (constructor SM86Barrier SM86BarrierNone) (byte 12) (byte 0)) def geluSM86ForwardProgram : (family SM86Program) = (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 1)) (byte 0) geluSM86ConstantBase sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86SpecialToRegister (geluSM86Register (byte 0)) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) geluSM86SetBarrier0) (geluSM86Next (constructor SM86InstructionBody SM86SpecialToRegister (geluSM86Register (byte 2)) (constructor SM86SpecialRegister SM86ThreadIdX) geluSM86SetBarrier1) (geluSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate (geluSM86Register (byte 3)) (geluSM86Register (byte 0)) geluSM86ImmediateTwoHundredFiftySix (geluSM86Register (byte 2)) geluSM86WaitSpecials) (geluSM86Next (constructor SM86InstructionBody SM86MoveImmediate (geluSM86Register (byte 4)) geluSM86ImmediateFour sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant (geluSM86Register (byte 6)) (geluSM86Register (byte 3)) (geluSM86Register (byte 4)) (byte 0) geluSM86InputPointer sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86LoadGlobal (geluSM86Register (byte 8)) (geluSM86Register (byte 6)) geluSM86ImmediateZero geluSM86SetBarrier2) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 10)) (byte 0) geluSM86ScaleOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 11)) (byte 0) geluSM86CubicOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 12)) (byte 0) geluSM86HalfOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 13)) (byte 0) geluSM86OneOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 14)) (geluSM86Register (byte 8)) (geluSM86Register (byte 8)) (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier2))) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 15)) (geluSM86Register (byte 14)) (geluSM86Register (byte 8)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd (geluSM86Register (byte 16)) (geluSM86Register (byte 15)) (geluSM86Register (byte 11)) (geluSM86Register (byte 8)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 16)) (geluSM86Register (byte 16)) (geluSM86Register (byte 10)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation (geluSM86Register (byte 17)) (geluSM86Register (byte 16)) (constructor SM86MultiFunction SM86HyperbolicTangent) geluSM86SetBarrier3) (geluSM86Next (constructor SM86InstructionBody SM86FloatAdd (geluSM86Register (byte 17)) (geluSM86Register (byte 17)) (geluSM86Register (byte 13)) geluSM86WaitBarrier3) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 17)) (geluSM86Register (byte 17)) (geluSM86Register (byte 12)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 18)) (geluSM86Register (byte 8)) (geluSM86Register (byte 17)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant (geluSM86Register (byte 20)) (geluSM86Register (byte 3)) (geluSM86Register (byte 4)) (byte 0) geluSM86OutputPointer sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86StoreGlobal (geluSM86Register (byte 20)) (geluSM86Register (byte 18)) geluSM86ImmediateZero sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) geluSM86End)))))))))))))))))))))) def geluSM86BackwardProgram : (family SM86Program) = (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 1)) (byte 0) geluSM86ConstantBase sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86SpecialToRegister (geluSM86Register (byte 0)) (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX) geluSM86SetBarrier0) (geluSM86Next (constructor SM86InstructionBody SM86SpecialToRegister (geluSM86Register (byte 2)) (constructor SM86SpecialRegister SM86ThreadIdX) geluSM86SetBarrier1) (geluSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate (geluSM86Register (byte 3)) (geluSM86Register (byte 0)) geluSM86ImmediateTwoHundredFiftySix (geluSM86Register (byte 2)) geluSM86WaitSpecials) (geluSM86Next (constructor SM86InstructionBody SM86MoveImmediate (geluSM86Register (byte 4)) geluSM86ImmediateFour sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant (geluSM86Register (byte 6)) (geluSM86Register (byte 3)) (geluSM86Register (byte 4)) (byte 0) geluSM86InputPointer sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant (geluSM86Register (byte 8)) (geluSM86Register (byte 3)) (geluSM86Register (byte 4)) (byte 0) geluSM86UpstreamPointer sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86LoadGlobal (geluSM86Register (byte 10)) (geluSM86Register (byte 6)) geluSM86ImmediateZero geluSM86SetBarrier2) (geluSM86Next (constructor SM86InstructionBody SM86LoadGlobal (geluSM86Register (byte 11)) (geluSM86Register (byte 8)) geluSM86ImmediateZero geluSM86SetBarrier3) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 12)) (byte 0) geluSM86ScaleOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 13)) (byte 0) geluSM86CubicOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 14)) (byte 0) geluSM86HalfOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 15)) (byte 0) geluSM86OneOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MoveConstant (geluSM86Register (byte 16)) (byte 0) geluSM86ThreeCubicOffset sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 17)) (geluSM86Register (byte 10)) (geluSM86Register (byte 10)) geluSM86WaitInputs) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 18)) (geluSM86Register (byte 17)) (geluSM86Register (byte 10)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd (geluSM86Register (byte 19)) (geluSM86Register (byte 18)) (geluSM86Register (byte 13)) (geluSM86Register (byte 10)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 19)) (geluSM86Register (byte 19)) (geluSM86Register (byte 12)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation (geluSM86Register (byte 20)) (geluSM86Register (byte 19)) (constructor SM86MultiFunction SM86HyperbolicTangent) geluSM86SetBarrier4) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 21)) (geluSM86Register (byte 20)) (geluSM86Register (byte 20)) geluSM86WaitBarrier4) (geluSM86Next (constructor SM86InstructionBody SM86FloatNegate (geluSM86Register (byte 21)) (geluSM86Register (byte 21)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatAdd (geluSM86Register (byte 21)) (geluSM86Register (byte 15)) (geluSM86Register (byte 21)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd (geluSM86Register (byte 22)) (geluSM86Register (byte 17)) (geluSM86Register (byte 16)) (geluSM86Register (byte 15)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 22)) (geluSM86Register (byte 22)) (geluSM86Register (byte 12)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatAdd (geluSM86Register (byte 23)) (geluSM86Register (byte 15)) (geluSM86Register (byte 20)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 23)) (geluSM86Register (byte 23)) (geluSM86Register (byte 14)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 24)) (geluSM86Register (byte 10)) (geluSM86Register (byte 21)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 24)) (geluSM86Register (byte 24)) (geluSM86Register (byte 22)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 24)) (geluSM86Register (byte 24)) (geluSM86Register (byte 14)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatAdd (geluSM86Register (byte 25)) (geluSM86Register (byte 23)) (geluSM86Register (byte 24)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86FloatMultiply (geluSM86Register (byte 25)) (geluSM86Register (byte 11)) (geluSM86Register (byte 25)) sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant (geluSM86Register (byte 26)) (geluSM86Register (byte 3)) (geluSM86Register (byte 4)) (byte 0) geluSM86OutputPointer sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86StoreGlobal (geluSM86Register (byte 26)) (geluSM86Register (byte 25)) geluSM86ImmediateZero sm86SafeControl) (geluSM86Next (constructor SM86InstructionBody SM86Exit sm86SafeControl) geluSM86End)))))))))))))))))))))))))))))))))) def geluSM86Program = (lambda unrestricted kind : (family GELUSM86ProgramKind) . (eliminate GELUSM86ProgramKind (lambda unrestricted current : (family GELUSM86ProgramKind) . (family SM86Program)) kind (branch GELUSM86Forward . geluSM86ForwardProgram) (branch GELUSM86Backward . geluSM86BackwardProgram))) def geluSM86ExpectedInstructions = (lambda unrestricted kind : (family GELUSM86ProgramKind) . (eliminate GELUSM86ProgramKind (lambda unrestricted current : (family GELUSM86ProgramKind) . Nat) kind (branch GELUSM86Forward . geluSM86NaturalTwentyTwo) (branch GELUSM86Backward . geluSM86NaturalThirtyFour))) def geluSM86RegisterCount = (lambda unrestricted kind : (family GELUSM86ProgramKind) . (eliminate GELUSM86ProgramKind (lambda unrestricted current : (family GELUSM86ProgramKind) . Nat) kind (branch GELUSM86Forward . geluSM86NaturalTwentyFour) (branch GELUSM86Backward . geluSM86NaturalThirtyTwo))) def geluSM86FailureCodeBytes = (lambda unrestricted code : (family GELUSM86FailureCode) . (eliminate GELUSM86FailureCode (lambda unrestricted current : (family GELUSM86FailureCode) . Bytes) code (branch GELUSM86ElementCountZero . b"ALPHA-SM86-GELU-001") (branch GELUSM86ElementCountMisaligned . b"ALPHA-SM86-GELU-002") (branch GELUSM86InstructionCountMismatch . b"ALPHA-SM86-GELU-003") (branch GELUSM86EncodingFailed . b"ALPHA-SM86-GELU-004") (branch GELUSM86IdentityInvalid . b"ALPHA-SM86-GELU-005"))) def geluSM86RejectedTelemetry = (lambda unrestricted code : (family GELUSM86FailureCode) . (lambda unrestricted ordinal : Nat . (constructor GELUSM86Telemetry GELUSM86TelemetryRejected code ordinal))) def geluSM86Plan = (lambda unrestricted kind : (family GELUSM86ProgramKind) . (lambda unrestricted elements : Nat . (nat-eliminate (lambda unrestricted nonzero : Nat . (family GELUSM86PlanResult)) (constructor GELUSM86PlanResult GELUSM86PlanFailed (constructor GELUSM86FailureCode GELUSM86ElementCountZero) (geluSM86RejectedTelemetry (constructor GELUSM86FailureCode GELUSM86ElementCountZero) zero)) (lambda unrestricted nonzeroPredecessor : Nat . (lambda unrestricted nonzeroInduction : (family GELUSM86PlanResult) . (nat-eliminate (lambda unrestricted aligned : Nat . (family GELUSM86PlanResult)) (constructor GELUSM86PlanResult GELUSM86PlanFailed (constructor GELUSM86FailureCode GELUSM86ElementCountMisaligned) (geluSM86RejectedTelemetry (constructor GELUSM86FailureCode GELUSM86ElementCountMisaligned) elements)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family GELUSM86PlanResult) . (app (lambda unrestricted program : (family SM86Program) . (app (lambda unrestricted actual : Nat . (nat-eliminate (lambda unrestricted countValid : Nat . (family GELUSM86PlanResult)) (constructor GELUSM86PlanResult GELUSM86PlanFailed (constructor GELUSM86FailureCode GELUSM86InstructionCountMismatch) (geluSM86RejectedTelemetry (constructor GELUSM86FailureCode GELUSM86InstructionCountMismatch) actual)) (lambda unrestricted countPredecessor : Nat . (lambda unrestricted countInduction : (family GELUSM86PlanResult) . (constructor GELUSM86PlanResult GELUSM86PlanReady (constructor GELUSM86Plan GELUSM86PlanValue kind elements program geluSM86ScalarBindings (constructor GELUSM86Telemetry GELUSM86TelemetryValue kind (geluSM86ExpectedInstructions kind) actual (geluSM86RegisterCount kind) elements (naturalDivideUnchecked elements geluSM86BlockX) geluSM86BlockX geluSM86NaturalFive zero zero zero zero))))) (naturalEqual actual (geluSM86ExpectedInstructions kind)))) (sm86ProgramCount program))) (geluSM86Program kind)))) (naturalIsZero (naturalModuloUnchecked elements geluSM86BlockX))))) (naturalNonzero elements)))) def geluSM86Image = (lambda unrestricted kind : (family GELUSM86ProgramKind) . (lambda unrestricted elements : Nat . (eliminate GELUSM86PlanResult (lambda unrestricted current : (family GELUSM86PlanResult) . (family GELUSM86ImageResult)) (geluSM86Plan kind elements) (branch GELUSM86PlanReady plan . (eliminate GELUSM86Plan (lambda unrestricted current : (family GELUSM86Plan) . (family GELUSM86ImageResult)) plan (branch GELUSM86PlanValue plannedKind plannedElements program scalars telemetry . (eliminate SM86ProgramEncodingResult (lambda unrestricted current : (family SM86ProgramEncodingResult) . (family GELUSM86ImageResult)) (sm86EncodeProgram program) (branch SM86ProgramEncodingSucceeded image encodingTelemetry . (app (lambda unrestricted identity : Bytes . (nat-eliminate (lambda unrestricted valid : Nat . (family GELUSM86ImageResult)) (constructor GELUSM86ImageResult GELUSM86ImageFailed (constructor GELUSM86FailureCode GELUSM86IdentityInvalid) zero (geluSM86FailureCodeBytes (constructor GELUSM86FailureCode GELUSM86IdentityInvalid)) telemetry) (lambda unrestricted validPredecessor : Nat . (lambda unrestricted validInduction : (family GELUSM86ImageResult) . (eliminate SM86ProgramEncodingTelemetry (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) . (family GELUSM86ImageResult)) encodingTelemetry (branch SM86ProgramEncodingTelemetryValue instructions bytes fields bits highest . (constructor GELUSM86ImageResult GELUSM86ImageReady plannedKind image identity (constructor GELUSM86Telemetry GELUSM86TelemetryValue plannedKind (geluSM86ExpectedInstructions plannedKind) instructions (geluSM86RegisterCount plannedKind) plannedElements (naturalDivideUnchecked plannedElements geluSM86BlockX) geluSM86BlockX geluSM86NaturalFive zero bytes fields bits)))))) (naturalEqual (bytes-length identity) (byte-to-nat (byte 64))))) (sha256HexBytesOrEmpty (sha256Hex image)))) (branch SM86ProgramEncodingFailed index failure encodingTelemetry . (constructor GELUSM86ImageResult GELUSM86ImageFailed (constructor GELUSM86FailureCode GELUSM86EncodingFailed) index (sm86InstructionEncodingStableCode failure) telemetry)))))) (branch GELUSM86PlanFailed code telemetry . (constructor GELUSM86ImageResult GELUSM86ImageFailed code zero (geluSM86FailureCodeBytes code) telemetry)))))