Runtime.NativeFiniteWords

1module Runtime.NativeFiniteWords
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Std.Foundation
6import Std.Natural
7
8family NativeFiniteWordFormat : Type 0
9constructor NativeFiniteF32
10constructor NativeFiniteBF16
11end-family
12
13def nativeFiniteFormatTag =
14  (lambda unrestricted format : (family NativeFiniteWordFormat) .
15    (eliminate NativeFiniteWordFormat
16      (lambda unrestricted current : (family NativeFiniteWordFormat) . Nat)
17      format
18      (branch NativeFiniteF32 . 0)
19      (branch NativeFiniteBF16 . 1)))
20
21-- The checkpoint validator examines representations, not floating-point
22-- arithmetic: exponent 255 means infinity or NaN in either IEEE binary32 or
23-- bfloat16. This is the same predicate used by the native host routine below.
24def finiteF32Bits =
25  (lambda unrestricted bits : Nat .
26    (naturalSelect
27      (naturalEqual
28        (naturalModuloUnchecked (naturalDivideUnchecked bits 8388608) 256)
29        255)
30      0 1))
31def finiteBF16Bits =
32  (lambda unrestricted bits : Nat .
33    (naturalSelect
34      (naturalEqual
35        (naturalModuloUnchecked (naturalDivideUnchecked bits 128) 256)
36        255)
37      0 1))
38def finiteBF16Pair =
39  (lambda unrestricted packed : Nat .
40    (naturalMultiply
41      (finiteBF16Bits (naturalModuloUnchecked packed 65536))
42      (finiteBF16Bits (naturalDivideUnchecked packed 65536))))
43
44def finiteRAX = (constructor X86NativeRegister64 X86NativeRAX)
45def finiteRCX = (constructor X86NativeRegister64 X86NativeRCX)
46def finiteRDI = (constructor X86NativeRegister64 X86NativeRDI)
47def finiteRSI = (constructor X86NativeRegister64 X86NativeRSI)
48def finiteR8 = (constructor X86NativeRegister64 X86NativeR8)
49def finiteEmit =
50  (lambda unrestricted instruction : (family X86NativeInstruction) .
51    (lambda unrestricted tail : (family X86NativeAssembly) .
52      (constructor X86NativeAssembly X86NativeAssemblyEmit instruction tail)))
53def finiteLabel =
54  (lambda unrestricted name : Bytes .
55    (lambda unrestricted tail : (family X86NativeAssembly) .
56      (constructor X86NativeAssembly X86NativeAssemblyLabel name tail)))
57def finiteJump =
58  (lambda unrestricted name : Bytes .
59    (lambda unrestricted tail : (family X86NativeAssembly) .
60      (constructor X86NativeAssembly X86NativeAssemblyJump name tail)))
61def finiteBranch =
62  (lambda unrestricted condition : (family X86NativeCondition) .
63    (lambda unrestricted name : Bytes .
64      (lambda unrestricted tail : (family X86NativeAssembly) .
65        (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name tail))))
66def finiteMove =
67  (lambda unrestricted destination : (family X86NativeRegister64) .
68    (lambda unrestricted source : (family X86NativeRegister64) .
69      (finiteEmit (constructor X86NativeInstruction X86NativeMoveRegister64 source destination))))
70def finiteAnd =
71  (lambda unrestricted register : (family X86NativeRegister64) .
72    (lambda unrestricted mask : Nat .
73      (finiteEmit (constructor X86NativeInstruction X86NativeAndImmediate64
74        register (x86NativeImmediate32FromNatural mask)))))
75def finiteCompare =
76  (lambda unrestricted register : (family X86NativeRegister64) .
77    (lambda unrestricted value : Nat .
78      (finiteEmit (constructor X86NativeInstruction X86NativeCompareImmediate64
79        register (x86NativeImmediate32FromNatural value)))))
80def finiteWordCheck =
81  (lambda unrestricted half : Nat .
82    (lambda unrestricted tail : (family X86NativeAssembly) .
83      (nat-eliminate (lambda unrestricted mode : Nat . (family X86NativeAssembly))
84        (finiteAnd finiteRAX 2139095040
85          (finiteCompare finiteRAX 2139095040
86            (finiteBranch (constructor X86NativeCondition X86NativeConditionZero)
87              b"reject" tail)))
88        (lambda unrestricted predecessor : Nat .
89          (lambda unrestricted unused : (family X86NativeAssembly) .
90            (finiteMove finiteRCX finiteRAX
91              (finiteAnd finiteRAX 32640
92                (finiteCompare finiteRAX 32640
93                  (finiteBranch (constructor X86NativeCondition X86NativeConditionZero)
94                    b"reject"
95                    (finiteEmit (constructor X86NativeInstruction
96                      X86NativeShiftRightImmediate64 finiteRCX
97                      (constructor X86NativeImmediate8 X86NativeImmediate8Value (byte 16)))
98                      (finiteAnd finiteRCX 32640
99                        (finiteCompare finiteRCX 32640
100                          (finiteBranch (constructor X86NativeCondition X86NativeConditionZero)
101                            b"reject" tail))))))))))
102        half)))
103
104-- System V: RDI points to `extent` mapped bytes; RSI is that extent. The
105-- caller chooses the format by embedding one of these two routine images.
106-- Every four-byte word is checked, including both halves of a BF16 pair.
107-- Zero or unaligned extents and a wrapping end address fail closed. The
108-- caller must prove the mapped span belongs to its typed staging region.
109def nativeFiniteWordsAssembly =
110  (lambda unrestricted half : Nat .
111    (finiteEmit (constructor X86NativeInstruction X86NativeTestRegister64 finiteRSI finiteRSI)
112    (finiteBranch (constructor X86NativeCondition X86NativeConditionZero) b"reject"
113    (finiteMove finiteRAX finiteRSI
114    (finiteAnd finiteRAX 3
115    (finiteBranch (constructor X86NativeCondition X86NativeConditionNotZero) b"reject"
116    (finiteMove finiteR8 finiteRDI
117    (finiteEmit (constructor X86NativeInstruction X86NativeAddRegister64 finiteRSI finiteR8)
118    (finiteEmit (constructor X86NativeInstruction X86NativeCompareRegister64 finiteRDI finiteR8)
119    (finiteBranch (constructor X86NativeCondition X86NativeConditionBelow) b"reject"
120    (finiteLabel b"scan"
121    (finiteEmit (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64
122      finiteRAX finiteRDI (x86NativeDisplacement32FromNatural 0))
123    (finiteWordCheck half
124    (finiteEmit (constructor X86NativeInstruction X86NativeAddImmediate64 finiteRDI
125      (x86NativeImmediate32FromNatural 4))
126    (finiteEmit (constructor X86NativeInstruction X86NativeCompareRegister64 finiteR8 finiteRDI)
127    (finiteBranch (constructor X86NativeCondition X86NativeConditionZero) b"accept"
128    (finiteJump b"scan"
129    (finiteLabel b"accept"
130    (finiteEmit (constructor X86NativeInstruction X86NativeClear32 finiteRAX)
131    (finiteEmit (constructor X86NativeInstruction X86NativeReturn)
132    (finiteLabel b"reject"
133    (finiteEmit (constructor X86NativeInstruction X86NativeMoveImmediate32 finiteRAX
134      (x86NativeImmediate32FromNatural 1))
135    (finiteEmit (constructor X86NativeInstruction X86NativeReturn)
136      (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))))))))))))))))
137def nativeFiniteWordsCode =
138  (lambda unrestricted half : Nat .
139    (eliminate X86NativeAssemblyResult
140      (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
141      (x86NativeAssemble (nativeFiniteWordsAssembly half))
142      (branch X86NativeAssemblyEncoded code . code)
143      (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
144      (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
145      (branch X86NativeAssemblyMissingLabel name . b"")
146      (branch X86NativeAssemblyDisplacementOutOfRange name . b"")))
147def nativeFiniteF32Routine : Bytes = (nativeFiniteWordsCode 0)
148def nativeFiniteBF16Routine : Bytes = (nativeFiniteWordsCode 1)
149def nativeFiniteRoutineFor =
150  (lambda unrestricted format : (family NativeFiniteWordFormat) .
151    (eliminate NativeFiniteWordFormat
152      (lambda unrestricted current : (family NativeFiniteWordFormat) . Bytes)
153      format
154      (branch NativeFiniteF32 . nativeFiniteF32Routine)
155      (branch NativeFiniteBF16 . nativeFiniteBF16Routine)))