Refactor compile to be offset-aware (v0.4).
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).
This commit is contained in:
Maximus Gorog
parent
f9ed9ec4c7
commit
2e9061abea
3 changed files with 172 additions and 146 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue