# Theory LBVSpec

Up to index of Isabelle/HOL/MicroJava

theory LBVSpec
imports SemilatAlg Opt
begin

    (*  Title:      HOL/MicroJava/BV/LBVSpec.thy
        ID:         $Id: LBVSpec.thy,v 1.30 2005/06/17 14:13:08 haftmann Exp $
        Author:     Gerwin Klein
        Copyright   1999 Technische Universitaet Muenchen
    *)

    header {* \isaheader{The Lightweight Bytecode Verifier} *}

    theory LBVSpec imports SemilatAlg Opt begin

    types
      's certificate = "'s list"

    consts
    merge :: "'s certificate => 's binop => 's ord => 's => nat => (nat × 's) list => 's => 's"
    primrec
    "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)"

    constdefs
    wtl_inst :: "'s certificate => 's binop => 's ord => 's =>
                 's step_type => nat => 's => 's"
    "wtl_inst cert f r T step pc s ≡ merge cert f r T pc (step pc s) (cert!(pc+1))"

    wtl_cert :: "'s certificate => 's binop => 's ord => 's => 's =>
                 's step_type => nat => 's => 's"
    "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"

    consts
    wtl_inst_list :: "'a list => 's certificate => 's binop => 's ord => 's => 's =>
                      's step_type => nat => 's => 's"
    primrec
    "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')"

    constdefs
      cert_ok :: "'s certificate => nat => 's => 's => 's set => bool"
      "cert_ok cert n T B A ≡ (∀i < n. cert!i ∈ A ∧ cert!i ≠ T) ∧ (cert!n = B)"

    constdefs
      bottom :: "'a ord => 'a => bool"
      "bottom r B ≡ ∀x. B <=_r x"

    locale (open) 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 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')∈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 [simp]: "l = (pc',s')" by (cases l)
      ultimately
      obtain x' where "?merge ls x'" by simp
      assume "!!x. ?set ls ==> ?merge ls x ==> ?P ls" hence "?P ls" .
      moreover
      from merge set
      have "pc' ≠ pc+1 --> s' <=_r (c!pc')" by (simp split: split_if_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 \<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" .
      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 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 ≠ \<top>"
      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: 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_def)
    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_def split: split_if_asm)
    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')∈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)
      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" ..
      moreover have "wti c pc (c!pc) ∈ A" ..
      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 "Suc n < length is"
      then obtain n: "n < length is" by simp
      assume "n < length is ==> ?wtl n ∈ A"
      hence "?wtl n ∈ A" .
      moreover
      from cert have "c!n ∈ A" by (rule cert_okD1)
      moreover
      have n1: "n+1 < length is" by simp
      with cert have "c!(n+1) ∈ A" by (rule cert_okD1)
      ultimately
      have "wtc c n (?wtl n) ∈ A" by - (rule wtc_pres)
      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

lemma wti:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> wtl_inst c f r T step pc s == merge c f r T pc (step pc s) (c ! (pc + 1))

lemma wtc:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> wtl_cert c f r T B step pc s ==
          if c ! pc = B then wtl_inst c f r T step pc s
          else if s <=_r c ! pc then wtl_inst c f r T step pc (c ! pc) else T

lemma cert_okD1:

      [| cert_ok c n T B A; pc < n |] ==> c ! pc ∈ A

lemma cert_okD2:

      cert_ok c n T B A ==> c ! n = B

lemma cert_okD3:

      [| cert_ok c n T B A; B ∈ A; pc < n |] ==> c ! Suc pc ∈ A

lemma cert_okD4:

      [| cert_ok c n T B A; pc < n |] ==> c ! pc ≠ T

## more semilattice lemmas

lemma sup_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; x ∈ A |]
      ==> x +_f T = T

lemma plusplussup_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; set xs ⊆ A |]
      ==> xs ++_f T = T

