module
public import Syscalls.Mmap
public import Syscalls.Memfd
@[expose] public section
open Aeneas Aeneas.Std Result

namespace Syscalls

/-- The Linux system-call boundary that the specifications trust: the host page
    size and the contracts of the system calls whose results the proofs use.

    Each field constrains a different opaque external (`pagesize`, `mmap64`,
    `munmap`, `ftruncate64`), so the fields cannot contradict each other. Add a
    contract as a new field when a proof needs one. The class has no instance:
    it is always an explicit assumption of the theorems that take it.

    `pageSize` is an output: the host has a single page size, so a theorem that
    doesn't mention it can still find the assumption in context. -/
class Linux (pageSize : outParam Usize) : Prop where
  /-- `sysconf(_SC_PAGESIZE)` returns `pageSize`. -/
  pagesize : vm_memory.base.sys.unix.system_info.pagesize = ok pageSize
  /-- The page size is a power of two. -/
  pageSize_pow : pageSize.val.isPowerOfTwo
  /-- `mmap(2)`; see `Syscalls.Mmap.MmapSpec`. -/
  mmap : Mmap.MmapSpec pageSize
  /-- `munmap(2)`; see `Syscalls.Mmap.MunmapSpec`. -/
  munmap : Mmap.MunmapSpec
  /-- `ftruncate(2)`; see `Syscalls.Memfd.FtruncateSpec`. -/
  ftruncate : Memfd.FtruncateSpec

end Syscalls