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

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

Misc.lean🔗

Tier 3 · arm64-semantics used by the symbolic proof 2 headline theorems depend on it 7 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.

Thread Identity and Affinity Syscalls

Trusted syscall dispatch bundle (Syscall.miscTable, Syscall.misc) re-exporting Kernel.Sys for single-thread set_tid_address, sched_getaffinity, getpid, and gettid.

@[expose] public section
namespace Arm64
namespace Syscall

def miscTableL28–42 ↗#

Dispatch table for single-thread identity and CPU-affinity syscalls (set_tid_address, sched_getaffinity, getpid, gettid).

def miscTable : List (BitVec 64 × (State → State)) := [(SYS_SET_TID_ADDRESS, execSetTidAddress), (SYS_SCHED_GETAFFINITY, execSchedGetaffinity), (SYS_GETPID, execGetpid), (SYS_GETTID, execGetpid)]
1 declaration not shown (lines 36–37): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.misc

end Syscall
end Arm64