max/crosslang
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Extend compiler with bool literals + sub + mul (v0.3).

Browse source 
Source.Expr: intLit, boolLit, add, sub, mul.
Each new constructor follows the pattern from v0.2:
  - one Source constructor + one Eval rule
  - one compile arm
  - one step_X lemma (push, pushB, add, sub, mul) - one line each
  - one compile_X_get_op lemma, all delegating to a generic
    getElem_at_op_boundary helper that handles the c1++c2++[op] shape
  - one case in compile_correct (~50 lines, mostly mechanical)

The pattern is fully grooved: each new arithmetic op is now a copy-
paste of the add case with substituted constructor names. The
substantive proof work happened once (in v0.2 for add); subsequent
arithmetic ops add no new proof shapes.

Generic helpers introduced:
  getElem_at_op_boundary (c1 c2 : Code) (op : Instr) (h) :
    (c1 ++ c2 ++ #[op])[c1.size + c2.size]'h = op
  - applies to add/sub/mul interchangeably; specialized via
    one-line wrappers (compile_add_get_op etc.)

Zero sorries / axioms / admits. Full build: 26 jobs clean.
This commit is contained in:
Maximus Gorog 2026-05-10 06:01:44 -06:00
parent ec65229050
commit f9ed9ec4c7
3 changed files with 169 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
TsmLean/Compile/Compile.lean
View file

@ -8,6 +8,9 @@ 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]
end TsmLean.Compile

171
TsmLean/Compile/Correctness.lean
View file

