Theory LBVSpec

(*  Title:      HOL/MicroJava/DFA/LBVSpec.thy
    Author:     Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹The Lightweight Bytecode Verifier›

theory LBVSpec
imports SemilatAlg Opt
begin

type_synonym 's certificate = "'s list"   

primrec merge :: "'s certificate  's binop  's ord  's  nat  (nat × 's) list  's  's" where
  "merge cert f r T pc []     x = x"
| "merge cert f r T pc (s#ss) x = merge cert f r T pc ss (let (pc',s') = s in 
                                  if pc'=pc+1 then s' +_f x
                                  else if s' <=_r (cert!pc') then x
                                  else T)"

definition wtl_inst :: "'s certificate  's binop  's ord  's 
             's step_type  nat  's  's" where
"wtl_inst cert f r T step pc s  merge cert f r T pc (step pc s) (cert!(pc+1))"

definition wtl_cert :: "'s certificate  's binop  's ord  's  's 
             's step_type  nat  's  's" where
"wtl_cert cert f r T B step pc s 
  if cert!pc = B then 
    wtl_inst cert f r T step pc s
  else
    if s <=_r (cert!pc) then wtl_inst cert f r T step pc (cert!pc) else T"

primrec wtl_inst_list :: "'a list  's certificate  's binop  's ord  's  's 
                  's step_type  nat  's  's" where
  "wtl_inst_list []     cert f r T B step pc s = s"
| "wtl_inst_list (i#is) cert f r T B step pc s = 
    (let s' = wtl_cert cert f r T B step pc s in
      if s' = T  s = T then T else wtl_inst_list is cert f r T B step (pc+1) s')"

definition cert_ok :: "'s certificate  nat  's  's  's set  bool" where
  "cert_ok cert n T B A  (i < n. cert!i  A  cert!i  T)  (cert!n = B)"

definition bottom :: "'a ord  'a  bool" where
  "bottom r B  x. B <=_r x"

locale lbv = Semilat +
  fixes T :: "'a" ("") 
  fixes B :: "'a" ("") 
  fixes step :: "'a step_type" 
  assumes top: "top r "
  assumes T_A: "  A"
  assumes bot: "bottom r " 
  assumes B_A: "  A"

  fixes merge :: "'a certificate  nat  (nat × 'a) list  'a  'a"
  defines mrg_def: "merge cert  LBVSpec.merge cert f r "

  fixes wti :: "'a certificate  nat  'a  'a"
  defines wti_def: "wti cert  wtl_inst cert f r  step"
 
  fixes wtc :: "'a certificate  nat  'a  'a"
  defines wtc_def: "wtc cert  wtl_cert cert f r   step"

  fixes wtl :: "'b list  'a certificate  nat  'a  'a"
  defines wtl_def: "wtl ins cert  wtl_inst_list ins cert f r   step"


lemma (in lbv) wti:
  "wti c pc s  merge c pc (step pc s) (c!(pc+1))"
  by (simp add: wti_def mrg_def wtl_inst_def)

lemma (in lbv) wtc: 
  "wtc c pc s  if c!pc =  then wti c pc s else if s <=_r c!pc then wti c pc (c!pc) else "
  by (unfold wtc_def wti_def wtl_cert_def)


lemma cert_okD1 [intro?]:
  "cert_ok c n T B A  pc < n  c!pc  A"
  by (unfold cert_ok_def) fast

lemma cert_okD2 [intro?]:
  "cert_ok c n T B A  c!n = B"
  by (simp add: cert_ok_def)

lemma cert_okD3 [intro?]:
  "cert_ok c n T B A  B  A  pc < n  c!Suc pc  A"
  by (drule Suc_leI) (auto simp add: le_eq_less_or_eq dest: cert_okD1 cert_okD2)

lemma cert_okD4 [intro?]:
  "cert_ok c n T B A  pc < n  c!pc  T"
  by (simp add: cert_ok_def)

declare Let_def [simp]

subsection "more semilattice lemmas"


lemma (in lbv) sup_top [simp, elim]:
  assumes x: "x  A" 
  shows "x +_f  = "
proof -
  from top have "x +_f  <=_r " ..
  moreover from x T_A have " <=_r x +_f " ..
  ultimately show ?thesis ..
qed
  
lemma (in lbv) plusplussup_top [simp, elim]:
  "set xs  A  xs ++_f  = "
  by (induct xs) auto



lemma (in Semilat) pp_ub1':
  assumes S: "snd`set S  A" 
  assumes y: "y  A" and ab: "(a, b)  set S" 
  shows "b <=_r map snd [(p', t')  S . p' = a] ++_f y"
