Theory Store

theory Store
imports Aexp Bexp
begin

section‹Stores›

text ‹In this section, we introduce the type of stores, which we use to link program variables 
with their symbolic counterpart during symbolic execution. We define the notion of consistency 
of a pair of program and symbolic states w.r.t.\ a store. This notion will prove helpful when 
defining various concepts and proving facts related to subsumption (see \verb?Conf.thy?). Finally, we 
model substitutions that will be performed during symbolic execution (see \verb?SymExec.thy?) by two 
operations: @{term adapt_aexp} and @{term adapt_bexp}.›

subsection ‹Basic definitions›

subsubsection ‹The @{term "store"} type-synonym›

text ‹Symbolic execution performs over configurations (see \verb?Conf.thy?), which are pairs made 
of:
\begin{itemize} 
\item a \emph{store} mapping program variables to symbolic variables,
\item a set of boolean expressions which records constraints over symbolic variables and whose 
conjunction is the actual path predicate of the configuration.
\end{itemize}
We define stores as total functions from program variables to indexes.›


type_synonym 'a store = "'a ⇒ nat"


subsubsection ‹Symbolic variables of a store›

text ‹The symbolic variable associated to a program variable @{term "v"} by a store 
@{term "s"} is the couple @{term "(v,s v)"}.›


definition symvar :: 
  "'a ⇒ 'a store ⇒ 'a symvar"
where
  "symvar v s ≡ (v,s v)"


text ‹The function associating symbolic variables to program variables obtained from 
@{term "s"} is injective.›


lemma 
  "inj (λ v. symvar v s)"
by (auto simp add : inj_on_def symvar_def)


text ‹The sets of symbolic variables of a store is the image set of the function @{term "symvar"}.›


definition symvars :: 
  "'a store ⇒ 'a symvar set" 
where
 "symvars s = (λ v. symvar v s) ` (UNIV::'a set)"


subsubsection ‹Fresh symbolic variables›

text ‹A symbolic variable is said to be fresh for a store if it is not a member of its set of 
symbolic variables.›


definition fresh_symvar :: 
  "'v symvar ⇒ 'v store ⇒ bool" 
where
 "fresh_symvar sv s = (sv ∉ symvars s)"


subsection ‹Consistency›

text ‹We say that a program state @{term "σ"} and a symbolic state @{term "σsym"} are 
\emph{consistent} with respect to a store @{term "s"} if, for each variable @{term "v"}, the 
value associated by @{term "σ"} to @{term "v"} is equal to the value associated by @{term "σsym"} 
to the symbolic variable associated to @{term "v"} by @{term "s"}.›


definition consistent ::
  "('v,'d) state ⇒ ('v symvar, 'd) state ⇒ 'v store ⇒ bool"
where
  "consistent σ σsym s ≡ (∀ v. σsym (symvar v s) = σ v)"


text ‹There always exists a couple of consistent states for a given store.›


lemma
  "∃ σ σsym. consistent σ σsym s"
by (auto simp add : consistent_def)


text ‹Moreover, given a store and a program (resp. symbolic) state, one can always build a symbolic 
(resp. program) state such that the two states are coherent wrt.\ the store. The four following 
lemmas show how to build the second state given the first one.›


lemma consistent_eq1 :
  "consistent σ σsym s = (∀ sv ∈ symvars s. σsym sv = σ (fst sv))"
by (auto simp add : consistent_def symvars_def symvar_def)


lemma consistent_eq2 :
  "consistent σ σsym store = (σ = (λ v. σsym (symvar v store)))"
by (auto simp add : consistent_def)


lemma consistentI1 : 
  "consistent σ (λ sv. σ (fst sv)) store" 
using consistent_eq1 by fast


lemma consistentI2 :
  "consistent (λ v. σsym (symvar v store)) σsym store"
using consistent_eq2 by fast



subsection ‹Adaptation of an arithmetic expression to a store›

text ‹Suppose that @{term "e"} is a term representing an arithmetic expression over program 
variables and let @{term "s"} be a store. We call \emph{adaptation of @{term "e"} to @{term "s"}} 
the term obtained by substituting occurrences of program variables in @{term "e"} by their 
symbolic counterpart given by @{term "s"}. Since we model arithmetic expressions by total 
functions and not terms, we define the adaptation of such expressions as follows.›


definition adapt_aexp :: 
  "('v,'d) aexp ⇒ 'v store ⇒ ('v symvar,'d) aexp" 
where
  "adapt_aexp e s = (λ σsym. e (λ v. σsym (symvar v s)))"


text ‹Given an arithmetic expression @{term "e"}, a program state @{term "σ"} and a symbolic 
state @{term "σsym"} coherent with a store @{term "s"}, the value associated to @{term "σsym"} by 
the adaptation of @{term "e"} to @{term "s"} is the same than the value associated by @{term "e"} to 
@{term "σ"}. This confirms the fact that @{term "adapt_aexp"} models the act of substituting 
occurrences of program variables by their symbolic counterparts in a term over program variables.›


