# Theory Compiler2

theory Compiler2
imports Compiler
(* Author: Gerwin Klein *)

theory Compiler2
imports Compiler
begin

text {*
The preservation of the source code semantics is already shown in the
parent theory @{theory Compiler}. This here shows the second direction.
*}

section {* Compiler Correctness, Reverse Direction *}

subsection {* Definitions *}

text {* Execution in @{term n} steps for simpler induction *}
primrec
exec_n :: "instr list ⇒ config ⇒ nat ⇒ config ⇒ bool"
("_/ ⊢ (_ →^_/ _)" [65,0,1000,55] 55)
where
"P ⊢ c →^0 c' = (c'=c)" |
"P ⊢ c →^(Suc n) c'' = (∃c'. (P ⊢ c → c') ∧ P ⊢ c' →^n c'')"

text {* The possible successor PCs of an instruction at position @{term n} *}
text_raw{*\snip{isuccsdef}{0}{1}{% *}
definition isuccs :: "instr ⇒ int ⇒ int set" where
"isuccs i n = (case i of
JMP j ⇒ {n + 1 + j} |
JMPLESS j ⇒ {n + 1 + j, n + 1} |
JMPGE j ⇒ {n + 1 + j, n + 1} |
_ ⇒ {n +1})"
text_raw{*}%endsnip*}

text {* The possible successors PCs of an instruction list *}
definition succs :: "instr list ⇒ int ⇒ int set" where
"succs P n = {s. ∃i::int. 0 ≤ i ∧ i < size P ∧ s ∈ isuccs (P!!i) (n+i)}"

text {* Possible exit PCs of a program *}
definition exits :: "instr list ⇒ int set" where
"exits P = succs P 0 - {0..< size P}"

subsection {* Basic properties of @{term exec_n} *}

lemma exec_n_exec:
"P ⊢ c →^n c' ⟹ P ⊢ c →* c'"
by (induct n arbitrary: c) (auto intro: star.step)

lemma exec_0 [intro!]: "P ⊢ c →^0 c" by simp

lemma exec_Suc:
"⟦ P ⊢ c → c'; P ⊢ c' →^n c'' ⟧ ⟹ P ⊢ c →^(Suc n) c''"
by (fastforce simp del: split_paired_Ex)

lemma exec_exec_n:
"P ⊢ c →* c' ⟹ ∃n. P ⊢ c →^n c'"
by (induct rule: star.induct) (auto intro: exec_Suc)

lemma exec_eq_exec_n:
"(P ⊢ c →* c') = (∃n. P ⊢ c →^n c')"
by (blast intro: exec_exec_n exec_n_exec)

lemma exec_n_Nil [simp]:
"[] ⊢ c →^k c' = (c' = c ∧ k = 0)"
by (induct k) (auto simp: exec1_def)

