theory vcg
imports ISMT
begin

text {* This file illustrates a problem with using Yices to solve
verification conditions that require quantified lemmas. In some cases
Yices' instantiation heuristics are inadequate, but currently Yices
provides no instantiation term pattern facility that would allow us to
apply our own domain-specific quantifier heuristics. As a result, we
have to manually instantiate lemmas, often multiple times. You can see
this in the proof of vcg_lemma below. *}


subsection "Helper proof rules"

lemma int_induct2:
  "\<lbrakk>\<And>n. n \<le> 0 \<Longrightarrow> P n;
    \<And>n. \<lbrakk>n \<ge> 0; P n\<rbrakk> \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow>
   P (a::int)"
by (induct a rule: int_induct[where k=0], auto)

lemma int_cases2:
  "\<lbrakk>n \<le> (0::int) \<Longrightarrow> P;
    \<And>k. \<lbrakk>k \<ge> 0; n = k+1\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow>
   P"
by (subgoal_tac "n \<le> 0 \<or> (\<exists>y. 0 \<le> y \<and> n = y + 1)", auto, arith)


subsection "Types"

types addr = int
      byte = int
      heap = "addr \<Rightarrow> byte"


subsection "Utility functions and lemmas"      

function
   is_str :: "addr \<Rightarrow> int \<Rightarrow> heap \<Rightarrow> bool" where
  "is_str ptr n h = (if n \<le> 0 then False
                     else (h ptr = 0 \<or> is_str (ptr+1) (n - 1) h))"
by (pat_completeness, auto)
termination
  by (relation "measure (nat o fst o snd)") auto

declare is_str.simps[simp del]

lemma is_str_0[simp]:
  "n \<le> 0 \<Longrightarrow>
   \<not> is_str ptr n h"
by (subst is_str.simps, auto)

lemma is_str_Suc[simp]:
  "n \<ge> 0 \<Longrightarrow>
   is_str ptr (n+1) h = (h ptr = 0 \<or> is_str (ptr+1) n h)"
by (subst is_str.simps, auto)

lemmas is_str_simps = is_str_0 is_str_Suc
 
lemma is_str_prefix:
  "\<lbrakk>n < n';
    is_str p n h\<rbrakk> \<Longrightarrow>
   is_str p n' h"
