Ignore:
Timestamp:
Feb 5, 2013, 10:49:42 PM (8 years ago)
Author:
piccolo
Message:

ERTLtoERTLptr in place.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2601 r2604  
    2020include "common/ExtraMonads.ma".
    2121
    22 axiom getLocalsFromId : ident → list register.
    23 
    2422definition ERTL_status ≝
    2523λprog : ertl_program.λstack_sizes.
    … …  
    3028joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
    3129
    32 definition sigma_map ≝ λ prog : ertlptr_program.
    33 joint_closed_internal_function ERTLptr (prog_var_names … prog) → label → option label.
     30definition sigma_map ≝ λ prog : ertl_program.
     31joint_closed_internal_function ERTL (prog_var_names … prog) → label → option label.
     32
    3433
    3534definition sigma_pc_opt :
    36 ∀ prog : ertlptr_program.
     35∀ prog : ertl_program.
    3736sigma_map prog → program_counter → option program_counter ≝
    3837λprog,sigma,pc.
    … …  
    5251     
    5352definition sigma_beval :
    54  ∀prog : ertlptr_program.
     53 ∀prog : ertl_program.
    5554  sigma_map prog →
    5655  beval → beval ≝
    … …  
    6968*)
    7069definition sigma_is :
    71  ∀prog : ertlptr_program.
     70 ∀prog : ertl_program.
    7271  sigma_map prog →
    7372  internal_stack → internal_stack ≝
    … …  
    129128
    130129definition sigma_mem :
    131  ∀prog : ertlptr_program . sigma_map prog → bemem → bemem ≝
     130 ∀prog : ertl_program . sigma_map prog → bemem → bemem ≝
    132131 λprog,sigma,m.
    133132 mk_mem
    … …  
    727726map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
    728727#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 %
    732741]
    733742qed.
    … …  
    775784
    776785definition sigma_register_env :
    777 ∀prog : ertlptr_program.∀sigma : (sigma_map prog).
     786∀prog : ertl_program.∀sigma : (sigma_map prog).
    778787register_env beval → list register →  register_env beval ≝
    779788λprog,sigma,psd_env,ids.
    780789let m' ≝  map ??? psd_env (λbv.sigma_beval prog sigma bv) in
    781 m' ∩ ids.
     790m' ∖ ids.
    782791
    783792(*
    … …  
    805814
    806815
     816lemma 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
    807821(*
    808822lemma clean_add : ∀tag,A,m,i,v.clean … (add tag A m i v) = add tag A (clean … m) i v.
    … …  
    938952lemma merge_eq : ∀A.∀p : positive_map A.∀choice. merge
    939953*)
     954(*
    940955lemma add_restrict : ∀tag,A,B.∀a : identifier_map tag A. ∀b : identifier_map tag B.
    941956∀i,v.i∈b → add tag A (a ∩ b) i v = (add tag A a i v) ∩ b.
    … …  
    980995whd in ⊢ (??%%); @eq_f @add_restrict assumption
    981996qed.
    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*)
     998lemma 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]
     1043qed.     
     1044
     1045lemma 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
     1050cases (lookup tag A a id) normalize [ %] #a @eq_f @add_set_minus assumption
     1051qed.
     1052
     1053
     1054record good_state_transformation
     1055(prog : ertl_program)
     1056(def_in : joint_closed_internal_function ERTL (prog_var_names ?? prog)) :
     1057Type[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
     1082definition get_internal_function_from_ident :
     1083∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
     1084ident → 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');
     1089return fn.
     1090
     1091definition get_sigma_from_good_state :
     1092∀prog : ertl_program.
     1093(∀ fn : joint_closed_internal_function ERTL (prog_var_names ?? prog).
     1094good_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                          ]);
     1106return res.
     1107
     1108
     1109definition sigma_frames : ∀prog : ertl_program.
     1110(∀fn.good_state_transformation prog fn) →
     1111list (register_env beval × ident) → (list (register_env beval × ident)) ≝
     1112λprog,good,frms.
     1113let sigma ≝ get_sigma_from_good_state … good in
     1114foldr ??
     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
    9871125
    9881126(*
    … …  
    10181156
    10191157definition sigma_hw_register_env :
    1020 ∀prog: ertlptr_program. ∀sigma : (sigma_map prog).
     1158∀prog: ertl_program. ∀sigma : (sigma_map prog).
    10211159hw_register_env → hw_register_env ≝
    10221160λprog,sigma,h_reg.mk_hw_register_env
    … …  
    10251163
    10261164definition sigma_regs :
    1027 ∀prog : ertlptr_program. ∀sigma : (sigma_map prog).
     1165∀prog : ertl_program. ∀sigma : (sigma_map prog).
    10281166(register_env beval)×hw_register_env→ list register →
    10291167(register_env beval)×hw_register_env ≝
    … …  
    10691207*)
    10701208
    1071 definition sigma_state :
    1072  ∀prog : ertlptr_program.
    1073  ∀sigma : sigma_map prog.
     1209definition sigma_state : ∀prog : ertl_program.
     1210(∀fn.good_state_transformation prog fn) →
    10741211 state ERTLptr_semantics → list register →
    10751212 state ERTL_semantics ≝
    1076 λprog,sigma,st,ids.
     1213λprog,good,st,ids.
     1214let sigma ≝ get_sigma_from_good_state … good in
    10771215mk_state ?
    1078   (sigma_frames prog sigma (st_frms … st))
    1079   (sigma_is prog sigma (istack … st))
     1216  (sigma_frames prog good (st_frms ERTLptr_semantics st))
     1217  (sigma_is ? sigma (istack … st))
    10801218  (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
    10831222
    10841223definition dummy_state : state ERTL_semantics ≝
    … …  
    10891228mk_state_pc ? dummy_state (null_pc one) (null_pc one).
    10901229
    1091 check fetch_internal_function
    1092 
    10931230definition sigma_state_pc :
    10941231∀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) →
    10971233state_pc ERTLptr_semantics →
    10981234 state_pc ERTL_semantics ≝
    1099 λprog,sigma,st.
    1100   let trans_prog ≝ ertl_to_ertlptr prog in
     1235λprog,good,st.
     1236  let sigma ≝ get_sigma_from_good_state … good in
    11011237  let ge ≝ globalenv_noinit … prog in
    11021238  if eqZb       (block_id (pc_block (pc … st))) (-1) then (* check for dummy pc *)
    11031239    dummy_state_pc
    11041240  else
    1105   match    (fetch_internal_function (joint_closed_internal_function ERTL
    1106                 (prog_var_names (joint_function ERTL) ℕ prog)) ge (pc_block (pc … st))) with
     1241  match (fetch_internal_function (joint_closed_internal_function ERTL
     1242         (prog_var_names (joint_function ERTL) ℕ prog)) ge (pc_block (pc … st))) with
    11071243   [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))
    11101247   |Error msg ⇒ dummy_state_pc].
    11111248
    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_env2
    1122 whd in match reg_store; whd in match update; normalize nodelta
    1123 #psd_env2_spec
    1124 % [ @hide_prf whd in psd_env2_spec : (??%%);
    1125     inversion (update beval ???) in psd_env2_spec; normalize nodelta
    1126     [#_ #ABS destruct] #pos_map #pos_map_spec #EQ destruct
    1127     * #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) assumption
    1131     | #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 nodelta
    1136     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 #prf2
    1151 whd in match ps_reg_store; normalize nodelta
    1152 @mfr_bind [3: @(reg_store_sigma_commute prog sigma id bv ? ? ?) |*:]
    1153 #m #wf_m @mfr_return % [assumption] cases prf2 #_ #H @H
    1154 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 #prf
    1164 whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
    1165 @opt_to_res_preserve #bv #H lapply((proj1 … prf))
    1166 whd in match well_formed_ertl_psd_env; normalize nodelta #H1
    1167 %{(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 destruct
    1180 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 daemon
    1190 qed. (*help for bit_vector_trie*)
    1191 
    1192 check hw_reg_store
    1193 
    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 daemon
    1203 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_regs
    1214 whd in match ertl_eval_move; normalize nodelta
    1215 @mfr_bind
    1216   [2: #bv @sigma_beval assumption |
    1217   |   cases arg_mv [#mv_dst1 | #b] normalize nodelta
    1218     [ cases mv_dst1 [#r | #b] normalize nodelta
    1219       [@ps_reg_retrieve_commute | @hw_reg_retrieve_commute]
    1220     | @mfr_return normalize % #EQ destruct
    1221     ]
    1222   | #bv #prf cases mv_dst [#r | #r] normalize nodelta
    1223     [@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 nodelta
    1233 [ @hide_prf % [2: cases prf1 #_ #x assumption] ]
    1234 whd in match set_psd_regs; normalize nodelta
    1235 [ 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 destruct
    1238   | * #EQ
    1239   >(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 @H1
    1242    [% @id|assumption]
    1243   ]
    1244 | whd in match sigma_regs; whd in match sigma_ertl_psd_env; normalize nodelta
    1245  @eq_f2 [2: %] @eq_f2 [2: %] whd in match sigma_register_env; normalize nodelta
    1246  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_push
    1260   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 nodelta
    1265 @opt_safe_elim #val' #EQsigma_val
    1266 %
    1267 [1,3: @hide_prf %
    1268 |*: whd in match sigma_is in ⊢ (???%); normalize nodelta
    1269   @opt_safe_elim #is''
    1270 ] whd in match sigma_is_opt; normalize nodelta
    1271 [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_val
    1277 whd in ⊢ (??%%→?); #EQ destruct(EQ)
    1278 whd in match sigma_is; normalize nodelta
    1279 @opt_safe_elim #is1
    1280 whd in match sigma_is_opt; normalize nodelta
    1281 [ #H @('bind_inversion H) #bv1''
    1282   >EQ_bv1' #EQ destruct(EQ) ]
    1283 whd in ⊢ (??%%→?); #EQ destruct(EQ) %
    1284 qed.
    1285 
    1286 check internal_stack
    1287 check BVpc
    1288 
    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 with
    1293 [ empty_is ⇒ return empty_is
    1294 | one_is bv ⇒ return one_is bv
    1295 | 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_st
    1310   [2: @mfr_bind
    1311     [3: whd in match push_ra; normalize nodelta @mfr_bind
    1312       [3: whd in match sigma_state_pc; whd in match push; whd in match sigma_state;
    1313           normalize nodelta @mfr_bind
    1314         [#is @(sigma_is_not_head_opt prog sigma is ≠ None ?)
    1315         |#is #prf @(opt_safe … prf)
    1316         |
    1317  
    1318  
    1319   #x #x_spec @mfr_bind
    1320 [ @(λ_.True) | #st * @(sigma_state prog sigma st) |
    1321   [3: cases kind normalize nodelta whd in match push_ra; normalize nodelta
    1322     [ whd in match sigma_state_pc; normalize nodelta #st #st_spec
    1323 *)
    13241249
    13251250definition ERTLptrStatusSimulation :
    13261251∀ prog : ertl_program.
    13271252let trans_prog ≝ ertl_to_ertlptr prog in
    1328 ∀stack_sizes.
    1329 sigma_map trans_prog →
     1253∀stack_sizes.(∀fn.good_state_transformation prog fn) →
    13301254status_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 ??
    13321258    (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes
    13331259       .λ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
    13361263               .as_classifier (ERTL_status prog stack_sizes) s cl_call
    13371264       .λs2:Σs:ERTLptr_status trans_prog stack_sizes
    13381265                .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
    13411269          (pc
    13421270           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes)
    … …  
    14731401*)
    14741402
    1475 lemma ps_reg_retrieve_ok :  ∀prog : ertlptr_program.
     1403lemma ps_reg_retrieve_ok :  ∀prog : ertl_program.
    14761404∀sigma : sigma_map prog. ∀r,restr.
    14771405preserving1 ?? res_preserve1 …
    … …  
    14831411whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1
    14841412whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta
    1485 >lookup_restrict @if_elim [2: #_ @opt_preserve_none1] #id_r_in
     1413>lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in
    14861414>(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1
    14871415#bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec %
    14881416qed.
    14891417
    1490 lemma hw_reg_retrieve_ok : ∀prog : ertlptr_program.
     1418lemma hw_reg_retrieve_ok : ∀prog : ertl_program.
    14911419∀sigma : sigma_map prog. ∀r,restr.
    14921420preserving1 ?? res_preserve1 …
    … …  
    15051433
    15061434
    1507 lemma ps_reg_store_ok : ∀prog : ertlptr_program.
     1435lemma ps_reg_store_ok : ∀prog : ertl_program.
    15081436∀sigma : sigma_map prog. ∀r,restr.
    15091437preserving21 ?? res_preserve1 …
    … …  
    15191447  #x #x_spec lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
    15201448  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) -H
     1449  normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %]
     1450  #id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) -H
    15231451  #x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec
    15241452  whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % //
    … …  
    15291457
    15301458
    1531 lemma hw_reg_store_ok : ∀prog : ertlptr_program.
     1459lemma hw_reg_store_ok : ∀prog : ertl_program.
    15321460∀sigma : sigma_map prog. ∀r,restr.
    15331461preserving21 ?? res_preserve1 …
    … …  
    15441472
    15451473
    1546 lemma ertl_eval_move_ok : ∀prog : ertlptr_program.
     1474lemma ertl_eval_move_ok : ∀prog : ertl_program.
    15471475∀sigma : sigma_map prog. ∀ restr,pm.
    15481476preserving1 ?? res_preserve1 …
    … …  
    15611489qed.
    15621490
    1563 lemma ps_arg_retrieve_ok : ∀prog : ertlptr_program.
     1491lemma ps_arg_retrieve_ok : ∀prog : ertl_program.
    15641492∀sigma : sigma_map prog. ∀a,restr.
    15651493preserving1 ?? res_preserve1 …
    … …  
    15781506lemma pop_ok :
    15791507∀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.
    15841510preserving1 ?? res_preserve1 ????
    1585    (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
     1511   (λst.sigma_state prog good st restr)
    15861512   (λ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〉)
    15891516   (pop ERTL_semantics)
    15901517   (pop ERTLptr_semantics).
    1591 #prog #sigma #stack_size #fn whd in match pop; normalize nodelta #st @mfr_bind1
     1518#prog #good #restr whd in match pop; normalize nodelta #st @mfr_bind1
    15921519[@(λ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 〉)
    15951523| whd in match is_pop; normalize nodelta whd in match sigma_state; normalize nodelta
    15961524  cases(istack ? st) normalize nodelta
    … …  
    16051533lemma push_ok :
    16061534∀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.
    16111537preserving21 ?? 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)
    16151541     (push ERTL_semantics)
    16161542     (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]
    16181550qed.
    16191551
    16201552lemma be_opaccs_ok :
    1621 ∀prog : ertlptr_program. ∀sigma : sigma_map prog.
     1553∀prog : ertl_program. ∀sigma : sigma_map prog.
    16221554∀ op.
    16231555preserving21 ?? res_preserve1 ??????
    … …  
    16291561    (be_opaccs op)
    16301562    (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
     1564whd 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: % [%] % |]
     1582qed.
     1583
     1584lemma be_op1_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
    16351585∀ op.
    16361586preserving1 ?? res_preserve1 …
    … …  
    16391589     (be_op1 op)
    16401590     (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]
     1601qed.
     1602
     1603lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') →
     1604res_preserve1 X Y F n (Error … e).
     1605#X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1
     1606qed.
     1607
     1608
     1609lemma be_op2_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
    16451610∀ b,op.
    16461611preserving21 ?? res_preserve1 …
    … …  
    16501615     (be_op2 b op)
    16511616     (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
     1618cases bv
     1619[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
     1620normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
     1621normalize nodelta
     1622cases 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]
     1630normalize 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: #bo|2,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: #bo|2,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]
     1704qed.
     1705
     1706lemma pointer_of_address_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
    16561707preserving1 … res_preserve1 …
    16571708     (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog sigma bv1,
    … …  
    16591710     (λx.x)
    16601711     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;
     1713whd in match pointer_of_bevals; normalize nodelta
     1714cases bv1 normalize nodelta
     1715[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
     1716try @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
     1724qed.
     1725
     1726lemma beloadv_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
    16651727∀ptr.
    16661728preserving1 … opt_preserve1 …
    … …  
    16691731     (λm.beloadv m ptr)
    16701732     (λ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;
     1734normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
     1735whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
     1736@if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?);
     1737normalize 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* %
     1742qed.
     1743
     1744lemma bestorev_ok : ∀prog : ertl_program.∀sigma : sigma_map prog.
    16751745∀ptr.
    16761746preserving21 … opt_preserve1 …
    … …  
    16801750    (λm.bestorev m ptr)
    16811751    (λ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;
     1753normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
     1754whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
     1755@if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *]
     1756whd 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]
     1826qed.
     1827
     1828lemma 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)) →
     1831P ((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]
     1834qed.
     1835
     1836
     1837lemma 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)
    16901842      (λx.x)
    16911843      (sp ERTL_semantics)
    16921844      (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
     1846whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state;
     1847normalize nodelta whd in match sigma_regs; normalize nodelta
     1848cases(regs ? st) #psd_r #hw_r normalize nodelta
     1849inversion(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
     1851whd in match sigma_hw_register_env; normalize nodelta
     1852change with (sigma_beval ? (get_sigma_from_good_state … good) BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?);
     1853>lookup_map >lookup_map
     1854cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef)
     1855[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
     1856whd 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]
     1870qed.
     1871
     1872lemma set_sp_ok :  ∀prog : ertl_program.
     1873∀good : (∀fn.good_state_transformation prog fn).
     1874∀restr.∀ptr,st.
     1875set_sp ? ptr (sigma_state prog good st restr) =
     1876sigma_state prog good (set_sp ? ptr st) restr.
    17041877cases daemon
    17051878qed.
    … …  
    17071880lemma eval_seq_no_pc_no_call_ok :
    17081881∀prog : ertl_program.
    1709   let trans_prog ≝ ertl_to_ertlptr prog in
    1710 ∀stack_size.∀sigma : sigma_map trans_prog.
    1711 ∀id. ∀fn : (joint_closed_internal_function ??) .∀seq.
     1882let 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.
    17121885   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))))
    17151888      (eval_seq_no_pc ERTL_semantics
    17161889             (globals (mk_prog_params ERTL_semantics prog stack_size))
    … …  
    17181891      (eval_seq_no_pc ERTLptr_semantics
    17191892  (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 *
    17221895whd in match eval_seq_no_pc; normalize nodelta
    17231896[ #c #st @mfr_return1
    … …  
    17251898| #pm #st whd in match pair_reg_move; normalize nodelta
    17261899  @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 %
    17301902  ]
    17311903| #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 |
    17361905  | * #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 |
    17391907    | #regs  @mfr_return_eq1 %
    17401908    ]
    17411909  ]
    17421910| #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 |
    17451912  | #bv @push_ok
    17461913  ]
    … …  
    17521919  change with ((dph_reg ERTL) → ?)
    17531920  #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))))
    17551922  | 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'
    17591925       >(find_symbol_transf …
    17601926          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
    17611927       >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 …))
    17631929                                               in ⊢ (???????(?????%?)?);
    1764        @ps_reg_store_ok
     1930       @ps_reg_store_ok |
    17651931    | #regs  @mfr_return_eq1 %
    17661932    ]
    … …  
    17691935          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
    17701936    >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 …))
    17741939                                               in ⊢ (???????(?????%?)?);
    1775       @ps_reg_store_ok
     1940      @ps_reg_store_ok |
    17761941    | #regs  @mfr_return_eq1 %
    17771942    ]
    17781943  ]
    17791944| #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 |
    17831947  | #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 |
    17871950   | #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 |
    17921952     | * #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))))
    17941954       | 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 |
    17971956         | #regs  @mfr_return_eq1 %
    17981957         ]
    17991958       | #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 nodelta
    1802             @ps_reg_store_ok
    1803          | #regs  @mfr_return_eq1 %         ]
     1959         [2: whd in match sigma_state; normalize nodelta
     1960            @ps_reg_store_ok |
     1961         | #regs  @mfr_return_eq1 %
     1962         ]         
    18041963       ]
    18051964     ]
    … …  
    18071966  ] 
    18081967| #op #r1 #r2 #st @mfr_bind1
    1809   [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1968  [ @(sigma_beval prog (get_sigma_from_good_state … good))
    18101969  | whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok
    18111970  | #bv1 @mfr_bind1
    1812     [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1971    [ @(sigma_beval prog (get_sigma_from_good_state … good))
    18131972    | @be_op1_ok
    18141973    | #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 |
    18171975      | #regs  @mfr_return_eq1 %
    18181976      ]
    … …  
    18201978  ]
    18211979| #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 |
    18241981  | #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 |
    18271983    | #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 |
    18301985      | * #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))))
    18321987        | 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 |
    18351989          | #regs  @mfr_return_eq1 %
    18361990          ]
    … …  
    18431997| #st  @mfr_return_eq1 %
    18441998| #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 |
    18472000  | #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 |
    18502002    | #bv1 @mfr_bind1
    18512003      [ @(λx.x)
    1852       | @(pointer_of_address_ok ? sigma 〈bv1,bv〉)
     2004      | @(pointer_of_address_ok ? ? 〈bv1,bv〉)
    18532005      | #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 |
    18562007        | #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 |
    18592009          | #regs  @mfr_return_eq1 %
    18602010          ]
    … …  
    18642014  ] 
    18652015| #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 |
    18682017  | #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 |
    18712019    | #bv1 @mfr_bind1
    18722020      [ @(λx.x)
    1873       |  @(pointer_of_address_ok ? sigma 〈bv1,bv〉)
     2021      |  @(pointer_of_address_ok ? ? 〈bv1,bv〉)
    18742022      | #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 |
    18772024        | #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 |
    18802026          | #m @mfr_return_eq1 %
    18812027          ]
    … …  
    18952041    | #r whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
    18962042      [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 ⊢ (???????(??%?)?);
    18982045          @ps_reg_store_ok
    18992046      |
    … …  
    19042051]
    19052052qed.
     2053
     2054
     2055xxxxxxxxxxxxxxxxx
    19062056
    19072057lemma fetch_statement_commute :
    … …  
    20542204
    20552205lemma pc_of_label_eq :
     2206  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
    20562207  ∀globals,ge,bl,i_fn,lbl.
    20572208  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
     2212whd in match pc_of_label;
     2213normalize nodelta >EQf >m_return_bind %
    20622214qed.
    20632215
    … …  
    22382390[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
    22392391  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 ]
    22432394#Hbl inversion(fetch_internal_function ???)
    22442395[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
    … …  
    22572408#H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
    22582409* #st1 #pc1 #EQpop whd in match next_of_call_pc; normalize nodelta
    2259 >m_bind_bind #H @('bind_inversion H) -H ** #f1 #fn2 * normalize nodelta
     2410>m_bind_bind #H @('bind_inversion H) -H ** #f1 #fn1 * normalize nodelta
    22602411[ * [ #c_id #args #dest | #r #lbl | #seq ] #nxt | #fin | * ]
    22612412#EQf1 normalize nodelta [2,3,4: whd in ⊢ (??%% → ?); #EQ destruct]
    … …  
    22642415normalize nodelta #EQf'
    22652416% [ whd in match joint_classify; normalize nodelta >EQf' >m_return_bind %]
    2266 cases(pop_ra_ok ? sigma  stack_size ??? EQpop) * #st3 #pc3 * #st3_spec
     2417change with (pop_ra ?? = ?) in EQpop; whd in match set_no_pc in EQpop;
     2418normalize nodelta in EQpop;
     2419cases(pop_ra_ok ? sigma  stack_size fn ?? EQpop) * #st3 #pc3 * #st3_spec
    22672420normalize nodelta #EQ destruct whd in match set_last_pop; whd in match succ_pc;
    22682421normalize nodelta whd in match (point_of_succ ???);
    … …  
    22782431          normalize nodelta whd in match sigma_pc_opt; normalize nodelta
    22792432           >bl3_spec normalize nodelta assumption
    2280         | #bl3_spec #H @('bind_inversion H) -H * #fn4 #id4
     2433        | #bl3_spec #H @('bind_inversion H) -H * #id4 #fn4
    22812434          #H lapply(res_eq_from_opt ??? H) -H #fn4_spec
    22822435          #H @('bind_inversion H) -H #lbl4 #lbl4_spec whd in ⊢ (??%? → ?); #EQ
    … …  
    22922445       |3: >(fetch_internal_function_transf … fn3_spec) % |*:]
    22932446       #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
     2450qed.
     2451
     2452(*
     2453lemma ertl_allocate_local_ok : ∀ prog : ertl_program.
     2454let trans_prog ≝ ertl_to_ertlptr prog in
     2455∀sigma : sigma_map.
     2456∀stack_size.
     2457∀id,regs.
     2458ertl_allocate_local id (sigma_regs ? sigma getLocalsFromId(
     2459*)
    23002460
    23012461lemma eval_tailcall_ok :
    … …  
    23192479  eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
    23202480    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
     2482whd 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
     2499whd in match eval_state; normalize nodelta >EQf >m_return_bind
     2500whd in match eval_statement_no_pc; whd in match eval_statement_advance;
     2501normalize nodelta >m_return_bind whd in match eval_tailcall;
     2502normalize nodelta #H @('bind_inversion H) -H #bl whd in match set_no_pc;
     2503normalize 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
     2510whd 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
     2512whd in match(setup_call ???????); >m_return_bind
     2513whd in ⊢ (??%% → ?); #EQ destruct whd in match sigma_state in ⊢ (% → ?);
     2514normalize  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*)
     2538qed.
     2539   
     2540   
     2541   
     2542   
    23662543lemma as_label_ok : ∀ prog : ertl_program.
    23672544let trans_prog ≝ ertl_to_ertlptr prog in
    … …  
    24282605cases daemon
    24292606qed.
     2607
     2608lemma bool_of_beval_ok : ∀prog : ertlptr_program.
     2609∀sigma : sigma_map prog.
     2610preserving1 … 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]
     2618try @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]
     2627qed.
     2628
     2629lemma eval_cond_ok :
     2630∀prog.
     2631let 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' →
     2643as_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)
     2647st st''.
     2648bool_to_Prop (taaf_non_empty … taf).
     2649#prog #stack_size #sigma #st #st' #f #fn #a #lb_t #lb_f
     2650whd 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;
     2665whd in match eval_statement_advance; whd in match sigma_state_pc in ⊢ (% → ?);
     2666normalize 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
     2669change with (ps_reg_retrieve ?? = ? → ?) whd in match set_no_pc;
     2670whd 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]
     2678whd 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}
     2689lapply (fetch_statement_commute prog sigma … stack_size … EQf)
     2690normalize 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]
     2713qed.
     2714       
     2715inductive 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
     2719lemma
     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
     2726whd in match find_funct_ptr; normalize nodelta
     2727cases b -b * normalize nodelta [#x #_ %] * normalize nodelta
     2728[1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta
     2729whd in match globalenv_allocmem; normalize nodelta
     2730cases daemon (*forse e' falso *)
     2731qed.
     2732
    24302733
    24312734
Note: See TracChangeset for help on using the changeset viewer.