add the C ffi

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

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)

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
@@ -27,23 +28,20 @@ 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
   let mut addr := origin
   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 +61,103 @@ 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 =>
+      -- 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
+    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,32 +166,37 @@ 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
-  -- 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 =>
-        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
+  -- pending key buffer for MMIO
+  let pending_key ← IO.mkRef (none : Option UInt16)
+  -- 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
-      -- non-TRAP instruction: use pure execute_step
-      match Execution.execute_step reg mem with
-      | some (new_reg, new_mem) =>
-        reg := new_reg
-        mem := new_mem
-      | none =>
-        break
+        | none =>
+          break
+  finally
+    Terminal.disableRawMode

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,13 +22,27 @@ lake build LC3Correct
 
 ## Running
 
-Run an assembled LC3 program:
+Run any assembled LC3 object file (`.obj`):
+
+```
+.lake/build/bin/lc3-lean <path-to-program.obj>
+```
+
+For example, to play 2048:
 
 ```
 .lake/build/bin/lc3-lean programs/2048.obj
 ```
 
-**Note:** Input currently requires pressing Enter after each keystroke. Raw terminal mode is not yet implemented.
+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:** 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
 
@@ -42,7 +56,8 @@ 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
+- **`c/terminal.c`** — C FFI for raw terminal mode (POSIX `termios`/`select`)
 - **`programs/`** — LC3 object files (2048, Rogue)
 
 ## Contributions

c/terminal.c

@@ -0,0 +1,43 @@
+#include <lean/lean.h>
+#include <termios.h>
+#include <unistd.h>
+#include <sys/select.h>
+
+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));
+}

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