State.lean🔗

Declarations on this page (82)

ARM64 Architectural State (Arm64.State)

Layer / Role: Arm64 Trusted Computing Base (Role::Spec, definitions only, 0 theorems).
Purpose & Key Exports: Programmer-visible AArch64 machine state (State), including condition flags (PState: n, z, c, v), 64-bit general-purpose registers (RegFile), 128-bit SIMD/FP registers (VRegFile), execution status (ExecStatus), nondeterministic oracle (Oracle, Timespec), recorded signal dispositions and alternate signal stack (SigAction, SigAltStack), and state accessors (readReg64, writeReg64, readReg32, writeReg32, readVReg128, writeVReg128, advancePC, setPC).
When to read: Read when writing or auditing State field projections in Spec.lean or checking register/flag/oracle representations; use ProofLib/State.lean for rewrite lemmas.

@[expose] public section

namespace Arm64

Processor condition flags (N, Z, C, V).

@[ext]
structure PState where
  n : Bool := false
  z : Bool := false
  c : Bool := false
  v : Bool := false
  deriving DecidableEq, Repr, Inhabited, BEq

namespace PState

def zeroL44–45 ↗#

All condition flags clear (NZCV = 0b0000).

def zero : PState := { n := false, z := false, c := false, v := false }

def ofBits4L47–52 ↗#

Construct PState from a 4-bit nzcv immediate (N=bit 3, Z=bit 2, C=bit 1, V=bit 0).

def ofBits4 (b : BitVec 4) : PState :=
  { n := b.getLsbD 3
    z := b.getLsbD 2
    c := b.getLsbD 1
    v := b.getLsbD 0 }

end PState

structure RegFileL56–59 ↗#

General-purpose register file (X0..X30, indexed by BitVec 5).

@[ext]
structure RegFile where
  regs : BitVec 5 → BitVec 64

namespace RegFile

def emptyL66–67 ↗#

The all-zero general-purpose register file.

