Theory LBVSpec
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) rule
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 semilat have "order r A" by auto
moreover from x T_A have xfT_inA: "x ⊔⇩f ⊤ ∈ A" by auto
with T_A top have xfT: "x ⊔⇩f ⊤ ⊑⇩r ⊤" by (simp add:top_def)
moreover from x T_A have "⊤ ⊑⇩r x ⊔⇩f ⊤" ..
ultimately show ?thesis using xfT_inA T_A by (rule order_antisym)
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_axioms show ?thesis using y ab 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 ∈ A ⟹ x ⊑⇩r ⊥ = (x = ⊥)"
using B_A 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 [simp]: "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 split: if_split_asm)
ultimately show "?P (l#ls)" by simp
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_def)
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_def split: if_split_asm)
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 semilat Semilat_axioms have "(map snd [(p', t') ← ss . p'=pc+1] ⨆⇘f⇙ x) ∈ A"
by (auto intro!: plusplus_closed)
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_type step n A"
assumes "c!pc ∈ A" and "c!(pc+1) ∈ A"
assumes "s ∈ A" and "pc < n"
shows "wtc c pc s ∈ A"
proof -
have "wti c pc s ∈ A" using assms(1,3-5) ..
moreover have "wti c pc (c!pc) ∈ A" using assms(1,3,2,5) ..
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 Suc_n: "Suc n < length is"
hence n1: "n+1 < length is" by simp
then obtain n: "n < length is" by simp
assume "n < length is ⟹ ?wtl n ∈ A"
hence "?wtl n ∈ A" using n .
from pres _ _ this n
have "wtc c n (?wtl n) ∈ A"
proof (rule wtc_pres)
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