module Runtime.NativeFilePlan

import Runtime.NativeDescriptor
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad
import Std.Natural

-- 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
def nativeFileCall =
  (lambda unrestricted number : Nat .
    (lambda unrestricted arguments : (family NativePhysicalArguments) .
      (lambda unrestricted slot : Nat .
        (lambda unrestricted expected : Nat .
          (lambda unrestricted error : Bytes .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalSystemCall
                  (nativeLaunchRecipeImmediate number)
                  arguments
                  b""
                  (nativeLaunchRecipeStore slot))
                error
                (nativeLaunchRecipeAssertEqual
                  (nativeLaunchRecipeSlotValue slot)
                  (nativeLaunchRecipeImmediate expected)
                  error
                  tail))))))))

def nativeFileOpen =
  (lambda unrestricted path : (family NativePhysicalOperand) .
    (lambda unrestricted flags : Nat .
      (lambda unrestricted descriptorSlot : Nat .
        (lambda unrestricted scratch : Nat .
          (lambda unrestricted error : Bytes .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalSystemCall
                  (nativeLaunchRecipeImmediate 257)
                  (nativeLaunchRecipeArguments
                    (nativeLaunchRecipeImmediate 18446744073709551516)
                    path
                    (nativeLaunchRecipeImmediate flags)
                    (nativeLaunchRecipeImmediate 384))
                  b""
                  (nativeLaunchRecipeStore descriptorSlot))
                error
                (nativeDescriptorRequire
                  (nativeLaunchRecipeSlotValue descriptorSlot)
                  scratch
                  error
                  tail))))))))

-- O_CLOEXEC | O_NOFOLLOW | O_NONBLOCK; pread on a non-seekable object fails.
def nativeFileReadFlags : Nat =
  657408

-- O_CLOEXEC | O_NOFOLLOW | O_CREAT | O_EXCL | O_RDWR, mode 0600.
def nativeFileCandidateFlags : Nat =
  655554

def nativeFileWhen =
  (lambda unrestricted flag : Nat .
    (lambda unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (nat-eliminate
          (lambda unrestricted admitted : Nat . (family NativePhysicalCommands))
          tail
          (lambda unrestricted previous : Nat .
            (lambda unrestricted ignored : (family NativePhysicalCommands) . (fragment tail)))
          flag))))

def nativeFileRead =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted buffer : (family NativePhysicalOperand) .
      (lambda unrestricted extent : Nat .
        (lambda unrestricted offset : (family NativePhysicalOperand) .
          (lambda unrestricted slot : Nat .
            (lambda unrestricted error : Bytes .
              (nativeFileCall
                17
                (nativeLaunchRecipeArguments
                  descriptor
                  buffer
                  (nativeLaunchRecipeImmediate extent)
                  offset)
                slot
                extent
                error)))))))

def nativeFileWrite =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted buffer : (family NativePhysicalOperand) .
      (lambda unrestricted extent : Nat .
        (lambda unrestricted offset : (family NativePhysicalOperand) .
          (lambda unrestricted slot : Nat .
            (lambda unrestricted error : Bytes .
              (nativeFileCall
                18
                (nativeLaunchRecipeArguments
                  descriptor
                  buffer
                  (nativeLaunchRecipeImmediate extent)
                  offset)
                slot
                extent
                error)))))))

def nativeFileRequireEOF =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted probe : (family NativePhysicalOperand) .
      (lambda unrestricted offset : Nat .
        (lambda unrestricted slot : Nat .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (nativeFileCall
              17
              (nativeLaunchRecipeArguments
                descriptor
                probe
                (nativeLaunchRecipeImmediate 1)
                (nativeLaunchRecipeImmediate offset))
              slot
              0
              b"checkpoint-trailing-bytes"
              tail))))))

