From 3be3cf686b2bcd9d3cdae612e19a400175399397 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 1 Apr 2026 13:10:27 +0200 Subject: [PATCH 1/3] implement MMIO for keyboard status/data registers --- Main.lean | 111 ++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 103 insertions(+), 8 deletions(-) diff --git a/Main.lean b/Main.lean index cf7edc5..b8d7e74 100644 --- a/Main.lean +++ b/Main.lean @@ -27,7 +27,7 @@ end aux def load_into_mem (file : ByteArray) (mem : Memory) : Option Memory := do -- Need at least 2 bytes for origin if file.size < 2 then none else - -- Get origin from first two bytes and swap endianness + -- Get origin from first two bytes (big-endian) let origin := UInt16.ofNat (file.get! 0).toNat <<< 8 ||| UInt16.ofNat (file.get! 1).toNat -- let mut memory := mem @@ -35,15 +35,12 @@ def load_into_mem (file : ByteArray) (mem : Memory) : Option Memory := do let mut idx := 2 -- Process two bytes at a time until end of file while idx + 1 < file.size do - -- Read two bytes and combine into a word let byte1 := file.get! idx let byte2 := file.get! (idx + 1) let word := UInt16.ofNat byte1.toNat <<< 8 ||| UInt16.ofNat byte2.toNat - -- Write the word to memory (already in correct endianness) memory := Memory.write memory addr word addr := addr + 1 idx := idx + 2 - -- some memory def load_file (file_path : String) (mem : Memory) : IO Memory := do @@ -63,6 +60,104 @@ def decode_trap (instr : UInt16) : Option Trap.Trapcodes := else if vector == 0x25 then some .TRAP_HALT else none +-- Memory-mapped I/O addresses +def KBSR : UInt16 := 0xFE00 -- keyboard status register +def KBDR : UInt16 := 0xFE02 -- keyboard data register + +-- IO-aware memory read: intercepts MMIO addresses +def mem_read_io (mem : Memory) (addr : UInt16) (pending_key : IO.Ref (Option UInt16)) : + IO (UInt16 × Memory) := do + if addr == KBSR then + -- Check if we have a pending key + match ← pending_key.get with + | some _ => + -- Key is available: set KBSR bit 15 + let mem := Memory.write mem KBSR 0x8000 + pure (0x8000, mem) + | none => + -- No key pending: block and read one from stdin + let handle ← IO.getStdin + let input ← handle.getLine + match input.toList with + | c :: _ => + let key := Trap.clear_high_bits (Trap.char_to_uint16 c) + pending_key.set (some key) + let mem := Memory.write mem KBSR 0x8000 + let mem := Memory.write mem KBDR key + pure (0x8000, mem) + | [] => + pure (0, mem) + else if addr == KBDR then + -- Read keyboard data and clear pending key + match ← pending_key.get with + | some key => + pending_key.set none + pure (key, mem) + | none => + pure (Memory.read mem addr, mem) + else + pure (Memory.read mem addr, mem) + +-- IO-aware execution step: handles MMIO for memory reads +-- We need to intercept memory reads that the instruction will perform. +-- For LDI/LD/LDR that might access MMIO addresses, we pre-populate memory. +def execute_step_io (reg : Registers.Register) (mem : Memory) + (pending_key : IO.Ref (Option UInt16)) : IO (Option (Registers.Register × Memory)) := do + let instr := Memory.read mem reg.pc + let reg := { reg with pc := reg.pc + 1 } + match Instructions.instr_to_op instr with + | none => pure none + | some opcode => + -- For instructions that read memory, check if the address is MMIO + match opcode with + | .OP_LDI => + -- LDI: DR = mem[mem[PC + offset]] + let offset := Execution.sign_extend (instr.land 0x1FF) 9 + let addr1 := reg.pc + offset + let addr2 := Memory.read mem addr1 -- the indirect address + -- Check if addr2 is MMIO + let (value, mem) ← mem_read_io mem addr2 pending_key + let dr := (instr >>> 9).land 0x7 + match Registers.write reg dr value with + | none => pure none + | some reg' => + let reg'' := Execution.set_condition_codes reg' value + pure (some (reg'', mem)) + | .OP_LD => + let offset := Execution.sign_extend (instr.land 0x1FF) 9 + let addr := reg.pc + offset + let (value, mem) ← mem_read_io mem addr pending_key + let dr := (instr >>> 9).land 0x7 + match Registers.write reg dr value with + | none => pure none + | some reg' => + let reg'' := Execution.set_condition_codes reg' value + pure (some (reg'', mem)) + | .OP_ST => + -- ST: mem[PC + offset] = SR — uses pure version but check for MMIO write to DSR + pure (Execution.op_st instr reg mem) + | .OP_STI => + -- STI might write to MMIO (display), handle with pure for now + pure (Execution.op_sti instr reg mem) + | _ => + -- All other instructions: use pure execute_step logic + -- Re-construct what execute_step does (without re-fetching/incrementing PC) + let result := match opcode with + | .OP_BR => Execution.op_br instr reg mem + | .OP_ADD => Execution.op_add instr reg mem + | .OP_JSR => Execution.op_jsr instr reg mem + | .OP_AND => Execution.op_and instr reg mem + | .OP_LDR => Execution.op_ldr instr reg mem + | .OP_STR => Execution.op_str instr reg mem + | .OP_RTI => Execution.op_rti instr reg mem + | .OP_NOT => Execution.op_not instr reg mem + | .OP_JMP => Execution.op_jmp instr reg mem + | .OP_RES => Execution.op_res instr reg mem + | .OP_LEA => Execution.op_lea instr reg mem + | .OP_TRAP => Execution.op_trap instr reg mem + | _ => none -- LD, LDI, ST, STI handled above + pure result + -- the main function def main (file_paths : List String) : IO Unit := do -- initialize register and memory @@ -71,15 +166,15 @@ def main (file_paths : List String) : IO Unit := do -- load the code into memory to execute let file_path := file_paths[0]! mem ← load_file file_path mem + -- pending key buffer for MMIO + let pending_key ← IO.mkRef (none : Option UInt16) -- execution loop while true do - -- fetch instruction and decode opcode let instr := Memory.read mem reg.pc let opcode := Instructions.instr_to_op instr -- intercept TRAP instructions for IO if opcode == some .OP_TRAP then let reg_stepped := { reg with pc := reg.pc + 1 } - -- save PC to R7 match Registers.write reg_stepped 7 reg_stepped.pc with | none => break | some reg_with_r7 => @@ -93,8 +188,8 @@ def main (file_paths : List String) : IO Unit := do mem := new_mem | none => break else - -- non-TRAP instruction: use pure execute_step - match Execution.execute_step reg mem with + -- IO-aware execution step (handles MMIO) + match ← execute_step_io reg mem pending_key with | some (new_reg, new_mem) => reg := new_reg mem := new_mem From 88baee5c5af41df69b7ee98f4cf20d4a76aa6d96 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 1 Apr 2026 13:14:57 +0200 Subject: [PATCH 2/3] update README with formal verification emphasis and usage instructions --- README.md | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 20c31ca..6ff3f79 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,8 @@ # LC3-Lean -A formally verified LC3 virtual machine in Lean 4, following the article [Write your Own Virtual Machine](https://www.jmeiners.com/lc3-vm/). +A **formally verified** LC3 virtual machine written in [Lean 4](https://lean-lang.org/), following the article [Write your Own Virtual Machine](https://www.jmeiners.com/lc3-vm/). -All 14 LC3 instruction opcodes are implemented and formally verified to match the [LC3 ISA specification](https://www.jmeiners.com/lc3-vm/supplies/lc3-isa.pdf) — zero `sorry` statements in the codebase. +All 14 LC3 instruction opcodes are implemented and **proven correct** against the [LC3 ISA specification](https://www.jmeiners.com/lc3-vm/supplies/lc3-isa.pdf) — zero `sorry` statements in the codebase. Each opcode has a formal theorem stating that the implementation matches the ISA-defined behavior. ## Building @@ -22,12 +22,26 @@ lake build LC3Correct ## Running -Run an assembled LC3 program: +Run any assembled LC3 object file (`.obj`): + +``` +.lake/build/bin/lc3-lean +``` + +For example, to play 2048: ``` .lake/build/bin/lc3-lean programs/2048.obj ``` +The VM supports: +- All 14 LC3 instructions (ADD, AND, NOT, BR, JMP, JSR, LD, LDI, LDR, LEA, ST, STI, STR, TRAP) +- I/O trap routines (GETC, OUT, PUTS, IN, PUTSP, HALT) +- Memory-mapped I/O (keyboard status/data registers at 0xFE00/0xFE02) +- Programs that use ANSI terminal escape codes + +Any `.obj` file assembled for the LC3 ISA should work. You can find LC3 programs to run [here](https://github.com/justinmeiners/lc3-vm) or assemble your own using an [LC3 assembler](https://github.com/chiragsakhuja/lc3tools). + **Note:** Input currently requires pressing Enter after each keystroke. Raw terminal mode is not yet implemented. ## Project Structure @@ -42,7 +56,7 @@ Run an assembled LC3 program: - `ExecutionCorrect.lean` — Correctness theorems for all 14 opcodes - `RegisterLemmas.lean` — Register read/write properties - `MemoryLemmas.lean` — Memory read/write properties -- **`Main.lean`** — Entry point, binary loader, execution loop with I/O trap dispatch +- **`Main.lean`** — Entry point, binary loader, execution loop with MMIO and I/O trap dispatch - **`programs/`** — LC3 object files (2048, Rogue) ## Contributions From f938a675c1e46a395694373970787a57c36c7261 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 1 Apr 2026 16:12:12 +0200 Subject: [PATCH 3/3] add c ffi --- LC3Lean/Terminal.lean | 19 ++++++++++++ LC3Lean/Trap.lean | 8 ++---- Main.lean | 67 +++++++++++++++++++++++-------------------- README.md | 3 +- c/terminal.c | 43 +++++++++++++++++++++++++++ lakefile.lean | 24 ++++++++++++++++ lakefile.toml | 14 --------- 7 files changed, 126 insertions(+), 52 deletions(-) create mode 100644 LC3Lean/Terminal.lean create mode 100644 c/terminal.c create mode 100644 lakefile.lean delete mode 100644 lakefile.toml diff --git a/LC3Lean/Terminal.lean b/LC3Lean/Terminal.lean new file mode 100644 index 0000000..1e8b330 --- /dev/null +++ b/LC3Lean/Terminal.lean @@ -0,0 +1,19 @@ +namespace Terminal + +@[extern "lc3_enable_raw_mode"] +opaque enableRawMode : IO Unit + +@[extern "lc3_disable_raw_mode"] +opaque disableRawMode : IO Unit + +@[extern "lc3_read_char"] +private opaque readCharCode : IO UInt32 + +@[extern "lc3_check_key"] +opaque checkKey : IO Bool + +def readChar : IO Char := do + let code ← readCharCode + pure (Char.ofNat code.toNat) + +end Terminal diff --git a/LC3Lean/Trap.lean b/LC3Lean/Trap.lean index 95637f2..9f99d83 100644 --- a/LC3Lean/Trap.lean +++ b/LC3Lean/Trap.lean @@ -1,5 +1,6 @@ import LC3Lean.Memory import LC3Lean.Registers +import LC3Lean.Terminal namespace Trap open Memory @@ -8,12 +9,7 @@ open Registers section aux - def get_char_from_terminal : IO Char := do - let handle ← IO.getStdin - let input ← handle.getLine -- read one 32-bit character - match input.toList with - | c :: _ => pure c -- Return the first character - | [] => throw $ IO.userError "Error: No input provided." + def get_char_from_terminal : IO Char := Terminal.readChar def char_to_uint16 (c : Char) : UInt16 := UInt16.ofNat (c.val.toNat) def uint16_to_char (u : UInt16) : Char := Char.ofNat (u.toNat) diff --git a/Main.lean b/Main.lean index b8d7e74..d188a17 100644 --- a/Main.lean +++ b/Main.lean @@ -4,6 +4,7 @@ import LC3Lean.Registers import LC3Lean.Instructions import LC3Lean.Execution import LC3Lean.Trap +import LC3Lean.Terminal open Memory open Trap @@ -75,17 +76,16 @@ def mem_read_io (mem : Memory) (addr : UInt16) (pending_key : IO.Ref (Option UIn let mem := Memory.write mem KBSR 0x8000 pure (0x8000, mem) | none => - -- No key pending: block and read one from stdin - let handle ← IO.getStdin - let input ← handle.getLine - match input.toList with - | c :: _ => + -- Non-blocking check for key input + let hasKey ← Terminal.checkKey + if hasKey then + let c ← Terminal.readChar let key := Trap.clear_high_bits (Trap.char_to_uint16 c) pending_key.set (some key) let mem := Memory.write mem KBSR 0x8000 let mem := Memory.write mem KBDR key pure (0x8000, mem) - | [] => + else pure (0, mem) else if addr == KBDR then -- Read keyboard data and clear pending key @@ -168,30 +168,35 @@ def main (file_paths : List String) : IO Unit := do mem ← load_file file_path mem -- pending key buffer for MMIO let pending_key ← IO.mkRef (none : Option UInt16) - -- execution loop - while true do - let instr := Memory.read mem reg.pc - let opcode := Instructions.instr_to_op instr - -- intercept TRAP instructions for IO - if opcode == some .OP_TRAP then - let reg_stepped := { reg with pc := reg.pc + 1 } - match Registers.write reg_stepped 7 reg_stepped.pc with - | none => break - | some reg_with_r7 => - match decode_trap instr with - | some .TRAP_HALT => - IO.println "HALT" - break - | some trapcode => - let (new_reg, new_mem) ← Trap.op_trap_io trapcode reg_with_r7 mem + -- enable raw terminal mode for character-at-a-time input + Terminal.enableRawMode + try + -- execution loop + while true do + let instr := Memory.read mem reg.pc + let opcode := Instructions.instr_to_op instr + -- intercept TRAP instructions for IO + if opcode == some .OP_TRAP then + let reg_stepped := { reg with pc := reg.pc + 1 } + match Registers.write reg_stepped 7 reg_stepped.pc with + | none => break + | some reg_with_r7 => + match decode_trap instr with + | some .TRAP_HALT => + IO.println "HALT" + break + | some trapcode => + let (new_reg, new_mem) ← Trap.op_trap_io trapcode reg_with_r7 mem + reg := new_reg + mem := new_mem + | none => break + else + -- IO-aware execution step (handles MMIO) + match ← execute_step_io reg mem pending_key with + | some (new_reg, new_mem) => reg := new_reg mem := new_mem - | none => break - else - -- IO-aware execution step (handles MMIO) - match ← execute_step_io reg mem pending_key with - | some (new_reg, new_mem) => - reg := new_reg - mem := new_mem - | none => - break + | none => + break + finally + Terminal.disableRawMode diff --git a/README.md b/README.md index 6ff3f79..4d7bfbb 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,7 @@ The VM supports: Any `.obj` file assembled for the LC3 ISA should work. You can find LC3 programs to run [here](https://github.com/justinmeiners/lc3-vm) or assemble your own using an [LC3 assembler](https://github.com/chiragsakhuja/lc3tools). -**Note:** Input currently requires pressing Enter after each keystroke. Raw terminal mode is not yet implemented. +**Note:** Raw terminal mode is provided via a small C FFI (see `c/terminal.c`), which enables character-at-a-time input and non-blocking keyboard polling on POSIX systems. All VM logic — instruction execution, memory, registers, trap routines, and formal proofs — is implemented entirely in Lean 4. The C code is solely for terminal I/O. ## Project Structure @@ -57,6 +57,7 @@ Any `.obj` file assembled for the LC3 ISA should work. You can find LC3 programs - `RegisterLemmas.lean` — Register read/write properties - `MemoryLemmas.lean` — Memory read/write properties - **`Main.lean`** — Entry point, binary loader, execution loop with MMIO and I/O trap dispatch +- **`c/terminal.c`** — C FFI for raw terminal mode (POSIX `termios`/`select`) - **`programs/`** — LC3 object files (2048, Rogue) ## Contributions diff --git a/c/terminal.c b/c/terminal.c new file mode 100644 index 0000000..36f27cf --- /dev/null +++ b/c/terminal.c @@ -0,0 +1,43 @@ +#include +#include +#include +#include + +static struct termios orig_termios; +static int raw_mode_enabled = 0; + +LEAN_EXPORT lean_obj_res lc3_enable_raw_mode(lean_obj_arg world) { + if (!raw_mode_enabled) { + tcgetattr(STDIN_FILENO, &orig_termios); + struct termios raw = orig_termios; + raw.c_lflag &= ~(ICANON | ECHO); + raw.c_cc[VMIN] = 1; + raw.c_cc[VTIME] = 0; + tcsetattr(STDIN_FILENO, TCSAFLUSH, &raw); + raw_mode_enabled = 1; + } + return lean_io_result_mk_ok(lean_box(0)); +} + +LEAN_EXPORT lean_obj_res lc3_disable_raw_mode(lean_obj_arg world) { + if (raw_mode_enabled) { + tcsetattr(STDIN_FILENO, TCSAFLUSH, &orig_termios); + raw_mode_enabled = 0; + } + return lean_io_result_mk_ok(lean_box(0)); +} + +LEAN_EXPORT lean_obj_res lc3_read_char(lean_obj_arg world) { + uint8_t c = 0; + read(STDIN_FILENO, &c, 1); + return lean_io_result_mk_ok(lean_box((size_t)c)); +} + +LEAN_EXPORT lean_obj_res lc3_check_key(lean_obj_arg world) { + fd_set readfds; + FD_ZERO(&readfds); + FD_SET(STDIN_FILENO, &readfds); + struct timeval timeout = {0, 0}; + int result = select(STDIN_FILENO + 1, &readfds, NULL, NULL, &timeout); + return lean_io_result_mk_ok(lean_box(result > 0 ? 1 : 0)); +} diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..0269468 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,24 @@ +import Lake +open Lake DSL + +package «LC3-Lean» where + version := v!"0.1.0" + +lean_lib «LC3Lean» where + +lean_lib «LC3Correct» where + roots := #[`LC3Correct.LC3Correct, `LC3Correct.ExecutionCorrect, + `LC3Correct.RegisterLemmas, `LC3Correct.MemoryLemmas] + +extern_lib «terminal» pkg := do + let name := nameToStaticLib "terminal" + let srcFile := pkg.dir / "c" / "terminal.c" + let oFile := pkg.buildDir / "c" / "terminal.o" + let srcJob ← inputTextFile srcFile + let incDir ← getLeanIncludeDir + let oJob ← buildO oFile srcJob #["-I", incDir.toString] #["-fPIC"] + buildStaticLib (pkg.staticLibDir / name) #[oJob] + +@[default_target] +lean_exe «lc3-lean» where + root := `Main diff --git a/lakefile.toml b/lakefile.toml deleted file mode 100644 index aa79bb6..0000000 --- a/lakefile.toml +++ /dev/null @@ -1,14 +0,0 @@ -name = "LC3-Lean" -version = "0.1.0" -defaultTargets = ["lc3-lean"] - -[[lean_lib]] -name = "LC3Lean" - -[[lean_lib]] -name = "LC3Correct" -roots = ["LC3Correct.LC3Correct", "LC3Correct.ExecutionCorrect", "LC3Correct.RegisterLemmas", "LC3Correct.MemoryLemmas"] - -[[lean_exe]] -name = "lc3-lean" -root = "Main"