Runtime.NativeMemoryRoutine

1module Runtime.NativeMemoryRoutine
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Data.SHA256Digest
6import Runtime.NativePhysicalNative
7import Runtime.MemoryCopyRoutine
8
9family NativeMemoryRoutineErrorCode : Type 0
10constructor NativeMemoryRoutineDuplicateLabel
11field unrestricted nativeMemoryRoutineDuplicateLabelName : Bytes
12constructor NativeMemoryRoutineOffsetOverflow
13constructor NativeMemoryRoutineMissingLabel
14field unrestricted nativeMemoryRoutineMissingLabelName : Bytes
15constructor NativeMemoryRoutineDisplacementOutOfRange
16field unrestricted nativeMemoryRoutineDistantLabelName : Bytes
17
18end-family
19
20family NativeMemoryRoutineTelemetry : Type 0
21constructor NativeMemoryRoutineTelemetryValue
22field unrestricted nativeMemoryRoutineTelemetryInstructions : Nat
23field unrestricted nativeMemoryRoutineTelemetryCodeBytes : Nat
24field unrestricted nativeMemoryRoutineTelemetryFailures : Nat
25field unrestricted nativeMemoryRoutineTelemetryFallbacks : Nat
26field unrestricted nativeMemoryRoutineTelemetryCodeSHA256 : Bytes
27field unrestricted nativeMemoryRoutineTelemetryLastError : Bytes
28
29end-family
30
31family NativeMemoryRoutine : Type 0
32constructor NativeMemoryRoutineValue
33field unrestricted nativeMemoryRoutineCode : Bytes
34field unrestricted nativeMemoryRoutineCodeSHA256 : Bytes
35field unrestricted nativeMemoryRoutineInstructionCount : Nat
36field unrestricted nativeMemoryRoutineTelemetry : (family NativeMemoryRoutineTelemetry)
37
38end-family
39
40family NativeMemoryRoutineResult : Type 0
41constructor NativeMemoryRoutineGenerated
42field unrestricted nativeMemoryGeneratedRoutine : (family NativeMemoryRoutine)
43field unrestricted nativeMemoryRoutineSuccessTelemetry : (family NativeMemoryRoutineTelemetry)
44constructor NativeMemoryRoutineGenerationFailed
45field unrestricted nativeMemoryRoutineGenerationError : (family NativeMemoryRoutineErrorCode)
46field unrestricted nativeMemoryRoutineFailureTelemetry : (family NativeMemoryRoutineTelemetry)
47
48end-family
49
50def nativeMemoryRoutineErrorCodeBytes =
51  (lambda unrestricted code : (family NativeMemoryRoutineErrorCode) .
52    (eliminate
53      NativeMemoryRoutineErrorCode
54      (lambda unrestricted current : (family NativeMemoryRoutineErrorCode) . Bytes)
55      code
56      (branch
57        NativeMemoryRoutineDuplicateLabel
58        labelName
59        .
60        (bytes-append b"ALPHA-MEM-001-" labelName))
61      (branch NativeMemoryRoutineOffsetOverflow . b"ALPHA-MEM-002")
62      (branch
63        NativeMemoryRoutineMissingLabel
64        labelName
65        .
66        (bytes-append b"ALPHA-MEM-003-" labelName))
67      (branch
68        NativeMemoryRoutineDisplacementOutOfRange
69        labelName
70        .
71        (bytes-append b"ALPHA-MEM-004-" labelName))))
72
73def nativeMemoryCopyInstructionCount : Nat =
74  (byte-to-nat (byte 11))
75
76-- Each target realizes one byte step; the termination loop has one owner.
77def nativeMemoryCopyStep =
78  (lambda unrestricted tail : (family X86NativeAssembly) .
79    (nativePhysicalNativeEmit
80      (nativePhysicalNativeLoad8
81        (constructor X86NativeRegister64 X86NativeRAX)
82        (constructor X86NativeRegister64 X86NativeRSI)
83        nativePhysicalNativeD0)
84      (nativePhysicalNativeEmit
85        (nativePhysicalNativeStore8
86          (constructor X86NativeRegister64 X86NativeRDI)
87          nativePhysicalNativeD0
88          (constructor X86NativeRegister64 X86NativeRAX))
89        (nativePhysicalNativeEmit
90          (nativePhysicalNativeAddImmediate
91            (constructor X86NativeRegister64 X86NativeRSI)
92            (nativePhysicalNativeI32Byte (byte 1)))
93          (nativePhysicalNativeEmit
94            (nativePhysicalNativeAddImmediate
95              (constructor X86NativeRegister64 X86NativeRDI)
96              (nativePhysicalNativeI32Byte (byte 1)))
97            (nativePhysicalNativeEmit
98              (nativePhysicalNativeAddImmediate
99                (constructor X86NativeRegister64 X86NativeRDX)
100                nativePhysicalNativeI32NegativeOne)
101              tail))))))
102
103def nativeMemoryCopyAssembly : (family X86NativeAssembly) =
104  (memoryCopyAssemblyFor
105    (family X86NativeAssembly)
106    nativeMemoryCopyStep
107    (nativePhysicalNativeEmit
108      (nativePhysicalNativeTest
109        (constructor X86NativeRegister64 X86NativeRDX)
110        (constructor X86NativeRegister64 X86NativeRDX)))
111    (nativePhysicalNativeJumpCondition (constructor X86NativeCondition X86NativeConditionZero))
112    (nativePhysicalNativeJumpCondition (constructor X86NativeCondition X86NativeConditionNotZero))
113    nativePhysicalNativeLabel
114    (lambda unrestricted tail : (family X86NativeAssembly) .
115      (nativePhysicalNativeEmit
116        (constructor
117          X86NativeInstruction
118          X86NativeClear32
119          (constructor X86NativeRegister64 X86NativeRAX))
120        (nativePhysicalNativeEmit nativePhysicalNativeReturnInstruction tail)))
121    (constructor X86NativeAssembly X86NativeAssemblyEnd))
122
123-- Canonical code identity used by target lowering; the diagnostic generator
124-- below adds its digest and report without changing these instruction bytes.
125-- Keep its assembler here: the compiler's native-encode intrinsic may choose
126-- another valid encoding, but host twin lookup keys the actual source bytes.
127def nativeMemoryCopyRoutineBytes : Bytes =
128  (eliminate
129    X86NativeAssemblyResult
130    (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
131    (x86NativeAssemble nativeMemoryCopyAssembly)
132    (branch X86NativeAssemblyEncoded code . code)
133    (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
134    (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
135    (branch X86NativeAssemblyMissingLabel name . b"")
136    (branch X86NativeAssemblyDisplacementOutOfRange name . b""))
137
138-- The shared forward copy returns zero, including for an empty region.
139-- Callers admit disjoint regions (or identical addresses), not memmove overlap.
140def nativeMemoryCopyCode : Bytes =
141  (compiler-native-encode (family X86NativeAssembly) nativeMemoryCopyAssembly)
142
143def nativeMemoryRoutineTelemetrySuccess =
144  (lambda unrestricted code : Bytes .
145    (lambda unrestricted digest : Bytes .
146      (constructor
147        NativeMemoryRoutineTelemetry
148        NativeMemoryRoutineTelemetryValue
149        nativeMemoryCopyInstructionCount
150        (bytes-length code)
151        zero
152        zero
153        digest
154        b"")))
155
156def nativeMemoryRoutineTelemetryFailure =
157  (lambda unrestricted error : (family NativeMemoryRoutineErrorCode) .
158    (constructor
159      NativeMemoryRoutineTelemetry
160      NativeMemoryRoutineTelemetryValue
161      nativeMemoryCopyInstructionCount
162      zero
163      (succ zero)
164      zero
165      b""
166      (nativeMemoryRoutineErrorCodeBytes error)))
167
168def nativeMemoryRoutineFail =
169  (lambda unrestricted error : (family NativeMemoryRoutineErrorCode) .
170    (constructor
171      NativeMemoryRoutineResult
172      NativeMemoryRoutineGenerationFailed
173      error
174      (nativeMemoryRoutineTelemetryFailure error)))
175
176-- Generation remains pure and byte-identical, but is requested by the
177-- actual lowering consumer rather than performed when this module is loaded.
178def nativeMemoryGenerateCopyRoutine :
179  (pi unrestricted request : Nat . (family NativeMemoryRoutineResult)) =
180  (lambda unrestricted request : Nat .
181    (eliminate
182      X86NativeAssemblyResult
183      (lambda unrestricted current : (family X86NativeAssemblyResult) .
184        (family NativeMemoryRoutineResult))
185      (x86NativeAssemble nativeMemoryCopyAssembly)
186      (branch
187        X86NativeAssemblyEncoded
188        code
189        .
190        (app
191          (lambda unrestricted digest : Bytes .
192            (app
193              (lambda unrestricted telemetry : (family NativeMemoryRoutineTelemetry) .
194                (constructor
195                  NativeMemoryRoutineResult
196                  NativeMemoryRoutineGenerated
197                  (constructor
198                    NativeMemoryRoutine
199                    NativeMemoryRoutineValue
200                    code
201                    digest
202                    nativeMemoryCopyInstructionCount
203                    telemetry)
204                  telemetry))
205              (nativeMemoryRoutineTelemetrySuccess code digest)))
206          (sha256HexBytesOrEmpty (sha256Hex code))))
207      (branch
208        X86NativeAssemblyEncodeDuplicateLabel
209        duplicateName
210        .
211        (nativeMemoryRoutineFail
212          (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineDuplicateLabel duplicateName)))
213      (branch
214        X86NativeAssemblyEncodeOffsetOverflow
215        .
216        (nativeMemoryRoutineFail
217          (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineOffsetOverflow)))
218      (branch
219        X86NativeAssemblyMissingLabel
220        missingName
221        .
222        (nativeMemoryRoutineFail
223          (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineMissingLabel missingName)))
224      (branch
225        X86NativeAssemblyDisplacementOutOfRange
226        distantName
227        .
228        (nativeMemoryRoutineFail
229          (constructor
230            NativeMemoryRoutineErrorCode
231            NativeMemoryRoutineDisplacementOutOfRange
232            distantName)))))
233
234-- Compare exactly rdx bytes at rdi/rsi, including empty buffers. Return 1 or
235-- 0, preserve callee-saved registers, and never read beyond the admitted views.
236-- This is integrity/header comparison, not a constant-time secret comparison.
237def nativeMemoryEqualAssembly : (family X86NativeAssembly) =
238  (nativePhysicalNativeEmit
239    (nativePhysicalNativeTest
240      (constructor X86NativeRegister64 X86NativeRDX)
241      (constructor X86NativeRegister64 X86NativeRDX))
242    (nativePhysicalNativeJumpCondition
243      (constructor X86NativeCondition X86NativeConditionZero)
244      b"memory-equal"
245      (nativePhysicalNativeLabel
246        b"memory-compare"
247        (nativePhysicalNativeEmit
248          (nativePhysicalNativeLoad8
249            (constructor X86NativeRegister64 X86NativeRAX)
250            (constructor X86NativeRegister64 X86NativeRDI)
251            nativePhysicalNativeD0)
252          (nativePhysicalNativeEmit
253            (nativePhysicalNativeLoad8
254              (constructor X86NativeRegister64 X86NativeRCX)
255              (constructor X86NativeRegister64 X86NativeRSI)
256              nativePhysicalNativeD0)
257            (nativePhysicalNativeEmit
258              (nativePhysicalNativeCompare
259                (constructor X86NativeRegister64 X86NativeRAX)
260                (constructor X86NativeRegister64 X86NativeRCX))
261              (nativePhysicalNativeJumpCondition
262                (constructor X86NativeCondition X86NativeConditionNotZero)
263                b"memory-different"
264                (nativePhysicalNativeEmit
265                  (nativePhysicalNativeAddImmediate
266                    (constructor X86NativeRegister64 X86NativeRDI)
267                    (nativePhysicalNativeI32Byte (byte 1)))
268                  (nativePhysicalNativeEmit
269                    (nativePhysicalNativeAddImmediate
270                      (constructor X86NativeRegister64 X86NativeRSI)
271                      (nativePhysicalNativeI32Byte (byte 1)))
272                    (nativePhysicalNativeEmit
273                      (nativePhysicalNativeAddImmediate
274                        (constructor X86NativeRegister64 X86NativeRDX)
275                        nativePhysicalNativeI32NegativeOne)
276                      (nativePhysicalNativeJumpCondition
277                        (constructor X86NativeCondition X86NativeConditionNotZero)
278                        b"memory-compare"
279                        (nativePhysicalNativeLabel
280                          b"memory-equal"
281                          (nativePhysicalNativeEmit
282                            (nativePhysicalNativeMoveImmediate32
283                              (constructor X86NativeRegister64 X86NativeRAX)
284                              (nativePhysicalNativeI32Byte (byte 1)))
285                            (nativePhysicalNativeEmit
286                              nativePhysicalNativeReturnInstruction
287                              (nativePhysicalNativeLabel
288                                b"memory-different"
289                                (nativePhysicalNativeEmit
290                                  (constructor
291                                    X86NativeInstruction
292                                    X86NativeClear32
293                                    (constructor X86NativeRegister64 X86NativeRAX))
294                                  (nativePhysicalNativeEmit
295                                    nativePhysicalNativeReturnInstruction
296                                    (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))))))))))
297
298def nativeMemoryEqualCode =
299  (compiler-native-encode (family X86NativeAssembly) nativeMemoryEqualAssembly)