theory EX_MainSum =  VCGExec:

section {* Definitions *}

subsection {* Name Declarations *}

constdefs
 this::nat
 "this \<equiv> 0"
 k::nat
 "k\<equiv>1"
 n::nat
 "n \<equiv> 2"
 res::nat
 "res\<equiv>3"

subsection {* Program Code *}

consts comment ::"instr \<Rightarrow> string \<Rightarrow> instr" ("(_ -- _)" [61,60] 60)
defs comment_def [simp]:
"comment i s \<equiv> i"

constdefs
 StartC :: "int \<Rightarrow> jvm_method cdecl"
 "StartC arg \<equiv> (Start,(Object, [],[(main,[],Integer,(2,4,[
 Push (Intg arg),
 Store n,
 Push (Intg 0),
 Store k,
 Push (Intg 0),
 Store res,
 Load k,
 Load n,
 IfIntLeq 10 -- ''if n <= k then terminate else k++; res+=k'' ,
 Load k,
 Push (Intg 1),
 IAdd,
 Store k,
 Load k,
 Load res,
 IAdd,
 Store res,
 Goto (-11),
 Load res,
 Return -- ''main_ret''],
 []))]))"

section {* Prove safety using hand-made annotations. *}

subsection {* Annotations *}

constdefs 
n0::"int"
"n0 \<equiv> 5"

constdefs
 sum_inv::"expr"
 "sum_inv \<equiv> And [Ty (Rg k) Integer, Ty (Rg res) Integer, 
  Ty (Rg n) Integer, 
  ((Cn (Intg 2)) \<otimes> (Rg res)) \<doteq> (Rg k \<otimes> (Rg k \<oplus> (Cn (Intg 1)))), 
  (Cn (Intg 0)) \<preceq> Rg k, (Rg k) \<preceq> Rg n, 
  Rg n \<doteq> Cn (Intg n0)]"

subsection {* Packing code and annotations *}

constdefs
prog::"jbc_prog"
"prog \<equiv> (SystemClasses @ [StartC n0],
 [((Start,main,6),sum_inv)])"

subsection {* Generate ML code for the VCG *}

(* Turn off longnames! *)

generate_code ("EX_Sum.ML") [term_of]
  wf_jvm_prog_phi = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phi \<Phi> P"
  wf = "wf"
  opt = "opt"
  vcg = "vcgTy"
  prog = "prog"


  (* If a program is not wellformed, the following
     functions help to find out why. *)
  
  phi_prog = "map_of2 (convert_pt (prog_kil (fst prog)))"
  wfS = "wfS"
  wf_jvm_prog_phiS = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phiS \<Phi> P"
  initjob = "initjob (fst prog) Start ''main''"
  nxtjob = "nxtjob  (fst prog) Start ''main''"
  printjob = "\<lambda> job. printjob (fst prog) Start ''main'' job"
  parsejob = "parsejob"

subsection {* Verification Condition *}

 
ML {* use "EX_Sum.ML" *}
ML {* wf prog; *}
ML {* val vc = opt (vcg prog); *}
ML {* val pvc = (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_expr vc))); *}

--{* now we trasfer the ML result back to Isabelle *}
ML_setup {*
val t = term_of_expr vc;
val T = fastype_of t;
Context.>> (fn thy => thy |>
  Theory.add_consts_i [("vc", T, NoSyn)] |>
  (fst o PureThy.add_defs_i false [(("vc_def", Logic.mk_equals (Const ("EX_MainSum.vc", T), t)), [])]));
*}

--{* the verification condition is now defined as constant vc::expr *}



subsection {* Proving the Verification Condition *}

text {* Here we prove the vc (via the semantics of formulae). The evaluation simpset from VCGexec.thy is tuned for this
        purpose. Some of the evaluation rules (evalEevalEs.simps) are ommitted, because
        this keeps the expansion overhead small.\\[1ex] *}