proof -
  from S have "(x,y)  set S. y  A" by auto
  with semilat y ab show ?thesis by - (rule ub1')
qed 

lemma (in lbv) bottom_le [simp, intro]:
  " <=_r x"
  using bot by (simp add: bottom_def)

lemma (in lbv) le_bottom [simp]:
  "x <=_r  = (x = )"
  by (blast intro: antisym_r)



subsection "merge"

lemma (in lbv) merge_Nil [simp]:
  "merge c pc [] x = x" by (simp add: mrg_def)

lemma (in lbv) merge_Cons [simp]:
  "merge c pc (l#ls) x = merge c pc ls (if fst l=pc+1 then snd l +_f x
                                        else if snd l <=_r (c!fst l) then x
                                        else )"
  by (simp add: mrg_def split_beta)

lemma (in lbv) merge_Err [simp]:
  "snd`set ss  A  merge c pc ss  = "
  by (induct ss) auto

lemma (in lbv) merge_not_top:
  "x. snd`set ss  A  merge c pc ss x    
  (pc',s')  set ss. (pc'  pc+1  s' <=_r (c!pc'))"
  (is "x. ?set ss  ?merge ss x  ?P ss")
proof (induct ss)
  show "?P []" by simp
next
  fix x ls l
  assume "?set (l#ls)" then obtain set: "snd`set ls  A" by simp
  assume merge: "?merge (l#ls) x" 
  moreover
  obtain pc' s' where l: "l = (pc',s')" by (cases l)
  ultimately
  obtain x' where merge': "?merge ls x'" by simp 
  assume "x. ?set ls  ?merge ls x  ?P ls" hence "?P ls" using set merge' .
  moreover
  from merge set
  have "pc'  pc+1  s' <=_r (c!pc')" by (simp add: l split: if_split_asm)
  ultimately
  show "?P (l#ls)" by (simp add: l)
qed


lemma (in lbv) merge_def:
  shows 
  "x. x  A  snd`set ss  A 
  merge c pc ss x = 
  (if (pc',s')  set ss. pc'pc+1  s' <=_r c!pc' then
    map snd [(p',t')  ss. p'=pc+1] ++_f x
  else )" 
  (is "x. _  _  ?merge ss x = ?if ss x" is "x. _  _  ?P ss x")
proof (induct ss)
  fix x show "?P [] x" by simp
next 
  fix x assume x: "x  A" 
  fix l::"nat × 'a" and ls  
  assume "snd`set (l#ls)  A"
  then obtain l: "snd l  A" and ls: "snd`set ls  A" by auto
  assume "x. x  A  snd`set ls  A  ?P ls x" 
  hence IH: "x. x  A  ?P ls x" using ls by iprover
  obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
  hence "?merge (l#ls) x = ?merge ls 
    (if pc'=pc+1 then s' +_f x else if s' <=_r c!pc' then x else )"
    (is "?merge (l#ls) x = ?merge ls ?if'")
    by simp 
  also have " = ?if ls ?if'" 
  proof -
    from l have "s'  A" by simp
    with x have "s' +_f x  A" by simp
    with x T_A have "?if'  A" by auto
    hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
  qed
  also have " = ?if (l#ls) x"
    proof (cases "(pc', s')set (l#ls). pc'pc+1  s' <=_r c!pc'")
      case True
      hence "(pc', s')set ls. pc'pc+1  s' <=_r c!pc'" by auto
      moreover
      from True have 
        "map snd [(p',t')ls . p'=pc+1] ++_f ?if' = 
        (map snd [(p',t')l#ls . p'=pc+1] ++_f x)"
        by simp
      ultimately
      show ?thesis using True by simp
    next
      case False 
      moreover
      from ls have "set (map snd [(p', t')ls . p' = Suc pc])  A" by auto
      ultimately show ?thesis by auto
    qed
  finally show "?P (l#ls) x" .
qed

lemma (in lbv) merge_not_top_s:
  assumes x:  "x  A" and ss: "snd`set ss  A"
  assumes m:  "merge c pc ss x  "
  shows "merge c pc ss x = (map snd [(p',t')  ss. p'=pc+1] ++_f x)"
proof -
  from ss m have "(pc',s')  set ss. (pc'  pc+1  s' <=_r c!pc')" 
    by (rule merge_not_top)
  with x ss m show ?thesis by - (drule merge_def, auto split: if_split_asm)
qed

subsection "wtl-inst-list"

lemmas [iff] = not_Err_eq

lemma (in lbv) wtl_Nil [simp]: "wtl [] c pc s = s" 
  by (simp add: wtl_def)

lemma (in lbv) wtl_Cons [simp]: 
  "wtl (i#is) c pc s = 
  (let s' = wtc c pc s in if s' =   s =  then  else wtl is c (pc+1) s')"
  by (simp add: wtl_def wtc_def)

lemma (in lbv) wtl_Cons_not_top:
  "wtl (i#is) c pc s   = 
  (wtc c pc s    s  T  wtl is c (pc+1) (wtc c pc s)  )"
  by (auto simp del: split_paired_Ex)

lemma (in lbv) wtl_top [simp]:  "wtl ls c pc  = "
  by (cases ls) auto

lemma (in lbv) wtl_not_top:
  "wtl ls c pc s    s  "
  by (cases "s=") auto

lemma (in lbv) wtl_append [simp]:
  "pc s. wtl (a@b) c pc s = wtl b c (pc+length a) (wtl a c pc s)"
  by (induct a) auto

lemma (in lbv) wtl_take:
  "wtl is c pc s    wtl (take pc' is) c pc s  "
  (is "?wtl is  _  _")
proof -
  assume "?wtl is  "
  hence "?wtl (take pc' is @ drop pc' is)  " by simp  
  thus ?thesis by (auto dest!: wtl_not_top simp del: append_take_drop_id)
qed

lemma take_Suc:
  "n. n < length l  take (Suc n) l = (take n l)@[l!n]" (is "?P l")
proof (induct l)
  show "?P []" by simp
next
  fix x xs assume IH: "?P xs"  
  show "?P (x#xs)"
  proof (intro strip)
    fix n assume "n < length (x#xs)"
    with IH show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" 
      by (cases n, auto)
  qed
qed

lemma (in lbv) wtl_Suc:
  assumes suc: "pc+1 < length is"
  assumes wtl: "wtl (take pc is) c 0 s  "
  shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
proof -
  from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
  with suc wtl show ?thesis by (simp add: min.absorb2)
qed

lemma (in lbv) wtl_all:
  assumes all: "wtl is c 0 s  " (is "?wtl is  _") 
  assumes pc:  "pc < length is"
  shows  "wtc c pc (wtl (take pc is) c 0 s)  "
proof -
  from pc have "0 < length (drop pc is)" by simp
  then  obtain i r where Cons: "drop pc is = i#r" 
    by (auto simp add: neq_Nil_conv simp del: length_drop drop_eq_Nil)
  hence "i#r = drop pc is" ..
  with all have take: "?wtl (take pc is@i#r)  " by simp 
  from pc have "is!pc = drop pc is ! 0" by simp
  with Cons have "is!pc = i" by simp
  with take pc show ?thesis by (auto simp add: min.absorb2)
qed

subsection "preserves-type"

lemma (in lbv) merge_pres:
  assumes s0: "snd`set ss  A" and x: "x  A"
  shows "merge c pc ss x  A"
proof -
  from s0 have "set (map snd [(p', t')ss . p'=pc+1])  A" by auto
  with x  have "(map snd [(p', t')ss . p'=pc+1] ++_f x)  A"
    by (auto intro!: plusplus_closed semilat)
  with s0 x show ?thesis by (simp add: merge_def T_A)
qed
  

lemma pres_typeD2:
  "pres_type step n A  s  A  p < n  snd`set (step p s)  A"
  by auto (drule pres_typeD)


lemma (in lbv) wti_pres [intro?]:
  assumes pres: "pres_type step n A" 
  assumes cert: "c!(pc+1)  A"
  assumes s_pc: "s  A" "pc < n"
  shows "wti c pc s  A"
proof -
  from pres s_pc have "snd`set (step pc s)  A" by (rule pres_typeD2)
  with cert show ?thesis by (simp add: wti merge_pres)
qed


lemma (in lbv) wtc_pres:
  assumes pres: "pres_type step n A"
  assumes cert: "c!pc  A" and cert': "c!(pc+1)  A"
  assumes s: "s  A" and pc: "pc < n"
  shows "wtc c pc s  A"
proof -
  have "wti c pc s  A" using pres cert' s pc ..
  moreover have "wti c pc (c!pc)  A" using pres cert' cert pc ..
  ultimately show ?thesis using T_A by (simp add: wtc) 
qed


lemma (in lbv) wtl_pres:
  assumes pres: "pres_type step (length is) A"
  assumes cert: "cert_ok c (length is)   A"
  assumes s:    "s  A" 
  assumes all:  "wtl is c 0 s  "
  shows "pc < length is  wtl (take pc is) c 0 s  A"
  (is "?len pc  ?wtl pc  A")
proof (induct pc)
  from s show "?wtl 0  A" by simp
next
  fix n assume IH: "Suc n < length is"
  then have n: "n < length is" by simp  
  from IH have n1: "n+1 < length is" by simp
  assume prem: "n < length is  ?wtl n  A"
  have "wtc c n (?wtl n)  A"
  using pres _ _ _ n
  proof (rule wtc_pres)
    from prem n show "?wtl n  A" .
    from cert n show "c!n  A" by (rule cert_okD1)
    from cert n1 show "c!(n+1)  A" by (rule cert_okD1)
  qed
  also
  from all n have "?wtl n  " by - (rule wtl_take)
  with n1 have "wtc c n (?wtl n) = ?wtl (n+1)" by (rule wtl_Suc [symmetric])
  finally  show "?wtl (Suc n)  A" by simp
qed

end