(* Title: HOL/MicroJava/DFA/LBVSpec.thy Author: Gerwin Klein Copyright 1999 Technische Universitaet Muenchen *) header {* \isaheader{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" ("\<top>") fixes B :: "'a" ("⊥") fixes step :: "'a step_type" assumes top: "top r \<top>" assumes T_A: "\<top> ∈ 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 \<top>" fixes wti :: "'a certificate => nat => 'a => 'a" defines wti_def: "wti cert ≡ wtl_inst cert f r \<top> step" fixes wtc :: "'a certificate => nat => 'a => 'a" defines wtc_def: "wtc cert ≡ wtl_cert cert f r \<top> ⊥ step" fixes wtl :: "'b list => 'a certificate => nat => 'a => 'a" defines wtl_def: "wtl ins cert ≡ wtl_inst_list ins cert f r \<top> ⊥ 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 \<top>" 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] section "more semilattice lemmas" lemma (in lbv) sup_top [simp, elim]: assumes x: "x ∈ A" shows "x +_f \<top> = \<top>" proof - from top have "x +_f \<top> <=_r \<top>" .. moreover from x T_A have "\<top> <=_r x +_f \<top>" .. ultimately show ?thesis .. qed lemma (in lbv) plusplussup_top [simp, elim]: "set xs ⊆ A ==> xs ++_f \<top> = \<top>" 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') \<leftarrow> 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" by (insert bot) (simp add: bottom_def) lemma (in lbv) le_bottom [simp]: "x <=_r ⊥ = (x = ⊥)" by (blast intro: antisym_r) section "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 \<top>)" by (simp add: mrg_def split_beta) lemma (in lbv) merge_Err [simp]: "snd`set ss ⊆ A ==> merge c pc ss \<top> = \<top>" by (induct ss) auto lemma (in lbv) merge_not_top: "!!x. snd`set ss ⊆ A ==> merge c pc ss x ≠ \<top> ==> ∀(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: split_if_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') \<leftarrow> ss. p'=pc+1] ++_f x else \<top>)" (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 \<top>)" (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')\<leftarrow>ls . p'=pc+1] ++_f ?if' = (map snd [(p',t')\<leftarrow>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')\<leftarrow>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 ≠ \<top>" shows "merge c pc ss x = (map snd [(p',t') \<leftarrow> 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: split_if_asm) qed section "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' = \<top> ∨ s = \<top> then \<top> 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 ≠ \<top> = (wtc c pc s ≠ \<top> ∧ s ≠ T ∧ wtl is c (pc+1) (wtc c pc s) ≠ \<top>)" by (auto simp del: split_paired_Ex) lemma (in lbv) wtl_top [simp]: "wtl ls c pc \<top> = \<top>" by (cases ls) auto lemma (in lbv) wtl_not_top: "wtl ls c pc s ≠ \<top> ==> s ≠ \<top>" by (cases "s=\<top>") 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 ≠ \<top> ==> wtl (take pc' is) c pc s ≠ \<top>" (is "?wtl is ≠ _ ==> _") proof - assume "?wtl is ≠ \<top>" hence "?wtl (take pc' is @ drop pc' is) ≠ \<top>" 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 ≠ \<top>" 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 ≠ \<top>" (is "?wtl is ≠ _") assumes pc: "pc < length is" shows "wtc c pc (wtl (take pc is) c 0 s) ≠ \<top>" 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) ≠ \<top>" 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 section "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')\<leftarrow>ss . p'=pc+1]) ⊆ A" by auto with x have "(map snd [(p', t')\<leftarrow>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) \<top> ⊥ A" assumes s: "s ∈ A" assumes all: "wtl is c 0 s ≠ \<top>" 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 ≠ \<top>" 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