Code review

Stream: new members

[Stefan Weber]

Hey everyone,

A couple of days ago I started getting into lean and have done a few exercises of "mathematics in lean".
Since I lack background in the field, it would be really nice, if someone could give me a little code review on my first "project" I did over the last two days.
What I did was a tiny cpu simulation using a custom mini instruction set. I then have a simple loop and show the program halts.
Any feedback is welcome :-)

Link: https://github.com/wechselstrom/cpu_sim/blob/main/cpu_sim/cpu.lean

[Derek Rhodes]

I think you're probably looking for feedback more about the proof technique side of things. It's cool that you proved the program halted, but I'm wondering if you could pull parts of the proof into a monadic context. Using the state monad it's possible to write an assembly DSL, (maybe you've already done things like this),

def Run := StateM ExecutionState Unit

def run (inst: Instr) : Run := modify (exec_instr inst)

def dec := run Instr.Dec
def jumpIfZero (n: ℕ) := run (Instr.JumpIfZero n)
def jump (n: ℕ) := run (Instr.Jump n)
def halt := run Instr.Halt

def tiny_prog' : Run := do
  dec
  jumpIfZero 3
  jump 0
  halt

Maybe someone knows how to incorporate proof elements, to get something like:

def tiny_prog' : Run := do
  dec
  jumpIfZero 3
  jump 0

  -- proofs
  have : stack_not_smashed := by aesop
  have : memory_bounds_on_array_respected := by hackers

  halt