def nativeFileClose =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted slot : Nat .
      (lambda unrestricted error : Bytes .
        (nativeFileCall
          3
          (nativeLaunchRecipeArguments
            descriptor
            (nativeLaunchRecipeImmediate 0)
            (nativeLaunchRecipeImmediate 0)
            (nativeLaunchRecipeImmediate 0))
          slot
          0
          error))))

def nativeFileRename =
  (lambda unrestricted replace : Nat .
    (lambda unrestricted candidate : (family NativePhysicalOperand) .
      (lambda unrestricted committed : (family NativePhysicalOperand) .
        (lambda unrestricted slot : Nat .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (nat-eliminate
              (lambda unrestricted policy : Nat . (family NativePhysicalCommands))
              (nativeFileCall
                316
                (constructor
                  NativePhysicalArguments
                  NativePhysicalArgumentsValue
                  (nativeLaunchRecipeImmediate 18446744073709551516)
                  candidate
                  (nativeLaunchRecipeImmediate 18446744073709551516)
                  committed
                  (nativeLaunchRecipeImmediate 1)
                  (nativeLaunchRecipeImmediate 0))
                slot
                0
                b"checkpoint-rename"
                tail)
              (lambda unrestricted previous : Nat .
                (lambda unrestricted ignored : (family NativePhysicalCommands) .
                  (nativeFileCall
                    82
                    (nativeLaunchRecipeArguments
                      candidate
                      committed
                      (nativeLaunchRecipeImmediate 0)
                      (nativeLaunchRecipeImmediate 0))
                    slot
                    0
                    b"checkpoint-rename"
                    tail)))
              replace))))))

-- 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.
def nativeFileCommitStages =
  (lambda unrestricted stages : Nat .
    (lambda unrestricted replace : Nat .
      (lambda unrestricted descriptorSlot : Nat .
        (lambda unrestricted scratch : Nat .
          (lambda unrestricted candidate : (family NativePhysicalOperand) .
            (lambda unrestricted committed : (family NativePhysicalOperand) .
              (lambda unrestricted directory : (family NativePhysicalOperand) .
                (lambda unrestricted tail : (family NativePhysicalCommands) .
                  (let unrestricted stage =
                    (lambda unrestricted index : Nat .
                      (nativeFileWhen (naturalLessOrEqual index stages)))
                    in
                    (stage
                      3
                      (lambda unrestricted after : (family NativePhysicalCommands) .
                        (nativeFileCall
                          75
                          (nativeLaunchRecipeArguments
                            (nativeLaunchRecipeSlotValue descriptorSlot)
                            (nativeLaunchRecipeImmediate 0)
                            (nativeLaunchRecipeImmediate 0)
                            (nativeLaunchRecipeImmediate 0))
                          scratch
                          0
                          b"checkpoint-sync"
                          after))
                      (stage
                        4
                        (lambda unrestricted after : (family NativePhysicalCommands) .
                          (nativeFileClose
                            (nativeLaunchRecipeSlotValue descriptorSlot)
                            scratch
                            b"checkpoint-close"
                            after))
                        (stage
                          5
                          (lambda unrestricted after : (family NativePhysicalCommands) .
                            (nativeFileRename replace candidate committed scratch after))
                          (stage
                            6
                            (lambda unrestricted after : (family NativePhysicalCommands) .
                              (nativeFileOpen
                                directory
                                65536
                                descriptorSlot
                                scratch
                                b"checkpoint-directory-open"
                                (nativeFileCall
                                  74
                                  (nativeLaunchRecipeArguments
                                    (nativeLaunchRecipeSlotValue descriptorSlot)
                                    (nativeLaunchRecipeImmediate 0)
                                    (nativeLaunchRecipeImmediate 0)
                                    (nativeLaunchRecipeImmediate 0))
                                  scratch
                                  0
                                  b"checkpoint-directory-sync"
                                  (nativeFileClose
                                    (nativeLaunchRecipeSlotValue descriptorSlot)
                                    scratch
                                    b"checkpoint-directory-close"
                                    after))))
                            tail)))))))))))))