lemma adapt_aexp_is_subst :
  assumes "consistent σ σsym s" 
  shows   "(adapt_aexp e s) σsym = e σ"
using assms by (simp add : consistent_eq2 adapt_aexp_def)



text ‹As said earlier, we will later need to prove that symbolic execution preserves finiteness 
of the set of symbolic variables in use, which requires that the adaptation of an arithmetic 
expression to a store preserves finiteness of the set of variables of expressions. We proceed as 
follows.›

text ‹First, we show that if @{term "v"} is a variable of an expression @{term "e"}, 
then the symbolic variable associated to @{term "v"} by a store is a variable of the adaptation of 
@{term "e"} to this store.›


lemma var_imp_symvar_var :
  assumes "v ∈ Aexp.vars e"
  shows   "symvar v s ∈ Aexp.vars (adapt_aexp e s)" (is "?sv ∈ Aexp.vars ?e'")
proof -
  obtain σ val where "e (σ (v := val)) ≠ e σ" 
  using assms unfolding Aexp.vars_def by blast  
  
  moreover
  have "(λva. ((λsv. σ (fst sv))(?sv := val)) (symvar va s)) = (σ(v := val))"
  by (auto simp add : symvar_def)  

  ultimately
  show ?thesis
  unfolding Aexp.vars_def mem_Collect_eq
  using consistentI1[of σ s] 
        consistentI2[of "(λsv. σ (fst sv))(?sv:= val)" s]
  by (rule_tac ?x="λsv. σ (fst sv)" in exI, rule_tac ?x="val" in exI) 
     (simp add : adapt_aexp_is_subst)
qed


text ‹On the other hand, if @{term "sv"} is a symbolic variable in the adaptation of an expression 
to a store, then the program variable it represents is a variable of this expression. This requires 
to prove that the set of variables of the adaptation of an expression to a store is a subset of the 
symbolic variables of this store.›


lemma symvars_of_adapt_aexp :
  "Aexp.vars (adapt_aexp e s) ⊆ symvars s" (is "Aexp.vars ?e' ⊆ symvars s")
unfolding subset_iff
proof (intro allI impI)
  fix sv

  assume "sv ∈ Aexp.vars ?e'"

  then obtain σsym val 
  where "?e' (σsym (sv := val)) ≠ ?e' σsym" 
  by (simp add : Aexp.vars_def, blast)

  hence "(λ x. (σsym (sv := val)) (symvar x s)) ≠ (λ x. σsym (symvar x s))"
  proof (intro notI)
    assume "(λx. (σsym(sv := val)) (symvar x s)) = (λx. σsym (symvar x s))"
    
    hence "?e' (σsym (sv := val)) = ?e' σsym" 
    by (simp add : adapt_aexp_def)
    
    thus False 
    using ‹?e' (σsym (sv := val)) ≠ ?e' σsym› 
    by (elim notE)
  qed

  then obtain v 
  where "(σsym (sv := val)) (symvar v s) ≠ σsym (symvar v s)" 
  by blast

  hence "sv = symvar v s" by (case_tac "sv = symvar v s", simp_all)

  thus "sv ∈ symvars s" by (simp add : symvars_def)
qed


lemma symvar_var_imp_var :
  assumes "sv ∈ Aexp.vars (adapt_aexp e s)" (is "sv ∈ Aexp.vars ?e'")
  shows   "fst sv ∈ Aexp.vars e"
proof -
  obtain v where "sv = (v, s v)" 
  using assms(1) symvars_of_adapt_aexp 
  unfolding symvars_def symvar_def 
  by blast
  
  obtain σsym val where "?e' (σsym (sv := val)) ≠ ?e' σsym"
  using assms unfolding Aexp.vars_def by blast

  moreover
  have "(λ v. (σsym (sv := val)) (symvar v s)) = (λ v. σsym (symvar v s)) (v := val)"
  using ‹sv = (v, s v)› by (auto simp add : symvar_def)
  
  ultimately
  show ?thesis
  using ‹sv = (v, s v)› 
        consistentI2[of σsym s] 
        consistentI2[of "σsym (sv := val)" s]
  unfolding Aexp.vars_def 
  by (simp add : adapt_aexp_is_subst) blast
qed



text ‹Thus, we have that the set of variables of the adaptation of an expression to a store is 
the set of symbolic variables associated by this store to the variables of this 
expression.›


lemma adapt_aexp_vars :
  "Aexp.vars (adapt_aexp e s) = (λ v. symvar v s) ` Aexp.vars e"
unfolding set_eq_iff image_def mem_Collect_eq Bex_def
proof (intro allI iffI, goal_cases)
  case (1 sv)

  moreover
  have "sv = symvar (fst sv) s" 
  using 1 symvars_of_adapt_aexp 
  by (force simp add:  symvar_def symvars_def)

  ultimately
  show ?case using symvar_var_imp_var by blast
next
  case (2 sv) thus ?case using var_imp_symvar_var by fast
