Changeset 2604 for src/ERTLptr/ERTLtoERTLptrOK.ma
 Timestamp:
 Feb 5, 2013, 10:49:42 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLtoERTLptrOK.ma
r2601 r2604 20 20 include "common/ExtraMonads.ma". 21 21 22 axiom getLocalsFromId : ident → list register.23 24 22 definition ERTL_status ≝ 25 23 λprog : ertl_program.λstack_sizes. … … 30 28 joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes). 31 29 32 definition sigma_map ≝ λ prog : ertlptr_program. 33 joint_closed_internal_function ERTLptr (prog_var_names … prog) → label → option label. 30 definition sigma_map ≝ λ prog : ertl_program. 31 joint_closed_internal_function ERTL (prog_var_names … prog) → label → option label. 32 34 33 35 34 definition sigma_pc_opt : 36 ∀ prog : ertl ptr_program.35 ∀ prog : ertl_program. 37 36 sigma_map prog → program_counter → option program_counter ≝ 38 37 λprog,sigma,pc. … … 52 51 53 52 definition sigma_beval : 54 ∀prog : ertl ptr_program.53 ∀prog : ertl_program. 55 54 sigma_map prog → 56 55 beval → beval ≝ … … 69 68 *) 70 69 definition sigma_is : 71 ∀prog : ertl ptr_program.70 ∀prog : ertl_program. 72 71 sigma_map prog → 73 72 internal_stack → internal_stack ≝ … … 129 128 130 129 definition sigma_mem : 131 ∀prog : ertl ptr_program . sigma_map prog → bemem → bemem ≝130 ∀prog : ertl_program . sigma_map prog → bemem → bemem ≝ 132 131 λprog,sigma,m. 133 132 mk_mem … … 727 726 map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v). 728 727 #tag #A #B #f * #m * #id #v normalize @eq_f lapply v v lapply id id elim m 729 [ #id elim id [#v %] #x #IH #id normalize >IH % 730  #opt_a #l #r #Hl #Hr * [2,3: #x #v normalize @eq_f2 %] #v normalize @eq_f2 731 try % [@Hr@Hl] 728 [ #id elim id [#v %] #x #IH #id normalize >IH normalize inversion(pm_set ? ? ? ?) 729 normalize // cases x normalize [2,3,5,6: #y] #EQ destruct 730  #opt_a #l #r #Hl #Hr * [2,3: #x #v normalize cases opt_a normalize [2: #a %] 731 cases (map_opt ? ? ? l) normalize [2: //] cases (map_opt ? ? ? r) normalize 732 //] #v normalize cases opt_a [2,4: #a] normalize // 733 [ cases(map_opt ? ? ? l) normalize // >Hr cases(map_opt ? ? ? r) normalize 734 [2: #opt_b #lb #rb] inversion(pm_set B x ? ?) normalize // cases x [2,3,5,6: #y] 735 normalize #EQ destruct 736  >Hl cases(map_opt ? ? ? l) normalize [2: #opt_b #lb #rb] 737 inversion (pm_set B x ? ?) normalize // 738 [1,2: cases x [2,3,5,6: #y] normalize #EQ destruct] 739 #opt_b' #lb' #rb' #_ normalize #_ #EQ cases(map_opt ? ? ? r) 740 normalize nodelta [%] #opt_b'' #lb'' #rb'' >EQ % 732 741 ] 733 742 qed. … … 775 784 776 785 definition sigma_register_env : 777 ∀prog : ertl ptr_program.∀sigma : (sigma_map prog).786 ∀prog : ertl_program.∀sigma : (sigma_map prog). 778 787 register_env beval → list register → register_env beval ≝ 779 788 λprog,sigma,psd_env,ids. 780 789 let m' ≝ map ??? psd_env (λbv.sigma_beval prog sigma bv) in 781 m' ∩ids.790 m' ∖ ids. 782 791 783 792 (* … … 805 814 806 815 816 lemma lookup_set_minus : ∀tag,A,B. ∀a : identifier_map tag A. ∀b : identifier_map tag B. 817 ∀i. lookup ?? (a ∖ b) i = if i ∈ b then None ? else lookup … a i. 818 #tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b) 819 [2: #b] % qed. 820 807 821 (* 808 822 lemma clean_add : ∀tag,A,m,i,v.clean … (add tag A m i v) = add tag A (clean … m) i v. … … 938 952 lemma merge_eq : ∀A.∀p : positive_map A.∀choice. merge 939 953 *) 954 (* 940 955 lemma add_restrict : ∀tag,A,B.∀a : identifier_map tag A. ∀b : identifier_map tag B. 941 956 ∀i,v.i∈b → add tag A (a ∩ b) i v = (add tag A a i v) ∩ b. … … 980 995 whd in ⊢ (??%%); @eq_f @add_restrict assumption 981 996 qed. 982 983 definition sigma_frames : ∀prog : ertlptr_program.sigma_map prog → 984 list (register_env beval × ident) → list (register_env beval × ident) ≝ 985 λprog,sigma,frms.map ?? 986 (λx.〈sigma_register_env prog sigma (\fst x) (getLocalsFromId (\snd x)),\snd x〉) frms. 997 *) 998 lemma add_set_minus : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B. 999 ∀i,v.¬(i ∈ b) → add tag A (a ∖ b) i v = (add tag A a i v) ∖ b. 1000 #tag #A #B * #a * #b * #i #v @notb_elim @if_elim normalize [#_ *] 1001 @if_elim [2: #_ *] @if_elim [#_ *] inversion(lookup_opt B i b) normalize [2: #x #_ *] 1002 #H * * * * @eq_f lapply H H lapply v v lapply b b lapply a a elim i 1003 [ * 1004 [ * [2: #opt_b #l #r] #v normalize in ⊢ (% → ?); #EQ destruct [2: %] 1005 normalize in ⊢ (??%%); cases (map_opt ??? l) // normalize cases(map_opt ??? r) 1006 normalize // 1007  * [2: #a] #l #r * [2,4: #opt_b #l1 #r1] #v normalize in ⊢ (% → ?); #EQ destruct 1008 normalize [3: % 1,2: cases(merge ???? l l1) // cases(merge ???? r r1) //] 1009 cases(map_opt ??? l) normalize // cases(map_opt ??? r) // 1010 ] 1011 2,3: #x #IH * [2,4: #opt_a #l #r] * [2,4,6,8: #opt_b #l1 #r1] #v 1012 normalize in ⊢ (% → ?); #H whd in match (pm_set ????) in ⊢ (???%); 1013 whd in match (merge ??????) in ⊢ (???%); 1014 [1,2,3,4: <IH try assumption whd in match (pm_set ????) in ⊢ (??%?); 1015 whd in match (merge ??????) in ⊢ (??%?); cases opt_b normalize 1016 [2,4,6,8: #b] [5,6: cases opt_a normalize //] 1017 [1,2,3,4: cases (merge ???? l l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] 1018 // cases (merge ???? r r1) normalize 1019 [2,4,6,8,10,12: #opt_a3 #l3 #r3] inversion(pm_set ????) 1020 normalize // cases x 1021 [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y] 1022 normalize #EQ destruct 1023 *: cases(map_opt ??? l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] // 1024 cases(map_opt ??? r1) normalize [2,4,6,8,10,12: #opt_a3 #l3 #r3] 1025 inversion(pm_set ????) normalize // cases x 1026 [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y] 1027 normalize #EQ destruct 1028 ] 1029 *: whd in match (pm_set ????) in ⊢ (??%?); 1030 whd in match (merge ??????) in ⊢ (??%?); [1,2: cases opt_a [2,4: #a]] 1031 normalize 1032 [1,2: @eq_f2 [1,4:%]  cases(map_opt ??? l) [2: #opt_a1 #l1 #r1] normalize 1033  cases(map_opt ??? r) [2: #opt_a1 #l1 #r1] normalize] 1034 [1,3,4: lapply(map_add tag A A (λx.x) (an_id_map … r) (an_identifier ? x) v) 1035 2,5,6: lapply(map_add tag A A (λx.x) (an_id_map … l) (an_identifier ? x) v) 1036 *: lapply(map_add tag A A (λx.x) (an_id_map … (pm_leaf ?)) (an_identifier ? x) v) 1037 ] normalize #EQ destruct >e0 try % [4,5: cases x [2,3,5,6: #y] normalize %] 1038 cases(map_opt ????) [2,4,6: #opt_a1 #l1 #r1] normalize 1039 inversion(pm_set ????) normalize // cases x [2,3,5,6,8,9,11,12: #y] 1040 normalize #EQ1 destruct 1041 ] 1042 ] 1043 qed. 1044 1045 lemma update_set_minus : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B. 1046 ∀i,v.¬(i ∈ b) → update ?? (a ∖ b) i v = 1047 ! a' ← update ?? a i v ; return a' ∖ b. 1048 #tag #A #B #a #b #id #v #H >update_def >lookup_set_minus @if_elim 1049 [ #H1 @⊥ lapply H1 lapply H @notb_elim >H1 normalize *] #_ >update_def 1050 cases (lookup tag A a id) normalize [ %] #a @eq_f @add_set_minus assumption 1051 qed. 1052 1053 1054 record good_state_transformation 1055 (prog : ertl_program) 1056 (def_in : joint_closed_internal_function ERTL (prog_var_names ?? prog)) : 1057 Type[0] ≝ 1058 { f_lbls : label → option (list label) 1059 ; f_regs : label → option (list register) 1060 ; part_partition_f_lbls : partial_partition … f_lbls 1061 ; part_partion_f_regs : partial_partition … f_regs 1062 ; freshness_lab : let def_out ≝ translate_internal … def_in in 1063 (∀l.opt_All … (All … 1064 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 1065 fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) 1066 ; freshness_regs : let def_out ≝ translate_internal … def_in in 1067 (∀l.opt_All … (All … 1068 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 1069 fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) 1070 ; multi_fetch_ok : let def_out ≝ translate_internal … def_in in 1071 ∀f_step,f_fin.∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 1072 ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧ 1073 match s with 1074 [ sequential s' nxt ⇒ 1075 l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out 1076  final s' ⇒ 1077 l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out 1078  FCOND abs _ _ _ ⇒ Ⓧabs 1079 ] 1080 }. 1081 1082 definition get_internal_function_from_ident : 1083 ∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals). 1084 ident → option (joint_closed_internal_function p globals) ≝ 1085 λp,globals,ge,id. 1086 ! bl ← (find_symbol (joint_function p globals) ge id); 1087 ! bl' ← (code_block_of_block bl); 1088 ! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl'); 1089 return fn. 1090 1091 definition get_sigma_from_good_state : 1092 ∀prog : ertl_program. 1093 (∀ fn : joint_closed_internal_function ERTL (prog_var_names ?? prog). 1094 good_state_transformation prog fn) → sigma_map prog ≝ 1095 λprog,good,fn,searched. 1096 !〈res,s〉 ← find ?? (joint_if_code … fn) 1097 (λlbl.λ_. match (f_lbls … (good fn)) lbl with 1098 [None ⇒ false 1099 Some lbls ⇒ 1100 match lbls with 1101 [nil ⇒ eq_identifier … searched lbl 1102 cons hd tl ⇒ let last ≝ last_ne … «hd::tl,I» in 1103 eq_identifier … searched last 1104 ] 1105 ]); 1106 return res. 1107 1108 1109 definition sigma_frames : ∀prog : ertl_program. 1110 (∀fn.good_state_transformation prog fn) → 1111 list (register_env beval × ident) → (list (register_env beval × ident)) ≝ 1112 λprog,good,frms. 1113 let sigma ≝ get_sigma_from_good_state … good in 1114 foldr ?? 1115 (λx,tl.let 〈reg_env,id〉 ≝ x in 1116 match get_internal_function_from_ident 1117 ERTL_semantics (prog_var_names … prog) 1118 (globalenv_noinit … prog) id with 1119 [Some fn ⇒ 1120 〈(sigma_register_env prog sigma reg_env 1121 (added_registers … fn (f_regs … (good fn)))),id〉 :: tl 1122 None ⇒ [ ] 1123 ]) ([ ]) frms. 1124 987 1125 988 1126 (* … … 1018 1156 1019 1157 definition sigma_hw_register_env : 1020 ∀prog: ertl ptr_program. ∀sigma : (sigma_map prog).1158 ∀prog: ertl_program. ∀sigma : (sigma_map prog). 1021 1159 hw_register_env → hw_register_env ≝ 1022 1160 λprog,sigma,h_reg.mk_hw_register_env … … 1025 1163 1026 1164 definition sigma_regs : 1027 ∀prog : ertl ptr_program. ∀sigma : (sigma_map prog).1165 ∀prog : ertl_program. ∀sigma : (sigma_map prog). 1028 1166 (register_env beval)×hw_register_env→ list register → 1029 1167 (register_env beval)×hw_register_env ≝ … … 1069 1207 *) 1070 1208 1071 definition sigma_state : 1072 ∀prog : ertlptr_program. 1073 ∀sigma : sigma_map prog. 1209 definition sigma_state : ∀prog : ertl_program. 1210 (∀fn.good_state_transformation prog fn) → 1074 1211 state ERTLptr_semantics → list register → 1075 1212 state ERTL_semantics ≝ 1076 λprog,sigma,st,ids. 1213 λprog,good,st,ids. 1214 let sigma ≝ get_sigma_from_good_state … good in 1077 1215 mk_state ? 1078 (sigma_frames prog sigma (st_frms …st))1079 (sigma_is progsigma (istack … st))1216 (sigma_frames prog good (st_frms ERTLptr_semantics st)) 1217 (sigma_is ? sigma (istack … st)) 1080 1218 (carry … st) 1081 (sigma_regs prog sigma (regs … st) ids) 1082 (sigma_mem prog sigma (m … st)). 1219 (sigma_regs ? sigma (regs … st) ids) 1220 (sigma_mem ? sigma (m … st)). 1221 1083 1222 1084 1223 definition dummy_state : state ERTL_semantics ≝ … … 1089 1228 mk_state_pc ? dummy_state (null_pc one) (null_pc one). 1090 1229 1091 check fetch_internal_function1092 1093 1230 definition sigma_state_pc : 1094 1231 ∀prog : ertl_program. 1095 let trans_prog ≝ ertl_to_ertlptr prog in 1096 ∀sigma : sigma_map trans_prog. 1232 (∀fn.good_state_transformation prog fn) → 1097 1233 state_pc ERTLptr_semantics → 1098 1234 state_pc ERTL_semantics ≝ 1099 λprog, sigma,st.1100 let trans_prog ≝ ertl_to_ertlptr progin1235 λprog,good,st. 1236 let sigma ≝ get_sigma_from_good_state … good in 1101 1237 let ge ≝ globalenv_noinit … prog in 1102 1238 if eqZb (block_id (pc_block (pc … st))) (1) then (* check for dummy pc *) 1103 1239 dummy_state_pc 1104 1240 else 1105 match 1106 1241 match (fetch_internal_function (joint_closed_internal_function ERTL 1242 (prog_var_names (joint_function ERTL) ℕ prog)) ge (pc_block (pc … st))) with 1107 1243 [OK x ⇒ let 〈i,fd〉 ≝ x in 1108 mk_state_pc ? (sigma_state trans_prog sigma st (joint_if_locals … fd)) 1109 (pc … st) (sigma_stored_pc trans_prog sigma (last_pop … st)) 1244 mk_state_pc ? 1245 (sigma_state prog good st (added_registers … fd (f_regs … (good fd)))) 1246 (pc … st) (sigma_stored_pc prog sigma (last_pop … st)) 1110 1247 Error msg ⇒ dummy_state_pc]. 1111 1248 1112 (*1113 lemma reg_store_sigma_commute :1114 ∀ prog : ertl_program. ∀sigma : (sigma_map prog).1115 ∀id. preserving2 … res_preserve …1116 (sigma_beval prog sigma)1117 (sigma_register_env prog sigma)1118 (sigma_register_env prog sigma)1119 (reg_store id)1120 (reg_store id).1121 #prog #sigma * #id #bv * #psd_env1 #prf1 #prf2 #psd_env21122 whd in match reg_store; whd in match update; normalize nodelta1123 #psd_env2_spec1124 % [ @hide_prf whd in psd_env2_spec : (??%%);1125 inversion (update beval ???) in psd_env2_spec; normalize nodelta1126 [#_ #ABS destruct] #pos_map #pos_map_spec #EQ destruct1127 * #id' #bv' cases (decidable_eq_pos id id')1128 [ #EQ <EQ normalize in ⊢ (??%? → ?);1129 >(update_lookup_opt_same ????? pos_map_spec)1130 #EQ1 destruct(EQ1) assumption1131  #inEQ normalize in ⊢ (??%? → ?);1132 <(update_lookup_opt_other ????? pos_map_spec id' inEQ)1133 @(prf2 (an_identifier ? id') bv')1134 ]1135  whd in match sigma_register_env; normalize nodelta1136 cases(map_update_commute ??????? psd_env2_spec ???)1137 [ #id_present #EQ <EQ %    ]1138 //1139 ]1140 qed.1141 1142 lemma ps_reg_store_commute :1143 ∀prog : ertl_program. ∀sigma : sigma_map prog.1144 ∀id. preserving2 ?? res_preserve …1145 (sigma_beval prog sigma)1146 (sigma_regs prog sigma)1147 (sigma_regs prog sigma)1148 (ps_reg_store id)1149 (ps_reg_store id).1150 #prog #sigma #id #bv * #psd1 #hw1 #prf1 #prf21151 whd in match ps_reg_store; normalize nodelta1152 @mfr_bind [3: @(reg_store_sigma_commute prog sigma id bv ? ? ?) *:]1153 #m #wf_m @mfr_return % [assumption] cases prf2 #_ #H @H1154 qed.1155 1156 lemma ps_reg_retrieve_commute :1157 ∀prog : ertl_program .∀sigma : sigma_map prog.1158 ∀r. preserving … res_preserve …1159 (sigma_regs prog sigma)1160 (sigma_beval prog sigma)1161 (λregs.ps_reg_retrieve regs r)1162 (λregs.ps_reg_retrieve regs r).1163 #prog #sigma #r ** #psd_regs #spilled #hw_regs #prf1164 whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta1165 @opt_to_res_preserve #bv #H lapply((proj1 … prf))1166 whd in match well_formed_ertl_psd_env; normalize nodelta #H11167 %{(H1 … H)} >(lookup_map … H) %1168 qed.1169 1170 lemma ps_arg_retrieve_commute :1171 ∀prog : ertl_program. ∀sigma : sigma_map prog.1172 ∀arg. preserving … res_preserve …1173 (sigma_regs prog sigma)1174 (sigma_beval prog sigma)1175 (λregs.ps_arg_retrieve regs arg)1176 (λregs.ps_arg_retrieve regs arg).1177 #prog #ismga * [#r  #b] whd in match ps_arg_retrieve;1178 normalize nodelta [@ps_reg_retrieve_commute]1179 #regs #wf_regs @mfr_return normalize % #EQ destruct1180 qed.1181 1182 lemma hw_reg_retrieve_commute :1183 ∀prog: ertl_program. ∀sigma : sigma_map prog.1184 ∀r. preserving … res_preserve …1185 (sigma_regs prog sigma)1186 (sigma_beval prog sigma)1187 (λregs.hw_reg_retrieve regs r)1188 (λregs.hw_reg_retrieve regs r).1189 cases daemon1190 qed. (*help for bit_vector_trie*)1191 1192 check hw_reg_store1193 1194 lemma hw_reg_store_commute :1195 ∀prog : ertl_program. ∀sigma : sigma_map prog.1196 ∀r. preserving2 … res_preserve …1197 (sigma_beval prog sigma)1198 (sigma_regs prog sigma)1199 (sigma_regs prog sigma)1200 (hw_reg_store r)1201 (hw_reg_store r).1202 cases daemon1203 qed.1204 1205 1206 lemma ertl_eval_move_commute :1207 ∀prog : ertl_program.∀sigma : sigma_map prog.1208 ∀move. preserving … res_preserve …1209 (sigma_regs prog sigma)1210 (sigma_regs prog sigma)1211 (λregs.ertl_eval_move regs move)1212 (λregs.ertl_eval_move regs move).1213 #prog #sigma * #mv_dst #arg_mv #regs #wf_regs1214 whd in match ertl_eval_move; normalize nodelta1215 @mfr_bind1216 [2: #bv @sigma_beval assumption 1217  cases arg_mv [#mv_dst1  #b] normalize nodelta1218 [ cases mv_dst1 [#r  #b] normalize nodelta1219 [@ps_reg_retrieve_commute  @hw_reg_retrieve_commute]1220  @mfr_return normalize % #EQ destruct1221 ]1222  #bv #prf cases mv_dst [#r  #r] normalize nodelta1223 [@ps_reg_store_commute  @hw_reg_store_commute ]1224 ]1225 qed.1226 1227 lemma ertl_allocate_local_commute : ∀prog : ertl_program.1228 ∀sigma : sigma_map prog.∀reg,regs,prf1. ∃ prf2.1229 ertl_allocate_local reg (sigma_regs prog sigma regs prf1) =1230 sigma_regs prog sigma (ertl_allocate_local reg regs) prf2.1231 #prog #sigma * #r ** #psd_r #sp #hw_regs #prf1 %1232 whd in match ertl_allocate_local; normalize nodelta1233 [ @hide_prf % [2: cases prf1 #_ #x assumption] ]1234 whd in match set_psd_regs; normalize nodelta1235 [ whd in match well_formed_ertl_psd_env; whd in match well_formed_register_env;1236 normalize nodelta * #id #bv cases(decidable_eq_pos id r)1237 [ #EQ >EQ >lookup_add_hit #EQ1 destruct(EQ1) normalize % #EQ2 destruct1238  * #EQ1239 >(lookup_add_miss ?? (psd_r) (an_identifier ? id) (an_identifier RegisterTag r) BVundef ?)1240 [2: % #EQ1 @EQ destruct %] cases prf1 whd in match well_formed_ertl_psd_env;1241 whd in match well_formed_register_env; normalize nodelta #H1 #_ #H @H11242 [% @idassumption]1243 ]1244  whd in match sigma_regs; whd in match sigma_ertl_psd_env; normalize nodelta1245 @eq_f2 [2: %] @eq_f2 [2: %] whd in match sigma_register_env; normalize nodelta1246 cases(map_inf_add beval beval RegisterTag psd_r ? BVundef (an_identifier ? r) ? ?)1247 [ #prf2 #EQ >EQ @eq_f % 1248  #bv #id' #id'' #prf #prf' %1249 ]1250 ]1251 qed.1252 1253 lemma is_push_sigma_commute :1254 ∀ prog : ertl_program. ∀ sigma : sigma_map prog.1255 preserving2 … res_preserve …1256 (sigma_is prog sigma)1257 (sigma_beval prog sigma)1258 (sigma_is prog sigma)1259 is_push1260 is_push.1261 #prog #sigma *1262 [  #bv1  #bv1 #bv2 ] #val #prf1 #prf2 #is'1263 whd in ⊢ (??%%→?); #EQ destruct(EQ)1264 whd in match sigma_beval; normalize nodelta1265 @opt_safe_elim #val' #EQsigma_val1266 %1267 [1,3: @hide_prf %1268 *: whd in match sigma_is in ⊢ (???%); normalize nodelta1269 @opt_safe_elim #is''1270 ] whd in match sigma_is_opt; normalize nodelta1271 [2,4:1272 inversion (sigma_beval_opt ???)1273 [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1;1274 normalize nodelta * #H @H % ]1275 #bv1' #EQ_bv1' >m_return_bind ]1276 >EQsigma_val1277 whd in ⊢ (??%%→?); #EQ destruct(EQ)1278 whd in match sigma_is; normalize nodelta1279 @opt_safe_elim #is11280 whd in match sigma_is_opt; normalize nodelta1281 [ #H @('bind_inversion H) #bv1''1282 >EQ_bv1' #EQ destruct(EQ) ]1283 whd in ⊢ (??%%→?); #EQ destruct(EQ) %1284 qed.1285 1286 check internal_stack1287 check BVpc1288 1289 definition sigma_is_not_head_opt : ∀ prog : ertl_program.1290 sigma_map prog → internal_stack → option internal_stack ≝1291 λprog,sigma,is.1292 match is with1293 [ empty_is ⇒ return empty_is1294  one_is bv ⇒ return one_is bv1295  both_is bv1 bv2 ⇒1296 ! bv2' ← sigma_beval_opt … sigma bv2 ;1297 return both_is bv1 bv2'1298 ].1299 1300 1301 lemma ertlptr_save_frame_commute : ∀prog: ertl_program.1302 ∀sigma : sigma_map prog. ∀kind.1303 preserving … res_preserve …1304 (sigma_state_pc prog sigma)1305 (sigma_state prog sigma)1306 (ertl_save_frame kind it)1307 (ertlptr_save_frame kind it).1308 #prog #sigma * whd in match ertl_save_frame; whd in match ertlptr_save_frame;1309 normalize nodelta * #st #pc #lp * #wf_lp #wf_st1310 [2: @mfr_bind1311 [3: whd in match push_ra; normalize nodelta @mfr_bind1312 [3: whd in match sigma_state_pc; whd in match push; whd in match sigma_state;1313 normalize nodelta @mfr_bind1314 [#is @(sigma_is_not_head_opt prog sigma is ≠ None ?)1315 #is #prf @(opt_safe … prf)1316 1317 1318 1319 #x #x_spec @mfr_bind1320 [ @(λ_.True)  #st * @(sigma_state prog sigma st) 1321 [3: cases kind normalize nodelta whd in match push_ra; normalize nodelta1322 [ whd in match sigma_state_pc; normalize nodelta #st #st_spec1323 *)1324 1249 1325 1250 definition ERTLptrStatusSimulation : 1326 1251 ∀ prog : ertl_program. 1327 1252 let trans_prog ≝ ertl_to_ertlptr prog in 1328 ∀stack_sizes. 1329 sigma_map trans_prog → 1253 ∀stack_sizes.(∀fn.good_state_transformation prog fn) → 1330 1254 status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝ 1331 λprog,stack_sizes,sigma.let trans_prog ≝ ertl_to_ertlptr prog in mk_status_rel ?? 1255 λprog,stack_sizes,good. 1256 let trans_prog ≝ ertl_to_ertlptr prog in 1257 mk_status_rel ?? 1332 1258 (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes 1333 1259 .λs2:ERTLptr_status trans_prog stack_sizes 1334 .s1=sigma_state_pc prog sigma s2) 1335 (* call_rel ≝ *) (λs1:Σs:ERTL_status prog stack_sizes 1260 .s1=sigma_state_pc prog good s2) 1261 (* call_rel ≝ *) 1262 (λs1:Σs:ERTL_status prog stack_sizes 1336 1263 .as_classifier (ERTL_status prog stack_sizes) s cl_call 1337 1264 .λs2:Σs:ERTLptr_status trans_prog stack_sizes 1338 1265 .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call 1339 .pc (mk_prog_params ERTL_semantics prog stack_sizes) s1 1340 =sigma_stored_pc trans_prog sigma 1266 .let sigma ≝ get_sigma_from_good_state … good in 1267 pc (mk_prog_params ERTL_semantics prog stack_sizes) s1 1268 =sigma_stored_pc prog sigma 1341 1269 (pc 1342 1270 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes) … … 1473 1401 *) 1474 1402 1475 lemma ps_reg_retrieve_ok : ∀prog : ertl ptr_program.1403 lemma ps_reg_retrieve_ok : ∀prog : ertl_program. 1476 1404 ∀sigma : sigma_map prog. ∀r,restr. 1477 1405 preserving1 ?? res_preserve1 … … … 1483 1411 whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1 1484 1412 whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta 1485 >lookup_ restrict @if_elim [2: #_ @opt_preserve_none1] #id_r_in1413 >lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in 1486 1414 >(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) H #bv1 1487 1415 #bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec % 1488 1416 qed. 1489 1417 1490 lemma hw_reg_retrieve_ok : ∀prog : ertl ptr_program.1418 lemma hw_reg_retrieve_ok : ∀prog : ertl_program. 1491 1419 ∀sigma : sigma_map prog. ∀r,restr. 1492 1420 preserving1 ?? res_preserve1 … … … 1505 1433 1506 1434 1507 lemma ps_reg_store_ok : ∀prog : ertl ptr_program.1435 lemma ps_reg_store_ok : ∀prog : ertl_program. 1508 1436 ∀sigma : sigma_map prog. ∀r,restr. 1509 1437 preserving21 ?? res_preserve1 … … … 1519 1447 #x #x_spec lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_ 1520 1448 lapply x_spec x_spec lapply EQpsd EQpsd whd in match sigma_register_env; 1521 normalize nodelta >lookup_ restrict @if_elim [2:#_ * #H @⊥ @H %]1522 #id_ in #_ >update_restrict[2: assumption] #H @('bind_inversion H) H1449 normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %] 1450 #id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) H 1523 1451 #x0 >map_update_commute #H @('bind_inversion H) H #x1 #x1_spec 1524 1452 whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % // … … 1529 1457 1530 1458 1531 lemma hw_reg_store_ok : ∀prog : ertl ptr_program.1459 lemma hw_reg_store_ok : ∀prog : ertl_program. 1532 1460 ∀sigma : sigma_map prog. ∀r,restr. 1533 1461 preserving21 ?? res_preserve1 … … … 1544 1472 1545 1473 1546 lemma ertl_eval_move_ok : ∀prog : ertl ptr_program.1474 lemma ertl_eval_move_ok : ∀prog : ertl_program. 1547 1475 ∀sigma : sigma_map prog. ∀ restr,pm. 1548 1476 preserving1 ?? res_preserve1 … … … 1561 1489 qed. 1562 1490 1563 lemma ps_arg_retrieve_ok : ∀prog : ertl ptr_program.1491 lemma ps_arg_retrieve_ok : ∀prog : ertl_program. 1564 1492 ∀sigma : sigma_map prog. ∀a,restr. 1565 1493 preserving1 ?? res_preserve1 … … … 1578 1506 lemma pop_ok : 1579 1507 ∀prog : ertl_program. 1580 let trans_prog ≝ ertl_to_ertlptr prog in 1581 ∀sigma : sigma_map trans_prog. 1582 ∀stack_size. 1583 ∀fn : (joint_closed_internal_function ERTL (globals (mk_prog_params ERTL_semantics prog stack_size))). 1508 ∀good : (∀fn.good_state_transformation prog fn). 1509 ∀restr. 1584 1510 preserving1 ?? res_preserve1 ???? 1585 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))1511 (λst.sigma_state prog good st restr) 1586 1512 (λx.let 〈bv,st〉 ≝ x in 1587 〈sigma_beval trans_prog sigma bv, 1588 sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn) 〉) 1513 〈let sigma ≝ get_sigma_from_good_state … good in 1514 sigma_beval prog sigma bv, 1515 sigma_state prog good st restr〉) 1589 1516 (pop ERTL_semantics) 1590 1517 (pop ERTLptr_semantics). 1591 #prog # sigma #stack_size #fnwhd in match pop; normalize nodelta #st @mfr_bind11518 #prog #good #restr whd in match pop; normalize nodelta #st @mfr_bind1 1592 1519 [@(λx.let 〈bv,is〉 ≝ x in 1593 〈sigma_beval (ertl_to_ertlptr prog) sigma bv, 1594 sigma_is (ertl_to_ertlptr prog) sigma is 〉) 1520 let sigma ≝ get_sigma_from_good_state … good in 1521 〈sigma_beval prog sigma bv, 1522 sigma_is prog sigma is 〉) 1595 1523  whd in match is_pop; normalize nodelta whd in match sigma_state; normalize nodelta 1596 1524 cases(istack ? st) normalize nodelta … … 1605 1533 lemma push_ok : 1606 1534 ∀prog : ertl_program. 1607 let trans_prog ≝ ertl_to_ertlptr prog in 1608 ∀sigma : sigma_map trans_prog. 1609 ∀stack_size. 1610 ∀fn : (joint_closed_internal_function ERTL (globals (mk_prog_params ERTL_semantics prog stack_size))). 1535 ∀good : (∀fn.good_state_transformation prog fn). 1536 ∀restr. 1611 1537 preserving21 ?? res_preserve1 … 1612 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))1613 ( sigma_beval trans_prog sigma)1614 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))1538 (λst.sigma_state prog good st restr) 1539 (let sigma ≝ get_sigma_from_good_state … good in sigma_beval prog sigma) 1540 (λst.sigma_state prog good st restr) 1615 1541 (push ERTL_semantics) 1616 1542 (push ERTLptr_semantics). 1617 cases daemon 1543 #prog #good #restr whd in match push; normalize nodelta #st #bv @mfr_bind1 1544 [ @(let sigma ≝ get_sigma_from_good_state … good in sigma_is ? sigma) 1545  whd in match is_push; normalize nodelta whd in match sigma_state; normalize nodelta 1546 cases (istack ? st) [2,3: #bv [2: #bv']] whd in match sigma_is in ⊢ (???????%?); 1547 normalize nodelta [@res_preserve_error1] @mfr_return_eq1 % 1548  #is @mfr_return_eq1 % 1549 ] 1618 1550 qed. 1619 1551 1620 1552 lemma be_opaccs_ok : 1621 ∀prog : ertl ptr_program. ∀sigma : sigma_map prog.1553 ∀prog : ertl_program. ∀sigma : sigma_map prog. 1622 1554 ∀ op. 1623 1555 preserving21 ?? res_preserve1 ?????? … … 1629 1561 (be_opaccs op) 1630 1562 (be_opaccs op). 1631 cases daemon 1632 qed. 1633 1634 lemma be_op1_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1563 #prog #sigma #op #bv #bv1 1564 whd in match be_opaccs; normalize nodelta @mfr_bind1 1565 [ @(λx.x) 1566  cases bv 1567 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 1568 whd in match Byte_of_val; normalize nodelta 1569 try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //] 1570 whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?) 1571 normalize nodelta [2: #pc] @res_preserve_error1 1572  #by @mfr_bind1 1573 [ @(λx.x) 1574  cases bv1 1575 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 1576 whd in match Byte_of_val; normalize nodelta 1577 try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //] 1578 whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?) 1579 normalize nodelta [2: #pc] @res_preserve_error1 1580  #by1 * #bv2 #bv3 cases(opaccs eval op by by1) #by' #by1' normalize nodelta 1581 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1582 qed. 1583 1584 lemma be_op1_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog. 1635 1585 ∀ op. 1636 1586 preserving1 ?? res_preserve1 … … … 1639 1589 (be_op1 op) 1640 1590 (be_op1 op). 1641 cases daemon 1642 qed. 1643 1644 lemma be_op2_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1591 #prog #sigma #o #bv whd in match be_op1; normalize nodelta @mfr_bind1 1592 [ @(λx.x) 1593  cases bv 1594 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 1595 whd in match Byte_of_val; whd in match sigma_beval; normalize nodelta 1596 try @res_preserve_error1 [ @mfr_return_eq1 %] 1597 cases(sigma_pc_opt prog sigma pc1) [2: #pc2] normalize nodelta 1598 @res_preserve_error1 1599  #by @mfr_return_eq1 % 1600 ] 1601 qed. 1602 1603 lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') → 1604 res_preserve1 X Y F n (Error … e). 1605 #X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1 1606 qed. 1607 1608 1609 lemma be_op2_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog. 1645 1610 ∀ b,op. 1646 1611 preserving21 ?? res_preserve1 … … … 1650 1615 (be_op2 b op) 1651 1616 (be_op2 b op). 1652 cases daemon 1653 qed. 1654 1655 lemma pointer_of_address_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1617 #prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta 1618 cases bv 1619 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 1620 normalize nodelta [@res_preserve_error1] whd in match sigma_beval; 1621 normalize nodelta 1622 cases bv1 1623 [1,2,8,9,15,16,22,23,29,30,36,37: 1624 3,10,17,24,31,38: #ptr1' #ptr2' #p' 1625 4,11,18,25,32,39: #by' 1626 5,12,19,26,33,40: #p' 1627 6,13,20,27,34,41: #ptr' #p' 1628 7,14,21,28,35,42: #pc1' #p1' 1629 ] 1630 normalize nodelta try @res_preserve_error1 1631 [4,5,8,13,16,20,21,22,23,24,25,26 : @res_preserve_error11 % 1632 [2,4,6,8,10,12,14,16,18,20,22,24: cases(sigma_pc_opt ???) try % #pc2 % 1633 *:] 1634 *: cases op normalize nodelta 1635 try @res_preserve_error1 try( @mfr_return_eq1 %) 1636 [1,2,12,13,16,17,18: @if_elim #_ try @res_preserve_error1 1637 try( @mfr_return_eq1 %) 1638 [ @if_elim #_ @mfr_return_eq1 % 1639  cases(ptype ptr) normalize nodelta 1640 [2: @res_preserve_error1] @mfr_bind1 1641 [ @(λx.x) 1642  whd in match Bit_of_val; normalize nodelta 1643 cases b [#bo #bo #ptr'' #p'' #bit_v] 1644 normalize nodelta [2,3: @res_preserve_error1] 1645 @mfr_return_eq1 % 1646  #bi cases(op2 ?????) #by #bi1 normalize nodelta 1647 @mfr_return_eq1 % 1648 ] 1649  cases(ptype ptr) normalize nodelta @res_preserve_error1 1650 ] 1651 3,4,5,6,7,8: @mfr_bind1 1652 [1,4,7,10,13,16: @(λx.x) 1653 2,5,8,11,14,17: whd in match Bit_of_val; normalize nodelta 1654 cases b [1,4,7,10,13,16: #bo 1655 2,5,8,11,14,17: 1656 3,6,9,12,15,18: #bo #ptr'' #p'' #bit_v 1657 ] normalize nodelta try @res_preserve_error1 1658 @mfr_return_eq1 % 1659 3,6,9,12,15,18: #bi cases(op2 ?????) #by #bi1 normalize nodelta 1660 @mfr_return_eq1 % 1661 ] 1662 *: whd in match be_add_sub_byte; normalize nodelta 1663 [1,2,3: cases(ptype ptr) normalize nodelta [2,4,6: @res_preserve_error1] 1664 cases p * [2,4,6: #p_no] #prf normalize nodelta 1665 [@res_preserve_error1 1666 2,3: cases b [1,4: #bo2,5: 3,6: #bo #ptr'' #p'' #bit_v] 1667 normalize nodelta [1,2,3,4: @res_preserve_error1] 1668 @if_elim #_ [2,4: @res_preserve_error1] 1669 @If_elim #INUTILE [2,4: @res_preserve_error1] 1670 @pair_elim #a1 #a2 #_ normalize nodelta 1671 @mfr_return_eq1 % 1672 *: @mfr_bind1 1673 [1,4,7: @(λx.x) 1674 2,5,8: whd in match Bit_of_val; normalize nodelta 1675 [@mfr_return_eq1 %] cases b 1676 [1,4: #bo2,5: 3,6: #bo #ptr'' #p'' #bit_v] 1677 normalize nodelta [3,4,5,6: @res_preserve_error1] 1678 @mfr_return_eq1 % 1679 3,6,9: * normalize nodelta [1,3,5: @res_preserve_error1] 1680 cases(op2 ?????) #a1 #a2 normalize nodelta 1681 @mfr_return_eq1 % 1682 ] 1683 ] 1684 *: cases(ptype ptr') normalize nodelta [2,4: @res_preserve_error1] 1685 cases p' * [2,4: #part_no] #prf normalize nodelta 1686 [ @res_preserve_error1 1687  cases b [#bo #bo #ptr'' #p'' #bit_v] 1688 normalize nodelta [1,2: @res_preserve_error1] @if_elim #_ 1689 [2: @res_preserve_error1] @If_elim #INUTILE [2: @res_preserve_error1] 1690 @pair_elim #a1 #a2 #_ normalize nodelta @mfr_return_eq1 % 1691 *: @mfr_bind1 1692 [1,4: @(λx.x) 1693 2,5: whd in match Bit_of_val; normalize nodelta [ @mfr_return_eq1 %] 1694 cases b [#bo #bo #ptr'' #p'' #bit_v] normalize nodelta 1695 [2,3: @res_preserve_error1] @mfr_return_eq1 % 1696 3,6: * normalize nodelta [1,3: @res_preserve_error1] 1697 cases(op2 ?????) #a1 #a2 normalize nodelta 1698 @mfr_return_eq1 % 1699 ] 1700 ] 1701 ] 1702 ] 1703 ] 1704 qed. 1705 1706 lemma pointer_of_address_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog. 1656 1707 preserving1 … res_preserve1 … 1657 1708 (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog sigma bv1, … … 1659 1710 (λx.x) 1660 1711 pointer_of_address pointer_of_address. 1661 cases daemon 1662 qed. 1663 1664 lemma beloadv_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1712 #prog #sigma * #bv1 #bv2 whd in match pointer_of_address; 1713 whd in match pointer_of_bevals; normalize nodelta 1714 cases bv1 normalize nodelta 1715 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 1716 try @res_preserve_error1 1717 [ cases bv2 [   #ptr1' #ptr2' #p'  #by'  #p'  #ptr' #p'  #pc1' #p1'] 1718 normalize nodelta 1719 [1,2,3,4,5: @res_preserve_error1 1720  @if_elim #_ [ @mfr_return_eq1 %  @res_preserve_error1] 1721 ] 1722 ] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???) 1723 [2,4: #pc4] normalize nodelta @res_preserve_error1 1724 qed. 1725 1726 lemma beloadv_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog. 1665 1727 ∀ptr. 1666 1728 preserving1 … opt_preserve1 … … … 1669 1731 (λm.beloadv m ptr) 1670 1732 (λm.beloadv m ptr). 1671 cases daemon 1672 qed. 1673 1674 lemma bestorev_ok : ∀prog : ertlptr_program.∀sigma : sigma_map prog. 1733 #prog #sigma #ptr #mem whd in match beloadv; whd in match do_if_in_bounds; 1734 normalize nodelta @if_elim [2: #_ @opt_preserve_none1] 1735 whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb 1736 @if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?); 1737 normalize nodelta @If_elim [2: >Hzlb * #H @⊥ @H %] #_ @andb_elim @if_elim 1738 [2: #_ *] #Hzleb #Hzlb' >Hzlb normalize nodelta >Hzlb' normalize nodelta 1739 @mfr_return_eq1 whd in match sigma_mem; normalize nodelta >Hzlb 1740 @If_elim [2: * #H @⊥ @H %] * >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] 1741 * % 1742 qed. 1743 1744 lemma bestorev_ok : ∀prog : ertl_program.∀sigma : sigma_map prog. 1675 1745 ∀ptr. 1676 1746 preserving21 … opt_preserve1 … … … 1680 1750 (λm.bestorev m ptr) 1681 1751 (λm.bestorev m ptr). 1682 cases daemon 1683 qed. 1684 1685 lemma sp_ok : ∀prog : ertl_program. ∀sigma : sigma_map (ertl_to_ertlptr prog). 1686 ∀stack_size. 1687 ∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))). 1688 preserving1 … res_preserve1 … 1689 (λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn)) 1752 #prog #sigma #ptr #mem #bv whd in match bestorev; whd in match do_if_in_bounds; 1753 normalize nodelta @if_elim [2: #_ @opt_preserve_none1] 1754 whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb 1755 @if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *] 1756 whd in match sigma_mem in ⊢ (% → % → ?); normalize nodelta >Hzlb 1757 @If_elim [2: * #H @⊥ @H %] * #Hzleb #Hzlb' normalize nodelta >Hzleb 1758 >Hzlb' normalize nodelta @mfr_return_eq1 whd in ⊢ (???%); @eq_f @mem_ext_eq 1759 [ #bl normalize nodelta % [%] 1760 [ whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] * 1761 whd in match update_block; normalize nodelta @if_elim 1762 [ @eq_block_elim [2: #_ *] #EQbl * >EQbl >Hzlb @If_elim [2: * #H @⊥ @H %] 1763 * whd in match low_bound; normalize nodelta @if_elim [ #_ %] 1764 @eq_block_elim #_ * % 1765  @eq_block_elim [#_ *] * #Hbl * @If_elim 1766 [ #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; 1767 normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl 1768 assumption 1769  #Hzlb'' >Hzlb'' @If_elim [*] #_ % 1770 ] 1771 ] 1772  whd in match update_block; whd in match sigma_mem; normalize nodelta 1773 @if_elim @eq_block_elim [2,3: #_ * 4: *] #Hbl #_ @If_elim 1774 [3,4: >Hbl >Hzlb * [2: #H @⊥ @H %] @If_elim [2: * #H @⊥ @H %] * 1775 whd in match high_bound; normalize nodelta @if_elim [#_ %] 1776 @eq_block_elim [ #_ *] * #H @⊥ @H % 1777  #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match high_bound; 1778 normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] 1779 #H @⊥ @Hbl assumption 1780  #Hzlb'' >Hzlb'' @If_elim [*] #_ % 1781 ] 1782  #z whd in match update_block; whd in match sigma_mem; normalize nodelta 1783 @if_elim @eq_block_elim [2,3: #_ * 4: *] #Hbl #_ 1784 [ @If_elim #Hzlb'' >Hzlb'' [2: @If_elim * #_ %] @If_elim @andb_elim 1785 @if_elim [2: #_ *] #Hzleb' #Hzlb''' 1786 [ @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta 1787 @If_elim @andb_elim @if_elim [2: #_ *] @if_elim 1788 [1,3,5: @eq_block_elim [2,4,6: #_ *] #H @⊥ @Hbl assumption] #_ >Hzleb' * 1789 whd in match high_bound; normalize nodelta @if_elim 1790 [1,3: @eq_block_elim [2,4: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb''' 1791 [ * %] * #H @⊥ @H % 1792  @If_elim * [2: #H @⊥ @H %] whd in match low_bound; normalize nodelta 1793 @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ 1794 >Hzleb' whd in match high_bound; normalize nodelta @if_elim 1795 [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb''' 1796 @If_elim [2: #_ %] * 1797  @If_elim [2: * #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim 1798 [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ #_ 1799 whd in match low_bound in Hzleb'; normalize nodelta in Hzleb'; 1800 whd in match high_bound; normalize nodelta @if_elim 1801 [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ @If_elim [2: #_ %] 1802 @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; * 1803 ] 1804  whd in ⊢ (??%?); @if_elim @eqZb_elim [2,3: #_ * 4: *] #Hz * 1805 [ >Hzlb @If_elim [2: * #H @⊥ @H %] * @If_elim @andb_elim @if_elim 1806 [2: #_ *] #Hzleb' #Hzlb'' >Hbl >Hzlb @If_elim [2,4,6: * #H @⊥ @H %] #_ 1807 whd in match low_bound; normalize nodelta @eq_block_elim 1808 [2,4,6: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound; 1809 normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %] 1810 #_ normalize nodelta 1811 [1,2: >Hzleb' >Hzlb'' @If_elim [2,3: * #H @⊥ @H %] 1812 #_ [2: %] whd in ⊢ (???(???%)); @if_elim [2: #_ %] 1813 @eqZb_elim [2: #_ *] #H @⊥ @Hz assumption 1814  @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; * 1815 ] 1816  >Hbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; 1817 normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] #_ normalize nodelta 1818 whd in match high_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] 1819 normalize nodelta >Hz >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] #_ #_ 1820 whd in ⊢ (???(???%)); @eqZb_elim [2: * #H @⊥ @H %] #_ % 1821 ] 1822 ] 1823 ] 1824  % 1825 ] 1826 qed. 1827 1828 lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region. 1829 ∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) → 1830 (∀ prf : r = Code.P (g prf)) → 1831 P ((match r return λx.(r = x → ?) with 1832 [XData ⇒ f  Code ⇒ g])(refl ? r)). 1833 #A #P * #f #g #H1 #H2 normalize nodelta [ @H1  @H2] 1834 qed. 1835 1836 1837 lemma sp_ok : ∀prog : ertl_program. 1838 ∀good : (∀fn.good_state_transformation prog fn). 1839 ∀restr. 1840 preserving1 … res_preserve1 … 1841 (λst.sigma_state prog good st restr) 1690 1842 (λx.x) 1691 1843 (sp ERTL_semantics) 1692 1844 (sp ERTLptr_semantics). 1693 cases daemon 1694 qed. 1695 1696 lemma set_sp_ok : ∀prog : ertl_program. 1697 let trans_prog ≝ ertl_to_ertlptr prog in 1698 ∀sigma : sigma_map trans_prog. 1699 ∀stack_size. 1700 ∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))). 1701 ∀ptr,st. 1702 set_sp ? ptr (sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) = 1703 sigma_state trans_prog sigma (set_sp ? ptr st) (joint_if_locals ERTL ? fn). 1845 #prog #good #restr #st whd in match sp; normalize nodelta 1846 whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state; 1847 normalize nodelta whd in match sigma_regs; normalize nodelta 1848 cases(regs ? st) #psd_r #hw_r normalize nodelta 1849 inversion(pointer_of_address ?) normalize nodelta [2: #e #_ @res_preserve_error1] 1850 #pt #EQ lapply(jmeq_to_eq ??? EQ) EQ whd in match hwreg_retrieve; normalize nodelta 1851 whd in match sigma_hw_register_env; normalize nodelta 1852 change with (sigma_beval ? (get_sigma_from_good_state … good) BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?); 1853 >lookup_map >lookup_map 1854 cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef) 1855 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 1856 whd in match pointer_of_address; whd in match pointer_of_bevals; normalize nodelta 1857 [1,2,3,4,5: #ABS destruct 1858  cases(lookup beval 6 (bitvector_of_register RegisterSPH) (reg_env hw_r) BVundef) 1859 [   #ptr1' #ptr2' #p'  #by'  #p'  #ptr' #p'  #pc1' #p1'] 1860 whd in match sigma_beval; normalize nodelta 1861 [1,2,3,4,5: #ABS destruct 1862  @if_elim [2: #_ #ABS destruct] #H whd in ⊢ (??%? → ?); #EQ destruct 1863 normalize nodelta @match_reg_elim #INUTILE 1864 [ @mfr_return_eq1 %  @res_preserve_error1 ] 1865  cases (sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct 1866 ] 1867  whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?) 1868 normalize nodelta [2: #x] #EQ destruct 1869 ] 1870 qed. 1871 1872 lemma set_sp_ok : ∀prog : ertl_program. 1873 ∀good : (∀fn.good_state_transformation prog fn). 1874 ∀restr.∀ptr,st. 1875 set_sp ? ptr (sigma_state prog good st restr) = 1876 sigma_state prog good (set_sp ? ptr st) restr. 1704 1877 cases daemon 1705 1878 qed. … … 1707 1880 lemma eval_seq_no_pc_no_call_ok : 1708 1881 ∀prog : ertl_program. 1709 let trans_prog ≝ ertl_to_ertlptr progin1710 ∀ stack_size.∀sigma : sigma_map trans_prog.1711 ∀ id. ∀fn : (joint_closed_internal_function ??) .∀seq.1882 let trans_prog ≝ (ertl_to_ertlptr prog) in 1883 ∀good : (∀fn.good_state_transformation prog fn). 1884 ∀stack_size. ∀id. ∀fn : (joint_closed_internal_function ??) .∀seq. 1712 1885 preserving1 ?? res_preserve1 ???? 1713 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))1714 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))1886 (λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn)))) 1887 (λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn)))) 1715 1888 (eval_seq_no_pc ERTL_semantics 1716 1889 (globals (mk_prog_params ERTL_semantics prog stack_size)) … … 1718 1891 (eval_seq_no_pc ERTLptr_semantics 1719 1892 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size)) 1720 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) ( translate_step_seq… seq)).1721 #prog # stack_size #sigma#f #fn *1893 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (seq_embed … seq)). 1894 #prog #good #stack_size #f #fn * 1722 1895 whd in match eval_seq_no_pc; normalize nodelta 1723 1896 [ #c #st @mfr_return1 … … 1725 1898  #pm #st whd in match pair_reg_move; normalize nodelta 1726 1899 @mfr_bind1 1727 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1728  change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok 1729  #regs @mfr_return_eq1 % 1900 [ 2: change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok 1901   #regs @mfr_return_eq1 % 1730 1902 ] 1731 1903  #r #st @mfr_bind1 1732 [@(λx.let 〈bv,st〉 ≝ x in 1733 〈sigma_beval (ertl_to_ertlptr prog) sigma bv, 1734 sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn) 〉) 1735  @pop_ok 1904 [2: @pop_ok  1736 1905  * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1 1737 [@(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1738  @ps_reg_store_ok 1906 [2: @ps_reg_store_ok  1739 1907  #regs @mfr_return_eq1 % 1740 1908 ] 1741 1909 ] 1742 1910  #r #st @mfr_bind1 1743 [@(λbv.sigma_beval (ertl_to_ertlptr prog) sigma bv) 1744  whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1911 [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok  1745 1912  #bv @push_ok 1746 1913 ] … … 1752 1919 change with ((dph_reg ERTL) → ?) 1753 1920 #dph #st @mfr_bind1 1754 [ @(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn))1921 [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn)))) 1755 1922  whd in match dpl_store; normalize nodelta @mfr_bind1 1756 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1757  @opt_safe_elim #bl #EQbl 1758 @opt_safe_elim #bl' 1923 [2: @opt_safe_elim #bl #EQbl 1924 @opt_safe_elim #bl' 1759 1925 >(find_symbol_transf … 1760 1926 (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?); 1761 1927 >EQbl #EQ destruct whd in match sigma_state; normalize nodelta 1762 change with (sigma_beval (ertl_to_ertlptr prog) sigma(BVptr …))1928 change with (sigma_beval prog (get_sigma_from_good_state … good) (BVptr …)) 1763 1929 in ⊢ (???????(?????%?)?); 1764 @ps_reg_store_ok 1930 @ps_reg_store_ok  1765 1931  #regs @mfr_return_eq1 % 1766 1932 ] … … 1769 1935 (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?); 1770 1936 >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1 1771 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1772  whd in match sigma_state; normalize nodelta 1773 change with (sigma_beval (ertl_to_ertlptr prog) sigma (BVptr …)) 1937 [2: whd in match sigma_state; normalize nodelta 1938 change with (sigma_beval prog (get_sigma_from_good_state … good) (BVptr …)) 1774 1939 in ⊢ (???????(?????%?)?); 1775 @ps_reg_store_ok 1940 @ps_reg_store_ok  1776 1941  #regs @mfr_return_eq1 % 1777 1942 ] 1778 1943 ] 1779 1944  #op #a #b #arg1 #arg2 #st @mfr_bind1 1780 [@(sigma_beval (ertl_to_ertlptr prog) sigma) 1781  whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta 1782 @ps_arg_retrieve_ok 1945 [2: whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta 1946 @ps_arg_retrieve_ok  1783 1947  #bv1 @mfr_bind1 1784 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1785  whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta 1786 @ps_arg_retrieve_ok 1948 [2: whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta 1949 @ps_arg_retrieve_ok  1787 1950  #bv2 @mfr_bind1 1788 [@(λx.let 〈bv1,bv2〉 ≝ x in 1789 〈sigma_beval (ertl_to_ertlptr prog) sigma bv1, 1790 sigma_beval (ertl_to_ertlptr prog) sigma bv2〉) 1791  @be_opaccs_ok 1951 [2: @be_opaccs_ok  1792 1952  * #bv3 #bv4 normalize nodelta @mfr_bind1 1793 [ @(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn))1953 [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn)))) 1794 1954  whd in match acca_store; normalize nodelta @mfr_bind1 1795 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1796  @ps_reg_store_ok 1955 [2: @ps_reg_store_ok  1797 1956  #regs @mfr_return_eq1 % 1798 1957 ] 1799 1958  #st1 whd in match accb_store; normalize nodelta @mfr_bind1 1800 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))1801  whd in match sigma_state; normalize nodelta1802 @ps_reg_store_ok1803  #regs @mfr_return_eq1 % ]1959 [2: whd in match sigma_state; normalize nodelta 1960 @ps_reg_store_ok  1961  #regs @mfr_return_eq1 % 1962 ] 1804 1963 ] 1805 1964 ] … … 1807 1966 ] 1808 1967  #op #r1 #r2 #st @mfr_bind1 1809 [ @(sigma_beval (ertl_to_ertlptr prog) sigma)1968 [ @(sigma_beval prog (get_sigma_from_good_state … good)) 1810 1969  whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok 1811 1970  #bv1 @mfr_bind1 1812 [ @(sigma_beval (ertl_to_ertlptr prog) sigma)1971 [ @(sigma_beval prog (get_sigma_from_good_state … good)) 1813 1972  @be_op1_ok 1814 1973  #bv2 whd in match acca_store; normalize nodelta @mfr_bind1 1815 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1816  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 1974 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok  1817 1975  #regs @mfr_return_eq1 % 1818 1976 ] … … 1820 1978 ] 1821 1979  #op2 #r1 #r2 #arg #st @mfr_bind1 1822 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1823  whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1980 [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok  1824 1981  #bv @mfr_bind1 1825 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1826  whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1982 [2: whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok  1827 1983  #bv1 @mfr_bind1 1828 [@(λx.let 〈bv,b〉≝ x in 〈sigma_beval (ertl_to_ertlptr prog) sigma bv,b〉) 1829  @be_op2_ok 1984 [2: @be_op2_ok  1830 1985  * #bv2 #b @mfr_bind1 1831 [ @(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn))1986 [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn)))) 1832 1987  whd in match acca_store; normalize nodelta @mfr_bind1 1833 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1834  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 1988 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok  1835 1989  #regs @mfr_return_eq1 % 1836 1990 ] … … 1843 1997  #st @mfr_return_eq1 % 1844 1998  #r1 #dpl #dph #st @mfr_bind1 1845 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1846  whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1999 [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok  1847 2000  #bv @mfr_bind1 1848 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1849  whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 2001 [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok  1850 2002  #bv1 @mfr_bind1 1851 2003 [ @(λx.x) 1852  @(pointer_of_address_ok ? sigma〈bv1,bv〉)2004  @(pointer_of_address_ok ? ? 〈bv1,bv〉) 1853 2005  #ptr @mfr_bind1 1854 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1855  @opt_to_res_preserve1 @beloadv_ok 2006 [2: @opt_to_res_preserve1 @beloadv_ok  1856 2007  #bv2 whd in match acca_store; normalize nodelta @mfr_bind1 1857 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1858  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 2008 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok  1859 2009  #regs @mfr_return_eq1 % 1860 2010 ] … … 1864 2014 ] 1865 2015  #dpl #dph #r #st @mfr_bind1 1866 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1867  whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 2016 [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok  1868 2017  #bv @mfr_bind1 1869 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1870  whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 2018 [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok  1871 2019  #bv1 @mfr_bind1 1872 2020 [ @(λx.x) 1873  @(pointer_of_address_ok ? sigma〈bv1,bv〉)2021  @(pointer_of_address_ok ? ? 〈bv1,bv〉) 1874 2022  #ptr @mfr_bind1 1875 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1876  whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 2023 [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok  1877 2024  #bv2 @mfr_bind1 1878 [ @(sigma_mem (ertl_to_ertlptr prog) sigma) 1879  @opt_to_res_preserve1 @bestorev_ok 2025 [2: @opt_to_res_preserve1 @bestorev_ok  1880 2026  #m @mfr_return_eq1 % 1881 2027 ] … … 1895 2041  #r whd in match ps_reg_store_status; normalize nodelta @mfr_bind1 1896 2042 [2: whd in match sigma_state; normalize nodelta 1897 change with (sigma_beval ? sigma (BVByte ?)) in ⊢ (???????(??%?)?); 2043 change with (sigma_beval ? (get_sigma_from_good_state … good) (BVByte ?)) 2044 in ⊢ (???????(??%?)?); 1898 2045 @ps_reg_store_ok 1899 2046  … … 1904 2051 ] 1905 2052 qed. 2053 2054 2055 xxxxxxxxxxxxxxxxx 1906 2056 1907 2057 lemma fetch_statement_commute : … … 2054 2204 2055 2205 lemma pc_of_label_eq : 2206 ∀p,p'.let pars ≝ make_sem_graph_params p p' in 2056 2207 ∀globals,ge,bl,i_fn,lbl. 2057 2208 fetch_internal_function ? ge bl = return i_fn → 2058 pc_of_label ERTL_semantics globals ge bl lbl = 2059 OK ? (pc_of_point ERTL_semantics bl lbl). 2060 #globals #ge #bl #i_fn #lbl #EQf whd in match pc_of_label; 2061 normalize nodelta >EQf % 2209 pc_of_label pars globals ge bl lbl = 2210 OK ? (pc_of_point ERTL_semantics bl lbl). 2211 #p #p' #globals #ge #bl #i_fn #lbl #EQf 2212 whd in match pc_of_label; 2213 normalize nodelta >EQf >m_return_bind % 2062 2214 qed. 2063 2215 … … 2238 2390 [ #EQbl whd in match dummy_state_pc; whd in match null_pc; 2239 2391 whd in match fetch_statement; whd in match fetch_internal_function; 2240 normalize nodelta lapply(fetch_function_no_zero ??????) 2241 [2: @( «mk_block Code OZ,refl region Code») 2242  %  @prog 7: #EQ >EQ *:] whd in ⊢ (??%% → ?); #EQ destruct] 2392 normalize nodelta >(fetch_function_no_zero ??????) [2: %] 2393 whd in ⊢ (??%% → ?); #EQ destruct ] 2243 2394 #Hbl inversion(fetch_internal_function ???) 2244 2395 [2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; … … 2257 2408 #H lapply (err_eq_from_io ????? H) H #H @('bind_inversion H) H 2258 2409 * #st1 #pc1 #EQpop whd in match next_of_call_pc; normalize nodelta 2259 >m_bind_bind #H @('bind_inversion H) H ** #f1 #fn 2* normalize nodelta2410 >m_bind_bind #H @('bind_inversion H) H ** #f1 #fn1 * normalize nodelta 2260 2411 [ * [ #c_id #args #dest  #r #lbl  #seq ] #nxt  #fin  * ] 2261 2412 #EQf1 normalize nodelta [2,3,4: whd in ⊢ (??%% → ?); #EQ destruct] … … 2264 2415 normalize nodelta #EQf' 2265 2416 % [ whd in match joint_classify; normalize nodelta >EQf' >m_return_bind %] 2266 cases(pop_ra_ok ? sigma stack_size ??? EQpop) * #st3 #pc3 * #st3_spec 2417 change with (pop_ra ?? = ?) in EQpop; whd in match set_no_pc in EQpop; 2418 normalize nodelta in EQpop; 2419 cases(pop_ra_ok ? sigma stack_size fn ?? EQpop) * #st3 #pc3 * #st3_spec 2267 2420 normalize nodelta #EQ destruct whd in match set_last_pop; whd in match succ_pc; 2268 2421 normalize nodelta whd in match (point_of_succ ???); … … 2278 2431 normalize nodelta whd in match sigma_pc_opt; normalize nodelta 2279 2432 >bl3_spec normalize nodelta assumption 2280  #bl3_spec #H @('bind_inversion H) H * # fn4 #id42433  #bl3_spec #H @('bind_inversion H) H * #id4 #fn4 2281 2434 #H lapply(res_eq_from_opt ??? H) H #fn4_spec 2282 2435 #H @('bind_inversion H) H #lbl4 #lbl4_spec whd in ⊢ (??%? → ?); #EQ … … 2292 2445 3: >(fetch_internal_function_transf … fn3_spec) % *:] 2293 2446 #bl3_spec whd in match pc_of_point; normalize nodelta #EQ >EQ in bl3_spec; * 2294  #_ inversion(fetch_internal_function ???) [#x #_ normalize nodelta % cases daemon (*serve lemma sul fetch della call *) 2295 xxxxxxxxxxxxxxx 2296  2297 whd in match sigma_state_pc; normalize nodelta @if_elim 2298 2299 qed. 2447  #_ cases daemon 2448 ] 2449 ] cases daemon 2450 qed. 2451 2452 (* 2453 lemma ertl_allocate_local_ok : ∀ prog : ertl_program. 2454 let trans_prog ≝ ertl_to_ertlptr prog in 2455 ∀sigma : sigma_map. 2456 ∀stack_size. 2457 ∀id,regs. 2458 ertl_allocate_local id (sigma_regs ? sigma getLocalsFromId( 2459 *) 2300 2460 2301 2461 lemma eval_tailcall_ok : … … 2319 2479 eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 2320 2480 st = return st''. 2321 cases daemon 2322 qed. 2323 2324 lemma eval_cond_ok : 2325 ∀prog. 2326 let trans_prog ≝ ertl_to_ertlptr prog in 2327 ∀stack_sizes. 2328 ∀sigma : sigma_map trans_prog. 2329 ∀st,st',f,fn,a,ltrue,lfalse. 2330 fetch_statement ERTL_semantics … 2331 (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) = 2332 return 〈f, fn, sequential … (COND ERTL … a ltrue) lfalse〉 → 2333 eval_state ERTL_semantics 2334 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2335 (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 2336 (sigma_state_pc ? sigma st) = 2337 return st' → 2338 as_costed (ERTL_status prog stack_sizes) 2339 st' → 2340 ∃ st''. st' = sigma_state_pc ? sigma st'' ∧ 2341 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) 2342 st st''. 2343 bool_to_Prop (taaf_non_empty … taf). 2344 cases daemon 2345 qed. 2346 2347 2348 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 2349 ex1_intro: ∀ x:A. P x → ex_Type1 A P. 2350 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) 2351 2352 lemma 2353 find_funct_ptr_none: 2354 ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). 2355 ∀b: block. 2356 find_funct_ptr ? (globalenv … iV p) b = None ? → 2357 find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?. 2358 #A #B #V #i #p #transf #b 2359 whd in match find_funct_ptr; normalize nodelta 2360 cases b b * normalize nodelta [#x #_ %] * normalize nodelta 2361 [1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta 2362 whd in match globalenv_allocmem; normalize nodelta 2363 cases daemon (*forse e' falso *) 2364 qed. 2365 2481 #prog #stack_size #sigma #st #st' #f #fn #fl #called #args 2482 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta 2483 @if_elim 2484 [ #EQbl whd in match dummy_state_pc; whd in match null_pc; 2485 whd in match fetch_statement; whd in match fetch_internal_function; 2486 normalize nodelta >(fetch_function_no_zero ??????) [2: %] 2487 whd in ⊢ (??%% → ?); #EQ destruct ] 2488 #Hbl inversion(fetch_internal_function ???) 2489 [2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; 2490 whd in match fetch_statement; whd in match fetch_internal_function; 2491 normalize nodelta lapply(fetch_function_no_zero ??????) 2492 [2: @( «mk_block Code OZ,refl region Code») 2493  %  @prog 7: #EQ >EQ *:] whd in ⊢ (??%% → ?); #EQ destruct] 2494 * #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) EQ #fn1_spec normalize nodelta 2495 #EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec 2496 >m_return_bind #H @('bind_inversion H) H #stmt' #_ whd in ⊢ (??%% → ?); 2497 #EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta 2498 @if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta 2499 whd in match eval_state; normalize nodelta >EQf >m_return_bind 2500 whd in match eval_statement_no_pc; whd in match eval_statement_advance; 2501 normalize nodelta >m_return_bind whd in match eval_tailcall; 2502 normalize nodelta #H @('bind_inversion H) H #bl whd in match set_no_pc; 2503 normalize nodelta #bl_spec #H @('bind_inversion H) H * #id1 * [#int_f  #ext_f] 2504 #H lapply(err_eq_from_io ????? H) H #id1_spec normalize nodelta 2505 [2: #H @('bind_inversion H) H #st1 whd in match eval_external_call; normalize nodelta 2506 #H @('bind_inversion H) H #l_val #_ #H @('bind_inversion H) H #le #_ 2507 #H @('bind_inversion H) H #x whd in match do_io; normalize nodelta 2508 whd in ⊢ (???% → ?); #EQ destruct ] 2509 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H #st1 2510 whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????); 2511 #H @('bind_inversion H) H #n #H lapply(opt_eq_from_res ???? H) H #n_spec 2512 whd in match(setup_call ???????); >m_return_bind 2513 whd in ⊢ (??%% → ?); #EQ destruct whd in match sigma_state in ⊢ (% → ?); 2514 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct 2515 % [ % 2516 [ % 2517 [ @(st_frms ERTLptr_semantics st) 2518  @(istack ERTLptr_semantics st) 2519  @(carry ERTLptr_semantics st) 2520  cases daemon 2521  @(m ERTLptr_semantics st) 2522 ] 2523  @(mk_program_counter bl 2524 (offset_of_point ERTL_semantics 2525 (joint_if_entry ERTL_semantics 2526 (prog_var_names (joint_function ERTL_semantics) ℕ prog) int_f))) 2527  @(last_pop ERTLptr_semantics st) 2528 ] 2529 ] 2530 % [ whd in match sigma_state_pc; normalize nodelta @if_elim whd in match pc_of_point; 2531 normalize nodelta 2532 [ #Hbl >fetch_function_no_minus_one in id1_spec; 2533 [2: lapply Hbl @eqZb_elim Hbl #Hbl * @Hbl] whd in ⊢ (???% → ?); 2534 #EQ destruct(EQ) 2535 ] #_ whd in match fetch_internal_function; normalize nodelta >id1_spec 2536 >m_return_bind normalize nodelta cases daemon (*TO BE COmpleted *) 2537 ] cases daemon (*TO BE COMPLETED*) 2538 qed. 2539 2540 2541 2542 2366 2543 lemma as_label_ok : ∀ prog : ertl_program. 2367 2544 let trans_prog ≝ ertl_to_ertlptr prog in … … 2428 2605 cases daemon 2429 2606 qed. 2607 2608 lemma bool_of_beval_ok : ∀prog : ertlptr_program. 2609 ∀sigma : sigma_map prog. 2610 preserving1 … res_preserve1 … 2611 (sigma_beval prog sigma) 2612 (λx.x) 2613 (bool_of_beval) 2614 (bool_of_beval). 2615 #prog #sigma whd in match bool_of_beval; normalize nodelta 2616 * normalize nodelta 2617 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p] 2618 try @res_preserve_error1 #x 2619 [1,2,3,4: whd in ⊢ (???% → ?); #EQ destruct 2620 [1,4: %{true} % // 2621 3: %{false} % // 2622  %{(eq_bv 8 (zero 8) by)} % // 2623 ] 2624  whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?) 2625 normalize nodelta [2: #pc1] whd in ⊢ (???% → ?); #EQ destruct 2626 ] 2627 qed. 2628 2629 lemma eval_cond_ok : 2630 ∀prog. 2631 let trans_prog ≝ ertl_to_ertlptr prog in 2632 ∀stack_sizes. 2633 ∀sigma : sigma_map trans_prog. 2634 ∀st,st',f,fn,a,ltrue,lfalse. 2635 fetch_statement ERTL_semantics … 2636 (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) = 2637 return 〈f, fn, sequential … (COND ERTL … a ltrue) lfalse〉 → 2638 eval_state ERTL_semantics 2639 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2640 (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 2641 (sigma_state_pc ? sigma st) = 2642 return st' → 2643 as_costed (ERTL_status prog stack_sizes) 2644 st' → 2645 ∃ st''. st' = sigma_state_pc ? sigma st'' ∧ 2646 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) 2647 st st''. 2648 bool_to_Prop (taaf_non_empty … taf). 2649 #prog #stack_size #sigma #st #st' #f #fn #a #lb_t #lb_f 2650 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta 2651 @if_elim 2652 [ #EQbl whd in match dummy_state_pc; whd in match null_pc; 2653 whd in match fetch_statement; whd in match fetch_internal_function; 2654 normalize nodelta >(fetch_function_no_zero ??????) [2: %] 2655 whd in ⊢ (??%% → ?); #EQ destruct ] 2656 #Hbl inversion(fetch_internal_function ???) 2657 [2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; 2658 whd in match fetch_statement; whd in match fetch_internal_function; 2659 normalize nodelta >(fetch_function_no_zero ??????) [2: %] 2660 whd in ⊢ (??%% → ?); #EQ destruct] 2661 * #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) EQ #fn1_spec normalize nodelta 2662 #EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec 2663 >m_return_bind #H @('bind_inversion H) H #stmt' #_ whd in ⊢ (??%% → ?); 2664 #EQ destruct whd in match eval_state; whd in match eval_statement_no_pc; 2665 whd in match eval_statement_advance; whd in match sigma_state_pc in ⊢ (% → ?); 2666 normalize nodelta @if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta 2667 >EQf >m_return_bind normalize nodelta >m_return_bind 2668 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H #bv 2669 change with (ps_reg_retrieve ?? = ? → ?) whd in match set_no_pc; 2670 whd in match sigma_state in ⊢ (??(?%?)? → ?); normalize nodelta #bv_spec 2671 #H @('bind_inversion H) H * #EQbv normalize nodelta 2672 [ whd in match goto; normalize nodelta >pc_of_label_eq [2: assumption 3:] 2673 >m_return_bind whd in match pc_of_point; normalize nodelta whd in ⊢ (??%% → ?); 2674 whd in match set_pc; normalize nodelta #EQ destruct 2675  whd in match next; whd in match set_pc; normalize nodelta whd in match (succ_pc ???); 2676 whd in match (point_of_succ ???); whd in ⊢ (??%% → ?); #EQ destruct 2677 ] 2678 whd in match as_costed; normalize nodelta * #n_cost % 2679 [1,3: % [1,4: @st 2680 2,5: @(mk_program_counter 2681 (pc_block (pc ERTLptr_semantics st)) 2682 (offset_of_point ERTL_semantics ?)) [ @lb_t  @lb_f] 2683 3,6: @(last_pop ? st) 2684 ] 2685 ] 2686 % [1,3: whd in match sigma_state_pc; normalize nodelta @if_elim 2687 [1,3: #EQ >EQ in Hbl; *] #_ >fn1_spec %] 2688 %{(taaf_step_jump … (taa_base …) …) I} 2689 lapply (fetch_statement_commute prog sigma … stack_size … EQf) 2690 normalize nodelta #EQf' 2691 [1,4: whd in match as_costed; normalize nodelta >as_label_ok [2,4: @sigma] 2692 % #H @n_cost <H whd in match sigma_state_pc; normalize nodelta 2693 @if_elim [1,3: #EQ >EQ in Hbl; *] #_ >fn1_spec % 2694 2,5: whd in match as_classifier; normalize nodelta whd in match (as_classify ??); 2695 normalize nodelta >EQf' % 2696 *: whd in match (as_execute ???); whd in match eval_state; normalize nodelta 2697 >EQf' >m_return_bind whd in match eval_statement_no_pc; normalize nodelta 2698 >m_return_bind whd in match eval_statement_advance; normalize nodelta 2699 change with (ps_reg_retrieve ??) in ⊢ (??(????(????%?))?); 2700 cases(ps_reg_retrieve_ok ????? ? bv_spec) #bv' * #bv_spec' #bv_bv' 2701 >bv_spec' >m_return_bind >bv_bv' in EQbv; #EQbv 2702 cases(bool_of_beval_ok ? sigma ? ? EQbv) #b1 * #b1_spec #EQ destruct 2703 >b1_spec >m_return_bind normalize nodelta [2: %] whd in match goto; 2704 normalize nodelta whd in match set_no_pc; normalize nodelta 2705 >pc_of_label_eq 2706 [ % 2707  lapply(fetch_internal_function_transf ????????) 2708 [3: @f 2: @fn  whd in ⊢ (???%); <fn1_spec in ⊢ (???%); % 2709   #vars @translate_internal 9: #EQ >EQ in ⊢ (??%?); % *:] 2710  2711 ] 2712 ] 2713 qed. 2714 2715 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 2716 ex1_intro: ∀ x:A. P x → ex_Type1 A P. 2717 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) 2718 2719 lemma 2720 find_funct_ptr_none: 2721 ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). 2722 ∀b: block. 2723 find_funct_ptr ? (globalenv … iV p) b = None ? → 2724 find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?. 2725 #A #B #V #i #p #transf #b 2726 whd in match find_funct_ptr; normalize nodelta 2727 cases b b * normalize nodelta [#x #_ %] * normalize nodelta 2728 [1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta 2729 whd in match globalenv_allocmem; normalize nodelta 2730 cases daemon (*forse e' falso *) 2731 qed. 2732 2430 2733 2431 2734
Note: See TracChangeset
for help on using the changeset viewer.