Theory IMP2_VCG

section ‹Verification Condition Generator›
theory IMP2_VCG
imports IMP2_Basic_Simpset IMP2_Program_Analysis IMP2_Var_Postprocessor IMP2_Var_Abs
begin

subsection ‹Preprocessing›

  lemma HT'_I[vcg_preprocess_rules]:
    assumes "⋀𝔰⇩0. ⟦ P 𝔰⇩0 ⟧ ⟹ wp π (c 𝔰⇩0) (Q 𝔰⇩0) 𝔰⇩0"
    shows "HT' π P c Q"
    using assms
    unfolding BB_PROTECT_def HT'_def by auto
  
  lemma HT'_partial_I[vcg_preprocess_rules]:
    assumes "⋀𝔰⇩0. ⟦ P 𝔰⇩0 ⟧ ⟹ wlp π (c 𝔰⇩0) (Q 𝔰⇩0) 𝔰⇩0"
    shows "HT'_partial π P c Q"
    using assms
    unfolding BB_PROTECT_def HT'_partial_def by auto
  
    
  lemmas [vcg_preprocess_rules] = allI impI conjI
    
  method i_vcg_preprocess = 
    (intro vcg_preprocess_rules)?

  subsection ‹VC rules›


  named_theorems vcg_comb_rules ‹VCG rules for Combinators›
  
  subsubsection ‹Goal Indication›  
  text ‹A marker to indicate where a goal comes from.›
  (* TODO: Noschinski has driven this to the extreme, allowing to generate a 
    complete isar case setup from such annotations. 
    We should adapt (at least parts of) this idea!
  *)
  definition GOAL_INDICATION :: "'a ⇒ bool" ("¶_" [1000])
    where "GOAL_INDICATION _ ≡ True"
  
  lemma move_goal_indication_to_front[simp, named_ss vcg_bb]: 
    "NO_MATCH (¶x) P ⟹ (P⟹¶n⟹PROP Q) ≡ (¶n ⟹ P ⟹ PROP Q)"  
    by (rule swap_prems_eq)
    (* TODO: Would like to use PROP P here, to also move over 
      meta-premises like ‹⋀x. a⟹b›, but ‹NO_MATCH› requires type! *)
  
  
  
  
  subsubsection ‹Modularity (Frame) Rules›  
  
  text ‹Frame rules are only applied if their first assumption can be 
    discharged by a specification rule.›
  named_theorems vcg_frame_rules ‹Frame rules for VCG Approximation Phase›

    
  lemma vcg_wlp_modularity_rl[vcg_frame_rules]:
    assumes "HT_partial_mods π mods P c Q"
    assumes "P s"
    assumes "⋀s'. ⟦modifies mods s' s; Q s s'⟧ ⟹ Q' s'"
    shows "wlp π (c) (λs'. Q' s') s"
    using vcg_wlp_conseq assms by metis
  
  lemma vcg_wp_modularity_rl[vcg_frame_rules]:
    assumes "HT_mods π mods P c Q"
    assumes "P s"
    assumes "⋀s'. ⟦modifies mods s' s ; Q s s'⟧ ⟹Q' s'"
    shows "wp π (c) (λs'. Q' s') s"
    using vcg_wp_conseq assms by metis
    
  lemma vcg_wp_wlp_modularity_rl[vcg_frame_rules]:
    assumes "HT_mods π mods P c Q"
    assumes "P s"
    assumes "⋀s'. ⟦modifies mods s' s; Q s s'⟧ ⟹ Q' s'"
    shows "wlp π (c) (λs'. Q' s') s"
    using vcg_wlp_wp_conseq assms by metis
  
  lemmas [named_ss vcg_bb] = Params_def Inline_def
  
  subsubsection ‹Skip and Sequential Composition›  
  text ‹Skip and sequential composition are unfolded by the VCG basic simpset›
        
  lemmas [named_ss vcg_bb] = 
    wp_skip_eq wp_seq_eq wlp_skip_eq wlp_seq_eq
    
    
  subsubsection ‹Assignments›  

  text ‹Assignments are unfolded, using the UPD_STATE constants with a custom simpset 
    to efficiently handle state updates.
  ›
  
  lemmas [named_ss vcg_bb] = 
    aval.simps bval.simps
  
  
  definition UPD_STATE :: "state ⇒ vname ⇒ val ⇒ state" where
    "UPD_STATE s x v ≡ s(x:=v)"

  definition UPD_IDX :: "val ⇒ int ⇒ pval ⇒ val" where
    "UPD_IDX av i pv ≡ av(i:=pv)"
        
  definition UPD_STATE_IDX :: "state ⇒ vname ⇒ int ⇒ pval ⇒ state" where
    "UPD_STATE_IDX s x i v ≡ s(x:=UPD_IDX (s x) i v)"
    

  lemma [named_ss vcg_bb]:
    "UPD_STATE (s(x:=w)) x v = s(x:=v)"
    "x≠y ⟹ UPD_STATE (s(x:=w)) y v = (UPD_STATE s y v)(x:=w)"  
    "NO_MATCH (SS(XX:=VV)) s ⟹ UPD_STATE s x v = s(x:=v)"
    by (auto simp: UPD_STATE_def)
        
  lemma [named_ss vcg_bb]:
    "UPD_STATE_IDX (s(x:=w)) x i v = s(x:=UPD_IDX w i v)"
    "x≠y ⟹ UPD_STATE_IDX (s(x:=w)) y i v = (UPD_STATE_IDX s y i v)(x:=w)"  
    "NO_MATCH (SS(XX:=VV)) s ⟹ UPD_STATE_IDX s x i v = s(x:=UPD_IDX (s x) i v)"
    by (auto simp: UPD_STATE_IDX_def)
 
  (* Note (hack): These two rewrite rules exploit inner-to-outer rewrite order
    to ensure that the first rule is applied first.
  *)  
  lemma [named_ss vcg_bb]:  
    "UPD_IDX (a(i:=v)) i = UPD_IDX a i"
    "UPD_IDX a i v = (a(i:=v))"          
    by (auto simp: UPD_IDX_def)
  
  lemma vcg_assign_idx_unfolds[named_ss vcg_bb]:
    "wlp π (x[i] ::= a) Q s = Q (UPD_STATE_IDX s x (aval i s) (aval a s))"
    "wp π (x[i] ::= a) Q s = Q (UPD_STATE_IDX s x (aval i s) (aval a s))"
    unfolding UPD_STATE_IDX_def UPD_IDX_def 
    by (simp_all add: wlp_eq wp_eq)
  
  lemma vcg_arraycpy_unfolds[named_ss vcg_bb]:
    "wlp π (x[] ::= a) Q s = Q (UPD_STATE s x (s a))"
    "wp π (x[] ::= a) Q s = Q (UPD_STATE s x (s a))"
    unfolding UPD_STATE_def 
    by (simp_all add: wlp_eq wp_eq)

  lemma vcg_arrayinit_unfolds[named_ss vcg_bb]:
    "wlp π (CLEAR x[]) Q s = Q (UPD_STATE s x (λ_. 0))"
    "wp π (CLEAR x[]) Q s = Q (UPD_STATE s x (λ_. 0))"
    unfolding UPD_STATE_def 
    by (simp_all add: wlp_eq wp_eq)
    
  text ‹Special case for procedure return value: 
    Insert a renaming to keep name of original variable›  

    
  lemma vcg_AssignIdx_retv_wlp_unfold[named_ss vcg_bb]:
    "wlp π (AssignIdx_retv x i a) Q s = (NAMING_HINT s a x ⟶ wlp π (x[i]::=V a) Q s)"
    unfolding AssignIdx_retv_def NAMING_HINT_def by auto
    
  lemma vcg_AssignIdx_retv_wp_unfold[named_ss vcg_bb]:
    "wp π (AssignIdx_retv x i a) Q s = (NAMING_HINT s a x ⟶ wp π (x[i]::=V a) Q s)"
    unfolding AssignIdx_retv_def NAMING_HINT_def by auto
    
  lemma vcg_ArrayCpy_retv_wlp_unfold[named_ss vcg_bb]:
    "wlp π (ArrayCpy_retv x a) Q s = (NAMING_HINT s a x ⟶ wlp π (x[]::=a) Q s)"  
    unfolding ArrayCpy_retv_def NAMING_HINT_def by auto
    
  lemma vcg_ArrayCpy_retv_wp_unfold[named_ss vcg_bb]:
    "wp π (ArrayCpy_retv x a) Q s = (NAMING_HINT s a x ⟶ wp π (x[]::=a) Q s)"  
    unfolding ArrayCpy_retv_def NAMING_HINT_def by auto

  lemma naming_hint_impI_simp[named_ss vcg_bb]: 
    "Trueprop (NAMING_HINT s a x ⟶ P) ≡ (NAMING_HINT s a x ⟹ P)" by rule auto

  subsubsection ‹Scope›    
    
  lemmas [named_ss vcg_bb] = 
    wp_scope_eq wlp_scope_eq


  subsubsection ‹While›  
        
  lemma wlp_whileI_modset:
    fixes c π
    defines [simp]: "modset ≡ ANALYZE (lhsv π c)"
    assumes INIT: "I s⇩0"
    assumes STEP: "⋀s. ⟦ modifies modset s s⇩0; I s; bval b s ⟧ ⟹ wlp π c (λs'. I s') s"
    assumes FINAL: "⋀s. ⟦ modifies modset s s⇩0; I s; ¬bval b s ⟧ ⟹ Q s"
    shows "wlp π (WHILE b DO c) Q s⇩0"
    apply (rule wlp_whileI[where I="λs. I s ∧ modifies modset s s⇩0"])
    subgoal using INIT by simp
    subgoal
      apply (rule wlp_conseq, rule wlp_strengthen_modset, rule STEP)
         apply (auto dest: modifies_trans simp: modifies_sym)
      done
    subgoal using FINAL by (simp add: modifies_sym)
    done
    
  lemma wp_whileI_modset:
    fixes c π
    defines [simp]: "modset ≡ ANALYZE (lhsv π c)"
    assumes WF: "wf R"
    assumes INIT: "I s⇩0"
    assumes STEP: "⋀s. ⟦ modifies modset s s⇩0; I s; bval b s ⟧ ⟹ wp π c (λs'. I s' ∧ (s',s)∈R) s"
    assumes FINAL: "⋀s. ⟦ modifies modset s s⇩0; I s; ¬bval b s ⟧ ⟹ Q s"
    shows "wp π (WHILE b DO c) Q s⇩0"
    apply (rule wp_whileI[where I="λs. I s ∧ modifies modset s s⇩0" and R=R])
       apply (rule WF)
      subgoal using INIT by simp
     subgoal
      apply (rule wp_conseq, rule wp_strengthen_modset, rule STEP)
         apply (auto dest: modifies_trans simp: modifies_sym)
      done
    subgoal using FINAL by (simp add: modifies_sym)
    done

  definition invar_var_goal where
    "invar_var_goal I R v s s' ≡ I s' ∧ (v s',v s)∈R"
  
  lemma invar_var_goalI[vcg_comb_rules]:
    "invar_var_goal I R v s s'" if "¶''Invar pres'' ⟹ I s'" "¶''Var pres'' ⟹ (v s',v s)∈R"
    using that unfolding invar_var_goal_def GOAL_INDICATION_def by auto
    
        
  lemma wp_while_rl[vcg_comb_rules]:
    assumes "¶''rel-wf'' ⟹ wf R"
    assumes "¶''invar-initial'' ⟹ I s⇩0"
    assumes "⋀s. ⟦ modifies modset s s⇩0; I s; bval b s ⟧ 
      ⟹ wp π c (invar_var_goal I R v s) s"
    assumes "⋀s. ⟦ ¶''invar-post''; modifies modset s s⇩0; I s; ¬bval b s ⟧ ⟹ Q s"
    assumes [simp]: "modset = ANALYZE (lhsv π c)"
    shows "wp π (WHILE_annotRVI R v I b c) Q s⇩0"
    using wp_whileI_modset[of "inv_image R v" I, OF _ assms(2)] assms(1,3,4)
    unfolding WHILE_annotRVI_def GOAL_INDICATION_def invar_var_goal_def
    by auto
  
  lemma wp_while_rl_dfltR[vcg_comb_rules]: 
    "wp π (WHILE_annotRVI (measure nat) v I b c) Q s⇩0 ⟹ wp π (WHILE_annotVI v I b c) Q s⇩0"
    unfolding WHILE_annotRVI_def WHILE_annotVI_def
    by auto
    

  lemma wlp_while_rl[vcg_comb_rules]:
    assumes "¶''invar-initial'' ⟹ I s⇩0"
    assumes "⋀s. ⟦ ¶''invar-pres''; modifies modset s s⇩0; I s; bval b s ⟧ ⟹ wlp π c I s"
    assumes "⋀s. ⟦ ¶''invar-post''; modifies modset s s⇩0; I s; ¬bval b s ⟧ ⟹ Q s"
    assumes [simp]: "modset = ANALYZE (lhsv π c)"
    shows "wlp π (WHILE_annotI I b c) Q s⇩0"
    using wlp_whileI_modset[of I, OF _ assms(2)] assms(1,3,4)
    unfolding WHILE_annotI_def GOAL_INDICATION_def
    by auto
    
  lemma wlp_if_rl[vcg_comb_rules]:
    assumes "⟦¶''then''; bval b s⟧ ⟹ wlp π c⇩1 Q s"
    assumes "⟦¶''else''; ¬bval b s⟧ ⟹ wlp π c⇩2 Q s"
    shows "wlp π (IF b THEN c⇩1 ELSE c⇩2) Q s"
    using assms unfolding GOAL_INDICATION_def
    by (simp add: wlp_if_eq)
        
  lemma wp_if_rl[vcg_comb_rules]:
    assumes "⟦¶''then''; bval b s⟧ ⟹ wp π c⇩1 Q s"
    assumes "⟦¶''else''; ¬bval b s⟧ ⟹ wp π c⇩2 Q s"
    shows "wp π (IF b THEN c⇩1 ELSE c⇩2) Q s"
    using assms unfolding GOAL_INDICATION_def
    by (simp add: wp_if_eq)

    
  subsection ‹VCG Methods›  
      
  subsubsection ‹Generation›
  
  method i_vcg_step = 
    (rule vcg_comb_rules)
  | ((rule vcg_frame_rules, rule vcg_specs))
  | (simp (no_asm_use) named_ss vcg_bb: )
    
  method i_vcg_gen = (i_vcg_step; i_vcg_gen)?  
    
  method i_vcg_rem_annot = simp named_ss vcg_bb: ANNOTATION_def
  

  subsubsection ‹Postprocessing›
  
  method i_vcg_remove_hints = ((determ ‹thin_tac "modifies _ _ _"›)+)?; i_vcg_remove_renamings_tac
    
  
  text ‹Postprocessing exposes user annotations completely, and then abstracts over variable names.›
  method i_vcg_postprocess =
    i_vcg_modifies_simp?;
    i_vcg_apply_renamings_tac?;
    i_vcg_remove_hints?;
    (unfold BB_PROTECT_def VAR_def)?;
    i_vcg_postprocess_vars

  subsubsection ‹Main Method›    
    
  method vcg = 
    i_vcg_preprocess; 
    i_vcg_gen; 
    i_vcg_rem_annot?; 
    i_vcg_postprocess
    
  method vcg_cs = vcg;(clarsimp?)
  

end