qed 


text ‹The fact that the adaptation of an arithmetic expression to a store preserves finiteness 
of the set of variables trivially follows the previous lemma.›


lemma finite_vars_imp_finite_adapt_a :
  assumes "finite (Aexp.vars e)"
  shows   "finite (Aexp.vars (adapt_aexp e s))"
unfolding adapt_aexp_vars using assms by auto

subsection ‹Adaptation of a boolean expression to a store›

text ‹We proceed analogously for the adaptation of boolean expressions to a store.›


definition adapt_bexp :: 
  "('v,'d) bexp ⇒ 'v store ⇒ ('v symvar,'d) bexp" 
where
  "adapt_bexp e s = (λ σ. e (λ x. σ (symvar x s)))"


lemma adapt_bexp_is_subst :
  assumes "consistent σ σsym s" 
  shows   "(adapt_bexp e s) σsym = e σ"
using assms by (simp add : consistent_eq2 adapt_bexp_def)


lemma var_imp_symvar_var2 :
  assumes "v ∈ Bexp.vars e"
  shows   "symvar v s ∈ Bexp.vars (adapt_bexp e s)" (is "?sv ∈ Bexp.vars ?e'")
proof -
  obtain σ val where A : "e (σ (v := val)) ≠ e σ" 
  using assms unfolding Bexp.vars_def by blast  
  
  moreover
  have "(λva. ((λsv. σ (fst sv))(?sv := val)) (symvar va s)) = (σ(v := val))"
  by (auto simp add : symvar_def)  

  ultimately
  show ?thesis
  unfolding Bexp.vars_def mem_Collect_eq
  using consistentI1[of σ s] 
        consistentI2[of "(λsv. σ (fst sv))(?sv:= val)" s]
  by (rule_tac ?x="λsv. σ (fst sv)" in exI, rule_tac ?x="val" in exI) 
     (simp add : adapt_bexp_is_subst)
qed


lemma symvars_of_adapt_bexp :
  "Bexp.vars (adapt_bexp e s) ⊆ symvars s" (is "Bexp.vars ?e' ⊆ ?SV")
proof
  fix sv
  assume "sv ∈ Bexp.vars ?e'"

  then obtain σsym val 
  where "?e' (σsym (sv := val)) ≠ ?e' σsym"
  by (simp add : Bexp.vars_def, blast)

  hence "(λ x. (σsym (sv := val)) (symvar x s)) ≠ (λ x. σsym (symvar x s))"
  by (auto simp add : adapt_bexp_def)

  hence "∃ v. (σsym (sv := val)) (symvar v s) ≠ σsym (symvar v s)" by force

  then obtain v 
  where "(σsym (sv := val)) (symvar v s) ≠ σsym (symvar v s)" 
  by blast

  hence "sv = symvar v s" by (case_tac "sv = symvar v s", simp_all)

  thus "sv ∈ symvars s" by (simp add : symvars_def)
qed


lemma symvar_var_imp_var2 :
  assumes "sv ∈ Bexp.vars (adapt_bexp e s)" (is "sv ∈ Bexp.vars ?e'")
  shows   "fst sv ∈ Bexp.vars e"
proof -
  obtain v where "sv = (v, s v)" 
  using assms symvars_of_adapt_bexp 
  unfolding symvars_def symvar_def 
  by blast
  
  obtain σsym val where "?e' (σsym (sv := val)) ≠ ?e' σsym"
  using assms unfolding vars_def by blast

  moreover
  have "(λ v. (σsym (sv := val)) (symvar v s)) = (λ v. σsym (symvar v s)) (v := val)"
  using ‹sv = (v, s v)› by (auto simp add : symvar_def)
  
  ultimately
  show ?thesis
  using ‹sv = (v, s v)› 
        consistentI2[of σsym s] 
        consistentI2[of "σsym (sv := val)" s]
  unfolding vars_def by (simp add : adapt_bexp_is_subst) blast
qed


lemma adapt_bexp_vars :
  "Bexp.vars (adapt_bexp e s) = (λ v. symvar v s) ` Bexp.vars e"
  (is "Bexp.vars ?e' = ?R")
unfolding set_eq_iff image_def mem_Collect_eq Bex_def
proof (intro allI iffI, goal_cases)
  case (1 sv)

  hence "fst sv ∈ vars e" by (rule symvar_var_imp_var2)

  moreover
  have "sv = symvar (fst sv) s" 
  using 1 symvars_of_adapt_bexp 
  by (force simp add:  symvar_def symvars_def)

  ultimately
  show ?case by blast
next
  case (2 sv)

  then obtain v where "v ∈ vars e" "sv = symvar v s" by blast

  thus ?case using var_imp_symvar_var2 by simp
qed 


lemma finite_vars_imp_finite_adapt_b :
  assumes "finite (Bexp.vars e)"
  shows   "finite (Bexp.vars (adapt_bexp e s))"
unfolding adapt_bexp_vars using assms by auto

end