diff --git a/Bytecode/Basic.lean b/Bytecode/Basic.lean
index d4fff5f..6e6db8f 100644
--- a/Bytecode/Basic.lean
+++ b/Bytecode/Basic.lean
@@ -52,6 +52,8 @@ def Ast.compile : Ast → M Unit
 | mul l r => M.op l.compile r.compile (·*·)
 | div l r => M.op l.compile r.compile (·/·)
 
+#eval (do Ast.compile (3/2 + 0.5); M.pop).run #[]
+
 def M.run (m : M Unit) : Option Rat :=
   OptionT.run (do m; pop) #[] |>.fst
 
@@ -70,7 +72,7 @@ theorem M.push_pop : (do push x; pop) = pure x := by
 --   id_map {a} x := by
 --     simp [Functor.map, OptionT.bind, OptionT.mk, StateT.instLawfulMonad]
 
-theorem Ast.compile_sound (ast : Ast)
+theorem Ast.compile_eq_push_interpret (ast : Ast)
     : ast.compile = M.push ast.interpret := by
   induction ast
   · rfl
@@ -78,3 +80,7 @@ theorem Ast.compile_sound (ast : Ast)
     simp only [M.op, compile, interpret, *]
     repeat rw [←bind_assoc, M.push_pop, pure_bind]
   )
+
+theorem Ast.compile_sound (ast : Ast)
+    : ast.compile.run = ast.interpret := by
+  simp [M.run, compile_eq_push_interpret, M.push_pop, pure, OptionT.pure, StateT.pure]
diff --git a/README.md b/README.md
index 9417fcb..7b9afa5 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,5 @@
-# bytecode
\ No newline at end of file
+# bytecode
+
+proof that an extremely basic bytecode compiler is sound
+
+(maybe todo: main)