Set the permission of all non-frozen mapped bytes in [base, base + len) to p's protection bits, preserving their byte values, lazyFree state, and anon state; frozen and unmapped bytes (and bytes outside the range) are unchanged. Used for mprotect transitions between Perm.rw and Perm.protNone (mm/mprotect.c change_protection, which updates PTE protection bits without clearing folio_test_lazyfree or changing VMA vm_ops). Never touches frozen bytes.

Smallest byte offset curOff ≤ off < curOff + rem such that (m.perm (base + BitVec.ofNat 64 off)).mapped = true, or none if [base + curOff, base + curOff + rem) is completely unmapped. Tail-recursive so large probes run in constant stack space.

Low-to-high page-aligned gap search over [addr, USER_VA_LIMIT) (vm_unmapped_area in mm/mmap.c), advancing past the page containing any mapped byte on collision.

Lowest page-aligned unmapped range [base, base + size) within [MMAP_MIN_ADDR, USER_VA_LIMIT) (arch_get_unmapped_area / vm_unmapped_area in mm/mmap.c), or none when size = 0, size is not page-aligned, or no free gap of size bytes exists.

Sanitize an oracle mmap / mremap placement candidate cand for a page-aligned request of size bytes (size > 0, size % PAGE_SIZE = 0, mm/mmap.c get_unmapped_area -> security_mmap_addr):

• if MMAP_MIN_ADDR ≤ cand.toNat, cand is PAGE_SIZE-aligned, cand.toNat + size ≤ USER_VA_LIMIT, and m.canMap cand size = true, accepts cand directly;

• otherwise substitutes findUnmappedArea m size, returning none only when no unmapped page-aligned range of size bytes fits in [MMAP_MIN_ADDR, USER_VA_LIMIT).

Anonymous private mmap(addr, len, prot, flags, fd, 0) (__NR_mmap = 222, mm/mmap.c:1661 ksys_mmap_pgoff -> do_mmap) with prot ∈ {PROT_NONE (0), PROT_READ | PROT_WRITE (3)} and flags ∈ {MAP_PRIVATE | MAP_ANONYMOUS (0x22), MAP_PRIVATE | MAP_ANONYMOUS | MAP_STACK (0x20022), MAP_PRIVATE | MAP_ANONYMOUS | MAP_FIXED (0x32)} (MAP_STACK is an advisory VM_NOHUGEPAGE no-op on Linux AArch64; MAP_FIXED | MAP_STACK = 0x20032 remains fail-closed). Linux ignores fd for anonymous mappings, and so does the model. With size := pageAlignUp len and newPerm := Perm.protNone when prot = 0, Perm.rw when prot = 3:

• [INTENTIONAL_SCOPE]: other prot/flags/offset combinations (file mappings, MAP_SHARED, PROT_READ alone, PROT_EXEC, a non-zero offset, ...) are unmodeled and raise .Exception rather than being silently approximated;

• len = 0 returns -EINVAL without consulting the oracle;

• without MAP_FIXED, Linux treats addr as a hint only; the model ignores it and sanitizes cand := s.oracle.mmap s.oracleIdx ([INTENTIONAL_OVERAPPROX]) via sanitizeMmapAddr s.mem cand size (mm/mmap.c get_unmapped_area); when no free gap of size bytes exists (none), it transitions to the terminal ExecStatus.OutOfMemory outcome (s.setStatus .OutOfMemory);

• with MAP_FIXED (used for PROT_NONE guard pages and PROT_READ | PROT_WRITE demand-zero page overlays), addr must be page-aligned within [MMAP_MIN_ADDR, 2 ^ 48 - size] (mm/mmap.c get_unmapped_area -> security_mmap_addr) and touch no frozen bytes. With reclaimed := s.mem.countRw addr size, prot = PROT_NONE replaces [addr, addr + size) with zero-filled Perm.protNone pages and refunds reclaimed to s.physMemAvail; prot = PROT_READ | PROT_WRITE transitions to ExecStatus.OutOfMemory when size > s.physMemAvail + reclaimed, and otherwise replaces [addr, addr + size) with zero-filled Perm.rw pages and sets s.physMemAvail := s.physMemAvail + reclaimed - size.

