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).
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))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.