Stages 1/2 belong to the format: header and verified payload/digests.
This is the one shared owner of 3 data sync, 4 close, 5 rename, 6 directory
sync. Stage prefixes are only for controlled failure tests; normal callers
request all six. replace=0 publishes an immutable generation (NOREPLACE);
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.