1module Runtime.NativeFilePlan
2
3import Runtime.NativeDescriptor
4import Runtime.NativePhysicalProgram
5import Runtime.NativeLaunchRecipeLoad
6import Std.Natural
7
8-- Linux x86-64 file realization through the maintained native program. Exact
9-- pread/pwrite counts are required; partial IO or EINTR aborts this attempt.
10-- No close or rename is replayed. The caller owns candidate paths and storage
11-- durability admission: candidate and committed must be on the admitted local
12-- filesystem and directory must name the committed path's containing directory.
13-- These bindings are planner/caller obligations, not inferred from argv here.
14-- All filesystem errors fail closed, never become empty
15-- checkpoints. ABI: Linux UAPI unistd_64.h and fcntl.h; publication ordering:
16-- https://man7.org/linux/man-pages/man2/fsync.2.html
17-- https://man7.org/linux/man-pages/man2/renameat2.2.html
18def nativeFileCall =
19 (lambda unrestricted number : Nat .
20 (lambda unrestricted arguments : (family NativePhysicalArguments) .
21 (lambda unrestricted slot : Nat .
22 (lambda unrestricted expected : Nat .
23 (lambda unrestricted error : Bytes .
24 (lambda unrestricted tail : (family NativePhysicalCommands) .
25 (nativeLaunchRecipeCommand
26 (constructor
27 NativePhysicalOperation
28 NativePhysicalSystemCall
29 (nativeLaunchRecipeImmediate number)
30 arguments
31 b""
32 (nativeLaunchRecipeStore slot))
33 error
34 (nativeLaunchRecipeAssertEqual
35 (nativeLaunchRecipeSlotValue slot)
36 (nativeLaunchRecipeImmediate expected)
37 error
38 tail))))))))
39
40def nativeFileOpen =
41 (lambda unrestricted path : (family NativePhysicalOperand) .
42 (lambda unrestricted flags : Nat .
43 (lambda unrestricted descriptorSlot : Nat .
44 (lambda unrestricted scratch : Nat .
45 (lambda unrestricted error : Bytes .
46 (lambda unrestricted tail : (family NativePhysicalCommands) .
47 (nativeLaunchRecipeCommand
48 (constructor
49 NativePhysicalOperation
50 NativePhysicalSystemCall
51 (nativeLaunchRecipeImmediate 257)
52 (nativeLaunchRecipeArguments
53 (nativeLaunchRecipeImmediate 18446744073709551516)
54 path
55 (nativeLaunchRecipeImmediate flags)
56 (nativeLaunchRecipeImmediate 384))
57 b""
58 (nativeLaunchRecipeStore descriptorSlot))
59 error
60 (nativeDescriptorRequire
61 (nativeLaunchRecipeSlotValue descriptorSlot)
62 scratch
63 error
64 tail))))))))
65
66-- O_CLOEXEC | O_NOFOLLOW | O_NONBLOCK; pread on a non-seekable object fails.
67def nativeFileReadFlags : Nat =
68 657408
69
70-- O_CLOEXEC | O_NOFOLLOW | O_CREAT | O_EXCL | O_RDWR, mode 0600.
71def nativeFileCandidateFlags : Nat =
72 655554
73
74def nativeFileWhen =
75 (lambda unrestricted flag : Nat .
76 (lambda unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
77 (lambda unrestricted tail : (family NativePhysicalCommands) .
78 (nat-eliminate
79 (lambda unrestricted admitted : Nat . (family NativePhysicalCommands))
80 tail
81 (lambda unrestricted previous : Nat .
82 (lambda unrestricted ignored : (family NativePhysicalCommands) . (fragment tail)))
83 flag))))
84
85def nativeFileRead =
86 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
87 (lambda unrestricted buffer : (family NativePhysicalOperand) .
88 (lambda unrestricted extent : Nat .
89 (lambda unrestricted offset : (family NativePhysicalOperand) .
90 (lambda unrestricted slot : Nat .
91 (lambda unrestricted error : Bytes .
92 (nativeFileCall
93 17
94 (nativeLaunchRecipeArguments
95 descriptor
96 buffer
97 (nativeLaunchRecipeImmediate extent)
98 offset)
99 slot
100 extent
101 error)))))))
102
103def nativeFileWrite =
104 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
105 (lambda unrestricted buffer : (family NativePhysicalOperand) .
106 (lambda unrestricted extent : Nat .
107 (lambda unrestricted offset : (family NativePhysicalOperand) .
108 (lambda unrestricted slot : Nat .
109 (lambda unrestricted error : Bytes .
110 (nativeFileCall
111 18
112 (nativeLaunchRecipeArguments
113 descriptor
114 buffer
115 (nativeLaunchRecipeImmediate extent)
116 offset)
117 slot
118 extent
119 error)))))))
120
121def nativeFileRequireEOF =
122 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
123 (lambda unrestricted probe : (family NativePhysicalOperand) .
124 (lambda unrestricted offset : Nat .
125 (lambda unrestricted slot : Nat .
126 (lambda unrestricted tail : (family NativePhysicalCommands) .
127 (nativeFileCall
128 17
129 (nativeLaunchRecipeArguments
130 descriptor
131 probe
132 (nativeLaunchRecipeImmediate 1)
133 (nativeLaunchRecipeImmediate offset))
134 slot
135 0
136 b"checkpoint-trailing-bytes"
137 tail))))))
138
139def nativeFileClose =
140 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
141 (lambda unrestricted slot : Nat .
142 (lambda unrestricted error : Bytes .
143 (nativeFileCall
144 3
145 (nativeLaunchRecipeArguments
146 descriptor
147 (nativeLaunchRecipeImmediate 0)
148 (nativeLaunchRecipeImmediate 0)
149 (nativeLaunchRecipeImmediate 0))
150 slot
151 0
152 error))))
153
154def nativeFileRename =
155 (lambda unrestricted replace : Nat .
156 (lambda unrestricted candidate : (family NativePhysicalOperand) .
157 (lambda unrestricted committed : (family NativePhysicalOperand) .
158 (lambda unrestricted slot : Nat .
159 (lambda unrestricted tail : (family NativePhysicalCommands) .
160 (nat-eliminate
161 (lambda unrestricted policy : Nat . (family NativePhysicalCommands))
162 (nativeFileCall
163 316
164 (constructor
165 NativePhysicalArguments
166 NativePhysicalArgumentsValue
167 (nativeLaunchRecipeImmediate 18446744073709551516)
168 candidate
169 (nativeLaunchRecipeImmediate 18446744073709551516)
170 committed
171 (nativeLaunchRecipeImmediate 1)
172 (nativeLaunchRecipeImmediate 0))
173 slot
174 0
175 b"checkpoint-rename"
176 tail)
177 (lambda unrestricted previous : Nat .
178 (lambda unrestricted ignored : (family NativePhysicalCommands) .
179 (nativeFileCall
180 82
181 (nativeLaunchRecipeArguments
182 candidate
183 committed
184 (nativeLaunchRecipeImmediate 0)
185 (nativeLaunchRecipeImmediate 0))
186 slot
187 0
188 b"checkpoint-rename"
189 tail)))
190 replace))))))
191
192-- Stages 1/2 belong to the format: header and verified payload/digests.
193-- This is the one shared owner of 3 data sync, 4 close, 5 rename, 6 directory
194-- sync. Stage prefixes are only for controlled failure tests; normal callers
195-- request all six. replace=0 publishes an immutable generation (NOREPLACE);
196-- replace=1 preserves the existing single-output host-request contract.
197def nativeFileCommitStages =
198 (lambda unrestricted stages : Nat .
199 (lambda unrestricted replace : Nat .
200 (lambda unrestricted descriptorSlot : Nat .
201 (lambda unrestricted scratch : Nat .
202 (lambda unrestricted candidate : (family NativePhysicalOperand) .
203 (lambda unrestricted committed : (family NativePhysicalOperand) .
204 (lambda unrestricted directory : (family NativePhysicalOperand) .
205 (lambda unrestricted tail : (family NativePhysicalCommands) .
206 (let unrestricted stage =
207 (lambda unrestricted index : Nat .
208 (nativeFileWhen (naturalLessOrEqual index stages)))
209 in
210 (stage
211 3
212 (lambda unrestricted after : (family NativePhysicalCommands) .
213 (nativeFileCall
214 75
215 (nativeLaunchRecipeArguments
216 (nativeLaunchRecipeSlotValue descriptorSlot)
217 (nativeLaunchRecipeImmediate 0)
218 (nativeLaunchRecipeImmediate 0)
219 (nativeLaunchRecipeImmediate 0))
220 scratch
221 0
222 b"checkpoint-sync"
223 after))
224 (stage
225 4
226 (lambda unrestricted after : (family NativePhysicalCommands) .
227 (nativeFileClose
228 (nativeLaunchRecipeSlotValue descriptorSlot)
229 scratch
230 b"checkpoint-close"
231 after))
232 (stage
233 5
234 (lambda unrestricted after : (family NativePhysicalCommands) .
235 (nativeFileRename replace candidate committed scratch after))
236 (stage
237 6
238 (lambda unrestricted after : (family NativePhysicalCommands) .
239 (nativeFileOpen
240 directory
241 65536
242 descriptorSlot
243 scratch
244 b"checkpoint-directory-open"
245 (nativeFileCall
246 74
247 (nativeLaunchRecipeArguments
248 (nativeLaunchRecipeSlotValue descriptorSlot)
249 (nativeLaunchRecipeImmediate 0)
250 (nativeLaunchRecipeImmediate 0)
251 (nativeLaunchRecipeImmediate 0))
252 scratch
253 0
254 b"checkpoint-directory-sync"
255 (nativeFileClose
256 (nativeLaunchRecipeSlotValue descriptorSlot)
257 scratch
258 b"checkpoint-directory-close"
259 after))))
260 tail)))))))))))))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.