Module pt 

x86-64 Page Table (PT / L1)

This module models the lowest paging level (L1, Page Table).

• L1Index: index type for VA bits [20:12].
• PtEntry4k: a PT entry (PTE). At this level, PS must be 0; entries represent 4 KiB leaf mappings only.
• PageTable: a 4 KiB-aligned array of 512 PTEs.

Semantics

• L1 does not point to another table. Every present entry maps a 4 KiB page.
• The base address stored in a PTE must be 4 KiB-aligned (hardware requirement).

Invariants & Notes

• PageTable is 4 KiB-aligned and contains exactly 512 entries.
• PtEntry4k::present_with forces PS=0 and present=1.
• Raw constructors do not validate consistency; prefer typed helpers.
• After modifying active mappings, the caller must perform any required TLB maintenance.

Structs

L1Index

Index into the Page Table (derived from VA bits [20:12]).

PageTable

The Page Table (L1): 512 entries, 4 KiB-aligned.

PtEntry4k

L1 PTE (4 KiB leaf) — maps a single 4 KiB page (bit 7 is PAT).