text {* The following lemma is used for the verification of the example. Alternatively
        one could use a tactic for bounded arithemtics. *}
lemma special_bounded_mult: "\<lbrakk> 2 * a = b * (b+1); b < (5::int); 0 \<le> b \<rbrakk> \<Longrightarrow>  b + a \<le> 14"
(*<*)
 apply (rule_tac c="2" in mult_left_le_imp_le)
 apply (simp add: zadd_zmult_distrib2)
 apply (subgoal_tac "3 * b \<le> 12")
  prefer 2
  apply arith
 apply (subgoal_tac "b * b \<le> 16")
  prefer 2
  apply (subgoal_tac "b * b \<le> b * 4")
   prefer 2
   apply (rule_tac c="b" in mult_left_mono)
   apply simp
   apply simp
  apply (subgoal_tac "b * 4 \<le> 4 * 4")
   prefer 2
   apply (rule_tac c="4" in mult_right_mono)
   apply simp
   apply simp
  apply simp
 apply simp
apply simp
--{* nprfsize = 55757 *}
done 
(*>*)


text {* short proof\\[1ex]*}


lemma vcg_prog_holds:
"prog \<turnstile> vc"
apply (simp only: provable_def vc_def)
apply (safe intro!: And0 AndI')
apply (simp only: deriv_def, rule ballI, clarsimp simp del: evalE_evalEs.simps simp add: sem_simps |
       drule special_bounded_mult, arith, assumption+, simp del: evalE_evalEs.simps add:  zadd_zmult_distrib zadd_zmult_distrib2 )+
done

text {* more explicit proof\\[1ex] *}

lemma vcg_prog_holds2:
"prog \<turnstile> vc"
apply (simp only: provable_def vc_def)
apply (safe intro!: And0 AndI')
--{* We get an initial condition and one condition for edge going out of an annotated position. *}
--{* Initial Condition: initF implies isafeF prog (ipc prog) *}
apply (simp only: deriv_def)
apply (rule ballI)
apply (clarsimp simp del: evalE_evalEs.simps simp add: sem_simps)

--{* (Start,main,6) nach (Start,main,6) oder (Start,main,19) *} 
--{* main challenge: arithmetical condition *}
apply (drule special_bounded_mult)
apply (simp del: evalE_evalEs.simps add:  zadd_zmult_distrib zadd_zmult_distrib2 )+
done

--{* \clearpage *}

section {* Verify program using interval annotations. \\[1ex]*}

subsection {* Annotations *}

constdefs 
n2::"int"
"n2 \<equiv> 4"

constdefs 
res2::"int"
"res2 \<equiv> 2147418112"

constdefs
 sum_inv2::"expr"
 "sum_inv2 \<equiv> And [Ty (Rg k) Integer, Ty (Rg res) Integer, 
  Ty (Rg n) Integer, 
  (Cn (Intg 0)) \<preceq> Rg res, (Rg res) \<preceq> Cn (Intg res2),
  (Cn (Intg 0)) \<preceq> Rg k, (Rg k) \<preceq> Cn (Intg n2), 
  Rg n \<doteq> Cn (Intg n2)]"

subsection {* Packing code and annotations *}

constdefs
prog2::"jbc_prog"
"prog2 \<equiv> (SystemClasses @ [StartC n2],
 [((Start,main,6),sum_inv2)])"

text {* Note, that suminv2 is the strongest intervall annotation. *}

subsection {* Generate ML code for the VCG *}


subsection {* Generate ML code for the VCG *}

generate_code ("EX_Sum.ML") [term_of]
  wf_jvm_prog_phi = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phi \<Phi> P"
  wf = "wf"
  opt = "opt"
  vcg = "vcgTy"
  prog = "prog2"


  (* If a program is not wellformed, the following
     functions help to find out why. *)
  
  phi_prog = "map_of2 (convert_pt (prog_kil (fst prog)))"
  wfS = "wfS"
  wf_jvm_prog_phiS = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phiS \<Phi> P"
  initjob = "initjob (fst prog) Start ''main''"
  nxtjob = "nxtjob  (fst prog) Start ''main''"
  printjob = "\<lambda> job. printjob (fst prog) Start ''main'' job"
  parsejob = "parsejob"