lemma exec1_exec_n [intro!]:
"P ⊢ c → c' ⟹ P ⊢ c →^1 c'"
by (cases c') simp

subsection {* Concrete symbolic execution steps *}

lemma exec_n_step:
"n ≠ n' ⟹
P ⊢ (n,stk,s) →^k (n',stk',s') =
(∃c. P ⊢ (n,stk,s) → c ∧ P ⊢ c →^(k - 1) (n',stk',s') ∧ 0 < k)"
by (cases k) auto

lemma exec1_end:
"size P <= fst c ⟹ ¬ P ⊢ c → c'"
by (auto simp: exec1_def)

lemma exec_n_end:
"size P <= (n::int) ⟹
P ⊢ (n,s,stk) →^k (n',s',stk') = (n' = n ∧ stk'=stk ∧ s'=s ∧ k =0)"
by (cases k) (auto simp: exec1_end)

lemmas exec_n_simps = exec_n_step exec_n_end

subsection {* Basic properties of @{term succs} *}

lemma succs_simps [simp]:
"succs [ADD] n = {n + 1}"
"succs [LOADI v] n = {n + 1}"
"succs [LOAD x] n = {n + 1}"
"succs [STORE x] n = {n + 1}"
"succs [JMP i] n = {n + 1 + i}"
"succs [JMPGE i] n = {n + 1 + i, n + 1}"
"succs [JMPLESS i] n = {n + 1 + i, n + 1}"
by (auto simp: succs_def isuccs_def)

lemma succs_empty [iff]: "succs [] n = {}"

lemma succs_Cons:
"succs (x#xs) n = isuccs x n ∪ succs xs (1+n)" (is "_ = ?x ∪ ?xs")
proof
let ?isuccs = "λp P n i::int. 0 ≤ i ∧ i < size P ∧ p ∈ isuccs (P!!i) (n+i)"
{ fix p assume "p ∈ succs (x#xs) n"
then obtain i::int where isuccs: "?isuccs p (x#xs) n i"
unfolding succs_def by auto
have "p ∈ ?x ∪ ?xs"
proof cases
assume "i = 0" with isuccs show ?thesis by simp
next
assume "i ≠ 0"
with isuccs
have "?isuccs p xs (1+n) (i - 1)" by auto
hence "p ∈ ?xs" unfolding succs_def by blast
thus ?thesis ..
qed
}
thus "succs (x#xs) n ⊆ ?x ∪ ?xs" ..

{ fix p assume "p ∈ ?x ∨ p ∈ ?xs"
hence "p ∈ succs (x#xs) n"
proof
assume "p ∈ ?x" thus ?thesis by (fastforce simp: succs_def)
next
assume "p ∈ ?xs"
then obtain i where "?isuccs p xs (1+n) i"
unfolding succs_def by auto
hence "?isuccs p (x#xs) n (1+i)"
thus ?thesis unfolding succs_def by blast
qed
}
thus "?x ∪ ?xs ⊆ succs (x#xs) n" by blast
qed

lemma succs_iexec1:
assumes "c' = iexec (P!!i) (i,s,stk)" "0 ≤ i" "i < size P"
shows "fst c' ∈ succs P 0"
using assms by (auto simp: succs_def isuccs_def split: instr.split)

lemma succs_shift:
"(p - n ∈ succs P 0) = (p ∈ succs P n)"
by (fastforce simp: succs_def isuccs_def split: instr.split)

lemma inj_op_plus [simp]:
"inj (op + (i::int))"

lemma succs_set_shift [simp]:
"op + i ` succs xs 0 = succs xs i"
by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)

lemma succs_append [simp]:
"succs (xs @ ys) n = succs xs n ∪ succs ys (n + size xs)"
by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps)

lemma exits_append [simp]:
"exits (xs @ ys) = exits xs ∪ (op + (size xs)) ` exits ys -
{0..<size xs + size ys}"
by (auto simp: exits_def image_set_diff)

lemma exits_single:
"exits [x] = isuccs x 0 - {0}"
by (auto simp: exits_def succs_def)

lemma exits_Cons:
"exits (x # xs) = (isuccs x 0 - {0}) ∪ (op + 1) ` exits xs -
{0..<1 + size xs}"
using exits_append [of "[x]" xs]

lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def)

lemma exits_simps [simp]:
"exits [STORE x] = {1}"
"i ≠ -1 ⟹ exits [JMP i] = {1 + i}"
"i ≠ -1 ⟹ exits [JMPGE i] = {1 + i, 1}"
"i ≠ -1 ⟹ exits [JMPLESS i] = {1 + i, 1}"
by (auto simp: exits_def)

lemma acomp_succs [simp]:
"succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
by (induct a arbitrary: n) auto

lemma acomp_size:
"(1::int) ≤ size (acomp a)"
by (induct a) auto

lemma acomp_exits [simp]:
"exits (acomp a) = {size (acomp a)}"
by (auto simp: exits_def acomp_size)

lemma bcomp_succs:
"0 ≤ i ⟹
succs (bcomp b f i) n ⊆ {n .. n + size (bcomp b f i)}
∪ {n + i + size (bcomp b f i)}"
proof (induction b arbitrary: f i n)
case (And b1 b2)
from And.prems
show ?case
by (cases f)
(auto dest: And.IH(1) [THEN subsetD, rotated]
And.IH(2) [THEN subsetD, rotated])
qed auto

lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]