def empty : RegFile := { regs := fun _ => 0#64 }

def readL69–72 ↗#

Read general-purpose register idx. Note this is the raw indexed read; XZR/SP disambiguation happens in State.readReg64.

def read (rf : RegFile) (idx : BitVec 5) : BitVec 64 :=
  rf.regs idx

def writeL74–77 ↗#

Write general-purpose register idx. Note this is the raw indexed write; XZR/SP disambiguation happens in State.writeReg64.

def write (rf : RegFile) (idx : BitVec 5) (val : BitVec 64) : RegFile :=
  { regs := fun i => if i = idx then val else rf.regs i }

end RegFile

structure VRegFileL81–84 ↗#

128-bit SIMD/FP register file (V0..V31 / Q0..Q31 / D0..D31 / S0..S31 / H0..H31 / B0..B31, indexed by BitVec 5).

@[ext]
structure VRegFile where
  regs : BitVec 5 → BitVec 128

namespace VRegFile

def emptyL91–92 ↗#

The all-zero SIMD/FP register file.

def empty : VRegFile := { regs := fun _ => 0#128 }

def readL94–96 ↗#

Read the full 128 bits of SIMD/FP register idx.

def read (vf : VRegFile) (idx : BitVec 5) : BitVec 128 :=
  vf.regs idx

def writeL98–100 ↗#

Write the full 128 bits of SIMD/FP register idx.

def write (vf : VRegFile) (idx : BitVec 5) (val : BitVec 128) : VRegFile :=
  { regs := fun i => if i = idx then val else vf.regs i }

end VRegFile

inductive OutputStreamL104–110 ↗#

Output stream destination for byte-granular write events (stdout = fd 1, stderr = fd 2, or an arbitrary file descriptor fd).

inductive OutputStream where
  | stdout
  | stderr
  | fd (num : BitVec 64)
  deriving DecidableEq, Repr, Inhabited, BEq

namespace OutputStream

def ofFdL114–118 ↗#

Map a Linux file descriptor (1 = stdout, 2 = stderr) to its OutputStream.

def ofFd (fd : BitVec 64) : OutputStream :=
  if fd == 1#64 then .stdout
  else if fd == 2#64 then .stderr
  else .fd fd

end OutputStream

inductive TraceEventL122–136 ↗#

Observable event in the execution trace.

inductive TraceEvent where
  /-- A byte written by the `write` system call (byte granularity). -/
  | writeByte (stream : OutputStream) (byte : BitVec 8)
  /-- An event defined by a user of the semantics. The semantics never produces it; it is for
      externs (`Program.externs`) to record observable effects that the semantics does not model
      (e.g. bytes received from the network, or random bytes generated). -/
  | userDefined (tag : String) (payload : List (BitVec 8))
  /-- `openat` changed the contents of regular file `path` without writing bytes: it created the
      missing file (`O_CREAT`) or truncated an existing one (`O_TRUNC`, also when it was already
      empty). Not output (`traceStreamBytes` drops it). With the `writeByte (.fd _)` events of
      `write`, it is an event of every system call that changes `FsState.files`, so a trace
      segment without either event tells that the system calls left the files alone. -/
  | fileChanged (path : String)
  deriving DecidableEq, Repr, Inhabited, BEq

namespace TraceEvent

2 declarations not shown (lines 140–144): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.TraceEvent.stdout, Arm64.TraceEvent.stderr

def ofBytesL146–148 ↗#

Convert a sequence of bytes written to stream into byte-granular TraceEvents.

def ofBytes (stream : OutputStream) (bytes : List (BitVec 8)) : List TraceEvent :=
  bytes.map (.writeByte stream)

end TraceEvent

inductive ExecStatusL152–170 ↗#

Execution status of the machine state.

inductive ExecStatus where
  | Running
  | Halted
  | Exited (code : BitVec 64)
  /-- Fatal signal termination (for example `tkill`/`tgkill` delivering `SIGABRT = 6` to the
      calling thread in `abort()`). A POSIX parent shell or `qemu-aarch64` observes wait status
      `128 + sig.toNat` (`134` for `SIGABRT = 6`). -/
  | Signaled (sig : BitVec 7)
  /-- A Rust panic entry point was reached (see `Arm64.Rust.panicExterns`). With
      `panic = abort` a panic never returns, so it ends execution like `exit`. -/
  | Panicked
  /-- A virtual-memory or physical-memory exhaustion condition occurred in `brk`, `mmap`,
      `mprotect`, or `mremap` (either no free 48-bit user virtual-address gap of the requested
      size exists in `mmap`, or the net new `Perm.rw` bytes required exceed `State.physMemAvail`).
      Ends execution like `exit` or `panic`. -/
  | OutOfMemory
  | Exception (msg : String)
  deriving DecidableEq, Repr, Inhabited, BEq

structure TimespecL172–213 ↗#

Per-call result of a Linux AArch64 clock_gettime syscall (struct __kernel_timespec in include/uapi/linux/time_types.h, written by put_timespec64 in kernel/time/time.c).

Per-call invariants guaranteed by the Linux kernel across all modeled clock IDs 0..7 (CLOCK_REALTIME = 0, CLOCK_MONOTONIC = 1, CLOCK_PROCESS_CPUTIME_ID = 2, CLOCK_THREAD_CPUTIME_ID = 3, CLOCK_MONOTONIC_RAW = 4, CLOCK_REALTIME_COARSE = 5, CLOCK_MONOTONIC_COARSE = 6, CLOCK_BOOTTIME = 7 in kernel/time/posix-timers.c and lib/vdso/gettimeofday.c):

Normalized nanoseconds (0 ≤ tv_nsec < 1_000_000_000, enforced by Fin 1000000000): high-resolution getters (ktime_get_real_ts64, ktime_get_ts64, ktime_get_raw_ts64 in kernel/time/timekeeping.c and vDSO do_hres in lib/vdso/gettimeofday.c) reduce nanoseconds via __iter_div_u64_rem(..., NSEC_PER_SEC, &ns); coarse getters (ktime_get_coarse_real_ts64, ktime_get_coarse_ts64 and vDSO do_coarse) and time-namespace offset additions (timens_add_monotonic, timens_add_boottime in include/linux/time_namespace.h) normalize via set_normalized_timespec64 (kernel/time/time.c), which adjusts tv_sec in both loops while (nsec >= NSEC_PER_SEC) and while (nsec < 0) so 0 ≤ tv_nsec < 1_000_000_000 even when tv_sec < 0; and CLOCK_BOOTTIME (ktime_get_boottime_ts64) and CPU clocks (posix_cpu_clock_get in kernel/time/posix-cpu-timers.c) convert s64 nanoseconds via ns_to_timespec64 (kernel/time/time.c), which likewise guarantees 0 ≤ tv_nsec < 1_000_000_000.
Seconds (sec : BitVec 64, unconstrained): CLOCK_REALTIME (0) and CLOCK_REALTIME_COARSE (5) cannot be set before the 1970 epoch (timespec64_valid in include/linux/time64.h rejects ts->tv_sec < 0, and timespec64_valid_settod is enforced by do_settimeofday64, timekeeping_inject_offset, and timekeeping_init in kernel/time/timekeeping.c, as well as do_sys_settimeofday64 in kernel/time/posix-stubs.c). In the initial time namespace (init_time_ns), all eight clocks 0..7 satisfy tv_sec ≥ 0. However, under CONFIG_TIME_NS (CLONE_NEWTIME), proc_timens_set_offset (kernel/time/namespace.c) validates a negative CLOCK_MONOTONIC offset against high-resolution ktime_get_ts64 (tp.tv_sec ≥ 0), whereas posix_get_monotonic_coarse (CLOCK_MONOTONIC_COARSE = 6) and posix_get_monotonic_raw (CLOCK_MONOTONIC_RAW = 4) apply that same ns->offsets.monotonic via timens_add_monotonic (kernel/time/posix-timers.c, lib/vdso/gettimeofday.c): because ktime_get_coarse_ts64 omits the sub-tick timekeeping_get_ns(&tk->tkr_mono) delta and ktime_get_raw_ts64 omits NTP slewing, timens_add_monotonic can normalize tv_sec to a negative value (e.g. -1) while keeping 0 ≤ tv_nsec < 1_000_000_000. Moreover, even for single calls, CLOCK_REALTIME can jump backward across calls (clock_settime / adjtimex). Leaving sec : BitVec 64 unconstrained with nsec : Fin 1000000000 therefore captures the exact per-call invariant guaranteed across all clocks 0..7.

structure Timespec where
  sec  : BitVec 64 := 0#64
  nsec : Fin 1000000000 := ⟨0, Nat.zero_lt_succ _⟩
  deriving DecidableEq, Repr, Inhabited, BEq

structure OracleL215–251 ↗#

Results of the nondeterministic system calls. Query n is the n-th nondeterministic syscall of the run, counting from zero (State.oracleIdx).

Step stays deterministic. The nondeterminism comes from the initial state: specs such as subroutine_ok quantify over every entry state s0, so they hold for every s0.oracle, i.e. for every possible kernel behaviour. Indexing by the query count loses nothing: given s0, the whole history before query n is determined, so a kernel that looks at that history (including the clock ID passed to clock_gettime) is still just some function of n.

mmap n: preferred address candidate for the n-th query if it is an anonymous mmap or mremap(..., MREMAP_MAYMOVE). execMmap and execMremap sanitize the candidate (mm/mmap.c get_unmapped_area): if it is below MMAP_MIN_ADDR, not page-aligned, exceeds the 48-bit user virtual address space (2 ^ 48), or overlaps an already-mapped byte, they deterministically substitute the lowest free page-aligned gap in [MMAP_MIN_ADDR, 2 ^ 48) that fits, failing only when no free gap of the requested size exists,
mremapFail n: whether the n-th query refuses an mremap(..., MREMAP_MAYMOVE) with -ENOMEM (leaving the existing mapping intact), conservatively retained to over-approximate nondeterministic mremap refusal (e.g. RLIMIT_AS / vm.max_map_count or allocator fallback paths from mremap to mmap),
getrandom n i: byte i of the buffer filled by the n-th query if it is a getrandom,
clockGettime n: normalized struct timespec (0 ≤ nsec < 1_000_000_000) written by the n-th query if it is a successful clock_gettime, with no monotonicity relation between successive queries,
exclFails: finite schedule of spurious store-exclusive (STXR*/STLXR*/STXP/STLXP) failures copied into State.exclFails at process load time (ElfImage.loadState). Every execution has finitely many spurious failures, adversarially placed (headD false, consumed per non-faulting store-exclusive). This models eventual LL/SC progress without an exclusive monitor; a retry-less stxr is unprovable because exclFails = [true] is a valid initial state.

structure Oracle where
  mmap         : Nat → BitVec 64 := fun _ => 0#64
  mremapFail   : Nat → Bool := fun _ => false
  getrandom    : Nat → Nat → BitVec 8 := fun _ _ => 0#8
  clockGettime : Nat → Timespec := fun _ => {}
  exclFails    : List Bool := []

inductive FsEntryL255–259 ↗#

Inode payload in the local file system (file byte sequence or dir directory entry).

inductive FsEntry where
  | file (bytes : List (BitVec 8))
  | dir
  deriving DecidableEq, Repr, Inhabited, BEq

inductive FdAccessModeL261–266 ↗#

File-descriptor access mode (O_RDONLY, O_WRONLY, O_RDWR).

inductive FdAccessMode where
  | rdonly
  | wronly
  | rdwr
  deriving DecidableEq, Repr, Inhabited, BEq

namespace FdAccessMode

def canReadL270–273 ↗#

True when the open file description permits reading (O_RDONLY or O_RDWR).

def canRead : FdAccessMode → Bool
  | .rdonly | .rdwr => true
  | .wronly => false

def canWriteL275–278 ↗#

True when the open file description permits writing (O_WRONLY or O_RDWR).

def canWrite : FdAccessMode → Bool
  | .wronly | .rdwr => true
  | .rdonly => false

end FdAccessMode

inductive FdKindL282–296 ↗#

Descriptor backend tag for entries in FsState.fds:

localFile: regular file backed by FsState.files.
localDir: read-only directory descriptor (O_RDONLY, S_IFDIR | 0755) backed by FsState.files (fstat returns encodeLinuxStat .dir, read returns -EISDIR, write returns -EBADF, close returns 0, and pread64/lseek fail closed).
stdio: standard stream (stdin / stdout / stderr), stored out of band from the working-directory file namespace (FsState.entries) in FsState.stdin / State.trace.
custom (tag : Nat): extension slot for future loopback socket / pipe / peer-oracle backends sharing FsState.fds without changing any FdEntry field or invalidating file-descriptor proofs.

inductive FdKind where
  | localFile
  | localDir
  | stdio
  | custom (tag : Nat)
  deriving DecidableEq, Repr, Inhabited, BEq

def MAX_LFS_FILESIZEL298–300 ↗#

Linux 64-bit MAX_LFS_FILESIZE (include/linux/fs.h, LLONG_MAX = 2 ^ 63 - 1): maximum file size and byte offset (loff_t) representable in a signed 64-bit file offset.

def MAX_LFS_FILESIZE : Nat := 2 ^ 63 - 1

abbrev FsPathL302–303 ↗#

Canonical relative path in the working-directory file-system model ([] = ".").

abbrev FsPath := List String

def splitSlashL305–313 ↗#

Split s on '/' into raw path segments using pure List Char recursion so path normalization reduces directly in the Lean kernel (rfl / decide +kernel) across module boundaries.

def splitSlash (s : String) : List String :=
  let rec go (cur : List Char) : List Char → List String
    | [] => [String.ofList cur.reverse]
    | '/' :: cs => String.ofList cur.reverse :: go [] cs
    | c :: cs => go (c :: cur) cs
  go [] s.toList

def hasLeadingSlashL315–317 ↗#

True when path begins with '/'.

def hasLeadingSlash (path : String) : Bool :=
  path.toList.head? == some '/'

def hasDotDotL319–321 ↗#

True when path contains a ".." path segment.

def hasDotDot (path : String) : Bool :=
  (splitSlash path).contains ".."

def normalizePathL323–327 ↗#

Normalize a relative POSIX pathname into its canonical non-empty, non-"." path segments (normalizePath "./coins" = ["coins"], normalizePath ".//a/./b/" = ["a", "b"], normalizePath "." = [], normalizePath "./" = []).

def normalizePath (path : String) : FsPath :=
  (splitSlash path).filter fun seg => !seg.isEmpty && seg != "."

def FsPath.nonEmptyPrefixesL329–333 ↗#

Non-empty path prefixes of segs in top-down order (FsPath.nonEmptyPrefixes ["a", "b", "c"] = [["a"], ["a", "b"], ["a", "b", "c"]]).

def FsPath.nonEmptyPrefixes : FsPath → List FsPath
  | [] => []
  | s :: rest => [s] :: (nonEmptyPrefixes rest).map (s :: ·)

def joinSlashCharsL335–339 ↗#

Join List (List Char) segments with '/' using pure List Char recursion.

def joinSlashChars : List (List Char) → List Char
  | [] => []
  | [s] => s
  | s :: rest => s ++ ('/' :: joinSlashChars rest)

def FsPath.toPathStringL341–344 ↗#

Canonical String form of p : FsPath ([] ↦ ".", ["a", "b"] ↦ "a/b").

def FsPath.toPathString : FsPath → String
  | [] => "."
  | segs => String.ofList (joinSlashChars (segs.map String.toList))

structure FdEntryL346–355 ↗#

Open file description entry in the process file-descriptor table (regular files, read-only directories, and standard streams).

structure FdEntry where
  path    : String
  accMode : FdAccessMode
  append  : Bool := false
  cloexec : Bool := false
  offset  : Nat  := 0
  kind    : FdKind := .localFile
  deriving DecidableEq, Repr, Inhabited, BEq

structure FsStateL357–364 ↗#

Process working-directory file-system tree (entries, keyed by canonical FsPath relative to AT_FDCWD, with [] denoting "."), out-of-band standard input stream bytes (stdin), and open file-descriptor table (fd ∈ [3, 1024) plus standard streams 0, 1, 2).

structure FsState where
  entries : FsPath → Option FsEntry := fun p => if p.isEmpty then some .dir else none
  stdin   : List (BitVec 8) := []
  fds     : BitVec 64 → Option FdEntry := fun _ => none
  deriving Inhabited

namespace FsState

def maxOpenFdsL368–369 ↗#

Maximum open file descriptor number + 1 (RLIMIT_NOFILE = 1024).

def maxOpenFds : Nat := 1024

def getEntryL371–373 ↗#

Look up canonical relative path p in fs, treating CWD ([]) as always .dir.

def getEntry (fs : FsState) (p : FsPath) : Option FsEntry :=
  if p.isEmpty then some .dir else fs.entries p

def setEntryL375–377 ↗#

Update canonical relative path p in fs.entries.

def setEntry (fs : FsState) (p : FsPath) (e : Option FsEntry) : FsState :=
  { fs with entries := fun q => if q == p then e else fs.entries q }

def filesL379–381 ↗#

Look up path in fs under its canonical normalizePath key.

def files (fs : FsState) (path : String) : Option FsEntry :=
  fs.getEntry (normalizePath path)

def setFileL383–385 ↗#

Update path in fs under its canonical normalizePath key ((fs.setFile "./f" v).files "f" = v by rfl).

def setFile (fs : FsState) (path : String) (e : Option FsEntry) : FsState :=
  fs.setEntry (normalizePath path) e

def fdBytesL387–393 ↗#

Byte sequence backing an open .localFile or .stdio descriptor (fs.stdin for .stdio, fs.files desc.path regular-file bytes for .localFile, [] otherwise).

def fdBytes (fs : FsState) (desc : FdEntry) : List (BitVec 8) :=
  match desc.kind with
  | .stdio => fs.stdin
  | .localFile => match fs.files desc.path with | some (.file bs) => bs | _ => []
  | .localDir | .custom _ => []

def setFdL395–397 ↗#

Update descriptor fd in fs.fds.

def setFd (fs : FsState) (fd : BitVec 64) (e : Option FdEntry) : FsState :=
  { fs with fds := fun k => if k == fd then e else fs.fds k }

def allocFdL399–402 ↗#

Allocate the lowest unused file descriptor fd ∈ [3, maxOpenFds).

def allocFd (fs : FsState) : Option (BitVec 64) :=
  ((List.range (maxOpenFds - 3)).find? fun i =>
    fs.fds (BitVec.ofNat 64 (i + 3)) == none).map fun i => BitVec.ofNat 64 (i + 3)

end FsState

def fpsrMaskL406–410 ↗#

Modeled FPSR mask (0x0800009f): cumulative IEEE 754 exception flags IOC (bit 0), DZC (bit 1), OFC (bit 2), UFC (bit 3), IXC (bit 4), IDC (bit 7), and cumulative SIMD saturation flag QC (bit 27). All other bits ([6:5], [26:8], and AArch32-only NZCV [31:28]) are RES0.

def fpsrMask : BitVec 32 := 0x0800009f#32

def fpsrIOCL412–413 ↗#

FPSR.IOC (bit 0): Invalid Operation cumulative exception flag.

def fpsrIOC : BitVec 32 := 0x00000001#32

def fpsrDZCL415–416 ↗#

FPSR.DZC (bit 1): Divide by Zero cumulative exception flag.

def fpsrDZC : BitVec 32 := 0x00000002#32

def fpsrOFCL418–419 ↗#

FPSR.OFC (bit 2): Overflow cumulative exception flag.

def fpsrOFC : BitVec 32 := 0x00000004#32

def fpsrUFCL421–422 ↗#

FPSR.UFC (bit 3): Underflow cumulative exception flag.

def fpsrUFC : BitVec 32 := 0x00000008#32

def fpsrIXCL424–425 ↗#

FPSR.IXC (bit 4): Inexact cumulative exception flag.

def fpsrIXC : BitVec 32 := 0x00000010#32

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

Arm64.fpsrIDC

def fpsrQCL430–431 ↗#

FPSR.QC (bit 27): Cumulative SIMD saturation flag.

def fpsrQC : BitVec 32 := 0x08000000#32

structure SigActionL433–444 ↗#

Per-signal 32-byte kernel disposition entry (struct k_sigaction on AArch64 Linux, include/linux/signal_types.h and arch/arm64/include/uapi/asm/signal.h): handler (0 = SIG_DFL, 1 = SIG_IGN, or a recorded user-space handler address for synchronous fault signals SIGSEGV / SIGBUS), flags, restorer, and 64-bit mask. Signal dispositions are recorded and returned by rt_sigaction; asynchronous signal delivery is not modeled, and hardware faults terminate fail-closed with .Exception.

structure SigAction where
  handler  : BitVec 64 := 0#64
  flags    : BitVec 64 := 0#64
  restorer : BitVec 64 := 0#64
  mask     : BitVec 64 := 0#64
  deriving DecidableEq, Repr, Inhabited, BEq

structure SigAltStackL446–458 ↗#

Per-thread alternate signal stack configuration (current->sas_ss_sp, current->sas_ss_size, current->sas_ss_flags in include/linux/sched.h, include/linux/sched/signal.h:571-615, and kernel/signal.c:4458): sp (0 when disabled), size (0 when disabled, reporting SS_DISABLE = 2), and the raw stored ssFlags word (sas_ss_flags, written verbatim by do_sigaltstack in kernel/signal.c:4508; its SS_AUTODISARM = 1 << 31 bit suppresses on_sig_stack). Alternate-stack settings are recorded and returned by sigaltstack; signal delivery is not modeled.

@[ext]
structure SigAltStack where
  sp      : BitVec 64 := 0#64
  size    : BitVec 64 := 0#64
  ssFlags : BitVec 32 := 0#32
  deriving DecidableEq, Repr, Inhabited, BEq

structure StateL460–517 ↗#

Complete AArch64 architectural machine state, plus the process state this model keeps for Linux syscalls and hardware nondeterminism (brkStart, brk, fs, oracle, oracleIdx, exclFails, trace, status, sigActions, sigAltStack).

@[ext]
structure State where
  regs      : RegFile := RegFile.empty
  vregs     : VRegFile := VRegFile.empty
  sp        : BitVec 64 := 0#64
  pc        : BitVec 64 := 0#64
  pstate    : PState := PState.zero
  mem       : Memory := Memory.empty
  tpidrEl0  : BitVec 64 := 0#64
  /-- Floating-point status register (`FPSR`), storing sticky IEEE 754 exception flags
      (`IOC`, `DZC`, `OFC`, `UFC`, `IXC`, `IDC`) and cumulative SIMD saturation (`QC`). -/
  fpsr      : BitVec 32 := 0#32
  /-- Initial program break (`mm->start_brk`), fixed at load or snapshot time.
      Execution (`Step`) never modifies `brkStart`. -/
  brkStart  : BitVec 64 := 0#64
  brk       : BitVec 64 := 0#64
  /-- Cooperative local-disk file system and open file-descriptor table. -/
  fs        : FsState := {}
  /-- Results of nondeterministic syscalls. Execution never modifies it. -/
  oracle    : Oracle := {}
  /-- Number of `oracle` queries so far, i.e. the index of the next query. -/
  oracleIdx : Nat := 0
  /-- Remaining schedule of spurious store-exclusive (`STXR*`/`STLXR*`/`STXP`/`STLXP`) failures.
      Every execution has finitely many spurious failures, adversarially placed: each
      non-faulting store-exclusive consumes the head (`headD false`), failing (`Ws := 1`,
      memory unchanged) on `true` and succeeding (`Ws := 0`, performing the store) on `false`
      or once `exclFails` is empty. This models eventual LL/SC progress without an exclusive
      monitor; a retry-less `stxr` is unprovable because `exclFails = [true]` is a valid
      initial state. -/
  exclFails : List Bool := []
  trace     : List TraceEvent := []
  status    : ExecStatus := .Running
  /-- Per-object symbol address table: `symtab obj name` is the runtime address of
      symbol `name` in object `obj` (`none` if absent or non-unique). For extern stubs
      and extern data (not owned by any loaded object), pass `""` as `obj` (or any name
      not matching a loaded object).
      Execution (`Step`) never modifies `symtab`. -/
  symtab      : String → String → Option (BitVec 64) := fun _ _ => none
  /-- Per-signal recorded kernel `k_sigaction` table (`1..64`), initialized to `SIG_DFL` (`0`)
      with zero flags, restorer, and mask (`exec_init_sighand` / `flush_signal_handlers` in
      `kernel/signal.c` for default dispositions). -/
  sigActions  : BitVec 32 → SigAction := fun _ => {}
  /-- Per-thread alternate signal stack configuration, initialized to `{}` (`sp = 0`, `size = 0`,
      raw `ssFlags = 0`, reporting `ss_flags = SS_DISABLE = 2` per `sas_ss_flags` in
      `include/linux/sched/signal.h:602-608`; see `E1` in `Arm64/Trusted/Process/Assumptions.lean`
      for why the raw flags are `0` rather than the `sas_ss_reset` value `SS_DISABLE`). -/
  sigAltStack : SigAltStack := {}
  /-- Remaining dynamic physical `Perm.rw` byte budget (`mm/mmap.c` `accountable_mapping` /
      `__vm_enough_memory`). Initialized from `inputs.init.physMemAvail` in `ElfImage.loadState`
      after ELF `PT_LOAD` segments and the initial stack are mapped; pure ISA steps and I/O
      syscalls leave `physMemAvail` unchanged, while VM syscalls (`brk`, `mmap`, `mprotect`,
      `munmap`, `mremap`) deduct newly mapped/promoted `Perm.rw` bytes and refund unmapped or
      `PROT_NONE`-demoted `Perm.rw` bytes. -/
  physMemAvail : Nat := 0
  deriving Inhabited

namespace State

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

Arm64.State.sym

def readVReg128L525–527 ↗#

Read a 128-bit SIMD/FP register (V0..V31 / Q0..Q31).

def readVReg128 (s : State) (idx : BitVec 5) : BitVec 128 :=
  s.vregs.read idx

def writeVReg128L529–531 ↗#

Write a 128-bit SIMD/FP register (V0..V31 / Q0..Q31).

def writeVReg128 (s : State) (idx : BitVec 5) (val : BitVec 128) : State :=
  { s with vregs := s.vregs.write idx val }

def readVReg64L533–535 ↗#

Read the low 64 bits (D0..D31) of SIMD/FP register idx.

def readVReg64 (s : State) (idx : BitVec 5) : BitVec 64 :=
  (s.readVReg128 idx).truncate 64

def writeVReg64L537–539 ↗#

Write a 64-bit value (D0..D31 or 64-bit vector v.8b/v.4h/v.2s/v.1d), zero-extending to 128 bits per AArch64 architecture.

def writeVReg64 (s : State) (idx : BitVec 5) (val : BitVec 64) : State :=
  s.writeVReg128 idx (val.zeroExtend 128)

def readVReg32L541–543 ↗#

Read the low 32 bits (S0..S31) of SIMD/FP register idx.

def readVReg32 (s : State) (idx : BitVec 5) : BitVec 32 :=
  (s.readVReg128 idx).truncate 32

def writeVReg32L545–547 ↗#

Write a 32-bit value (S0..S31), zero-extending to 128 bits per AArch64 architecture.

def writeVReg32 (s : State) (idx : BitVec 5) (val : BitVec 32) : State :=
  s.writeVReg128 idx (val.zeroExtend 128)

def readReg64L549–554 ↗#

Read a 64-bit register (X0..X30, SP, or XZR).

def readReg64 (s : State) (r : Reg) : BitVec 64 :=
  match r with
  | .gpr idx => if idx == 31#5 then 0#64 else s.regs.read idx
  | .sp      => s.sp
  | .xzr     => 0#64

def writeReg64L556–564 ↗#

Write a 64-bit register (X0..X30, SP, or XZR). Writes to XZR are ignored.

def writeReg64 (s : State) (r : Reg) (val : BitVec 64) : State :=
  { s with
    regs := match r with
      | .gpr idx => if idx == 31#5 then s.regs else s.regs.write idx val
      | _ => s.regs
    sp := match r with
      | .sp => val
      | _ => s.sp }

def readReg32L566–568 ↗#

Read the low 32 bits of a register (W0..W30, WSP, or WZR).

def readReg32 (s : State) (r : Reg) : BitVec 32 :=
  (s.readReg64 r).truncate 32

def writeReg32L570–572 ↗#

Write a 32-bit value to a register (W0..W30, WSP, or WZR), zero-extending to 64 bits per AArch64 architecture.

def writeReg32 (s : State) (r : Reg) (val : BitVec 32) : State :=
  s.writeReg64 r (val.zeroExtend 64)

def readRegL574–578 ↗#

Read register at width w (W32 zero-extended to 64 bits, or W64).

def readReg (s : State) (w : Width) (r : Reg) : BitVec 64 :=
  match w with
  | .W32 => (s.readReg32 r).zeroExtend 64
  | .W64 => s.readReg64 r

def writeRegL580–582 ↗#

Write register at width w (W32 truncates to 32 bits and zero-extends to 64 bits; W64 writes all 64 bits).

def writeReg (s : State) (w : Width) (r : Reg) (val : BitVec 64) : State :=
  s.writeReg64 r (match w with | .W32 => (val.truncate 32).zeroExtend 64 | .W64 => val)

def advancePCL584–586 ↗#

Advance PC by 4 bytes (s.pc + 4).

def advancePC (s : State) : State :=
  { s with pc := s.pc + 4#64 }

def setPCL588–590 ↗#

Set PC to newPC.

def setPC (s : State) (newPC : BitVec 64) : State :=
  { s with pc := newPC }

def setPStateL592–594 ↗#

Update PState flags.

def setPState (s : State) (ps : PState) : State :=
  { s with pstate := ps }

def setFpsrL596–598 ↗#

Set FPSR to fpsr.

def setFpsr (s : State) (fpsr : BitVec 32) : State :=
  { s with fpsr := fpsr }

def orFpsrL600–602 ↗#

Accumulate exception or saturation flags into FPSR (s.fpsr ||| flags).

def orFpsr (s : State) (flags : BitVec 32) : State :=
  { s with fpsr := s.fpsr ||| flags }

def setMemL604–606 ↗#

Update memory.

def setMem (s : State) (m : Memory) : State :=
  { s with mem := m }

def setStatusL608–610 ↗#

Update execution status.

def setStatus (s : State) (st : ExecStatus) : State :=
  { s with status := st }

def setBrkL612–614 ↗#

Update the program break (brk).

def setBrk (s : State) (newBrk : BitVec 64) : State :=
  { s with brk := newBrk }

def setPhysMemAvailL616–618 ↗#

Update the remaining dynamic physical Perm.rw byte budget (physMemAvail).

def setPhysMemAvail (s : State) (n : Nat) : State :=
  { s with physMemAvail := n }

def setFsL620–622 ↗#

Update the local file system and file-descriptor state (fs).

def setFs (s : State) (newFs : FsState) : State :=
  { s with fs := newFs }

def getSigActionL624–626 ↗#

Read the recorded kernel signal disposition for signal sig.

def getSigAction (s : State) (sig : BitVec 32) : SigAction :=
  s.sigActions sig

def setSigActionL628–630 ↗#

Update the recorded kernel signal disposition for signal sig.

def setSigAction (s : State) (sig : BitVec 32) (act : SigAction) : State :=
  { s with sigActions := fun k => if k == sig then act else s.sigActions k }

def setSigAltStackL632–634 ↗#

Update the recorded alternate signal stack (sigAltStack).

def setSigAltStack (s : State) (sas : SigAltStack) : State :=
  { s with sigAltStack := sas }

def nextOracleL636–638 ↗#

Consume one oracle query (increment oracleIdx).

def nextOracle (s : State) : State :=
  { s with oracleIdx := s.oracleIdx + 1 }

def exclWillFailL640–644 ↗#

Whether the next non-faulting store-exclusive (STXR*/STLXR*/STXP/STLXP) will spuriously fail (s.exclFails.headD false). Once the finite list s.exclFails is exhausted, store-exclusives succeed (false).

def exclWillFail (s : State) : Bool :=
  s.exclFails.headD false

def stepExclOracleL646–648 ↗#

Consume one store-exclusive failure decision (s.exclFails.tail).

def stepExclOracle (s : State) : State :=
  { s with exclFails := s.exclFails.tail }

def appendTraceL650–652 ↗#

Append byte-level events to the observable execution trace (s.trace ++ evs).

def appendTrace (s : State) (evs : List TraceEvent) : State :=
  { s with trace := s.trace ++ evs }

2 declarations not shown (lines 654–664): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.State.stdoutBytes, Arm64.State.stderrBytes

def spAlignedL673–685 ↗#

Architectural stack pointer alignment predicate (CheckSPAlignment() in ARMv8-A pseudocode): whenever SP is used as the base register of a memory access, SP must be 16-byte aligned (SP[3:0] == 0b0000).

Structured ASL: arm-asl-extract query CheckSPAlignment (shared_pseudocode.xml, see .agents/skills/review-arm64-asl/SKILL.md).

See the ARM Architecture Reference Manual (DDI 0487):

-- ARM Architecture Reference Manual (DDI 0487) HTML links for SP alignment:
-- - Section D1.4.10 ("Program Counter and stack pointer alignment", D1.4.10.2 "SP alignment checking"):
--   https://developer.arm.com/documentation/ddi0487/latest/-Part-D-The-AArch64-System-Level-Architecture/-Chapter-D1-The-AArch64-System-Level-Programmers--Model/-D1-4-Exceptions/-D1-4-10-Program-Counter-and-stack-pointer-alignment
-- - Section C6.1.3 ("Use of the stack pointer"):
--   https://developer.arm.com/documentation/ddi0487/latest/-Part-C-The-AArch64-Instruction-Set/-Chapter-C6-A64-Base-Instruction-Descriptions/-C6-1-About-the-A64-base-instructions/-C6-1-3-Use-of-the-stack-pointer
-- - Section J1.2.305 (`CheckSPAlignment` pseudocode):
--   https://developer.arm.com/documentation/ddi0487/latest/-Part-J-Architectural-Pseudocode/-Chapter-J1-A-profile-Architecture-Pseudocode/-J1-2-Pseudocode-for-AArch64-operation/-J1-2-305-CheckSPAlignment
@[inline] def spAligned (s : State) : Bool :=
  (s.sp &&& 0b1111#64) == 0#64

end State

end Arm64