subsection {* Verification Condition *}

ML {* use "EX_Sum.ML" *}
ML {* wf prog; *}
ML {* val vc2 = opt (vcg prog); *}
ML {* val pvc = (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_expr vc2))); *}

--{* now we trasfer the ML result back to Isabelle *}
ML_setup {*
val t = term_of_expr vc2;
val T = fastype_of t;
Context.>> (fn thy => thy |>
  Theory.add_consts_i [("vc2", T, NoSyn)] |>
  (fst o PureThy.add_defs_i false [(("vc2_def", Logic.mk_equals (Const ("EX_MainSum.vc2", T), t)), [])]));
*}

--{* the verification condition is now defined as constant vc2::expr *}

lemma vcg_prog2_holds:
"prog2 \<turnstile> vc2"
apply (simp only: provable_def vc2_def)
apply (safe intro!: And0 AndI')
apply (simp only: deriv_def, rule ballI, clarsimp simp del: evalE_evalEs.simps simp add: sem_simps)
--{* problem: annotation is not inductive! *}
txt {* @{subgoals [display, indent=0, margin=90]} *}
oops

text {* Verification fails because suminv2 is not inductive! *}

constdefs
 sum_inv2I::"expr"
 "sum_inv2I \<equiv> And [Ty (Rg k) Integer, Ty (Rg res) Integer, 
  Ty (Rg n) Integer, 
  Cn (Intg 0) \<preceq> Rg res, Rg res \<preceq> ((Cn MX) \<ominus> (Rg k \<oplus> Cn (Intg 1))),
  Cn (Intg 0) \<preceq> Rg k, Rg k \<preceq> Cn (Intg n2), 
  Rg n \<doteq> Cn (Intg n2)]"

subsection {* Packing code and annotations *}

constdefs
prog2'::"jbc_prog"
"prog2' \<equiv> (SystemClasses @ [StartC n2],
 [((Start,main,6),sum_inv2I)])"

subsection {* Generate ML code for the VCG *}

subsection {* Generate ML code for the VCG *}

generate_code ("EX_Sum.ML") [term_of]
  wf_jvm_prog_phi = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phi \<Phi> P"
  wf = "wf"
  opt = "opt"
  vcg = "vcgTy"
  prog = "prog2'"


  (* If a program is not wellformed, the following
     functions help to find out why. *)
  
  phi_prog = "map_of2 (convert_pt (prog_kil (fst prog)))"
  wfS = "wfS"
  wf_jvm_prog_phiS = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phiS \<Phi> P"
  initjob = "initjob (fst prog) Start ''main''"
  nxtjob = "nxtjob  (fst prog) Start ''main''"
  printjob = "\<lambda> job. printjob (fst prog) Start ''main'' job"
  parsejob = "parsejob"

subsection {* Verification Condition *}

