Alloc.lean🔗

Virtual-Memory Allocator Syscalls

Re-exports the Linux 7.3 virtual-memory syscall models and bundles them into Syscall.allocTable and Syscall.alloc:

Arm64.Trusted.Syscalls.Mm.Mmap (mm/mmap.c, mm/vma.c: brk, munmap, mmap)
Arm64.Trusted.Syscalls.Mm.Mprotect (mm/mprotect.c: mprotect)
Arm64.Trusted.Syscalls.Mm.Mremap (mm/mremap.c: mremap)
Arm64.Trusted.Syscalls.Mm.Madvise (mm/madvise.c: madvise)

@[expose] public section

namespace Arm64

namespace Syscall

def allocTableL35–51 ↗#

Dispatch table for the virtual-memory allocator family (brk, munmap, mremap, mmap, mprotect, madvise).

def allocTable : List (BitVec 64 × (State → State)) :=
  [(SYS_BRK, execBrk),
   (SYS_MUNMAP, execMunmap),
   (SYS_MREMAP, execMremap),
   (SYS_MMAP, execMmap),
   (SYS_MPROTECT, execMprotect),
   (SYS_MADVISE, execMadvise)]

1 declaration not shown (lines 45–46): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.alloc

end Syscall

end Arm64