diff --git a/TsmLean/Compile/Compile.lean b/TsmLean/Compile/Compile.lean
index fe3d36d..b8e96b0 100644
--- a/TsmLean/Compile/Compile.lean
+++ b/TsmLean/Compile/Compile.lean
@@ -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
diff --git a/TsmLean/Compile/Correctness.lean b/TsmLean/Compile/Correctness.lean
index 22ad1c9..0efa4f6 100644
--- a/TsmLean/Compile/Correctness.lean
+++ b/TsmLean/Compile/Correctness.lean
@@ -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
diff --git a/TsmLean/Compile/Source.lean b/TsmLean/Compile/Source.lean
index cb63650..c2a5604 100644
--- a/TsmLean/Compile/Source.lean
+++ b/TsmLean/Compile/Source.lean
@@ -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