theory EX_SmartCardPurse = SALOverflowFWInst + AuxBox: section {* Smart Card Purse *} text {* This program adds a credit C to a balance B if the new balance B + C does not execeed an upper bound MAX (the highest number the safety policy accepts). To check this condition a procedure is called which sets a flag F to NAT 0 if this condition is violated *} --{* program variables *} constdefs B :: nat -- "balance" "B \ 0" C :: nat -- "credit" "C \ 1" M :: nat -- "maximum" "M \ 2" P :: nat -- "return address storage" "P \ 3" --{* initial values *} constdefs b0 :: nat "b0 \ 4" -- "maximal intial balance" c0 :: nat "c0 \ 2" -- "initial credit" constdefs prog :: "SALprogram" "prog \ [(0, [(SET B b0, None), (SET C c0, None), (CALL P 1, Some (\ (pc,m,e).m B = NAT b0 \ m C = NAT c0)), (ADD B C, Some (\ (pc,m,e). m B = NAT b0 \ (\ c. m C = NAT c \ c = (if (b0 + c0 < MAX) then c0 else 0) ))), (HALT, None) ] ), (1,[(SET M MAX, Some (\ (pc,m,e). m P = RA (incA (\ e)) \ (\ b. m B = NAT b) \ (\ c. m C = NAT c) \ (\ x. x \ P \ m x = (\ e) x) )), (SUB M C, None), (JMPL B M 2, None), (SET C 0, None), (RET P, Some (\ (pc,m,e). (\ x. x\C \ x \ M \ x \ P \ m x = (\ e) x) \ (\ b c c'. m B = NAT b \ m C = NAT c \ (\ e) C = NAT c' \ c = (if (b + c' < MAX) then c' else 0) ))) ] ) ]" (*<*) lemma [code]: "prog = [ (0,[(SET B b0, None), (SET C c0, None), (CALL P 1, Some (term (\ (pc,m,e).m B = NAT b0 \ m C = NAT c0))), (ADD B C, Some (term (\ (pc,m,e). m B = NAT b0 \ (\ c. m C = NAT c \ c = (if (b0 + c0 < MAX) then c0 else 0) )))), (HALT, None)]), (1,[(SET M MAX, Some (term (\ (pc,m,e). m P = RA (incA (\ e)) \ (\ b. m B = NAT b) \ (\ c. m C = NAT c) \ (\ x. x \ P \ m x = (\ e) x)))), (SUB M C, None), (JMPL B M 2, None), (SET C 0, None), (RET P, Some (term (\ (pc,m,e). (\ x. x\C \ x \ M \ x \ P \ m x = (\ e) x) \ (\ b c c'. m B = NAT b \ m C = NAT c \ (\ e) C = NAT c' \ c = (if (b + c' < MAX) then c' else 0) ))))])]" apply (simp add: prog_def term_def to_term_def) done (*>*) subsection {* The Verification Condition *} text {* Generate an ML file vcgSAL.ML that contains an executable VCG and the program source. *} (* use "vcgSAL.ML"; set show_numeral_types; set show_brackets; val vc = vcg prog; val pvc = Pretty.writeln (Sign.pretty_term (sign_of Main.thy) vc); File.write (Path.unpack "pvc.txt") (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) vc)); + delete misprinted brackets for EX + delete misprinted brackets for let \ in *) generate_code ("vcgSAL.ML") [term_of] vcg = "vcgSAL" prg = "prog" text {* This is the output our ML program for the VCG yield for this example (copy and paste). *} constdefs vc :: SALform "vc \ (%s. (((%s. (((%(pc, m, e). ((pc = ((0::nat), (0::nat))) & (((cs e) = [((0::nat), m)]) & (((h e) = []) & (ALL X. ((m X) = ILLEGAL)))))) s) --> ((%s. (((%(pc, m, e). ((Suc (Suc (Suc (Suc (0::nat))))) <= MAX)) s) & ((%s. (((%s. (((%(pc, m, e). (pc = ((0::nat), (0::nat)))) s) --> ((%(pc, m, e). ((%s. (((%(pc, m, e). ((Suc (Suc (0::nat))) <= MAX)) s) & ((%s. (((%s. (((%(pc, m, e). (pc = ((0::nat), (Suc (0::nat))))) s) --> ((%(pc, m, e). ((%s. (((%s. True) s) & ((%s. (((%(pc, m, e). (((m B) = (NAT b0)) & ((m C) = (NAT c0)))) s) & ((%s. True) s))) s))) (((0::nat), (Suc (Suc (0::nat)))), (update m (Suc (0::nat)) (NAT (Suc (Suc (0::nat))))), (h_update ((h e) @ [((0::nat), (Suc (0::nat)))]) e)))) s))) s) & ((%s. True) s))) s))) (((0::nat), (Suc (0::nat))), (update m (0::nat) (NAT (Suc (Suc (Suc (Suc (0::nat))))))), (h_update ((h e) @ [((0::nat), (0::nat))]) e)))) s))) s) & ((%s. True) s))) s))) s))) s) & ((%s. (((%s. (((%s. (((%s. (((%s. (((%s. True) s) & ((%s. (((%(pc, m, e). (((m B) = (NAT b0)) & ((m C) = (NAT c0)))) s) & ((%s. True) s))) s))) s) & ((%s. (((%(pc, m, e). (pc = ((0::nat), (Suc (Suc (0::nat)))))) s) & ((%s. True) s))) s))) s) --> ((%(pc, m, e). ((%s. (((%(pc, m, e). ((Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (0::nat)))))))))))))))) <= MAX)) s) & ((%s. (((%(pc, m, e). (((m P) = (RA (incA (callpc e)))) & ((EX b. ((m B) = (NAT b))) & ((EX c. ((m C) = (NAT c))) & (ALL x. ((x ~= P) --> ((m x) = (callmem e x)))))))) s) & ((%s. True) s))) s))) (((Suc (0::nat)), (0::nat)), (update m (Suc (Suc (Suc (0::nat)))) (RA ((0::nat), (Suc (Suc (Suc (0::nat))))))), (cs_update (((length (h e)), m) # (cs e)) (h_update ((h e) @ [((0::nat), (Suc (Suc (0::nat))))]) e))))) s))) s) & ((%s. True) s))) s) & ((%s. (((%s. (((%s. (((%s. (((%s. (((%(pc, m, e). ((EX n. ((m (0::nat)) = (NAT n))) & ((EX n. ((m (Suc (0::nat))) = (NAT n))) & (EX n. (((lift op + (m (0::nat)) (m (Suc (0::nat)))) = (NAT n)) & (n <= MAX)))))) s) & ((%s. (((%(pc, m, e). (((m B) = (NAT b0)) & (EX c. (((m C) = (NAT c)) & (c = (if ((b0 + c0) < MAX) then c0 else (0::nat))))))) s) & ((%s. True) s))) s))) s) & ((%s. (((%(pc, m, e). (pc = ((0::nat), (Suc (Suc (Suc (0::nat))))))) s) & ((%s. True) s))) s))) s) --> ((%(pc, m, e). ((%s. (((%s. True) s) & ((%s. True) s))) (((0::nat), (Suc (Suc (Suc (Suc (0::nat)))))), (update m (0::nat) (lift op + (m (0::nat)) (m (Suc (0::nat))))), (h_update ((h e) @ [((0::nat), (Suc (Suc (Suc (0::nat)))))]) e)))) s))) s) & ((%s. True) s))) s) & ((%s. (((%s. (((%s. (((%s. (((%s. (((%(pc, m, e). ((Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (0::nat)))))))))))))))) <= MAX)) s) & ((%s. (((%(pc, m, e). (((m P) = (RA (incA (callpc e)))) & ((EX b. ((m B) = (NAT b))) & ((EX c. ((m C) = (NAT c))) & (ALL x. ((x ~= P) --> ((m x) = (callmem e x)))))))) s) & ((%s. True) s))) s))) s) & ((%s. (((%(pc, m, e). (pc = ((Suc (0::nat)), (0::nat)))) s) & ((%s. True) s))) s))) s) --> ((%(pc, m, e). ((%s. (((%(pc, m, e). ((EX n. ((m (Suc (Suc (0::nat)))) = (NAT n))) & (EX n. ((m (Suc (0::nat))) = (NAT n))))) s) & ((%s. (((%s. (((%(pc, m, e). (pc = ((Suc (0::nat)), (Suc (0::nat))))) s) --> ((%(pc, m, e). ((%s. (((%(pc, m, e). ((EX n. ((m (0::nat)) = (NAT n))) & (EX n. ((m (Suc (Suc (0::nat)))) = (NAT n))))) s) & ((%s. (((%s. (((%(pc, m, e). ((EX n n'. (((m (0::nat)) = (NAT n)) & (((m (Suc (Suc (0::nat)))) = (NAT n')) & (n < n')))) & (pc = ((Suc (0::nat)), (Suc (Suc (0::nat))))))) s) --> ((%(pc, m, e). ((%s. (((%(pc, m, e). (EX pn' i'. (((m (Suc (Suc (Suc (0::nat))))) = (RA (pn', (Suc i')))) & (EX k m' cl css. (((cs e) = ((k, m') # (cl # css))) & ((pn', i') = ((h e) ! k))))))) s) & ((%s. (((%(pc, m, e). ((ALL x. (((x ~= C) & ((x ~= M) & (x ~= P))) --> ((m x) = (callmem e x)))) & (EX b c c'. (((m B) = (NAT b)) & (((m C) = (NAT c)) & (((callmem e C) = (NAT c')) & (c = (if ((b + c') < MAX) then c' else (0::nat))))))))) s) & ((%s. True) s))) s))) (((Suc (0::nat)), (Suc (Suc (Suc (Suc (0::nat)))))), m, (h_update ((h e) @ [((Suc (0::nat)), (Suc (Suc (0::nat))))]) e)))) s))) s) & ((%s. (((%s. (((%(pc, m, e). ((EX n n'. (((m (0::nat)) = (NAT n)) & (((m (Suc (Suc (0::nat)))) = (NAT n')) & (~ (n < n'))))) & (pc = ((Suc (0::nat)), (Suc (Suc (0::nat))))))) s) --> ((%(pc, m, e). ((%s. (((%(pc, m, e). ((0::nat) <= MAX)) s) & ((%s. (((%s. (((%(pc, m, e). (pc = ((Suc (0::nat)), (Suc (Suc (Suc (0::nat))))))) s) --> ((%(pc, m, e). ((%s. (((%(pc, m, e). (EX pn' i'. (((m (Suc (Suc (Suc (0::nat))))) = (RA (pn', (Suc i')))) & (EX k m' cl css. (((cs e) = ((k, m') # (cl # css))) & ((pn', i') = ((h e) ! k))))))) s) & ((%s. (((%(pc, m, e). ((ALL x. (((x ~= C) & ((x ~= M) & (x ~= P))) --> ((m x) = (callmem e x)))) & (EX b c c'. (((m B) = (NAT b)) & (((m C) = (NAT c)) & (((callmem e C) = (NAT c')) & (c = (if ((b + c') < MAX) then c' else (0::nat))))))))) s) & ((%s. True) s))) s))) (((Suc (0::nat)), (Suc (Suc (Suc (Suc (0::nat)))))), (update m (Suc (0::nat)) (NAT (0::nat))), (h_update ((h e) @ [((Suc (0::nat)), (Suc (Suc (Suc (0::nat)))))]) e)))) s))) s) & ((%s. True) s))) s))) (((Suc (0::nat)), (Suc (Suc (Suc (0::nat))))), m, (h_update ((h e) @ [((Suc (0::nat)), (Suc (Suc (0::nat))))]) e)))) s))) s) & ((%s. True) s))) s))) s))) (((Suc (0::nat)), (Suc (Suc (0::nat)))), (update m (Suc (Suc (0::nat))) (lift op - (m (Suc (Suc (0::nat)))) (m (Suc (0::nat))))), (h_update ((h e) @ [((Suc (0::nat)), (Suc (0::nat)))]) e)))) s))) s) & ((%s. True) s))) s))) (((Suc (0::nat)), (Suc (0::nat))), (update m (Suc (Suc (0::nat))) (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (0::nat)))))))))))))))))), (h_update ((h e) @ [((Suc (0::nat)), (0::nat))]) e)))) s))) s) & ((%s. True) s))) s) & ((%s. (((%s. (((%s. (((%s. (((%s. (((%(pc, m, e). (EX pn' i'. (((m (Suc (Suc (Suc (0::nat))))) = (RA (pn', (Suc i')))) & (EX k m' cl css. (((cs e) = ((k, m') # (cl # css))) & ((pn', i') = ((h e) ! k))))))) s) & ((%s. (((%(pc, m, e). ((ALL x. (((x ~= C) & ((x ~= M) & (x ~= P))) --> ((m x) = (callmem e x)))) & (EX b c c'. (((m B) = (NAT b)) & (((m C) = (NAT c)) & (((callmem e C) = (NAT c')) & (c = (if ((b + c') < MAX) then c' else (0::nat))))))))) s) & ((%s. True) s))) s))) s) & ((%s. (((%s. (((%(pc, m, e). (((m (Suc (Suc (Suc (0::nat))))) = (RA ((0::nat), (Suc (Suc (Suc (0::nat))))))) & (pc = ((Suc (0::nat)), (Suc (Suc (Suc (Suc (0::nat))))))))) s) & ((%s. (((%(pc, m, e). ((%(pc, m, e). (((m B) = (NAT b0)) & ((m C) = (NAT c0)))) (let (k, m') = (hd (cs e)); cs' = (tl (cs e)); h' = (take k (h e)) in (((h e) ! k), m', (h_update h' (cs_update cs' e)))))) s) & ((%s. True) s))) s))) s) & ((%s. True) s))) s))) s) --> ((%(pc, m, e). ((%s. (((%(pc, m, e). ((EX n. ((m (0::nat)) = (NAT n))) & ((EX n. ((m (Suc (0::nat))) = (NAT n))) & (EX n. (((lift op + (m (0::nat)) (m (Suc (0::nat)))) = (NAT n)) & (n <= MAX)))))) s) & ((%s. (((%(pc, m, e). (((m B) = (NAT b0)) & (EX c. (((m C) = (NAT c)) & (c = (if ((b0 + c0) < MAX) then c0 else (0::nat))))))) s) & ((%s. True) s))) s))) (((0::nat), (Suc (Suc (Suc (0::nat))))), m, (cs_update (tl (cs e)) (h_update ((h e) @ [((Suc (0::nat)), (Suc (Suc (Suc (Suc (0::nat))))))]) e))))) s))) s) & ((%s. True) s))) s) & ((%s. True) s))) s))) s))) s))) s)))" lemma domC_prog:"domC prog = [(0,0),(0,1),(0,2),(0,3),(0,4),(1,0),(1,1),(1,2),(1,3),(1,4)]" apply (simp add: domC.simps prog_def Let_def fst_conv snd_conv) done lemma anF_prog:"domA prog = [(0,2),(0,3),(1,0),(1,4)]" apply (simp only: domA_def domC_prog) apply (simp add: anF.simps prog_def noProc.simps Let_def fst_conv snd_conv split_def filter.simps) done subsection {* Program Verification *} text {* First we ensure that the program is wellformed. *} lemma wf_prog: "wf prog" apply (simp add: wf_def checkPos.simps prog_def Let_def split_def fst_conv snd_conv cmd.simps domC.simps ret_succs.simps callpoints_def isCall_def anF.simps) done text {* Then, we prove the verification condition *} (*<*) lemma env_simp: "e\h:=a,h:=b\ = e\h:=b\" apply simp done (*>*) lemmas vc_simps [simp] = nat_number split_def Let_def fst_conv snd_conv B_def MAX_def b0_def C_def c0_def M_def P_def update_def fun_upd_apply callpc_def callmem_def callenv_def incA_def nth_append lift_def text {* Automated Proof *} lemma vc_prog_holds: "provable prog vc" --{* start up *} apply (simp add: provable_def valid_def | rule allI | rule impI)+ apply (cut_tac wf_prog, drule vc_proof_startup,assumption, (erule conjE | erule exE)+) apply (simp only: vc_def) (* txt {* \newpage the vc:\\ @{subgoals [display, indent=0, margin=100]} *} *) --{* main proof *} apply auto apply arith apply arith done text {* Manually Guided Proof *} declare vc_simps [simp del] lemma vc_prog_holds2: "provable prog vc" --{* start up *} apply (simp add: provable_def valid_def | rule allI | rule impI)+ apply (rename_tac pn i m e) apply (cut_tac wf_prog) apply (drule vc_proof_startup) apply assumption apply (erule conjE | erule exE)+ apply (simp only: vc_def) (* txt {* \newpage @{subgoals [display, indent=0, margin=100]} *} *) --{* main proof *} apply (case_tac "prog,((pn,i),m,e) \ (initF prog)") apply (simp add: initF_def valid_def B_def MAX_def b0_def C_def c0_def update_def fun_upd_apply) --{* case: not initF *} apply (erule isafeP_elims) apply (simp only: simp_thms fst_conv snd_conv) --{* now we know that ((pn,i),m,e) is inductively safe *} apply (drule_tac t="s''" in sym) apply (rule conjI) --{* (initF prg) implies (isafeF prg (ipc prg)) *} apply (simp add: MAX_def c0_def b0_def B_def C_def update_def fun_upd_apply) apply (rule conjI) --{* (0,2) nach (1,0), prozedureinsprung *} apply (simp add: MAX_def c0_def b0_def B_def C_def P_def update_def fun_upd_apply callpc_def callmem_def nth_append incA_def fst_conv snd_conv) apply (rule conjI) --{* (0,3) nach (0,4), programmende *} apply (simp add: fst_def) apply (rule conjI) --{* (1,0) nach (1,4), prozedurbody, zwei wege *} apply (simp add: fst_conv snd_conv MAX_def c0_def b0_def B_def C_def P_def M_def update_def fun_upd_apply) apply (rule impI)+ apply (erule conjE | erule exE)+ apply (case_tac "css") apply (simp add: Let_def split_def fst_conv snd_conv) --{* case: css = a list *} apply (simp add: Let_def split_def fst_conv snd_conv lift_def callpc_def del: sysinv.simps sysinv2.simps) apply (rule conjI) --{* Fall: Sprungbedingung gilt *} apply (rule impI) apply (rule conjI) apply (rule_tac x="fst (h e ! fst c)" in exI) apply (rule_tac x="snd (h e ! fst c)" in exI) apply (simp add: incA_def split_def nat_number Let_def fst_conv snd_conv) apply (rule_tac x="fst c" in exI) apply (erule conjE)+ apply (simp add: nth_append) apply (rule_tac x="snd c" in exI) apply simp apply (rule conjI) apply (rule allI) apply (rule impI) apply (erule_tac x="x" in allE) apply (simp add: callmem_def) apply (rule_tac x="ca" in exI) apply (simp add: callmem_def) apply (subgoal_tac "(b + ca < MAX) = (b < MAX - ca)") prefer 2 apply (rule sym) apply (rule less_diff_conv) apply (simp add: nat_number MAX_def) --{* Sprungbedingung gilt nicht *} apply (rule impI) apply (rule conjI) apply (rule_tac x="fst (h e ! fst c)" in exI) apply (rule_tac x="snd (h e ! fst c)" in exI) apply (simp add: incA_def split_def nat_number Let_def fst_conv snd_conv) apply (rule_tac x="fst c" in exI) apply (erule conjE)+ apply (simp add: nth_append) apply (rule_tac x="snd c" in exI) apply simp apply (rule conjI) apply (rule allI) apply (rule impI) apply (erule_tac x="x" in allE) apply (simp add: callmem_def) apply (rule_tac x="ca" in exI) apply (simp add: callmem_def) apply (subgoal_tac "(b + ca < MAX) = (b < MAX - ca)") prefer 2 apply (rule sym) apply (rule less_diff_conv) apply (simp add: nat_number MAX_def) --{* (1,4) nach (0,3); prozeduraussprung *} apply (simp add: MAX_def c0_def b0_def B_def C_def P_def M_def update_def fun_upd_apply) apply (rule impI)+ apply (erule conjE | erule exE)+ apply (simp add: Let_def split_def fst_conv snd_conv lift_def callmem_def) --{* nprfsize() = 245.170 *} done end