lemma pp_ub1':

      [| semilat (A, r, f); snd ` set S ⊆ A; y ∈ A; (a, b) ∈ set S |]
      ==> b <=_r map snd [(p', t')∈S . p' = a] ++_f y

lemma bottom_le:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |] ==> B <=_r x

lemma le_bottom:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> (x <=_r B) = (x = B)

## merge

lemma merge_Nil:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> merge c f r T pc [] x = x

lemma merge_Cons:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> merge c f r T pc (l # ls) x =
          merge c f r T pc ls
           (if fst l = pc + 1 then snd l +_f x
            else if snd l <=_r c ! fst l then x else T)

lemma merge_Err:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; snd ` set ss ⊆ A |]
      ==> merge c f r T pc ss T = T

lemma merge_not_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; snd ` set ss ⊆ A;
         merge c f r T pc ss x ≠ T |]
      ==> ∀(pc', s')∈set ss. pc' ≠ pc + 1 --> s' <=_r c ! pc'

lemma merge_def:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; x ∈ A;
         snd ` set ss ⊆ A |]
      ==> merge c f r T 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 T)

lemma merge_not_top_s:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; x ∈ A;
         snd ` set ss ⊆ A; merge c f r T pc ss x ≠ T |]
      ==> merge c f r T pc ss x = map snd [(p', t')∈ss . p' = pc + 1] ++_f x

## wtl-inst-list

lemmas

      (x ≠ Err) = (∃a. x = OK a)

lemmas

      (x ≠ Err) = (∃a. x = OK a)

lemma wtl_Nil:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> wtl_inst_list [] c f r T B step pc s = s

lemma wtl_Cons:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> wtl_inst_list (i # is) c f r T B step pc s =
          (let s' = wtl_cert c f r T B step pc s
           in if s' = T ∨ s = T then T
              else wtl_inst_list is c f r T B step (pc + 1) s')

lemma wtl_Cons_not_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> (wtl_inst_list (i # is) c f r T B step pc s ≠ T) =
          (wtl_cert c f r T B step pc s ≠ T ∧
           s ≠ T ∧
           wtl_inst_list is c f r T B step (pc + 1) (wtl_cert c f r T B step pc s) ≠
           T)

lemma wtl_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> wtl_inst_list ls c f r T B step pc T = T

lemma wtl_not_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         wtl_inst_list ls c f r T B step pc s ≠ T |]
      ==> s ≠ T

lemma wtl_append:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> wtl_inst_list (a @ b) c f r T B step pc s =
          wtl_inst_list b c f r T B step (pc + length a)
           (wtl_inst_list a c f r T B step pc s)

lemma wtl_take:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         wtl_inst_list is c f r T B step pc s ≠ T |]
      ==> wtl_inst_list (take pc' is) c f r T B step pc s ≠ T

lemma take_Suc:

      ∀n<length l. take (Suc n) l = take n l @ [l ! n]

lemma wtl_Suc:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; pc + 1 < length is;
         wtl_inst_list (take pc is) c f r T B step 0 s ≠ T |]
      ==> wtl_inst_list (take (pc + 1) is) c f r T B step 0 s =
          wtl_cert c f r T B step pc (wtl_inst_list (take pc is) c f r T B step 0 s)

lemma wtl_all:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         wtl_inst_list is c f r T B step 0 s ≠ T; pc < length is |]
      ==> wtl_cert c f r T B step pc (wtl_inst_list (take pc is) c f r T B step 0 s) ≠
          T

## preserves-type

lemma merge_pres:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; snd ` set ss ⊆ A;
         x ∈ A |]
      ==> merge c f r T pc ss x ∈ A

lemma pres_typeD2:

      [| pres_type step n A; s ∈ A; p < n |] ==> snd ` set (step p s) ⊆ A

lemma wti_pres:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; pres_type step n A;
         c ! (pc + 1) ∈ A; s ∈ A; pc < n |]
      ==> wtl_inst c f r T step pc s ∈ A

lemma wtc_pres:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; pres_type step n A;
         c ! pc ∈ A; c ! (pc + 1) ∈ A; s ∈ A; pc < n |]
      ==> wtl_cert c f r T B step pc s ∈ A

lemma wtl_pres:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         pres_type step (length is) A; cert_ok c (length is) T B A; s ∈ A;
         wtl_inst_list is c f r T B step 0 s ≠ T; pc < length is |]
      ==> wtl_inst_list (take pc is) c f r T B step 0 s ∈ A