Runtime.NativeFilePlan

Linux x86-64 file realization through the maintained native program. Exact pread/pwrite counts are required; partial IO or EINTR aborts this attempt. No close or rename is replayed. The caller owns candidate paths and storage durability admission: candidate and committed must be on the admitted local filesystem and directory must name the committed path's containing directory. These bindings are planner/caller obligations, not inferred from argv here. All filesystem errors fail closed, never become empty checkpoints. ABI: Linux UAPI unistd_64.h and fcntl.h; publication ordering: https://man7.org/linux/man-pages/man2/fsync.2.html 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))))))))