Compiler.ELF

1module Compiler.ELF
2
3import Compiler.AST
4import Compiler.Lexer
5import Compiler.Parser
6import Compiler.Elaborator
7import Compiler.Codegen
8import Model.Parameter
9import Model.Word64
10import Std.Natural
11
12family ExecutableResult : Type 0
13constructor ExecutableGenerated
14field unrestricted executableBytes : Bytes
15constructor ExecutableUnboundVariable
16field unrestricted executableUnboundSpelling : Bytes
17constructor ExecutableUnsupportedTerm
18field unrestricted executableUnsupportedCode : Nat
19constructor ExecutableUnsupportedSuccessor
20
21end-family
22
23-- The ELF machines the physical executor is built for: e_machine 62
24-- (EM_X86_64) or 183 (EM_AARCH64).  Everything else in the header -- entry
25-- 0x400078, one PT_LOAD at 0x400000 with a 4 MiB memory extent, 4 KiB
26-- alignment -- is the same for both.
27def elfMachineX86_64 : Byte = (byte 62)
28def elfMachineAArch64 : Byte = (byte 183)
29
30-- the ELF identification and e_type, before e_machine
31def elfHeaderBeforeMachine : Bytes =
32  (bytes 127 69 76 70 2 1 1 0 0 0 0 0 0 0 0 0 2 0)
33
34-- from e_machine's second byte to the program header's p_filesz
35def elfHeaderAfterMachine : Bytes =
36  (bytes 0 1 0 0 0 120 0 64 0 0 0 0 0 64 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 64 0 56 0 1 0 0 0 0 0 0 0 1 0 0 0 5 0 0 0 0 0 0 0 0 0 0 0 0 0 64 0 0 0 0 0 0 0 64 0 0 0 0 0)
37
38def elfHeaderPrefix : Bytes =
39  (bytes-append elfHeaderBeforeMachine (bytes-append (bytes elfMachineX86_64) elfHeaderAfterMachine))
40
41def elfLoadSize64k : Bytes =
42  (bytes 0 0 4 0 0 0 0 0)
43
44def elfHeaderAlign : Bytes =
45  (bytes 0 16 0 0 0 0 0 0)
46
47def fixedZeroELFHeader : Bytes =
48  (bytes-append
49    elfHeaderPrefix
50    (bytes-append elfLoadSize64k (bytes-append elfLoadSize64k elfHeaderAlign)))
51
52def zeroPadding1 : Bytes =
53  (bytes 0)
54
55def zeroPadding2 : Bytes =
56  (bytes-append zeroPadding1 zeroPadding1)
57
58def zeroPadding4 : Bytes =
59  (bytes-append zeroPadding2 zeroPadding2)
60
61def zeroPadding8 : Bytes =
62  (bytes-append zeroPadding4 zeroPadding4)
63
64def zeroPadding16 : Bytes =
65  (bytes-append zeroPadding8 zeroPadding8)
66
67def zeroPadding32 : Bytes =
68  (bytes-append zeroPadding16 zeroPadding16)
69
70def zeroPadding64 : Bytes =
71  (bytes-append zeroPadding32 zeroPadding32)
72
73def zeroPadding128 : Bytes =
74  (bytes-append zeroPadding64 zeroPadding64)
75
76def zeroPadding256 : Bytes =
77  (bytes-append zeroPadding128 zeroPadding128)
78
79def zeroPadding512 : Bytes =
80  (bytes-append zeroPadding256 zeroPadding256)
81
82def zeroPadding1024 : Bytes =
83  (bytes-append zeroPadding512 zeroPadding512)
84
85def zeroPadding2048 : Bytes =
86  (bytes-append zeroPadding1024 zeroPadding1024)
87
88def zeroPadding4096 : Bytes =
89  (bytes-append zeroPadding2048 zeroPadding2048)
90
91def zeroPadding8192 : Bytes =
92  (bytes-append zeroPadding4096 zeroPadding4096)
93
94def zeroPadding16384 : Bytes =
95  (bytes-append zeroPadding8192 zeroPadding8192)
96
97def zeroPadding32768 : Bytes =
98  (bytes-append zeroPadding16384 zeroPadding16384)
99
100def zeroPadding65536 : Bytes =
101  (bytes-append zeroPadding32768 zeroPadding32768)
102
103def zeroPadding131072 : Bytes =
104  (bytes-append zeroPadding65536 zeroPadding65536)
105
106def zeroPadding262144 : Bytes =
107  (bytes-append zeroPadding131072 zeroPadding131072)
108
109def wrapMachineCode =
110  (lambda unrestricted machineCode : Bytes .
111    (bytes-append (bytes-append fixedZeroELFHeader machineCode) zeroPadding262144))
112
113-- Larger LOAD segment (4 MiB) for the PHYSICAL native-program path only (nvctl/GPU probes whose
114-- interpreted image body + embedded kernel + upload payloads exceed the 256 KiB fixedZeroELFHeader
115-- segment). The header LENGTH is byte-identical to fixedZeroELFHeader (120 bytes), so the machine
116-- code still starts at file offset 120 and the interpreter's state/scratch base is unchanged; only
117-- the mapped segment END moves out from 0x440000 to 0x800000. The self-host compiler ELF path
118-- (compileClosedZeroExecutable -> wrapMachineCode) is deliberately NOT changed, so its byte-identity
119-- is preserved. p_filesz = p_memsz = 0x00400000 (4 MiB); the file is padded to cover it.  The old
120-- 1-MiB physical segment was smaller than a valid 4,242-command checkpoint-resume program: Linux
121-- mapped only 0x400000..0x500000 and execution faulted exactly at the unmapped 0x500000 boundary.
122def zeroPadding524288 : Bytes =
123  (bytes-append zeroPadding262144 zeroPadding262144)
124
125def zeroPadding1048576 : Bytes =
126  (bytes-append zeroPadding524288 zeroPadding524288)
127
128def zeroPadding2097152 : Bytes =
129  (bytes-append zeroPadding1048576 zeroPadding1048576)
130
131def zeroPadding4194304 : Bytes =
132  (bytes-append zeroPadding2097152 zeroPadding2097152)
133
134def elfLoadSize4M : Bytes =
135  (bytes 0 0 64 0 0 0 0 0)
136
137def fixedZeroELFHeaderLarge : Bytes =
138  (bytes-append
139    elfHeaderPrefix
140    (bytes-append elfLoadSize4M (bytes-append elfLoadSize4M elfHeaderAlign)))
141
142def wrapMachineCodeLarge =
143  (lambda unrestricted machineCode : Bytes .
144    (bytes-append (bytes-append fixedZeroELFHeaderLarge machineCode) zeroPadding4194304))
145
146-- Encode a model word in the little-endian byte order used by ELF64 fields.
147def elfModelWord64Bytes =
148  (lambda unrestricted value : (family ModelWord64) .
149    (eliminate
150      ModelWord64
151      (lambda unrestricted current : (family ModelWord64) . Bytes)
152      value
153      (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 .
154        (bytes b0 b1 b2 b3 b4 b5 b6 b7))))
155
156-- The physical executor still receives the same 4 MiB PT_LOAD memory extent,
157-- but the file carries only its header and machine bytes, padded with zeros
158-- to the next 0x1000-byte page.  Linux zero-fills p_memsz - p_filesz,
159-- avoiding a 4 MiB compile-time Bytes value.  The page padding is not
160-- optional: the segment is not writable, and a kernel before 6.7 zeroes the
161-- rest of the last file-backed page itself (padzero) and fails the exec with
162-- EFAULT when it cannot write it -- measured 2026-09-24 on a RunPod host with
163-- Linux 6.5.0-44: every artifact died in execve with SIGSEGV; the same
164-- bytes padded to a page loaded.  With p_filesz ending on a page boundary
165-- there is no partial page to zero.
166def elfPageBytes : Nat = 4096
167
168-- zeroPadding<bit> when that bit of n is set
169def elfZerosIfBit =
170  (lambda unrestricted n : Nat . (lambda unrestricted bit : Nat . (lambda unrestricted chunk : Bytes .
171    (nat-eliminate (lambda unrestricted current : Nat . Bytes) b""
172      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Bytes . chunk))
173      (naturalModuloUnchecked (naturalDivideUnchecked n bit) 2)))))
174
175-- n zero bytes, n below a page
176def elfZerosBelowPage =
177  (lambda unrestricted n : Nat .
178    (bytes-append (elfZerosIfBit n 2048 zeroPadding2048) (bytes-append (elfZerosIfBit n 1024 zeroPadding1024)
179    (bytes-append (elfZerosIfBit n 512 zeroPadding512) (bytes-append (elfZerosIfBit n 256 zeroPadding256)
180    (bytes-append (elfZerosIfBit n 128 zeroPadding128) (bytes-append (elfZerosIfBit n 64 zeroPadding64)
181    (bytes-append (elfZerosIfBit n 32 zeroPadding32) (bytes-append (elfZerosIfBit n 16 zeroPadding16)
182    (bytes-append (elfZerosIfBit n 8 zeroPadding8) (bytes-append (elfZerosIfBit n 4 zeroPadding4)
183    (bytes-append (elfZerosIfBit n 2 zeroPadding2) (elfZerosIfBit n 1 zeroPadding1)))))))))))))
184
185-- the zeros that carry header + machine code to the next page
186def elfPagePadding =
187  (lambda unrestricted machineCode : Bytes .
188    (elfZerosBelowPage
189      (naturalModuloUnchecked
190        (naturalSaturatingSubtract elfPageBytes
191          (naturalModuloUnchecked (naturalAdd (byte-to-nat (byte 120)) (bytes-length machineCode)) elfPageBytes))
192        elfPageBytes)))
193
194-- elfHeaderPrefix for another e_machine
195def elfHeaderPrefixFor =
196  (lambda unrestricted machine : Byte .
197    (bytes-append elfHeaderBeforeMachine (bytes-append (bytes machine) elfHeaderAfterMachine)))
198
199def fixedZeroELFHeaderSparseLargeFor =
200  (lambda unrestricted machine : Byte .
201    (lambda unrestricted machineCode : Bytes .
202      (let unrestricted fileExtent =
203        (modelWord64FromNaturalTruncated
204          (naturalAdd (byte-to-nat (byte 120)) (naturalAdd (bytes-length machineCode) (bytes-length (elfPagePadding machineCode)))))
205      in
206        (bytes-append
207          (elfHeaderPrefixFor machine)
208          (bytes-append
209            (elfModelWord64Bytes fileExtent)
210            (bytes-append elfLoadSize4M elfHeaderAlign))))))
211
212def wrapMachineCodeSparseLargeFor =
213  (lambda unrestricted machine : Byte .
214    (lambda unrestricted machineCode : Bytes .
215      (bytes-append (fixedZeroELFHeaderSparseLargeFor machine machineCode) (bytes-append machineCode (elfPagePadding machineCode)))))
216
217-- The same container with its memory extent exactly its file extent.  The
218-- 4 MiB extent above dates from when the file itself had to cover the
219-- image; the file now does, and nothing is read from memory beyond it (an
220-- embedded artifact's payloads are read with pread).  The AArch64 host uses
221-- this one: a loader that maps no zero-filled tail is also one qemu-user
222-- accepts without the segment being writable, so the executable its tests
223-- run is the executable itself.  x86-64 keeps the 4 MiB extent, which is
224-- what its published executables carry.
225def fixedZeroELFHeaderExactFor =
226  (lambda unrestricted machine : Byte .
227    (lambda unrestricted machineCode : Bytes .
228      (let unrestricted fileExtent =
229        (elfModelWord64Bytes
230          (modelWord64FromNaturalTruncated
231            (naturalAdd (byte-to-nat (byte 120)) (naturalAdd (bytes-length machineCode) (bytes-length (elfPagePadding machineCode))))))
232      in
233        (bytes-append
234          (elfHeaderPrefixFor machine)
235          (bytes-append fileExtent (bytes-append fileExtent elfHeaderAlign))))))
236
237def wrapMachineCodeExactFor =
238  (lambda unrestricted machine : Byte .
239    (lambda unrestricted machineCode : Bytes .
240      (bytes-append (fixedZeroELFHeaderExactFor machine machineCode) (bytes-append machineCode (elfPagePadding machineCode)))))
241
242def fixedZeroELFHeaderSparseLarge = (fixedZeroELFHeaderSparseLargeFor elfMachineX86_64)
243
244def wrapMachineCodeSparseLarge = (wrapMachineCodeSparseLargeFor elfMachineX86_64)
245
246def fixedZeroELF : Bytes =
247  (wrapMachineCode fixedZeroMachineCode)
248
249def compileClosedZeroExecutable =
250  (lambda unrestricted result : (family ClosedNaturalElaboration) .
251    (eliminate
252      CodegenResult
253      (lambda unrestricted value : (family CodegenResult) . (family ExecutableResult))
254      (compileClosedNaturalElaboration result)
255      (branch
256        CodeGenerated
257        machineCode
258        .
259        (constructor ExecutableResult ExecutableGenerated (wrapMachineCode machineCode)))
260      (branch
261        CodegenUnboundVariable
262        codegenUnboundSpelling
263        .
264        (constructor ExecutableResult ExecutableUnboundVariable codegenUnboundSpelling))
265      (branch
266        CodegenUnsupportedTerm
267        codegenUnsupportedCode
268        .
269        (constructor ExecutableResult ExecutableUnsupportedTerm codegenUnsupportedCode))))
270
271def executableSample : (family ExecutableResult) =
272  (compileClosedZeroExecutable elaboratedParserSample)
273
274def executableSize : Nat =
275  (eliminate
276    ExecutableResult
277    (lambda unrestricted result : (family ExecutableResult) . Nat)
278    executableSample
279    (branch ExecutableGenerated executableBytes . (bytes-length executableBytes))
280    (branch ExecutableUnboundVariable executableUnboundSpelling . zero)
281    (branch ExecutableUnsupportedTerm executableUnsupportedCode . zero)
282    (branch ExecutableUnsupportedSuccessor . zero))