Changeset 2332 for src/Clight/switchRemoval.ma
- Timestamp:
- Sep 12, 2012, 12:36:46 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2304 r2332 2 2 include "Clight/fresh.ma". 3 3 include "basics/lists/list.ma". 4 include "basics/lists/listb.ma". 4 5 include "common/Identifiers.ma". 6 include "utilities/extralib.ma". 5 7 include "Clight/Cexec.ma". 6 8 include "Clight/CexecInd.ma". 7 9 include "Clight/frontend_misc.ma". 8 include "Clight/casts.ma". (* lemmas related to bitvectors ... *) 9 10 (* 11 include "Clight/maps_obsequiv.ma". 12 *) 13 10 include "Clight/memoryInjections.ma". 14 11 15 12 (* ----------------------------------------------------------------------------- … … 145 142 | 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/ 146 143 ] qed. 147 148 (* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *)149 (*150 let rec produce_cond151 (e : expr)152 (switch_cases : stlist)153 (def_case : ident × sf_statement)154 (exit : label) on switch_cases : sf_statement × label ≝155 match switch_cases with156 [ nil ⇒157 match def_case with158 [ mk_Prod default_label default_statement ⇒159 〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉160 ]161 | cons switch_case tail ⇒162 let 〈case_label, case_value, case_statement〉 ≝ switch_case in163 match case_value with164 [ mk_DPair sz val ⇒165 let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in166 (* let test ≝ Expr (Ebinop Oeq e e) (Tint I32 Unsigned) in *)167 (* let test ≝ Expr (Econst_int I32 (bvzero 32)) (Tint I32 Signed) in *)168 let 〈sub_statement, sub_label〉 ≝ produce_cond e tail def_case exit in169 let result ≝170 Sifthenelse test171 (Slabel case_label172 (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)173 (Sgoto sub_label)))174 (pi1 … sub_statement)175 in176 〈«result, ?», case_label〉177 ]178 ].179 [ 1: normalize @convert_break_lift elim default_statement //180 | 2: whd @conj normalize try @conj try //181 [ 1: @convert_break_lift elim case_statement //182 | 2: elim sub_statement // ]183 ] qed. *)184 185 (* We assume that the expression e is consistely typed w.r.t. the switch branches *)186 (*187 let rec produce_cond2188 (e : expr)189 (switch_cases : stlist)190 (def_case : ident × sf_statement)191 (exit : label) on switch_cases : sf_statement × label ≝192 match switch_cases with193 [ nil ⇒194 let 〈default_label, default_statement〉 ≝ def_case in195 〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉196 | cons switch_case tail ⇒197 let 〈case_label, case_value, case_statement〉 ≝ switch_case in198 match case_value with199 [ mk_DPair sz val ⇒200 let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in201 let 〈sub_statement, sub_label〉 ≝ produce_cond2 e tail def_case exit in202 let case_statement_res ≝203 Sifthenelse test204 (Slabel case_label205 (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)206 (Sgoto sub_label)))207 Sskip208 in209 〈«Ssequence case_statement_res (pi1 … sub_statement), ?», case_label〉210 ]211 ].212 [ 1: normalize @convert_break_lift elim default_statement //213 | 2: whd @conj214 [ 1: whd @conj try // whd in match (switch_free ?); @conj215 [ 1: @convert_break_lift elim case_statement //216 | 2: // ]217 | 2: elim sub_statement // ]218 ] qed. *)219 144 220 145 (* (def_case : ident × sf_statement) *) … … 846 771 qed. 847 772 848 (*849 lemma switch_removal_fresh : ∀i,s,u.850 fresh_for_univ ? i u →851 fresh_for_univ ? i (\snd (switch_removal s u)).852 #i #s @(statement_ind2 ? (λls. ∀u. fresh_for_univ ? i u →853 fresh_for_univ ? i (\snd (switch_removal_branches ls u))) … s)854 try //855 [ 1: #s1' #s2' #Hind1 #Hind2 #u #Hyp856 whd in match (switch_removal (Ssequence s1' s2') u);857 lapply (Hind1 u Hyp) elim (switch_removal s1' u)858 * #irr1 #irr2 #uA #HuA normalize nodelta859 lapply (Hind2 uA HuA) elim (switch_removal s2' uA)860 * #irr3 #irr4 #uB #HuB normalize nodelta //861 | 2: #e #s1' #s2' #Hind1 #Hind2 #u #Hyp862 whd in match (switch_removal (Sifthenelse e s1' s2') u);863 lapply (Hind1 u Hyp) elim (switch_removal s1' u)864 * #irr1 #irr2 #uA #HuA normalize nodelta865 lapply (Hind2 uA HuA) elim (switch_removal s2' uA)866 * #irr3 #irr4 #uB #HuB normalize nodelta //867 | 3,4: #e #s' #Hind #u #Hyp868 whd in match (switch_removal ? u);869 lapply (Hind u Hyp) elim (switch_removal s' u)870 * #irr1 #irr2 #uA #HuA normalize nodelta //871 | 5: #s1' #e #s2' #s3' #Hind1 #Hind2 #Hind3 #u #Hyp872 whd in match (switch_removal (Sfor s1' e s2' s3') u);873 lapply (Hind1 u Hyp) elim (switch_removal s1' u)874 * #irr1 #irr2 #uA #HuA normalize nodelta875 lapply (Hind2 uA HuA) elim (switch_removal s2' uA)876 * #irr3 #irr4 #uB #HuB normalize nodelta877 lapply (Hind3 uB HuB) elim (switch_removal s3' uB)878 * #irr5 #irr6 #uC #HuC normalize nodelta //879 | 6: #e #ls #Hind #u #Hyp880 whd in match (switch_removal (Sswitch e ls) u);881 lapply (Hind u Hyp)882 cases (switch_removal_branches ls u)883 * #irr1 #irr2 #uA #HuA normalize nodelta884 lapply (fresh_for_univ_still_fresh … HuA)885 cases (fresh SymbolTag uA) #v #uA' #Haux lapply (Haux v uA' (refl ? 〈v,uA'〉))886 -Haux #HuA' normalize nodelta887 lapply (simplify_switch_fresh uA' i (Expr (Evar v) (typeof e)) irr1 HuA')888 cases (simplify_switch ???) #stm #uB889 #Haux normalize nodelta //890 | 7,8: #label #body #Hind #u #Hyp891 whd in match (switch_removal ? u);892 lapply (Hind u Hyp) elim (switch_removal body u)893 * #irr1 #irr2 #uA #HuA normalize nodelta //894 | 9: #defcase #Hind #u #Hyp whd in match (switch_removal_branches ??);895 lapply (Hind u Hyp) elim (switch_removal defcase u)896 * #irr1 #irr2 #uA #HuA normalize nodelta //897 | 10: #sz #i0 #s0 #tl #Hind1 #Hind2 #u #Hyp normalize898 lapply (Hind2 u Hyp) elim (switch_removal_branches tl u)899 * #irr1 #irr2 #uA #HuA normalize nodelta900 lapply (Hind1 uA HuA) elim (switch_removal s0 uA)901 * #irr3 #irr4 #uB #HuB //902 ] qed.903 904 lemma switch_removal_branches_fresh : ∀i,ls,u.905 fresh_for_univ ? i u →906 fresh_for_univ ? i (\snd (switch_removal_branches ls u)).907 #i #ls @(labeled_statements_ind2 (λs. ∀u. fresh_for_univ ? i u →908 fresh_for_univ ? i (\snd (switch_removal s u))) ? … ls)909 try /2 by switch_removal_fresh/910 [ 1: #s #Hind #u #Hfresh normalize lapply (switch_removal_fresh ? s ? Hfresh)911 cases (switch_removal s u) * //912 | 2: #sz #i #s #tl #Hs #Htl #u #Hfresh normalize913 lapply (Htl u Hfresh)914 cases (switch_removal_branches tl u) * normalize nodelta915 #ls' #fvs #u' #Hfresh'916 lapply (Hs u' Hfresh')917 cases (switch_removal s u') * //918 ] qed.919 *)920 773 (* ----------------------------------------------------------------------------- 921 774 Simulation proof and related voodoo. … … 984 837 ]. 985 838 986 987 839 (* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched 988 840 by a non-constant number of evaluations in the converted program. More precisely, … … 992 844 (* A version of simplify_switch hiding the ugly projs *) 993 845 definition fresh_for_expression ≝ 994 λe,u. fresh_for_univ SymbolTag (max_of_expr e) u.846 λe,u. fresh_for_univ SymbolTag (max_of_expr e) u. 995 847 996 848 definition fresh_for_statement ≝ 997 λs,u. fresh_for_univ SymbolTag (max_of_statement s) u.849 λs,u. fresh_for_univ SymbolTag (max_of_statement s) u. 998 850 999 851 (* needed during mutual induction ... *) 1000 852 definition fresh_for_labeled_statements ≝ 1001 λls,u. fresh_for_univ ? (max_of_ls ls) u.853 λls,u. fresh_for_univ ? (max_of_ls ls) u. 1002 854 1003 855 definition fresh_for_function ≝ 1004 λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.856 λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u. 1005 857 1006 858 (* misc properties of the max function on positives. *) 1007 1008 lemma max_one_neutral : ∀v. max v one = v.1009 * // qed.1010 859 1011 860 lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v. … … 1016 865 >commutative_max // qed. 1017 866 1018 lemma transitive_le : transitive ? le. // qed.1019 1020 lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.1021 #a #b /2/ qed.1022 1023 (* cycle of length 1 *)1024 lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.1025 * /2 by absurd/ qed.1026 1027 (* cycle of length 2 *)1028 lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False.1029 #a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2))1030 #Heq @(le_S_contradiction_1 a) destruct // qed.1031 1032 (* cycle of length 3 *)1033 lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False.1034 #a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H41035 @(le_S_contradiction_2 … H3 H4)1036 qed.1037 1038 lemma reflexive_leb : ∀a. leb a a = true.1039 #a @(le_to_leb_true a a) // qed.1040 1041 (* This should be somewhere else. *)1042 lemma associative_max : associative ? max.1043 #a #b #c1044 whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);1045 lapply (pos_compare_to_Prop a b)1046 cases (pos_compare a b) whd in ⊢ (% → ?); #Hab1047 [ 1: >(le_to_leb_true a b) normalize nodelta /2/1048 lapply (pos_compare_to_Prop b c)1049 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc1050 [ 1: >(le_to_leb_true b c) normalize nodelta1051 lapply (pos_compare_to_Prop a c)1052 cases (pos_compare a c) whd in ⊢ (% → ?); #Hac1053 [ 1: >(le_to_leb_true a c) /2/1054 | 2: destruct cases (leb c c) //1055 | 3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *)1056 @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac))1057 ]1058 @le_S_weaken //1059 | 2: destruct1060 cases (leb c c) normalize nodelta1061 >(le_to_leb_true a c) /2/1062 | 3: >(not_le_to_leb_false b c) normalize nodelta /2/1063 >(le_to_leb_true a b) /2/1064 ]1065 | 2: destruct (Hab) >reflexive_leb normalize nodelta1066 lapply (pos_compare_to_Prop b c)1067 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc1068 [ 1: >(le_to_leb_true b c) normalize nodelta1069 >(le_to_leb_true b c) normalize nodelta1070 /2/1071 | 2: destruct >reflexive_leb normalize nodelta1072 >reflexive_leb //1073 | 3: >(not_le_to_leb_false b c) normalize nodelta1074 >reflexive_leb /2/ ]1075 | 3: >(not_le_to_leb_false a b) normalize nodelta /2/1076 lapply (pos_compare_to_Prop b c)1077 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc1078 [ 1: >(le_to_leb_true b c) normalize nodelta /2/1079 | 2: destruct >reflexive_leb normalize nodelta @refl1080 | 3: >(not_le_to_leb_false b c) normalize nodelta1081 >(not_le_to_leb_false a b) normalize nodelta1082 >(not_le_to_leb_false a c) normalize nodelta1083 lapply (transitive_le … Hbc (le_S_weaken … Hab))1084 #Hca /2/1085 ]1086 ] qed.1087 1088 867 lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3). 1089 868 * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max // 1090 869 qed. 1091 (* 1092 lemma max_of_expr_rewrite : 1093 ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id. 1094 @(expr_ind2 … (λed,t. ∀id. max_of_expr (Expr ed t) id=max_id (max_of_expr (Expr ed t) (an_identifier SymbolTag one)) id)) 1095 [ 1: #ed #t // ] 1096 [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 1097 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] 1098 #ty 1099 [ 3: * #id_p whd in match (max_of_expr ??); cases var_id #var_p normalize nodelta 1100 whd in match (max_id ??) in ⊢ (???%); 1101 >max_one_neutral // ] 1102 [ 1,2,11: * * // 1103 | 3,4,5,7,13: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); @Hind 1104 | 6,9,10: #Hind1 #Hind2 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); 1105 >(Hind1 (max_of_expr e2 (an_identifier SymbolTag one))) 1106 >max_id_associative 1107 >Hind1 1108 cases (max_of_expr e1 ?) 1109 #v1 <Hind2 @refl 1110 | 8: #Hind1 #Hind2 #Hind3 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); 1111 >Hind1 in ⊢ (??%?); >Hind2 in ⊢ (??%?); >Hind3 in ⊢ (??%?); 1112 >Hind1 in ⊢ (???%); >Hind2 in ⊢ (???%); 1113 >max_id_associative >max_id_associative @refl 1114 | 12: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); 1115 cases field #p normalize nodelta 1116 >Hind cases (max_of_expr e1 ?) #e' 1117 cases id #id' 1118 whd in match (max_id ??); normalize nodelta 1119 whd in match (max_id ??); >associative_max @refl 1120 ] qed. 1121 *) 870 1122 871 lemma fresh_max_split : ∀a,b,u. fresh_for_univ SymbolTag (max_id a b) u → fresh_for_univ ? a u ∧ fresh_for_univ ? b u. 1123 872 * #a * #b * #u normalize … … 1139 888 <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl 1140 889 ] qed. 1141 1142 (* -----------------------------------------------------------------------------1143 Stuff on memory and environments extensions.1144 Let us recap: the memory model of a function is in two layers. An environment1145 (type [env]) maps identifiers to blocks, and a memory maps blocks1146 switch_removal introduces new, fresh variables. What is to be noted is that1147 switch_removal modifies both the contents of the "disjoint" part of memory, but1148 also where the data is allocated. The first solution considered was to consider1149 an extensional equivalence relation on values, saying that equivalent pointers1150 point to equivalent values. This has to be a coinductive relation, in order to1151 take into account cyclic data structures. Rather than using coinductive types,1152 we use the compcert solution, using so-called memory embeddings.1153 ---------------------------------------------------------------------------- *)1154 1155 (* ---------------- *)1156 (* auxillary lemmas *)1157 lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.1158 #a #b #HA1159 lapply (Zltb_true_to_Zlt … HA) #HA_prop1160 @Zlt_to_Zltb_true /2/1161 qed.1162 1163 lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.1164 #a @Zlt_to_Zltb_true /2/ qed.1165 (*1166 definition le_offset : offset → offset → bool.1167 λx,y. Zleb (offv x) (offv y).1168 *)1169 lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.1170 1171 lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.1172 1173 (* When equality on A is decidable, [mem A elt l] is too. *)1174 lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).1175 #A #dec #elt #l elim l1176 [ 1: normalize %2 /2/1177 | 2: #hd #tl #Hind1178 elim (dec elt hd)1179 [ 1: #Heq >Heq %1 /2/1180 | 2: #Hneq cases Hind1181 [ 1: #Hmem %1 /2/1182 | 2: #Hnmem %2 normalize1183 % #H cases H1184 [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)1185 | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]1186 ] ] ]1187 qed.1188 1189 lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.1190 #a #b @(eq_block_elim … a b) /2/ qed.1191 1192 lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.1193 #l #elt1 #elt2 elim l1194 [ 1: normalize #Habsurd @(False_ind … Habsurd)1195 | 2: #hd #tl #Hind normalize #Hl #Hr1196 cases Hl1197 [ 1: #Heq >Heq1198 @(eq_block_elim … hd elt2)1199 [ 1: #Heq >Heq /2 by not_to_not/1200 | 2: #x @x ]1201 | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)1202 [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem21203 | 2: #Hmem2 @Hind //1204 ]1205 ]1206 ] qed.1207 1208 lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.1209 #b1 #b2 * #Hb1210 @(eq_block_elim … b1 b2)1211 [ 1: #Habsurd @(False_ind … (Hb Habsurd))1212 | 2: // ] qed.1213 1214 (* Type of blocks in a particular region. *)1215 definition block_in : region → Type[0] ≝ λrg. Σb. (block_region b) = rg.1216 1217 (* An embedding is a function from blocks to (blocks+offset). *)1218 definition embedding ≝ block → option (block × offset).1219 1220 definition offset_plus : offset → offset → offset ≝1221 λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)).1222 1223 1224 (* Prove that (zero n) is a neutral element for (addition_n n) *)1225 1226 lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.1227 #n #bv whd in match (add_with_carries ????); elim bv //1228 #n #hd #tl #Hind whd in match (fold_right2_i ????????);1229 >Hind normalize1230 cases n in tl;1231 [ 1: #tl cases hd normalize @refl1232 | 2: #n' #tl cases hd normalize @refl ]1233 qed.1234 1235 lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.1236 #n #bv whd in match (addition_n ???);1237 >add_with_carries_n_O //1238 qed.1239 1240 lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o.1241 * #o1242 whd in match (offset_plus ??);1243 >addition_n_0 @refl1244 qed.1245 1246 1247 (* Translates a pointer through an embedding. *)1248 definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝1249 λp,E.1250 match p with1251 [ mk_pointer pblock poff ⇒1252 match E pblock with1253 [ None ⇒ None ?1254 | Some loc ⇒1255 let 〈dest_block,dest_off〉 ≝ loc in1256 let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in1257 Some ? ptr1258 ]1259 ].1260 1261 (* We parameterise the "equivalence" relation on values with an embedding. *)1262 (* Front-end values. *)1263 inductive value_eq (E : embedding) : val → val → Prop ≝1264 | undef_eq : ∀v.1265 value_eq E Vundef v1266 | vint_eq : ∀sz,i.1267 value_eq E (Vint sz i) (Vint sz i)1268 | vfloat_eq : ∀f.1269 value_eq E (Vfloat f) (Vfloat f)1270 | vnull_eq :1271 value_eq E Vnull Vnull1272 | vptr_eq : ∀p1,p2.1273 pointer_translation p1 E = Some ? p2 →1274 value_eq E (Vptr p1) (Vptr p2).1275 1276 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t.1277 * the values are equivalent. *)1278 definition load_sim ≝1279 λ(E : embedding).λ(m1 : mem).λ(m2 : mem).1280 ∀b1,off1,b2,off2,ty,v1.1281 valid_block m1 b1 → (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)1282 E b1 = Some ? 〈b2,off2〉 →1283 load_value_of_type ty m1 b1 off1 = Some ? v1 →1284 (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).1285 1286 definition load_sim_ptr ≝1287 λ(E : embedding).λ(m1 : mem).λ(m2 : mem).1288 ∀b1,off1,b2,off2,ty,v1.1289 valid_pointer m1 (mk_pointer b1 off1) = true → (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)1290 pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) →1291 load_value_of_type ty m1 b1 off1 = Some ? v1 →1292 (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).1293 1294 (* Definition of a memory injection *)1295 record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝1296 { (* Load simulation *)1297 mi_inj : load_sim_ptr E m1 m2;1298 (* Invalid blocks are not mapped *)1299 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;1300 (* Valid pointers are mapped to valid pointers*)1301 mi_valid_pointers : ∀p,p'.1302 valid_pointer m1 p = true →1303 pointer_translation p E = Some ? p' →1304 valid_pointer m2 p' = true;1305 (* Blocks in the codomain are valid *)1306 (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *)1307 (* Regions are preserved *)1308 mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';1309 (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's.1310 * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where1311 * all variables are allocated in the same block. *)1312 mi_disjoint : ∀b1,b2,b1',b2',o1',o2'.1313 b1 ≠ b2 →1314 E b1 = Some ? 〈b1',o1'〉 →1315 E b2 = Some ? 〈b2',o2'〉 →1316 b1' ≠ b2'1317 }.1318 1319 (* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\1320 * A memory extension is a [memory_inj] with some particular blocks designated as1321 * being writeable. *)1322 1323 alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".1324 1325 record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝1326 { me_inj : memory_inj E m1 m2;1327 (* A list of blocks where we can write freely *)1328 me_writeable : list block;1329 (* These blocks are valid *)1330 me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;1331 (* And pointers to m1 are oblivious to these blocks *)1332 me_writeable_ok : ∀p,p'.1333 valid_pointer m1 p = true →1334 pointer_translation p E = Some ? p' →1335 ¬ (meml ? (pblock p') me_writeable)1336 }.1337 1338 (* ---------------------------------------------------------------------------- *)1339 (* End of the definitions on memory injections. Now, on to proving some lemmas. *)1340 1341 (* A particular inversion. *)1342 lemma value_eq_ptr_inversion :1343 ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.1344 #E #p1 #v #Heq inversion Heq1345 [ 1: #v #Habsurd destruct (Habsurd)1346 | 2: #sz #i #Habsurd destruct (Habsurd)1347 | 3: #f #Habsurd destruct (Habsurd)1348 | 4: #Habsurd destruct (Habsurd)1349 | 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct1350 %{p2} @conj try @refl try assumption1351 ] qed.1352 1353 (* A cleaner version of inversion for [value_eq] *)1354 lemma value_eq_inversion :1355 ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →1356 (∀v. P Vundef v) →1357 (∀sz,i. P (Vint sz i) (Vint sz i)) →1358 (∀f. P (Vfloat f) (Vfloat f)) →1359 (P Vnull Vnull) →1360 (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →1361 P v1 v2.1362 #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H51363 inversion Heq1364 [ 1: #v #Hv1 #Hv2 #_ destruct @H11365 | 2: #sz #i #Hv1 #Hv2 #_ destruct @H21366 | 3: #f #Hv1 #Hv2 #_ destruct @H31367 | 4: #Hv1 #Hv2 #_ destruct @H41368 | 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.1369 1370 (* If we succeed to load something by value from a 〈b,off〉 location,1371 [b] is a valid block. *)1372 lemma load_by_value_success_valid_block_aux :1373 ∀ty,m,b,off,v.1374 access_mode ty = By_value (typ_of_type ty) →1375 load_value_of_type ty m b off = Some ? v →1376 Zltb (block_id b) (nextblock m) = true.1377 #ty #m * #brg #bid #off #v1378 cases ty1379 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain1380 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]1381 whd in match (load_value_of_type ????);1382 [ 1,7,8: #_ #Habsurd destruct (Habsurd) ]1383 #Hmode1384 [ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]1385 normalize in match (typesize ?);1386 whd in match (loadn ???);1387 whd in match (beloadv ??);1388 cases (Zltb bid (nextblock m)) normalize nodelta1389 try // #Habsurd destruct (Habsurd)1390 | *: normalize in Hmode; destruct (Hmode)1391 ] qed.1392 1393 (* If we succeed in loading some data from a location, then this loc is a valid pointer. *)1394 lemma load_by_value_success_valid_ptr_aux :1395 ∀ty,m,b,off,v.1396 access_mode ty = By_value (typ_of_type ty) →1397 load_value_of_type ty m b off = Some ? v →1398 Zltb (block_id b) (nextblock m) = true ∧1399 Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧1400 Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.1401 #ty #m * #brg #bid #off #v1402 cases ty1403 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain1404 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]1405 whd in match (load_value_of_type ????);1406 [ 1,7,8: #_ #Habsurd destruct (Habsurd) ]1407 #Hmode1408 [ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]1409 normalize in match (typesize ?);1410 whd in match (loadn ???);1411 whd in match (beloadv ??);1412 cases (Zltb bid (nextblock m)) normalize nodelta1413 cases (Zleb (low (blocks m (mk_block brg bid)))1414 (Z_of_unsigned_bitvector offset_size (offv off)))1415 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brg bid))))1416 normalize nodelta1417 #Heq destruct (Heq)1418 try /3 by conj, refl/1419 | *: normalize in Hmode; destruct (Hmode)1420 ] qed.1421 1422 1423 lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.1424 * #rg #id #m normalize1425 elim id /2/ qed.1426 1427 lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.1428 * #rg #id #m normalize1429 elim id /2/ qed.1430 1431 lemma load_by_value_success_valid_block :1432 ∀ty,m,b,off,v.1433 access_mode ty = By_value (typ_of_type ty) →1434 load_value_of_type ty m b off = Some ? v →1435 valid_block m b.1436 #ty #m #b #off #v #Haccess_mode #Hload1437 @valid_block_from_bool1438 elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //1439 qed.1440 1441 lemma load_by_value_success_valid_pointer :1442 ∀ty,m,b,off,v.1443 access_mode ty = By_value (typ_of_type ty) →1444 load_value_of_type ty m b off = Some ? v →1445 valid_pointer m (mk_pointer b off).1446 #ty #m #b #off #v #Haccess_mode #Hload normalize1447 elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)1448 * #H1 #H2 #H3 >H1 >H2 normalize nodelta1449 >Zle_to_Zleb_true try //1450 lapply (Zlt_to_Zle … (Zltb_true_to_Zlt … H3)) /2/1451 qed.1452 1453 1454 (* Making explicit the contents of memory_inj for load_value_of_type *)1455 lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.1456 memory_inj E m1 m2 →1457 value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →1458 load_value_of_type ty m1 b1 off1 = Some ? v1 →1459 ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.1460 #E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq1461 lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct1462 lapply (refl ? (access_mode ty))1463 cases ty1464 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain1465 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]1466 normalize in ⊢ ((???%) → ?); #Hmode #Hyp1467 [ 1,7,8: normalize in Hyp; destruct (Hyp)1468 | 5,6: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]1469 lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer1470 lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H1471 qed.1472 1473 1474 (* -------------------------------------- *)1475 (* Lemmas pertaining to memory allocation *)1476 1477 (* A valid block stays valid after an alloc. *)1478 lemma alloc_valid_block_conservation :1479 ∀m,m',z1,z2,r,new_block.1480 alloc m z1 z2 r = 〈m', new_block〉 →1481 ∀b. valid_block m b → valid_block m' b.1482 #m #m' #z1 #z2 #r * #b' #Hregion_eq1483 elim m #contents #nextblock #Hcorrect whd in match (alloc ????);1484 #Halloc destruct (Halloc)1485 #b whd in match (valid_block ??) in ⊢ (% → %); /2/1486 qed.1487 1488 (* Allocating a new zone produces a valid block. *)1489 lemma alloc_valid_new_block :1490 ∀m,m',z1,z2,r,new_block.1491 alloc m z1 z2 r = 〈m', new_block〉 →1492 valid_block m' new_block.1493 * #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq1494 whd in match (alloc ????); whd in match (valid_block ??);1495 #Halloc destruct (Halloc) /2/1496 qed.1497 1498 (* All data in a valid block is unchanged after an alloc. *)1499 lemma alloc_beloadv_conservation :1500 ∀m,m',block,offset,z1,z2,r,new_block.1501 valid_block m block →1502 alloc m z1 z2 r = 〈m', new_block〉 →1503 beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).1504 * #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc1505 whd in Halloc:(??%?); destruct (Halloc)1506 whd in match (beloadv ??) in ⊢ (??%%);1507 lapply (valid_block_to_bool … Hvalid) #Hlt1508 >Hlt >(zlt_succ … Hlt)1509 normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);1510 cut (eqZb (block_id block) next = false)1511 [ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq1512 >Hneq cases (eq_region ??) normalize nodelta @refl1513 qed.1514 1515 (* Lift [alloc_beloadv_conservation] to loadn *)1516 lemma alloc_loadn_conservation :1517 ∀m,m',z1,z2,r,new_block.1518 alloc m z1 z2 r = 〈m', new_block〉 →1519 ∀n. ∀block,offset.1520 valid_block m block →1521 loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.1522 #m #m' #z1 #z2 #r #new_block #Halloc #n1523 elim n try //1524 #n' #Hind #block #offset #Hvalid_block1525 whd in ⊢ (??%%);1526 >(alloc_beloadv_conservation … Hvalid_block Halloc)1527 cases (beloadv m' (mk_pointer block offset)) //1528 #bev normalize nodelta1529 whd in match (shift_pointer ???); >Hind try //1530 qed.1531 1532 (* Memory allocation preserves [memory_inj] *)1533 lemma alloc_memory_inj :1534 ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.1535 alloc m2 z1 z2 r = 〈m2', new_block〉 →1536 memory_inj E m1 m2'.1537 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc1538 %1539 [ 1:1540 whd1541 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload1542 elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)1543 #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //1544 lapply (refl ? (access_mode ty))1545 cases ty in Hload_eq;1546 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain1547 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]1548 #Hload normalize in ⊢ ((???%) → ?); #Haccess1549 [ 1,7,8: normalize in Hload; destruct (Hload)1550 | 2,3,4,9: whd in match (load_value_of_type ????);1551 whd in match (load_value_of_type ????);1552 lapply (load_by_value_success_valid_block … Haccess Hload)1553 #Hvalid_block1554 whd in match (load_value_of_type ????) in Hload;1555 <(alloc_loadn_conservation … Halloc … Hvalid_block)1556 @Hload1557 | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]1558 | 2: @(mi_freeblock … Hmemory_inj)1559 | 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)1560 elim m2 in Halloc; #contentmap #nextblock #Hnextblock1561 elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)1562 whd in match (valid_pointer ??) in ⊢ (% → %);1563 @Zltb_elim_Type01564 [ 2: normalize #_ #Habsurd destruct (Habsurd) ]1565 #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]1566 #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);1567 whd in match (high_bound ??) in ⊢ (% → %);1568 whd in match (update_block ?????);1569 whd in match (eq_block ??);1570 cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]1571 #Hbid_neq >Hbid_neq1572 cases (eq_region br' r) normalize #H @H1573 | 4: @(mi_region … Hmemory_inj)1574 | 5: @(mi_disjoint … Hmemory_inj)1575 ] qed.1576 1577 (* Memory allocation induces a memory extension. *)1578 lemma alloc_memory_ext :1579 ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.1580 alloc m2 z1 z2 r = 〈m2', new_block〉 →1581 memory_ext E m1 m2'.1582 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc1583 lapply (alloc_memory_inj … Hmemory_inj Halloc)1584 #Hinj' %1585 [ 1: @Hinj'1586 | 2: @[new_block]1587 | 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]1588 #Heq destruct (Heq) whd elim m2 in Halloc;1589 #Hcontents #nextblock #Hnextblock1590 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)1591 /2/1592 | 4: * #b #o * #b' #o' #Hvalid_ptr #Hembed %1593 normalize in ⊢ (% → ?); * [ 2: #H @H ]1594 #Heq destruct (Heq)1595 lapply (mi_valid_pointers … Hmemory_inj … Hvalid_ptr Hembed)1596 whd in ⊢ (% → ?);1597 (* contradiction because ¬ (valid_block m2 new_block) *)1598 elim m2 in Halloc;1599 #contents_m2 #nextblock_m2 #Hnextblock_m21600 whd in ⊢ ((??%?) → ?);1601 #Heq_alloc destruct (Heq_alloc)1602 normalize1603 lapply (irreflexive_Zlt nextblock_m2)1604 @Zltb_elim_Type01605 [ #H * #Habsurd @(False_ind … (Habsurd H)) ] #_ #_ normalize #Habsurd destruct (Habsurd)1606 ] qed.1607 1608 lemma bestorev_beloadv_conservation :1609 ∀mA,mB,wb,wo,v.1610 bestorev mA (mk_pointer wb wo) v = Some ? mB →1611 ∀rb,ro. eq_block wb rb = false →1612 beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).1613 #mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq1614 whd in ⊢ (??%%);1615 elim mB in Hstore; #contentsB #nextblockB #HnextblockB1616 normalize in ⊢ (% → ?);1617 cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta1618 [ 2: #Habsurd destruct (Habsurd) ]1619 cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo))1620 then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb))1621 else false) normalize nodelta1622 [ 2: #Habsurd destruct (Habsurd) ]1623 #Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid1624 cases rr cases wr normalize try //1625 @(eqZb_elim … rid wid)1626 [ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]1627 try //1628 qed.1629 1630 (* lift [bestorev_beloadv_conservation to [loadn] *)1631 lemma bestorev_loadn_conservation :1632 ∀mA,mB,n,wb,wo,v.1633 bestorev mA (mk_pointer wb wo) v = Some ? mB →1634 ∀rb,ro. eq_block wb rb = false →1635 loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.1636 #mA #mB #n1637 elim n1638 [ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl1639 | 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq1640 whd in ⊢ (??%%);1641 >(bestorev_beloadv_conservation … Hstore … Hneq)1642 >(Hind … Hstore … Hneq) @refl1643 ] qed.1644 1645 (* lift [bestorev_loadn_conservation] to [load_value_of_type] *)1646 lemma bestorev_load_value_of_type_conservation :1647 ∀mA,mB,wb,wo,v.1648 bestorev mA (mk_pointer wb wo) v = Some ? mB →1649 ∀rb,ro. eq_block wb rb = false →1650 ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.1651 #mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty1652 cases ty1653 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain1654 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try //1655 [ 1: elim sz | 2: elim fsz | 3: | 4: ]1656 whd in ⊢ (??%%);1657 >(bestorev_loadn_conservation … Hstore … Hneq) @refl1658 qed.1659 1660 (* Writing in the "extended" part of a memory preserves the underlying injection *)1661 lemma bestorev_memory_ext_to_load_sim :1662 ∀E,mA,mB,mC.1663 ∀Hext:memory_ext E mA mB.1664 ∀wb,wo,v. meml ? wb (me_writeable … Hext) →1665 bestorev mB (mk_pointer wb wo) v = Some ? mC →1666 load_sim_ptr E mA mC.1667 #E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd1668 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload1669 (* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *)1670 lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb21671 lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b21672 cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false1673 <(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)1674 @(mi_inj … (me_inj … Hext) … Hvalid … Hembed … Hload)1675 qed.1676 1677 (* Writing in the "extended" part of a memory preserves the whole memory injection *)1678 lemma bestorev_memory_ext_to_memory_inj :1679 ∀E,mA,mB,mC.1680 ∀Hext:memory_ext E mA mB.1681 ∀wb,wo,v. meml ? wb (me_writeable … Hext) →1682 bestorev mB (mk_pointer wb wo) v = Some ? mC →1683 memory_inj E mA mC.1684 #E #mA * #contentsB #nextblockB #HnextblockB #mC1685 #Hext #wb #wo #v #Hwb #Hstore1686 %1687 [ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]1688 elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok1689 #Hmem1690 [ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] -Hvalid -Hregion -Hdisjoint1691 whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)1692 normalize in ⊢ (% → ?); #Hlt_wb1693 #p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) -Hcodomain1694 normalize in match (valid_pointer ??) in ⊢ (% → %);1695 >(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta1696 cases (Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector offset_size (offv wo))1697 ∧Zltb (Z_of_unsigned_bitvector offset_size (offv wo)) (high (contentsB wb)))1698 normalize nodelta1699 [ 2: #Habsurd destruct (Habsurd) ]1700 #Heq destruct (Heq)1701 cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta1702 [ 2: // ]1703 whd in match (update_block ?????);1704 cut (eq_block (pblock p') wb = false)1705 [ 2: #Heq >Heq normalize nodelta #H @H ]1706 @neq_block_eq_block_false @sym_neq1707 @(mem_not_mem_neq writeable … Hmem)1708 @(Hwriteable_ok … HvalidA Hembed)1709 qed.1710 1711 (* It even preserves memory extensions, with the same writeable blocks. *)1712 lemma bestorev_memory_ext_to_memory_ext :1713 ∀E,mA,mB.1714 ∀Hext:memory_ext E mA mB.1715 ∀wb,wo,v. meml ? wb (me_writeable … Hext) →1716 ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →1717 ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).1718 #E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore1719 %{(mk_memory_ext …1720 (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)1721 (me_writeable … Hext)1722 ?1723 (me_writeable_ok … Hext)1724 )} try @refl1725 #b #Hmemb1726 lapply (me_writeable_valid … Hext b Hmemb)1727 lapply (me_writeable_valid … Hext wb Hmem)1728 elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid1729 lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);1730 >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta1731 cases (if Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector 16 (offv wo))1732 then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (contentsB wb))1733 else false)1734 normalize [ 2: #Habsurd destruct (Habsurd) ]1735 #Heq destruct (Heq) @Hb_valid1736 qed.1737 1738 (* Lift [bestorev_memory_ext_to_memory_ext] to storen *)1739 lemma storen_memory_ext_to_memory_ext :1740 ∀E,mA,l,mB,mC.1741 ∀Hext:memory_ext E mA mB.1742 ∀wb,wo. meml ? wb (me_writeable … Hext) →1743 storen mB (mk_pointer wb wo) l = Some ? mC →1744 memory_ext E mA mC.1745 #E #mA #l elim l1746 [ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)1747 @Hext1748 | 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem1749 whd in ⊢ ((??%?) → ?);1750 lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)1751 cases (bestorev mB (mk_pointer wb wo) hd)1752 normalize nodelta1753 [ 1: #H #Habsurd destruct (Habsurd) ]1754 #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore1755 @(Hind … HextD … Hstore)1756 <Heq @Hmem1757 ] qed.1758 1759 (* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)1760 lemma store_value_of_type_memory_ext_to_memory_ext :1761 ∀E,mA,mB,mC.1762 ∀Hext:memory_ext E mA mB.1763 ∀wb,wo. meml ? wb (me_writeable … Hext) →1764 ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →1765 memory_ext E mA mC.1766 #E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v1767 cases ty1768 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain1769 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]1770 whd in ⊢ ((??%?) → ?);1771 [ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]1772 #Hstore1773 @(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)1774 qed.1775 1776 (* End of the memory injection-related stuff. *)1777 (* ------------------------------------------ *)1778 890 1779 891 (* Lookup functions in list environments (used to type local variables in functions) *) … … 1800 912 ]. 1801 913 914 (* --------------------------------------------------------------------------- *) 915 (* Memory extensions (limited form on memoryInjection.ma). Note that we state the 916 properties at the back-end level. *) 917 (* --------------------------------------------------------------------------- *) 918 919 (* 920 definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_blockb ?. 921 * #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2) 922 [ 1: #Heq >Heq cases r1 cases r2 normalize 923 >eqZb_reflexive normalize @conj #H destruct (H) 924 try @refl 925 | 2: #Hneq cases r1 cases r2 normalize 926 >(eqZb_false … Hneq) normalize @conj 927 #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??))) 928 ] qed. *) 929 930 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the back-end values are equal. *) 931 definition load_sim ≝ 932 λ(m1 : mem).λ(m2 : mem). 933 ∀ptr,bev. 934 beloadv m1 ptr = Some ? bev → 935 beloadv m2 ptr = Some ? bev. 936 937 (* The [valid_pointer] property is too weak to be preserved by [free]. We use the following guard. *) 938 (* definition freed_pointer ≝ λ(m : mem).λ(p : pointer). 939 low_bound m (pblock p) = OZ ∧ 940 high_bound m (pblock p) = OZ. *) 941 942 (* definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. *) 943 944 definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. 945 946 definition outbound_pointer ≝ λm,p. 947 Zltb (block_id (pblock p)) (nextblock m) = true ∧ 948 Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧ 949 high_bound m (pblock p) = Z_of_unsigned_bitvector … (offv (poff p)). 950 951 lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p. 952 #m #p @conj 953 [ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??); 954 whd in match (outbound_pointer ??); 955 whd in match (do_if_in_bounds); normalize nodelta 956 cases (Zltb (block_id (pblock p)) (nextblock m)) 957 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] 958 >andb_lsimpl_true normalize nodelta 959 cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 960 [ 2: normalize nodelta #Habsurd destruct (Habsurd) ] 961 >andb_lsimpl_true normalize nodelta 962 lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p))) 963 elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p))) 964 [ 1: #H >H #_ normalize nodelta #_ %1 #A #f /2 by ex_intro/ 965 | 2: * #_ #H1 #_ #H2 >(Zleb_true_to_Zleb_true_to_eq … H1 H2) %2 @conj try @conj @refl ] 966 | 2: whd in match (valid_pointer ??); * 967 [ 1: whd in match (in_bounds_pointer ??); #H 968 lapply (H bool (λblock,contents,off. true)) 969 * #foo whd in match (do_if_in_bounds ????); 970 cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta 971 [ 2: #Habsurd destruct (Habsurd) ] 972 >andb_lsimpl_true 973 cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 974 normalize nodelta 975 [ 2: #Habsurd destruct (Habsurd) ] 976 >andb_lsimpl_true 977 elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p)))) 978 [ 1: #H >(Zltb_to_Zleb_true … H) #_ @refl 979 | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ] 980 | 2: whd in match (outbound_pointer ??); * * #Hlt #Hleb >Hlt >Hleb 981 #Hhigh >Hhigh >andb_lsimpl_true 982 lapply (reflexive_Zle … (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 983 #Hle >(Zle_to_Zleb_true … Hle) @refl 984 ] 985 ] qed. 986 987 (* 988 lemma freed_pointer_dec : ∀m,p. freed_pointer m p ∨ (¬freed_pointer m p). 989 #m #p 990 whd in match (freed_pointer ??); 991 cases (low_bound m (pblock p)) 992 [ 2,3: #low %2 % * #H destruct (H) ] 993 cases (high_bound m (pblock p)) 994 [ 1: %1 @conj @refl | 2,3: #low %2 % * #_ #H destruct (H) ] 995 qed. *) 996 997 (* In the limited setting of switch removal, a memory extension is a list of fresh blocks 998 * to which we can write. *) 999 record sr_memext (m1 : mem) (m2 : mem) : Type[0] ≝ 1000 { me_inj : load_sim m1 m2; 1001 (* A list of blocks where we can write freely *) 1002 me_writeable : list block; 1003 (* These blocks are valid *) 1004 me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b; 1005 (* And pointers to m1 are oblivious to these blocks *) 1006 me_writeable_ok : ∀p.valid_pointer m1 p = true → 1007 ¬ (meml ? (pblock p) me_writeable); 1008 (* Valid pointers are still valid in m2. One could think that this is superfluous as 1009 being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer 1010 to be one off the end of a block bound. The internal check in beloadv does not. 1011 valid_pointer should be understood as "pointer making sense" rather than "pointer from 1012 which you can load stuff". [mi_valid_pointers] is used for instance when proving the 1013 semantics preservation for equality testing (where we check that the pointers we 1014 compare are valid before being equal). 1015 *) 1016 me_valid_pointers : ∀p. (* ¬ (freed_pointer m1 p) → *) 1017 valid_pointer m1 p = true → 1018 valid_pointer m2 p = true 1019 }. 1020 1802 1021 (* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension 1803 1022 of the environment [e1] s.t. the new binders are in [new], and such that those … … 1805 1024 definition disjoint_extension ≝ 1806 1025 λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem). 1807 λ(new : list (ident × type)). λ( E:embedding). λ(Hext: memory_ext Em1 m2).1026 λ(new : list (ident × type)). λ(Hext: sr_memext m1 m2). 1808 1027 ∀id. match mem_assoc_env id new with 1809 1028 [ true ⇒ … … 1811 1030 ∧ meml ? b (me_writeable … Hext) 1812 1031 ∧ lookup ?? e1 id = None ? 1813 | false ⇒ 1814 match lookup ?? e1 id with 1815 [ None ⇒ lookup ?? e2 id = None ? 1816 | Some b1 ⇒ 1817 match lookup ?? e2 id with 1818 [ None ⇒ False 1819 | Some b2 ⇒ 1820 valid_block m1 b1 ∧ 1821 value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset)) 1822 ] 1823 ] 1032 | false ⇒ lookup ?? e1 id = lookup ?? e2 id 1824 1033 ]. 1034 1035 (* Lift load_sim to loadn. *) 1036 lemma load_sim_loadn : 1037 ∀m1,m2. load_sim m1 m2 → 1038 ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res. 1039 #m1 #m2 #Hload_sim #sz 1040 elim sz 1041 [ 1: #p #res #H @H 1042 | 2: #n' #Hind #p #res 1043 whd in match (loadn ???); 1044 whd in match (loadn m2 ??); 1045 lapply (Hload_sim p) 1046 cases (beloadv m1 p) normalize nodelta 1047 [ 1: #_ #Habsurd destruct (Habsurd) ] 1048 #bval #H >(H ? (refl ??)) normalize nodelta 1049 lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1))) 1050 cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n') 1051 normalize nodelta 1052 [ 1: #_ #Habsurd destruct (Habsurd) ] 1053 #res' #H >(H ? (refl ??)) normalize 1054 #H @H 1055 ] qed. 1056 1057 (* Lift load_sim to front-end values. *) 1058 lemma load_sim_fe : 1059 ∀m1,m2. load_sim m1 m2 → 1060 ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v → 1061 load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v. 1062 #m1 #m2 #Hloadsim #ptr #ty #v 1063 cases ty 1064 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty 1065 | 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ] 1066 whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?)); 1067 [ 1,7,8: #Habsurd destruct (Habsurd) 1068 | 5,6: #H @H 1069 | 2,3,4,9: 1070 generalize in match (mk_pointer (pblock ptr) (poff ptr)); 1071 elim (typesize ?) 1072 [ 1,3,5,7: #p #H @H 1073 | 2,4,6,8: #n' #Hind #p 1074 lapply (load_sim_loadn … Hloadsim (S n') p) 1075 cases (loadn m1 p (S n')) normalize nodelta 1076 [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ] 1077 #bv #H >(H ? (refl ??)) #H @H 1078 ] 1079 ] qed. 1080 1081 (* Lemmas relating memory extensions to [free] *) 1082 1083 (* Successful beloadv implies valid_pointer. The converse is *NOT* true. *) 1084 lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true. 1085 * #contents #next #nextpos #ptr #res 1086 whd in match (beloadv ??); 1087 whd in match (valid_pointer ??); 1088 cases (Zltb (block_id (pblock ptr)) next) 1089 normalize nodelta 1090 [ 2: #Habsurd destruct (Habsurd) ] 1091 >andb_lsimpl_true 1092 whd in match (low_bound ??); 1093 whd in match (high_bound ??); 1094 cases (Zleb (low (contents (pblock ptr))) 1095 (Z_of_unsigned_bitvector offset_size (offv (poff ptr)))) 1096 [ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ] 1097 >andb_lsimpl_true 1098 normalize nodelta #H 1099 @Zltb_to_Zleb_true 1100 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H; 1101 try // normalize #Habsurd destruct (Habsurd) qed. 1102 1103 lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1). 1104 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize 1105 @(eqZb_elim … bid1 bid2) 1106 [ 1: #Heq >Heq cases br1 cases br2 normalize 1107 [ 1,4: * #H @(False_ind … (H (refl ??))) ] 1108 #_ @refl 1109 | 2: cases br1 cases br2 normalize #_ #_ @refl ] 1110 qed. 1111 1112 lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1). 1113 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize 1114 @(eqZb_elim … bid1 bid2) 1115 [ 1: #Heq >Heq cases br1 cases br2 normalize 1116 [ 1,4: * #H @(False_ind … (H (refl ??))) ] 1117 #_ @refl 1118 | 2: cases br1 cases br2 normalize #_ #_ @refl ] 1119 qed. 1120 1121 lemma beloadv_free_blocks_neq : 1122 ∀m,block,pblock,poff,res. 1123 beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block. 1124 * #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res 1125 normalize 1126 cases (Zltb pbid next) normalize nodelta 1127 [ 2: #Habsurd destruct (Habsurd) ] 1128 cases pbr cases br normalize nodelta 1129 [ 2,3: #_ % #Habsurd destruct (Habsurd) ] 1130 @(eqZb_elim pbid bid) normalize nodelta 1131 #Heq destruct (Heq) 1132 [ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ] 1133 #_ % #H destruct (H) elim Heq #H @H @refl 1134 qed. 1135 1136 (* 1137 lemma be_to_fe_value_inj : ∀bv1,bv2. 1138 be_to_fe_value (ASTint I8 Unsigned) [bv1] 1139 = be_to_fe_value (ASTint I8 Unsigned) [bv2] → bv1 = bv2. 1140 #bv1 #bv2 1141 whd in match (be_to_fe_value ??); 1142 whd in match (be_to_fe_value ??); 1143 cases bv1 normalize nodelta 1144 [ 1: cases bv2 normalize nodelta 1145 [ 1: #H @refl | 2: 1146 try // 1147 [ cases bv2 *) 1148 1149 lemma beloadv_free_beloadv : 1150 ∀m,block,ptr,res. 1151 beloadv (free m block) ptr = Some ? res → 1152 beloadv m ptr = Some ? res. 1153 * #contents #next #nextpos #block * #pblock #poff #res 1154 #H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq 1155 lapply H 1156 whd in match (beloadv ??); 1157 whd in match (beloadv ??) in ⊢ (? → %); 1158 whd in match (nextblock (free ??)); 1159 cases (Zltb (block_id pblock) next) 1160 [ 2: normalize #Habsurd destruct (Habsurd) ] 1161 normalize nodelta 1162 <(low_free_eq … Hblocks_neq) 1163 <(high_free_eq … Hblocks_neq) 1164 whd in match (free ??); 1165 whd in match (update_block ?????); 1166 @(eq_block_elim … pblock block) 1167 [ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ] 1168 #_ normalize nodelta 1169 #H @H 1170 qed. 1171 1172 lemma beloadv_free_beloadv2 : 1173 ∀m,block,ptr,res. 1174 pblock ptr ≠ block → 1175 beloadv m ptr = Some ? res → 1176 beloadv (free m block) ptr = Some ? res. 1177 * #contents #next #nextpos #block * #pblock #poff #res #Hneq 1178 whd in match (beloadv ??); 1179 whd in match (beloadv ??) in ⊢ (? → %); 1180 whd in match (nextblock (free ??)); 1181 cases (Zltb (block_id pblock) next) 1182 [ 2: normalize #Habsurd destruct (Habsurd) ] 1183 normalize nodelta 1184 <(low_free_eq … Hneq) 1185 <(high_free_eq … Hneq) 1186 whd in match (free ??); 1187 whd in match (update_block ?????); 1188 @(eq_block_elim … pblock block) 1189 [ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ] 1190 #_ normalize nodelta 1191 #H @H 1192 qed. 1193 1194 lemma beloadv_free_simulation : 1195 ∀m1,m2,block,ptr,res. 1196 ∀mem_hyp : sr_memext m1 m2. 1197 beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res. 1198 * #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 1199 * #br #bid * * #pr #pid #poff #res * 1200 #Hload_sim #Hme_writeable #Hme_writeable_valid #Hptr_not_mem #Hvalid_conserv 1201 #Hload 1202 lapply (beloadv_free_beloadv … Hload) #Hload_before_free 1203 lapply (beloadv_free_blocks_neq … Hload) #Hblocks_neq 1204 @beloadv_free_beloadv2 1205 [ 1: @Hblocks_neq ] 1206 @Hload_sim assumption 1207 qed. 1208 1209 lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p. 1210 #m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %); 1211 #H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %); 1212 elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b))) 1213 [ 1: #Hlt >Hlt normalize nodelta 1214 @(eq_block_elim … b (pblock p)) 1215 [ 1: #Heq >Heq whd in match (free ??); 1216 whd in match (update_block ?????); >eq_block_b_b 1217 normalize nodelta normalize in match (low ?); 1218 >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta 1219 #Habsurd destruct (Habsurd) 1220 | 2: #Hblock_neq whd in match (free ? ?); 1221 whd in match (update_block ?????); 1222 >(not_eq_block_rev … Hblock_neq) normalize nodelta 1223 cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 1224 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] 1225 >andb_lsimpl_true 1226 lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) 1227 (high (blocks m (pblock p)))) 1228 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p)))) 1229 [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 1230 normalize nodelta #H #_ /2 by ex_intro/ 1231 ] 1232 | 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ] 1233 qed. 1234 1235 lemma outbound_free_to_outbound : ∀m,b,p. outbound_pointer (free m b) p → outbound_pointer m p. 1236 #m #b #p whd in match (free ??); 1237 whd in match (outbound_pointer ??) in ⊢ (% → %); 1238 whd in match (update_block ????); 1239 whd in match (low_bound ??); whd in match (high_bound ??); 1240 @(eq_block_elim … (pblock p) b) normalize nodelta 1241 [ 1: #Heq >Heq cases (Zltb ? (nextblock m)) 1242 [ 2: * * #Habsurd destruct (Habsurd) ] 1243 * * #_ whd in match (low ?); whd in match (high ?); 1244 #H1 #H2 <H2 in H1; normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 1245 | 2: #Hneq #H @H ] 1246 qed. 1247 1248 lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true. 1249 #m #b #p #Hvalid 1250 lapply (valid_pointer_def … m p) * #_ #Hdef @Hdef 1251 elim (valid_pointer_def … (free m b) p) #H #_ 1252 elim (H Hvalid) 1253 [ 1: #Hin %1 @in_bounds_free_to_in_bounds assumption 1254 | 2: #Hout %2 @outbound_free_to_outbound assumption ] 1255 qed. 1256 1257 lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p. 1258 #m #b #p 1259 whd in match (valid_pointer ??); 1260 whd in match (free ??); 1261 whd in match (update_block ????); 1262 whd in match (low_bound ??); 1263 whd in match (high_bound ??); 1264 @(eq_block_elim … b (pblock p)) 1265 [ 1: #Heq >Heq >eq_block_b_b normalize nodelta 1266 whd in match (low ?); whd in match (high ?); 1267 cases (Zltb ? (nextblock m)) 1268 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] 1269 >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd) 1270 | 2: #Hneq #_ @Hneq ] 1271 qed. 1272 1273 lemma valid_pointer_free : ∀m1,m2. sr_memext m1 m2 → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true. 1274 #m1 #m2 #Hext #p #b #Hvalid 1275 lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free 1276 lapply (me_valid_pointers … Hext … Hvalid_before_free) 1277 lapply (valid_after_free … Hvalid) #Hneq 1278 whd in match (free ??); 1279 whd in match (update_block ????); 1280 whd in match (valid_pointer ??) in ⊢ (% → %); 1281 whd in match (low_bound ??) in ⊢ (% → %); 1282 whd in match (high_bound ??) in ⊢ (% → %); 1283 >(not_eq_block_rev … Hneq) normalize nodelta #H @H 1284 qed. 1285 1286 (* Performing a [free] preserves memory extensions. *) 1287 lemma free_memory_ext : 1288 ∀m1,m2,bl. 1289 sr_memext m1 m2 → 1290 sr_memext (free m1 bl) (free m2 bl). 1291 #m1 #m2 #bl #Hext 1292 % 1293 [ 1: @(λptr,bev. beloadv_free_simulation m1 m2 bl ptr bev Hext) 1294 | 2: @(filter ? (λwb. notb (eq_block wb bl)) (me_writeable … Hext)) 1295 | 3: #b #Hmem 1296 cut (mem block b (me_writeable m1 m2 Hext)) 1297 [ elim (me_writeable m1 m2 Hext) in Hmem; 1298 [ 1: #H @H 1299 | 2: #h #tl #Hind whd in match (filter ???); 1300 @(eq_block_elim … h bl) normalize in match (notb ?); normalize nodelta 1301 [ 1: #Heq #H whd in match (meml ???); destruct %2 @Hind @H 1302 | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * 1303 [ 1: #H %1 @H 1304 | 2: #H %2 @Hind @H ] ] ] ] 1305 #Hmem2 lapply (me_writeable_valid … Hmem2) 1306 elim m2 #contents #nextblock #pos elim b #br #bid 1307 normalize #H @H 1308 | 4: #p #Hvalid elim (valid_pointer_free_ok_alt … Hvalid) 1309 [ 1: #Heq >Heq elim (me_writeable m1 m2 Hext) 1310 [ 1: normalize % // 1311 | 2: #hd #tl #Hind 1312 whd in match (filter ???); 1313 @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta 1314 [ 1: #Heq @Hind 1315 | 2: #Hneq whd in match (meml ???); % * 1316 [ 1: #Heq elim Hneq #H @H @(sym_eq … Heq) 1317 | 2: #H elim Hind #Hind @Hind @H ] ] ] 1318 | 2: * #_ #Hvalid lapply (me_writeable_ok … Hext … Hvalid) 1319 * #Hyp % #Htarget @Hyp 1320 elim (me_writeable m1 m2 Hext) in Htarget; 1321 [ 1: normalize // 1322 | 2: #hd #tl #Hind 1323 whd in match (filter ???); 1324 @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta 1325 [ 1: #Heq whd in match (meml ???) in ⊢ (? → %); 1326 #H %2 @Hind @H 1327 | 2: #Hneq whd in match (meml ???); 1328 whd in match (meml ???) in ⊢ (? → %); * 1329 [ 1: #H %1 @H 1330 | 2: #H %2@Hind @H ] ] ] ] 1331 | 5: #p @valid_pointer_free @Hext 1332 ] qed. 1333 1334 1335 lemma free_list_memory_ext : 1336 ∀l,m1,m2. 1337 sr_memext m1 m2 → 1338 sr_memext (free_list m1 l) (free_list m2 l). 1339 #l elim l 1340 [ 1: #m1 #m2 #H @H 1341 | 2: #hd #tl #Hind #m1 #m2 #H >free_list_cons >free_list_cons 1342 @free_memory_ext @Hind @H 1343 ] qed. 1344 1345 (* Extend the previous lemma to [free_list] *) 1346 lemma beloadv_free_list_memory_ext : 1347 ∀m1,m2,blocks,ptr,res. 1348 ∀mem_hyp : sr_memext m1 m2. 1349 beloadv (free_list m1 blocks) ptr = Some ? res → beloadv (free_list m2 blocks) ptr = Some ? res. 1350 #m1 #m2 #blocks #mtr #res #Hext #Hload 1351 lapply (free_list_memory_ext blocks … Hext) #Hext_list 1352 lapply (me_inj … Hext_list) #H @H @Hload 1353 qed. 1354 1355 1356 (* Prove that memory extensions are preserved by free.*) 1357 (* 1358 lemma memext_free_conservation : 1359 ∀m1,m2 : mem. 1360 ∀mem_hyp : sr_memext m1 m2. 1361 ∀env,env_ext. 1362 ∀new_vars. 1363 ∀env_hyp : disjoint_extension env m1 env_ext m2 new_vars mem_hyp. 1364 (sr_memext (free_list m1 (blocks_of_env env)) 1365 (free_list m2 (blocks_of_env env_ext))). 1366 #m1 #m2 * #Hloadsim #Hwriteable #Hwritevalid #Holdnotwriteable #Hvalidok #env #env_ext #new_vars 1367 whd in ⊢ (% → ?); #Hdisjoint *) 1368 1825 1369 1826 1370 (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if … … 1846 1390 qed. *) 1847 1391 1848 1849 1392 (* "generic" simulation relation on [res ?] *) 1850 1393 definition res_sim ≝ 1851 1394 λ(A : Type[0]). 1852 λ(eq : A → A → Prop).1853 1395 λ(r1, r2 : res A). 1854 ∀a 1. r1 = OK ? a1 → ∃a2. r2 = OK ? a2 ∧ eq a1 a2.1396 ∀a. r1 = OK ? a → r2 = OK ? a. 1855 1397 1856 1398 (* Specialisation of [res_sim] to match [exec_expr] *) 1857 definition exec_expr_sim ≝ λE. 1858 res_sim (val × trace) (λr1,r2. value_eq E (\fst r1) (\fst r2) ∧ (\snd r1 = \snd r2)). 1399 definition exec_expr_sim ≝ res_sim (val × trace). 1859 1400 1860 1401 (* Specialisation of [res_sim] to match [exec_lvalue] *) 1861 definition exec_lvalue_sim ≝ λE. 1862 res_sim (block × offset × trace) 1863 (λr1,r2. 1864 let 〈b1,o1,tr1〉 ≝ r1 in 1865 let 〈b2,o2,tr2〉 ≝ r2 in 1866 value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) ∧ tr1 = tr2). 1402 definition exec_lvalue_sim ≝ res_sim (block × offset × trace). 1867 1403 1868 1404 lemma load_value_of_type_dec : ∀ty, m, b, o. load_value_of_type ty m b o = None ? ∨ ∃r. load_value_of_type ty m b o = Some ? r. 1869 1405 #ty #m #b #o cases (load_value_of_type ty m b o) 1870 1406 [ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed. 1871 1872 (*1873 lemma switch_removal_alloc_extension : ∀f, f', vars, env, env', m, m'.1874 env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →1875 〈f',vars〉 = function_switch_removal f →1876 env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →1877 environment_extension env env' vars.1878 1879 #f #f'1880 cut (∀l:list (ident × type). [ ] @ l = l) [ // ] #nil_append1881 cases (fn_params f) cases (fn_vars f)1882 [ 1: #vars >append_nil >append_nil >nil_append elim vars1883 [ 1: #env #env' #m #m' normalize in ⊢ (% → ? → % → ?); #Henv1 #_ #Henv2 destruct //1884 | 2: #hd #tl #Hind #env #env' #m #m' #Henv1 #Heq1885 whd in ⊢ ((???(???%)) → ?);1886 #Henv #Hswrem #Henv'1887 #id1888 *)1889 1890 (*1891 lemma substatement_fresh : ∀s,u.1892 fresh_for_statement s u →1893 substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).1894 #s #u @(statement_ind2 ? (λls.fresh_for_labeled_statements ls u → substatement_ls ls (λs':statement.fresh_for_statement s' u)) … s)1895 try /by I/1896 [ 1: #e1 #e2 #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj assumption1897 | 2: *1898 [ 1: #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *1899 #Hfresh_e #Hfresh_args @conj try assumption1900 normalize nodelta in Hfresh_args;1901 >max_id_commutative in Hfresh_args; >max_id_one_neutral1902 #Hfresh_args1903 | 2: #ret #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *1904 #Hfresh_e #H lapply (fresh_max_split ??? H) *1905 #Hfresh_ret #Hfresh_args @conj try @conj try assumption ]1906 elim args in Hfresh_args;1907 [ 1,3: //1908 | 2,4: #hd #tl #Hind whd in match (foldl ?????); whd in match (All ???);1909 >foldl_max #H elim (fresh_max_split ??? H) #Hu #HAll @conj1910 [ 1,3: @Hu1911 | 2,4: @Hind assumption ] ]1912 | 3: #s1 #s2 #_ #_1913 whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *1914 whd in match (substatement_P ??); /2/1915 | 4: #e #cond #iftrue #iffalse #_1916 whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *1917 #Hexpr #H2 lapply (fresh_max_split … H2) * /2/1918 | 5,6: #e #stm #_1919 whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * /2/1920 | 7: #init #cond #step #body #_ #_ #_ #H lapply (fresh_max_split … H) *1921 #H1 #H2 elim (fresh_max_split … H1) #Hinit #Hcond1922 elim (fresh_max_split … H2) #Hstep #Hbody whd @conj try @conj try @conj /3/1923 | 8: #ret #H whd elim ret in H; try //1924 | 9: #expr #ls #Hind #H whd @conj1925 [ 1: elim (fresh_max_split … H) //1926 | 2: @Hind elim (fresh_max_split … H) // ]1927 | 10: #l #body #Hind #H whd elim (fresh_max_split … H) //1928 | 11: #sz #i #hd #tl #Hhd #Htl #H whd1929 elim (fresh_max_split … H) #Htl_fresh #Hhd_fresh @conj //1930 @Htl //1931 ] qed.1932 *)1933 1934 (* Eliminating switches introduces fresh variables. [environment_extension] characterizes1935 * a local environment extended by some local variables. *)1936 1937 1938 (* lookup on environment extension *)1939 (*1940 lemma extension_lookup :1941 ∀map, map', ext, id, result.1942 environment_extension map map' ext →1943 lookup ?? map id = Some ? result →1944 lookup ?? map' id = Some ? result.1945 #map #map' #ext #id #result #Hext lapply (Hext id)1946 cases (mem_assoc_env ??) normalize nodelta1947 [ 1: * * #ext_result #H1 >H1 #Habsurd destruct (Habsurd)1948 | 2: #H >H // ] qed.1949 1950 *)1951 1952 (* Extending a map by an empty list of variables yields an observationally equivalent1953 * environment. *)1954 (*1955 lemma environment_extension_nil : ∀en,en':env. (environment_extension en en' [ ]) → imap_eq ?? en en'.1956 * #map1 * #map2 whd in ⊢ (% → ?); #Hext whd % #id #v #H1957 [ 1: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta1958 cases (lookup_opt block id map2) normalize1959 [ 1: >H #H2 >H2 @refl1960 | 2: #b >H cases v1961 [ 1: normalize * #H @(False_ind … H)1962 | 2: #block normalize // ] ]1963 | 2: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta1964 >H cases v normalize try //1965 #block cases (lookup_opt ? id map1) normalize try //1966 * #H @(False_ind … H)1967 ] qed. *)1968 1969 (* If two identifier maps are observationally equal, then they contain the same bocks.1970 * see maps_obsequiv.ma for the details of the proof. *)1971 (*1972 lemma blocks_of_env_eq : ∀e,e'. imap_eq ?? e e' → blocks_of_env e = blocks_of_env e'.1973 * #map1 * #map2 normalize #Hpmap_eq lapply (pmap_eq_fold … Hpmap_eq) #Hfold1974 >Hfold @refl1975 qed.1976 *)1977 1407 1978 1408 (* Simulation relations. *) … … 2023 1453 (Kcall r (\fst (function_switch_removal f)) en' k'). 2024 1454 2025 2026 1455 (* 2027 1456 en' = exec_alloc_variables en m (\snd (function_switch_removal f)) … … 2054 1483 *) 2055 1484 2056 inductive switch_state_sim : state → state → Prop ≝ 2057 | sws_state : ∀u,f,s,k,k',m,m',result. 2058 ∀env, env', f', vars. 2059 ∀E:embedding. 2060 ∀Hext:memory_ext E m m'. 2061 fresh_for_statement s u → 2062 (* 2063 env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) → 2064 env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) → 2065 *) 2066 〈f',vars〉 = function_switch_removal f → 2067 disjoint_extension env m env' m' vars E Hext → 2068 switch_removal s (map ?? (fst ??) vars) u = Some ? result → 2069 switch_cont_sim (map ?? (fst ??) vars) k k' → 1485 (* env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) → 1486 env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) → *) 1487 record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { 1488 rg_find_symbol: ∀s. 1489 find_symbol ? ge s = find_symbol ? ge' s; 1490 rg_find_funct: ∀v,f. 1491 find_funct ? ge v = Some ? f → 1492 find_funct ? ge' v = Some ? (t f); 1493 rg_find_funct_ptr: ∀b,f. 1494 find_funct_ptr ? ge b = Some ? f → 1495 find_funct_ptr ? ge' b = Some ? (t f) 1496 }. 1497 1498 (* This record aims to shorten the definition of the simulation relation on states more readeable. *) 1499 inductive switch_state_sim (ge : genv) : state → state → Prop ≝ 1500 | sws_state : 1501 (* current statement *) 1502 ∀sss_statement : statement. 1503 (* statement after transformation *) 1504 ∀sss_result : swret statement. 1505 (* label universe *) 1506 ∀sss_lu : universe SymbolTag. 1507 (* [sss_lu] must be fresh *) 1508 ∀sss_lu_fresh : fresh_for_statement sss_statement sss_lu. 1509 (* current function *) 1510 ∀sss_func : function. 1511 (* current function after translation *) 1512 ∀sss_func_tr : function. 1513 (* variables generated during conversion of the function *) 1514 ∀sss_new_vars : list (ident × type). 1515 (* statement of the transformation *) 1516 ∀sss_func_hyp : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func. 1517 (* memory state before conversion *) 1518 ∀sss_m : mem. 1519 (* memory state after conversion *) 1520 ∀sss_m_ext : mem. 1521 (* environment before conversion *) 1522 ∀sss_env : env. 1523 (* environment after conversion *) 1524 ∀sss_env_ext : env. 1525 (* continuation before conversion *) 1526 ∀sss_k : cont. 1527 (* continuation after conversion *) 1528 ∀sss_k_ext : cont. 1529 (* memory "injection" *) 1530 ∀sss_mem_hyp : sr_memext sss_m sss_m_ext. 1531 (* The extended environment does not interfer with the old one. *) 1532 ∀sss_env_hyp : disjoint_extension sss_env sss_m sss_env_ext sss_m_ext sss_new_vars sss_mem_hyp. 1533 (* conversion of the current statement, using the variables produced during the conversion of the current function *) 1534 ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result. 1535 (* simulation between the continuations before and after conversion. *) 1536 ∀sss_k_hyp : switch_cont_sim (map ?? (fst ??) sss_new_vars) sss_k sss_k_ext. 1537 ext_fresh_for_genv sss_new_vars ge → 2070 1538 switch_state_sim 2071 (State f s k env m) 2072 (State f' (ret_st ? result) k' env' m') 1539 ge 1540 (State sss_func sss_statement sss_k sss_env sss_m) 1541 (State sss_func_tr (ret_st … sss_result) sss_k_ext sss_env_ext sss_m_ext) 2073 1542 | sws_callstate : ∀vars, fd,args,k,k',m. 2074 1543 switch_cont_sim vars k k' → 2075 switch_state_sim (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) 2076 | sws_returnstate : ∀vars,res,k,k',m. 2077 switch_cont_sim vars k k' → 2078 switch_state_sim (Returnstate res k m) (Returnstate res k' m) 1544 switch_state_sim ge (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) 1545 | sws_returnstate : 1546 ∀ssr_vars. 1547 ∀ssr_result. 1548 ∀ssr_k : cont. 1549 ∀ssr_k_ext : cont. 1550 ∀ssr_m : mem. 1551 ∀ssr_m_ext : mem. 1552 ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext. 1553 switch_cont_sim ssr_vars ssr_k ssr_k_ext → 1554 switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext) 2079 1555 | sws_finalstate : ∀r. 2080 switch_state_sim (Finalstate r) (Finalstate r).1556 switch_state_sim ge (Finalstate r) (Finalstate r). 2081 1557 2082 1558 lemma call_cont_swremoval : ∀fv,k,k'. … … 2107 1583 #ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP} (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *) 2108 1584 qed. 2109 (* 2110 lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 2111 ∃t'.eventually ge P s (t ⧺ t'). 2112 #ge #P #s #t * #s' * #Hexec #HP %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} 2113 qed. 2114 *) 1585 2115 1586 lemma eventually_later : ∀ge,P,s,t. 2116 1587 (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) → … … 2120 1591 qed. 2121 1592 2122 (* lift value_eq to option block *)2123 definition option_block_eq ≝ λE,ob1,ob2.2124 match ob1 with2125 [ None ⇒2126 match ob2 with2127 [ None ⇒ True2128 | Some _ ⇒ False ]2129 | Some b1 ⇒2130 match ob2 with2131 [ None ⇒ False2132 | Some b2 ⇒ value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset)) ]2133 ].2134 2135 definition value_eq_opt ≝ λE,ov1,ov2.2136 match ov1 with2137 [ None ⇒2138 match ov2 with2139 [ None ⇒ True2140 | Some _ ⇒ False ]2141 | Some v1 ⇒2142 match ov2 with2143 [ None ⇒ False2144 | Some v2 ⇒2145 value_eq E v1 v2 ]2146 ].2147 2148 record switch_removal_globals (E : embedding) (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {2149 rg_find_symbol: ∀s.2150 option_block_eq E (find_symbol ? ge s) (find_symbol ? ge' s);2151 rg_find_funct: ∀v,f.2152 find_funct ? ge v = Some ? f →2153 find_funct ? ge' v = Some ? (t f);2154 rg_find_funct_ptr: ∀b,f.2155 find_funct_ptr ? ge b = Some ? f →2156 find_funct_ptr ? ge' b = Some ? (t f)2157 }.2158 2159 1593 lemma exec_lvalue_expr_elim : 2160 ∀E,r1,r2,Pok,Qok. 2161 ∀H:exec_lvalue_sim E r1 r2. 2162 (∀bo1,bo2,tr. 2163 let 〈b1,o1〉 ≝ bo1 in 2164 let 〈b2,o2〉 ≝ bo2 in 2165 value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) → 2166 match Pok 〈bo1,tr〉 with 1594 ∀r1,r2,Pok,Qok. 1595 exec_lvalue_sim r1 r2 → 1596 (∀val,trace. 1597 match Pok 〈val,trace〉 with 2167 1598 [ Error err ⇒ True 2168 | OK vt1⇒2169 let 〈 val1,trace1〉 ≝ vt1in2170 match Qok 〈 bo2,tr〉 with1599 | OK pvt ⇒ 1600 let 〈pval,ptrace〉 ≝ pvt in 1601 match Qok 〈val,trace〉 with 2171 1602 [ Error err ⇒ False 2172 | OK vt2⇒2173 let 〈 val2,trace2〉 ≝ vt2in2174 trace1 = trace2 ∧ value_eq E val1 val21603 | OK qvt ⇒ 1604 let 〈qval,qtrace〉 ≝ qvt in 1605 ptrace = qtrace ∧ pval = qval 2175 1606 ] 2176 ]) → 2177 exec_expr_sim E1607 ]) → 1608 exec_expr_sim 2178 1609 (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) 2179 1610 (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). 2180 #E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); 1611 #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); 1612 elim r1 1613 [ 2: #error #_ #_ normalize #a #Habsurd destruct (Habsurd) 1614 | 1: normalize nodelta #a #H lapply (H a (refl ??)) 1615 #Hr2 >Hr2 normalize #H #a' elim a * #b #o #tr 1616 lapply (H 〈b, o〉 tr) #H1 #H2 >H2 in H1; 1617 normalize nodelta elim a' in H2; #pval #ptrace #Hpok 1618 normalize nodelta cases (Qok 〈b,o,tr〉) 1619 [ 2: #error normalize #Habsurd @(False_ind … Habsurd) 1620 | 1: * #qval #qtrace normalize nodelta * #Htrace #Hval 1621 destruct @refl 1622 ] ] qed. 1623 1624 1625 lemma exec_expr_expr_elim : 1626 ∀r1,r2,Pok,Qok. 1627 exec_expr_sim r1 r2 → 1628 (∀val,trace. 1629 match Pok 〈val,trace〉 with 1630 [ Error err ⇒ True 1631 | OK pvt ⇒ 1632 let 〈pval,ptrace〉 ≝ pvt in 1633 match Qok 〈val,trace〉 with 1634 [ Error err ⇒ False 1635 | OK qvt ⇒ 1636 let 〈qval,qtrace〉 ≝ qvt in 1637 ptrace = qtrace ∧ pval = qval 1638 ] 1639 ]) → 1640 exec_expr_sim 1641 (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) 1642 (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). 1643 #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); 2181 1644 elim r1 2182 1645 [ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd) 2183 | 1: normalize nodelta #a1 #H lapply (H a1 (refl ??)) 2184 * #a2 * #Hr2 >Hr2 normalize nodelta 2185 elim a1 * #b1 #o1 #tr1 2186 elim a2 * #b2 #o2 #tr2 normalize nodelta 2187 * #Hvalue_eq #Htrace_eq #H2 2188 destruct (Htrace_eq) 2189 lapply (H2 〈b1, o1〉 〈b2, o2〉 tr2 Hvalue_eq) 2190 cases (Pok 〈b1, o1, tr2〉) 2191 [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd) 2192 | 1: * #v1 #tr1' normalize nodelta #H3 whd 2193 * #v1' #tr1'' #Heq destruct (Heq) 2194 cases (Qok 〈b2,o2,tr2〉) in H3; 2195 [ 2: #error #Hfalse @(False_ind … Hfalse) 2196 | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq) 2197 #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj // 1646 | 1: normalize nodelta #a #H lapply (H a (refl ??)) 1647 #Hr2 >Hr2 normalize nodelta #H 1648 elim a in Hr2; #val #trace 1649 lapply (H … val trace) 1650 cases (Pok 〈val, trace〉) 1651 [ 2: #error normalize #_ #_ #a' #Habsurd destruct (Habsurd) 1652 | 1: * #pval #ptrace normalize nodelta 1653 cases (Qok 〈val,trace〉) 1654 [ 2: #error normalize #Hfalse @(False_ind … Hfalse) 1655 | 1: * #qval #qtrace normalize nodelta * #Htrace_eq #Hval_eq 1656 #Hr2_eq destruct #a #H @H 2198 1657 ] ] ] qed. 2199 1658 2200 lemma exec_expr_expr_elim : 2201 ∀E,r1,r2,Pok,Qok. 2202 ∀H:exec_expr_sim E r1 r2. 2203 (∀v1,v2,trace. 2204 value_eq E v1 v2 → 2205 match Pok 〈v1,trace〉 with 2206 [ Error err ⇒ True 2207 | OK vt1 ⇒ 2208 let 〈val1,trace1〉 ≝ vt1 in 2209 match Qok 〈v2,trace〉 with 2210 [ Error err ⇒ False 2211 | OK vt2 ⇒ 2212 let 〈val2,trace2〉 ≝ vt2 in 2213 trace1 = trace2 ∧ value_eq E val1 val2 2214 ] 2215 ]) → 2216 exec_expr_sim E 2217 (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) 2218 (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). 2219 #E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); 2220 elim r1 2221 [ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd) 2222 | 1: normalize nodelta #a1 #H lapply (H a1 (refl ??)) 2223 * #a2 * #Hr2 >Hr2 normalize nodelta 2224 elim a1 #v1 #tr1 2225 elim a2 #v2 #tr2 normalize nodelta 2226 * #Hvalue_eq #Htrace_eq #H2 2227 destruct (Htrace_eq) 2228 lapply (H2 v1 v2 tr2 Hvalue_eq) 2229 cases (Pok 〈v1, tr2〉) 2230 [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd) 2231 | 1: * #v1 #tr1' normalize nodelta #H3 whd 2232 * #v1' #tr1'' #Heq destruct (Heq) 2233 cases (Qok 〈v2,tr2〉) in H3; 2234 [ 2: #error #Hfalse @(False_ind … Hfalse) 2235 | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq) 2236 #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj // 2237 ] ] ] qed. 2238 2239 (* Commutation results of standard binary operations with value_eq. *) 2240 lemma unary_operation_value_eq : 2241 ∀E,op,v1,v2,ty. 2242 value_eq E v1 v2 → 2243 ∀r1. 2244 sem_unary_operation op v1 ty = Some ? r1 → 2245 ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2. 2246 #E #op #v1 #v2 #ty #Hvalue_eq #r1 2247 inversion Hvalue_eq 2248 [ 1: #v #Hv1 #Hv2 #_ destruct 2249 cases op normalize 2250 [ 1: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2251 normalize #Habsurd destruct (Habsurd) 2252 | 3: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2253 normalize #Habsurd destruct (Habsurd) 2254 | 2: #Habsurd destruct (Habsurd) ] 2255 | 2: #vsz #i #Hv1 #Hv2 #_ 2256 cases op 2257 [ 1: cases ty 2258 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2259 whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???); 2260 [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct 2261 %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))} 2262 cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj 2263 // 2264 | *: #Habsurd destruct (Habsurd) ] 2265 | 2: whd in match (sem_unary_operation ???); 2266 #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj // 2267 | 3: whd in match (sem_unary_operation ???); 2268 cases ty 2269 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2270 normalize nodelta 2271 whd in ⊢ ((??%?) → ?); 2272 [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct 2273 %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj // 2274 | *: #Habsurd destruct (Habsurd) ] ] 2275 | 3: #f #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???); 2276 cases op normalize nodelta 2277 [ 1: cases ty 2278 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2279 whd in match (sem_notbool ??); 2280 #Heq1 destruct 2281 cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/ 2282 | 2: normalize #Habsurd destruct (Habsurd) 2283 | 3: cases ty 2284 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2285 whd in match (sem_neg ??); 2286 #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ] 2287 | 4: #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???); 2288 cases op normalize nodelta 2289 [ 1: cases ty 2290 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2291 whd in match (sem_notbool ??); 2292 #Heq1 destruct /3 by ex_intro, vint_eq, conj/ 2293 | 2: normalize #Habsurd destruct (Habsurd) 2294 | 3: cases ty 2295 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2296 whd in match (sem_neg ??); 2297 #Heq1 destruct ] 2298 | 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_ whd in match (sem_unary_operation ???); 2299 cases op normalize nodelta 2300 [ 1: cases ty 2301 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2302 whd in match (sem_notbool ??); 2303 #Heq1 destruct /3 by ex_intro, vint_eq, conj/ 2304 | 2: normalize #Habsurd destruct (Habsurd) 2305 | 3: cases ty 2306 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2307 whd in match (sem_neg ??); 2308 #Heq1 destruct ] 2309 ] 2310 qed. 2311 2312 lemma commutative_add_with_carries : ∀n,a,b,carry. add_with_carries n a b carry = add_with_carries n b a carry. 2313 #n elim n 2314 [ 1: #a #b #carry 2315 lapply (BitVector_O … a) lapply (BitVector_O … b) #H1 #H2 destruct @refl 2316 | 2: #n' #Hind #a #b #carry 2317 lapply (BitVector_Sn … a) lapply (BitVector_Sn … b) 2318 * #bhd * #btl #Heqb 2319 * #ahd * #atl #Heqa destruct 2320 lapply (Hind atl btl carry) 2321 whd in match (add_with_carries ????) in ⊢ ((??%%) → (??%%)); 2322 normalize in match (rewrite_l ??????); 1659 1660 lemma load_value_of_type_inj : ∀m1,m2,b,off,ty. 1661 sr_memext m1 m2 → ∀v. 1662 load_value_of_type ty m1 b off = Some ? v → 1663 load_value_of_type ty m2 b off = Some ? v. 1664 #m1 #m2 #b #off #ty #Hinj #v 1665 @(load_sim_fe … (me_inj … Hinj) (mk_pointer b off)) 1666 qed. 1667 1668 (* Conservation of the smenantics of binary operators *) 1669 lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2. 1670 ∀Hext:sr_memext m1 m2. ∀res. 1671 sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res → 1672 sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res. 1673 #op #v1 #v2 #e1 #e2 #m1 #m2 #Hmemext #res cases op 1674 whd in match (sem_binary_operation ??????); 1675 try // 1676 whd in match (sem_binary_operation ??????); 1677 elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1 1678 elim m2 #contents2 #nextblocks2 #Hnextpos2 1679 * #Hptrsim #writeable #Hvalid #Hdisjoint #Hvalid_cons 1680 whd in match (sem_cmp ??????); 1681 whd in match (sem_cmp ??????); 1682 [ 1: cases (classify_cmp (typeof e1) (typeof e2)) 2323 1683 normalize nodelta 2324 #Heq >Heq 2325 generalize in match (fold_right2_i ????????); * #res #carries 1684 [ 1: #sz #sg try // 1685 | 2: #opt #ty 1686 cases v1 normalize nodelta 1687 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 1688 [ 1,2,3: #Habsurd destruct (Habsurd) 1689 | 4: #H @H ] 1690 cases v2 normalize nodelta 1691 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 1692 [ 1,2,3: #Habsurd destruct (Habsurd) 1693 | 4: #H @H ] 1694 lapply (Hvalid_cons ptr) 1695 elim (freed_pointer_dec … (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 1696 [ 2: #Hnot_freed #Hvalid lapply (Hvalid … Hnot_freed) 1697 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 1698 [ 2: >andb_lsimpl_false normalize nodelta #_ #Habsurd destruct (Habsurd) ] 1699 #Hvalid >(Hvalid (refl ??)) 1700 lapply (Hvalid_cons ptr') 1701 elim (freed_pointer_dec … (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 1702 [ 2: #Hnot_freed' #Hvalid' lapply (Hvalid' … Hnot_freed') 1703 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 1704 [ 2: >andb_lsimpl_true #_ normalize nodelta #Habsurd destruct (Habsurd) ] 1705 #H' >(H' (refl ??)) >andb_lsimpl_true #Hres @Hres 1706 | 1: normalize in ⊢ (% → ?); * #Hlow' #Hhigh' #_ 1707 >andb_lsimpl_true >andb_lsimpl_true 1708 whd in match (valid_pointer ??); 1709 whd in match (low_bound ??); 1710 whd in match (high_bound ??); 1711 >Hlow' >Hhigh' >Zleb_unsigned_OZ >andb_comm >andb_lsimpl_true 1712 whd in match (valid_pointer ??); 1713 1714 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 1715 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1716 #H' >(H' (refl ??)) #Hok @Hok 1717 | 1: 1718 ] 1719 | 3: #fsz #H @H 1720 | 4: #ty1 #ty2 #H @H ] 1721 | 2: cases (classify_cmp (typeof e1) (typeof e2)) 2326 1722 normalize nodelta 2327 cases ahd cases bhd @refl 1723 [ 1: #sz #sg try // 1724 | 2: #opt #ty 1725 cases v1 normalize nodelta 1726 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 1727 [ 1,2,3: #Habsurd destruct (Habsurd) 1728 | 4: #H @H ] 1729 cases v2 normalize nodelta 1730 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 1731 [ 1,2,3: #Habsurd destruct (Habsurd) 1732 | 4: #H @H ] 1733 lapply (Hvalid_cons ptr) 1734 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 1735 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1736 #H >(H (refl ??)) 1737 lapply (Hvalid_cons ptr') 1738 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 1739 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1740 #H' >(H' (refl ??)) #Hok @Hok 1741 | 3: #fsz #H @H 1742 | 4: #ty1 #ty2 #H @H ] 1743 | 3: cases (classify_cmp (typeof e1) (typeof e2)) 1744 normalize nodelta 1745 [ 1: #sz #sg try // 1746 | 2: #opt #ty 1747 cases v1 normalize nodelta 1748 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 1749 [ 1,2,3: #Habsurd destruct (Habsurd) 1750 | 4: #H @H ] 1751 cases v2 normalize nodelta 1752 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 1753 [ 1,2,3: #Habsurd destruct (Habsurd) 1754 | 4: #H @H ] 1755 lapply (Hvalid_cons ptr) 1756 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 1757 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1758 #H >(H (refl ??)) 1759 lapply (Hvalid_cons ptr') 1760 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 1761 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1762 #H' >(H' (refl ??)) #Hok @Hok 1763 | 3: #fsz #H @H 1764 | 4: #ty1 #ty2 #H @H ] 1765 | 4: cases (classify_cmp (typeof e1) (typeof e2)) 1766 normalize nodelta 1767 [ 1: #sz #sg #H @H 1768 | 2: #opt #ty 1769 cases v1 normalize nodelta 1770 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 1771 [ 1,2,3: #Habsurd destruct (Habsurd) 1772 | 4: #H @H ] 1773 cases v2 normalize nodelta 1774 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 1775 [ 1,2,3: #Habsurd destruct (Habsurd) 1776 | 4: #H @H ] 1777 lapply (Hvalid_cons ptr) 1778 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 1779 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1780 #H >(H (refl ??)) 1781 lapply (Hvalid_cons ptr') 1782 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 1783 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1784 #H' >(H' (refl ??)) #Hok @Hok 1785 | 3: #fsz #H @H 1786 | 4: #ty1 #ty2 #H @H ] 1787 | 5: cases (classify_cmp (typeof e1) (typeof e2)) 1788 normalize nodelta 1789 [ 1: #sz #sg #H @H 1790 | 2: #opt #ty 1791 cases v1 normalize nodelta 1792 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 1793 [ 1,2,3: #Habsurd destruct (Habsurd) 1794 | 4: #H @H ] 1795 cases v2 normalize nodelta 1796 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 1797 [ 1,2,3: #Habsurd destruct (Habsurd) 1798 | 4: #H @H ] 1799 lapply (Hvalid_cons ptr) 1800 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 1801 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1802 #H >(H (refl ??)) 1803 lapply (Hvalid_cons ptr') 1804 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 1805 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1806 #H' >(H' (refl ??)) #Hok @Hok 1807 | 3: #fsz #H @H 1808 | 4: #ty1 #ty2 #H @H ] 1809 | 6: cases (classify_cmp (typeof e1) (typeof e2)) 1810 normalize nodelta 1811 [ 1: #sz #sg #H @H 1812 | 2: #opt #ty 1813 cases v1 normalize nodelta 1814 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 1815 [ 1,2,3: #Habsurd destruct (Habsurd) 1816 | 4: #H @H ] 1817 cases v2 normalize nodelta 1818 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 1819 [ 1,2,3: #Habsurd destruct (Habsurd) 1820 | 4: #H @H ] 1821 lapply (Hvalid_cons ptr) 1822 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 1823 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1824 #H >(H (refl ??)) 1825 lapply (Hvalid_cons ptr') 1826 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 1827 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 1828 #H' >(H' (refl ??)) #Hok @Hok 1829 | 3: #fsz #H @H 1830 | 4: #ty1 #ty2 #H @H ] 2328 1831 ] qed. 2329 1832 2330 2331 lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a. 2332 #n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries 2333 @refl 2334 qed. 2335 2336 (* -------------------------------------------------------------------------- *) 2337 (* Associativity proof for addition_n. The proof relies on the observation 2338 * that the two carries (inner and outer) in the associativity equation are not 2339 * independent. In fact, the global carry can be encoded in a three-valued bits 2340 * (versus 2 full bits, i.e. 4 possibilites, for two carries). *) 2341 2342 inductive ternary : Type[0] ≝ 2343 | Zero_carry : ternary 2344 | One_carry : ternary 2345 | Two_carry : ternary. 2346 2347 definition carry_0 ≝ λcarry. 2348 match carry with 2349 [ Zero_carry ⇒ 〈false, Zero_carry〉 2350 | One_carry ⇒ 〈true, Zero_carry〉 2351 | Two_carry ⇒ 〈false, One_carry〉 ]. 2352 2353 definition carry_1 ≝ λcarry. 2354 match carry with 2355 [ Zero_carry ⇒ 〈true, Zero_carry〉 2356 | One_carry ⇒ 〈false, One_carry〉 2357 | Two_carry ⇒ 〈true, One_carry〉 ]. 2358 2359 definition carry_2 ≝ λcarry. 2360 match carry with 2361 [ Zero_carry ⇒ 〈false, One_carry〉 2362 | One_carry ⇒ 〈true, One_carry〉 2363 | Two_carry ⇒ 〈false, Two_carry〉 ]. 2364 2365 definition carry_3 ≝ λcarry. 2366 match carry with 2367 [ Zero_carry ⇒ 〈true, One_carry〉 2368 | One_carry ⇒ 〈false, Two_carry〉 2369 | Two_carry ⇒ 〈true, Two_carry〉 ]. 2370 2371 (* Count the number of true bits in {xa,xb,xc} and compute the new bit along the new carry, 2372 according to the last one. *) 2373 definition ternary_carry_of ≝ λxa,xb,xc,carry. 2374 if xa then 2375 if xb then 2376 if xc then 2377 carry_3 carry 2378 else 2379 carry_2 carry 2380 else 2381 if xc then 2382 carry_2 carry 2383 else 2384 carry_1 carry 2385 else 2386 if xb then 2387 if xc then 2388 carry_2 carry 2389 else 2390 carry_1 carry 2391 else 2392 if xc then 2393 carry_1 carry 2394 else 2395 carry_0 carry. 2396 2397 let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝ 2398 match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with 2399 [ VEmpty ⇒ λ_,_. 〈VEmpty ?, init〉 2400 | VCons sz' xa tla ⇒ λb',c'. 2401 let xb ≝ head' … b' in 2402 let xc ≝ head' … c' in 2403 let tlb ≝ tail … b' in 2404 let tlc ≝ tail … c' in 2405 let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc init in 2406 let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in 2407 〈bit ::: bits, carry〉 2408 ] b c. 2409 2410 (* convert the classical carries (inner and outer) to ternary) *) 2411 definition carries_to_ternary ≝ λcarry1,carry2. 2412 if carry1 2413 then if carry2 2414 then Two_carry 2415 else One_carry 2416 else if carry2 2417 then One_carry 2418 else Zero_carry. 2419 2420 lemma add_with_carries_Sn : ∀n,a_hd,a_tl,b_hd,b_tl,carry. 2421 add_with_carries (S n) (a_hd ::: a_tl) (b_hd ::: b_tl) carry = 2422 (let 〈lower_bits,carries〉 ≝ add_with_carries n a_tl b_tl carry in 2423 let last_carry ≝ 2424 match carries in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 2425 [VEmpty⇒carry 2426 |VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy] 2427 in 2428 if last_carry then 2429 let bit ≝ xorb (xorb a_hd b_hd) true in 2430 let carry ≝ carry_of a_hd b_hd true in 2431 〈bit:::lower_bits,carry:::carries〉 2432 else 2433 let bit ≝ xorb (xorb a_hd b_hd) false in 2434 let carry ≝ carry_of a_hd b_hd false in 2435 〈bit:::lower_bits,carry:::carries〉). 2436 #n #a_hd #a_tl #b_hd #b_tl #carry 2437 whd in match (add_with_carries ????); 2438 normalize nodelta 2439 <add_with_carries_unfold 2440 cases (add_with_carries n a_tl b_tl carry) 2441 #lower_bits #carries normalize nodelta 2442 elim n in a_tl b_tl lower_bits carries; 2443 [ 1: #a_tl #b_tl #lower_bits #carries 2444 >(BitVector_O … carries) normalize nodelta 2445 cases carry normalize nodelta 2446 cases a_hd cases b_hd // 2447 | 2: #n' #Hind #a_tl #b_tl #lower_bits #carries 2448 lapply (BitVector_Sn … carries) * #carries_hd * #carries_tl 2449 #Heq >Heq normalize nodelta 2450 cases carries_hd cases a_hd cases b_hd normalize nodelta 2451 // 2452 ] qed. 2453 2454 (* Correction of [canonical_add], left side. Note the invariant on carries. *) 2455 lemma canonical_add_left : ∀n,carry1,carry2,a,b,c. 2456 let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b carry1 in 2457 let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c carry2 in 2458 let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in 2459 res_ab_c = res_canonical 2460 ∧ (match n return λx. BitVector x → BitVector x → Prop with 2461 [ O ⇒ λ_.λ_. True 2462 | S _ ⇒ λflags_ab',flags_ab_c'. carries_to_ternary (head' … flags_ab') (head' … flags_ab_c') = last_carry 2463 ] flags_ab flags_ab_c). 2464 #n elim n 2465 [ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try // 2466 | 2: #n' #Hind #carry1 #carry2 #a #b #c 2467 elim (BitVector_Sn … a) #xa * #a' #Heq_a 2468 elim (BitVector_Sn … b) #xb * #b' #Heq_b 2469 elim (BitVector_Sn … c) #xc * #c' #Heq_c 2470 lapply (Hind … carry1 carry2 a' b' c') -Hind 2471 destruct >add_with_carries_Sn 2472 elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta 2473 lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a' 2474 -Hflags_ab -Hres_ab -c' -b' -a' 2475 cases n' 2476 [ 1: #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta 2477 >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c') 2478 >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab) 2479 normalize nodelta #_ 2480 cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try // 2481 | 2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta 2482 elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab 2483 normalize nodelta 2484 elim (BitVector_Sn … Hres_ab) #hd_res_ab * #tl_res_ab #Heq_res_ab >Heq_res_ab 2485 cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta 2486 >add_with_carries_Sn 2487 elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c 2488 normalize nodelta 2489 elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c 2490 normalize nodelta 2491 cases hd_flags_ab_c in Heq_flags_ab_c; #Heq_flags_ab_c 2492 normalize nodelta 2493 whd in match (canonical_add (S (S ?)) ? ? ? ?); 2494 whd in match (tail ???); whd in match (tail ???); 2495 elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize 2496 * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize 2497 >Hres_ab_is_canonical 2498 cases xa cases xb cases xc try @conj try @refl 2499 ] 2500 ] qed. 2501 2502 (* Symmetric. The two sides are most certainly doable in a single induction, but lazyness 2503 prevails over style. *) 2504 lemma canonical_add_right : ∀n,carry1,carry2,a,b,c. 2505 let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c carry1 in 2506 let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc carry2 in 2507 let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in 2508 res_a_bc = res_canonical 2509 ∧ (match n return λx. BitVector x → BitVector x → Prop with 2510 [ O ⇒ λ_.λ_. True 2511 | S _ ⇒ λflags_bc',flags_a_bc'. carries_to_ternary (head' … flags_bc') (head' … flags_a_bc') = last_carry 2512 ] flags_bc flags_a_bc). 2513 #n elim n 2514 [ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try // 2515 | 2: #n' #Hind #carry1 #carry2 #a #b #c 2516 elim (BitVector_Sn … a) #xa * #a' #Heq_a 2517 elim (BitVector_Sn … b) #xb * #b' #Heq_b 2518 elim (BitVector_Sn … c) #xc * #c' #Heq_c 2519 lapply (Hind … carry1 carry2 a' b' c') -Hind 2520 destruct >add_with_carries_Sn 2521 elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta 2522 lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a' 2523 -Hflags_bc -Hres_bc -c' -b' -a' 2524 cases n' 2525 [ 1: #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta 2526 >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c') 2527 >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc) 2528 normalize nodelta #_ 2529 cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try // 2530 | 2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta 2531 elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc 2532 normalize nodelta 2533 elim (BitVector_Sn … Hres_bc) #hd_res_bc * #tl_res_bc #Heq_res_bc >Heq_res_bc 2534 cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta 2535 >add_with_carries_Sn 2536 elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc 2537 normalize nodelta 2538 elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc 2539 normalize nodelta 2540 cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc 2541 whd in match (canonical_add (S (S ?)) ????); 2542 whd in match (tail ???); whd in match (tail ???); 2543 elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize 2544 * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize 2545 >Hres_bc_is_canonical 2546 cases xa cases xb cases xc try @conj try @refl 2547 ] 2548 ] qed. 2549 2550 2551 (* Note that we prove a result more general that just associativity: we can vary the carries. *) 2552 lemma associative_add_with_carries : 2553 ∀n,carry1,carry2,a,b,c. 2554 (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c carry1 in res) carry2)) 2555 = 2556 (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b carry1 in res) c carry2)). 2557 #n cases n 2558 [ 1: #carry1 #carry2 #a #b #c 2559 >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) 2560 normalize try @refl 2561 | 2: #n' #carry1 #carry2 #a #b #c 2562 lapply (canonical_add_left … carry1 carry2 a b c) 2563 lapply (canonical_add_right … carry1 carry2 a b c) 2564 normalize nodelta 2565 elim (add_with_carries (S n') b c carry1) #res_bc #flags_bc 2566 elim (add_with_carries (S n') a b carry1) #res_ab #flags_ab 2567 normalize nodelta 2568 elim (add_with_carries (S n') a res_bc carry2) #res_a_bc #flags_a_bc 2569 normalize nodelta 2570 elim (add_with_carries (S n') res_ab c carry2) #res_ab_c #flags_ab_c 2571 normalize nodelta 2572 cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry 2573 normalize nodelta 2574 * #HA #HB * #HC #HD destruct @refl 2575 ] qed. 2576 2577 (* This closes the proof of associativity for bitvector addition. *) 2578 2579 lemma associative_addition_n : ∀n,a,b,c. addition_n n a (addition_n n b c) = addition_n n (addition_n n a b) c. 2580 #n #a #b #c 2581 whd in match (addition_n ???) in ⊢ (??%%); 2582 whd in match (addition_n n b c); 2583 whd in match (addition_n n a b); 2584 lapply (associative_add_with_carries … false false a b c) 2585 elim (add_with_carries n b c false) #bc_bits #bc_flags 2586 elim (add_with_carries n a b false) #ab_bits #ab_flags 2587 normalize nodelta 2588 elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags 2589 elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags 2590 normalize 2591 #H @H 2592 qed. 2593 2594 2595 (* value_eq lifts to addition *) 2596 lemma add_value_eq : 2597 ∀E,v1,v2,v1',v2',ty1,ty2. 2598 value_eq E v1 v2 → 2599 value_eq E v1' v2' → 2600 (* memory_inj E m1 m2 → This injection seems useless TODO *) 2601 ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→ 2602 ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 2603 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 2604 @(value_eq_inversion E … Hvalue_eq1) 2605 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 2606 [ 1: whd in match (sem_add ????); normalize nodelta 2607 cases (classify_add ty1 ty2) normalize nodelta 2608 [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ] 2609 #Habsurd destruct (Habsurd) 2610 | 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 2611 cases (classify_add ty1 ty2) normalize nodelta 2612 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2613 [ 2,3,5: #Habsurd destruct (Habsurd) ] 2614 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2615 [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ] 2616 [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ] 2617 [ 1: @intsize_eq_elim_elim 2618 [ 1: #_ #Habsurd destruct (Habsurd) 2619 | 2: #Heq destruct (Heq) normalize nodelta 2620 #Heq destruct (Heq) 2621 /3 by ex_intro, conj, vint_eq/ ] 2622 | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct 2623 /3 by ex_intro, conj, vint_eq/ 2624 | 3: #Heq destruct (Heq) 2625 normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed 2626 %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl 2627 @vptr_eq whd in match (pointer_translation ??); 2628 cases (E b1') in Hembed; 2629 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2630 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) 2631 whd in match (shift_pointer_n ????); 2632 cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset = 2633 (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) i)) 2634 [ 1: whd in match (offset_plus ??); 2635 whd in match (shift_offset_n ????) in ⊢ (??%%); 2636 >commutative_addition_n >associative_addition_n 2637 <(commutative_addition_n … (offv offset) (offv o1')) @refl ] 2638 #Heq >Heq @refl ] 2639 ] 2640 | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 2641 cases (classify_add ty1 ty2) normalize nodelta 2642 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2643 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2644 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2645 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2646 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2647 #Heq destruct (Heq) 2648 /3 by ex_intro, conj, vfloat_eq/ 2649 | 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 2650 cases (classify_add ty1 ty2) normalize nodelta 2651 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2652 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2653 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2654 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2655 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2656 @eq_bv_elim 2657 [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ 2658 | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2659 | 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 2660 cases (classify_add ty1 ty2) normalize nodelta 2661 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2662 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2663 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2664 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2665 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2666 #Heq destruct (Heq) 2667 %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl 2668 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 2669 elim p1 in Hembed; #b1 #o1 normalize nodelta 2670 cases (E b1) 2671 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2672 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) 2673 whd in match (shift_pointer_n ????); 2674 whd in match (shift_offset_n ????) in ⊢ (??%%); 2675 whd in match (offset_plus ??); 2676 whd in match (offset_plus ??); 2677 >commutative_addition_n >(associative_addition_n … offset_size ?) 2678 >(commutative_addition_n ? (offv offset) ?) @refl 2679 ] 2680 ] qed. 2681 2682 lemma map_Sn : ∀A,B:Type[0].∀n,f,hd.∀tl:Vector A n. 2683 map A B (S n) f (hd ::: tl) = (f hd) ::: (map A B n f tl). 2684 #A #B #n #f #hd #tl normalize @refl qed. 2685 2686 lemma replicate_Sn : ∀A,sz,elt. 2687 replicate A (S sz) elt = elt ::: (replicate A sz elt). 2688 // qed. 2689 2690 lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed. 2691 2692 lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a). 2693 #n #xa #a normalize @refl qed. 2694 2695 2696 (* useful facts on xorb *) 2697 2698 lemma xorb_neg : ∀a,b. notb (xorb a b) = xorb a (notb b). * * @refl qed. 2699 lemma xorb_false : ∀a. xorb a false = a. * @refl qed. 2700 lemma xorb_true : ∀a. xorb a true = (¬a). * @refl qed. 2701 lemma xorb_comm : ∀a,b. xorb a b = xorb b a. * * @refl qed. 2702 lemma xorb_assoc : ∀a,b,c. xorb a (xorb b c) = xorb (xorb a b) c. * * * @refl qed. 2703 lemma xorb_lneg : ∀a,b. xorb (¬a) b = (¬xorb a b). * * @refl qed. 2704 lemma xorb_rneg : ∀a,b. xorb a (¬b) = (¬xorb a b). * * @refl qed. 2705 lemma xorb_inj : ∀a,b,c. xorb a b = xorb a c ↔ b = c. * * * @conj try // normalize try // qed. 2706 2707 (* useful facts on carry_of *) 2708 lemma carry_of_TT : ∀x. carry_of true true x = true. // qed. 2709 lemma carry_of_TF : ∀x. carry_of true false x = x. // qed. 2710 lemma carry_of_FF : ∀x. carry_of false false x = false. // qed. 2711 lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed. 2712 lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed. 2713 2714 (* useful facts on various boolean operations *) 2715 lemma andb_lsimpl_true : ∀x. andb true x = x. // qed. 2716 lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed. 2717 lemma andb_comm : ∀x,y. andb x y = andb y x. // qed. 2718 lemma notb_true : notb true = false. // qed. 2719 lemma notb_false : notb false = true. % #H destruct qed. 2720 lemma notb_fold : ∀x. if x then false else true = (¬x). // qed. 2721 2722 (* 2723 let rec one_bv (n : nat) on n : BitVector n ≝ 2724 match n return λx. BitVector x with 2725 [ O ⇒ [[]] 2726 | S x' ⇒ 2727 match x' return λx. x = x' → BitVector (S x) with 2728 [ O ⇒ λ_. [[true]] 2729 | S x ⇒ λH. ? ] (refl ? x') ]. 2730 >H @(false ::: (one_bv x')) 2731 qed. 2732 *) 2733 definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)). 2734 2735 lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n). 2736 add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 → 2737 add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉. 2738 #n elim n 2739 [ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits 2740 elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags 2741 >(BitVector_O … tl_flags) >(BitVector_O … tl_bits) 2742 normalize #Heq destruct (Heq) @refl 2743 | 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits 2744 destruct #Hind >add_with_carries_Sn >replicate_Sn 2745 whd in match (zero ?) in Hind; lapply Hind 2746 elim (add_with_carries (S (S n')) 2747 (false:::replicate bool (S n') false) 2748 (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct 2749 normalize >add_with_carries_Sn in Hind; 2750 elim (add_with_carries (S n') (replicate bool (S n') false) 2751 (replicate bool (S n') false) true) #flags' #bits' 2752 normalize 2753 cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 2754 [VEmpty⇒true|VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy]) 2755 normalize #Heq destruct @refl 2756 ] qed. 2757 2758 lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)). 2759 #n lapply (one_bv_Sn_aux n) 2760 whd in match (one_bv ?) in ⊢ (? → (??%%)); 2761 elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags 2762 #H lapply (H bits flags (refl ??)) #H2 >H2 @refl 2763 qed. 2764 2765 lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n. 2766 add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false. 2767 #n 2768 elim n 2769 [ 1: #a >(BitVector_O … a) normalize @refl 2770 | 2: #n' cases n' 2771 [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct 2772 >(BitVector_O … tl) normalize cases xa @refl 2773 | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct 2774 >one_bv_Sn >zero_Sn 2775 lapply (Hind tl) 2776 >add_with_carries_Sn >add_with_carries_Sn 2777 #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags 2778 normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq 2779 normalize nodelta @refl 2780 ] qed. 2781 2782 (* In order to use associativity on increment, we hide it under addition_n. *) 2783 lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n). 2784 #n 2785 whd in match (increment ??) in ⊢ (∀_.??%?); 2786 whd in match (addition_n ???) in ⊢ (∀_.???%); 2787 #a lapply (increment_to_addition_n_aux n a) 2788 #Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl 2789 qed. 2790 2791 (* Explicit formulation of addition *) 2792 2793 (* Explicit formulation of the last carry bit *) 2794 let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝ 2795 match n return λx. BitVector x → BitVector x → bool with 2796 [ O ⇒ λ_,_. init 2797 | S x ⇒ λa',b'. 2798 let hd_a ≝ head' … a' in 2799 let hd_b ≝ head' … b' in 2800 let tl_a ≝ tail … a' in 2801 let tl_b ≝ tail … b' in 2802 carry_of hd_a hd_b (ith_carry x tl_a tl_b init) 2803 ] a b. 2804 2805 lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n). 2806 ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)). 2807 #n #init #a #b @refl qed. 2808 2809 lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n. 2810 ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed. 2811 2812 (* correction of [ith_carry] *) 2813 lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n). 2814 〈res_ab,flags_ab〉 = add_with_carries ? a b init → 2815 head' … flags_ab = ith_carry ? a b init. 2816 #n elim n 2817 [ 1: #init #a #b #res_ab #flags_ab 2818 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a 2819 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b 2820 elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res 2821 elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags 2822 destruct 2823 >(BitVector_O … tl_a) >(BitVector_O … tl_b) 2824 cases hd_a cases hd_b cases init normalize #Heq destruct (Heq) 2825 @refl 2826 | 2: #n' #Hind #init #a #b #res_ab #flags_ab 2827 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a 2828 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b 2829 elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res 2830 elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags 2831 destruct 2832 lapply (Hind … init tl_a tl_b tl_res tl_flags) 2833 >add_with_carries_Sn >(ith_carry_Sn (S n')) 2834 elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab 2835 elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab 2836 normalize nodelta cases hd_flags_ab normalize nodelta 2837 whd in match (head' ? (S n') ?); #H1 #H2 2838 destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl 2839 ] qed. 2840 2841 (* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *) 2842 definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit. 2843 match n return λx. BitVector x → BitVector x → bool with 2844 [ O ⇒ λ_,_. init 2845 | S x ⇒ λa',b'. 2846 let hd_a ≝ head' … a' in 2847 let hd_b ≝ head' … b' in 2848 let tl_a ≝ tail … a' in 2849 let tl_b ≝ tail … b' in 2850 xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init) 2851 ] a b. 2852 2853 lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n). 2854 ith_bit ? a b init = xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init). 2855 #n #a #b // qed. 2856 2857 lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n. 2858 ith_bit ? (xa ::: a) (xb ::: b) init = xorb (xorb xa xb) (ith_carry ? a b init). // qed. 2859 2860 (* correction of ith_bit *) 2861 lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n). 2862 〈res_ab,flags_ab〉 = add_with_carries ? a b init → 2863 head' … res_ab = ith_bit ? a b init. 2864 #n 2865 cases n 2866 [ 1: #init #a #b #res_ab #flags_ab 2867 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a 2868 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b 2869 elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res 2870 elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags 2871 destruct 2872 >(BitVector_O … tl_a) >(BitVector_O … tl_b) 2873 >(BitVector_O … tl_flags) >(BitVector_O … tl_res) 2874 normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl 2875 | 2: #n' #init #a #b #res_ab #flags_ab 2876 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a 2877 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b 2878 elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res 2879 elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags 2880 destruct 2881 lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags) 2882 #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry; 2883 #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags' 2884 >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2) 2885 cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %; 2886 <(H1 (refl ??)) @refl 2887 ] qed. 2888 2889 (* Transform a function from bit-vectors to bits into a vector by folding *) 2890 let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝ 2891 match v with 2892 [ VEmpty ⇒ VEmpty ? 2893 | VCons sz elt tl ⇒ 2894 let bit ≝ f ? v in 2895 bit ::: (bitvector_fold ? tl f) 2896 ]. 2897 2898 (* Two-arguments version *) 2899 let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝ 2900 match v1 with 2901 [ VEmpty ⇒ λ_. VEmpty ? 2902 | VCons sz elt tl ⇒ λv2'. 2903 let bit ≝ f ? v1 v2 in 2904 bit ::: (bitvector_fold2 ? tl (tail … v2') f) 2905 ] v2. 2906 2907 lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f. 2908 bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed. 2909 2910 (* These functions pack all the relevant information (including carries) directly. *) 2911 definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init). 2912 2913 lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init. 2914 addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed. 2915 2916 lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed. 2917 2918 (* Prove the equivalence of addition_n_direct with add_with_carries *) 2919 lemma addition_n_direct_ok : ∀n,carry,v1,v2. 2920 (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry. 2921 #n elim n 2922 [ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl 2923 | 2: #n' #Hind #carry #v1 #v2 2924 elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1 2925 elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2 2926 lapply (Hind carry tl1 tl2) 2927 lapply (ith_bit_ok ? carry v1 v2) 2928 lapply (ith_carry_ok ? carry v1 v2) 2929 destruct 2930 #Hind >addition_n_direct_Sn 2931 >ith_bit_Sn >add_with_carries_Sn 2932 elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta 2933 cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 2934 [VEmpty⇒carry|VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy]) 2935 normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??)) 2936 whd in match head'; normalize nodelta 2937 #H1 #H2 >H1 >H2 @refl 2938 ] qed. 2939 2940 (* trivially lift associativity to our new setting *) 2941 lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n. 2942 addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 = 2943 addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2. 2944 #n #carry1 #carry2 #v1 #v2 #v3 2945 <addition_n_direct_ok <addition_n_direct_ok 2946 <addition_n_direct_ok <addition_n_direct_ok 2947 lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3) 2948 elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta 2949 elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta 2950 #H @(sym_eq … H) 2951 qed. 2952 2953 lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n. 2954 addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false. 2955 #n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/ 2956 qed. 2957 2958 definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false. 2959 definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v). 2960 2961 (* fold andb on a bitvector. *) 2962 let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝ 2963 match b with 2964 [ VEmpty ⇒ true 2965 | VCons sz elt tl ⇒ 2966 andb elt (andb_fold ? tl) 2967 ]. 2968 2969 lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed. 2970 2971 lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true. 2972 #n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl 2973 qed. 2974 2975 lemma ith_increment_carry : ∀n. ∀a : BitVector (S n). 2976 ith_carry … a (one_bv ?) false = andb_fold … a. 2977 #n elim n 2978 [ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl) 2979 cases hd normalize @refl 2980 | 2: #n' #Hind #a 2981 elim (BitVector_Sn … a) #hd * #tl #Heq >Heq 2982 lapply (Hind … tl) #Hind >one_bv_Sn 2983 >ith_carry_Sn whd in match (andb_fold ??); 2984 cases hd >Hind @refl 2985 ] qed. 2986 2987 lemma ith_increment_bit : ∀n. ∀a : BitVector (S n). 2988 ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)). 2989 #n #a 2990 elim (BitVector_Sn … a) #hd * #tl #Heq >Heq 2991 whd in match (head' ???); 2992 -a cases n in tl; 2993 [ 1: #tl >(BitVector_O … tl) cases hd normalize try // 2994 | 2: #n' #tl >one_bv_Sn >ith_bit_Sn 2995 >ith_increment_carry >tail_Sn 2996 cases hd try // 2997 ] qed. 2998 2999 (* Lemma used to prove involutivity of two-complement negation *) 3000 lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n). 3001 (andb_fold (S n) (negation_bv (S n) v) = 3002 andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))). 3003 #n elim n 3004 [ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl 3005 | 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq 3006 lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn 3007 >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind 3008 cases hd normalize nodelta 3009 [ 1: >xorb_false >(xorb_comm false ?) >xorb_false 3010 | 2: >xorb_false >(xorb_comm true ?) >xorb_true ] 3011 >ith_increment_carry 3012 cases (andb_fold (S n') (negation_bv (S n') tl)) @refl 3013 ] qed. 3014 3015 (* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *) 3016 lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v. 3017 #n elim n 3018 [ 1: #v >(BitVector_O v) @refl 3019 | 2: #n' cases n' 3020 [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq 3021 >(BitVector_O … tl) normalize cases hd @refl 3022 | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq 3023 lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%); 3024 whd in match twocomp_neg_direct; normalize nodelta 3025 whd in match increment_direct; normalize nodelta 3026 >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??) 3027 >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn 3028 generalize in match (addition_n_direct (S n'') 3029 (negation_bv (S n'') 3030 (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false)) 3031 (one_bv (S n'')) false); #tail 3032 >ith_increment_carry >ith_increment_carry 3033 cases hd normalize nodelta 3034 [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false 3035 | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ] 3036 <twocomp_neg_involutive_aux 3037 cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl 3038 ] 3039 ] qed. 3040 3041 lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb. 3042 #n #a #b #va #vb #H destruct (H) @conj @refl qed. 3043 3044 lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed. 3045 3046 (* Injectivity of increment *) 3047 lemma increment_inj : ∀n. ∀a,b : BitVector n. 3048 increment_direct ? a = increment_direct ? b → 3049 a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false). 3050 #n whd in match increment_direct; normalize nodelta elim n 3051 [ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj // 3052 | 2: #n' cases n' 3053 [ 1: #_ #a #b 3054 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a 3055 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b 3056 >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b 3057 normalize #H @conj try // 3058 | 2: #n'' #Hind #a #b 3059 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a 3060 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b 3061 lapply (Hind … tl_a tl_b) -Hind #Hind 3062 >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn 3063 >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false 3064 #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2 3065 lapply (Hind Heq2) * #Heq3 #Heq4 3066 cut (hd_a = hd_b) 3067 [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b) 3068 * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm ? hd_b) #Heq6 >(Heq6 Heq5) 3069 @refl ] 3070 #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ] 3071 >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl 3072 ] qed. 3073 3074 (* Inverse of injecivity of increment, does not lose information (cf increment_inj) *) 3075 lemma increment_inj_inv : ∀n. ∀a,b : BitVector n. 3076 a = b → increment_direct ? a = increment_direct ? b. // qed. 3077 3078 lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed. 3079 3080 lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n). 3081 ith_carry (S n) a (one_bv (S n)) false 3082 = ith_carry (S n) a (zero (S n)) true. 3083 #n elim n 3084 [ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl 3085 | 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq 3086 lapply (Hind tl_a) #Hind 3087 >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl 3088 ] qed. 3089 3090 lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false. 3091 #n elim n // 3092 #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn 3093 >ith_carry_Sn >(Hind tl) cases hd @refl. 3094 qed. 3095 3096 lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n. 3097 addition_n_direct ? v (zero ?) false = v. 3098 #n elim n 3099 [ 1: #v >(BitVector_O … v) normalize @refl 3100 | 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq 3101 lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn 3102 >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux 3103 >xorb_false @refl 3104 ] qed. 3105 3106 lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true. 3107 #n elim n 3108 [ 1: #a >(BitVector_O … a) normalize @refl 3109 | 2: #n' cases n' 3110 [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl 3111 | 2: #n'' #Hind #a 3112 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq 3113 lapply (Hind tl_a) -Hind #Hind 3114 >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn 3115 >addition_n_direct_Sn >ith_bit_Sn 3116 >xorb_false >Hind @bitvector_cons_eq 3117 >increment_to_carry_aux @refl 3118 ] 3119 ] qed. 3120 3121 lemma increment_to_carry : ∀n. ∀a,b : BitVector n. 3122 addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true. 3123 #n #a #b >increment_to_carry_zero <associative_addition_n_direct 3124 >neutral_addition_n_direct @refl 3125 qed. 3126 3127 (* Prove -(a + b) = -a + -b *) 3128 lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n. 3129 twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false. 3130 whd in match twocomp_neg_direct; normalize nodelta 3131 lapply increment_inj_inv 3132 whd in match increment_direct; normalize nodelta 3133 #H #n #a #b 3134 <associative_addition_n_direct @H 3135 >associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n)) 3136 >increment_to_carry 3137 -H lapply b lapply a -b -a 3138 cases n 3139 [ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl 3140 | 2: #n' #a #b 3141 cut (negation_bv ? (addition_n_direct ? a b false) 3142 = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧ 3143 notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true)) 3144 [ -n lapply b lapply a elim n' 3145 [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a) 3146 elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b) 3147 cases hd_a cases hd_b normalize @conj @refl 3148 | 2: #n #Hind #a #b 3149 elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa 3150 elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb 3151 lapply (Hind tl_a tl_b) * #H1 #H2 3152 @conj 3153 [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn 3154 >carry_notb >H2 @refl 3155 | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn 3156 >negation_bv_Sn >negation_bv_Sn 3157 >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq 3158 >xorb_lneg >xorb_rneg >notb_notb 3159 <xorb_rneg >H2 @refl 3160 ] 3161 ] ] 3162 * #H1 #H2 @H1 3163 ] qed. 3164 3165 lemma addition_n_direct_neg : ∀n. ∀a. 3166 (addition_n_direct n a (negation_bv n a) false) = replicate ?? true 3167 ∧ (ith_carry n a (negation_bv n a) false = false). 3168 #n elim n 3169 [ 1: #a >(BitVector_O … a) @conj @refl 3170 | 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq 3171 lapply (Hind … tl) -Hind * #HA #HB 3172 @conj 3173 [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl 3174 | 1: >negation_bv_Sn >addition_n_direct_Sn 3175 >ith_bit_Sn >HB >xorb_false >HA 3176 @bitvector_cons_eq elim hd @refl 3177 ] 3178 ] qed. 3179 3180 (* -a + a = 0 *) 3181 lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?). 3182 whd in match twocomp_neg_direct; 3183 whd in match increment_direct; 3184 normalize nodelta 3185 #n #a <associative_addition_n_direct 3186 elim (addition_n_direct_neg … a) #H #_ >H 3187 -H -a 3188 cases n try // 3189 #n' 3190 cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n'))) 3191 ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true)) 3192 [ elim n' 3193 [ 1: @conj @refl 3194 | 2: #n' * #HA #HB @conj 3195 [ 1: >replicate_Sn >one_bv_Sn >addition_n_direct_Sn 3196 >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl 3197 | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ] 3198 ] 3199 ] * #H1 #H2 @H1 3200 qed. 3201 3202 (* Lift back the previous result to standard operations. *) 3203 lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v. 3204 #n #v whd in match twocomp_neg_direct; normalize nodelta 3205 whd in match increment_direct; normalize nodelta 3206 whd in match two_complement_negation; normalize nodelta 3207 >increment_to_addition_n <addition_n_direct_ok 3208 whd in match addition_n; normalize nodelta 3209 elim (add_with_carries ????) #a #b @refl 3210 qed. 3211 3212 lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n. 3213 two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b). 3214 #n #a #b 3215 lapply (twocomp_neg_plus ? a b) 3216 >twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok 3217 <addition_n_direct_ok <addition_n_direct_ok 3218 whd in match addition_n; normalize nodelta 3219 elim (add_with_carries n a b false) #bits #flags normalize nodelta 3220 elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags' 3221 normalize nodelta #H @H 3222 qed. 3223 3224 lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?). 3225 #n #a lapply (bitvector_opp_direct ? a) 3226 >twocomp_neg_direct_ok <addition_n_direct_ok 3227 whd in match (addition_n ???); 3228 elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H 3229 qed. 3230 3231 lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a. 3232 #n #a 3233 lapply (neutral_addition_n_direct n a) 3234 <addition_n_direct_ok 3235 whd in match (addition_n ???); 3236 elim (add_with_carries n a (zero n) false) #bits #flags #H @H 3237 qed. 3238 3239 lemma subtraction_delta : ∀x,y,delta. 3240 subtraction offset_size 3241 (addition_n offset_size x delta) 3242 (addition_n offset_size y delta) = 3243 subtraction offset_size x y. 3244 #x #y #delta whd in match subtraction; normalize nodelta 3245 (* Remove all the equal parts on each side of the equation. *) 3246 <associative_addition_n 3247 >two_complement_negation_plus 3248 <(commutative_addition_n … (two_complement_negation ? delta)) 3249 >(associative_addition_n ? delta) >bitvector_opp_addition_n 3250 >(commutative_addition_n ? (zero ?)) >neutral_addition_n 3251 @refl 3252 qed. 3253 3254 (* Offset subtraction is invariant by translation *) 3255 lemma sub_offset_translation : 3256 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta). 3257 #n #x #y #delta 3258 whd in match (sub_offset ???) in ⊢ (??%%); 3259 elim x #x' elim y #y' elim delta #delta' 3260 whd in match (offset_plus ??); 3261 whd in match (offset_plus ??); 3262 >subtraction_delta @refl 3263 qed. 3264 3265 (* value_eq lifts to addition *) 3266 lemma sub_value_eq : 3267 ∀E,v1,v2,v1',v2',ty1,ty2. 3268 value_eq E v1 v2 → 3269 value_eq E v1' v2' → 3270 ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→ 3271 ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 3272 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 3273 @(value_eq_inversion E … Hvalue_eq1) 3274 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 3275 [ 1: whd in match (sem_sub ????); normalize nodelta 3276 cases (classify_sub ty1 ty2) normalize nodelta 3277 [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ] 3278 #Habsurd destruct (Habsurd) 3279 | 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 3280 cases (classify_sub ty1 ty2) normalize nodelta 3281 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 3282 [ 2,3,5: #Habsurd destruct (Habsurd) ] 3283 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3284 [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ] 3285 [ 1,2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ] 3286 @intsize_eq_elim_elim 3287 [ 1: #_ #Habsurd destruct (Habsurd) 3288 | 2: #Heq destruct (Heq) normalize nodelta 3289 #Heq destruct (Heq) 3290 /3 by ex_intro, conj, vint_eq/ 3291 ] 3292 | 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 3293 cases (classify_sub ty1 ty2) normalize nodelta 3294 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 3295 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 3296 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3297 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 3298 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 3299 #Heq destruct (Heq) 3300 /3 by ex_intro, conj, vfloat_eq/ 3301 | 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 3302 cases (classify_sub ty1 ty2) normalize nodelta 3303 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 3304 [ 1,2,5: #Habsurd destruct (Habsurd) ] 3305 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3306 [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ] 3307 [ 1,2,4,5,6,7,9,10: #Habsurd destruct (Habsurd) ] 3308 [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ 3309 | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 3310 | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ] 3311 | 5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 3312 cases (classify_sub ty1 ty2) normalize nodelta 3313 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 3314 [ 1,2,5: #Habsurd destruct (Habsurd) ] 3315 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3316 [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ] 3317 [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] 3318 #Heq destruct (Heq) 3319 [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl 3320 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 3321 elim p1 in Hembed; #b1 #o1 normalize nodelta 3322 cases (E b1) 3323 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 3324 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) 3325 whd in match (offset_plus ??) in ⊢ (??%%); 3326 whd in match (neg_shift_pointer_n ????) in ⊢ (??%%); 3327 whd in match (neg_shift_offset_n ????) in ⊢ (??%%); 3328 whd in match (subtraction) in ⊢ (??%%); normalize nodelta 3329 generalize in match (short_multiplication ???); #mult 3330 /3 by associative_addition_n, commutative_addition_n, refl/ 3331 ] 3332 | 2: lapply Heq @eq_block_elim 3333 [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) 3334 | 1: #Hpblock1_eq normalize nodelta 3335 elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1 3336 elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq) 3337 whd in ⊢ ((??%?) → (??%?) → ?); 3338 cases (E b1') normalize nodelta 3339 [ 1: #Habsurd destruct (Habsurd) ] 3340 * #dest_block #dest_off normalize nodelta 3341 #Heq_ptr1 #Heq_ptr2 destruct >eq_block_identity normalize nodelta 3342 cases (eqb (sizeof tsg) O) normalize nodelta 3343 [ 1: #Habsurd destruct (Habsurd) 3344 | 2: >(sub_offset_translation 32 off1 off1' dest_off) 3345 cases (division_u 31 3346 (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off)) 3347 (repr (sizeof tsg))) 3348 [ 1: normalize nodelta #Habsurd destruct (Habsurd) 3349 | 2: #r1' normalize nodelta #Heq2 destruct (Heq2) 3350 /3 by ex_intro, conj, vint_eq/ ] 3351 ] ] ] 3352 ] qed. 3353 3354 3355 lemma mul_value_eq : 3356 ∀E,v1,v2,v1',v2',ty1,ty2. 3357 value_eq E v1 v2 → 3358 value_eq E v1' v2' → 3359 ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→ 3360 ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 3361 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 3362 @(value_eq_inversion E … Hvalue_eq1) 3363 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 3364 [ 1: whd in match (sem_mul ????); normalize nodelta 3365 cases (classify_aop ty1 ty2) normalize nodelta 3366 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3367 #Habsurd destruct (Habsurd) 3368 | 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 3369 cases (classify_aop ty1 ty2) normalize nodelta 3370 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3371 [ 2,3: #Habsurd destruct (Habsurd) ] 3372 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3373 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 3374 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 3375 @intsize_eq_elim_elim 3376 [ 1: #_ #Habsurd destruct (Habsurd) 3377 | 2: #Heq destruct (Heq) normalize nodelta 3378 #Heq destruct (Heq) 3379 /3 by ex_intro, conj, vint_eq/ 3380 ] 3381 | 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 3382 cases (classify_aop ty1 ty2) normalize nodelta 3383 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3384 [ 1,3: #Habsurd destruct (Habsurd) ] 3385 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3386 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 3387 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 3388 #Heq destruct (Heq) 3389 /3 by ex_intro, conj, vfloat_eq/ 3390 | 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 3391 cases (classify_aop ty1 ty2) normalize nodelta 3392 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3393 #Habsurd destruct (Habsurd) 3394 | 5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 3395 cases (classify_aop ty1 ty2) normalize nodelta 3396 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3397 #Habsurd destruct (Habsurd) 3398 ] qed. 3399 3400 lemma div_value_eq : 3401 ∀E,v1,v2,v1',v2',ty1,ty2. 3402 value_eq E v1 v2 → 3403 value_eq E v1' v2' → 3404 ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→ 3405 ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 3406 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 3407 @(value_eq_inversion E … Hvalue_eq1) 3408 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 3409 [ 1: whd in match (sem_div ????); normalize nodelta 3410 cases (classify_aop ty1 ty2) normalize nodelta 3411 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3412 #Habsurd destruct (Habsurd) 3413 | 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 3414 cases (classify_aop ty1 ty2) normalize nodelta 3415 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3416 [ 2,3: #Habsurd destruct (Habsurd) ] 3417 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3418 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 3419 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 3420 elim sg normalize nodelta 3421 @intsize_eq_elim_elim 3422 [ 1,3: #_ #Habsurd destruct (Habsurd) 3423 | 2,4: #Heq destruct (Heq) normalize nodelta 3424 @(match (division_s (bitsize_of_intsize sz') i i') with 3425 [ None ⇒ ? 3426 | Some bv' ⇒ ? ]) 3427 [ 1: normalize #Habsurd destruct (Habsurd) 3428 | 2: normalize #Heq destruct (Heq) 3429 /3 by ex_intro, conj, vint_eq/ 3430 | 3,4: elim sz' in i' i; #i' #i 3431 normalize in match (pred_size_intsize ?); 3432 generalize in match division_u; #division_u normalize 3433 @(match (division_u ???) with 3434 [ None ⇒ ? 3435 | Some bv ⇒ ?]) normalize nodelta 3436 #H destruct (H) 3437 /3 by ex_intro, conj, vint_eq/ ] 3438 ] 3439 | 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 3440 cases (classify_aop ty1 ty2) normalize nodelta 3441 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3442 [ 1,3: #Habsurd destruct (Habsurd) ] 3443 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3444 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 3445 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 3446 #Heq destruct (Heq) 3447 /3 by ex_intro, conj, vfloat_eq/ 3448 | 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 3449 cases (classify_aop ty1 ty2) normalize nodelta 3450 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3451 #Habsurd destruct (Habsurd) 3452 | 5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 3453 cases (classify_aop ty1 ty2) normalize nodelta 3454 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3455 #Habsurd destruct (Habsurd) 3456 ] qed. 3457 3458 lemma mod_value_eq : 3459 ∀E,v1,v2,v1',v2',ty1,ty2. 3460 value_eq E v1 v2 → 3461 value_eq E v1' v2' → 3462 ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→ 3463 ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 3464 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 3465 @(value_eq_inversion E … Hvalue_eq1) 3466 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 3467 [ 1: whd in match (sem_mod ????); normalize nodelta 3468 cases (classify_aop ty1 ty2) normalize nodelta 3469 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3470 #Habsurd destruct (Habsurd) 3471 | 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 3472 cases (classify_aop ty1 ty2) normalize nodelta 3473 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3474 [ 2,3: #Habsurd destruct (Habsurd) ] 3475 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3476 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 3477 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 3478 elim sg normalize nodelta 3479 @intsize_eq_elim_elim 3480 [ 1,3: #_ #Habsurd destruct (Habsurd) 3481 | 2,4: #Heq destruct (Heq) normalize nodelta 3482 @(match (modulus_s (bitsize_of_intsize sz') i i') with 3483 [ None ⇒ ? 3484 | Some bv' ⇒ ? ]) 3485 [ 1: normalize #Habsurd destruct (Habsurd) 3486 | 2: normalize #Heq destruct (Heq) 3487 /3 by ex_intro, conj, vint_eq/ 3488 | 3,4: elim sz' in i' i; #i' #i 3489 generalize in match modulus_u; #modulus_u normalize 3490 @(match (modulus_u ???) with 3491 [ None ⇒ ? 3492 | Some bv ⇒ ?]) normalize nodelta 3493 #H destruct (H) 3494 /3 by ex_intro, conj, vint_eq/ ] 3495 ] 3496 | 3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 3497 cases (classify_aop ty1 ty2) normalize nodelta 3498 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3499 #Habsurd destruct (Habsurd) 3500 | 4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 3501 cases (classify_aop ty1 ty2) normalize nodelta 3502 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3503 #Habsurd destruct (Habsurd) 3504 | 5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 3505 cases (classify_aop ty1 ty2) normalize nodelta 3506 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3507 #Habsurd destruct (Habsurd) 3508 ] qed. 3509 3510 (* boolean ops *) 3511 lemma and_value_eq : 3512 ∀E,v1,v2,v1',v2'. 3513 value_eq E v1 v2 → 3514 value_eq E v1' v2' → 3515 ∀r1. (sem_and v1 v1'=Some val r1→ 3516 ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2). 3517 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 3518 @(value_eq_inversion E … Hvalue_eq1) 3519 [ 2: #sz #i 3520 @(value_eq_inversion E … Hvalue_eq2) 3521 [ 2: #sz' #i' whd in match (sem_and ??); 3522 @intsize_eq_elim_elim 3523 [ 1: #_ #Habsurd destruct (Habsurd) 3524 | 2: #Heq destruct (Heq) normalize nodelta 3525 #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] 3526 ] ] 3527 normalize in match (sem_and ??); #arg1 destruct 3528 normalize in match (sem_and ??); #arg2 destruct 3529 normalize in match (sem_and ??); #arg3 destruct 3530 normalize in match (sem_and ??); #arg4 destruct 3531 qed. 3532 3533 lemma or_value_eq : 3534 ∀E,v1,v2,v1',v2'. 3535 value_eq E v1 v2 → 3536 value_eq E v1' v2' → 3537 ∀r1. (sem_or v1 v1'=Some val r1→ 3538 ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2). 3539 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 3540 @(value_eq_inversion E … Hvalue_eq1) 3541 [ 2: #sz #i 3542 @(value_eq_inversion E … Hvalue_eq2) 3543 [ 2: #sz' #i' whd in match (sem_or ??); 3544 @intsize_eq_elim_elim 3545 [ 1: #_ #Habsurd destruct (Habsurd) 3546 | 2: #Heq destruct (Heq) normalize nodelta 3547 #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] 3548 ] ] 3549 normalize in match (sem_or ??); #arg1 destruct 3550 normalize in match (sem_or ??); #arg2 destruct 3551 normalize in match (sem_or ??); #arg3 destruct 3552 normalize in match (sem_or ??); #arg4 destruct 3553 qed. 3554 3555 lemma xor_value_eq : 3556 ∀E,v1,v2,v1',v2'. 3557 value_eq E v1 v2 → 3558 value_eq E v1' v2' → 3559 ∀r1. (sem_xor v1 v1'=Some val r1→ 3560 ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2). 3561 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 3562 @(value_eq_inversion E … Hvalue_eq1) 3563 [ 2: #sz #i 3564 @(value_eq_inversion E … Hvalue_eq2) 3565 [ 2: #sz' #i' whd in match (sem_xor ??); 3566 @intsize_eq_elim_elim 3567 [ 1: #_ #Habsurd destruct (Habsurd) 3568 | 2: #Heq destruct (Heq) normalize nodelta 3569 #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] 3570 ] ] 3571 normalize in match (sem_xor ??); #arg1 destruct 3572 normalize in match (sem_xor ??); #arg2 destruct 3573 normalize in match (sem_xor ??); #arg3 destruct 3574 normalize in match (sem_xor ??); #arg4 destruct 3575 qed. 3576 3577 lemma shl_value_eq : 3578 ∀E,v1,v2,v1',v2'. 3579 value_eq E v1 v2 → 3580 value_eq E v1' v2' → 3581 ∀r1. (sem_shl v1 v1'=Some val r1→ 3582 ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2). 3583 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 3584 @(value_eq_inversion E … Hvalue_eq1) 3585 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 3586 [ 2: 3587 @(value_eq_inversion E … Hvalue_eq2) 3588 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 3589 [ 2: whd in match (sem_shl ??); 3590 cases (lt_u ???) normalize nodelta 3591 [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ 3592 | 2: #Habsurd destruct (Habsurd) 3593 ] 3594 | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ] 3595 | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ] 3596 qed. 3597 3598 lemma shr_value_eq : 3599 ∀E,v1,v2,v1',v2',ty,ty'. 3600 value_eq E v1 v2 → 3601 value_eq E v1' v2' → 3602 ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→ 3603 ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2). 3604 #E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1 3605 @(value_eq_inversion E … Hvalue_eq1) 3606 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 3607 whd in match (sem_shr ????); whd in match (sem_shr ????); 3608 [ 1: cases (classify_aop ty ty') normalize nodelta 3609 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3610 #Habsurd destruct (Habsurd) 3611 | 2: cases (classify_aop ty ty') normalize nodelta 3612 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3613 [ 2,3: #Habsurd destruct (Habsurd) ] 3614 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3615 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 3616 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 3617 elim sg normalize nodelta 3618 cases (lt_u ???) normalize nodelta #Heq destruct (Heq) 3619 /3 by ex_intro, conj, refl, vint_eq/ 3620 | 3: cases (classify_aop ty ty') normalize nodelta 3621 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3622 #Habsurd destruct (Habsurd) 3623 | 4: cases (classify_aop ty ty') normalize nodelta 3624 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3625 #Habsurd destruct (Habsurd) 3626 | 5: cases (classify_aop ty ty') normalize nodelta 3627 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 3628 #Habsurd destruct (Habsurd) 3629 ] qed. 3630 3631 lemma monotonic_Zlt_Zsucc: monotonic Z Zlt Zsucc. 3632 whd #x #y #Hlt lapply (Zlt_to_Zle … Hlt) #Hle lapply (Zle_to_Zlt … Hle) 3633 /3 by monotonic_Zle_Zplus_r, Zle_to_Zlt/ qed. 3634 3635 lemma monotonic_Zlt_Zpred: monotonic Z Zlt Zpred. 3636 whd #x #y #Hlt lapply (Zlt_to_Zle … Hlt) #Hle lapply (Zle_to_Zlt … Hle) 3637 /3 by monotonic_Zle_Zpred, Zle_to_Zlt/ qed. 3638 3639 lemma antimonotonic_Zle_Zsucc: ∀x,y. Zsucc x ≤ Zsucc y → x ≤ y. 3640 #x #y #H lapply (monotonic_Zle_Zpred … H) >Zpred_Zsucc >Zpred_Zsucc #H @H 3641 qed. 3642 3643 (* 3644 lemma antimonotonic_Zle_Zpred: ∀x,y. Zpred x ≤ Zpred y → x ≤ y. 3645 #x #y #H lapply (monotonic_Zle_Zsucc … H) >Zsucc_Zpred >Zsucc_Zpred #H @H 3646 qed. *) 3647 3648 lemma antimonotonic_Zlt_Zsucc: ∀x,y. Zsucc x < Zsucc y → x < y. 3649 #x #y #Hlt lapply (Zle_to_Zlt … (antimonotonic_Zle_Zsucc … (Zlt_to_Zle … Hlt))) 3650 >Zpred_Zsucc #H @H 3651 qed. 3652 3653 lemma antimonotonic_Zlt_Zpred: ∀x,y. Zpred x < Zpred y → x < y. 3654 #x #y #Hlt lapply (monotonic_Zlt_Zsucc … Hlt) >Zsucc_Zpred >Zsucc_Zpred #H @H 3655 qed. 3656 3657 lemma not_Zlt_to_Zltb_false : ∀n,m. n ≮ m → Zltb n m = false. 3658 #n #m #Hnlt 3659 @Zltb_elim_Type0 3660 [ 1: elim Hnlt #H0 #H1 @(False_ind … (H0 H1)) 3661 | 2: #_ @refl ] qed. 3662 3663 lemma Zplus_eq_eq : ∀x,y,delta:Z. eqZb x y = eqZb (x + delta) (y + delta). 3664 #x #y #delta 3665 @eqZb_elim 3666 [ 1: #Heq >Heq >eqZb_z_z @refl 3667 | 2: * #Hneq cut (x+delta ≠ y + delta) 3668 [ 1: % #H cut (x = y) [ 1: @(injective_Zplus_l delta) @H ] #H' @Hneq @H' ] 3669 #H @sym_eq @eqZb_false @H ] qed. 3670 3671 lemma Zltb_Zsucc : ∀x,y. Zltb x y = Zltb (Zsucc x) (Zsucc y). 3672 #x #y 3673 @(Zltb_elim_Type0 … x y) 3674 [ 1: #Hlt @sym_eq lapply (monotonic_Zlt_Zsucc … Hlt) #Hlt' @(Zlt_to_Zltb_true … Hlt') 3675 | 2: #Hnlt @sym_eq @not_Zlt_to_Zltb_false % #Hltsucc 3676 lapply (antimonotonic_Zlt_Zsucc … Hltsucc) #Hlt 3677 @(absurd … Hlt Hnlt) 3678 ] qed. 3679 3680 lemma Zltb_Zpred : ∀x,y. Zltb x y = Zltb (Zpred x) (Zpred y). 3681 #x #y 3682 @(Zltb_elim_Type0 … x y) 3683 [ 1: #Hlt @sym_eq 3684 lapply (monotonic_Zlt_Zpred … Hlt) #Hlt' @(Zlt_to_Zltb_true … Hlt') 3685 | 2: #Hnlt @sym_eq @not_Zlt_to_Zltb_false % #Hltsucc 3686 lapply (antimonotonic_Zlt_Zpred … Hltsucc) #Hlt 3687 @(absurd … Hlt Hnlt) 3688 ] qed. 3689 3690 lemma Zplus_pos_lt_lt : ∀x,y.∀delta. Zltb x y = Zltb (x + (pos delta)) (y + (pos delta)). 3691 #x #y #delta @(pos_elim … delta) 3692 [ 1: >(sym_Zplus x) >(sym_Zplus y) <Zsucc_Zplus_pos_O <Zsucc_Zplus_pos_O 3693 >Zltb_Zsucc @refl 3694 | 2: #n #Hind >Hind >Zltb_Zsucc 3695 >(sym_Zplus x) >(sym_Zplus y) 3696 <Zplus_Zsucc <Zplus_Zsucc 3697 >(sym_Zplus ? x) >(sym_Zplus ? y) 3698 normalize in match (Zsucc ?); @refl 3699 ] qed. 3700 3701 lemma Zplus_neg_lt_lt : ∀x,y.∀delta. Zltb x y = Zltb (x + (neg delta)) (y + (neg delta)). 3702 #x #y #delta @(pos_elim … delta) 3703 [ 1: >(sym_Zplus x) >(sym_Zplus y) <Zpred_Zplus_neg_O <Zpred_Zplus_neg_O 3704 >Zltb_Zpred @refl 3705 | 2: #n #Hind >Hind >Zltb_Zpred 3706 >(sym_Zplus x) >(sym_Zplus y) 3707 <Zplus_Zpred <Zplus_Zpred 3708 >(sym_Zplus ? x) >(sym_Zplus ? y) 3709 normalize in match (Zpred ?); @refl 3710 ] qed. 3711 3712 (* I would not be surprised for a simpler proof that mine to exist. *) 3713 lemma Zplus_lt_lt : ∀x,y,delta:Z. Zltb x y = Zltb (x + delta) (y + delta). 3714 #x #y #delta 3715 cases delta 3716 [ 1: >Zplus_z_OZ >Zplus_z_OZ @refl 3717 | 2: #p @Zplus_pos_lt_lt 3718 | 3: #p @Zplus_neg_lt_lt 3719 ] qed. 3720 3721 (* offset equality is invariant by translation *) 3722 lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y. 3723 #delta #x #y normalize 3724 elim delta #zdelta @sym_eq @cthulhu qed. (* @Zplus_eq_eq qed.*) 3725 3726 lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y. 3727 @cthulhu qed. 3728 (* #delta #x #y normalize 3729 elim delta #zdelta @sym_eq <Zplus_eq_eq qed. *) 3730 3731 lemma cmp_offset_translation : ∀op,delta,x,y. 3732 cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta). @cthulhu qed. 3733 (* 3734 * #delta #x #y normalize 3735 elim delta #zdelta 3736 [ 1: @Zplus_eq_eq 3737 | 2: <Zplus_eq_eq @refl 3738 | 3: @Zplus_lt_lt 3739 | 4: <Zplus_lt_lt @refl 3740 | 5: @Zplus_lt_lt 3741 | 6: <Zplus_lt_lt @refl 3742 qed. *) 3743 3744 lemma cmp_value_eq : 3745 ∀E,v1,v2,v1',v2',ty,ty',m1,m2. 3746 value_eq E v1 v2 → 3747 value_eq E v1' v2' → 3748 memory_inj E m1 m2 → 3749 ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→ 3750 ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2). 3751 #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1 3752 elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj 3753 whd in match (sem_cmp ??????) in ⊢ ((??%?) → %); 3754 cases (classify_cmp ty ty') normalize nodelta 3755 [ 1: #tsz #tsg 3756 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 3757 [ 1: #v #Habsurd destruct (Habsurd) 3758 | 3: #f #Habsurd destruct (Habsurd) 3759 | 4: #Habsurd destruct (Habsurd) 3760 | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 3761 #sz #i 3762 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3763 [ 1: #v #Habsurd destruct (Habsurd) 3764 | 3: #f #Habsurd destruct (Habsurd) 3765 | 4: #Habsurd destruct (Habsurd) 3766 | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 3767 #sz' #i' cases tsg normalize nodelta 3768 @intsize_eq_elim_elim 3769 [ 1,3: #Hneq #Habsurd destruct (Habsurd) 3770 | 2,4: #Heq destruct (Heq) normalize nodelta 3771 #Heq destruct (Heq) 3772 [ 1: cases (cmp_int ????) whd in match (of_bool ?); 3773 | 2: cases (cmpu_int ????) whd in match (of_bool ?); ] 3774 /3 by ex_intro, conj, vint_eq/ ] 3775 | 3: #fsz 3776 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 3777 [ 1: #v #Habsurd destruct (Habsurd) 3778 | 2: #sz #i #Habsurd destruct (Habsurd) 3779 | 4: #Habsurd destruct (Habsurd) 3780 | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 3781 #f 3782 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3783 [ 1: #v #Habsurd destruct (Habsurd) 3784 | 2: #sz #i #Habsurd destruct (Habsurd) 3785 | 4: #Habsurd destruct (Habsurd) 3786 | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 3787 #f' 3788 #Heq destruct (Heq) cases (Fcmp op f f') 3789 /3 by ex_intro, conj, vint_eq/ 3790 | 4: #ty1 #ty2 #Habsurd destruct (Habsurd) 3791 | 2: #optn #typ 3792 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 3793 [ 1: #v #Habsurd destruct (Habsurd) 3794 | 2: #sz #i #Habsurd destruct (Habsurd) 3795 | 3: #f #Habsurd destruct (Habsurd) 3796 | 5: #p1 #p2 #Hembed ] 3797 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 3798 [ 1,6: #v #Habsurd destruct (Habsurd) 3799 | 2,7: #sz #i #Habsurd destruct (Habsurd) 3800 | 3,8: #f #Habsurd destruct (Habsurd) 3801 | 5,10: #p1' #p2' #Hembed' ] 3802 [ 2,3: cases op whd in match (sem_cmp_mismatch ?); 3803 #Heq destruct (Heq) 3804 [ 1,3: %{Vfalse} @conj try @refl @vint_eq 3805 | 2,4: %{Vtrue} @conj try @refl @vint_eq ] 3806 | 4: cases op whd in match (sem_cmp_match ?); 3807 #Heq destruct (Heq) 3808 [ 2,4: %{Vfalse} @conj try @refl @vint_eq 3809 | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ] 3810 lapply (mi_valid_pointers … Hinj p1' p2') 3811 lapply (mi_valid_pointers … Hinj p1 p2) 3812 cases (valid_pointer (mk_mem ???) p1') 3813 [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 3814 cases (valid_pointer (mk_mem ???) p1) 3815 [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 3816 #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2 3817 >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2 3818 elim p1 in Hembed; #b1 #o1 3819 elim p1' in Hembed'; #b1' #o1' 3820 whd in match (pointer_translation ??); 3821 whd in match (pointer_translation ??); 3822 @(eq_block_elim … b1 b1') 3823 [ 1: #Heq destruct (Heq) 3824 cases (E b1') normalize nodelta 3825 [ 1: #Habsurd destruct (Habsurd) ] 3826 * #eb1' #eo1' normalize nodelta 3827 #Heq1 #Heq2 #Heq3 destruct 3828 >eq_block_identity normalize nodelta 3829 <cmp_offset_translation 3830 cases (cmp_offset ???) normalize nodelta 3831 /3 by ex_intro, conj, vint_eq/ 3832 | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1') 3833 cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 3834 * #eb1 #eo1 3835 cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ] 3836 * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct 3837 lapply (H ???? Hneq (refl ??) (refl ??)) 3838 #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta 3839 elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq) 3840 /3 by ex_intro, conj, vint_eq/ 3841 ] 3842 ] qed. 3843 3844 (* Commutation result for binary operators. *) 3845 lemma binary_operation_value_eq : 3846 ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2. 3847 value_eq E v1 v2 → 3848 value_eq E v1' v2' → 3849 memory_inj E m1 m2 → 3850 ∀r1. 3851 sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 → 3852 ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2. 3853 #E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1 3854 cases op 3855 whd in match (sem_binary_operation ??????); 3856 whd in match (sem_binary_operation ??????); 3857 [ 1: @add_value_eq try assumption 3858 | 2: @sub_value_eq try assumption 3859 | 3: @mul_value_eq try assumption 3860 | 4: @div_value_eq try assumption 3861 | 5: @mod_value_eq try assumption 3862 | 6: @and_value_eq try assumption 3863 | 7: @or_value_eq try assumption 3864 | 8: @xor_value_eq try assumption 3865 | 9: @shl_value_eq try assumption 3866 | 10: @shr_value_eq try assumption 3867 | *: @cmp_value_eq try assumption 3868 ] qed. 3869 3870 lemma cast_value_eq : 3871 ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 → 3872 ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res → 3873 ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'. 3874 #E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res 3875 @(value_eq_inversion … Hvalue_eq) 3876 [ 1: #v normalize #Habsurd destruct (Habsurd) 3877 | 2: #vsz #vi whd in match (exec_cast ????); 3878 cases ty 3879 [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ] 3880 normalize nodelta 3881 [ 1,3,7,8,9: #Habsurd destruct (Habsurd) 3882 | 2: @intsize_eq_elim_elim 3883 [ 1: #Hneq #Habsurd destruct (Habsurd) 3884 | 2: #Heq destruct (Heq) normalize nodelta 3885 cases cast_ty 3886 [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn 3887 | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ] 3888 normalize nodelta 3889 [ 1,7,8,9: #Habsurd destruct (Habsurd) 3890 | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/ 3891 | 3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/ 3892 | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta 3893 @eq_bv_elim 3894 [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta 3895 whd in match (m_bind ?????); 3896 #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 3897 | 2,4,6: #Hneq >eq_intsize_identity normalize nodelta 3898 whd in match (m_bind ?????); 3899 #Habsurd destruct (Habsurd) ] ] 3900 ] 3901 | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta 3902 @eq_bv_elim 3903 [ 1,3,5: #Heq destruct (Heq) normalize nodelta 3904 whd in match (m_bind ?????); #Habsurd destruct (Habsurd) 3905 | 2,4,6: #Hneq normalize nodelta 3906 whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ] 3907 ] 3908 | 3: #f whd in match (exec_cast ????); 3909 cases ty 3910 [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n 3911 | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ] 3912 normalize nodelta 3913 [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] 3914 cases cast_ty 3915 [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn 3916 | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ] 3917 normalize nodelta 3918 [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] 3919 #Heq destruct (Heq) 3920 [ 1: /3 by ex_intro, conj, vint_eq/ 3921 | 2: /3 by ex_intro, conj, vfloat_eq/ ] 3922 | 4: whd in match (exec_cast ????); 3923 cases ty 3924 [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n 3925 | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ] 3926 normalize 3927 [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ] 3928 cases cast_ty normalize nodelta 3929 [ 1,10,19: #Habsurd destruct (Habsurd) 3930 | 2,11,20: #csz #csg #Habsurd destruct (Habsurd) 3931 | 3,12,21: #cfl #Habsurd destruct (Habsurd) 3932 | 4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 3933 | 5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 3934 | 6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 3935 | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd) 3936 | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd) 3937 | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ] 3938 | 5: #p1 #p2 #Hembed whd in match (exec_cast ????); 3939 cases ty 3940 [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n 3941 | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ] 3942 normalize 3943 [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ] 3944 cases cast_ty normalize nodelta 3945 [ 1,10,19: #Habsurd destruct (Habsurd) 3946 | 2,11,20: #csz #csg #Habsurd destruct (Habsurd) 3947 | 3,12,21: #cfl #Habsurd destruct (Habsurd) 3948 | 4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption 3949 | 5,14,23: #carrayty #cn #Heq destruct (Heq) 3950 %{(Vptr p2)} @conj try @refl @vptr_eq assumption 3951 | 6,15,24: #ctl #cretty #Heq destruct (Heq) 3952 %{(Vptr p2)} @conj try @refl @vptr_eq assumption 3953 | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd) 3954 | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd) 3955 | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ] 3956 qed. 3957 3958 lemma bool_of_val_value_eq : 3959 ∀E,v1,v2. value_eq E v1 v2 → 3960 ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b. 3961 #E #v1 #v2 #Hvalue_eq #ty #b 3962 @(value_eq_inversion … Hvalue_eq) // 3963 [ 1: #v #H normalize in H; destruct (H) 3964 | 2: #p1 #p2 #Hembed #H @H ] qed. 3965 1833 3966 1834 (* Simulation relation on expressions *) 3967 1835 lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext. 3968 ∀E:embedding. 3969 ∀Hext:memory_ext E m1 m2. 3970 switch_removal_globals E ? fundef_switch_removal ge ge' → 3971 disjoint_extension en1 m1 en2 m2 ext E Hext → 1836 ∀Hext:sr_memext m1 m2. 1837 switch_removal_globals ? fundef_switch_removal ge ge' → 1838 disjoint_extension en1 m1 en2 m2 ext Hext → 3972 1839 ext_fresh_for_genv ext ge → 3973 (∀e. exec_expr_sim E(exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧3974 (∀ed, ty. exec_lvalue_sim E(exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).3975 #ge #ge' #en1 #m1 #en2 #m2 #ext # E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv1840 (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ 1841 (∀ed, ty. exec_lvalue_sim (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)). 1842 #ge #ge' #en1 #m1 #en2 #m2 #ext #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv 3976 1843 @expr_lvalue_ind_combined 3977 1844 [ 1: #csz #cty #i #a1 … … 3994 1861 cases (exec_lvalue' ge en1 m1 ? ty) in Hind; 3995 1862 [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 3996 | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *3997 elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr23998 #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq1863 | 1,3,5: normalize nodelta #b1 #H lapply (H b1 (refl ??)) #Heq >Heq 1864 normalize nodelta 1865 elim b1 * #bl1 #o1 #tr1 (* elim b2 * #bl2 #o2 #tr2 *) 3999 1866 whd in match (load_value_of_type' ???); 4000 1867 whd in match (load_value_of_type' ???); 4001 lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)1868 lapply (load_value_of_type_inj m1 m2 bl1 o1 ty Hext) 4002 1869 cases (load_value_of_type ty m1 bl1 o1) 4003 1870 [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 4004 | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq) 4005 elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload 4006 normalize /4 by ex_intro, conj/ 1871 | 2,4,6: #v #H normalize in ⊢ (% → ?); #Heq destruct (Heq) 1872 >(H v (refl ??)) @refl 4007 1873 ] ] ] 4008 | 4: #v #ty whd * * #b 1 #o1 #tr11874 | 4: #v #ty whd * * #b #o #tr 4009 1875 whd in match (exec_lvalue' ?????); 4010 1876 whd in match (exec_lvalue' ?????); … … 4018 1884 | 2: normalize nodelta 4019 1885 cases (lookup ?? en1 v) normalize nodelta 4020 [ 1: #Hlookup2 >Hlookup2 normalize nodelta 4021 lapply (rg_find_symbol … Hrelated v) 4022 cases (find_symbol ???) normalize 4023 [ 1: #_ #Habsurd destruct (Habsurd) 4024 | 2: #block cases (lookup ?? (symbols clight_fundef ge') v) 4025 [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse) 4026 | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq) 4027 %{〈block',mk_offset (zero offset_size),[]〉} @conj try @refl 4028 normalize /2/ 4029 ] ] 4030 | 2: #block 1886 [ 1: #Hlookup2 <Hlookup2 normalize nodelta 1887 lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym 1888 #H @H 1889 | 2: #block 4031 1890 cases (lookup ?? en2 v) normalize nodelta 4032 [ 1: #Hfalse @(False_ind … Hfalse) 4033 | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq) 4034 %{〈b, zero_offset, E0〉} @conj try @refl 4035 normalize /2/ 4036 ] ] ] 1891 [ 1: #Habsurd destruct (Habsurd) 1892 | 2: #b #Heq destruct (Heq) #H @H ] 1893 ] 1894 ] 4037 1895 | 5: #e #ty whd in ⊢ (% → %); 4038 1896 whd in match (exec_lvalue' ?????); 4039 1897 whd in match (exec_lvalue' ?????); 4040 1898 cases (exec_expr ge en1 m1 e) 4041 [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta 4042 * elim v1 normalize nodelta 4043 [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd) 4044 | 2: #sz #i #_ #_ #a1 #Habsurd destruct (Habsurd) 4045 | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd) 4046 | 4: #_ #_ #a1 #Habsurd destruct (Habsurd) 4047 | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq 4048 >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2 4049 #Hvalue_eq normalize 4050 cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 4051 * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace) 4052 * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize 4053 %{〈b2,mk_offset (addition_n ? (offv o1') (offv o2')),tr1''〉} @conj try @refl 4054 normalize @conj // ] 1899 [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' #H @H 4055 1900 | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] 4056 1901 | 6: #ty #e #ty' … … 4058 1903 cases ty 4059 1904 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 4060 * #b 1 #o1 * #b2 #o2normalize nodelta try /2 by I/4061 #tr #H @conj try @refl try assumption1905 * #b #o normalize nodelta try /2 by I/ 1906 #tr @conj try @refl 4062 1907 | 7: #ty #op #e 4063 #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq 4064 lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq) 4065 cases (sem_unary_operation op v1 (typeof e)) normalize nodelta 4066 [ 1: #_ @I 4067 | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq 4068 normalize /2/ ] 1908 #Hsim @(exec_expr_expr_elim … Hsim) #v #trace 1909 cases (sem_unary_operation op v (typeof e)) normalize nodelta 1910 try @I 1911 #v @conj @refl 4069 1912 | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 4070 @(exec_expr_expr_elim … Hsim1) #v 1 #v2 #trace #Hvalue_eq1913 @(exec_expr_expr_elim … Hsim1) #v #trace 4071 1914 cases (exec_expr ge en1 m1 e2) in Hsim2; 4072 1915 [ 2: #error // ] 4073 * # val #trace normalize in ⊢ (% → ?); #Hsim24074 elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec24075 whd in match (m_bind ?????); whd in match (m_bind ?????);4076 lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext))4077 cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1)4078 [ 1: #_ // ]4079 #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq #Hvalue_eq_opval4080 >Hopval_eq normalize destruct /2 by conj/1916 * #pval #ptrace normalize in ⊢ (% → ?); #Hsim2 1917 whd in match (m_bind ?????); 1918 >(Hsim2 ? (refl ??)) 1919 whd in match (m_bind ?????); 1920 lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 Hext) 1921 cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1) 1922 [ 1: #_ // ] #val #H >(H val (refl ??)) 1923 normalize destruct @conj @refl 4081 1924 | 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) 4082 #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty) 4083 cases (exec_cast m1 v1 (typeof e) cast_ty) 4084 [ 2: #error #_ normalize @I 4085 | 1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????); 4086 * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta 4087 @conj // ] 1925 #v #tr 1926 cut (exec_cast m1 v (typeof e) cast_ty = exec_cast m2 v (typeof e) cast_ty) 1927 [ @refl ] 1928 #Heq >Heq 1929 cases (exec_cast m2 v (typeof e) cast_ty) 1930 [ 2: // 1931 | 1: #v normalize @conj @refl ] 4088 1932 | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 4089 @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq 4090 lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1)) 1933 @(exec_expr_expr_elim … Hsim1) #v #tr 4091 1934 cases (exec_bool_of_val ? (typeof e1)) #b 4092 [ 2: #_ normalize @I ] 4093 #H lapply (H ? (refl ??)) #Hexec >Hexec normalize 1935 [ 2: normalize @I ] 4094 1936 cases b normalize nodelta 1937 whd in match (m_bind ?????); 1938 whd in match (m_bind ?????); 1939 normalize nodelta 4095 1940 [ 1: (* true branch *) 4096 1941 cases (exec_expr ge en1 m1 e2) in Hsim2; 4097 1942 [ 2: #error normalize #_ @I 4098 | 1: * #e2v #e2tr normalize #H elim (H ? (refl ??)) 4099 * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize 4100 destruct @conj try // ] 1943 | 1: * #e2v #e2tr normalize #H >(H ? (refl ??)) normalize nodelta 1944 @conj @refl ] 4101 1945 | 2: (* false branch *) 4102 1946 cases (exec_expr ge en1 m1 e3) in Hsim3; 4103 1947 [ 2: #error normalize #_ @I 4104 | 1: * #e3v #e3tr normalize #H elim (H ? (refl ??)) 4105 * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize 4106 destruct @conj // ] ] 1948 | 1: * #e3v #e3tr normalize #H >(H ? (refl ??)) normalize nodelta 1949 @conj @refl ] ] 4107 1950 | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 4108 @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq 4109 lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1)) 4110 cases (exec_bool_of_val v1 (typeof e1)) 4111 [ 2,4: #error #_ normalize @I ] 4112 #b cases b #H lapply (H ? (refl ??)) #Heq >Heq 1951 @(exec_expr_expr_elim … Hsim1) #v #tr 1952 cases (exec_bool_of_val v (typeof e1)) 1953 [ 2,4: #error normalize @I ] 1954 * 4113 1955 whd in match (m_bind ?????); 4114 1956 whd in match (m_bind ?????); 4115 [ 2,3: normalize @conj try @refl try @vint_eq]1957 [ 2,3: normalize @conj try @refl ] 4116 1958 cases (exec_expr ge en1 m1 e2) in Hsim2; 4117 1959 [ 2,4: #error #_ normalize @I ] 4118 * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??)) 4119 * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta 4120 lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2)) 1960 * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta >(H2 ? (refl ??)) 1961 normalize nodelta 4121 1962 cases (exec_bool_of_val v2 (typeof e2)) 4122 [ 2,4: #error #_ normalize @I ] 4123 #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta 4124 destruct @conj try @conj // 4125 cases b2 whd in match (of_bool ?); @vint_eq 1963 [ 2,4: #error normalize @I ] 1964 * normalize @conj @refl 4126 1965 | 13: #ty #ty' cases ty 4127 1966 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n 4128 1967 | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 4129 whd in match (exec_expr ????); whd 4130 * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉} 4131 @conj try @refl @conj // 4132 | 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta 1968 whd in match (exec_expr ????); whd #a #H @H 1969 | 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr 4133 1970 whd in match (exec_lvalue' ?????); 4134 1971 whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty); … … 4144 1981 cases (exec_lvalue' ge en1 m1 ed ?) in Hsim; 4145 1982 [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 4146 * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??)) 4147 * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq 4148 whd in match (exec_lvalue ????); >Hexec normalize nodelta 4149 [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj // 4150 normalize @conj // ] 4151 cases (field_offset i fl') 4152 [ 2: #error normalize #Habsurd destruct (Habsurd) ] 4153 #offset whd in match (m_bind ?????); #Heq destruct (Heq) 4154 whd in match (m_bind ?????); 4155 %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj 4156 destruct // normalize nodelta @conj try @refl @vptr_eq 4157 -H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq 4158 whd in match (pointer_translation ??); 4159 whd in match (pointer_translation ??); 4160 cases (E b) 4161 [ 1: normalize nodelta #Habsurd destruct (Habsurd) ] 4162 * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq) 4163 cut (offset_plus (mk_offset (addition_n offset_size 4164 (offv o1) 4165 (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 offset)))) o' 4166 = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset))) 4167 [ whd in match (shift_offset ???) in ⊢ (???%); 4168 whd in match (offset_plus ??) in ⊢ (??%%); 4169 /3 by associative_addition_n, commutative_addition_n, refl/ ] 4170 #Heq >Heq @refl 1983 * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H 1984 whd in match (exec_lvalue ge' en2 m2 (Expr ed ?)); 1985 >(H ? (refl ??)) normalize nodelta #H @H 4171 1986 | 15: #ty #l #e #Hsim 4172 @(exec_expr_expr_elim … Hsim) #v 1 #v2 #trace #Hvalue_eqnormalize nodelta @conj //1987 @(exec_expr_expr_elim … Hsim) #v #tr normalize nodelta @conj // 4173 1988 | 16: * 4174 1989 [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 … … 4176 1991 #ty normalize in ⊢ (% → ?); 4177 1992 [ 3,4,13: @False_ind 4178 | *: #_ normalize #a1 #Habsurd destruct (Habsurd)]1993 | *: #_ normalize #a1 #Habsurd @Habsurd ] 4179 1994 ] qed. 1995 4180 1996 4181 1997 … … 4420 2236 ] qed. 4421 2237 4422 (* 4423 lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr. 4424 exec_expr ge e m cond = OK ? 〈v,tr〉 → 4425 (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) → 4426 exec_expr ge' e m cond = OK ? 〈v,tr〉. 4427 #ge #ge' #e #m #cond #v #tr #H * 4428 [ 1: #Hsim >(Hsim ? H) // 4429 | 2: * #error >H #Habsurd destruct (Habsurd) ] 4430 qed. *) 4431 4432 (* 4433 lemma switch_simulation : 4434 ∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u. 4435 switch_cont_sim k k' → 4436 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) → 4437 fresh_for_statement (Sswitch cond switchcases) u → 4438 ∃tr'. 4439 (eventually ge' 4440 (λs2':state 4441 .switch_state_sim 4442 (State f 4443 (seq_of_labeled_statement (select_switch condsz condval switchcases)) 4444 (Kswitch k) e m) s2') 4445 (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m) 4446 tr'). 4447 #ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh 4448 whd in match (sw_rem (Sswitch cond switchcases) u); 4449 whd in match (switch_removal (Sswitch cond switchcases) u); 4450 cases switchcases in Hfresh; 4451 [ 1: #default_statement #Hfresh_for_default 4452 whd in match (switch_removal_branches ??); 4453 whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?); 4454 elim (switch_removal_eq default_statement u) 4455 #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq 4456 normalize nodelta 4457 cut (u' = (\snd (switch_removal default_statement u))) 4458 [ 1: >Hdefault_statement_eq // ] #Heq_u' 4459 cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u') 4460 [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u' 4461 lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u') 4462 #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉)) 4463 -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *) 4464 normalize nodelta 4465 whd in match (simplify_switch (Expr ??) ?? uv2); 4466 lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2) 4467 #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉)) 4468 -Hfreshness #Heq_uv3 4469 normalize nodelta whd in match (add_starting_lbl_list ????); 4470 lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3) 4471 #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉)) 4472 -Hfreshness #Heq_uv4 4473 normalize nodelta 4474 @(eventually_later ge' ?? E0) 4475 whd in match (exec_step ??); 4476 %{(State (function_switch_removal f) 4477 (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond) 4478 (Kseq 4479 (Ssequence 4480 (Slabel default_lab (convert_break_to_goto default_statement' exit_label)) 4481 (Slabel exit_label Sskip)) 4482 k') e m)} @conj try // 4483 @(eventually_later ge' ?? E0) 4484 whd in match (exec_step ??); 4485 4486 @chthulhu | @chthulhu 4487 qed. *) 4488 4489 4490 4491 (* Main theorem. To be ported and completed to memory injections. TODO *) 4492 (* 4493 theorem switch_removal_correction : ∀ge, ge'. 4494 related_globals ? fundef_switch_removal ge ge' → 4495 ∀s1, s1', tr, s2. 4496 switch_state_sim s1 s1' → 2238 lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed. 2239 2240 lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c. 2241 #A #B #a #b * #a' #b' #H destruct @refl 2242 qed. 2243 2244 lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c. 2245 #A #B #a #b * #a' #b' #H destruct @refl 2246 qed. 2247 2248 (* Main theorem. To be ported and completed to memory injections. TODO *) 2249 theorem switch_removal_correction : 2250 ∀ge,ge',s1, s1', tr, s2. 2251 switch_removal_globals ? fundef_switch_removal ge ge' → 2252 switch_state_sim ge s1 s1' → 4497 2253 exec_step ge s1 = Value … 〈tr,s2〉 → 4498 eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.4499 #ge #ge' # Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step2254 eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr. 2255 #ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state 4500 2256 inversion Hsim_state 4501 2257 [ 1: (* regular state *) 4502 #u #f #s #k #k' #m #m' #result #en #en' #f' #vars 4503 #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_ 4504 4505 lapply (sim_related_globals ge ge' e m Hrelated) * 4506 #Hexpr_related #Hlvalue_related 4507 >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?); 4508 cases s in Hu_fresh Heq_env; 4509 4510 4511 theorem switch_removal_correction : ∀ge, ge'. 4512 related_globals ? fundef_switch_removal ge ge' → 4513 ∀s1, s1', tr, s2. 4514 switch_state_sim s1 s1' → 4515 exec_step ge s1 = Value … 〈tr,s2〉 → 4516 eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr. 4517 #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step 4518 inversion Hsim_state 4519 [ 1: (* regular state *) 4520 #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_ 4521 lapply (sim_related_globals ge ge' e m Hrelated) * 4522 #Hexpr_related #Hlvalue_related 4523 >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?); 4524 cases s in Hu_fresh Heq_env; 4525 (* Perform the intros for the statements*) 2258 #sss_statement #sss_result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars 2259 #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_mem_hyp 2260 #sss_env_hyp #sss_result_hyp #sss_k_hyp #Hext_fresh_for_ge 2261 elim (sim_related_globals … ge ge' 2262 sss_env sss_m sss_env_ext sss_m_ext sss_new_vars 2263 sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge) 2264 #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_ 2265 cases sss_statement in sss_lu_fresh sss_result_hyp; 2266 (* Perform the intros for the statements *) 4526 2267 [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body 4527 2268 | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body 4528 2269 | 14: #lab | 15: #cost #body ] 4529 # Hu_fresh #Heq_env2270 #sss_lu_fresh #sss_result_hyp 4530 2271 [ 1: (* Skip *) 4531 whd in match (sw_rem ??); 4532 inversion Hsim_cont normalize nodelta 4533 [ 1: #Hk #Hk' #_ #Hexec_step 4534 @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify 4535 cases (fn_return f) in Hexec_step; 4536 [ 1,10: | 2,11: #sz #sg | 3,12: #fsz | 4,13: #rg #ptr_ty | 5,14: #rg #array_ty #array_sz | 6,15: #domain #codomain 4537 | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ] 2272 whd in match (switch_removal ???) in sss_result_hyp; 2273 <(some_inj ??? sss_result_hyp) 2274 inversion sss_k_hyp normalize nodelta 2275 [ 1: #fvs #Hfvs_eq #Hk #Hk' #_ #Hexec_step 2276 @(eventually_now ????) whd in match (exec_step ??); 2277 >(prod_eq_lproj ????? sss_func_hyp) 2278 >fn_return_simplify 2279 whd in match (exec_step ??) in Hexec_step; 2280 cases (fn_return sss_func) in Hexec_step; 2281 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 2282 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 4538 2283 normalize nodelta 4539 [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H) 4540 %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @conj try // 2284 whd in ⊢ ((??%?) → ?); 2285 [ 1: #H destruct (H) %{(Returnstate Vundef Kstop (free_list sss_m_ext (blocks_of_env sss_env_ext)))} 2286 @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)} try // 2287 %{(Returnstate Vundef Kstop (free1_list sss_m_ext (blocks_of_env sss_env_ext)))} @conj try // 4541 2288 normalize in Heq_env; destruct (Heq_env) 4542 2289 %3 // … … 4958 2705 4959 2706 *) 2707 2708 (* 2709 lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr. 2710 exec_expr ge e m cond = OK ? 〈v,tr〉 → 2711 (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) → 2712 exec_expr ge' e m cond = OK ? 〈v,tr〉. 2713 #ge #ge' #e #m #cond #v #tr #H * 2714 [ 1: #Hsim >(Hsim ? H) // 2715 | 2: * #error >H #Habsurd destruct (Habsurd) ] 2716 qed. *) 2717 2718 (* 2719 lemma switch_simulation : 2720 ∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u. 2721 switch_cont_sim k k' → 2722 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) → 2723 fresh_for_statement (Sswitch cond switchcases) u → 2724 ∃tr'. 2725 (eventually ge' 2726 (λs2':state 2727 .switch_state_sim 2728 (State f 2729 (seq_of_labeled_statement (select_switch condsz condval switchcases)) 2730 (Kswitch k) e m) s2') 2731 (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m) 2732 tr'). 2733 #ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh 2734 whd in match (sw_rem (Sswitch cond switchcases) u); 2735 whd in match (switch_removal (Sswitch cond switchcases) u); 2736 cases switchcases in Hfresh; 2737 [ 1: #default_statement #Hfresh_for_default 2738 whd in match (switch_removal_branches ??); 2739 whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?); 2740 elim (switch_removal_eq default_statement u) 2741 #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq 2742 normalize nodelta 2743 cut (u' = (\snd (switch_removal default_statement u))) 2744 [ 1: >Hdefault_statement_eq // ] #Heq_u' 2745 cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u') 2746 [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u' 2747 lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u') 2748 #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉)) 2749 -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *) 2750 normalize nodelta 2751 whd in match (simplify_switch (Expr ??) ?? uv2); 2752 lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2) 2753 #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉)) 2754 -Hfreshness #Heq_uv3 2755 normalize nodelta whd in match (add_starting_lbl_list ????); 2756 lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3) 2757 #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉)) 2758 -Hfreshness #Heq_uv4 2759 normalize nodelta 2760 @(eventually_later ge' ?? E0) 2761 whd in match (exec_step ??); 2762 %{(State (function_switch_removal f) 2763 (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond) 2764 (Kseq 2765 (Ssequence 2766 (Slabel default_lab (convert_break_to_goto default_statement' exit_label)) 2767 (Slabel exit_label Sskip)) 2768 k') e m)} @conj try // 2769 @(eventually_later ge' ?? E0) 2770 whd in match (exec_step ??); 2771 2772 @chthulhu | @chthulhu 2773 qed. *) 2774 2775 2776 4960 2777
Note: See TracChangeset
for help on using the changeset viewer.