1module Accelerator.SM86.FieldEncoding
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.ControlEncoding
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.Immediate
7import Accelerator.SM86.Types
8import Std.Natural
9import Std.Byte
10
11family SM86EncodingErrorCode : Type 0
12constructor SM86EncodingWordLengthInvalid
13constructor SM86EncodingFieldWidthInvalid
14constructor SM86EncodingFieldExtentInvalid
15constructor SM86EncodingFieldValueOverflow
16constructor SM86EncodingControlInvalid
17
18end-family
19
20family SM86EncodedField : Type 0
21constructor SM86EncodedFieldValue
22field unrestricted sm86EncodedFieldPosition : Nat
23field unrestricted sm86EncodedFieldWidth : Nat
24field unrestricted sm86EncodedFieldValue : Nat
25constructor SM86EncodedFieldWord32Value
26field unrestricted sm86EncodedFieldWord32Position : Nat
27field unrestricted sm86EncodedFieldWord32Value : (family SM86Unsigned32)
28constructor SM86EncodedFieldWord24Value
29field unrestricted sm86EncodedFieldWord24Position : Nat
30field unrestricted sm86EncodedFieldWord24Byte0 : Byte
31field unrestricted sm86EncodedFieldWord24Byte1 : Byte
32field unrestricted sm86EncodedFieldWord24Byte2 : Byte
33
34end-family
35
36family SM86EncodedFieldList : Type 0
37constructor SM86EncodedFieldListEmpty
38constructor SM86EncodedFieldListCons
39field unrestricted sm86EncodedFieldListHead : (family SM86EncodedField)
40recursive unrestricted sm86EncodedFieldListTail
41
42end-family
43
44family SM86FieldEncodingTelemetry : Type 0
45constructor SM86FieldEncodingTelemetryValue
46field unrestricted sm86FieldTelemetryFieldsEncoded : Nat
47field unrestricted sm86FieldTelemetryBitsWritten : Nat
48field unrestricted sm86FieldTelemetryOutputBytes : Nat
49field unrestricted sm86FieldTelemetryHighestExclusiveBit : Nat
50
51end-family
52
53family SM86FieldEncodingResult : Type 0
54constructor SM86FieldEncodingSucceeded
55field unrestricted sm86FieldEncodedBytes : Bytes
56field unrestricted sm86FieldEncodingTelemetry : (family SM86FieldEncodingTelemetry)
57constructor SM86FieldEncodingFailed
58field unrestricted sm86FieldEncodingError : (family SM86EncodingErrorCode)
59field unrestricted sm86FieldEncodingPosition : Nat
60field unrestricted sm86FieldEncodingWidth : Nat
61field unrestricted sm86FieldEncodingDetail : Nat
62field unrestricted sm86FieldFailureTelemetry : (family SM86FieldEncodingTelemetry)
63
64end-family
65
66family SM86HeaderGuard : Type 0
67constructor SM86HeaderGuardValue
68field unrestricted sm86HeaderGuardPredicate : Nat
69field unrestricted sm86HeaderGuardNegated : Nat
70
71end-family
72
73def sm86EncodingNaturalTwo =
74 (byte-to-nat (byte 2))
75
76def sm86EncodingNaturalThree =
77 (byte-to-nat (byte 3))
78
79def sm86EncodingNaturalEight =
80 (byte-to-nat (byte 8))
81
82def sm86EncodingNaturalTwelve =
83 (byte-to-nat (byte 12))
84
85def sm86EncodingNaturalFifteen =
86 (byte-to-nat (byte 15))
87
88def sm86EncodingNaturalSixteen =
89 (byte-to-nat (byte 16))
90
91def sm86EncodingNaturalTwentyFour =
92 (byte-to-nat (byte 24))
93
94def sm86EncodingNaturalThirtyTwo =
95 (byte-to-nat (byte 32))
96
97def sm86EncodingNaturalTwentyThree =
98 (byte-to-nat (byte 23))
99
100def sm86EncodingNaturalOneHundredFive =
101 (byte-to-nat (byte 105))
102
103def sm86EncodingNaturalOneHundredTwentyEight =
104 (byte-to-nat (byte 128))
105
106def sm86EncodingNaturalSixtyFiveThousandFiveHundredThirtySix =
107 (naturalMultiply byteNaturalTwoHundredFiftySix byteNaturalTwoHundredFiftySix)
108
109def sm86EmptyInstructionBytes =
110 (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)
111
112def sm86EncodingErrorOrdinal =
113 (lambda unrestricted error : (family SM86EncodingErrorCode) .
114 (eliminate
115 SM86EncodingErrorCode
116 (lambda unrestricted current : (family SM86EncodingErrorCode) . Nat)
117 error
118 (branch SM86EncodingWordLengthInvalid . (byte-to-nat (byte 1)))
119 (branch SM86EncodingFieldWidthInvalid . (byte-to-nat (byte 2)))
120 (branch SM86EncodingFieldExtentInvalid . (byte-to-nat (byte 3)))
121 (branch SM86EncodingFieldValueOverflow . (byte-to-nat (byte 4)))
122 (branch SM86EncodingControlInvalid . (byte-to-nat (byte 5)))))
123
124def sm86EncodingErrorStableCode =
125 (lambda unrestricted error : (family SM86EncodingErrorCode) .
126 (eliminate
127 SM86EncodingErrorCode
128 (lambda unrestricted current : (family SM86EncodingErrorCode) . Bytes)
129 error
130 (branch
131 SM86EncodingWordLengthInvalid
132 .
133 b"ALPHA-SM86-ENC-001")
134 (branch
135 SM86EncodingFieldWidthInvalid
136 .
137 b"ALPHA-SM86-ENC-002")
138 (branch
139 SM86EncodingFieldExtentInvalid
140 .
141 b"ALPHA-SM86-ENC-003")
142 (branch
143 SM86EncodingFieldValueOverflow
144 .
145 b"ALPHA-SM86-ENC-004")
146 (branch
147 SM86EncodingControlInvalid
148 .
149 b"ALPHA-SM86-ENC-005")))
150
151def sm86FieldTelemetryZero =
152 (constructor
153 SM86FieldEncodingTelemetry
154 SM86FieldEncodingTelemetryValue
155 zero
156 zero
157 sm86EncodingNaturalSixteen
158 zero)
159
160def sm86FieldTelemetryFailure =
161 (lambda unrestricted outputBytes : Nat .
162 (lambda unrestricted highestExclusiveBit : Nat .
163 (constructor
164 SM86FieldEncodingTelemetry
165 SM86FieldEncodingTelemetryValue
166 zero
167 zero
168 outputBytes
169 highestExclusiveBit)))
170
171def sm86FieldTelemetryOne =
172 (lambda unrestricted width : Nat .
173 (lambda unrestricted highestExclusiveBit : Nat .
174 (constructor
175 SM86FieldEncodingTelemetry
176 SM86FieldEncodingTelemetryValue
177 (succ zero)
178 width
179 sm86EncodingNaturalSixteen
180 highestExclusiveBit)))
181
182def sm86NaturalMaximum =
183 (lambda unrestricted left : Nat .
184 (lambda unrestricted right : Nat . (naturalSelect (naturalLessOrEqual left right) right left)))
185
186def sm86MergeFieldTelemetry =
187 (lambda unrestricted left : (family SM86FieldEncodingTelemetry) .
188 (lambda unrestricted right : (family SM86FieldEncodingTelemetry) .
189 (eliminate
190 SM86FieldEncodingTelemetry
191 (lambda unrestricted current : (family SM86FieldEncodingTelemetry) .
192 (family SM86FieldEncodingTelemetry))
193 left
194 (branch
195 SM86FieldEncodingTelemetryValue
196 leftFields
197 leftBits
198 leftBytes
199 leftHighest
200 .
201 (eliminate
202 SM86FieldEncodingTelemetry
203 (lambda unrestricted current : (family SM86FieldEncodingTelemetry) .
204 (family SM86FieldEncodingTelemetry))
205 right
206 (branch
207 SM86FieldEncodingTelemetryValue
208 rightFields
209 rightBits
210 rightBytes
211 rightHighest
212 .
213 (constructor
214 SM86FieldEncodingTelemetry
215 SM86FieldEncodingTelemetryValue
216 (naturalAdd leftFields rightFields)
217 (naturalAdd leftBits rightBits)
218 rightBytes
219 (sm86NaturalMaximum leftHighest rightHighest))))))))
220
221def sm86ByteAt =
222 (lambda unrestricted index : Nat .
223 (nat-eliminate
224 (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . Byte))
225 (lambda unrestricted input : Bytes . (bytes-head input))
226 (lambda unrestricted predecessor : Nat .
227 (lambda unrestricted induction : (pi unrestricted input : Bytes . Byte) .
228 (lambda unrestricted input : Bytes . (induction (bytes-tail input)))))
229 index))
230
231def sm86ReplaceByteAt =
232 (lambda unrestricted index : Nat .
233 (lambda unrestricted replacement : Byte .
234 (nat-eliminate
235 (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . Bytes))
236 (lambda unrestricted input : Bytes . (bytes-cons replacement (bytes-tail input)))
237 (lambda unrestricted predecessor : Nat .
238 (lambda unrestricted induction : (pi unrestricted input : Bytes . Bytes) .
239 (lambda unrestricted input : Bytes .
240 (bytes-cons (bytes-head input) (induction (bytes-tail input))))))
241 index)))
242
243-- Place ONE bit, given the bit's TARGET position and the bit itself.
244--
245-- This used to take the field's value and a bit index and recover the bit with
246-- `value / 2^bitIndex mod 2`. That `2^bitIndex` is the reason the encoder could
247-- not be run: naturals are unary here, so `naturalPowerOfTwo 31` -- what a
248-- field at bit 31 needs -- materialises a successor chain of 2,147,483,648
249-- elements, and the divide beside it is repeated subtraction over that numeral.
250-- Measured, 2^22 alone took 921 ms; one instruction is 128 such placements.
251--
252-- The caller now threads the value, halving it per bit, so the only power left
253-- here is `2^(targetBit mod 8)` -- at most 128, because a bit's home inside a
254-- byte is what it is regardless of how wide the field is.
255def sm86PlaceBitAt =
256 (lambda unrestricted targetBit : Nat .
257 (lambda unrestricted sourceBit : Nat .
258 (lambda unrestricted encoded : Bytes .
259 (app
260 (lambda unrestricted targetByteIndex : Nat .
261 (app
262 (lambda unrestricted targetBitIndex : Nat .
263 (app
264 (lambda unrestricted targetPower : Nat .
265 (app
266 (lambda unrestricted priorByte : Nat .
267 (app
268 (lambda unrestricted priorBit : Nat .
269 (sm86ReplaceByteAt
270 targetByteIndex
271 (nat-to-byte
272 (naturalAdd
273 (naturalSaturatingSubtract
274 priorByte
275 (naturalMultiply priorBit targetPower))
276 (naturalMultiply sourceBit targetPower)))
277 encoded))
278 (naturalModuloUnchecked
279 (naturalDivideUnchecked priorByte targetPower)
280 sm86EncodingNaturalTwo)))
281 (byte-to-nat (sm86ByteAt targetByteIndex encoded))))
282 (naturalPowerOfTwo targetBitIndex)))
283 (naturalModuloUnchecked targetBit sm86EncodingNaturalEight)))
284 (naturalDivideUnchecked targetBit sm86EncodingNaturalEight)))))
285
286-- Place a field's bits, threading the POSITION and the remaining VALUE instead
287-- of recomputing a power per bit.
288--
289-- The motive is a `pi` over both, because the recursion changes both: each turn
290-- writes the low bit of the value at the current position, then hands the
291-- induction the next position and the value halved. The bits are written in
292-- ascending order into disjoint positions, so the order is not observable --
293-- what changed is that no numeral larger than a byte is ever built.
294def sm86PlaceFieldBitsUnchecked =
295 (lambda unrestricted position : Nat .
296 (lambda unrestricted width : Nat .
297 (lambda unrestricted value : Nat .
298 (lambda unrestricted encoded : Bytes .
299 (app
300 (app
301 (app
302 (nat-eliminate
303 (lambda unrestricted current : Nat .
304 (pi unrestricted currentPosition : Nat .
305 (pi unrestricted currentValue : Nat .
306 (pi unrestricted currentBytes : Bytes . Bytes))))
307 (lambda unrestricted currentPosition : Nat .
308 (lambda unrestricted currentValue : Nat .
309 (lambda unrestricted currentBytes : Bytes . currentBytes)))
310 (lambda unrestricted predecessor : Nat .
311 (lambda unrestricted induction : (pi unrestricted currentPosition : Nat . (pi unrestricted currentValue : Nat . (pi unrestricted currentBytes : Bytes . Bytes))) .
312 (lambda unrestricted currentPosition : Nat .
313 (lambda unrestricted currentValue : Nat .
314 (lambda unrestricted currentBytes : Bytes .
315 (eliminate
316 NaturalDivisionState
317 (lambda unrestricted current : (family NaturalDivisionState) . Bytes)
318 (naturalDivisionState currentValue sm86EncodingNaturalTwo)
319 (branch
320 NaturalDivisionStateValue
321 remainder
322 quotient
323 .
324 (induction
325 (succ currentPosition)
326 quotient
327 (sm86PlaceBitAt currentPosition remainder currentBytes)))))))))
328 width)
329 position)
330 value)
331 encoded)))))
332
333def sm86FieldFailure =
334 (lambda unrestricted error : (family SM86EncodingErrorCode) .
335 (lambda unrestricted position : Nat .
336 (lambda unrestricted width : Nat .
337 (lambda unrestricted detail : Nat .
338 (lambda unrestricted outputBytes : Nat .
339 (constructor
340 SM86FieldEncodingResult
341 SM86FieldEncodingFailed
342 error
343 position
344 width
345 detail
346 (sm86FieldTelemetryFailure outputBytes (naturalAdd position width))))))))
347
348def sm86FieldWord32InRange : (pi unrestricted value : Nat . Nat) =
349 (lambda unrestricted value : Nat .
350 (nat-less-than
351 (naturalDivideUnchecked
352 (naturalDivideUnchecked
353 (naturalDivideUnchecked
354 (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)
355 byteNaturalTwoHundredFiftySix)
356 byteNaturalTwoHundredFiftySix)
357 byteNaturalTwoHundredFiftySix)
358 (succ zero)))
359
360-- Only width32 uses the already-qualified base256 range identity.
361-- Select functions so the unused old power expression is not evaluated.
362-- Quotient chunks avoid constructing a power larger than one byte.
363-- For width = 8*q+r, floor(value / 256^q) < 2^r exactly means value < 2^width.
364def sm86FieldDivideByteChunks =
365 (lambda unrestricted count : Nat .
366 (lambda unrestricted value : Nat .
367 (app
368 (nat-eliminate
369 (lambda unrestricted current : Nat . (pi unrestricted remainingValue : Nat . Nat))
370 (lambda unrestricted remainingValue : Nat . remainingValue)
371 (lambda unrestricted predecessor : Nat .
372 (lambda unrestricted induction : (pi unrestricted remainingValue : Nat . Nat) .
373 (lambda unrestricted remainingValue : Nat .
374 (induction (naturalDivideUnchecked remainingValue byteNaturalTwoHundredFiftySix)))))
375 count)
376 value)))
377
378def sm86FieldValueFitsByByteChunks =
379 (lambda unrestricted width : Nat .
380 (lambda unrestricted value : Nat .
381 (eliminate
382 NaturalDivisionState
383 (lambda unrestricted current : (family NaturalDivisionState) . Nat)
384 (naturalDivisionState width sm86EncodingNaturalEight)
385 (branch
386 NaturalDivisionStateValue
387 remainder
388 quotient
389 .
390 (nat-less-than (sm86FieldDivideByteChunks quotient value) (naturalPowerOfTwo remainder))))))
391
392def sm86FieldValueFits =
393 (lambda unrestricted width : Nat .
394 (lambda unrestricted value : Nat .
395 (app
396 (nat-eliminate
397 (lambda unrestricted current : Nat . (pi unrestricted ignored : Nat . Nat))
398 (lambda unrestricted ignored : Nat . (sm86FieldValueFitsByByteChunks width value))
399 (lambda unrestricted predecessor : Nat .
400 (lambda unrestricted induction : (pi unrestricted ignored : Nat . Nat) .
401 (lambda unrestricted ignored : Nat . (sm86FieldWord32InRange value))))
402 (naturalEqual width (byte-to-nat (byte 32))))
403 zero)))
404
405-- A fixed32 field keeps its already bounded four-byte representation.
406-- Each reused bit loop sees one byte only; target positions may be unaligned.
407def sm86PlaceWord32BitsUnchecked =
408 (lambda unrestricted position : Nat .
409 (lambda unrestricted value : (family SM86Unsigned32) .
410 (lambda unrestricted encoded : Bytes .
411 (eliminate
412 SM86Unsigned32
413 (lambda unrestricted current : (family SM86Unsigned32) . Bytes)
414 value
415 (branch
416 SM86Unsigned32Value
417 byte0
418 byte1
419 byte2
420 byte3
421 .
422 (sm86PlaceFieldBitsUnchecked
423 (naturalAdd position (byte-to-nat (byte 24)))
424 sm86EncodingNaturalEight
425 (byte-to-nat byte3)
426 (sm86PlaceFieldBitsUnchecked
427 (naturalAdd position sm86EncodingNaturalSixteen)
428 sm86EncodingNaturalEight
429 (byte-to-nat byte2)
430 (sm86PlaceFieldBitsUnchecked
431 (naturalAdd position sm86EncodingNaturalEight)
432 sm86EncodingNaturalEight
433 (byte-to-nat byte1)
434 (sm86PlaceFieldBitsUnchecked
435 position
436 sm86EncodingNaturalEight
437 (byte-to-nat byte0)
438 encoded)))))))))
439
440-- The fixed32 constructor makes width/value overflow unrepresentable.
441-- Keep the old word-length-before-extent error order and one-field telemetry.
442-- Select thunks so malformed output never invokes the unchecked placement.
443def sm86PlaceWord32FieldWithValidWord =
444 (lambda unrestricted position : Nat .
445 (lambda unrestricted value : (family SM86Unsigned32) .
446 (lambda unrestricted encoded : Bytes .
447 (app
448 (lambda unrestricted extent : Nat .
449 (app
450 (nat-eliminate
451 (lambda unrestricted current : Nat .
452 (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)))
453 (lambda unrestricted ignored : Nat .
454 (sm86FieldFailure
455 (constructor SM86EncodingErrorCode SM86EncodingFieldExtentInvalid)
456 position
457 sm86EncodingNaturalThirtyTwo
458 extent
459 (bytes-length encoded)))
460 (lambda unrestricted predecessor : Nat .
461 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) .
462 (lambda unrestricted ignored : Nat .
463 (constructor
464 SM86FieldEncodingResult
465 SM86FieldEncodingSucceeded
466 (sm86PlaceWord32BitsUnchecked position value encoded)
467 (sm86FieldTelemetryOne sm86EncodingNaturalThirtyTwo extent)))))
468 (naturalLessOrEqual extent sm86EncodingNaturalOneHundredTwentyEight))
469 zero))
470 (naturalAdd position sm86EncodingNaturalThirtyTwo)))))
471
472def sm86PlaceWord32Field =
473 (lambda unrestricted position : Nat .
474 (lambda unrestricted value : (family SM86Unsigned32) .
475 (lambda unrestricted encoded : Bytes .
476 (app
477 (nat-eliminate
478 (lambda unrestricted current : Nat .
479 (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)))
480 (lambda unrestricted ignored : Nat .
481 (sm86FieldFailure
482 (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid)
483 position
484 sm86EncodingNaturalThirtyTwo
485 (bytes-length encoded)
486 (bytes-length encoded)))
487 (lambda unrestricted predecessor : Nat .
488 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) .
489 (lambda unrestricted ignored : Nat .
490 (sm86PlaceWord32FieldWithValidWord position value encoded))))
491 (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen))
492 zero))))
493
494-- The fixed24 payload is exactly three bytes. Reuse the qualified low-to-high
495-- bit writer; preserve neighboring bits and one-field24-bit telemetry.
496def sm86PlaceWord24BitsUnchecked =
497 (lambda unrestricted position : Nat .
498 (lambda unrestricted byte0 : Byte .
499 (lambda unrestricted byte1 : Byte .
500 (lambda unrestricted byte2 : Byte .
501 (lambda unrestricted encoded : Bytes .
502 (sm86PlaceFieldBitsUnchecked
503 (naturalAdd position (byte-to-nat (byte 16)))
504 (byte-to-nat (byte 8))
505 (byte-to-nat byte2)
506 (sm86PlaceFieldBitsUnchecked
507 (naturalAdd position (byte-to-nat (byte 8)))
508 (byte-to-nat (byte 8))
509 (byte-to-nat byte1)
510 (sm86PlaceFieldBitsUnchecked
511 position
512 (byte-to-nat (byte 8))
513 (byte-to-nat byte0)
514 encoded))))))))
515
516def sm86PlaceWord24FieldWithValidWord =
517 (lambda unrestricted position : Nat .
518 (lambda unrestricted byte0 : Byte .
519 (lambda unrestricted byte1 : Byte .
520 (lambda unrestricted byte2 : Byte .
521 (lambda unrestricted encoded : Bytes .
522 (app
523 (lambda unrestricted extent : Nat .
524 (app
525 (nat-eliminate
526 (lambda unrestricted condition : Nat .
527 (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)))
528 (lambda unrestricted ignored : Nat .
529 (sm86FieldFailure
530 (constructor SM86EncodingErrorCode SM86EncodingFieldExtentInvalid)
531 position
532 sm86EncodingNaturalTwentyFour
533 extent
534 (bytes-length encoded)))
535 (lambda unrestricted predecessor : Nat .
536 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) .
537 (lambda unrestricted ignored : Nat .
538 (constructor
539 SM86FieldEncodingResult
540 SM86FieldEncodingSucceeded
541 (sm86PlaceWord24BitsUnchecked position byte0 byte1 byte2 encoded)
542 (sm86FieldTelemetryOne sm86EncodingNaturalTwentyFour extent)))))
543 (naturalLessOrEqual extent sm86EncodingNaturalOneHundredTwentyEight))
544 zero))
545 (naturalAdd position sm86EncodingNaturalTwentyFour)))))))
546
547def sm86PlaceWord24Field =
548 (lambda unrestricted position : Nat .
549 (lambda unrestricted byte0 : Byte .
550 (lambda unrestricted byte1 : Byte .
551 (lambda unrestricted byte2 : Byte .
552 (lambda unrestricted encoded : Bytes .
553 (app
554 (nat-eliminate
555 (lambda unrestricted condition : Nat .
556 (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)))
557 (lambda unrestricted ignored : Nat .
558 (sm86FieldFailure
559 (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid)
560 position
561 sm86EncodingNaturalTwentyFour
562 (bytes-length encoded)
563 (bytes-length encoded)))
564 (lambda unrestricted predecessor : Nat .
565 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) .
566 (lambda unrestricted ignored : Nat .
567 (sm86PlaceWord24FieldWithValidWord position byte0 byte1 byte2 encoded))))
568 (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen))
569 zero))))))
570
571def sm86PlaceEncodedField =
572 (lambda unrestricted field : (family SM86EncodedField) .
573 (lambda unrestricted encoded : Bytes .
574 (eliminate
575 SM86EncodedField
576 (lambda unrestricted current : (family SM86EncodedField) . (family SM86FieldEncodingResult))
577 field
578 (branch
579 SM86EncodedFieldValue
580 position
581 width
582 value
583 .
584 (app
585 (lambda unrestricted extent : Nat .
586 (nat-eliminate
587 (lambda unrestricted wordLengthValid : Nat . (family SM86FieldEncodingResult))
588 (sm86FieldFailure
589 (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid)
590 position
591 width
592 (bytes-length encoded)
593 (bytes-length encoded))
594 (lambda unrestricted lengthPredecessor : Nat .
595 (lambda unrestricted lengthInduction : (family SM86FieldEncodingResult) .
596 (nat-eliminate
597 (lambda unrestricted widthValid : Nat . (family SM86FieldEncodingResult))
598 (sm86FieldFailure
599 (constructor SM86EncodingErrorCode SM86EncodingFieldWidthInvalid)
600 position
601 width
602 width
603 (bytes-length encoded))
604 (lambda unrestricted widthPredecessor : Nat .
605 (lambda unrestricted widthInduction : (family SM86FieldEncodingResult) .
606 (nat-eliminate
607 (lambda unrestricted extentValid : Nat .
608 (family SM86FieldEncodingResult))
609 (sm86FieldFailure
610 (constructor SM86EncodingErrorCode SM86EncodingFieldExtentInvalid)
611 position
612 width
613 extent
614 (bytes-length encoded))
615 (lambda unrestricted extentPredecessor : Nat .
616 (lambda unrestricted extentInduction : (family SM86FieldEncodingResult) .
617 (nat-eliminate
618 (lambda unrestricted valueValid : Nat .
619 (family SM86FieldEncodingResult))
620 (sm86FieldFailure
621 (constructor
622 SM86EncodingErrorCode
623 SM86EncodingFieldValueOverflow)
624 position
625 width
626 value
627 (bytes-length encoded))
628 (lambda unrestricted valuePredecessor : Nat .
629 (lambda unrestricted valueInduction : (family SM86FieldEncodingResult) .
630 (constructor
631 SM86FieldEncodingResult
632 SM86FieldEncodingSucceeded
633 (sm86PlaceFieldBitsUnchecked position width value encoded)
634 (sm86FieldTelemetryOne width extent))))
635 (sm86FieldValueFits width value))))
636 (naturalLessOrEqual extent sm86EncodingNaturalOneHundredTwentyEight))))
637 (nat-less-than zero width))))
638 (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen)))
639 (naturalAdd position width)))
640 (branch
641 SM86EncodedFieldWord32Value
642 position
643 value
644 .
645 (sm86PlaceWord32Field position value encoded))
646 (branch
647 SM86EncodedFieldWord24Value
648 position
649 byte0
650 byte1
651 byte2
652 .
653 (sm86PlaceWord24Field position byte0 byte1 byte2 encoded)))))
654
655def sm86EncodeFieldListFrom =
656 (lambda unrestricted fields : (family SM86EncodedFieldList) .
657 (eliminate
658 SM86EncodedFieldList
659 (lambda unrestricted current : (family SM86EncodedFieldList) .
660 (pi unrestricted encoded : Bytes . (family SM86FieldEncodingResult)))
661 fields
662 (branch
663 SM86EncodedFieldListEmpty
664 .
665 (lambda unrestricted encoded : Bytes .
666 (constructor
667 SM86FieldEncodingResult
668 SM86FieldEncodingSucceeded
669 encoded
670 sm86FieldTelemetryZero)))
671 (branch
672 SM86EncodedFieldListCons
673 field
674 tail
675 ih_tail
676 .
677 (lambda unrestricted encoded : Bytes .
678 (eliminate
679 SM86FieldEncodingResult
680 (lambda unrestricted current : (family SM86FieldEncodingResult) .
681 (family SM86FieldEncodingResult))
682 (sm86PlaceEncodedField field encoded)
683 (branch
684 SM86FieldEncodingSucceeded
685 placed
686 fieldTelemetry
687 .
688 (eliminate
689 SM86FieldEncodingResult
690 (lambda unrestricted current : (family SM86FieldEncodingResult) .
691 (family SM86FieldEncodingResult))
692 (ih_tail placed)
693 (branch
694 SM86FieldEncodingSucceeded
695 complete
696 tailTelemetry
697 .
698 (constructor
699 SM86FieldEncodingResult
700 SM86FieldEncodingSucceeded
701 complete
702 (sm86MergeFieldTelemetry fieldTelemetry tailTelemetry)))
703 (branch
704 SM86FieldEncodingFailed
705 error
706 position
707 width
708 detail
709 tailTelemetry
710 .
711 (constructor
712 SM86FieldEncodingResult
713 SM86FieldEncodingFailed
714 error
715 position
716 width
717 detail
718 (sm86MergeFieldTelemetry fieldTelemetry tailTelemetry)))))
719 (branch
720 SM86FieldEncodingFailed
721 error
722 position
723 width
724 detail
725 telemetry
726 .
727 (constructor
728 SM86FieldEncodingResult
729 SM86FieldEncodingFailed
730 error
731 position
732 width
733 detail
734 telemetry)))))))
735
736def sm86EncodeFields =
737 (lambda unrestricted fields : (family SM86EncodedFieldList) .
738 (sm86EncodeFieldListFrom fields sm86EmptyInstructionBytes))
739
740def sm86HeaderGuard =
741 (lambda unrestricted guard : (family SM86InstructionGuard) .
742 (eliminate
743 SM86InstructionGuard
744 (lambda unrestricted current : (family SM86InstructionGuard) . (family SM86HeaderGuard))
745 guard
746 (branch
747 SM86InstructionAlways
748 .
749 (constructor SM86HeaderGuard SM86HeaderGuardValue (byte-to-nat (byte 7)) zero))
750 (branch
751 SM86InstructionWhen
752 predicate
753 .
754 (constructor
755 SM86HeaderGuard
756 SM86HeaderGuardValue
757 (byte-to-nat (sm86PredicateNumber predicate))
758 zero))
759 (branch
760 SM86InstructionWhenNot
761 predicate
762 .
763 (constructor
764 SM86HeaderGuard
765 SM86HeaderGuardValue
766 (byte-to-nat (sm86PredicateNumber predicate))
767 (succ zero)))))
768
769def sm86ControlEncodingNatural =
770 (lambda unrestricted encoded : Bytes .
771 (naturalAdd
772 (byte-to-nat (sm86ByteAt zero encoded))
773 (naturalAdd
774 (naturalMultiply
775 (byte-to-nat (sm86ByteAt (succ zero) encoded))
776 byteNaturalTwoHundredFiftySix)
777 (naturalMultiply
778 (byte-to-nat (sm86ByteAt (succ (succ zero)) encoded))
779 sm86EncodingNaturalSixtyFiveThousandFiveHundredThirtySix))))
780
781def sm86HeaderFields =
782 (lambda unrestricted opcode : Nat .
783 (lambda unrestricted guard : (family SM86HeaderGuard) .
784 (lambda unrestricted controlNatural : Nat .
785 (eliminate
786 SM86HeaderGuard
787 (lambda unrestricted current : (family SM86HeaderGuard) . (family SM86EncodedFieldList))
788 guard
789 (branch
790 SM86HeaderGuardValue
791 predicate
792 negated
793 .
794 (constructor
795 SM86EncodedFieldList
796 SM86EncodedFieldListCons
797 (constructor
798 SM86EncodedField
799 SM86EncodedFieldValue
800 zero
801 sm86EncodingNaturalTwelve
802 opcode)
803 (constructor
804 SM86EncodedFieldList
805 SM86EncodedFieldListCons
806 (constructor
807 SM86EncodedField
808 SM86EncodedFieldValue
809 sm86EncodingNaturalTwelve
810 sm86EncodingNaturalThree
811 predicate)
812 (constructor
813 SM86EncodedFieldList
814 SM86EncodedFieldListCons
815 (constructor
816 SM86EncodedField
817 SM86EncodedFieldValue
818 sm86EncodingNaturalFifteen
819 (succ zero)
820 negated)
821 (constructor
822 SM86EncodedFieldList
823 SM86EncodedFieldListCons
824 (constructor
825 SM86EncodedField
826 SM86EncodedFieldValue
827 sm86EncodingNaturalOneHundredFive
828 sm86EncodingNaturalTwentyThree
829 controlNatural)
830 (constructor SM86EncodedFieldList SM86EncodedFieldListEmpty))))))))))
831
832def sm86EncodeInstructionHeader =
833 (lambda unrestricted opcode : Nat .
834 (lambda unrestricted guard : (family SM86InstructionGuard) .
835 (lambda unrestricted control : (family SM86Control) .
836 (eliminate
837 SM86ControlEncodingResult
838 (lambda unrestricted current : (family SM86ControlEncodingResult) .
839 (family SM86FieldEncodingResult))
840 (encodeSM86ControlLE control)
841 (branch
842 SM86ControlEncoded
843 controlBytes
844 .
845 (sm86EncodeFields
846 (sm86HeaderFields
847 opcode
848 (sm86HeaderGuard guard)
849 (sm86ControlEncodingNatural controlBytes))))
850 (branch
851 SM86ControlEncodingFailed
852 code
853 .
854 (constructor
855 SM86FieldEncodingResult
856 SM86FieldEncodingFailed
857 (constructor SM86EncodingErrorCode SM86EncodingControlInvalid)
858 sm86EncodingNaturalOneHundredFive
859 sm86EncodingNaturalTwentyThree
860 code
861 sm86FieldTelemetryZero))))))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.