• Physical memory accounting (s.physMemAvail): PROT_NONE mappings consume 0 physical bytes (accountable_mapping in mm/mmap.c); PROT_READ | PROT_WRITE mappings deduct the net newly committed writable bytes (size for non-fixed mappings, size - reclaimed net for MAP_FIXED) from s.physMemAvail, transitioning to ExecStatus.OutOfMemory if insufficient.

munmap(addr, len) (__NR_munmap = 215, mm/vma.c:1718 do_vmi_munmap). With size := pageAlignUp len:

• if addr is not page-aligned (addr.toNat % PAGE_SIZE != 0), len == 0, or [addr, addr + size) exceeds the 48-bit user virtual address space (addr.toNat + size > 2 ^ 48), returns -EINVAL;

• [INTENTIONAL_SCOPE]: if [addr, addr + size) intersects any frozen byte (some Perm.ro or some Perm.rx), fails closed with .Exception "munmap on frozen memory";

• otherwise unmaps all non-frozen bytes in [addr, addr + size) (s.mem.unmapNonFrozen addr size, allowing already-unmapped holes in the range per POSIX/Linux), refunds s.mem.countRw addr size to s.physMemAvail, and returns 0.

brk(addr) (__NR_brk = 214, mm/mmap.c:115 SYSCALL_DEFINE1(brk) -> do_brk_flags / do_brk_munmap): query or adjust the program break without consulting Oracle.

• [INTENTIONAL_SCOPE]: models single-threaded user-space execution under RLIMIT_DATA = RLIM_INFINITY and RLIMIT_AS = RLIM_INFINITY (check_data_rlimit in mm/mmap.c:134, may_expand_vm in mm/vma.c:3028), mm->map_count ≤ sysctl_max_map_count (mm/vma.c:3031), and no active MCL_FUTURE (mlock_future_ok in mm/vma.c:3034).

• Query or below-base (addr = 0 or addr < s.brkStart): returns the current break s.brk with memory and s.brk unchanged.

• Shrink or same-page (newPage ≤ oldPage, where oldPage := pageAlignUp s.brk.toNat and newPage := pageAlignUp addr.toNat, shrinkBytes := oldPage - newPage):

  • if newPage < oldPage and [newPage, oldPage) is not fully mapped (!s.mem.allPerm (·.mapped) (BitVec.ofNat 64 newPage) shrinkBytes, e.g. after munmap of the heap tail, matching !brkvma || brkvma->vm_start >= oldbrk in mm/mmap.c:167), returns the unchanged s.brk (origbrk) with memory and physMemAvail unchanged;

  • otherwise unmaps freed writable pages [newPage, oldPage) (s.mem.unmapWritable, do_brk_munmap in mm/mmap.c:155), refunds s.mem.countRw newPage shrinkBytes to s.physMemAvail, sets s.brk := addr, and returns addr.

• Grow (oldPage < newPage, growBytes := newPage - oldPage):

  1. VMA collision + BRK_GUARD_GAP (256 * PAGE_SIZE = 1 MiB) guard gap (newbrk + PAGE_SIZE > vm_start_gap(next) in mm/mmap.c:186): if newPage + BRK_GUARD_GAP > USER_VA_LIMIT or !s.mem.canMap (BitVec.ofNat 64 oldPage) (growBytes + BRK_GUARD_GAP), returns the unchanged s.brk in X0 with status = .Running so allocators (mallocng) deterministically fall back to SYS_mmap.

  2. Physical memory budget: if s.physMemAvail < growBytes, transitions to ExecStatus.OutOfMemory.

  3. Otherwise maps [oldPage, newPage) read-write and zero-filled (s.mem.mapZero), deducts growBytes from s.physMemAvail, sets s.brk := addr, and returns addr.