Quelle  Compiler2.thy   Sprache: Isabelle

(* Author: Gerwin Klein *)

section ‹Compiler Correctness, Reverse Direction›

theory Compiler2
imports Compiler
begin

text ‹
The preservation of the source code semantics is already shown in the 
parent theory ‹Compiler›. This here shows the second direction.
›

subsection ‹Definitions›

text ‹Execution in 🍋‹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 🍋‹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 🍋‹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 🍋‹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 = {}"
  by (simp add: succs_def)

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)"
  have "p \ ?x \ ?xs" if assm: "p \ succs (x#xs) n" for p
  proof -
    from assm obtain i::int where isuccs: "?isuccs p (x#xs) n i"
      unfolding succs_def by auto     
    show ?thesis
    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
  qed
  thus "succs (x#xs) n \ ?x \ ?xs" ..

  have "p \ succs (x#xs) n" if assm: "p \ ?x \ p \ ?xs" for p
  proof -
    from assm show ?thesis
    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)"
        by (simp add: algebra_simps)
      thus ?thesis unfolding succs_def by blast
    qed
  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 ((+) (i::int))"
  by (metis add_minus_cancel inj_on_inverseI)

lemma succs_set_shift [simp]:
  "(+) 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 \ ((+) (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}) \ ((+) 1) ` exits xs -
                     {0..<1 + size xs}"
  using exits_append [of "[x]" xs]
  by (simp add: exits_single)

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

lemma exits_simps [simp]:
  "exits [ADD] = {1}"
  "exits [LOADI v] = {1}"
  "exits [LOAD x] = {1}"
  "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_exits [simp]:
  "exits (acomp a) = {size (acomp a)}"
proof -
  have "Suc 0 \ length (acomp a)" 
    by (induct a) auto
  then show ?thesis
    by (auto simp add: exits_def)
qed

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]

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

lemma exec_n_drop_right:
  fixes j :: int
  assumes "c @ P' \ (0, s) \^n (j, s')" "j \ {0..
  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 🍋‹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)"
  by (simp add: closed_def)

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')" 
    by (simp add: algebra_simps)
      
  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.. "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)

    have ?case if assm: "\ bval b s"
    proof -
      from assm "1.prems"
      show ?case
        by simp (fastforce dest!: bcomp_split simp: exec_n_simps)
    qed
    moreover
    have ?case if b: "bval b s"
    proof -
      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)
      
      show ?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
    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