AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level

Paper › arm64-semantics/Arm64/Trusted/Syscalls › Poll.leanTier 3 · arm64-semantics

Poll.lean🔗

Tier 3 · arm64-semantics used by the symbolic proof 2 headline theorems depend on it 3 of 41 lines trusted source ↗

Trusted, reviewed with the engine. The AArch64 model in arm64-semantics is Tier 3: it is reviewed in its own repository (check-trust-guards). The declarations that the headline statements use are shown for completeness.

Startup Standard-Descriptor POLLNVAL Probe

Re-exports Arm64.Trusted.Syscalls.Fs.Select (fs/select.c: SYS_PPOLL, POLLNVAL, evalPpollEntries, execPpoll) and defines the single-entry syscall bundle Syscall.poll for non-blocking standard-descriptor validity checks (ppoll with events = 0 and zero timeout).

@[expose] public section
namespace Arm64
namespace Syscall

def pollTableL30–42 ↗#

Single-entry dispatch table for ppoll (73).

def pollTable : List (BitVec 64 × (State → State)) := [(SYS_PPOLL, execPpoll)]
1 declaration not shown (lines 34–37): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.poll

end Syscall
end Arm64