module Accelerator.SM86.FieldEncoding import Accelerator.SM86.Control import Accelerator.SM86.ControlEncoding import Accelerator.SM86.Instruction import Accelerator.SM86.Immediate import Accelerator.SM86.Types import Std.Natural import Std.Byte family SM86EncodingErrorCode : Type 0 constructor SM86EncodingWordLengthInvalid constructor SM86EncodingFieldWidthInvalid constructor SM86EncodingFieldExtentInvalid constructor SM86EncodingFieldValueOverflow constructor SM86EncodingControlInvalid end-family family SM86EncodedField : Type 0 constructor SM86EncodedFieldValue field unrestricted sm86EncodedFieldPosition : Nat field unrestricted sm86EncodedFieldWidth : Nat field unrestricted sm86EncodedFieldValue : Nat constructor SM86EncodedFieldWord32Value field unrestricted sm86EncodedFieldWord32Position : Nat field unrestricted sm86EncodedFieldWord32Value : (family SM86Unsigned32) constructor SM86EncodedFieldWord24Value field unrestricted sm86EncodedFieldWord24Position : Nat field unrestricted sm86EncodedFieldWord24Byte0 : Byte field unrestricted sm86EncodedFieldWord24Byte1 : Byte field unrestricted sm86EncodedFieldWord24Byte2 : Byte end-family family SM86EncodedFieldList : Type 0 constructor SM86EncodedFieldListEmpty constructor SM86EncodedFieldListCons field unrestricted sm86EncodedFieldListHead : (family SM86EncodedField) recursive unrestricted sm86EncodedFieldListTail end-family family SM86FieldEncodingTelemetry : Type 0 constructor SM86FieldEncodingTelemetryValue field unrestricted sm86FieldTelemetryFieldsEncoded : Nat field unrestricted sm86FieldTelemetryBitsWritten : Nat field unrestricted sm86FieldTelemetryOutputBytes : Nat field unrestricted sm86FieldTelemetryHighestExclusiveBit : Nat end-family family SM86FieldEncodingResult : Type 0 constructor SM86FieldEncodingSucceeded field unrestricted sm86FieldEncodedBytes : Bytes field unrestricted sm86FieldEncodingTelemetry : (family SM86FieldEncodingTelemetry) constructor SM86FieldEncodingFailed field unrestricted sm86FieldEncodingError : (family SM86EncodingErrorCode) field unrestricted sm86FieldEncodingPosition : Nat field unrestricted sm86FieldEncodingWidth : Nat field unrestricted sm86FieldEncodingDetail : Nat field unrestricted sm86FieldFailureTelemetry : (family SM86FieldEncodingTelemetry) end-family family SM86HeaderGuard : Type 0 constructor SM86HeaderGuardValue field unrestricted sm86HeaderGuardPredicate : Nat field unrestricted sm86HeaderGuardNegated : Nat end-family def sm86EncodingNaturalTwo = (byte-to-nat (byte 2)) def sm86EncodingNaturalThree = (byte-to-nat (byte 3)) def sm86EncodingNaturalEight = (byte-to-nat (byte 8)) def sm86EncodingNaturalTwelve = (byte-to-nat (byte 12)) def sm86EncodingNaturalFifteen = (byte-to-nat (byte 15)) def sm86EncodingNaturalSixteen = (byte-to-nat (byte 16)) def sm86EncodingNaturalTwentyFour = (byte-to-nat (byte 24)) def sm86EncodingNaturalThirtyTwo = (byte-to-nat (byte 32)) def sm86EncodingNaturalTwentyThree = (byte-to-nat (byte 23)) def sm86EncodingNaturalOneHundredFive = (byte-to-nat (byte 105)) def sm86EncodingNaturalOneHundredTwentyEight = (byte-to-nat (byte 128)) def sm86EncodingNaturalSixtyFiveThousandFiveHundredThirtySix = (naturalMultiply byteNaturalTwoHundredFiftySix byteNaturalTwoHundredFiftySix) def sm86EmptyInstructionBytes = (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) def sm86EncodingErrorOrdinal = (lambda unrestricted error : (family SM86EncodingErrorCode) . (eliminate SM86EncodingErrorCode (lambda unrestricted current : (family SM86EncodingErrorCode) . Nat) error (branch SM86EncodingWordLengthInvalid . (byte-to-nat (byte 1))) (branch SM86EncodingFieldWidthInvalid . (byte-to-nat (byte 2))) (branch SM86EncodingFieldExtentInvalid . (byte-to-nat (byte 3))) (branch SM86EncodingFieldValueOverflow . (byte-to-nat (byte 4))) (branch SM86EncodingControlInvalid . (byte-to-nat (byte 5))))) def sm86EncodingErrorStableCode = (lambda unrestricted error : (family SM86EncodingErrorCode) . (eliminate SM86EncodingErrorCode (lambda unrestricted current : (family SM86EncodingErrorCode) . Bytes) error (branch SM86EncodingWordLengthInvalid . b"ALPHA-SM86-ENC-001") (branch SM86EncodingFieldWidthInvalid . b"ALPHA-SM86-ENC-002") (branch SM86EncodingFieldExtentInvalid . b"ALPHA-SM86-ENC-003") (branch SM86EncodingFieldValueOverflow . b"ALPHA-SM86-ENC-004") (branch SM86EncodingControlInvalid . b"ALPHA-SM86-ENC-005"))) def sm86FieldTelemetryZero = (constructor SM86FieldEncodingTelemetry SM86FieldEncodingTelemetryValue zero zero sm86EncodingNaturalSixteen zero) def sm86FieldTelemetryFailure = (lambda unrestricted outputBytes : Nat . (lambda unrestricted highestExclusiveBit : Nat . (constructor SM86FieldEncodingTelemetry SM86FieldEncodingTelemetryValue zero zero outputBytes highestExclusiveBit))) def sm86FieldTelemetryOne = (lambda unrestricted width : Nat . (lambda unrestricted highestExclusiveBit : Nat . (constructor SM86FieldEncodingTelemetry SM86FieldEncodingTelemetryValue (succ zero) width sm86EncodingNaturalSixteen highestExclusiveBit))) def sm86NaturalMaximum = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalSelect (naturalLessOrEqual left right) right left))) def sm86MergeFieldTelemetry = (lambda unrestricted left : (family SM86FieldEncodingTelemetry) . (lambda unrestricted right : (family SM86FieldEncodingTelemetry) . (eliminate SM86FieldEncodingTelemetry (lambda unrestricted current : (family SM86FieldEncodingTelemetry) . (family SM86FieldEncodingTelemetry)) left (branch SM86FieldEncodingTelemetryValue leftFields leftBits leftBytes leftHighest . (eliminate SM86FieldEncodingTelemetry (lambda unrestricted current : (family SM86FieldEncodingTelemetry) . (family SM86FieldEncodingTelemetry)) right (branch SM86FieldEncodingTelemetryValue rightFields rightBits rightBytes rightHighest . (constructor SM86FieldEncodingTelemetry SM86FieldEncodingTelemetryValue (naturalAdd leftFields rightFields) (naturalAdd leftBits rightBits) rightBytes (sm86NaturalMaximum leftHighest rightHighest)))))))) def sm86ByteAt = (lambda unrestricted index : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . Byte)) (lambda unrestricted input : Bytes . (bytes-head input)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted input : Bytes . Byte) . (lambda unrestricted input : Bytes . (induction (bytes-tail input))))) index)) def sm86ReplaceByteAt = (lambda unrestricted index : Nat . (lambda unrestricted replacement : Byte . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . Bytes)) (lambda unrestricted input : Bytes . (bytes-cons replacement (bytes-tail input))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted input : Bytes . Bytes) . (lambda unrestricted input : Bytes . (bytes-cons (bytes-head input) (induction (bytes-tail input)))))) index))) -- Place ONE bit, given the bit's TARGET position and the bit itself. -- -- This used to take the field's value and a bit index and recover the bit with -- `value / 2^bitIndex mod 2`. That `2^bitIndex` is the reason the encoder could -- not be run: naturals are unary here, so `naturalPowerOfTwo 31` -- what a -- field at bit 31 needs -- materialises a successor chain of 2,147,483,648 -- elements, and the divide beside it is repeated subtraction over that numeral. -- Measured, 2^22 alone took 921 ms; one instruction is 128 such placements. -- -- The caller now threads the value, halving it per bit, so the only power left -- here is `2^(targetBit mod 8)` -- at most 128, because a bit's home inside a -- byte is what it is regardless of how wide the field is. def sm86PlaceBitAt = (lambda unrestricted targetBit : Nat . (lambda unrestricted sourceBit : Nat . (lambda unrestricted encoded : Bytes . (app (lambda unrestricted targetByteIndex : Nat . (app (lambda unrestricted targetBitIndex : Nat . (app (lambda unrestricted targetPower : Nat . (app (lambda unrestricted priorByte : Nat . (app (lambda unrestricted priorBit : Nat . (sm86ReplaceByteAt targetByteIndex (nat-to-byte (naturalAdd (naturalSaturatingSubtract priorByte (naturalMultiply priorBit targetPower)) (naturalMultiply sourceBit targetPower))) encoded)) (naturalModuloUnchecked (naturalDivideUnchecked priorByte targetPower) sm86EncodingNaturalTwo))) (byte-to-nat (sm86ByteAt targetByteIndex encoded)))) (naturalPowerOfTwo targetBitIndex))) (naturalModuloUnchecked targetBit sm86EncodingNaturalEight))) (naturalDivideUnchecked targetBit sm86EncodingNaturalEight))))) -- Place a field's bits, threading the POSITION and the remaining VALUE instead -- of recomputing a power per bit. -- -- The motive is a `pi` over both, because the recursion changes both: each turn -- writes the low bit of the value at the current position, then hands the -- induction the next position and the value halved. The bits are written in -- ascending order into disjoint positions, so the order is not observable -- -- what changed is that no numeral larger than a byte is ever built. def sm86PlaceFieldBitsUnchecked = (lambda unrestricted position : Nat . (lambda unrestricted width : Nat . (lambda unrestricted value : Nat . (lambda unrestricted encoded : Bytes . (app (app (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted currentPosition : Nat . (pi unrestricted currentValue : Nat . (pi unrestricted currentBytes : Bytes . Bytes)))) (lambda unrestricted currentPosition : Nat . (lambda unrestricted currentValue : Nat . (lambda unrestricted currentBytes : Bytes . currentBytes))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted currentPosition : Nat . (pi unrestricted currentValue : Nat . (pi unrestricted currentBytes : Bytes . Bytes))) . (lambda unrestricted currentPosition : Nat . (lambda unrestricted currentValue : Nat . (lambda unrestricted currentBytes : Bytes . (eliminate NaturalDivisionState (lambda unrestricted current : (family NaturalDivisionState) . Bytes) (naturalDivisionState currentValue sm86EncodingNaturalTwo) (branch NaturalDivisionStateValue remainder quotient . (induction (succ currentPosition) quotient (sm86PlaceBitAt currentPosition remainder currentBytes))))))))) width) position) value) encoded))))) def sm86FieldFailure = (lambda unrestricted error : (family SM86EncodingErrorCode) . (lambda unrestricted position : Nat . (lambda unrestricted width : Nat . (lambda unrestricted detail : Nat . (lambda unrestricted outputBytes : Nat . (constructor SM86FieldEncodingResult SM86FieldEncodingFailed error position width detail (sm86FieldTelemetryFailure outputBytes (naturalAdd position width)))))))) def sm86FieldWord32InRange : (pi unrestricted value : Nat . Nat) = (lambda unrestricted value : Nat . (nat-less-than (naturalDivideUnchecked (naturalDivideUnchecked (naturalDivideUnchecked (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix) byteNaturalTwoHundredFiftySix) byteNaturalTwoHundredFiftySix) byteNaturalTwoHundredFiftySix) (succ zero))) -- Only width32 uses the already-qualified base256 range identity. -- Select functions so the unused old power expression is not evaluated. -- Quotient chunks avoid constructing a power larger than one byte. -- For width = 8*q+r, floor(value / 256^q) < 2^r exactly means value < 2^width. def sm86FieldDivideByteChunks = (lambda unrestricted count : Nat . (lambda unrestricted value : Nat . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted remainingValue : Nat . Nat)) (lambda unrestricted remainingValue : Nat . remainingValue) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted remainingValue : Nat . Nat) . (lambda unrestricted remainingValue : Nat . (induction (naturalDivideUnchecked remainingValue byteNaturalTwoHundredFiftySix))))) count) value))) def sm86FieldValueFitsByByteChunks = (lambda unrestricted width : Nat . (lambda unrestricted value : Nat . (eliminate NaturalDivisionState (lambda unrestricted current : (family NaturalDivisionState) . Nat) (naturalDivisionState width sm86EncodingNaturalEight) (branch NaturalDivisionStateValue remainder quotient . (nat-less-than (sm86FieldDivideByteChunks quotient value) (naturalPowerOfTwo remainder)))))) def sm86FieldValueFits = (lambda unrestricted width : Nat . (lambda unrestricted value : Nat . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted ignored : Nat . Nat)) (lambda unrestricted ignored : Nat . (sm86FieldValueFitsByByteChunks width value)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted ignored : Nat . Nat) . (lambda unrestricted ignored : Nat . (sm86FieldWord32InRange value)))) (naturalEqual width (byte-to-nat (byte 32)))) zero))) -- A fixed32 field keeps its already bounded four-byte representation. -- Each reused bit loop sees one byte only; target positions may be unaligned. def sm86PlaceWord32BitsUnchecked = (lambda unrestricted position : Nat . (lambda unrestricted value : (family SM86Unsigned32) . (lambda unrestricted encoded : Bytes . (eliminate SM86Unsigned32 (lambda unrestricted current : (family SM86Unsigned32) . Bytes) value (branch SM86Unsigned32Value byte0 byte1 byte2 byte3 . (sm86PlaceFieldBitsUnchecked (naturalAdd position (byte-to-nat (byte 24))) sm86EncodingNaturalEight (byte-to-nat byte3) (sm86PlaceFieldBitsUnchecked (naturalAdd position sm86EncodingNaturalSixteen) sm86EncodingNaturalEight (byte-to-nat byte2) (sm86PlaceFieldBitsUnchecked (naturalAdd position sm86EncodingNaturalEight) sm86EncodingNaturalEight (byte-to-nat byte1) (sm86PlaceFieldBitsUnchecked position sm86EncodingNaturalEight (byte-to-nat byte0) encoded))))))))) -- The fixed32 constructor makes width/value overflow unrepresentable. -- Keep the old word-length-before-extent error order and one-field telemetry. -- Select thunks so malformed output never invokes the unchecked placement. def sm86PlaceWord32FieldWithValidWord = (lambda unrestricted position : Nat . (lambda unrestricted value : (family SM86Unsigned32) . (lambda unrestricted encoded : Bytes . (app (lambda unrestricted extent : Nat . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult))) (lambda unrestricted ignored : Nat . (sm86FieldFailure (constructor SM86EncodingErrorCode SM86EncodingFieldExtentInvalid) position sm86EncodingNaturalThirtyTwo extent (bytes-length encoded))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) . (lambda unrestricted ignored : Nat . (constructor SM86FieldEncodingResult SM86FieldEncodingSucceeded (sm86PlaceWord32BitsUnchecked position value encoded) (sm86FieldTelemetryOne sm86EncodingNaturalThirtyTwo extent))))) (naturalLessOrEqual extent sm86EncodingNaturalOneHundredTwentyEight)) zero)) (naturalAdd position sm86EncodingNaturalThirtyTwo))))) def sm86PlaceWord32Field = (lambda unrestricted position : Nat . (lambda unrestricted value : (family SM86Unsigned32) . (lambda unrestricted encoded : Bytes . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult))) (lambda unrestricted ignored : Nat . (sm86FieldFailure (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid) position sm86EncodingNaturalThirtyTwo (bytes-length encoded) (bytes-length encoded))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) . (lambda unrestricted ignored : Nat . (sm86PlaceWord32FieldWithValidWord position value encoded)))) (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen)) zero)))) -- The fixed24 payload is exactly three bytes. Reuse the qualified low-to-high -- bit writer; preserve neighboring bits and one-field24-bit telemetry. def sm86PlaceWord24BitsUnchecked = (lambda unrestricted position : Nat . (lambda unrestricted byte0 : Byte . (lambda unrestricted byte1 : Byte . (lambda unrestricted byte2 : Byte . (lambda unrestricted encoded : Bytes . (sm86PlaceFieldBitsUnchecked (naturalAdd position (byte-to-nat (byte 16))) (byte-to-nat (byte 8)) (byte-to-nat byte2) (sm86PlaceFieldBitsUnchecked (naturalAdd position (byte-to-nat (byte 8))) (byte-to-nat (byte 8)) (byte-to-nat byte1) (sm86PlaceFieldBitsUnchecked position (byte-to-nat (byte 8)) (byte-to-nat byte0) encoded)))))))) def sm86PlaceWord24FieldWithValidWord = (lambda unrestricted position : Nat . (lambda unrestricted byte0 : Byte . (lambda unrestricted byte1 : Byte . (lambda unrestricted byte2 : Byte . (lambda unrestricted encoded : Bytes . (app (lambda unrestricted extent : Nat . (app (nat-eliminate (lambda unrestricted condition : Nat . (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult))) (lambda unrestricted ignored : Nat . (sm86FieldFailure (constructor SM86EncodingErrorCode SM86EncodingFieldExtentInvalid) position sm86EncodingNaturalTwentyFour extent (bytes-length encoded))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) . (lambda unrestricted ignored : Nat . (constructor SM86FieldEncodingResult SM86FieldEncodingSucceeded (sm86PlaceWord24BitsUnchecked position byte0 byte1 byte2 encoded) (sm86FieldTelemetryOne sm86EncodingNaturalTwentyFour extent))))) (naturalLessOrEqual extent sm86EncodingNaturalOneHundredTwentyEight)) zero)) (naturalAdd position sm86EncodingNaturalTwentyFour))))))) def sm86PlaceWord24Field = (lambda unrestricted position : Nat . (lambda unrestricted byte0 : Byte . (lambda unrestricted byte1 : Byte . (lambda unrestricted byte2 : Byte . (lambda unrestricted encoded : Bytes . (app (nat-eliminate (lambda unrestricted condition : Nat . (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult))) (lambda unrestricted ignored : Nat . (sm86FieldFailure (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid) position sm86EncodingNaturalTwentyFour (bytes-length encoded) (bytes-length encoded))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) . (lambda unrestricted ignored : Nat . (sm86PlaceWord24FieldWithValidWord position byte0 byte1 byte2 encoded)))) (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen)) zero)))))) def sm86PlaceEncodedField = (lambda unrestricted field : (family SM86EncodedField) . (lambda unrestricted encoded : Bytes . (eliminate SM86EncodedField (lambda unrestricted current : (family SM86EncodedField) . (family SM86FieldEncodingResult)) field (branch SM86EncodedFieldValue position width value . (app (lambda unrestricted extent : Nat . (nat-eliminate (lambda unrestricted wordLengthValid : Nat . (family SM86FieldEncodingResult)) (sm86FieldFailure (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid) position width (bytes-length encoded) (bytes-length encoded)) (lambda unrestricted lengthPredecessor : Nat . (lambda unrestricted lengthInduction : (family SM86FieldEncodingResult) . (nat-eliminate (lambda unrestricted widthValid : Nat . (family SM86FieldEncodingResult)) (sm86FieldFailure (constructor SM86EncodingErrorCode SM86EncodingFieldWidthInvalid) position width width (bytes-length encoded)) (lambda unrestricted widthPredecessor : Nat . (lambda unrestricted widthInduction : (family SM86FieldEncodingResult) . (nat-eliminate (lambda unrestricted extentValid : Nat . (family SM86FieldEncodingResult)) (sm86FieldFailure (constructor SM86EncodingErrorCode SM86EncodingFieldExtentInvalid) position width extent (bytes-length encoded)) (lambda unrestricted extentPredecessor : Nat . (lambda unrestricted extentInduction : (family SM86FieldEncodingResult) . (nat-eliminate (lambda unrestricted valueValid : Nat . (family SM86FieldEncodingResult)) (sm86FieldFailure (constructor SM86EncodingErrorCode SM86EncodingFieldValueOverflow) position width value (bytes-length encoded)) (lambda unrestricted valuePredecessor : Nat . (lambda unrestricted valueInduction : (family SM86FieldEncodingResult) . (constructor SM86FieldEncodingResult SM86FieldEncodingSucceeded (sm86PlaceFieldBitsUnchecked position width value encoded) (sm86FieldTelemetryOne width extent)))) (sm86FieldValueFits width value)))) (naturalLessOrEqual extent sm86EncodingNaturalOneHundredTwentyEight)))) (nat-less-than zero width)))) (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen))) (naturalAdd position width))) (branch SM86EncodedFieldWord32Value position value . (sm86PlaceWord32Field position value encoded)) (branch SM86EncodedFieldWord24Value position byte0 byte1 byte2 . (sm86PlaceWord24Field position byte0 byte1 byte2 encoded))))) def sm86EncodeFieldListFrom = (lambda unrestricted fields : (family SM86EncodedFieldList) . (eliminate SM86EncodedFieldList (lambda unrestricted current : (family SM86EncodedFieldList) . (pi unrestricted encoded : Bytes . (family SM86FieldEncodingResult))) fields (branch SM86EncodedFieldListEmpty . (lambda unrestricted encoded : Bytes . (constructor SM86FieldEncodingResult SM86FieldEncodingSucceeded encoded sm86FieldTelemetryZero))) (branch SM86EncodedFieldListCons field tail ih_tail . (lambda unrestricted encoded : Bytes . (eliminate SM86FieldEncodingResult (lambda unrestricted current : (family SM86FieldEncodingResult) . (family SM86FieldEncodingResult)) (sm86PlaceEncodedField field encoded) (branch SM86FieldEncodingSucceeded placed fieldTelemetry . (eliminate SM86FieldEncodingResult (lambda unrestricted current : (family SM86FieldEncodingResult) . (family SM86FieldEncodingResult)) (ih_tail placed) (branch SM86FieldEncodingSucceeded complete tailTelemetry . (constructor SM86FieldEncodingResult SM86FieldEncodingSucceeded complete (sm86MergeFieldTelemetry fieldTelemetry tailTelemetry))) (branch SM86FieldEncodingFailed error position width detail tailTelemetry . (constructor SM86FieldEncodingResult SM86FieldEncodingFailed error position width detail (sm86MergeFieldTelemetry fieldTelemetry tailTelemetry))))) (branch SM86FieldEncodingFailed error position width detail telemetry . (constructor SM86FieldEncodingResult SM86FieldEncodingFailed error position width detail telemetry))))))) def sm86EncodeFields = (lambda unrestricted fields : (family SM86EncodedFieldList) . (sm86EncodeFieldListFrom fields sm86EmptyInstructionBytes)) def sm86HeaderGuard = (lambda unrestricted guard : (family SM86InstructionGuard) . (eliminate SM86InstructionGuard (lambda unrestricted current : (family SM86InstructionGuard) . (family SM86HeaderGuard)) guard (branch SM86InstructionAlways . (constructor SM86HeaderGuard SM86HeaderGuardValue (byte-to-nat (byte 7)) zero)) (branch SM86InstructionWhen predicate . (constructor SM86HeaderGuard SM86HeaderGuardValue (byte-to-nat (sm86PredicateNumber predicate)) zero)) (branch SM86InstructionWhenNot predicate . (constructor SM86HeaderGuard SM86HeaderGuardValue (byte-to-nat (sm86PredicateNumber predicate)) (succ zero))))) def sm86ControlEncodingNatural = (lambda unrestricted encoded : Bytes . (naturalAdd (byte-to-nat (sm86ByteAt zero encoded)) (naturalAdd (naturalMultiply (byte-to-nat (sm86ByteAt (succ zero) encoded)) byteNaturalTwoHundredFiftySix) (naturalMultiply (byte-to-nat (sm86ByteAt (succ (succ zero)) encoded)) sm86EncodingNaturalSixtyFiveThousandFiveHundredThirtySix)))) def sm86HeaderFields = (lambda unrestricted opcode : Nat . (lambda unrestricted guard : (family SM86HeaderGuard) . (lambda unrestricted controlNatural : Nat . (eliminate SM86HeaderGuard (lambda unrestricted current : (family SM86HeaderGuard) . (family SM86EncodedFieldList)) guard (branch SM86HeaderGuardValue predicate negated . (constructor SM86EncodedFieldList SM86EncodedFieldListCons (constructor SM86EncodedField SM86EncodedFieldValue zero sm86EncodingNaturalTwelve opcode) (constructor SM86EncodedFieldList SM86EncodedFieldListCons (constructor SM86EncodedField SM86EncodedFieldValue sm86EncodingNaturalTwelve sm86EncodingNaturalThree predicate) (constructor SM86EncodedFieldList SM86EncodedFieldListCons (constructor SM86EncodedField SM86EncodedFieldValue sm86EncodingNaturalFifteen (succ zero) negated) (constructor SM86EncodedFieldList SM86EncodedFieldListCons (constructor SM86EncodedField SM86EncodedFieldValue sm86EncodingNaturalOneHundredFive sm86EncodingNaturalTwentyThree controlNatural) (constructor SM86EncodedFieldList SM86EncodedFieldListEmpty)))))))))) def sm86EncodeInstructionHeader = (lambda unrestricted opcode : Nat . (lambda unrestricted guard : (family SM86InstructionGuard) . (lambda unrestricted control : (family SM86Control) . (eliminate SM86ControlEncodingResult (lambda unrestricted current : (family SM86ControlEncodingResult) . (family SM86FieldEncodingResult)) (encodeSM86ControlLE control) (branch SM86ControlEncoded controlBytes . (sm86EncodeFields (sm86HeaderFields opcode (sm86HeaderGuard guard) (sm86ControlEncodingNatural controlBytes)))) (branch SM86ControlEncodingFailed code . (constructor SM86FieldEncodingResult SM86FieldEncodingFailed (constructor SM86EncodingErrorCode SM86EncodingControlInvalid) sm86EncodingNaturalOneHundredFive sm86EncodingNaturalTwentyThree code sm86FieldTelemetryZero))))))