ML {* use "EX_Sum.ML" *}
ML {* wf prog; *}
ML {* val vc2' = opt (vcg prog); *}
ML {* val pvc = (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_expr vc2'))); *}

--{* now we trasfer the ML result back to Isabelle *}
ML_setup {*
val t = term_of_expr vc2';
val T = fastype_of t;
Context.>> (fn thy => thy |>
  Theory.add_consts_i [("vc2'", T, NoSyn)] |>
  (fst o PureThy.add_defs_i false [(("vc2'_def", Logic.mk_equals (Const ("EX_MainSum.vc2'", T), t)), [])]));
*}

lemma vcg_prog2'_holds:
"prog2' \<turnstile> vc2'"
apply (simp only: provable_def vc2'_def)
apply (safe intro!: And0 AndI')
apply (simp only: deriv_def, rule ballI, clarsimp simp del: evalE_evalEs.simps simp add: sem_simps)
--{* problem: annotation is not inductive! *}
txt {* @{subgoals [display, indent=0, margin=90]} *}
oops

--{* Fails again. No linear invariant seems to be sufficient. *}

--{* \clearpage *}
section {* Verify robust program using intervals. \\[1ex] *}



constdefs
 StartCR :: "int \<Rightarrow> jvm_method cdecl"
 "StartCR arg \<equiv> (Start,(Object, [],[
(main,[],Integer,(2,4,[
 Push (Intg arg),
 Store n,
 Push (Intg 0),
 Store res,
 Push (Intg 0),
 Store k,
 Load k -- ''LOOP: suminv3'', 
 Load n,
 IfIntLeq 13 -- ''if n <= k then terminate else k++; res+=k'' ,
 Load res,
 Push (Intg 2147418113) --  ''2147418112 is the maximum value res can have at this position without causing an overflow'',
 IfIntLeq 10,
 Load k -- ''k: [0,arg], res:[0,2147418112]'',
 Push (Intg 1),
 IAdd,
 Store k,
 Load k,
 Load res,
 IAdd,
 Store res,
 Goto (-14) -- ''goto LOOP'',
 Load res,
 Return -- ''main_ret''],
 []))]))"

constdefs 
n3::"int"
"n3 \<equiv> 65535"

constdefs
 sum_inv3::"expr"
 "sum_inv3 \<equiv> And [Ty (Rg k) Integer, Ty (Rg res) Integer, 
  Ty (Rg n) Integer, 
  (Cn (Intg 0)) \<preceq> Rg res, (Rg res) \<preceq> Cn (Intg MAX),
  (Cn (Intg 0)) \<preceq> Rg k, (Rg k) \<preceq> (Cn (Intg 65535)), 
  Rg n \<preceq> Cn (Intg 65535)]"

subsection {* Packing code and annotations *}

constdefs
prog3::"jbc_prog"
"prog3 \<equiv> (SystemClasses @ [StartCR n3],
 [((Start,main,6),sum_inv3)])"

subsection {* Generate ML code for the VCG *}

generate_code ("EX_Sum.ML") [term_of]
  wf_jvm_prog_phi = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phi \<Phi> P"
  wf = "wf"
  opt = "opt"
  vcg = "vcgTy"
  prog = "prog3"


  (* If a program is not wellformed, the following
     functions help to find out why. *)
  
  phi_prog = "map_of2 (convert_pt (prog_kil (fst prog)))"
  wfS = "wfS"
  wf_jvm_prog_phiS = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phiS \<Phi> P"
  initjob = "initjob (fst prog) Start ''main''"
  nxtjob = "nxtjob  (fst prog) Start ''main''"
  printjob = "\<lambda> job. printjob (fst prog) Start ''main'' job"
  parsejob = "parsejob"

subsection {* Verification Condition *}

ML {* use "EX_Sum.ML" *}
ML {* wf prog; *}
ML {* val vc3 = opt (vcg prog); *}
ML {* val pvc = (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_expr vc3))); *}

--{* now we trasfer the ML result back to Isabelle *}
ML_setup {*
val t = term_of_expr vc3;
val T = fastype_of t;
Context.>> (fn thy => thy |>
  Theory.add_consts_i [("vc3", T, NoSyn)] |>
  (fst o PureThy.add_defs_i false [(("vc3_def", Logic.mk_equals (Const ("EX_MainSum.vc3", T), t)), [])]));
*}

lemma vcg_prog3_holds:
"prog3 \<turnstile> vc3"
apply (simp only: provable_def vc3_def)
apply (safe intro!: And0 AndI')
apply (simp only: deriv_def, rule ballI, clarsimp simp del: evalE_evalEs.simps simp add: sem_simps)
done


end