apply (induct n arbitrary: p n' h rule: int_induct2, auto)
by (case_tac[!] n' rule: int_cases2, auto)


function
   str_addrs :: "addr \<Rightarrow> int \<Rightarrow> heap \<Rightarrow> addr list" where
  "str_addrs ptr n h
   = (if n \<le> 0 then []
      else ptr # (if h ptr = 0 then [] else str_addrs (ptr+1) (n - 1) h))"
by (pat_completeness, auto)
termination
  by (relation "measure (nat o fst o snd)") auto

declare str_addrs.simps[simp del]

lemma str_addrs_0[simp]:
  "n \<le> 0 \<Longrightarrow> str_addrs ptr n h = []"
by (subst str_addrs.simps, auto)

lemma str_addrs_Suc[simp]:
  "n \<ge> 0 \<Longrightarrow>
   str_addrs ptr (n+1) h
   = ptr # (if h ptr = 0 then [] else str_addrs (ptr+1) n h)"
by (subst str_addrs.simps, auto)

lemmas str_addrs_simps = str_addrs_0 str_addrs_Suc

lemma str_addrs_simp:
  "\<not>(p' mem str_addrs p n h) \<or> ((h p' = 0) = (x = 0)) \<Longrightarrow>
   str_addrs p n (h(p' := x)) = str_addrs p n h"
by (induct n arbitrary: p' p h rule: int_induct2, auto)

lemma str_addrs_null[simp]:
  "\<lbrakk>0 < n; h p = 0\<rbrakk> \<Longrightarrow>
   str_addrs p n h = [p]"
apply (insert str_addrs_simps)
by ismt

lemma str_addrs_fwd:
  "\<lbrakk>is_str p n h\<rbrakk> \<Longrightarrow>
   str_addrs p n h = p # (if h p = 0 then [] else str_addrs (p+1) n h)"
by (induct n arbitrary: p h rule: int_induct2, auto)

lemma mem_str_addrs_fwd:
  "\<lbrakk>is_str p n h\<rbrakk> \<Longrightarrow>
   p' mem str_addrs p n h = (p' = p \<or> h p \<noteq> 0 \<and> p' mem str_addrs (p+1) n h)"
by (auto simp add: str_addrs_fwd)


subsection "Proof of the verification condition"

text {*
src = "start of source string"
s_ptr = "location of variable s in memory (rvalue of s)"
s = "next byte in the source string to copy"
dst = "start of destination buffer"
d = "location in destination buffer to copy the next byte to"
n = "size of destination buffer (and maximum allowable size of source string,
     including null byte)"
h = "memory heap"
h' = "memory heap after the source byte has been copied and s has been incremented"
*}
definition
   vcg :: "addr \<Rightarrow> addr \<Rightarrow> addr \<Rightarrow> int \<Rightarrow> heap \<Rightarrow> bool" where
  "vcg src dst s_ptr n h
   = (let s = h s_ptr;
          d = dst - src + s;
          h' = h(d := h s, s_ptr := h s_ptr + 1)
      in ( src \<le> s \<and> is_str s (src + n - s) h
         \<and> \<not> s_ptr mem (str_addrs s n h)
         \<and> \<not> d mem (str_addrs s n h)
         \<and> h s \<noteq> 0
         \<longrightarrow> \<not> s_ptr mem (str_addrs (s+1) n h')))"

lemma vcg_lemma:
  "vcg src dst s_ptr n h"
apply (unfold vcg_def)
apply (insert is_str_0)
apply (insert is_str_prefix)
apply (insert str_addrs_simp[where p'="dst - src + h s_ptr" and x="h (h s_ptr)"])
apply (insert str_addrs_simp[where p'=s_ptr and x="h s_ptr + 1"])
apply (insert mem_str_addrs_fwd)
apply ismt
done


subsection "Detailed proof of the verification condition"

text "These are the subgoals we manually backchained on to find the
appropriate (partially) quantified lemmas to add. We started with the
conclusion at the bottom of the proof script and worked our way back
up towards the assumptions. At each backward step we checked that ismt
could solve the current lemma before trying to prove the lemmas it
depended on. "

lemma detailed_vcg_lemma:
  "vcg src dst s_ptr n h"
proof (unfold vcg_def Let_def, (rule impI | erule conjE)+)
  let ?s = "h s_ptr"
  let ?d = "dst - src + ?s"
  let ?h_tmp = "h(?d := h ?s)"
  let ?h' = "h(?d := h ?s, s_ptr := ?s + 1)"

  assume A1: "src \<le> ?s"
     and A2: "is_str ?s (src + n - ?s) h"
     and A3: "\<not> s_ptr mem (str_addrs ?s n h)"
     and A4: "\<not> ?d mem (str_addrs ?s n h)"
     and A5: "h ?s \<noteq> 0"

  from A1 A2 is_str_0 is_str_prefix
  have L1: "is_str ?s n h"
    by ismt

  from A4 A5 L1 mem_str_addrs_fwd
  have L2: "\<not> ?d mem (str_addrs (?s + 1) n h)"
    by ismt

  from L2 str_addrs_simp[where p' = ?d and x = "h ?s"]
  have L3: "str_addrs (?s+1) n ?h_tmp = str_addrs (?s+1) n h"
    by ismt

  from A3 A5 L1 L3 mem_str_addrs_fwd
  have L4: "\<not> s_ptr mem (str_addrs (?s + 1) n ?h_tmp)"
    by ismt

  from L4 str_addrs_simp[where p' = s_ptr and x = "?s + 1"]
  have L5: "str_addrs (?s+1) n ?h' = str_addrs (?s+1) n ?h_tmp"
    by ismt

  from L3 L5
  have L6: "str_addrs (?s+1) n ?h' = str_addrs (?s+1) n h"
    by ismt

  from A3 A5 L1 L6 mem_str_addrs_fwd
  show "\<not> s_ptr mem (str_addrs (?s + 1) n ?h')"
    by ismt
qed


subsection "Other failed proof attempts (commented out)"

text {* The commented-out calls below to ismt didn't return after three minutes. *}

(****
lemma str_addrs_simp:
  "\<not>(p' mem str_addrs p n h) \<or> ((h p' = 0) = (x = 0)) \<Longrightarrow>
   str_addrs p n (h(p' := x)) = str_addrs p n h"
apply (insert str_addrs_simps)
apply (insert member.simps[where ?'a_1.0=int])
apply ismt
*****)

(****
lemma "vcg src dst s_ptr n h"
apply (unfold vcg_def)
apply (insert is_str_0)
apply (insert is_str_prefix)
apply (insert str_addrs_simp[where p'="dst + h s_ptr - src"])
apply (insert str_addrs_simp[where p'=s_ptr])
apply (insert mem_str_addrs_fwd)
apply ismt
done
*****)

(*****
lemma "vcg src dst s_ptr n h"
apply (unfold vcg_def)
apply (insert is_str_0)
apply (insert is_str_prefix)
apply (insert str_addrs_simp[where x="h (h s_ptr)"])
apply (insert str_addrs_simp[where x="h s_ptr + 1"])
apply (insert mem_str_addrs_fwd)
apply ismt
done
******)

text {* However, the last two instantiations of str_addrs_simp
above do work for the proof of detailed_vcg_lemma
when used to prove local lemmas L3 and L5. However, we
kept the more detailed instantations there, since the
point of that proof was to find the right instantiations
for vcg_lemma. *}


end