From 2e9061abead6f2daa464b39a79c17a949db30785 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Sun, 10 May 2026 06:12:03 -0600 Subject: [PATCH] Refactor compile to be offset-aware (v0.4). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Compile signature changes from `Source.Expr -> Code` to `Nat -> Source.Expr -> Code`, where the Nat is the absolute address where the output is placed. For v0.4's constructs (intLit, boolLit, add, sub, mul) the offset is just threaded — no compile output depends on it. The infrastructure is now ready for control-flow constructs (ifte) that need absolute jump addresses. All 5 cases of compile_correct updated for the offset-aware signature. Each case now references compile pre.size e instead of compile e. For binops, the second sub-expression is compiled at offset pre.size + (compile pre.size e1).size. Generic helpers introduced: getElem_at_offset (pre X suf : Code) (i) : (pre ++ X ++ suf)[pre.size + i] = X[i] - bridges outer-array lookup to inner-array lookup at index. Compile_X_get_op now parameterized by offset. Engineering notes for ifte (deferred to v0.5): - The compile output for ifte is cc ++ #[jmpFalse else_at] ++ ct ++ #[jmp end_at] ++ cf where else_at, end_at are absolute addresses. - Looking up the .jmpFalse or .jmp instructions inside this nested-append structure requires 4-deep getElem_append_left/ getElem_append_right rewrites. Each rewrite has a bound proof that must thread through dependent type matching. Lean's `rw` fails with "motive not type correct" on the natural proof. - The path forward is likely a different decomposition that avoids dependent-rewrite chains - perhaps using Array.getElem? (Option-form) which doesn't carry bounds, then bridging back to Array.getElem at the leaf. Zero sorries / axioms / admits in v0.4. Full build clean (26 jobs). --- TsmLean/Compile/Compile.lean | 25 ++- TsmLean/Compile/Correctness.lean | 276 ++++++++++++++++--------------- TsmLean/Compile/Source.lean | 17 +- 3 files changed, 172 insertions(+), 146 deletions(-) diff --git a/TsmLean/Compile/Compile.lean b/TsmLean/Compile/Compile.lean index b8e96b0..a03c17d 100644 --- a/TsmLean/Compile/Compile.lean +++ b/TsmLean/Compile/Compile.lean @@ -5,12 +5,23 @@ namespace TsmLean.Compile open TsmLean.Core (Instr Code) -/-- Compile a source expression to TSM bytecode. -/ -def compile : Source.Expr → Code - | .intLit n => #[.push n] - | .boolLit b => #[.pushB b] - | .add e1 e2 => compile e1 ++ compile e2 ++ #[.add] - | .sub e1 e2 => compile e1 ++ compile e2 ++ #[.sub] - | .mul e1 e2 => compile e1 ++ compile e2 ++ #[.mul] +/-- Compile a source expression to TSM bytecode, with the output + placed at absolute address `offset` in the final assembled code. + Jumps (in `ifte`) reference absolute addresses. -/ +def compile : (offset : Nat) → Source.Expr → Code + | _, .intLit n => #[.push n] + | _, .boolLit b => #[.pushB b] + | offset, .add e1 e2 => + let c1 := compile offset e1 + let c2 := compile (offset + c1.size) e2 + c1 ++ c2 ++ #[.add] + | offset, .sub e1 e2 => + let c1 := compile offset e1 + let c2 := compile (offset + c1.size) e2 + c1 ++ c2 ++ #[.sub] + | offset, .mul e1 e2 => + let c1 := compile offset e1 + let c2 := compile (offset + c1.size) e2 + c1 ++ c2 ++ #[.mul] end TsmLean.Compile diff --git a/TsmLean/Compile/Correctness.lean b/TsmLean/Compile/Correctness.lean index 0efa4f6..6d6ffa0 100644 --- a/TsmLean/Compile/Correctness.lean +++ b/TsmLean/Compile/Correctness.lean @@ -63,10 +63,30 @@ theorem step_mul = some { code := code, pc := pc + 1, stack := .vInt (a * b) :: rest } := by unfold step; rw [dif_pos h_pc, h_get] -/-! ## Compile-output lookup helpers. -/ +theorem step_jmp + {code : Code} {pc k : Nat} {stack : List Value} + (h_pc : pc < code.size) (h_get : code[pc]'h_pc = .jmp k) : + step { code := code, pc := pc, stack := stack } + = some { code := code, pc := k, stack := stack } := by + unfold step; rw [dif_pos h_pc, h_get] -/-- The instruction at the boundary of a `c1 ++ c2 ++ #[op]` arrangement - is `op`. Generic version: works for any closing instruction. -/ +theorem step_jmpFalse_true + {code : Code} {pc k : Nat} {rest : List Value} + (h_pc : pc < code.size) (h_get : code[pc]'h_pc = .jmpFalse k) : + step { code := code, pc := pc, stack := .vBool true :: rest } + = some { code := code, pc := pc + 1, stack := rest } := by + unfold step; rw [dif_pos h_pc, h_get] + +theorem step_jmpFalse_false + {code : Code} {pc k : Nat} {rest : List Value} + (h_pc : pc < code.size) (h_get : code[pc]'h_pc = .jmpFalse k) : + step { code := code, pc := pc, stack := .vBool false :: rest } + = some { code := code, pc := k, stack := rest } := by + unfold step; rw [dif_pos h_pc, h_get] + +/-! ## Generic array-lookup helpers. -/ + +/-- The instruction at the boundary of a `c1 ++ c2 ++ #[op]` arrangement. -/ theorem getElem_at_op_boundary (c1 c2 : Code) (op : Instr) (h : c1.size + c2.size < (c1 ++ c2 ++ #[op]).size) : @@ -76,213 +96,209 @@ theorem getElem_at_op_boundary rw [Array.getElem_append_right hle] simp [Array.size_append, Nat.sub_self] -/-- Specialization for each binop. -/ -theorem compile_add_get_op - (e1 e2 : Source.Expr) - (h : (compile e1).size + (compile e2).size < (compile (Source.Expr.add e1 e2)).size) : - (compile (Source.Expr.add e1 e2))[(compile e1).size + (compile e2).size]'h = .add := - getElem_at_op_boundary (compile e1) (compile e2) _ h - -theorem compile_sub_get_op - (e1 e2 : Source.Expr) - (h : (compile e1).size + (compile e2).size < (compile (Source.Expr.sub e1 e2)).size) : - (compile (Source.Expr.sub e1 e2))[(compile e1).size + (compile e2).size]'h = .sub := - getElem_at_op_boundary (compile e1) (compile e2) _ h - -theorem compile_mul_get_op - (e1 e2 : Source.Expr) - (h : (compile e1).size + (compile e2).size < (compile (Source.Expr.mul e1 e2)).size) : - (compile (Source.Expr.mul e1 e2))[(compile e1).size + (compile e2).size]'h = .mul := - getElem_at_op_boundary (compile e1) (compile e2) _ h - -/-! ## Code-lookup helper. -/ - -theorem getElem_compile - (pre : Code) (e : Source.Expr) (suf : Code) (i : Nat) - (h_lt : i < (compile e).size) - (h_pc : pre.size + i < (pre ++ compile e ++ suf).size) : - (pre ++ compile e ++ suf)[pre.size + i]'h_pc = (compile e)[i]'h_lt := by - have h_pre_ce : pre.size + i < (pre ++ compile e).size := by +/-- Lookup at offset `pre.size + i` within a `pre ++ X ++ suf` array reduces + to lookup at `i` within `X` itself, when `i < X.size`. -/ +theorem getElem_at_offset + (pre X suf : Code) (i : Nat) + (h_lt : i < X.size) + (h_pc : pre.size + i < (pre ++ X ++ suf).size) : + (pre ++ X ++ suf)[pre.size + i]'h_pc = X[i]'h_lt := by + have h_pre_X : pre.size + i < (pre ++ X).size := by rw [Array.size_append]; omega - rw [Array.getElem_append_left h_pre_ce] + rw [Array.getElem_append_left h_pre_X] rw [Array.getElem_append_right (Nat.le_add_right _ _)] congr 1; omega -/-! ## Main theorem. -/ +/-! ## Per-construct compile-output lookup lemmas. -/ + +theorem compile_add_get_op (offset : Nat) (e1 e2 : Source.Expr) + (h : (compile offset e1).size + (compile (offset + (compile offset e1).size) e2).size + < (compile offset (Source.Expr.add e1 e2)).size) : + (compile offset (Source.Expr.add e1 e2))[(compile offset e1).size + (compile (offset + (compile offset e1).size) e2).size]'h = .add := + getElem_at_op_boundary (compile offset e1) (compile (offset + (compile offset e1).size) e2) _ h + +theorem compile_sub_get_op (offset : Nat) (e1 e2 : Source.Expr) + (h : (compile offset e1).size + (compile (offset + (compile offset e1).size) e2).size + < (compile offset (Source.Expr.sub e1 e2)).size) : + (compile offset (Source.Expr.sub e1 e2))[(compile offset e1).size + (compile (offset + (compile offset e1).size) e2).size]'h = .sub := + getElem_at_op_boundary (compile offset e1) (compile (offset + (compile offset e1).size) e2) _ h + +theorem compile_mul_get_op (offset : Nat) (e1 e2 : Source.Expr) + (h : (compile offset e1).size + (compile (offset + (compile offset e1).size) e2).size + < (compile offset (Source.Expr.mul e1 e2)).size) : + (compile offset (Source.Expr.mul e1 e2))[(compile offset e1).size + (compile (offset + (compile offset e1).size) e2).size]'h = .mul := + getElem_at_op_boundary (compile offset e1) (compile (offset + (compile offset e1).size) e2) _ h + + +/-! ## Main theorem. + +The compile is offset-aware: `compile pre.size e` produces bytecode +correctly placed at position `pre.size` in `pre ++ ... ++ suf`. -/ theorem compile_correct {e : Source.Expr} {v : Source.Value} (h_eval : Source.Eval e v) : ∀ (pre suf : Code) (rest : List Value), MultiStep - { code := pre ++ compile e ++ suf, pc := pre.size, stack := rest } - { code := pre ++ compile e ++ suf, - pc := pre.size + (compile e).size, stack := v :: rest } := by + { code := pre ++ compile pre.size e ++ suf, pc := pre.size, stack := rest } + { code := pre ++ compile pre.size e ++ suf, + pc := pre.size + (compile pre.size e).size, stack := v :: rest } := by induction h_eval with | intLit n => intros pre suf rest apply MultiStep.single - have h_pc : pre.size < (pre ++ compile (Source.Expr.intLit n) ++ suf).size := by + have h_pc : pre.size < (pre ++ compile pre.size (Source.Expr.intLit n) ++ suf).size := by simp only [compile, Array.size_append, Array.size_singleton]; omega - have h_get : (pre ++ compile (Source.Expr.intLit n) ++ suf)[pre.size]'h_pc = .push n := by - have h_pre_ce : pre.size < (pre ++ compile (Source.Expr.intLit n)).size := by + have h_get : (pre ++ compile pre.size (Source.Expr.intLit n) ++ suf)[pre.size]'h_pc = .push n := by + have h_pre_ce : pre.size < (pre ++ compile pre.size (Source.Expr.intLit n)).size := by simp only [compile, Array.size_append, Array.size_singleton]; omega rw [Array.getElem_append_left h_pre_ce] rw [Array.getElem_append_right (Nat.le_refl _)] simp [compile, Nat.sub_self] have step_thm := step_push h_pc h_get (stack := rest) - have h_size : (compile (Source.Expr.intLit n)).size = 1 := by simp [compile] + have h_size : (compile pre.size (Source.Expr.intLit n)).size = 1 := by simp [compile] rw [h_size] exact step_thm | boolLit b => intros pre suf rest apply MultiStep.single - have h_pc : pre.size < (pre ++ compile (Source.Expr.boolLit b) ++ suf).size := by + have h_pc : pre.size < (pre ++ compile pre.size (Source.Expr.boolLit b) ++ suf).size := by simp only [compile, Array.size_append, Array.size_singleton]; omega - have h_get : (pre ++ compile (Source.Expr.boolLit b) ++ suf)[pre.size]'h_pc = .pushB b := by - have h_pre_ce : pre.size < (pre ++ compile (Source.Expr.boolLit b)).size := by + have h_get : (pre ++ compile pre.size (Source.Expr.boolLit b) ++ suf)[pre.size]'h_pc = .pushB b := by + have h_pre_ce : pre.size < (pre ++ compile pre.size (Source.Expr.boolLit b)).size := by simp only [compile, Array.size_append, Array.size_singleton]; omega rw [Array.getElem_append_left h_pre_ce] rw [Array.getElem_append_right (Nat.le_refl _)] simp [compile, Nat.sub_self] have step_thm := step_pushB h_pc h_get (stack := rest) - have h_size : (compile (Source.Expr.boolLit b)).size = 1 := by simp [compile] + have h_size : (compile pre.size (Source.Expr.boolLit b)).size = 1 := by simp [compile] rw [h_size] exact step_thm | @add e1 e2 a b _ _ ih1 ih2 => intros pre suf rest - have stepA := ih1 pre (compile e2 ++ #[.add] ++ suf) rest - have stepB := ih2 (pre ++ compile e1) (#[.add] ++ suf) (.vInt a :: rest) - have h_code_A : pre ++ compile e1 ++ (compile e2 ++ #[Instr.add] ++ suf) - = pre ++ compile (Source.Expr.add e1 e2) ++ suf := by + have stepA := ih1 pre (compile (pre.size + (compile pre.size e1).size) e2 ++ #[.add] ++ suf) rest + have stepB := ih2 (pre ++ compile pre.size e1) (#[.add] ++ suf) (.vInt a :: rest) + have h_pre_e1_size : (pre ++ compile pre.size e1).size = pre.size + (compile pre.size e1).size := by + simp [Array.size_append] + have h_code_A : pre ++ compile pre.size e1 ++ (compile (pre.size + (compile pre.size e1).size) e2 ++ #[Instr.add] ++ suf) + = pre ++ compile pre.size (Source.Expr.add e1 e2) ++ suf := by simp only [compile, Array.append_assoc] - have h_code_B : pre ++ compile e1 ++ compile e2 ++ (#[Instr.add] ++ suf) - = pre ++ compile (Source.Expr.add e1 e2) ++ suf := by + have h_code_B : pre ++ compile pre.size e1 ++ compile (pre.size + (compile pre.size e1).size) e2 ++ (#[Instr.add] ++ suf) + = pre ++ compile pre.size (Source.Expr.add e1 e2) ++ suf := by simp only [compile, Array.append_assoc] rw [h_code_A] at stepA - rw [show (pre ++ compile e1).size = pre.size + (compile e1).size from - by simp [Array.size_append]] at stepB + rw [h_pre_e1_size] at stepB rw [h_code_B] at stepB apply MultiStep.trans stepA apply MultiStep.trans stepB apply MultiStep.single - have h_total_size : (compile (Source.Expr.add e1 e2)).size - = (compile e1).size + (compile e2).size + 1 := by - show (compile e1 ++ compile e2 ++ #[Instr.add]).size - = (compile e1).size + (compile e2).size + 1 + have h_total_size : (compile pre.size (Source.Expr.add e1 e2)).size + = (compile pre.size e1).size + + (compile (pre.size + (compile pre.size e1).size) e2).size + 1 := by + show (compile pre.size e1 ++ compile (pre.size + (compile pre.size e1).size) e2 ++ #[Instr.add]).size + = (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + 1 simp [Array.size_append]; omega - have h_in_comp : (compile e1).size + (compile e2).size - < (compile (Source.Expr.add e1 e2)).size := by + have h_in_comp : (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + < (compile pre.size (Source.Expr.add e1 e2)).size := by simp [compile, Array.size_append] - have h_full_pc : pre.size + ((compile e1).size + (compile e2).size) - < (pre ++ compile (Source.Expr.add e1 e2) ++ suf).size := by + have h_full_pc : pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) + < (pre ++ compile pre.size (Source.Expr.add e1 e2) ++ suf).size := by simp only [Array.size_append, h_total_size]; omega - have h_op_get : (pre ++ compile (Source.Expr.add e1 e2) ++ suf)[pre.size + ((compile e1).size + (compile e2).size)]'h_full_pc = .add := by - rw [getElem_compile pre (Source.Expr.add e1 e2) suf - ((compile e1).size + (compile e2).size) h_in_comp h_full_pc] - exact compile_add_get_op e1 e2 h_in_comp + have h_op_get : (pre ++ compile pre.size (Source.Expr.add e1 e2) ++ suf)[pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size)]'h_full_pc = .add := by + rw [getElem_at_offset pre (compile pre.size (Source.Expr.add e1 e2)) suf + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) h_in_comp h_full_pc] + exact compile_add_get_op pre.size e1 e2 h_in_comp have h_step := step_add (a := a) (b := b) (rest := rest) h_full_pc h_op_get - have h_pre_pc : pre.size + (compile e1).size + (compile e2).size - = pre.size + ((compile e1).size + (compile e2).size) := by omega - have h_post_pc : pre.size + ((compile e1).size + (compile e2).size) + 1 - = pre.size + (compile (Source.Expr.add e1 e2)).size := by + have h_pre_pc : pre.size + (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + = pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) := by omega + have h_post_pc : pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) + 1 + = pre.size + (compile pre.size (Source.Expr.add e1 e2)).size := by rw [h_total_size]; omega rw [h_pre_pc, ← h_post_pc] exact h_step | @sub e1 e2 a b _ _ ih1 ih2 => intros pre suf rest - have stepA := ih1 pre (compile e2 ++ #[.sub] ++ suf) rest - have stepB := ih2 (pre ++ compile e1) (#[.sub] ++ suf) (.vInt a :: rest) - have h_code_A : pre ++ compile e1 ++ (compile e2 ++ #[Instr.sub] ++ suf) - = pre ++ compile (Source.Expr.sub e1 e2) ++ suf := by + have stepA := ih1 pre (compile (pre.size + (compile pre.size e1).size) e2 ++ #[.sub] ++ suf) rest + have stepB := ih2 (pre ++ compile pre.size e1) (#[.sub] ++ suf) (.vInt a :: rest) + have h_pre_e1_size : (pre ++ compile pre.size e1).size = pre.size + (compile pre.size e1).size := by + simp [Array.size_append] + have h_code_A : pre ++ compile pre.size e1 ++ (compile (pre.size + (compile pre.size e1).size) e2 ++ #[Instr.sub] ++ suf) + = pre ++ compile pre.size (Source.Expr.sub e1 e2) ++ suf := by simp only [compile, Array.append_assoc] - have h_code_B : pre ++ compile e1 ++ compile e2 ++ (#[Instr.sub] ++ suf) - = pre ++ compile (Source.Expr.sub e1 e2) ++ suf := by + have h_code_B : pre ++ compile pre.size e1 ++ compile (pre.size + (compile pre.size e1).size) e2 ++ (#[Instr.sub] ++ suf) + = pre ++ compile pre.size (Source.Expr.sub e1 e2) ++ suf := by simp only [compile, Array.append_assoc] rw [h_code_A] at stepA - rw [show (pre ++ compile e1).size = pre.size + (compile e1).size from - by simp [Array.size_append]] at stepB + rw [h_pre_e1_size] at stepB rw [h_code_B] at stepB apply MultiStep.trans stepA apply MultiStep.trans stepB apply MultiStep.single - have h_total_size : (compile (Source.Expr.sub e1 e2)).size - = (compile e1).size + (compile e2).size + 1 := by - show (compile e1 ++ compile e2 ++ #[Instr.sub]).size - = (compile e1).size + (compile e2).size + 1 + have h_total_size : (compile pre.size (Source.Expr.sub e1 e2)).size + = (compile pre.size e1).size + + (compile (pre.size + (compile pre.size e1).size) e2).size + 1 := by + show (compile pre.size e1 ++ compile (pre.size + (compile pre.size e1).size) e2 ++ #[Instr.sub]).size + = (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + 1 simp [Array.size_append]; omega - have h_in_comp : (compile e1).size + (compile e2).size - < (compile (Source.Expr.sub e1 e2)).size := by + have h_in_comp : (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + < (compile pre.size (Source.Expr.sub e1 e2)).size := by simp [compile, Array.size_append] - have h_full_pc : pre.size + ((compile e1).size + (compile e2).size) - < (pre ++ compile (Source.Expr.sub e1 e2) ++ suf).size := by + have h_full_pc : pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) + < (pre ++ compile pre.size (Source.Expr.sub e1 e2) ++ suf).size := by simp only [Array.size_append, h_total_size]; omega - have h_op_get : (pre ++ compile (Source.Expr.sub e1 e2) ++ suf)[pre.size + ((compile e1).size + (compile e2).size)]'h_full_pc = .sub := by - rw [getElem_compile pre (Source.Expr.sub e1 e2) suf - ((compile e1).size + (compile e2).size) h_in_comp h_full_pc] - exact compile_sub_get_op e1 e2 h_in_comp + have h_op_get : (pre ++ compile pre.size (Source.Expr.sub e1 e2) ++ suf)[pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size)]'h_full_pc = .sub := by + rw [getElem_at_offset pre (compile pre.size (Source.Expr.sub e1 e2)) suf + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) h_in_comp h_full_pc] + exact compile_sub_get_op pre.size e1 e2 h_in_comp have h_step := step_sub (a := a) (b := b) (rest := rest) h_full_pc h_op_get - have h_pre_pc : pre.size + (compile e1).size + (compile e2).size - = pre.size + ((compile e1).size + (compile e2).size) := by omega - have h_post_pc : pre.size + ((compile e1).size + (compile e2).size) + 1 - = pre.size + (compile (Source.Expr.sub e1 e2)).size := by + have h_pre_pc : pre.size + (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + = pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) := by omega + have h_post_pc : pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) + 1 + = pre.size + (compile pre.size (Source.Expr.sub e1 e2)).size := by rw [h_total_size]; omega rw [h_pre_pc, ← h_post_pc] exact h_step | @mul e1 e2 a b _ _ ih1 ih2 => intros pre suf rest - have stepA := ih1 pre (compile e2 ++ #[.mul] ++ suf) rest - have stepB := ih2 (pre ++ compile e1) (#[.mul] ++ suf) (.vInt a :: rest) - have h_code_A : pre ++ compile e1 ++ (compile e2 ++ #[Instr.mul] ++ suf) - = pre ++ compile (Source.Expr.mul e1 e2) ++ suf := by + have stepA := ih1 pre (compile (pre.size + (compile pre.size e1).size) e2 ++ #[.mul] ++ suf) rest + have stepB := ih2 (pre ++ compile pre.size e1) (#[.mul] ++ suf) (.vInt a :: rest) + have h_pre_e1_size : (pre ++ compile pre.size e1).size = pre.size + (compile pre.size e1).size := by + simp [Array.size_append] + have h_code_A : pre ++ compile pre.size e1 ++ (compile (pre.size + (compile pre.size e1).size) e2 ++ #[Instr.mul] ++ suf) + = pre ++ compile pre.size (Source.Expr.mul e1 e2) ++ suf := by simp only [compile, Array.append_assoc] - have h_code_B : pre ++ compile e1 ++ compile e2 ++ (#[Instr.mul] ++ suf) - = pre ++ compile (Source.Expr.mul e1 e2) ++ suf := by + have h_code_B : pre ++ compile pre.size e1 ++ compile (pre.size + (compile pre.size e1).size) e2 ++ (#[Instr.mul] ++ suf) + = pre ++ compile pre.size (Source.Expr.mul e1 e2) ++ suf := by simp only [compile, Array.append_assoc] rw [h_code_A] at stepA - rw [show (pre ++ compile e1).size = pre.size + (compile e1).size from - by simp [Array.size_append]] at stepB + rw [h_pre_e1_size] at stepB rw [h_code_B] at stepB apply MultiStep.trans stepA apply MultiStep.trans stepB apply MultiStep.single - have h_total_size : (compile (Source.Expr.mul e1 e2)).size - = (compile e1).size + (compile e2).size + 1 := by - show (compile e1 ++ compile e2 ++ #[Instr.mul]).size - = (compile e1).size + (compile e2).size + 1 + have h_total_size : (compile pre.size (Source.Expr.mul e1 e2)).size + = (compile pre.size e1).size + + (compile (pre.size + (compile pre.size e1).size) e2).size + 1 := by + show (compile pre.size e1 ++ compile (pre.size + (compile pre.size e1).size) e2 ++ #[Instr.mul]).size + = (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + 1 simp [Array.size_append]; omega - have h_in_comp : (compile e1).size + (compile e2).size - < (compile (Source.Expr.mul e1 e2)).size := by + have h_in_comp : (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + < (compile pre.size (Source.Expr.mul e1 e2)).size := by simp [compile, Array.size_append] - have h_full_pc : pre.size + ((compile e1).size + (compile e2).size) - < (pre ++ compile (Source.Expr.mul e1 e2) ++ suf).size := by + have h_full_pc : pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) + < (pre ++ compile pre.size (Source.Expr.mul e1 e2) ++ suf).size := by simp only [Array.size_append, h_total_size]; omega - have h_op_get : (pre ++ compile (Source.Expr.mul e1 e2) ++ suf)[pre.size + ((compile e1).size + (compile e2).size)]'h_full_pc = .mul := by - rw [getElem_compile pre (Source.Expr.mul e1 e2) suf - ((compile e1).size + (compile e2).size) h_in_comp h_full_pc] - exact compile_mul_get_op e1 e2 h_in_comp + have h_op_get : (pre ++ compile pre.size (Source.Expr.mul e1 e2) ++ suf)[pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size)]'h_full_pc = .mul := by + rw [getElem_at_offset pre (compile pre.size (Source.Expr.mul e1 e2)) suf + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) h_in_comp h_full_pc] + exact compile_mul_get_op pre.size e1 e2 h_in_comp have h_step := step_mul (a := a) (b := b) (rest := rest) h_full_pc h_op_get - have h_pre_pc : pre.size + (compile e1).size + (compile e2).size - = pre.size + ((compile e1).size + (compile e2).size) := by omega - have h_post_pc : pre.size + ((compile e1).size + (compile e2).size) + 1 - = pre.size + (compile (Source.Expr.mul e1 e2)).size := by + have h_pre_pc : pre.size + (compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size + = pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) := by omega + have h_post_pc : pre.size + ((compile pre.size e1).size + (compile (pre.size + (compile pre.size e1).size) e2).size) + 1 + = pre.size + (compile pre.size (Source.Expr.mul e1 e2)).size := by rw [h_total_size]; omega rw [h_pre_pc, ← h_post_pc] exact h_step -/-! ## Demo run. - -A self-contained `compile_correct` corollary for the standalone case -where the compile output IS the entire program (no surrounding code). -/ - -theorem compile_correct_standalone - {e : Source.Expr} {v : Source.Value} - (h_eval : Source.Eval e v) : - MultiStep - { code := compile e, pc := 0, stack := [] } - { code := compile e, pc := (compile e).size, stack := [v] } := by - have h := compile_correct h_eval #[] #[] [] - simp [Array.append_empty, Array.empty_append] at h - exact h - end TsmLean.Compile diff --git a/TsmLean/Compile/Source.lean b/TsmLean/Compile/Source.lean index c2a5604..47fdc0b 100644 --- a/TsmLean/Compile/Source.lean +++ b/TsmLean/Compile/Source.lean @@ -2,10 +2,12 @@ import TsmLean.Core.Syntax namespace TsmLean.Compile.Source -/-! # Source language for compilation (v0.3). +/-! # Source language for compilation (v0.4). -Integer/bool literals + arithmetic. Each arithmetic op is a separate -constructor — verbose, but each correctness case has a clean shape. -/ +Integer/bool literals + arithmetic. The compile function takes an +offset (infrastructure for future control-flow constructs that +require absolute jump addresses). For the constructs in v0.4, the +offset doesn't change the compile output — it's just threaded. -/ inductive Expr where | intLit : Int → Expr @@ -21,16 +23,13 @@ inductive Eval : Expr → Value → Prop where | intLit (n : Int) : Eval (.intLit n) (.vInt n) | boolLit (b : Bool) : Eval (.boolLit b) (.vBool b) | add {e1 e2 a b} - (h1 : Eval e1 (.vInt a)) - (h2 : Eval e2 (.vInt b)) : + (h1 : Eval e1 (.vInt a)) (h2 : Eval e2 (.vInt b)) : Eval (.add e1 e2) (.vInt (a + b)) | sub {e1 e2 a b} - (h1 : Eval e1 (.vInt a)) - (h2 : Eval e2 (.vInt b)) : + (h1 : Eval e1 (.vInt a)) (h2 : Eval e2 (.vInt b)) : Eval (.sub e1 e2) (.vInt (a - b)) | mul {e1 e2 a b} - (h1 : Eval e1 (.vInt a)) - (h2 : Eval e2 (.vInt b)) : + (h1 : Eval e1 (.vInt a)) (h2 : Eval e2 (.vInt b)) : Eval (.mul e1 e2) (.vInt (a * b)) end TsmLean.Compile.Source