lightmode

Light Lean proofs about low-level machine behavior.

🚧 Status: under construction. 🚧

Right now, it models a couple instructions for AArch64 and x86_64, then proves a tiny specification (isZero) against those models.

What’s included

• A small Word64 spec (isZeroSpec)
• AArch64 model and proof for isZero
• x86_64 model and proof for isZero
• Simple tests that reuse a shared IsZeroImpl interface

Project layout

• Lightmode/IsZero.lean: spec and supporting lemmas
• Lightmode/AArch64/*: AArch64 core model + proof
• Lightmode/X86_64/*: x86_64 core model + proof
• Lightmode/Tests.lean: shared interface + proof-driven tests

Build

1. Install Lean 4:
   • https://leanprover-community.github.io/get_started.html
2. Build the project:

   lake build

Scope and non-goals

• This is not a full ISA model.
• This is not a verified compiler pipeline.

License

Apache-2.0. See LICENSE.