1module Std.Word
2
3import Std.Byte
4import Model.Config
5import Model.Parameter
6import Model.Word32
7import Model.Word64
8import Std.Foundation
9import Std.Codec
10import Std.Natural
11import Data.Bytes
12import Std.Flag
13
14-- Fixed-width integers (Language & Testing Evolution L11, PRD 08 N4). The public
15-- vocabulary aliases the existing word owners; U8/U16, the signed I8..I64
16-- families, div/rem, bit/shift, comparisons, conversions and byte codecs arrive
17-- in L11c/L11d. `Model.Word*` names stay internal until the rename chunk
18-- (NUM-009): `Std.Word` is the public name.
19-- L11r adds division (StdDivision, stdU8..U64DivRem, stdI8..I64DivRem{Checked,Wrapping})
20-- and the checked U32 shifts; see the DIVISION sections below.
21-- I64: a signed 64-bit integer as a DISTINCT two's-complement wrapper over the
22-- unsigned word (L11g). A distinct type keeps signed and unsigned apart in the
23-- type system; the bits are a ModelWord64. Signed comparison/arithmetic (the
24-- subtle two's-complement operations) land next; L11g provides the type,
25-- construction/projection, and bit-equality.
26family StdI64 : Type 0
27constructor StdI64Of
28field unrestricted stdI64Bits : (family ModelWord64)
29
30end-family
31
32-- I8: a signed 8-bit integer as a DISTINCT two's-complement wrapper over the
33-- core Byte (L11i). Its comparisons are the direct core byte primitives (fast).
34family StdI8 : Type 0
35constructor StdI8Of
36field unrestricted stdI8Bits : Byte
37
38end-family
39
40-- I32: a signed 32-bit integer as a DISTINCT two's-complement wrapper over the
41-- unsigned ModelWord32 (L11k).
42family StdI32 : Type 0
43constructor StdI32Of
44field unrestricted stdI32Bits : (family ModelWord32)
45
46end-family
47
48-- U16 / I16: the 16-bit widths (L11l). No Model.Word16 exists, so U16 is a
49-- two-byte record here (field 0 = low byte, field 1 = high byte); I16 is its
50-- distinct two's-complement wrapper.
51family StdU16 : Type 0
52constructor StdU16Of
53field unrestricted stdU16Low : Byte
54field unrestricted stdU16High : Byte
55
56end-family
57
58family StdI16 : Type 0
59constructor StdI16Of
60field unrestricted stdI16Bits : (family StdU16)
61
62end-family
63
64-- DIVISION (L11r, NUM-004). Division is the one arithmetic family with an
65-- error EVERY API must report: x / 0 is an error in checked AND wrapping APIs.
66-- The signed checked API additionally refuses signedMinimum / -1 (the quotient
67-- 2^(width-1) is not representable); the signed WRAPPING API answers it with
68-- (signedMinimum, 0), the two's-complement wrap. Quotients truncate toward
69-- zero and the remainder carries the DIVIDEND's sign (the C / Rust / x86-64
70-- `idiv` convention), so dividend = quotient * divisor + remainder always.
71family StdDivisionErrorCode : Type 0
72constructor StdDivisionByZero
73constructor StdDivisionOverflow
74
75end-family
76
77-- The result of a division: both the quotient and the remainder (one traversal
78-- produces both), or the error. The word type is a parameter (one family for
79-- every width), the same shape as StdOption / StdResult.
80family StdDivision : Type 0
81parameter erased stdDivisionWord : Type 0
82constructor StdDivisionSucceeded
83field unrestricted stdDivisionQuotient : stdDivisionWord
84field unrestricted stdDivisionRemainder : stdDivisionWord
85constructor StdDivisionFailed
86field unrestricted stdDivisionError : (family StdDivisionErrorCode)
87
88end-family
89
90-- Restoring-division state (remainder, quotient, the dividend bits still to
91-- shift in), one family per loop width.
92family StdU64DivisionState : Type 0
93constructor StdU64DivisionStateOf
94field unrestricted stdU64DivisionStateRemainder : (family ModelWord64)
95field unrestricted stdU64DivisionStateQuotient : (family ModelWord64)
96field unrestricted stdU64DivisionStateDividend : (family ModelWord64)
97
98end-family
99
100family StdU32DivisionState : Type 0
101constructor StdU32DivisionStateOf
102field unrestricted stdU32DivisionStateRemainder : (family ModelWord32)
103field unrestricted stdU32DivisionStateQuotient : (family ModelWord32)
104field unrestricted stdU32DivisionStateDividend : (family ModelWord32)
105
106end-family
107
108-- Fully qualified public spellings. The shorter aliases remain source
109-- compatible, but public APIs can now name every unsigned width consistently
110-- without exposing the historical Model.Word implementation owner.
111def StdU8 =
112 Byte
113
114def StdU32 =
115 (family ModelWord32)
116
117def StdU64 =
118 (family ModelWord64)
119
120def U8 =
121 StdU8
122
123def U32 =
124 StdU32
125
126def U64 =
127 StdU64
128
129-- WRAPPING arithmetic (modular). Separate from the checked forms so an optimizer
130-- may not swap them (§6.4).
131def stdU32AddWrapping =
132 modelWord32Add
133
134def stdU64AddWrapping =
135 modelWord64Add
136
137def stdU64SubtractWrapping =
138 modelWord64Subtract
139
140-- CHECKED arithmetic: returns a ModelWord64CheckedResult carrying the
141-- overflow/underflow error code on failure.
142def stdU64AddChecked =
143 modelWord64AddChecked
144
145def stdU64SubtractChecked =
146 modelWord64SubtractChecked
147
148-- BITWISE (no overflow concept). L11c.
149def stdU64And =
150 modelWord64And
151
152def stdU64Xor =
153 modelWord64Xor
154
155def stdU64Not =
156 modelWord64Complement
157
158def stdU32Xor =
159 modelWord32Xor
160
161-- COMPARISON (return the model's boolean flag).
162def stdU64Equal =
163 modelWord64Equal
164
165def stdU64LessThan =
166 modelWord64LessThan
167
168def stdU64IsZero =
169 modelWord64IsZero
170
171-- SHIFTS by one.
172def stdU64ShiftLeftOne =
173 modelWord64ShiftLeftOne
174
175def stdU64ShiftRightOne =
176 modelWord64ShiftRightOne
177
178-- CHECKED multiply (returns a ModelWord64MultiplyCheckedResult).
179def stdU64MultiplyChecked =
180 modelWord64MultiplyChecked
181
182-- U8: the byte-width unsigned integer (L11d). It IS the core `Byte`; its
183-- arithmetic is byte-add-with-carry (Std.Byte), and its comparison/conversion
184-- are the core byte primitives, exposed here under the width vocabulary. The
185-- signed families I8..I64 (two's complement) and U16 land in L11e.
186def stdU8Equal =
187 (lambda unrestricted a : U8 . (lambda unrestricted b : U8 . (byte-equal a b)))
188
189def stdU8LessThan =
190 (lambda unrestricted a : U8 . (lambda unrestricted b : U8 . (byte-less-than a b)))
191
192def stdU8ToNatural =
193 (lambda unrestricted a : U8 . (byte-to-nat a))
194
195-- SHIFTS by n and BIT-POSITION queries (L11e), aliasing the proven Model ops.
196def stdU32ShiftLeft =
197 modelWord32ShiftLeft
198
199def stdU32ShiftRight =
200 modelWord32ShiftRight
201
202def stdU32LeastBit =
203 modelWord32LeastBit
204
205def stdU32ToNatural =
206 modelWord32ToNatural
207
208def stdU64HighBit =
209 modelWord64HighBit
210
211def stdU64LeastBit =
212 modelWord64LeastBit
213
214-- I64 signed wrapper (L11g): type + construction/projection + bit-equality.
215def I64 =
216 (family StdI64)
217
218def stdI64FromWord =
219 (lambda unrestricted bits : (family ModelWord64) . (constructor StdI64 StdI64Of bits))
220
221def stdI64ToWord =
222 (lambda unrestricted value : (family StdI64) .
223 (eliminate
224 StdI64
225 (lambda unrestricted current : (family StdI64) . (family ModelWord64))
226 value
227 (branch StdI64Of bits . bits)))
228
229def stdI64BitsEqual =
230 (lambda unrestricted a : (family StdI64) .
231 (lambda unrestricted b : (family StdI64) . (modelWord64Equal (stdI64ToWord a) (stdI64ToWord b))))
232
233-- I64 SIGNED comparison (two's complement, L11h). If the sign bits differ the
234-- negative operand is less; if they agree, the unsigned order IS the signed
235-- order. Returns the Nat flag ((succ zero) = less). Distinct from stdU64LessThan
236-- (NUM-004: signed vs unsigned comparisons are distinct).
237def stdI64LessThan =
238 (lambda unrestricted a : (family StdI64) .
239 (lambda unrestricted b : (family StdI64) .
240 (nat-eliminate
241 (lambda unrestricted current : Nat . Nat)
242 (nat-eliminate
243 (lambda unrestricted current : Nat . Nat)
244 (modelWord64LessThan (stdI64ToWord a) (stdI64ToWord b))
245 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
246 (modelWord64HighBit (stdI64ToWord b)))
247 (lambda unrestricted predecessor : Nat .
248 (lambda unrestricted induction : Nat .
249 (nat-eliminate
250 (lambda unrestricted current : Nat . Nat)
251 (succ zero)
252 (lambda unrestricted predecessorB : Nat .
253 (lambda unrestricted inductionB : Nat .
254 (modelWord64LessThan (stdI64ToWord a) (stdI64ToWord b))))
255 (modelWord64HighBit (stdI64ToWord b)))))
256 (modelWord64HighBit (stdI64ToWord a)))))
257
258-- I64 signed add / subtract: in two's complement these ARE the wrapping bit ops
259-- on the underlying word (the sign falls out of the representation).
260def stdI64AddWrapping =
261 (lambda unrestricted a : (family StdI64) .
262 (lambda unrestricted b : (family StdI64) .
263 (stdI64FromWord (modelWord64Add (stdI64ToWord a) (stdI64ToWord b)))))
264
265def stdI64SubtractWrapping =
266 (lambda unrestricted a : (family StdI64) .
267 (lambda unrestricted b : (family StdI64) .
268 (stdI64FromWord (modelWord64Subtract (stdI64ToWord a) (stdI64ToWord b)))))
269
270-- I8 signed wrapper (L11i): type, construction/projection, bit-equality,
271-- two's-complement signed comparison, wrapping add.
272def I8 =
273 (family StdI8)
274
275def stdI8FromByte =
276 (lambda unrestricted bits : Byte . (constructor StdI8 StdI8Of bits))
277
278def stdI8ToByte =
279 (lambda unrestricted value : (family StdI8) .
280 (eliminate
281 StdI8
282 (lambda unrestricted current : (family StdI8) . Byte)
283 value
284 (branch StdI8Of bits . bits)))
285
286def stdI8BitsEqual =
287 (lambda unrestricted a : (family StdI8) .
288 (lambda unrestricted b : (family StdI8) . (byte-equal (stdI8ToByte a) (stdI8ToByte b))))
289
290-- sign test: a byte is NON-negative iff it is below 128 (flag 1 = non-negative)
291def stdI8IsNonNegative =
292 (lambda unrestricted value : (family StdI8) . (byte-less-than (stdI8ToByte value) (byte 128)))
293
294-- signed order: if the signs differ the negative operand is less; if they agree
295-- the unsigned byte order IS the signed order.
296def stdI8LessThan =
297 (lambda unrestricted a : (family StdI8) .
298 (lambda unrestricted b : (family StdI8) .
299 (nat-eliminate
300 (lambda unrestricted current : Nat . Nat)
301 (nat-eliminate
302 (lambda unrestricted current : Nat . Nat)
303 (byte-less-than (stdI8ToByte a) (stdI8ToByte b))
304 (lambda unrestricted predecessor : Nat .
305 (lambda unrestricted induction : Nat . (succ zero)))
306 (stdI8IsNonNegative b))
307 (lambda unrestricted predecessor : Nat .
308 (lambda unrestricted induction : Nat .
309 (nat-eliminate
310 (lambda unrestricted current : Nat . Nat)
311 zero
312 (lambda unrestricted predecessorB : Nat .
313 (lambda unrestricted inductionB : Nat .
314 (byte-less-than (stdI8ToByte a) (stdI8ToByte b))))
315 (stdI8IsNonNegative b))))
316 (stdI8IsNonNegative a))))
317
318-- wrapping add: the byte sum, carry discarded (two's complement wraps mod 256)
319def stdI8AddWrapping =
320 (lambda unrestricted a : (family StdI8) .
321 (lambda unrestricted b : (family StdI8) .
322 (eliminate
323 ByteAddResult
324 (lambda unrestricted current : (family ByteAddResult) . (family StdI8))
325 (byteAddWithCarry (stdI8ToByte a) (stdI8ToByte b) zero)
326 (branch ByteAddResultValue sum carry . (constructor StdI8 StdI8Of sum)))))
327
328-- Nat-flag logic ((succ zero) = true). L11k.
329-- Both delegate to the one owner (Std.Flag): alpha-equivalent to
330-- inferenceFlagAnd/inferenceFlagOr (differing only in the parameter
331-- names), found by `alpha-ast duplicates --alpha-equivalent` (L24y).
332def stdFlagAnd =
333 inferenceFlagAnd
334
335def stdFlagOr =
336 inferenceFlagOr
337
338-- U32 comparison primitives (L11k). Model.Word32 is frozen and lacks them, so
339-- they are built here over its four byte fields (field 0 = low byte, field 3 =
340-- high byte, the carry direction of modelWord32Add) with the core byte ops.
341def stdU32IsZero =
342 (lambda unrestricted value : (family ModelWord32) .
343 (eliminate
344 ModelWord32
345 (lambda unrestricted current : (family ModelWord32) . Nat)
346 value
347 (branch
348 ModelWord32Value
349 b0
350 b1
351 b2
352 b3
353 .
354 (stdFlagAnd
355 (byte-equal b0 (byte 0))
356 (stdFlagAnd
357 (byte-equal b1 (byte 0))
358 (stdFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0))))))))
359
360def stdU32Equal =
361 (lambda unrestricted a : (family ModelWord32) .
362 (lambda unrestricted b : (family ModelWord32) . (stdU32IsZero (modelWord32Xor a b))))
363
364-- the sign bit of the high byte (1 = the byte is >= 128)
365def stdU32HighBit =
366 (lambda unrestricted value : (family ModelWord32) .
367 (eliminate
368 ModelWord32
369 (lambda unrestricted current : (family ModelWord32) . Nat)
370 value
371 (branch
372 ModelWord32Value
373 b0
374 b1
375 b2
376 b3
377 .
378 (nat-eliminate
379 (lambda unrestricted current : Nat . Nat)
380 (succ zero)
381 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
382 (byte-less-than b3 (byte 128))))))
383
384-- unsigned order: lexicographic from the high byte down
385def stdU32LessThan =
386 (lambda unrestricted a : (family ModelWord32) .
387 (lambda unrestricted b : (family ModelWord32) .
388 (eliminate
389 ModelWord32
390 (lambda unrestricted current : (family ModelWord32) . Nat)
391 a
392 (branch
393 ModelWord32Value
394 a0
395 a1
396 a2
397 a3
398 .
399 (eliminate
400 ModelWord32
401 (lambda unrestricted current : (family ModelWord32) . Nat)
402 b
403 (branch
404 ModelWord32Value
405 b0
406 b1
407 b2
408 b3
409 .
410 (stdFlagOr
411 (byte-less-than a3 b3)
412 (stdFlagAnd
413 (byte-equal a3 b3)
414 (stdFlagOr
415 (byte-less-than a2 b2)
416 (stdFlagAnd
417 (byte-equal a2 b2)
418 (stdFlagOr
419 (byte-less-than a1 b1)
420 (stdFlagAnd (byte-equal a1 b1) (byte-less-than a0 b0)))))))))))))
421
422-- I32 signed wrapper (L11k): the I64 pattern over ModelWord32.
423def I32 =
424 (family StdI32)
425
426def stdI32FromWord =
427 (lambda unrestricted bits : (family ModelWord32) . (constructor StdI32 StdI32Of bits))
428
429def stdI32ToWord =
430 (lambda unrestricted value : (family StdI32) .
431 (eliminate
432 StdI32
433 (lambda unrestricted current : (family StdI32) . (family ModelWord32))
434 value
435 (branch StdI32Of bits . bits)))
436
437def stdI32BitsEqual =
438 (lambda unrestricted a : (family StdI32) .
439 (lambda unrestricted b : (family StdI32) . (stdU32Equal (stdI32ToWord a) (stdI32ToWord b))))
440
441def stdI32LessThan =
442 (lambda unrestricted a : (family StdI32) .
443 (lambda unrestricted b : (family StdI32) .
444 (nat-eliminate
445 (lambda unrestricted current : Nat . Nat)
446 (nat-eliminate
447 (lambda unrestricted current : Nat . Nat)
448 (stdU32LessThan (stdI32ToWord a) (stdI32ToWord b))
449 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
450 (stdU32HighBit (stdI32ToWord b)))
451 (lambda unrestricted predecessor : Nat .
452 (lambda unrestricted induction : Nat .
453 (nat-eliminate
454 (lambda unrestricted current : Nat . Nat)
455 (succ zero)
456 (lambda unrestricted predecessorB : Nat .
457 (lambda unrestricted inductionB : Nat .
458 (stdU32LessThan (stdI32ToWord a) (stdI32ToWord b))))
459 (stdU32HighBit (stdI32ToWord b)))))
460 (stdU32HighBit (stdI32ToWord a)))))
461
462def stdI32AddWrapping =
463 (lambda unrestricted a : (family StdI32) .
464 (lambda unrestricted b : (family StdI32) .
465 (stdI32FromWord (modelWord32Add (stdI32ToWord a) (stdI32ToWord b)))))
466
467-- U16 (L11l): construction and the byte-lexicographic primitives.
468def U16 =
469 (family StdU16)
470
471def stdU16FromBytes =
472 (lambda unrestricted low : Byte .
473 (lambda unrestricted high : Byte . (constructor StdU16 StdU16Of low high)))
474
475def stdU16IsZero =
476 (lambda unrestricted value : (family StdU16) .
477 (eliminate
478 StdU16
479 (lambda unrestricted current : (family StdU16) . Nat)
480 value
481 (branch StdU16Of low high . (stdFlagAnd (byte-equal low (byte 0)) (byte-equal high (byte 0))))))
482
483def stdU16Equal =
484 (lambda unrestricted a : (family StdU16) .
485 (lambda unrestricted b : (family StdU16) .
486 (eliminate
487 StdU16
488 (lambda unrestricted current : (family StdU16) . Nat)
489 a
490 (branch
491 StdU16Of
492 aLow
493 aHigh
494 .
495 (eliminate
496 StdU16
497 (lambda unrestricted current : (family StdU16) . Nat)
498 b
499 (branch
500 StdU16Of
501 bLow
502 bHigh
503 .
504 (stdFlagAnd (byte-equal aLow bLow) (byte-equal aHigh bHigh))))))))
505
506def stdU16HighBit =
507 (lambda unrestricted value : (family StdU16) .
508 (eliminate
509 StdU16
510 (lambda unrestricted current : (family StdU16) . Nat)
511 value
512 (branch
513 StdU16Of
514 low
515 high
516 .
517 (nat-eliminate
518 (lambda unrestricted current : Nat . Nat)
519 (succ zero)
520 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
521 (byte-less-than high (byte 128))))))
522
523def stdU16LessThan =
524 (lambda unrestricted a : (family StdU16) .
525 (lambda unrestricted b : (family StdU16) .
526 (eliminate
527 StdU16
528 (lambda unrestricted current : (family StdU16) . Nat)
529 a
530 (branch
531 StdU16Of
532 aLow
533 aHigh
534 .
535 (eliminate
536 StdU16
537 (lambda unrestricted current : (family StdU16) . Nat)
538 b
539 (branch
540 StdU16Of
541 bLow
542 bHigh
543 .
544 (stdFlagOr
545 (byte-less-than aHigh bHigh)
546 (stdFlagAnd (byte-equal aHigh bHigh) (byte-less-than aLow bLow)))))))))
547
548-- I16 signed wrapper (L11l): the verified I64/I32 pattern over StdU16.
549def I16 =
550 (family StdI16)
551
552def stdI16FromU16 =
553 (lambda unrestricted bits : (family StdU16) . (constructor StdI16 StdI16Of bits))
554
555def stdI16ToU16 =
556 (lambda unrestricted value : (family StdI16) .
557 (eliminate
558 StdI16
559 (lambda unrestricted current : (family StdI16) . (family StdU16))
560 value
561 (branch StdI16Of bits . bits)))
562
563def stdI16BitsEqual =
564 (lambda unrestricted a : (family StdI16) .
565 (lambda unrestricted b : (family StdI16) . (stdU16Equal (stdI16ToU16 a) (stdI16ToU16 b))))
566
567def stdI16LessThan =
568 (lambda unrestricted a : (family StdI16) .
569 (lambda unrestricted b : (family StdI16) .
570 (nat-eliminate
571 (lambda unrestricted current : Nat . Nat)
572 (nat-eliminate
573 (lambda unrestricted current : Nat . Nat)
574 (stdU16LessThan (stdI16ToU16 a) (stdI16ToU16 b))
575 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
576 (stdU16HighBit (stdI16ToU16 b)))
577 (lambda unrestricted predecessor : Nat .
578 (lambda unrestricted induction : Nat .
579 (nat-eliminate
580 (lambda unrestricted current : Nat . Nat)
581 (succ zero)
582 (lambda unrestricted predecessorB : Nat .
583 (lambda unrestricted inductionB : Nat .
584 (stdU16LessThan (stdI16ToU16 a) (stdI16ToU16 b))))
585 (stdU16HighBit (stdI16ToU16 b)))))
586 (stdU16HighBit (stdI16ToU16 a)))))
587
588-- CONVERSIONS (L11l, NUM-005): sign-extension and narrowing are byte assembly,
589-- never a round trip through Natural (which would be unary).
590-- the byte that extends a sign: 0xff for negative, 0x00 for non-negative
591def stdI8SignByte =
592 (lambda unrestricted value : (family StdI8) .
593 (nat-eliminate
594 (lambda unrestricted current : Nat . Byte)
595 (byte 255)
596 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Byte . (byte 0)))
597 (stdI8IsNonNegative value)))
598
599def stdI8ToI16 =
600 (lambda unrestricted value : (family StdI8) .
601 (stdI16FromU16 (stdU16FromBytes (stdI8ToByte value) (stdI8SignByte value))))
602
603def stdI8ToI32 =
604 (lambda unrestricted value : (family StdI8) .
605 (stdI32FromWord
606 (constructor
607 ModelWord32
608 ModelWord32Value
609 (stdI8ToByte value)
610 (stdI8SignByte value)
611 (stdI8SignByte value)
612 (stdI8SignByte value))))
613
614def stdI16ToI32 =
615 (lambda unrestricted value : (family StdI16) .
616 (eliminate
617 StdU16
618 (lambda unrestricted current : (family StdU16) . (family StdI32))
619 (stdI16ToU16 value)
620 (branch
621 StdU16Of
622 low
623 high
624 .
625 (stdI32FromWord
626 (constructor
627 ModelWord32
628 ModelWord32Value
629 low
630 high
631 (nat-eliminate
632 (lambda unrestricted current : Nat . Byte)
633 (byte 255)
634 (lambda unrestricted predecessor : Nat .
635 (lambda unrestricted induction : Byte . (byte 0)))
636 (byte-less-than high (byte 128)))
637 (nat-eliminate
638 (lambda unrestricted current : Nat . Byte)
639 (byte 255)
640 (lambda unrestricted predecessor : Nat .
641 (lambda unrestricted induction : Byte . (byte 0)))
642 (byte-less-than high (byte 128))))))))
643
644-- narrowing keeps the low bytes (wrapping semantics; a checked narrow is later)
645def stdI32ToI8 =
646 (lambda unrestricted value : (family StdI32) .
647 (eliminate
648 ModelWord32
649 (lambda unrestricted current : (family ModelWord32) . (family StdI8))
650 (stdI32ToWord value)
651 (branch ModelWord32Value b0 b1 b2 b3 . (stdI8FromByte b0))))
652
653def stdI16ToI8 =
654 (lambda unrestricted value : (family StdI16) .
655 (eliminate
656 StdU16
657 (lambda unrestricted current : (family StdU16) . (family StdI8))
658 (stdI16ToU16 value)
659 (branch StdU16Of low high . (stdI8FromByte low))))
660
661-- CHECKED NARROWING (L11n, NUM-005): `StdSome` exactly when the value is
662-- representable at the narrower width, `StdNone` otherwise (the wrapping
663-- narrows above keep the low bytes regardless). Unsigned: every dropped byte
664-- must be zero. Signed: every dropped byte must equal the sign byte of the
665-- kept part, so the value sign-extends back to itself.
666def stdU16ToU8Checked =
667 (lambda unrestricted value : (family StdU16) .
668 (eliminate
669 StdU16
670 (lambda unrestricted current : (family StdU16) . (family StdOption Byte))
671 value
672 (branch
673 StdU16Of
674 low
675 high
676 .
677 (nat-eliminate
678 (lambda unrestricted current : Nat . (family StdOption Byte))
679 (constructor StdOption StdNone Byte)
680 (lambda unrestricted predecessor : Nat .
681 (lambda unrestricted induction : (family StdOption Byte) .
682 (constructor StdOption StdSome Byte low)))
683 (byte-equal high (byte 0))))))
684
685def stdU32ToU8Checked =
686 (lambda unrestricted value : (family ModelWord32) .
687 (eliminate
688 ModelWord32
689 (lambda unrestricted current : (family ModelWord32) . (family StdOption Byte))
690 value
691 (branch
692 ModelWord32Value
693 b0
694 b1
695 b2
696 b3
697 .
698 (nat-eliminate
699 (lambda unrestricted current : Nat . (family StdOption Byte))
700 (constructor StdOption StdNone Byte)
701 (lambda unrestricted predecessor : Nat .
702 (lambda unrestricted induction : (family StdOption Byte) .
703 (constructor StdOption StdSome Byte b0)))
704 (stdFlagAnd
705 (byte-equal b1 (byte 0))
706 (stdFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0))))))))
707
708def stdU32ToU16Checked =
709 (lambda unrestricted value : (family ModelWord32) .
710 (eliminate
711 ModelWord32
712 (lambda unrestricted current : (family ModelWord32) . (family StdOption (family StdU16)))
713 value
714 (branch
715 ModelWord32Value
716 b0
717 b1
718 b2
719 b3
720 .
721 (nat-eliminate
722 (lambda unrestricted current : Nat . (family StdOption (family StdU16)))
723 (constructor StdOption StdNone (family StdU16))
724 (lambda unrestricted predecessor : Nat .
725 (lambda unrestricted induction : (family StdOption (family StdU16)) .
726 (constructor StdOption StdSome (family StdU16) (stdU16FromBytes b0 b1))))
727 (stdFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0)))))))
728
729def stdU64ToU32Checked =
730 (lambda unrestricted value : (family ModelWord64) .
731 (eliminate
732 ModelWord64
733 (lambda unrestricted current : (family ModelWord64) . (family StdOption (family ModelWord32)))
734 value
735 (branch
736 ModelWord64Value
737 b0
738 b1
739 b2
740 b3
741 b4
742 b5
743 b6
744 b7
745 .
746 (nat-eliminate
747 (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
748 (constructor StdOption StdNone (family ModelWord32))
749 (lambda unrestricted predecessor : Nat .
750 (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
751 (constructor
752 StdOption
753 StdSome
754 (family ModelWord32)
755 (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3))))
756 (stdFlagAnd
757 (byte-equal b4 (byte 0))
758 (stdFlagAnd
759 (byte-equal b5 (byte 0))
760 (stdFlagAnd (byte-equal b6 (byte 0)) (byte-equal b7 (byte 0)))))))))
761
762def stdI16ToI8Checked =
763 (lambda unrestricted value : (family StdI16) .
764 (eliminate
765 StdU16
766 (lambda unrestricted current : (family StdU16) . (family StdOption (family StdI8)))
767 (stdI16ToU16 value)
768 (branch
769 StdU16Of
770 low
771 high
772 .
773 (nat-eliminate
774 (lambda unrestricted current : Nat . (family StdOption (family StdI8)))
775 (constructor StdOption StdNone (family StdI8))
776 (lambda unrestricted predecessor : Nat .
777 (lambda unrestricted induction : (family StdOption (family StdI8)) .
778 (constructor StdOption StdSome (family StdI8) (stdI8FromByte low))))
779 (byte-equal high (stdI8SignByte (stdI8FromByte low)))))))
780
781def stdI32ToI8Checked =
782 (lambda unrestricted value : (family StdI32) .
783 (eliminate
784 ModelWord32
785 (lambda unrestricted current : (family ModelWord32) . (family StdOption (family StdI8)))
786 (stdI32ToWord value)
787 (branch
788 ModelWord32Value
789 b0
790 b1
791 b2
792 b3
793 .
794 (app
795 (lambda unrestricted sign : Byte .
796 (nat-eliminate
797 (lambda unrestricted current : Nat . (family StdOption (family StdI8)))
798 (constructor StdOption StdNone (family StdI8))
799 (lambda unrestricted predecessor : Nat .
800 (lambda unrestricted induction : (family StdOption (family StdI8)) .
801 (constructor StdOption StdSome (family StdI8) (stdI8FromByte b0))))
802 (stdFlagAnd
803 (byte-equal b1 sign)
804 (stdFlagAnd (byte-equal b2 sign) (byte-equal b3 sign)))))
805 (stdI8SignByte (stdI8FromByte b0))))))
806
807def stdI32ToI16Checked =
808 (lambda unrestricted value : (family StdI32) .
809 (eliminate
810 ModelWord32
811 (lambda unrestricted current : (family ModelWord32) . (family StdOption (family StdI16)))
812 (stdI32ToWord value)
813 (branch
814 ModelWord32Value
815 b0
816 b1
817 b2
818 b3
819 .
820 (app
821 (lambda unrestricted sign : Byte .
822 (nat-eliminate
823 (lambda unrestricted current : Nat . (family StdOption (family StdI16)))
824 (constructor StdOption StdNone (family StdI16))
825 (lambda unrestricted predecessor : Nat .
826 (lambda unrestricted induction : (family StdOption (family StdI16)) .
827 (constructor
828 StdOption
829 StdSome
830 (family StdI16)
831 (stdI16FromU16 (stdU16FromBytes b0 b1)))))
832 (stdFlagAnd (byte-equal b2 sign) (byte-equal b3 sign))))
833 (stdI8SignByte (stdI8FromByte b1))))))
834
835def stdI64ToI32Checked =
836 (lambda unrestricted value : (family StdI64) .
837 (eliminate
838 ModelWord64
839 (lambda unrestricted current : (family ModelWord64) . (family StdOption (family StdI32)))
840 (stdI64ToWord value)
841 (branch
842 ModelWord64Value
843 b0
844 b1
845 b2
846 b3
847 b4
848 b5
849 b6
850 b7
851 .
852 (app
853 (lambda unrestricted sign : Byte .
854 (nat-eliminate
855 (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
856 (constructor StdOption StdNone (family StdI32))
857 (lambda unrestricted predecessor : Nat .
858 (lambda unrestricted induction : (family StdOption (family StdI32)) .
859 (constructor
860 StdOption
861 StdSome
862 (family StdI32)
863 (stdI32FromWord (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3)))))
864 (stdFlagAnd
865 (byte-equal b4 sign)
866 (stdFlagAnd
867 (byte-equal b5 sign)
868 (stdFlagAnd (byte-equal b6 sign) (byte-equal b7 sign))))))
869 (stdI8SignByte (stdI8FromByte b3))))))
870
871-- U8 ARITHMETIC (L11p, REG-012): the owner is Std.Byte's byteAddWithCarry
872-- (low byte + carry flag). Wrapping keeps the low byte; checked is absent
873-- exactly when the carry is set (255 + 1 -> None; 254 + 1 -> Some 255).
874def stdU8AddWrapping =
875 (lambda unrestricted a : Byte .
876 (lambda unrestricted b : Byte .
877 (eliminate
878 ByteAddResult
879 (lambda unrestricted current : (family ByteAddResult) . Byte)
880 (byteAddWithCarry a b zero)
881 (branch ByteAddResultValue low carry . low))))
882
883def stdU8AddChecked =
884 (lambda unrestricted a : Byte .
885 (lambda unrestricted b : Byte .
886 (eliminate
887 ByteAddResult
888 (lambda unrestricted current : (family ByteAddResult) . (family StdOption Byte))
889 (byteAddWithCarry a b zero)
890 (branch
891 ByteAddResultValue
892 low
893 carry
894 .
895 (nat-eliminate
896 (lambda unrestricted current : Nat . (family StdOption Byte))
897 (constructor StdOption StdSome Byte low)
898 (lambda unrestricted predecessor : Nat .
899 (lambda unrestricted induction : (family StdOption Byte) .
900 (constructor StdOption StdNone Byte)))
901 carry)))))
902
903-- CODECS (L11o, NUM-008). The OWNER of the fixed-width LE/BE codecs is
904-- Data.Bytes (evidence/language-testing/L11n-codec-owner-audit.md); these are
905-- the width-vocabulary names for its functions, never a second implementation.
906-- Encode* : value -> Bytes (byte assembly; LE = byte 0 first, BE = last)
907-- Read* : bounded read -> value + the remaining input, or InputTooShort
908-- Decode*Exact : canonical decode -> value only when the input is EXACTLY the
909-- width (short AND trailing input -> MalformedLength)
910def stdU32EncodeLE =
911 dataBytesWord32LE
912
913def stdU32EncodeBE =
914 dataBytesWord32BE
915
916def stdU64EncodeLE =
917 dataBytesWord64LE
918
919def stdU64EncodeBE =
920 dataBytesWord64BE
921
922def stdU32ReadLE =
923 dataBytesReadWord32LE
924
925def stdU32ReadBE =
926 dataBytesReadWord32BE
927
928def stdU64ReadLE =
929 dataBytesReadWord64LE
930
931def stdU64ReadBE =
932 dataBytesReadWord64BE
933
934def stdU32DecodeLEExact =
935 dataBytesDecodeWord32LEExact
936
937def stdU32DecodeBEExact =
938 dataBytesDecodeWord32BEExact
939
940def stdU64DecodeLEExact =
941 dataBytesDecodeWord64LEExact
942
943def stdU64DecodeBEExact =
944 dataBytesDecodeWord64BEExact
945
946-- answers of the owner's result families under the vocabulary: value-or,
947-- remaining input (empty on failure), and a failed flag (1 = failed)
948def stdU32ReadValueOr =
949 (lambda unrestricted fallback : (family ModelWord32) .
950 (lambda unrestricted result : (family DataBytesWord32DecodeResult) .
951 (eliminate
952 DataBytesWord32DecodeResult
953 (lambda unrestricted current : (family DataBytesWord32DecodeResult) . (family ModelWord32))
954 result
955 (branch DataBytesWord32Decoded value remaining . value)
956 (branch DataBytesWord32DecodeFailed code . fallback))))
957
958def stdU32ReadRemaining =
959 (lambda unrestricted result : (family DataBytesWord32DecodeResult) .
960 (eliminate
961 DataBytesWord32DecodeResult
962 (lambda unrestricted current : (family DataBytesWord32DecodeResult) . Bytes)
963 result
964 (branch DataBytesWord32Decoded value remaining . remaining)
965 (branch DataBytesWord32DecodeFailed code . b"")))
966
967def stdU32ReadFailed =
968 (lambda unrestricted result : (family DataBytesWord32DecodeResult) .
969 (eliminate
970 DataBytesWord32DecodeResult
971 (lambda unrestricted current : (family DataBytesWord32DecodeResult) . Nat)
972 result
973 (branch DataBytesWord32Decoded value remaining . zero)
974 (branch DataBytesWord32DecodeFailed code . (succ zero))))
975
976def stdU32ExactValueOr =
977 (lambda unrestricted fallback : (family ModelWord32) .
978 (lambda unrestricted result : (family DataBytesWord32ExactDecodeResult) .
979 (eliminate
980 DataBytesWord32ExactDecodeResult
981 (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) .
982 (family ModelWord32))
983 result
984 (branch DataBytesWord32ExactlyDecoded value telemetry . value)
985 (branch DataBytesWord32ExactDecodeFailed code telemetry . fallback))))
986
987def stdU32ExactFailed =
988 (lambda unrestricted result : (family DataBytesWord32ExactDecodeResult) .
989 (eliminate
990 DataBytesWord32ExactDecodeResult
991 (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) . Nat)
992 result
993 (branch DataBytesWord32ExactlyDecoded value telemetry . zero)
994 (branch DataBytesWord32ExactDecodeFailed code telemetry . (succ zero))))
995
996def stdU64ReadValueOr =
997 (lambda unrestricted fallback : (family ModelWord64) .
998 (lambda unrestricted result : (family DataBytesWord64DecodeResult) .
999 (eliminate
1000 DataBytesWord64DecodeResult
1001 (lambda unrestricted current : (family DataBytesWord64DecodeResult) . (family ModelWord64))
1002 result
1003 (branch DataBytesWord64Decoded value remaining . value)
1004 (branch DataBytesWord64DecodeFailed code . fallback))))
1005
1006def stdU64ReadRemaining =
1007 (lambda unrestricted result : (family DataBytesWord64DecodeResult) .
1008 (eliminate
1009 DataBytesWord64DecodeResult
1010 (lambda unrestricted current : (family DataBytesWord64DecodeResult) . Bytes)
1011 result
1012 (branch DataBytesWord64Decoded value remaining . remaining)
1013 (branch DataBytesWord64DecodeFailed code . b"")))
1014
1015def stdU64ReadFailed =
1016 (lambda unrestricted result : (family DataBytesWord64DecodeResult) .
1017 (eliminate
1018 DataBytesWord64DecodeResult
1019 (lambda unrestricted current : (family DataBytesWord64DecodeResult) . Nat)
1020 result
1021 (branch DataBytesWord64Decoded value remaining . zero)
1022 (branch DataBytesWord64DecodeFailed code . (succ zero))))
1023
1024def stdU64ExactValueOr =
1025 (lambda unrestricted fallback : (family ModelWord64) .
1026 (lambda unrestricted result : (family DataBytesWord64ExactDecodeResult) .
1027 (eliminate
1028 DataBytesWord64ExactDecodeResult
1029 (lambda unrestricted current : (family DataBytesWord64ExactDecodeResult) .
1030 (family ModelWord64))
1031 result
1032 (branch DataBytesWord64ExactlyDecoded value telemetry . value)
1033 (branch DataBytesWord64ExactDecodeFailed code telemetry . fallback))))
1034
1035def stdU64ExactFailed =
1036 (lambda unrestricted result : (family DataBytesWord64ExactDecodeResult) .
1037 (eliminate
1038 DataBytesWord64ExactDecodeResult
1039 (lambda unrestricted current : (family DataBytesWord64ExactDecodeResult) . Nat)
1040 result
1041 (branch DataBytesWord64ExactlyDecoded value telemetry . zero)
1042 (branch DataBytesWord64ExactDecodeFailed code telemetry . (succ zero))))
1043
1044-- U16 (no owner had a 16-bit codec): the same three shapes, built in the
1045-- owner's style. The bounded read answers Std.Codec's StdDecoded (value + rest,
1046-- or truncated); the exact decode answers StdOption (absent unless the input is
1047-- exactly two bytes).
1048def stdU16EncodeLE =
1049 (lambda unrestricted value : (family StdU16) .
1050 (eliminate
1051 StdU16
1052 (lambda unrestricted current : (family StdU16) . Bytes)
1053 value
1054 (branch StdU16Of low high . (bytes-cons low (bytes-cons high b"")))))
1055
1056def stdU16EncodeBE =
1057 (lambda unrestricted value : (family StdU16) .
1058 (eliminate
1059 StdU16
1060 (lambda unrestricted current : (family StdU16) . Bytes)
1061 value
1062 (branch StdU16Of low high . (bytes-cons high (bytes-cons low b"")))))
1063
1064def stdU16ReadLE =
1065 (lambda unrestricted input : Bytes .
1066 (nat-eliminate
1067 (lambda unrestricted current : Nat . (family StdDecoded (family StdU16)))
1068 (constructor StdDecoded StdDecodedTruncated (family StdU16))
1069 (lambda unrestricted predecessor : Nat .
1070 (lambda unrestricted induction : (family StdDecoded (family StdU16)) .
1071 (constructor
1072 StdDecoded
1073 StdDecodedValue
1074 (family StdU16)
1075 (stdU16FromBytes (bytes-head input) (bytes-head (bytes-tail input)))
1076 (bytes-tail (bytes-tail input)))))
1077 (naturalLessOrEqual (succ (succ zero)) (bytes-length input))))
1078
1079def stdU16ReadBE =
1080 (lambda unrestricted input : Bytes .
1081 (nat-eliminate
1082 (lambda unrestricted current : Nat . (family StdDecoded (family StdU16)))
1083 (constructor StdDecoded StdDecodedTruncated (family StdU16))
1084 (lambda unrestricted predecessor : Nat .
1085 (lambda unrestricted induction : (family StdDecoded (family StdU16)) .
1086 (constructor
1087 StdDecoded
1088 StdDecodedValue
1089 (family StdU16)
1090 (stdU16FromBytes (bytes-head (bytes-tail input)) (bytes-head input))
1091 (bytes-tail (bytes-tail input)))))
1092 (naturalLessOrEqual (succ (succ zero)) (bytes-length input))))
1093
1094def stdU16DecodeLEExact =
1095 (lambda unrestricted input : Bytes .
1096 (nat-eliminate
1097 (lambda unrestricted current : Nat . (family StdOption (family StdU16)))
1098 (constructor StdOption StdNone (family StdU16))
1099 (lambda unrestricted predecessor : Nat .
1100 (lambda unrestricted induction : (family StdOption (family StdU16)) .
1101 (constructor
1102 StdOption
1103 StdSome
1104 (family StdU16)
1105 (stdU16FromBytes (bytes-head input) (bytes-head (bytes-tail input))))))
1106 (naturalEqual (bytes-length input) (succ (succ zero)))))
1107
1108def stdU16DecodeBEExact =
1109 (lambda unrestricted input : Bytes .
1110 (nat-eliminate
1111 (lambda unrestricted current : Nat . (family StdOption (family StdU16)))
1112 (constructor StdOption StdNone (family StdU16))
1113 (lambda unrestricted predecessor : Nat .
1114 (lambda unrestricted induction : (family StdOption (family StdU16)) .
1115 (constructor
1116 StdOption
1117 StdSome
1118 (family StdU16)
1119 (stdU16FromBytes (bytes-head (bytes-tail input)) (bytes-head input)))))
1120 (naturalEqual (bytes-length input) (succ (succ zero)))))
1121
1122-- DIVISION (L11r, NUM-004): see the StdDivision family for the contract.
1123-- EVALUATOR NOTE (measured at L11r): the reference evaluator is a NORMALIZER
1124-- -- it normalizes every closed subterm, including the branch an eliminator
1125-- does not select (a slow closed term under an unselected successor lambda
1126-- still costs its full time). No shape below therefore makes a REFUSED word
1127-- division cheap on the evaluator lane: the loop is normalized anyway. The
1128-- refusal is kept in the zero case and the work under the successor lambda
1129-- because that is the natural shape (the flag reads "may divide"), not for
1130-- laziness; the evaluator-lane laws cover U8 (bounded naturals) and the
1131-- native lane carries every word-width value and refusal (NUM-006).
1132def stdDivisionErrorCodeBytes =
1133 (lambda unrestricted code : (family StdDivisionErrorCode) .
1134 (eliminate
1135 StdDivisionErrorCode
1136 (lambda unrestricted current : (family StdDivisionErrorCode) . Bytes)
1137 code
1138 (branch StdDivisionByZero . b"ALPHA-STD-WORD-001")
1139 (branch StdDivisionOverflow . b"ALPHA-STD-WORD-002")))
1140
1141-- Answer helpers over the result family (the word type is explicit).
1142def stdDivisionQuotientOr =
1143 (lambda erased word : Type 0 .
1144 (lambda unrestricted fallback : word .
1145 (lambda unrestricted result : (family StdDivision word) .
1146 (eliminate
1147 StdDivision
1148 (lambda unrestricted current : (family StdDivision word) . word)
1149 result
1150 (branch StdDivisionSucceeded quotient remainder . quotient)
1151 (branch StdDivisionFailed error . fallback)))))
1152
1153def stdDivisionRemainderOr =
1154 (lambda erased word : Type 0 .
1155 (lambda unrestricted fallback : word .
1156 (lambda unrestricted result : (family StdDivision word) .
1157 (eliminate
1158 StdDivision
1159 (lambda unrestricted current : (family StdDivision word) . word)
1160 result
1161 (branch StdDivisionSucceeded quotient remainder . remainder)
1162 (branch StdDivisionFailed error . fallback)))))
1163
1164def stdDivisionIsFailed =
1165 (lambda erased word : Type 0 .
1166 (lambda unrestricted result : (family StdDivision word) .
1167 (eliminate
1168 StdDivision
1169 (lambda unrestricted current : (family StdDivision word) . Nat)
1170 result
1171 (branch StdDivisionSucceeded quotient remainder . zero)
1172 (branch StdDivisionFailed error . (succ zero)))))
1173
1174-- The failure's code bytes, or empty bytes when the division succeeded.
1175def stdDivisionFailureBytes =
1176 (lambda erased word : Type 0 .
1177 (lambda unrestricted result : (family StdDivision word) .
1178 (eliminate
1179 StdDivision
1180 (lambda unrestricted current : (family StdDivision word) . Bytes)
1181 result
1182 (branch StdDivisionSucceeded quotient remainder . b"")
1183 (branch StdDivisionFailed error . (stdDivisionErrorCodeBytes error)))))
1184
1185-- Flag helpers on the 0/1 naturals the word owners use as booleans.
1186def stdFlagNot =
1187 modelWord64FlagNot
1188
1189def stdFlagXor =
1190 (lambda unrestricted a : Nat .
1191 (lambda unrestricted b : Nat .
1192 (nat-eliminate
1193 (lambda unrestricted current : Nat . Nat)
1194 b
1195 (lambda unrestricted predecessor : Nat .
1196 (lambda unrestricted induction : Nat . (modelWord64FlagNot b)))
1197 a)))
1198
1199-- U64 restoring division: 64 iterations, each shifting the next dividend bit
1200-- into the partial remainder and subtracting the divisor when it fits. The
1201-- remainder is always < divisor, so 2r+1 can exceed 64 bits only when the
1202-- remainder's high bit was set; that bit is the carry out of the shift and
1203-- means the divisor fits (2r >= 2^64 > divisor), and the wrapped subtraction
1204-- still yields the exact new remainder (the true value is < 2^64).
1205def stdU64DivisionStep =
1206 (lambda unrestricted divisor : (family ModelWord64) .
1207 (lambda unrestricted state : (family StdU64DivisionState) .
1208 (eliminate
1209 StdU64DivisionState
1210 (lambda unrestricted current : (family StdU64DivisionState) . (family StdU64DivisionState))
1211 state
1212 (branch
1213 StdU64DivisionStateOf
1214 remainder
1215 quotient
1216 dividend
1217 .
1218 (app
1219 (lambda unrestricted shifted : (family ModelWord64) .
1220 (app
1221 (lambda unrestricted shiftedQuotient : (family ModelWord64) .
1222 (app
1223 (lambda unrestricted shiftedDividend : (family ModelWord64) .
1224 (nat-eliminate
1225 (lambda unrestricted current : Nat . (family StdU64DivisionState))
1226 (constructor
1227 StdU64DivisionState
1228 StdU64DivisionStateOf
1229 shifted
1230 shiftedQuotient
1231 shiftedDividend)
1232 (lambda unrestricted predecessor : Nat .
1233 (lambda unrestricted induction : (family StdU64DivisionState) .
1234 (constructor
1235 StdU64DivisionState
1236 StdU64DivisionStateOf
1237 (modelWord64Subtract shifted divisor)
1238 (modelWord64Add shiftedQuotient modelWord64One)
1239 shiftedDividend)))
1240 (modelWord64FlagOr
1241 (modelWord64HighBit remainder)
1242 (modelWord64FlagNot (modelWord64LessThan shifted divisor)))))
1243 (modelWord64ShiftLeftOne dividend)))
1244 (modelWord64ShiftLeftOne quotient)))
1245 (modelWord64Add
1246 (modelWord64ShiftLeftOne remainder)
1247 (modelWord64Select (modelWord64HighBit dividend) modelWord64One modelWord64Zero)))))))
1248
1249def stdU64DivisionRun =
1250 (lambda unrestricted dividend : (family ModelWord64) .
1251 (lambda unrestricted divisor : (family ModelWord64) .
1252 (nat-eliminate
1253 (lambda unrestricted current : Nat . (family StdU64DivisionState))
1254 (constructor
1255 StdU64DivisionState
1256 StdU64DivisionStateOf
1257 modelWord64Zero
1258 modelWord64Zero
1259 dividend)
1260 (lambda unrestricted predecessor : Nat .
1261 (lambda unrestricted induction : (family StdU64DivisionState) .
1262 (stdU64DivisionStep divisor induction)))
1263 modelWord64NaturalSixtyFour)))
1264
1265-- U64 division: divisor zero -> StdDivisionByZero, else quotient + remainder.
1266def stdU64DivRem =
1267 (lambda unrestricted dividend : (family ModelWord64) .
1268 (lambda unrestricted divisor : (family ModelWord64) .
1269 (nat-eliminate
1270 (lambda unrestricted current : Nat . (family StdDivision (family ModelWord64)))
1271 (constructor
1272 StdDivision
1273 StdDivisionFailed
1274 (family ModelWord64)
1275 (constructor StdDivisionErrorCode StdDivisionByZero))
1276 (lambda unrestricted predecessor : Nat .
1277 (lambda unrestricted induction : (family StdDivision (family ModelWord64)) .
1278 (eliminate
1279 StdU64DivisionState
1280 (lambda unrestricted current : (family StdU64DivisionState) .
1281 (family StdDivision (family ModelWord64)))
1282 (stdU64DivisionRun dividend divisor)
1283 (branch
1284 StdU64DivisionStateOf
1285 remainder
1286 quotient
1287 rest
1288 .
1289 (constructor
1290 StdDivision
1291 StdDivisionSucceeded
1292 (family ModelWord64)
1293 quotient
1294 remainder)))))
1295 (modelWord64FlagNot (modelWord64IsZero divisor)))))
1296
1297-- U32: Model.Word32 is frozen and has no subtract/complement, so the wrapping
1298-- subtract is built here (a - b = a + not b + 1), then the same restoring
1299-- division over the four-byte word.
1300def stdU32AllOnes =
1301 (constructor ModelWord32 ModelWord32Value (byte 255) (byte 255) (byte 255) (byte 255))
1302
1303def stdU32Not =
1304 (lambda unrestricted value : (family ModelWord32) . (modelWord32Xor value stdU32AllOnes))
1305
1306def stdU32SubtractWrapping =
1307 (lambda unrestricted a : (family ModelWord32) .
1308 (lambda unrestricted b : (family ModelWord32) .
1309 (modelWord32Add a (modelWord32Add (stdU32Not b) modelWord32One))))
1310
1311-- Delegates to the one owner (Model.Word32, already imported here); found
1312-- as an exact duplicate by `alpha-ast duplicates` (L24d).
1313def stdU32Select =
1314 modelWord32Select
1315
1316def stdU32NaturalThirtyTwo =
1317 (byte-to-nat (byte 32))
1318
1319def stdU32DivisionStep =
1320 (lambda unrestricted divisor : (family ModelWord32) .
1321 (lambda unrestricted state : (family StdU32DivisionState) .
1322 (eliminate
1323 StdU32DivisionState
1324 (lambda unrestricted current : (family StdU32DivisionState) . (family StdU32DivisionState))
1325 state
1326 (branch
1327 StdU32DivisionStateOf
1328 remainder
1329 quotient
1330 dividend
1331 .
1332 (app
1333 (lambda unrestricted shifted : (family ModelWord32) .
1334 (app
1335 (lambda unrestricted shiftedQuotient : (family ModelWord32) .
1336 (app
1337 (lambda unrestricted shiftedDividend : (family ModelWord32) .
1338 (nat-eliminate
1339 (lambda unrestricted current : Nat . (family StdU32DivisionState))
1340 (constructor
1341 StdU32DivisionState
1342 StdU32DivisionStateOf
1343 shifted
1344 shiftedQuotient
1345 shiftedDividend)
1346 (lambda unrestricted predecessor : Nat .
1347 (lambda unrestricted induction : (family StdU32DivisionState) .
1348 (constructor
1349 StdU32DivisionState
1350 StdU32DivisionStateOf
1351 (stdU32SubtractWrapping shifted divisor)
1352 (modelWord32Add shiftedQuotient modelWord32One)
1353 shiftedDividend)))
1354 (stdFlagOr
1355 (stdU32HighBit remainder)
1356 (stdFlagNot (stdU32LessThan shifted divisor)))))
1357 (modelWord32ShiftLeftOne dividend)))
1358 (modelWord32ShiftLeftOne quotient)))
1359 (modelWord32Add
1360 (modelWord32ShiftLeftOne remainder)
1361 (stdU32Select (stdU32HighBit dividend) modelWord32One modelWord32Zero)))))))
1362
1363def stdU32DivisionRun =
1364 (lambda unrestricted dividend : (family ModelWord32) .
1365 (lambda unrestricted divisor : (family ModelWord32) .
1366 (nat-eliminate
1367 (lambda unrestricted current : Nat . (family StdU32DivisionState))
1368 (constructor
1369 StdU32DivisionState
1370 StdU32DivisionStateOf
1371 modelWord32Zero
1372 modelWord32Zero
1373 dividend)
1374 (lambda unrestricted predecessor : Nat .
1375 (lambda unrestricted induction : (family StdU32DivisionState) .
1376 (stdU32DivisionStep divisor induction)))
1377 stdU32NaturalThirtyTwo)))
1378
1379def stdU32DivRem =
1380 (lambda unrestricted dividend : (family ModelWord32) .
1381 (lambda unrestricted divisor : (family ModelWord32) .
1382 (nat-eliminate
1383 (lambda unrestricted current : Nat . (family StdDivision (family ModelWord32)))
1384 (constructor
1385 StdDivision
1386 StdDivisionFailed
1387 (family ModelWord32)
1388 (constructor StdDivisionErrorCode StdDivisionByZero))
1389 (lambda unrestricted predecessor : Nat .
1390 (lambda unrestricted induction : (family StdDivision (family ModelWord32)) .
1391 (eliminate
1392 StdU32DivisionState
1393 (lambda unrestricted current : (family StdU32DivisionState) .
1394 (family StdDivision (family ModelWord32)))
1395 (stdU32DivisionRun dividend divisor)
1396 (branch
1397 StdU32DivisionStateOf
1398 remainder
1399 quotient
1400 rest
1401 .
1402 (constructor
1403 StdDivision
1404 StdDivisionSucceeded
1405 (family ModelWord32)
1406 quotient
1407 remainder)))))
1408 (stdFlagNot (stdU32IsZero divisor)))))
1409
1410-- U16 divides as U32 (zero-extend, divide, keep the low bytes: both results
1411-- are bounded by the operands, so the narrow never drops a set bit).
1412def stdU16ToU32 =
1413 (lambda unrestricted value : (family StdU16) .
1414 (eliminate
1415 StdU16
1416 (lambda unrestricted current : (family StdU16) . (family ModelWord32))
1417 value
1418 (branch
1419 StdU16Of
1420 low
1421 high
1422 .
1423 (constructor ModelWord32 ModelWord32Value low high (byte 0) (byte 0)))))
1424
1425def stdU32ToU16 =
1426 (lambda unrestricted value : (family ModelWord32) .
1427 (eliminate
1428 ModelWord32
1429 (lambda unrestricted current : (family ModelWord32) . (family StdU16))
1430 value
1431 (branch ModelWord32Value b0 b1 b2 b3 . (stdU16FromBytes b0 b1))))
1432
1433def stdU16DivRem =
1434 (lambda unrestricted dividend : (family StdU16) .
1435 (lambda unrestricted divisor : (family StdU16) .
1436 (eliminate
1437 StdDivision
1438 (lambda unrestricted current : (family StdDivision (family ModelWord32)) .
1439 (family StdDivision (family StdU16)))
1440 (stdU32DivRem (stdU16ToU32 dividend) (stdU16ToU32 divisor))
1441 (branch
1442 StdDivisionSucceeded
1443 quotient
1444 remainder
1445 .
1446 (constructor
1447 StdDivision
1448 StdDivisionSucceeded
1449 (family StdU16)
1450 (stdU32ToU16 quotient)
1451 (stdU32ToU16 remainder)))
1452 (branch
1453 StdDivisionFailed
1454 error
1455 .
1456 (constructor StdDivision StdDivisionFailed (family StdU16) error)))))
1457
1458-- U8 divides through the core naturals (values are at most 255, so this is
1459-- exact on every lane); Std.Natural owns the natural division and its
1460-- NaturalDivisionState already carries BOTH the quotient and the remainder, so
1461-- one traversal answers both. RECORDED (L11r): the owner's separate
1462-- naturalModuloUnchecked is pathological on the reference evaluator (255 mod 16
1463-- gives no answer in 100 s while naturalDivideUnchecked 255 16 answers in
1464-- 0.3 s), which is why the remainder is projected from the state, never
1465-- recomputed through the modulo.
1466def stdU8DivRem =
1467 (lambda unrestricted dividend : Byte .
1468 (lambda unrestricted divisor : Byte .
1469 (nat-eliminate
1470 (lambda unrestricted current : Nat . (family StdDivision Byte))
1471 (constructor
1472 StdDivision
1473 StdDivisionFailed
1474 Byte
1475 (constructor StdDivisionErrorCode StdDivisionByZero))
1476 (lambda unrestricted predecessor : Nat .
1477 (lambda unrestricted induction : (family StdDivision Byte) .
1478 (eliminate
1479 NaturalDivisionState
1480 (lambda unrestricted current : (family NaturalDivisionState) .
1481 (family StdDivision Byte))
1482 (naturalDivisionState (byte-to-nat dividend) (byte-to-nat divisor))
1483 (branch
1484 NaturalDivisionStateValue
1485 remainder
1486 quotient
1487 .
1488 (constructor
1489 StdDivision
1490 StdDivisionSucceeded
1491 Byte
1492 (nat-to-byte quotient)
1493 (nat-to-byte remainder))))))
1494 (byte-to-nat divisor))))
1495
1496-- SIGNED division through magnitudes: |a| / |b| unsigned, then the quotient
1497-- is negated when the signs differ and the remainder when the dividend is
1498-- negative. |signedMinimum| = 2^(width-1) is representable unsigned, so the
1499-- wrapping API needs no special case: 2^(width-1) / 1 negated wraps back to
1500-- signedMinimum with remainder 0. The checked API refuses exactly that shape.
1501def stdU64NegateIf =
1502 (lambda unrestricted flag : Nat .
1503 (lambda unrestricted bits : (family ModelWord64) .
1504 (modelWord64Select flag (modelWord64Subtract modelWord64Zero bits) bits)))
1505
1506def stdI64IsNegative =
1507 (lambda unrestricted value : (family StdI64) . (modelWord64HighBit (stdI64ToWord value)))
1508
1509def stdI64Negate =
1510 (lambda unrestricted value : (family StdI64) .
1511 (stdI64FromWord (modelWord64Subtract modelWord64Zero (stdI64ToWord value))))
1512
1513def stdI64Magnitude =
1514 (lambda unrestricted value : (family StdI64) .
1515 (stdU64NegateIf (stdI64IsNegative value) (stdI64ToWord value)))
1516
1517def stdI64MinimumBits =
1518 (constructor
1519 ModelWord64
1520 ModelWord64Value
1521 (byte 0)
1522 (byte 0)
1523 (byte 0)
1524 (byte 0)
1525 (byte 0)
1526 (byte 0)
1527 (byte 0)
1528 (byte 128))
1529
1530def stdU64AllOnes =
1531 (constructor
1532 ModelWord64
1533 ModelWord64Value
1534 (byte 255)
1535 (byte 255)
1536 (byte 255)
1537 (byte 255)
1538 (byte 255)
1539 (byte 255)
1540 (byte 255)
1541 (byte 255))
1542
1543def stdI64DivRemWrapping =
1544 (lambda unrestricted dividend : (family StdI64) .
1545 (lambda unrestricted divisor : (family StdI64) .
1546 (eliminate
1547 StdDivision
1548 (lambda unrestricted current : (family StdDivision (family ModelWord64)) .
1549 (family StdDivision (family StdI64)))
1550 (stdU64DivRem (stdI64Magnitude dividend) (stdI64Magnitude divisor))
1551 (branch
1552 StdDivisionSucceeded
1553 quotient
1554 remainder
1555 .
1556 (constructor
1557 StdDivision
1558 StdDivisionSucceeded
1559 (family StdI64)
1560 (stdI64FromWord
1561 (stdU64NegateIf
1562 (stdFlagXor (stdI64IsNegative dividend) (stdI64IsNegative divisor))
1563 quotient))
1564 (stdI64FromWord (stdU64NegateIf (stdI64IsNegative dividend) remainder))))
1565 (branch
1566 StdDivisionFailed
1567 error
1568 .
1569 (constructor StdDivision StdDivisionFailed (family StdI64) error)))))
1570
1571def stdI64DivRemChecked =
1572 (lambda unrestricted dividend : (family StdI64) .
1573 (lambda unrestricted divisor : (family StdI64) .
1574 (nat-eliminate
1575 (lambda unrestricted current : Nat . (family StdDivision (family StdI64)))
1576 (constructor
1577 StdDivision
1578 StdDivisionFailed
1579 (family StdI64)
1580 (constructor StdDivisionErrorCode StdDivisionOverflow))
1581 (lambda unrestricted predecessor : Nat .
1582 (lambda unrestricted induction : (family StdDivision (family StdI64)) .
1583 (stdI64DivRemWrapping dividend divisor)))
1584 (stdFlagNot
1585 (stdFlagAnd
1586 (modelWord64Equal (stdI64ToWord dividend) stdI64MinimumBits)
1587 (modelWord64Equal (stdI64ToWord divisor) stdU64AllOnes))))))
1588
1589-- I32 over the U32 division.
1590def stdU32NegateIf =
1591 (lambda unrestricted flag : Nat .
1592 (lambda unrestricted bits : (family ModelWord32) .
1593 (stdU32Select flag (stdU32SubtractWrapping modelWord32Zero bits) bits)))
1594
1595def stdI32IsNegative =
1596 (lambda unrestricted value : (family StdI32) . (stdU32HighBit (stdI32ToWord value)))
1597
1598def stdI32Negate =
1599 (lambda unrestricted value : (family StdI32) .
1600 (stdI32FromWord (stdU32SubtractWrapping modelWord32Zero (stdI32ToWord value))))
1601
1602def stdI32Magnitude =
1603 (lambda unrestricted value : (family StdI32) .
1604 (stdU32NegateIf (stdI32IsNegative value) (stdI32ToWord value)))
1605
1606def stdI32MinimumBits =
1607 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 128))
1608
1609def stdI32DivRemWrapping =
1610 (lambda unrestricted dividend : (family StdI32) .
1611 (lambda unrestricted divisor : (family StdI32) .
1612 (eliminate
1613 StdDivision
1614 (lambda unrestricted current : (family StdDivision (family ModelWord32)) .
1615 (family StdDivision (family StdI32)))
1616 (stdU32DivRem (stdI32Magnitude dividend) (stdI32Magnitude divisor))
1617 (branch
1618 StdDivisionSucceeded
1619 quotient
1620 remainder
1621 .
1622 (constructor
1623 StdDivision
1624 StdDivisionSucceeded
1625 (family StdI32)
1626 (stdI32FromWord
1627 (stdU32NegateIf
1628 (stdFlagXor (stdI32IsNegative dividend) (stdI32IsNegative divisor))
1629 quotient))
1630 (stdI32FromWord (stdU32NegateIf (stdI32IsNegative dividend) remainder))))
1631 (branch
1632 StdDivisionFailed
1633 error
1634 .
1635 (constructor StdDivision StdDivisionFailed (family StdI32) error)))))
1636
1637def stdI32DivRemChecked =
1638 (lambda unrestricted dividend : (family StdI32) .
1639 (lambda unrestricted divisor : (family StdI32) .
1640 (nat-eliminate
1641 (lambda unrestricted current : Nat . (family StdDivision (family StdI32)))
1642 (constructor
1643 StdDivision
1644 StdDivisionFailed
1645 (family StdI32)
1646 (constructor StdDivisionErrorCode StdDivisionOverflow))
1647 (lambda unrestricted predecessor : Nat .
1648 (lambda unrestricted induction : (family StdDivision (family StdI32)) .
1649 (stdI32DivRemWrapping dividend divisor)))
1650 (stdFlagNot
1651 (stdFlagAnd
1652 (stdU32Equal (stdI32ToWord dividend) stdI32MinimumBits)
1653 (stdU32Equal (stdI32ToWord divisor) stdU32AllOnes))))))
1654
1655-- I16 and I8 divide as I32 (sign-extend, divide WRAPPING at 32 bits where
1656-- every 16/8-bit quotient fits, narrow back): the only narrow that drops a
1657-- bit is signedMinimum / -1, which the wrapping narrow turns back into
1658-- signedMinimum (the wrap) and the checked API refuses first.
1659def stdI32ToI16 =
1660 (lambda unrestricted value : (family StdI32) .
1661 (eliminate
1662 ModelWord32
1663 (lambda unrestricted current : (family ModelWord32) . (family StdI16))
1664 (stdI32ToWord value)
1665 (branch ModelWord32Value b0 b1 b2 b3 . (stdI16FromU16 (stdU16FromBytes b0 b1)))))
1666
1667def stdI16DivRemWrapping =
1668 (lambda unrestricted dividend : (family StdI16) .
1669 (lambda unrestricted divisor : (family StdI16) .
1670 (eliminate
1671 StdDivision
1672 (lambda unrestricted current : (family StdDivision (family StdI32)) .
1673 (family StdDivision (family StdI16)))
1674 (stdI32DivRemWrapping (stdI16ToI32 dividend) (stdI16ToI32 divisor))
1675 (branch
1676 StdDivisionSucceeded
1677 quotient
1678 remainder
1679 .
1680 (constructor
1681 StdDivision
1682 StdDivisionSucceeded
1683 (family StdI16)
1684 (stdI32ToI16 quotient)
1685 (stdI32ToI16 remainder)))
1686 (branch
1687 StdDivisionFailed
1688 error
1689 .
1690 (constructor StdDivision StdDivisionFailed (family StdI16) error)))))
1691
1692def stdI16MinimumBits =
1693 (stdU16FromBytes (byte 0) (byte 128))
1694
1695def stdU16AllOnes =
1696 (stdU16FromBytes (byte 255) (byte 255))
1697
1698def stdI16DivRemChecked =
1699 (lambda unrestricted dividend : (family StdI16) .
1700 (lambda unrestricted divisor : (family StdI16) .
1701 (nat-eliminate
1702 (lambda unrestricted current : Nat . (family StdDivision (family StdI16)))
1703 (constructor
1704 StdDivision
1705 StdDivisionFailed
1706 (family StdI16)
1707 (constructor StdDivisionErrorCode StdDivisionOverflow))
1708 (lambda unrestricted predecessor : Nat .
1709 (lambda unrestricted induction : (family StdDivision (family StdI16)) .
1710 (stdI16DivRemWrapping dividend divisor)))
1711 (stdFlagNot
1712 (stdFlagAnd
1713 (stdU16Equal (stdI16ToU16 dividend) stdI16MinimumBits)
1714 (stdU16Equal (stdI16ToU16 divisor) stdU16AllOnes))))))
1715
1716def stdI8DivRemWrapping =
1717 (lambda unrestricted dividend : (family StdI8) .
1718 (lambda unrestricted divisor : (family StdI8) .
1719 (eliminate
1720 StdDivision
1721 (lambda unrestricted current : (family StdDivision (family StdI32)) .
1722 (family StdDivision (family StdI8)))
1723 (stdI32DivRemWrapping (stdI8ToI32 dividend) (stdI8ToI32 divisor))
1724 (branch
1725 StdDivisionSucceeded
1726 quotient
1727 remainder
1728 .
1729 (constructor
1730 StdDivision
1731 StdDivisionSucceeded
1732 (family StdI8)
1733 (stdI32ToI8 quotient)
1734 (stdI32ToI8 remainder)))
1735 (branch
1736 StdDivisionFailed
1737 error
1738 .
1739 (constructor StdDivision StdDivisionFailed (family StdI8) error)))))
1740
1741def stdI8DivRemChecked =
1742 (lambda unrestricted dividend : (family StdI8) .
1743 (lambda unrestricted divisor : (family StdI8) .
1744 (nat-eliminate
1745 (lambda unrestricted current : Nat . (family StdDivision (family StdI8)))
1746 (constructor
1747 StdDivision
1748 StdDivisionFailed
1749 (family StdI8)
1750 (constructor StdDivisionErrorCode StdDivisionOverflow))
1751 (lambda unrestricted predecessor : Nat .
1752 (lambda unrestricted induction : (family StdDivision (family StdI8)) .
1753 (stdI8DivRemWrapping dividend divisor)))
1754 (stdFlagNot
1755 (stdFlagAnd
1756 (byte-equal (stdI8ToByte dividend) (byte 128))
1757 (byte-equal (stdI8ToByte divisor) (byte 255)))))))
1758
1759-- CHECKED SHIFTS (U32): a count >= the width is an error; the wrapping
1760-- `stdU32ShiftLeft/Right` (Model.Word32) repeat the one-bit shift `count`
1761-- times, so a count >= 32 yields ZERO there (stated: NOT the x86-64 `shl`
1762-- count-masking; a program wanting masking reduces the count itself).
1763def stdU32ShiftLeftChecked =
1764 (lambda unrestricted value : (family ModelWord32) .
1765 (lambda unrestricted count : Nat .
1766 (nat-eliminate
1767 (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
1768 (constructor StdOption StdNone (family ModelWord32))
1769 (lambda unrestricted predecessor : Nat .
1770 (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
1771 (constructor StdOption StdSome (family ModelWord32) (modelWord32ShiftLeft value count))))
1772 (nat-less-than count stdU32NaturalThirtyTwo))))
1773
1774def stdU32ShiftRightChecked =
1775 (lambda unrestricted value : (family ModelWord32) .
1776 (lambda unrestricted count : Nat .
1777 (nat-eliminate
1778 (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
1779 (constructor StdOption StdNone (family ModelWord32))
1780 (lambda unrestricted predecessor : Nat .
1781 (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
1782 (constructor StdOption StdSome (family ModelWord32) (modelWord32ShiftRight value count))))
1783 (nat-less-than count stdU32NaturalThirtyTwo))))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.