lemma bcomp_exits:
fixes i :: int
shows
"0 ≤ i ⟹
exits (bcomp b f i) ⊆ {size (bcomp b f i), i + size (bcomp b f i)}"
by (auto simp: exits_def)

lemma bcomp_exitsD [dest!]:
"p ∈ exits (bcomp b f i) ⟹ 0 ≤ i ⟹
p = size (bcomp b f i) ∨ p = i + size (bcomp b f i)"
using bcomp_exits by auto

lemma ccomp_succs:
"succs (ccomp c) n ⊆ {n..n + size (ccomp c)}"
proof (induction c arbitrary: n)
case SKIP thus ?case by simp
next
case Assign thus ?case by simp
next
case (Seq c1 c2)
from Seq.prems
show ?case
by (fastforce dest: Seq.IH [THEN subsetD])
next
case (If b c1 c2)
from If.prems
show ?case
by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
next
case (While b c)
from While.prems
show ?case by (auto dest!: While.IH [THEN subsetD])
qed

lemma ccomp_exits:
"exits (ccomp c) ⊆ {size (ccomp c)}"
using ccomp_succs [of c 0] by (auto simp: exits_def)

lemma ccomp_exitsD [dest!]:
"p ∈ exits (ccomp c) ⟹ p = size (ccomp c)"
using ccomp_exits by auto

subsection {* Splitting up machine executions *}

