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

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

Time.lean🔗

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

Clock and Time Syscalls

Re-exports Arm64.Trusted.Syscalls.Kernel.Time (kernel/time/posix-timers.c: clock_gettime) and defines the POSIX clock syscall dispatch table Syscall.timeTable and handler Syscall.time.

@[expose] public section
namespace Arm64
namespace Syscall

def timeTableL29–39 ↗#

Dispatch table for POSIX clock queries (clock_gettime).

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

Arm64.Syscall.time

end Syscall
end Arm64