@ -10,11 +10,7 @@ open TsmLean.Core
`Source.Eval e v ⟹ TSM.MultiStep (start of compile e) (end of compile e, with v on stack)`
The CompCert-flavored bridge: source-level evaluation and target-level
execution agree on the value produced. This is the substrate-projection
theorem at miniature scale — for v0.1 instantiated only on integer
literals; extending to compound expressions is mechanical and the
infrastructure (multi-step utilities, code-lookup helper, single-step
reduction lemmas) is already in place. -/
execution agree on the value produced. -/
/-! ## Multi-step utilities. -/
@ -39,6 +35,13 @@ theorem step_push
= some { code := code, pc := pc + 1, stack := .vInt n :: stack } := by
unfold step; rw [dif_pos h_pc, h_get]
theorem step_pushB
{code : Code} {pc : Nat} {stack : List Value} {b : Bool}
(h_pc : pc < code.size) (h_get : code[pc]'h_pc = .pushB b) :
step { code := code, pc := pc, stack := stack }
= some { code := code, pc := pc + 1, stack := .vBool b :: stack } := by
unfold step; rw [dif_pos h_pc, h_get]
theorem step_add
{code : Code} {pc : Nat} {a b : Int} {rest : List Value}
(h_pc : pc < code.size) (h_get : code[pc]'h_pc = .add) :
@ -46,25 +49,53 @@ theorem step_add
= some { code := code, pc := pc + 1, stack := .vInt (a + b) :: rest } := by
unfold step; rw [dif_pos h_pc, h_get]
theorem step_sub
{code : Code} {pc : Nat} {a b : Int} {rest : List Value}
(h_pc : pc < code.size) (h_get : code[pc]'h_pc = .sub) :
step { code := code, pc := pc, stack := .vInt b :: .vInt a :: rest }
= some { code := code, pc := pc + 1, stack := .vInt (a - b) :: rest } := by
unfold step; rw [dif_pos h_pc, h_get]
theorem step_mul
{code : Code} {pc : Nat} {a b : Int} {rest : List Value}
(h_pc : pc < code.size) (h_get : code[pc]'h_pc = .mul) :
step { code := code, pc := pc, stack := .vInt b :: .vInt a :: rest }
= 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. -/
/-- The instruction at the end of `compile (.add e1 e2)` (right after both
sub-compiled segments) is `.add`. -/
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 := by
show ((compile e1 ++ compile e2) ++ #[Instr.add])[(compile e1).size + (compile e2).size]'h = .add
have hle : (compile e1 ++ compile e2).size ≤ (compile e1).size + (compile e2).size :=
Nat.le_of_eq Array.size_append
/-- The instruction at the boundary of a `c1 ++ c2 ++ #[op]` arrangement
is `op`. Generic version: works for any closing instruction. -/
theorem getElem_at_op_boundary
(c1 c2 : Code) (op : Instr)
(h : c1.size + c2.size < (c1 ++ c2 ++ #[op]).size) :
(c1 ++ c2 ++ #[op])[c1.size + c2.size]'h = op := by
show ((c1 ++ c2) ++ #[op])[c1.size + c2.size]'h = op
have hle : (c1 ++ c2).size ≤ c1.size + c2.size := Nat.le_of_eq Array.size_append
rw [Array.getElem_append_right hle]
simp [Array.size_append, Nat.sub_self]
/-! ## Code-lookup helper.
/-- 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
Looking up an index `pre.size + i` in `pre ++ compile e ++ suf` reduces
to the corresponding index in `compile e` — used in the inductive case
when extending v0.1 to compound expressions. -/
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)
@ -103,13 +134,25 @@ theorem compile_correct
have h_size : (compile (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
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
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]
rw [h_size]
exact step_thm
| @add e1 e2 a b _ _ ih1 ih2 =>
intros pre suf rest
-- Step A: compile e1
have stepA := ih1 pre (compile e2 ++ #[.add] ++ suf) rest
-- Step B: compile e2 (with prefix extended)
have stepB := ih2 (pre ++ compile e1) (#[.add] ++ suf) (.vInt a :: rest)
-- Code rearrangements
have h_code_A : pre ++ compile e1 ++ (compile e2 ++ #[Instr.add] ++ suf)
= pre ++ compile (Source.Expr.add e1 e2) ++ suf := by
simp only [compile, Array.append_assoc]
@ -123,15 +166,11 @@ theorem compile_correct
apply MultiStep.trans stepA
apply MultiStep.trans stepB
apply MultiStep.single
-- Final .add step
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
simp [Array.size_append]; omega
have h_op_pc : pre.size + (compile e1).size + (compile e2).size
< (pre ++ compile (Source.Expr.add e1 e2) ++ suf).size := by
simp only [Array.size_append, h_total_size]; omega
have h_in_comp : (compile e1).size + (compile e2).size
< (compile (Source.Expr.add e1 e2)).size := by
simp [compile, Array.size_append]
@ -150,6 +189,86 @@ theorem compile_correct
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
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
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_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
simp [Array.size_append]; omega
have h_in_comp : (compile e1).size + (compile e2).size
< (compile (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
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_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
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
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
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_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
simp [Array.size_append]; omega
have h_in_comp : (compile e1).size + (compile e2).size
< (compile (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
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_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
rw [h_total_size]; omega
rw [h_pre_pc, ← h_post_pc]
exact h_step
/-! ## Demo run.
@ -163,7 +282,7 @@ theorem compile_correct_standalone
{ code := compile e, pc := 0, stack := [] }
{ code := compile e, pc := (compile e).size, stack := [v] } := by
have h := compile_correct h_eval #[] #[] []
simp [Array.size_empty, Array.append_empty, Array.empty_append] at h
simp [Array.append_empty, Array.empty_append] at h
exact h
end TsmLean.Compile

30
TsmLean/Compile/Source.lean
View file

@ -2,23 +2,35 @@ import TsmLean.Core.Syntax
namespace TsmLean.Compile.Source
/-! # Source language for compilation (v0.2).
/-! # Source language for compilation (v0.3).
Integer literals + addition. The minimal "tree of operations" that
exercises the compositional structure of the correctness proof. -/
Integer/bool literals + arithmetic. Each arithmetic op is a separate
constructor — verbose, but each correctness case has a clean shape. -/
inductive Expr where
| intLit : Int → Expr
| add : Expr → Expr → Expr
| intLit : Int → Expr
| boolLit : Bool → Expr
| add : Expr → Expr → Expr
| sub : Expr → Expr → Expr
| mul : Expr → Expr → Expr
deriving Repr, Inhabited
abbrev Value := TsmLean.Core.Value
inductive Eval : Expr → Value → Prop where
| intLit (n : Int) : Eval (.intLit n) (.vInt n)
| add {e1 e2 a b}
(h1 : Eval e1 (.vInt a))
(h2 : Eval e2 (.vInt b)) :
| 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)) :
Eval (.add e1 e2) (.vInt (a + b))
| sub {e1 e2 a 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)) :
Eval (.mul e1 e2) (.vInt (a * b))
end TsmLean.Compile.Source