lemma exec1_split:
fixes i j :: int
shows
"P @ c @ P' ⊢ (size P + i, s) → (j,s') ⟹ 0 ≤ i ⟹ i < size c ⟹
c ⊢ (i,s) → (j - size P, s')"
by (auto split: instr.splits simp: exec1_def)

lemma exec_n_split:
fixes i j :: int
assumes "P @ c @ P' ⊢ (size P + i, s) →^n (j, s')"
"0 ≤ i" "i < size c"
"j ∉ {size P ..< size P + size c}"
shows "∃s'' (i'::int) k m.
c ⊢ (i, s) →^k (i', s'') ∧
i' ∈ exits c ∧
P @ c @ P' ⊢ (size P + i', s'') →^m (j, s') ∧
n = k + m"
using assms proof (induction n arbitrary: i j s)
case 0
thus ?case by simp
next
case (Suc n)
have i: "0 ≤ i" "i < size c" by fact+
from Suc.prems
have j: "¬ (size P ≤ j ∧ j < size P + size c)" by simp
from Suc.prems
obtain i0 s0 where
step: "P @ c @ P' ⊢ (size P + i, s) → (i0,s0)" and
rest: "P @ c @ P' ⊢ (i0,s0) →^n (j, s')"
by clarsimp

from step i
have c: "c ⊢ (i,s) → (i0 - size P, s0)" by (rule exec1_split)

have "i0 = size P + (i0 - size P) " by simp
then obtain j0::int where j0: "i0 = size P + j0"  ..

note split_paired_Ex [simp del]

{ assume "j0 ∈ {0 ..< size c}"
with j0 j rest c
have ?case
by (fastforce dest!: Suc.IH intro!: exec_Suc)
} moreover {
assume "j0 ∉ {0 ..< size c}"
moreover
from c j0 have "j0 ∈ succs c 0"
by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
ultimately
have "j0 ∈ exits c" by (simp add: exits_def)
with c j0 rest
have ?case by fastforce
}
ultimately
show ?case by cases
qed

lemma exec_n_drop_right:
fixes j :: int
assumes "c @ P' ⊢ (0, s) →^n (j, s')" "j ∉ {0..<size c}"
shows "∃s'' i' k m.
(if c = [] then s'' = s ∧ i' = 0 ∧ k = 0
else c ⊢ (0, s) →^k (i', s'') ∧
i' ∈ exits c) ∧
c @ P' ⊢ (i', s'') →^m (j, s') ∧
n = k + m"
using assms
by (cases "c = []")
(auto dest: exec_n_split [where P="[]", simplified])

text {*
Dropping the left context of a potentially incomplete execution of @{term c}.
*}

lemma exec1_drop_left:
fixes i n :: int
assumes "P1 @ P2 ⊢ (i, s, stk) → (n, s', stk')" and "size P1 ≤ i"
shows "P2 ⊢ (i - size P1, s, stk) → (n - size P1, s', stk')"
proof -
have "i = size P1 + (i - size P1)" by simp
then obtain i' :: int where "i = size P1 + i'" ..
moreover
have "n = size P1 + (n - size P1)" by simp
then obtain n' :: int where "n = size P1 + n'" ..
ultimately
show ?thesis using assms
by (clarsimp simp: exec1_def simp del: iexec.simps)
qed

lemma exec_n_drop_left:
fixes i n :: int
assumes "P @ P' ⊢ (i, s, stk) →^k (n, s', stk')"
"size P ≤ i" "exits P' ⊆ {0..}"
shows "P' ⊢ (i - size P, s, stk) →^k (n - size P, s', stk')"
using assms proof (induction k arbitrary: i s stk)
case 0 thus ?case by simp
next
case (Suc k)
from Suc.prems
obtain i' s'' stk'' where
step: "P @ P' ⊢ (i, s, stk) → (i', s'', stk'')" and
rest: "P @ P' ⊢ (i', s'', stk'') →^k (n, s', stk')"
by auto
from step `size P ≤ i`
have *: "P' ⊢ (i - size P, s, stk) → (i' - size P, s'', stk'')"
by (rule exec1_drop_left)
then have "i' - size P ∈ succs P' 0"
by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
with `exits P' ⊆ {0..}`
have "size P ≤ i'" by (auto simp: exits_def)
from rest this `exits P' ⊆ {0..}`
have "P' ⊢ (i' - size P, s'', stk'') →^k (n - size P, s', stk')"
by (rule Suc.IH)
with * show ?case by auto
qed

lemmas exec_n_drop_Cons =
exec_n_drop_left [where P="[instr]", simplified] for instr

definition
"closed P ⟷ exits P ⊆ {size P}"

lemma ccomp_closed [simp, intro!]: "closed (ccomp c)"
using ccomp_exits by (auto simp: closed_def)

lemma acomp_closed [simp, intro!]: "closed (acomp c)"

lemma exec_n_split_full:
fixes j :: int
assumes exec: "P @ P' ⊢ (0,s,stk) →^k (j, s', stk')"
assumes P: "size P ≤ j"
assumes closed: "closed P"
assumes exits: "exits P' ⊆ {0..}"
shows "∃k1 k2 s'' stk''. P ⊢ (0,s,stk) →^k1 (size P, s'', stk'') ∧
P' ⊢ (0,s'',stk'') →^k2 (j - size P, s', stk')"
proof (cases "P")
case Nil with exec
show ?thesis by fastforce
next
case Cons
hence "0 < size P" by simp
with exec P closed
obtain k1 k2 s'' stk'' where
1: "P ⊢ (0,s,stk) →^k1 (size P, s'', stk'')" and
2: "P @ P' ⊢ (size P,s'',stk'') →^k2 (j, s', stk')"
by (auto dest!: exec_n_split [where P="[]" and i=0, simplified]
simp: closed_def)
moreover
have "j = size P + (j - size P)" by simp
then obtain j0 :: int where "j = size P + j0" ..
ultimately
show ?thesis using exits
by (fastforce dest: exec_n_drop_left)
qed

subsection {* Correctness theorem *}

lemma acomp_neq_Nil [simp]:
"acomp a ≠ []"
by (induct a) auto

lemma acomp_exec_n [dest!]:
"acomp a ⊢ (0,s,stk) →^n (size (acomp a),s',stk') ⟹
s' = s ∧ stk' = aval a s#stk"
proof (induction a arbitrary: n s' stk stk')
case (Plus a1 a2)
let ?sz = "size (acomp a1) + (size (acomp a2) + 1)"
from Plus.prems
have "acomp a1 @ acomp a2 @ [ADD] ⊢ (0,s,stk) →^n (?sz, s', stk')"

then obtain n1 s1 stk1 n2 s2 stk2 n3 where
"acomp a1 ⊢ (0,s,stk) →^n1 (size (acomp a1), s1, stk1)"
"acomp a2 ⊢ (0,s1,stk1) →^n2 (size (acomp a2), s2, stk2)"
"[ADD] ⊢ (0,s2,stk2) →^n3 (1, s', stk')"
by (auto dest!: exec_n_split_full)

thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps exec1_def)
qed (auto simp: exec_n_simps exec1_def)

lemma bcomp_split:
fixes i j :: int
assumes "bcomp b f i @ P' ⊢ (0, s, stk) →^n (j, s', stk')"
"j ∉ {0..<size (bcomp b f i)}" "0 ≤ i"
shows "∃s'' stk'' (i'::int) k m.
bcomp b f i ⊢ (0, s, stk) →^k (i', s'', stk'') ∧
(i' = size (bcomp b f i) ∨ i' = i + size (bcomp b f i)) ∧
bcomp b f i @ P' ⊢ (i', s'', stk'') →^m (j, s', stk') ∧
n = k + m"
using assms by (cases "bcomp b f i = []") (fastforce dest!: exec_n_drop_right)+

lemma bcomp_exec_n [dest]:
fixes i j :: int
assumes "bcomp b f j ⊢ (0, s, stk) →^n (i, s', stk')"
"size (bcomp b f j) ≤ i" "0 ≤ j"
shows "i = size(bcomp b f j) + (if f = bval b s then j else 0) ∧
s' = s ∧ stk' = stk"
using assms proof (induction b arbitrary: f j i n s' stk')
case Bc thus ?case
by (simp split: if_split_asm add: exec_n_simps exec1_def)
next
case (Not b)
from Not.prems show ?case
by (fastforce dest!: Not.IH)
next
case (And b1 b2)

let ?b2 = "bcomp b2 f j"
let ?m  = "if f then size ?b2 else size ?b2 + j"
let ?b1 = "bcomp b1 False ?m"

have j: "size (bcomp (And b1 b2) f j) ≤ i" "0 ≤ j" by fact+

from And.prems
obtain s'' stk'' and i'::int and k m where
b1: "?b1 ⊢ (0, s, stk) →^k (i', s'', stk'')"
"i' = size ?b1 ∨ i' = ?m + size ?b1" and
b2: "?b2 ⊢ (i' - size ?b1, s'', stk'') →^m (i - size ?b1, s', stk')"
by (auto dest!: bcomp_split dest: exec_n_drop_left)
from b1 j
have "i' = size ?b1 + (if ¬bval b1 s then ?m else 0) ∧ s'' = s ∧ stk'' = stk"
by (auto dest!: And.IH)
with b2 j
show ?case
by (fastforce dest!: And.IH simp: exec_n_end split: if_split_asm)
next
case Less
thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def) (* takes time *)
qed

lemma ccomp_empty [elim!]:
"ccomp c = [] ⟹ (c,s) ⇒ s"
by (induct c) auto

declare assign_simp [simp]

lemma ccomp_exec_n:
"ccomp c ⊢ (0,s,stk) →^n (size(ccomp c),t,stk')
⟹ (c,s) ⇒ t ∧ stk'=stk"
proof (induction c arbitrary: s t stk stk' n)
case SKIP
thus ?case by auto
next
case (Assign x a)
thus ?case
by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps exec1_def)
next
case (Seq c1 c2)
thus ?case by (fastforce dest!: exec_n_split_full)
next
case (If b c1 c2)
note If.IH [dest!]

let ?if = "IF b THEN c1 ELSE c2"
let ?cs = "ccomp ?if"
let ?bcomp = "bcomp b False (size (ccomp c1) + 1)"

from `?cs ⊢ (0,s,stk) →^n (size ?cs,t,stk')`
obtain i' :: int and k m s'' stk'' where
cs: "?cs ⊢ (i',s'',stk'') →^m (size ?cs,t,stk')" and
"?bcomp ⊢ (0,s,stk) →^k (i', s'', stk'')"
"i' = size ?bcomp ∨ i' = size ?bcomp + size (ccomp c1) + 1"
by (auto dest!: bcomp_split)

hence i':
"s''=s" "stk'' = stk"
"i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)"
by auto

with cs have cs':
"ccomp c1@JMP (size (ccomp c2))#ccomp c2 ⊢
(if bval b s then 0 else size (ccomp c1)+1, s, stk) →^m
(1 + size (ccomp c1) + size (ccomp c2), t, stk')"
by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)

show ?case
proof (cases "bval b s")
case True with cs'
show ?thesis
by simp
(fastforce dest: exec_n_drop_right
split: if_split_asm
simp: exec_n_simps exec1_def)
next
case False with cs'
show ?thesis
by (auto dest!: exec_n_drop_Cons exec_n_drop_left
simp: exits_Cons isuccs_def)
qed
next
case (While b c)

from While.prems
show ?case
proof (induction n arbitrary: s rule: nat_less_induct)
case (1 n)

{ assume "¬ bval b s"
with "1.prems"
have ?case
by simp
(fastforce dest!: bcomp_exec_n bcomp_split simp: exec_n_simps)
} moreover {
assume b: "bval b s"
let ?c0 = "WHILE b DO c"
let ?cs = "ccomp ?c0"
let ?bs = "bcomp b False (size (ccomp c) + 1)"
let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]"

from "1.prems" b
obtain k where
cs: "?cs ⊢ (size ?bs, s, stk) →^k (size ?cs, t, stk')" and
k:  "k ≤ n"
by (fastforce dest!: bcomp_split)

have ?case
proof cases
assume "ccomp c = []"
with cs k
obtain m where
"?cs ⊢ (0,s,stk) →^m (size (ccomp ?c0), t, stk')"
"m < n"
by (auto simp: exec_n_step [where k=k] exec1_def)
with "1.IH"
show ?case by blast
next
assume "ccomp c ≠ []"
with cs
obtain m m' s'' stk'' where
c: "ccomp c ⊢ (0, s, stk) →^m' (size (ccomp c), s'', stk'')" and
rest: "?cs ⊢ (size ?bs + size (ccomp c), s'', stk'') →^m
(size ?cs, t, stk')" and
m: "k = m + m'"
by (auto dest: exec_n_split [where i=0, simplified])
from c
have "(c,s) ⇒ s''" and stk: "stk'' = stk"
by (auto dest!: While.IH)
moreover
from rest m k stk
obtain k' where
"?cs ⊢ (0, s'', stk) →^k' (size ?cs, t, stk')"
"k' < n"
by (auto simp: exec_n_step [where k=m] exec1_def)
with "1.IH"
have "(?c0, s'') ⇒ t ∧ stk' = stk" by blast
ultimately
show ?case using b by blast
qed
}
ultimately show ?case by cases
qed
qed

theorem ccomp_exec:
"ccomp c ⊢ (0,s,stk) →* (size(ccomp c),t,stk') ⟹ (c,s) ⇒ t"
by (auto dest: exec_exec_n ccomp_exec_n)

corollary ccomp_sound:
"ccomp c ⊢ (0,s,stk) →* (size(ccomp c),t,stk)  ⟷  (c,s) ⇒ t"
by (blast intro!: ccomp_exec ccomp_bigstep)

end