Changeset 2387 for src/Clight/switchRemoval.ma
 Timestamp:
 Oct 3, 2012, 1:27:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2353 r2387 1 1 include "Clight/Csyntax.ma". 2 2 include "Clight/fresh.ma". 3 include "basics/lists/list.ma".4 include "basics/lists/listb.ma".5 3 include "common/Identifiers.ma". 6 4 include "utilities/extralib.ma". … … 9 7 include "Clight/frontend_misc.ma". 10 8 include "Clight/memoryInjections.ma". 9 include "basics/lists/list.ma". 10 include "basics/lists/listb.ma". 11 11 12 12 13 (*  … … 901 902 ]. 902 903 903 let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝ 904 match l with 905 [ nil ⇒ None ? 906  cons hd tl ⇒ 907 let 〈id, ty〉 ≝ hd in 908 match identifier_eq SymbolTag i id with 909 [ inl Hid_eq ⇒ Some ? ty 910  inr Hid_neq ⇒ assoc_env i tl 911 ] 912 ]. 904 (*  *) 905 (* "Observational" memory equivalence. Memories use closures to represent contents, 906 so we have to use that short of asserting functional extensionality to reason 907 on reordering of operations on memories, among others. For our 908 limited purposes, we do not need (at this time of writing, i.e. 22 sept. 2012) 909 to push the observation in the content_map. *) 910 (*  *) 911 definition memory_eq ≝ λm1,m2. 912 nextblock m1 = nextblock m2 ∧ 913 ∀b. blocks m1 b = blocks m2 b. 914 915 (* memory_eq is an equivalence relation. *) 916 lemma reflexive_memory_eq : reflexive ? memory_eq. 917 whd * #contents #nextblock #Hpos normalize @conj try // 918 qed. 919 920 lemma symmetric_memory_eq : symmetric ? memory_eq. 921 whd * #contents #nextblock #Hpos * #contents' #nextblock' #Hpos' 922 normalize * #H1 #H2 @conj >H1 try // 923 qed. 924 925 lemma transitive_memory_eq : transitive ? memory_eq. 926 whd 927 * #contents #nextblock #Hpos 928 * #contents1 #nextblock1 #Hpos1 929 * #contents2 #nextblock2 #Hpos2 930 normalize * #H1 #H2 * #H3 #H4 @conj // 931 qed. 913 932 914 933 (*  *) … … 916 935 properties at the backend level. *) 917 936 (*  *) 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 normalize923 >eqZb_reflexive normalize @conj #H destruct (H)924 try @refl925  2: #Hneq cases r1 cases r2 normalize926 >(eqZb_false … Hneq) normalize @conj927 #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??)))928 ] qed. *)929 937 930 938 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the backend values are equal. *) … … 935 943 beloadv m2 ptr = Some ? bev. 936 944 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 945 definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. 945 946 … … 948 949 Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧ 949 950 high_bound m (pblock p) = Z_of_unsigned_bitvector … (offv (poff p)). 950 951 952 (* a valid_pointer is either /inside/ the bounds of the target block xor /one off/ the end. *) 951 953 lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p. 952 954 #m #p @conj … … 985 987 ] qed. 986 988 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); 989 (* A writeable_block is a block that is: 990 . valid 991 . nonempty (i.e. it has been allocated a nonempty size) 992 *) 993 record nonempty_block (m : mem) (b : block) : Prop ≝ 994 { 995 wb_valid : valid_block m b; 996 wb_nonempty : low (blocks m b) < high (blocks m b) 997 }. 998 999 (* Type stating that m2 is an extension of m1, parameterised by a list of blocks where we can write freely *) 1000 record sr_memext (m1 : mem) (m2 : mem) (writeable : list block) : Prop ≝ 1001 { (* Nonempty blocks are preserved as they are. This entails [load_sim]. *) 1002 me_nonempty : ∀b. nonempty_block m1 b → nonempty_block m2 b ∧ blocks m1 b = blocks m2 b; 1003 (* These blocks are valid in [m2] *) 1004 me_writeable_valid : ∀b. meml ? b writeable → nonempty_block m2 b; 1005 (* blocks in [m1] than can be validly pointed to cannot be in [me_writeable]. *) 1006 me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable); 1007 (* This field does not entail [me_not_writeable] and is necessary to prove valid 1008 pointer conservation after a [free]. *) 1009 me_not_writeable_ptr : ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable); 1010 1011 (* Extension blocks contain nothing in [m1] *) 1012 (* me_not_mapped : ∀b. meml … b me_writeable → blocks m1 b = empty_block OZ OZ; *) 1008 1013 (* Valid pointers are still valid in m2. One could think that this is superfluous as 1009 1014 being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer … … 1018 1023 valid_pointer m2 p = true 1019 1024 }. 1025 1026 (* If we have a memory extension, we can simulate loads *) 1027 lemma sr_memext_load_sim : ∀m1,m2,writeable. sr_memext m1 m2 writeable → load_sim m1 m2. 1028 #m1 #m2 #writeable #Hext #ptr #bev whd in match (beloadv ??) in ⊢ (% → %); 1029 #H cut (nonempty_block m1 (pblock ptr) ∧ 1030 Zle (low (blocks m1 (pblock ptr))) 1031 (Z_of_unsigned_bitvector 16 (offv (poff ptr))) ∧ 1032 Zlt (Z_of_unsigned_bitvector 16 (offv (poff ptr))) 1033 (high (blocks m1 (pblock ptr))) ∧ 1034 bev = (contents (blocks m1 (pblock ptr)) (Z_of_unsigned_bitvector 16 (offv (poff ptr))))) 1035 [ @conj try @conj try @conj try % 1036 [ 1: @Zltb_true_to_Zlt ] 1037 cases (Zltb (block_id (pblock ptr)) (nextblock m1)) in H; normalize nodelta 1038 [ 1: // 1039  2,4,6,8,10: #Habsurd destruct ] 1040 generalize in match (Z_of_unsigned_bitvector offset_size (offv (poff ptr))); #z 1041 lapply (Zleb_true_to_Zle (low (blocks m1 (pblock ptr))) z) 1042 lapply (Zltb_true_to_Zlt z (high (blocks m1 (pblock ptr)))) 1043 cases (Zleb (low (blocks m1 (pblock ptr))) z) 1044 cases (Zltb z (high (blocks m1 (pblock ptr)))) #H1 #H2 1045 [ 2,3,4,6,7,8,10,11,12,14,15,16: normalize #Habsurd destruct ] normalize #Heq 1046 lapply (H1 (refl ??)) lapply (H2 (refl ??)) 1047 #Hle #Hlt destruct try assumption try @refl 1048 @(Zle_to_Zlt_to_Zlt … Hle Hlt) ] 1049 * * * #Hnonempty #Hlow #Hhigh #Hres lapply (me_nonempty … Hext … Hnonempty) * 1050 * #Hvalid #Hlt #Hblocks_eq 1051 >(Zlt_to_Zltb_true … Hvalid) normalize <Hblocks_eq 1052 >(Zle_to_Zleb_true … Hlow) >(Zlt_to_Zltb_true … Hhigh) normalize 1053 >Hres @refl 1054 qed. 1055 1056 (*  *) 1057 (* Some lemmas on environments and their contents *) 1058 1059 1060 (* Definition of environment inclusion and equivalence *) 1061 (* Environment "inclusion". *) 1062 definition environment_sim ≝ λenv1,env2. 1063 ∀id, res. lookup SymbolTag block env1 id = Some ? res → 1064 lookup SymbolTag block env2 id = Some ? res. 1065 1066 lemma environment_sim_invert_aux : ∀en1,en2. 1067 (∀id,res. lookup_opt block id en1 = Some ? res → lookup_opt ? id en2 = Some ? res) → 1068 ∀id. lookup_opt ? id en2 = None ? → lookup_opt ? id en1 = None ?. 1069 #en1 elim en1 try // 1070 #opt1 #left1 #right1 #Hindl1 #Hindr1 #en2 #Hsim 1071 normalize #id elim id normalize nodelta 1072 [ 1: #Hlookup cases opt1 in Hsim; try // #res #Hsim lapply (Hsim one res (refl ??)) 1073 #Hlookup2 >Hlookup2 in Hlookup; #H @H 1074  2: #id' cases en2 in Hsim; 1075 [ 1: normalize #Hsim #_ #_ lapply (Hsim (p1 id')) normalize nodelta 1076 cases (lookup_opt block id' right1) try // 1077 #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct 1078  2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup' 1079 @(Hindr1 right2) try // #id0 #res0 1080 lapply (Hsim (p1 id0) res0) normalize #Hsol #H @Hsol @H ] 1081  3: #id' cases en2 in Hsim; 1082 [ 1: normalize #Hsim #_ #_ lapply (Hsim (p0 id')) normalize nodelta 1083 cases (lookup_opt block id' left1) try // 1084 #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct 1085  2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup' 1086 @(Hindl1 left2) try // #id0 #res0 1087 lapply (Hsim (p0 id0) res0) normalize #Hsol #H @Hsol @H ] 1088 ] qed. 1089 1090 lemma environment_sim_invert : 1091 ∀en1,en2. environment_sim en1 en2 → 1092 ∀id. lookup SymbolTag block en2 id = None ? → 1093 lookup SymbolTag block en1 id = None ?. 1094 * #en1 * #en2 #Hsim * #id @environment_sim_invert_aux 1095 #id' #res #Hlookup normalize in Hsim; 1096 lapply (Hsim (an_identifier … id') res) normalize #Hsol @Hsol @Hlookup 1097 qed. 1098 1099 (* Environment equivalence. *) 1100 definition environment_eq ≝ λenv1,env2. environment_sim env1 env2 ∧ environment_sim env2 env1. 1101 1102 lemma symmetric_environment_eq : ∀env1,env2. environment_eq env1 env2 → environment_eq env2 env1. 1103 #env1 #env2 * #Hsim1 #Hsim2 % // qed. 1104 1105 lemma reflexive_environment_eq : ∀env. environment_eq env env. 1106 #env % // qed. 1107 1108 (* An environment [e2] is a disjoint extension of [e1] iff (the new bindings are 1109 fresh and [e2] is equivalent to adding extension blocks to [e1]). *) 1110 definition disjoint_extension ≝ 1111 λ(e1, e2 : env). 1112 λ(new_vars : list (ident × type)). 1113 (∀id. mem_assoc_env id new_vars = true → lookup ?? e1 id = None ?) ∧ (* extension not in e1 *) 1114 (∀id. mem_assoc_env id new_vars = true → ∃res.lookup ?? e2 id = Some ? res) ∧ (* all of the extension is in e2 *) 1115 (∀id. mem_assoc_env id new_vars = false → lookup ?? e1 id = lookup ?? e2 id). (* only [new_vars] extends e2 *) 1020 1116 1021 (* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension 1022 of the environment [e1] s.t. the new binders are in [new], and such that those 1023 new binders are "writeable" in the memory extension [Hext] *) 1024 definition disjoint_extension ≝ 1025 λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem). 1026 λ(new : list (ident × type)). λ(Hext: sr_memext m1 m2). 1027 ∀id. match mem_assoc_env id new with 1028 [ true ⇒ 1029 ∃b. lookup ?? e2 id = Some ? b 1030 ∧ meml ? b (me_writeable … Hext) 1031 ∧ lookup ?? e1 id = None ? 1032  false ⇒ lookup ?? e1 id = lookup ?? e2 id 1033 ]. 1034 1117 lemma disjoint_extension_to_inclusion : 1118 ∀e1,e2,vars. disjoint_extension e1 e2 vars → 1119 environment_sim e1 e2. 1120 #e1 #e2 #vars * * #HA #HB #HC whd #id #res 1121 @(match (mem_assoc_env id vars) return λx.(mem_assoc_env id vars = x) → ? 1122 with 1123 [ true ⇒ λH. ? 1124  false ⇒ λH. ? 1125 ] (refl ? (mem_assoc_env id vars))) 1126 [ 1: #Hlookup lapply (HA ? H) #Habsurd >Habsurd in Hlookup; #H destruct 1127  2: #Hlookup <(HC ? H) assumption ] 1128 qed. 1129 1130 (* Small aux lemma to decompose folds on maps with list accumulators *) 1131 lemma fold_to_concat : ∀A:Type[0].∀m:positive_map A.∀l.∀f. 1132 (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m l) 1133 = (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m []) @ l. 1134 #A #m elim m 1135 [ 1: #l #f normalize @refl 1136  2: #optblock #left #right 1137 #Hind1 #Hind2 #l #f 1138 whd in match (fold ?????) in ⊢ (??%%); 1139 cases optblock 1140 [ 1: normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%); 1141 >associative_append @refl 1142  2: #block normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%); 1143 >Hind1 in ⊢ (???%); >append_cons <associative_append @refl 1144 ] 1145 ] qed. 1146 1147 lemma map_proj_fold : ∀A:Type[0].∀m:positive_map A. ∀f. ∀l. 1148 map ?? (λx.\snd x) (fold ?? (λx,a,el.〈an_identifier SymbolTag x,a〉::el) m l) = 1149 map ?? (λx.\snd x) (fold ?? (λx,a,el.〈an_identifier SymbolTag (f x),a〉::el) m l). 1150 #A #m elim m 1151 [ 1: #f #l normalize @refl 1152  2: #opt #left #right #Hind1 #Hind2 #f #l 1153 normalize cases opt 1154 [ 1: normalize nodelta >fold_to_concat >fold_to_concat in ⊢ (???%); 1155 <map_append <map_append <Hind2 <Hind2 in ⊢ (???%); 1156 <Hind1 <Hind1 in ⊢ (???%); @refl 1157  2: #elt normalize nodelta >fold_to_concat >fold_to_concat in ⊢ (???%); 1158 <map_append <map_append <Hind2 <Hind2 in ⊢ (???%); 1159 <(Hind1 p0) <Hind1 in ⊢ (???%); 1160 >(fold_to_concat ?? (〈an_identifier SymbolTag one,elt〉::l)) 1161 >(fold_to_concat ?? (〈an_identifier SymbolTag (f one),elt〉::l)) 1162 <map_append <map_append normalize in match (map ??? (cons ???)); @refl 1163 ] 1164 ] qed. 1165 1166 lemma lookup_entails_block : ∀en:env.∀id,res. 1167 lookup SymbolTag block en id = Some ? res → 1168 meml ? res (blocks_of_env en). 1169 * #map * #id #res 1170 whd in match (blocks_of_env ?); 1171 whd in match (elements ???); 1172 whd in match (lookup ????); 1173 normalize nodelta 1174 lapply res lapply id id res 1175 elim map 1176 [ 1: #id #res normalize #Habsurd destruct (Habsurd) 1177  2: #optblock #left #right #Hind1 #Hind2 #id #res #Hind3 1178 whd in match (fold ?????); 1179 cases optblock in Hind3; 1180 [ 1: normalize nodelta 1181 whd in match (lookup_opt ???); 1182 cases id normalize nodelta 1183 [ 1: #Habsurd destruct (Habsurd) 1184  2: #p #Hright lapply (Hind2 … Hright) 1185 normalize >fold_to_concat in ⊢ (? → %); 1186 <map_append #Haux @mem_append_backwards %1 1187 <map_proj_fold @Haux 1188  3: #p #Hleft lapply (Hind1 … Hleft) 1189 normalize >fold_to_concat in ⊢ (? → %); 1190 <map_append #Haux @mem_append_backwards %2 1191 <map_proj_fold @Haux ] 1192  2: #blo whd in match (lookup_opt ???); 1193 normalize >fold_to_concat <map_append 1194 cases id normalize nodelta 1195 [ 1: #Heq destruct (Heq) 1196 @mem_append_backwards %2 >fold_to_concat 1197 <map_append @mem_append_backwards %2 normalize %1 @refl 1198  2: #p #Hlookup lapply (Hind2 … Hlookup) #H 1199 @mem_append_backwards %1 1200 <map_proj_fold @H 1201  3: #p #Hlookup lapply (Hind1 … Hlookup) #H 1202 @mem_append_backwards %2 >fold_to_concat 1203 <map_append @mem_append_backwards %1 1204 <map_proj_fold @H 1205 ] 1206 ] 1207 ] qed. 1208 1209 1210 lemma blocks_of_env_cons : 1211 ∀en,id,hd. mem ? hd (blocks_of_env (add SymbolTag block en id hd)). 1212 #en #id #hd @(lookup_entails_block … id) 1213 cases id #p elim p try /2/ qed. 1214 1215 lemma in_blocks_exists_id : ∀env.∀bl. meml … bl (blocks_of_env env) → ∃id. lookup SymbolTag block env id = Some ? bl. 1216 #env elim env #m elim m 1217 [ 1: #bl normalize @False_ind 1218  2: #opt #left #right #Hind1 #Hind2 #bl normalize 1219 >fold_to_concat <map_append #H 1220 elim (mem_append_forward ???? H) 1221 [ 1: <map_proj_fold H #H lapply (Hind2 … H) 1222 * * #id #Hlookup normalize in Hlookup; 1223 %{(an_identifier SymbolTag (p1 id))} normalize nodelta @Hlookup 1224  2: <map_proj_fold cases opt 1225 [ 1: normalize H #H lapply (Hind1 … H) 1226 * * #id #Hlookup normalize in Hlookup; 1227 %{(an_identifier SymbolTag (p0 id))} normalize nodelta @Hlookup 1228  2: #bl' normalize >fold_to_concat <map_append normalize 1229 #H' elim (mem_append_forward ???? H') 1230 [ 1: H #H lapply (Hind1 … H) * * #id normalize #Hlookup 1231 %{(an_identifier ? (p0 id))} normalize nodelta @Hlookup 1232  2: normalize * [ 2: @False_ind ] 1233 #Heq destruct (Heq) 1234 %{(an_identifier SymbolTag one)} @refl 1235 ] 1236 ] 1237 ] 1238 ] qed. 1239 1240 let rec inclusion_elim 1241 (A : Type[0]) 1242 (m1, m2 : positive_map A) 1243 (P : positive_map A → positive_map A → Prop) 1244 (H1 : ∀m2. P (pm_leaf A) m2) 1245 (H2 : ∀opt1,left1,right1. P left1 (pm_leaf A) → P right1 (pm_leaf A) → P (pm_node A opt1 left1 right1) (pm_leaf A)) 1246 (H3 : ∀opt1,left1,right1,opt2,left2,right2. P left1 left2 → P right1 right2 → P (pm_node A opt1 left1 right1) (pm_node A opt2 left2 right2)) 1247 on m1 : P m1 m2 ≝ 1248 match m1 with 1249 [ pm_leaf ⇒ 1250 H1 m2 1251  pm_node opt1 left1 right1 ⇒ 1252 match m2 with 1253 [ pm_leaf ⇒ 1254 H2 opt1 left1 right1 (inclusion_elim A left1 (pm_leaf A) P H1 H2 H3) (inclusion_elim A right1 (pm_leaf A) P H1 H2 H3) 1255  pm_node opt2 left2 right2 ⇒ 1256 H3 opt1 left1 right1 opt2 left2 right2 (inclusion_elim A left1 left2 P H1 H2 H3) (inclusion_elim A right1 right2 P H1 H2 H3) 1257 ] 1258 ]. 1259 1260 (* Environment inclusion entails block inclusion. *) 1261 lemma environment_sim_blocks_inclusion : 1262 ∀env1, env2. environment_sim env1 env2 → lset_inclusion ? (blocks_of_env env1) (blocks_of_env env2). 1263 * #m1 * #m2 @(inclusion_elim … m1 m2) m1 m2 1264 [ 1: #m2 normalize #_ @I 1265  2: #opt1 #left1 #right1 #Hind1 #Hind2 #Hsim 1266 normalize >fold_to_concat in ⊢ (???%); <map_append @All_append 1267 [ 1: <map_proj_fold @Hind2 #id #res elim id #id' #Hlookup @(Hsim (an_identifier ? (p1 id')) res Hlookup) 1268  2: cases opt1 in Hsim; 1269 [ 1: normalize nodelta #Hsim 1270 <map_proj_fold @Hind1 #id #res elim id #id' #Hlookup @(Hsim (an_identifier ? (p0 id')) res Hlookup) 1271  2: #bl #Hsim lapply (Hsim (an_identifier ? one) bl ?) normalize try @refl 1272 #Habsurd destruct (Habsurd) 1273 ] 1274 ] 1275  3: #opt1 #left1 #right1 #opt2 #left2 #right2 #Hind1 #Hind2 #Hsim 1276 normalize >fold_to_concat >fold_to_concat in ⊢ (???%); 1277 <map_append <map_append in ⊢ (???%); @All_append 1278 [ 1: cases opt2; normalize nodelta 1279 [ 1: <map_proj_fold <map_proj_fold in ⊢ (???%); <(map_proj_fold ?? p0) 1280 cut (environment_sim (an_id_map SymbolTag block right1) (an_id_map SymbolTag block right2)) 1281 [ 1: * #id' #res #Hlookup 1282 lapply (Hsim (an_identifier ? (p1 id')) res) normalize #H @H @Hlookup ] 1283 #Hsim' lapply (Hind2 Hsim') @All_mp 1284 #a #Hmem @mem_append_backwards %1 @Hmem 1285  2: #bl <map_proj_fold <map_proj_fold in ⊢ (???%); <(map_proj_fold ?? p0) 1286 cut (environment_sim (an_id_map SymbolTag block right1) (an_id_map SymbolTag block right2)) 1287 [ 1: * #id' #res #Hlookup 1288 lapply (Hsim (an_identifier ? (p1 id')) res) normalize #H @H @Hlookup ] 1289 #Hsim' lapply (Hind2 Hsim') @All_mp 1290 #a #Hmem @mem_append_backwards %1 @Hmem ] 1291  2: cut (environment_sim (an_id_map SymbolTag block left1) (an_id_map SymbolTag block left2)) 1292 [ 1: * #id' #res #Hlookup 1293 lapply (Hsim (an_identifier ? (p0 id')) res) normalize #H @H @Hlookup ] #Hsim' 1294 lapply (Hind1 … Hsim') 1295 <map_proj_fold <map_proj_fold in ⊢ (? → (???%)); <(map_proj_fold ?? p0) 1296 cases opt1 in Hsim; normalize nodelta 1297 [ 1: #Hsim @All_mp #a #Hmem @mem_append_backwards %2 1298 cases opt2 normalize nodelta 1299 [ 1: @Hmem 1300  2: #bl >fold_to_concat <map_append @mem_append_backwards %1 @Hmem ] 1301  2: #bl #Hsim #Hmem >fold_to_concat in ⊢ (???%); <map_append @All_append 1302 [ 2: normalize @conj try @I 1303 cases opt2 in Hsim; 1304 [ 1: #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) 1305 normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 1306  2: #bl2 #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) 1307 normalize in ⊢ (% → ?); #Heq >Heq normalize nodelta 1308 @mem_append_backwards %2 >fold_to_concat <map_append 1309 @mem_append_backwards %2 normalize %1 @refl ] 1310  1: cases opt2 in Hsim; 1311 [ 1: #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) 1312 normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 1313  2: #bl2 #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) 1314 normalize in ⊢ (% → ?); #Heq lapply (Hind1 Hsim') 1315 @All_mp #a #Hmem >Heq normalize nodelta 1316 @mem_append_backwards %2 >fold_to_concat <map_append 1317 @mem_append_backwards %1 @Hmem ] ] 1318 ] 1319 ] 1320 ] qed. 1321 1322 1323 (* equivalent environments yield "equal" sets of block (cf. frontend_misc.ma) *) 1324 lemma environment_eq_blocks_eq : ∀env1,env2. 1325 environment_eq env1 env2 → 1326 lset_eq ? (blocks_of_env env1) (blocks_of_env env2). 1327 #env1 #env2 * #Hsim1 #Hsim2 @conj 1328 @environment_sim_blocks_inclusion assumption 1329 qed. 1330 1331 (* [env_codomain env vars] is the image of vars through env seen as a function. *) 1332 definition env_codomain : env → list (ident×type) → lset block ≝ λe,l. 1333 foldi … (λid,block,acc. 1334 if mem_assoc_env … id l then 1335 block :: acc 1336 else 1337 acc 1338 ) e [ ]. 1339 1340 (*  *) 1341 1342 (* Two equivalent memories yield a trivial memory extension. *) 1343 lemma memory_eq_to_mem_ext : ∀m1,m2. memory_eq m1 m2 → sr_memext m1 m2 [ ]. 1344 * #contents1 #nextblock1 #Hpos * #contents2 #nextblock2 #Hpos' normalize * 1345 #Hnextblock #Hcontents_eq destruct % 1346 [ 1: #b #H @conj try % elim H try // 1347  2: #b * 1348  3: #b #_ normalize % // 1349  4: #p #Hvalid % * 1350 (*  4: #b * *) 1351  5: #p normalize >Hcontents_eq #H @H 1352 ] qed. 1353 1354 (* memory extensions form a preorder relation *) 1355 1356 lemma memory_ext_transitive : 1357 ∀m1,m2,m3,writeable1,writeable2. 1358 sr_memext m1 m2 writeable1 → 1359 sr_memext m2 m3 writeable2 → 1360 sr_memext m1 m3 (writeable1 @ writeable2). 1361 #m1 #m2 #m3 #writeable1 #writeable2 #H12 #H23 % 1362 [ 1: #b #Hnonempty1 1363 lapply (me_nonempty … H12 b Hnonempty1) * #Hnonempty2 #Hblocks_eq 1364 lapply (me_nonempty … H23 b Hnonempty2) * #Hnonempty3 #Hblocks_eq' @conj 1365 try assumption >Hblocks_eq >Hblocks_eq' @refl 1366  2: #b #Hmem lapply (mem_append_forward ???? Hmem) * 1367 [ 1: #Hmem12 lapply (me_writeable_valid … H12 b Hmem12) #Hnonempty2 1368 elim (me_nonempty … H23 … Hnonempty2) // 1369  2: #Hmem23 @(me_writeable_valid … H23 b Hmem23) ] 1370  3: #b #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) * 1371 [ 1: #Hmem12 1372 lapply (me_not_writeable … H12 … Hvalid) * #H @H assumption 1373  2: #Hmem23 lapply (me_nonempty … H12 … Hvalid) * #Hvalid2 1374 lapply (me_not_writeable … H23 … Hvalid2) * #H #_ @H assumption 1375 ] 1376  4: #p #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) * 1377 [ 1: #Hmem12 1378 lapply (me_not_writeable_ptr … H12 … Hvalid) * #H @H assumption 1379  2: #Hmem23 1380 lapply (me_valid_pointers … H12 … Hvalid) #Hvalid2 1381 lapply (me_not_writeable_ptr … H23 … Hvalid2) * #H @H assumption 1382 ] 1383  5: #p #Hvalid @(me_valid_pointers … H23) @(me_valid_pointers … H12) @Hvalid 1384 ] qed. 1385 1386 lemma memory_ext_reflexive : 1387 ∀m. sr_memext m m [ ]. 1388 #m % /2/ #b * qed. 1389 1390 (*  *) 1391 (* Lift beloadv simulation to the frontend. *) 1392 1035 1393 (* Lift load_sim to loadn. *) 1036 1394 lemma load_sim_loadn : … … 1079 1437 ] qed. 1080 1438 1081 (* Lemmas relating memory extensions to [free] *) 1439 (*  *) 1440 (* Lemmas relating reading and writing operation to memory properties. *) 1082 1441 1083 1442 (* Successful beloadv implies valid_pointer. The converse is *NOT* true. *) … … 1099 1458 @Zltb_to_Zleb_true 1100 1459 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H; 1101 try // normalize #Habsurd destruct (Habsurd) qed. 1460 try // normalize #Habsurd destruct (Habsurd) 1461 qed. 1462 1463 (*  *) 1464 (* Lemmas relating memory extensions to [free] *) 1102 1465 1103 1466 lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1). … … 1133 1496 #_ % #H destruct (H) elim Heq #H @H @refl 1134 1497 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 #bv21141 whd in match (be_to_fe_value ??);1142 whd in match (be_to_fe_value ??);1143 cases bv1 normalize nodelta1144 [ 1: cases bv2 normalize nodelta1145 [ 1: #H @refl  2:1146 try //1147 [ cases bv2 *)1148 1498 1149 1499 lemma beloadv_free_beloadv : … … 1193 1543 1194 1544 lemma beloadv_free_simulation : 1195 ∀m1,m2, block,ptr,res.1196 ∀mem_hyp : sr_memext m1 m2 .1545 ∀m1,m2,writeable,block,ptr,res. 1546 ∀mem_hyp : sr_memext m1 m2 writeable. 1197 1547 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 1548 * #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 #writeable 1549 * #br #bid * * #pr #pid #poff #res #Hext 1550 (*#Hme_nonempty #Hme_writeable #Hme_nonempty #Hvalid_conserv*) 1201 1551 #Hload 1202 1552 lapply (beloadv_free_beloadv … Hload) #Hload_before_free … … 1204 1554 @beloadv_free_beloadv2 1205 1555 [ 1: @Hblocks_neq ] 1206 @ Hload_simassumption1556 @(sr_memext_load_sim … Hext) assumption 1207 1557 qed. 1208 1558 … … 1271 1621 qed. 1272 1622 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 #Hvalid1623 lemma valid_pointer_free : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true. 1624 #m1 #m2 #writeable #Hext #p #b #Hvalid 1275 1625 lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free 1276 1626 lapply (me_valid_pointers … Hext … Hvalid_before_free) … … 1284 1634 qed. 1285 1635 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 1636 lemma nonempty_block_mismatch : ∀m,b,bl. 1637 nonempty_block (free m bl) b → 1638 nonempty_block m b ∧ b ≠ bl. 1639 #m #b #bl #Hnonempty 1640 @(eq_block_elim … b bl) 1641 [ 1: #Heq >Heq in Hnonempty; * #_ normalize 1642 cases (block_region bl) normalize >eqZb_reflexive normalize * 1643  2: #Hneq @conj try assumption elim Hnonempty #Hvalid #Hlh % 1644 [ 1: lapply Hvalid normalize // 1645  2: lapply Hlh normalize 1646 cases (block_region b) normalize nodelta 1647 cases (block_region bl) normalize nodelta try // 1648 @(eqZb_elim … (block_id b) (block_id bl)) 1649 [ 1,3: * normalize * 1650  2,4: #_ // ] ] ] 1651 qed. 1652 1653 lemma eqb_to_eq_block : ∀a,b : block. a == b = eq_block a b. 1654 #a #b lapply (eqb_true ? a b) @(eq_block_elim … a b) 1655 /2 by neq_block_eq_block_false, true_to_andb_true/ 1656 qed. 1657 1658 (* We can free in both sides of a memory extension if we take care of removing 1659 the freed block from the set of writeable blocks. *) 1660 lemma free_memory_ext : 1661 ∀m1,m2,writeable,bl. 1662 sr_memext m1 m2 writeable → 1663 sr_memext (free m1 bl) (free m2 bl) (lset_remove ? writeable bl). 1664 #m1 #m2 #writeable #bl #Hext % 1665 [ 1: #b #Hnonempty lapply (nonempty_block_mismatch … Hnonempty) 1666 * #Hnonempty' #Hblocks_neq lapply (me_nonempty … Hext … Hnonempty') * 1667 #Hnonempty2 #Hcontents_eq @conj 1668 [ 1: % try @(wb_valid … Hnonempty2) 1669 whd in match (free ??); 1670 whd in match (update_block ?????); 1671 >(neq_block_eq_block_false … Hblocks_neq) normalize 1672 try @(wb_nonempty … Hnonempty2) 1673  2: whd in match (free ??) in ⊢ (??%%); 1674 whd in match (update_block ?????) in ⊢ (??%%); 1675 >(neq_block_eq_block_false … Hblocks_neq) 1676 normalize nodelta assumption ] 1677  2: #b #Hmem 1678 cut (mem block b writeable ∧ b ≠ bl) 1679 [ elim writeable in Hmem; 1680 [ 1: normalize * 1681  2: #hd #tl #Hind whd in match (filter ???); 1682 >eqb_to_eq_block 1683 @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta 1684 [ 1: #Heq #H whd in match (meml ???); elim (Hind H) #H0 #H1 @conj 1685 [ 1: %2 ] assumption 1302 1686  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 1687 [ 1: #H destruct /3 by conj, or_introl, refl/ 1688  2: #H elim (Hind H) #H1 #H2 /3 by conj, or_intror, refl/ ] ] ] 1689 ] * #Hmem2 #Hblocks_neq 1690 lapply (me_writeable_valid … Hext … Hmem2) * #Hvalid #Hnonempty % 1691 try assumption whd in match (free ??); whd in match (update_block ?????); 1692 >(neq_block_eq_block_false … Hblocks_neq) @Hnonempty 1693  3: #p #Hvalid lapply (nonempty_block_mismatch … Hvalid) * #Hnonempty #Hblocks_neq 1694 % #Hmem lapply (me_not_writeable … Hext … Hnonempty) * #H @H 1695 elim writeable in Hmem; 1696 [ 1: * 1697  2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block 1698 @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta 1699 [ 1: #Heq #H normalize %2 @(Hind H) 1700  2: #Hblocks_neq whd in match (meml ???); * 1701 [ 1: #Hneq normalize %1 assumption 1702  2: #Hmem normalize %2 @(Hind Hmem) ] 1703 ] 1704 ] 1705  4: #p #Hvalid 1706 lapply (valid_free_to_valid … Hvalid) #Hvalid' 1707 lapply (me_not_writeable_ptr … Hext … Hvalid') * #HA % #HB @HA 1708 elim writeable in HB; 1709 [ 1: * 1710  2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block 1711 @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta 1712 [ 1: #Heq #H normalize %2 @(Hind H) 1713  2: #Hblocks_neq whd in match (meml ???); * 1714 [ 1: #Hneq normalize %1 assumption 1715  2: #Hmem normalize %2 @(Hind Hmem) ] 1716 ] 1717 ] 1718  5: #p @(valid_pointer_free … writeable) @Hext 1332 1719 ] qed. 1333 1720 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 1721 (* Freeing from an extension block is ok. *) 1722 lemma memext_free_extended_conservation : 1723 ∀m1,m2 : mem. 1724 ∀writeable. 1725 ∀mem_hyp : sr_memext m1 m2 writeable. 1726 ∀b. meml ? b writeable → 1727 sr_memext m1 (free m2 b) (lset_remove … writeable b). 1728 #m1 #m2 #writeable #Hext #b #Hb_writeable % 1729 [ 1: #bl #Hnonempty lapply (me_not_writeable … Hext … Hnonempty) #Hnot_mem 1730 lapply (mem_not_mem_neq … Hb_writeable Hnot_mem) #Hblocks_neq 1731 @conj 1732 [ 2: whd in match (free ??); whd in match (update_block ?????); 1733 >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize 1734 elim (me_nonempty … Hext … Hnonempty) // 1735  1: % elim (me_nonempty … Hext … Hnonempty) * try // 1736 #Hvalid2 #Hlh #Hcontents_eq whd in match (free ??); 1737 whd in match (update_block ?????); 1738 >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize assumption 1739 ] 1740  2: #b' #Hmem (* contradiction in first premise *) 1741 cut (mem block b' writeable ∧ b' ≠ b) 1742 [ elim writeable in Hmem; 1743 [ 1: normalize @False_ind 1744  2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block 1745 @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta 1746 [ 1: #Heq #H whd in match (meml ???); destruct 1747 elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption 1748  2: #Hneq whd in match (meml ???) in ⊢ (% → %); * 1749 [ 1: #H @conj [ 1: %1 @H  2: destruct @Hneq ] 1750  2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] 1751 ] ] ] 1752 * #Hb' #Hneq lapply (me_writeable_valid … Hext … Hb') #Hvalid % 1753 [ 1: @(wb_valid … Hvalid) 1754  2: whd in match (free ??); 1755 whd in match (update_block ?????); 1756 >(neq_block_eq_block_false … Hneq) 1757 @(wb_nonempty … Hvalid) ] 1758  3: #b' #Hnonempty % #Hmem 1759 cut (mem block b' writeable ∧ b' ≠ b) 1760 [ elim writeable in Hmem; 1761 [ 1: normalize @False_ind 1762  2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block 1763 @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta 1764 [ 1: #Heq #H whd in match (meml ???); destruct 1765 elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption 1766  2: #Hneq whd in match (meml ???) in ⊢ (% → %); * 1767 [ 1: #H @conj [ 1: %1 @H  2: destruct @Hneq ] 1768  2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] 1769 ] ] ] * #Hmem' #Hblocks_neq 1770 lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption 1771  4: #p #Hnonempty % #Hmem 1772 cut (mem block (pblock p) writeable ∧ (pblock p) ≠ b) 1773 [ elim writeable in Hmem; 1774 [ 1: normalize @False_ind 1775  2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block 1776 @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta 1777 [ 1: #Heq #H whd in match (meml ???); destruct 1778 elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption 1779  2: #Hneq whd in match (meml ???) in ⊢ (% → %); * 1780 [ 1: #H @conj [ 1: %1 @H  2: destruct @Hneq ] 1781  2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] 1782 ] ] ] * #Hmem' #Hblocks_neq 1783 lapply (me_not_writeable_ptr … Hext … Hnonempty) * #H @H assumption 1784  5: #p #Hvalid lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_mem 1785 lapply (mem_not_mem_neq … Hb_writeable … Hnot_mem) #Hneq 1786 lapply (me_valid_pointers … Hext … Hvalid) #Hvalid' 1787 whd in match (free ??); 1788 whd in match (valid_pointer ??) in ⊢ (??%%); 1789 whd in match (low_bound ??); whd in match (high_bound ??); 1790 whd in match (update_block ?????); 1791 >(not_eq_block_rev … Hneq) normalize 1792 @Hvalid' 1343 1793 ] qed. 1344 1794 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 *) 1795 1796 1797 1798 lemma disjoint_extension_nil_eq_set : 1799 ∀env1,env2. 1800 disjoint_extension env1 env2 [ ] → 1801 lset_eq ? (blocks_of_env env1) (blocks_of_env env2). 1802 #env1 #env whd in ⊢ (% → ?); * * #_ #_ #H normalize in H; 1803 @environment_eq_blocks_eq whd @conj 1804 #id #res >(H id) // 1805 qed. 1806 1807 lemma free_list_equivalent_sets : 1808 ∀m,set1,set2. 1809 lset_eq ? set1 set2 → 1810 memory_eq (free_list m set1) (free_list m set2). 1811 #m #set1 #set2 #Heq whd in match (free_list ??) in ⊢ (?%%); 1812 @(lset_eq_fold block_DeqSet mem memory_eq … Heq) 1813 [ 1: @reflexive_memory_eq 1814  2: @transitive_memory_eq 1815  3: @symmetric_memory_eq 1816  4: #x #acc1 #acc2 1817 whd in match (free ??) in ⊢ (? → (?%%)); 1818 whd in match (memory_eq ??) in ⊢ (% → %); * 1819 #Hnextblock_eq #Hcontents_eq @conj try assumption 1820 #b normalize >Hcontents_eq @refl 1821  5: #x1 #x2 #acc normalize @conj try @refl 1822 * * #id normalize nodelta cases (block_region x1) 1823 cases (block_region x2) normalize nodelta 1824 @(eqZb_elim id (block_id x1)) #Hx1 normalize nodelta 1825 @(eqZb_elim id (block_id x2)) #Hx2 normalize nodelta try @refl 1826  6: * #r #i * #contents #nextblock #Hpos @conj 1827 [ 1: @refl 1828  2: #b normalize cases (block_region b) normalize 1829 cases r normalize cases (eqZb (block_id b) i) 1830 normalize @refl 1831 ] 1832 ] qed. 1833 1834 lemma foldr_identity : ∀A:Type[0]. ∀l:list A. foldr A ? (λx:A.λl0.x::l0) [] l = l. 1835 #A #l elim l // 1836 #hd #tl #Hind whd in match (foldr ?????); >Hind @refl 1837 qed. 1838 1839 (* freeing equivalent sets of blocks on memory extensions yields memory extensions *) 1840 lemma free_equivalent_sets : 1841 ∀m1,m2,writeable,set1,set2. 1842 lset_eq ? set1 set2 → 1843 sr_memext m1 m2 writeable → 1844 sr_memext (free_list m1 set1) (free_list m2 set2) (lset_difference ? writeable set1). 1845 #m1 #m2 #writeable #set1 #set2 #Heq #Hext 1846 lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq)) 1847 #Heq 1848 lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext' 1849 lapply (memory_ext_transitive (free_list m1 set1) (free_list m2 set1) (free_list m2 set2) (filter block_eq (λwb:block_eq.¬wb∈set1) writeable) [ ] ? Hext') 1850 [ 2: >append_nil #H @H ] 1851 elim set1 1852 [ 1: whd in match (free_list ??); whd in match (free_list ??); 1853 normalize >foldr_identity @Hext 1854  2: #hd #tl #Hind >free_list_cons >free_list_cons 1855 lapply (free_memory_ext … hd … Hind) 1856 cut ((lset_remove block_eq (filter block_eq (λwb:block_eq.¬wb∈tl) writeable) hd) = 1857 (filter block_eq (λwb:block_eq.¬wb∈hd::tl) writeable)) 1858 [ whd in match (lset_remove ???); elim writeable // 1859 #hd' #tl' #Hind_cut >filter_cons_unfold >filter_cons_unfold 1860 whd in match (memb ???) in ⊢ (???%); >eqb_to_eq_block 1861 (* elim (eqb_true block_DeqSet hd' hd)*) 1862 @(eq_block_elim … hd' hd) normalize nodelta 1863 [ 1: #Heq 1864 cases (¬hd'∈tl) normalize nodelta 1865 [ 1: whd in match (foldr ?????); >Heq >eqb_to_eq_block >eq_block_b_b normalize in match (notb ?); 1866 normalize nodelta 1867 lapply Hind_cut destruct #H @H 1868  2: lapply Hind_cut destruct #H @H ] 1869  2: #Hneq cases (¬hd'∈tl) normalize nodelta try assumption 1870 whd in match (foldr ?????); >eqb_to_eq_block 1871 >(neq_block_eq_block_false … Hneq) 1872 normalize in match (notb ?); normalize nodelta >Hind_cut @refl 1873 ] 1874 ] 1875 #Heq >Heq #H @H 1876 ] qed. 1877 1878 (* Remove a writeable block. *) 1879 lemma memory_ext_weaken : 1880 ∀m1,m2,hd,writeable. 1881 sr_memext m1 m2 (hd :: writeable) → 1882 sr_memext m1 m2 writeable. 1883 #m1 #m2 #hd #writeable * 1884 #Hnonempty #Hwriteable_valid #Hnot_writeable #Hnot_writeable_ptr #Hvalid_pointers % 1885 try assumption 1886 [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption 1887  2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem 1888  3: #p #Hvalid % #Hmem elim (Hnot_writeable_ptr … Hvalid) #H @H whd %2 @Hmem 1889 ] qed. 1890 1891 (* Perform a "rewrite" using lset_eq on the writeable blocks *) 1892 lemma memory_ext_writeable_eq : 1893 ∀m1,m2,wr1,wr2. 1894 sr_memext m1 m2 wr1 → 1895 lset_eq ? wr1 wr2 → 1896 sr_memext m1 m2 wr2. 1897 #m1 #m2 #wr1 #wr2 #Hext #Hset_eq % 1898 [ 1: @(me_nonempty … Hext) 1899  2: #b #Hmem lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) 1900 @(me_writeable_valid … Hext) 1901  3: #b #Hnonempty % #Hmem 1902 lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem' 1903 lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption 1904  4: #p #Hvalid % #Hmem 1905 lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem' 1906 lapply (me_not_writeable_ptr … Hext … Hvalid) * #H @H assumption 1907  5: @(me_valid_pointers … Hext) ] 1908 qed. 1909 1910 axiom lset_inclusion_difference : 1911 ∀A : DeqSet. 1912 ∀s1,s2 : lset (carr A). 1913 lset_inclusion ? s1 s2 → 1914 ∃s2'. lset_eq ? s2 (s1 @ s2') ∧ 1915 lset_disjoint ? s1 s2' ∧ 1916 lset_eq ? s2' (lset_difference ? s2 s1). 1917 1918 lemma memory_eq_to_memory_ext_pre : 1919 ∀m1,m1',m2,writeable. 1920 memory_eq m1 m1' → 1921 sr_memext m1' m2 writeable → 1922 sr_memext m1 m2 writeable. 1923 #m1 #m1' #m2 #writeable #Heq #Hext 1924 lapply (memory_eq_to_mem_ext … Heq) #Hext' 1925 @(memory_ext_transitive … Hext' Hext) 1926 qed. 1927 1928 lemma memory_eq_to_memory_ext_post : 1929 ∀m1,m2,m2',writeable. 1930 memory_eq m2' m2 → 1931 sr_memext m1 m2' writeable → 1932 sr_memext m1 m2 writeable. 1933 #m1 #m2 #m2' #writeable #Heq #Hext 1934 lapply (memory_eq_to_mem_ext … Heq) #Hext' 1935 lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H 1936 qed. 1937 1938 lemma lset_not_mem_difference : 1939 ∀A : DeqSet. ∀s1,s2,s3. lset_inclusion (carr A) s1 (lset_difference ? s2 s3) → ∀x. mem ? x s1 → ¬(mem ? x s3). 1940 #A #s1 #s2 #s3 #Hincl #x #Hmem 1941 lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3 1942 elim s1 in Hincl Hmem; 1943 [ 1: #_ * 1944  2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall * 1945 [ 2: #Hmem_x_tl @Hind assumption 1946  1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ] 1947 ] qed. 1948 1949 lemma lset_difference_nil : ∀A,s. lset_difference A s [ ] = s. #A #s elim s // 1950 #hd #tl #Hind >lset_difference_unfold normalize in match (memb ???); normalize nodelta >Hind @refl 1951 qed. 1952 1953 lemma lset_mem_inclusion_mem : 1954 ∀A,s1,s2,elt. 1955 mem A elt s1 → lset_inclusion ? s1 s2 → mem ? elt s2. 1956 #A #s1 elim s1 1957 [ 1: #s2 #elt * 1958  2: #hd #tl #Hind #s2 #elt * 1959 [ 1: #Heq destruct * // 1960  2: #Hmem_tl * #Hmem #Hall elim tl in Hall Hmem_tl; 1961 [ 1: #_ * 1962  2: #hd' #tl' #Hind * #Hmem' #Hall * 1963 [ 1: #Heq destruct @Hmem' 1964  2: #Hmem'' @Hind assumption ] ] ] ] 1965 qed. 1966 1967 lemma lset_remove_inclusion : 1968 ∀A : DeqSet. ∀s,elt. 1969 lset_inclusion A (lset_remove ? s elt) s. 1970 #A #s elim s try // qed. 1971 1972 lemma lset_difference_remove_inclusion : 1973 ∀A : DeqSet. ∀s1,s2,elt. 1974 lset_inclusion A 1975 (lset_difference ? (lset_remove ? s1 elt) s2) 1976 (lset_difference ? s1 s2). 1977 #A #s elim s try // qed. 1978 1979 lemma lset_difference_permute : 1980 ∀A : DeqSet. ∀s1,s2,s3. 1981 lset_difference A s1 (s2 @ s3) = 1982 lset_difference A s1 (s3 @ s2). 1983 #A #s1 #s2 elim s2 try // 1984 #hd #tl #Hind #s3 >lset_difference_unfold2 >lset_difference_lset_remove_commute 1985 >Hind elim s3 try // 1986 #hd' #tl' #Hind' >cons_to_append >associative_append 1987 >associative_append >(cons_to_append … hd tl) 1988 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append 1989 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append 1990 <Hind' generalize in match (lset_difference ???); #foo 1991 whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?); 1992 whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%)); 1993 elim foo 1994 [ 1: normalize @refl 1995  2: #hd'' #tl'' #Hind normalize 1996 @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with 1997 [ true ⇒ λH. ? 1998  false ⇒ λH. ? 1999 ] (refl ? (hd''==hd'))) 2000 @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with 2001 [ true ⇒ λH'. ? 2002  false ⇒ λH'. ? 2003 ] (refl ? (hd''==hd))) 2004 normalize nodelta 2005 try @Hind 2006 [ 1: normalize >H normalize nodelta @Hind 2007  2: normalize >H' normalize nodelta @Hind 2008  3: normalize >H >H' normalize nodelta >Hind @refl 2009 ] qed. 2010 2011 lemma mem_not_mem_diff_aux : 2012 ∀s1,s2,s3,hd. 2013 mem ? hd s1 → 2014 ¬(mem ? hd s2) → 2015 mem block hd (lset_difference ? s1 (s2@(filter block_DeqSet (λx:block_DeqSet.¬x==hd) s3))). 2016 #s1 #s2 #s3 #hd #Hmem #Hnotmem lapply Hmem lapply s1 s1 2017 elim s3 2018 [ 1: #s1 >append_nil elim s1 try // 2019 #hd' #tl' #Hind * 2020 [ 1: #Heq >lset_difference_unfold 2021 @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with 2022 [ true ⇒ λH. ? 2023  false ⇒ λH. ? 2024 ] (refl ? (hd'∈s2))) normalize nodelta 2025 [ 1: lapply (memb_to_mem … H) #Hmem elim Hnotmem #H' destruct 2026 @(False_ind … (H' Hmem)) 2027  2: whd %1 assumption ] 2028  2: #Hmem >lset_difference_unfold 2029 @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with 2030 [ true ⇒ λH. ? 2031  false ⇒ λH. ? 2032 ] (refl ? (hd'∈s2))) normalize nodelta 2033 [ 1: @Hind @Hmem 2034  2: %2 @Hind @Hmem ] ] 2035  2: #hd' #tl' #H #s1 #Hmem >filter_cons_unfold >eqb_to_eq_block 2036 @(eq_block_elim … hd' hd) 2037 [ 1: >notb_true normalize nodelta #Heq @H @Hmem 2038  2: #Hneq >notb_false normalize nodelta 2039 >lset_difference_permute >(cons_to_append … hd') 2040 >associative_append >lset_difference_unfold2 >nil_append 2041 >lset_difference_permute @H 2042 elim s1 in Hmem; try // 2043 #hd'' #tl'' #Hind * 2044 [ 1: #Heq destruct whd in match (lset_remove ???); 2045 >eqb_to_eq_block >(neq_block_eq_block_false … (sym_neq … Hneq)) 2046 >notb_false normalize nodelta %1 @refl 2047  2: #Hmem whd in match (lset_remove ???); 2048 cases (¬(hd''==hd')) normalize nodelta 2049 [ 1: %2 @Hind @Hmem 2050  2: @Hind @Hmem ] ] ] 2051 ] qed. 2052 2053 lemma memext_free_extended_environment : 2054 ∀m1,m2,writeable. 2055 sr_memext m1 m2 writeable → 2056 ∀env,env_ext,vars. 2057 disjoint_extension env env_ext vars → 2058 lset_inclusion ? (lset_difference ? (blocks_of_env env_ext) (blocks_of_env env)) writeable → 2059 sr_memext 2060 (free_list m1 (blocks_of_env env)) 2061 (free_list m2 (blocks_of_env env_ext)) 2062 (lset_difference ? writeable (blocks_of_env env_ext)). 2063 #m1 #m2 #writeable #Hext #env #env_ext #vars #Hdisjoint #Hext_in_writeable 2064 (* Disjoint extension induces environment "inclusion", i.e. simulation *) 2065 lapply (disjoint_extension_to_inclusion … Hdisjoint) #Hincl 2066 (* Environment inclusion entails set inclusion on the mapped blocks *) 2067 lapply (environment_sim_blocks_inclusion … Hincl) #Hblocks_incl 2068 (* This set inclusion can be decomposed on a common part and an extended part. *) 2069 lapply (lset_inclusion_difference ??? Hblocks_incl) 2070 * #extended_part * * #Hset_eq #Henv_disjoint_ext #Hextended_eq 2071 lapply (lset_difference_lset_eq … writeable … Hset_eq) #HeqA 2072 cut (lset_inclusion ? extended_part writeable) 2073 [ 1: cases Hextended_eq #HinclA #_ @(transitive_lset_inclusion … HinclA … Hext_in_writeable) ] 2074 Hext_in_writeable #Hext_in_writeable 2075 @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqA)) 2076 lapply (free_list_equivalent_sets m2 ?? Hset_eq) #Hmem_eq 2077 @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq)) 2078 (* Add extended ⊆ (lset_difference block_eq writeable (blocks_of_env env @ tl)) in Hind *) 2079 cut (∀x. mem ? x extended_part → ¬ (mem ? x (blocks_of_env env))) 2080 [ 1: cases Hextended_eq #Hincl_ext #_ @(lset_not_mem_difference … Hincl_ext) ] 2081 lapply (proj2 … Hset_eq) lapply Hext_in_writeable 2082 @(WF_rect ????? (filtered_list_wf block_DeqSet extended_part)) 2083 * 2084 [ 1: #_ #_ #_ #_ #_ >append_nil 2085 @(free_equivalent_sets ???? (blocks_of_env env) (reflexive_lset_eq ??) Hext) 2086  2: #hd #tl #Hwf_step #Hind_wf #Hext_in_writeable #Hset_incl #Hin_ext_not_in_env 2087 cut (lset_eq ? (blocks_of_env env@hd::tl) (hd::(blocks_of_env env@tl))) 2088 [ 1: >cons_to_append >cons_to_append in ⊢ (???%); 2089 @lset_eq_concrete_to_lset_eq // ] 2090 #Hpermute 2091 lapply (free_list_equivalent_sets m2 ?? Hpermute) #Hmem_eq2 2092 @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq2)) 2093 >free_list_cons 2094 lapply (lset_difference_lset_eq … writeable … Hpermute) #HeqB 2095 @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqB)) 2096 >lset_difference_unfold2 2097 lapply (lset_difference_lset_remove_commute ? hd writeable (blocks_of_env env@tl)) 2098 #Heq_commute >Heq_commute 2099 (* lapply (memory_ext_writeable_eq ????? (symmetric_lset_eq … Heq_commute)) *) 2100 lapply (Hind_wf (filter … (λx.¬(x==hd)) tl) ????) 2101 [ 2: @(transitive_lset_inclusion … Hset_incl) 2102 @lset_inclusion_concat_monotonic 2103 @cons_preserves_inclusion 2104 @lset_inclusion_filter_self 2105  3: @(transitive_lset_inclusion … Hext_in_writeable) 2106 @cons_preserves_inclusion 2107 @lset_inclusion_filter_self 2108  4: whd whd in ⊢ (???%); 2109 lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?); 2110 normalize nodelta @refl 2111  1: #x #H @Hin_ext_not_in_env %2 elim tl in H; // 2112 #hd' #tl' #Hind >filter_cons_unfold >eqb_to_eq_block @(eq_block_elim … hd' hd) 2113 >notb_true >notb_false normalize nodelta 2114 [ 1: #Heq >Heq #H %2 @Hind @H 2115  2: #Hneq * 2116 [ 1: #Heq destruct %1 @refl 2117  2: #H %2 @Hind @H ] ] 2118 ] 2119 #Hext_ind 2120 lapply (Hin_ext_not_in_env … hd (or_introl … (refl ??))) 2121 #Hnot_in_env 2122 lapply (memext_free_extended_conservation … Hext_ind hd ?) 2123 [ 1: @mem_not_mem_diff_aux try assumption elim Hext_in_writeable #H #_ @H ] 2124 Hext_ind #Hext_ind 2125 cut (memory_eq (free (free_list m2 (blocks_of_env env@filter block_DeqSet (λx:block_DeqSet.¬x==hd) tl)) hd) 2126 (free (free_list m2 (blocks_of_env env@tl)) hd)) 2127 [ 1: <free_list_cons <free_list_cons 2128 @free_list_equivalent_sets @lset_eq_concrete_to_lset_eq 2129 >cons_to_append >cons_to_append in ⊢ (???%); 2130 @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????)) 2131 @symmetric_lset_eq_concrete 2132 @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????)) 2133 @lset_eq_to_lset_eq_concrete 2134 elim (blocks_of_env env) 2135 [ 1: @symmetric_lset_eq @lset_eq_filter 2136  2: #hd0 #tl0 #Hind >cons_to_append 2137 >associative_append in ⊢ (??%%); 2138 >associative_append in ⊢ (??%%); 2139 @cons_monotonic_eq @Hind ] ] 2140 #Hmem_eq3 @(memory_eq_to_memory_ext_post … Hmem_eq3) 2141 @(memory_ext_writeable_eq … Hext_ind) 2142 <lset_difference_lset_remove_commute <lset_difference_lset_remove_commute 2143 <lset_difference_unfold2 <lset_difference_unfold2 2144 @lset_difference_lset_eq 2145 (* Note: exactly identical to the proof in the cut. *) 2146 @lset_eq_concrete_to_lset_eq 2147 >cons_to_append >cons_to_append in ⊢ (???%); 2148 @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????)) 2149 @symmetric_lset_eq_concrete 2150 @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????)) 2151 @lset_eq_to_lset_eq_concrete 2152 elim (blocks_of_env env) 2153 [ 1: @symmetric_lset_eq @lset_eq_filter 2154  2: #hd0 #tl0 #Hind >cons_to_append 2155 >associative_append in ⊢ (??%%); 2156 >associative_append in ⊢ (??%%); 2157 @cons_monotonic_eq @Hind ] 2158 ] qed. 1368 2159 1369 2160 … … 1378 2169 ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?. 1379 2170 1380 (* Any environment is a "disjoint" extension of itself with nothing. *)1381 (*1382 lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types [].1383 #e #m #ty #id1384 normalize in match (mem_assoc_env id []); normalize nodelta1385 cases (lookup ?? e id) try //1386 #b normalize nodelta1387 % #ty cases (load_value_of_type ????)1388 [ 1: %2 /2/  2: #v %1 %{v} %{v} @conj //1389 cases (assoc_env id ty) //1390 qed. *)1391 1392 2171 (* "generic" simulation relation on [res ?] *) 1393 2172 definition res_sim ≝ … … 1415 2194 switch_removal s fvs u = Some ? result → 1416 2195 switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k') 1417  swc_while : ∀fvs,e,s, cl,k,k',u,result.1418 fresh_for_statement (Swhile e s cl) u →2196  swc_while : ∀fvs,e,s,optlab,k,k',u,result. 2197 fresh_for_statement (Swhile e s optlab) u → 1419 2198 switch_cont_sim fvs k k' → 1420 2199 switch_removal s fvs u = Some ? result → 1421 switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) clk')2200 switch_cont_sim fvs (Kwhile e s optlab k) (Kwhile e (ret_st ? result) optlab k') 1422 2201  swc_dowhile : ∀fvs,e,s,k,k',u,result. 1423 2202 fresh_for_statement (Sdowhile e s) u → … … 1483 2262 *) 1484 2263 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 2264 record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { 1488 2265 rg_find_symbol: ∀s. … … 1496 2273 }. 1497 2274 1498 (* This record aims to shorten the definition of the simulation relation on states more readeable. *)1499 2275 inductive switch_state_sim (ge : genv) : state → state → Prop ≝ 1500 2276  sws_state : … … 1527 2303 (* continuation after conversion *) 1528 2304 ∀sss_k_ext : cont. 2305 (* writeable blocks *) 2306 ∀sss_writeable : list block. 1529 2307 (* memory "injection" *) 1530 ∀sss_mem_hyp : sr_memext sss_m sss_m_ext .2308 ∀sss_mem_hyp : sr_memext sss_m sss_m_ext sss_writeable. 1531 2309 (* 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.2310 ∀sss_env_hyp : disjoint_extension sss_env sss_env_ext sss_new_vars. 1533 2311 (* conversion of the current statement, using the variables produced during the conversion of the current function *) 1534 2312 ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result. … … 1550 2328 ∀ssr_m : mem. 1551 2329 ∀ssr_m_ext : mem. 1552 ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext. 2330 ∀ssr_writeable : list block. 2331 ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext ssr_writeable. 1553 2332 switch_cont_sim ssr_vars ssr_k ssr_k_ext → 1554 2333 switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext) … … 1574 2353 trace = (t ⧺ t') → 1575 2354 eventually ge P s trace. 1576 2355 1577 2356 (* [eventually] is not so nice to use directly, we would like to make the mandatory 1578 2357 * [exec_step ge s = Value ??? 〈t, s'] visible  and in the end we would like not … … 1589 2368 #ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq} 1590 2369 try assumption 1591 qed. 2370 qed. 1592 2371 1593 2372 lemma exec_lvalue_expr_elim : … … 1657 2436 ] ] ] qed. 1658 2437 1659 1660 lemma load_value_of_type_inj : ∀m1,m2,b,off,ty. 1661 sr_memext m1 m2 → ∀v. 2438 lemma load_value_of_type_inj : ∀m1,m2,writeable,b,off,ty. 2439 sr_memext m1 m2 writeable → ∀v. 1662 2440 load_value_of_type ty m1 b off = Some ? v → 1663 2441 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. 2442 #m1 #m2 #writeable #b #off #ty #Hinj #v 2443 @(load_sim_fe ?? (sr_memext_load_sim … Hinj) (mk_pointer b off)) 2444 qed. 2445 2446 2447 (* Conservation of the smenantics of binary operators under memory extensions *) 2448 lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable. 2449 ∀Hext:sr_memext m1 m2 writeable. ∀res. 1671 2450 sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res → 1672 2451 sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res. 1673 #op #v1 #v2 #e1 #e2 #m1 #m2 # Hmemext #res cases op2452 #op #v1 #v2 #e1 #e2 #m1 #m2 #writeable #Hmemext #res cases op 1674 2453 whd in match (sem_binary_operation ??????); 1675 2454 try // … … 1693 2472  4: #H @H ] 1694 2473 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 ] 2474 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 2475 [ 2: >andb_lsimpl_false normalize nodelta #_ #Habsurd destruct (Habsurd) ] 2476 #Hvalid >(Hvalid (refl ??)) 2477 lapply (Hvalid_cons ptr') 2478 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 2479 [ 2: >andb_lsimpl_true #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2480 #H' >(H' (refl ??)) >andb_lsimpl_true #Hres @Hres 1719 2481  3: #fsz #H @H 1720 2482  4: #ty1 #ty2 #H @H ] … … 1831 2593 ] qed. 1832 2594 1833 1834 2595 (* Simulation relation on expressions *) 1835 lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2, ext.1836 ∀Hext:sr_memext m1 m2 .2596 lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,writeable,ext. 2597 ∀Hext:sr_memext m1 m2 writeable. 1837 2598 switch_removal_globals ? fundef_switch_removal ge ge' → 1838 disjoint_extension en1 m1 en2 m2 ext Hext → 2599 disjoint_extension en1 en2 ext → 2600 (* disjoint_extension en1 en2 ext Hext → *) 1839 2601 ext_fresh_for_genv ext ge → 1840 2602 (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ 1841 2603 (∀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_genv2604 #ge #ge' #en1 #m1 #en2 #m2 #writeable #ext #Hext #Hrelated #Hdisjoint (* #Hdisjoint *) #Hext_fresh_for_genv 1843 2605 @expr_lvalue_ind_combined 1844 2606 [ 1: #csz #cty #i #a1 … … 1866 2628 whd in match (load_value_of_type' ???); 1867 2629 whd in match (load_value_of_type' ???); 1868 lapply (load_value_of_type_inj m1 m2 bl1 o1 ty Hext)2630 lapply (load_value_of_type_inj m1 m2 writeable bl1 o1 ty Hext) 1869 2631 cases (load_value_of_type ty m1 bl1 o1) 1870 2632 [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) … … 1874 2636  4: #v #ty whd * * #b #o #tr 1875 2637 whd in match (exec_lvalue' ?????); 1876 whd in match (exec_lvalue' ?????); 1877 lapply (Hdisjoint v)2638 whd in match (exec_lvalue' ?????); cases Hdisjoint * 2639 #HA #HB #HC lapply (HA v) lapply (HB v) lapply (HC v) HA HB HC 1878 2640 lapply (Hext_fresh_for_genv v) 1879 2641 cases (mem_assoc_env v ext) #Hglobal 1880 [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1 1881 >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?); 1882 >(Hglobal (refl ??)) normalize 1883 #Habsurd destruct (Habsurd) 1884  2: normalize nodelta 1885 cases (lookup ?? en1 v) normalize nodelta 1886 [ 1: #Hlookup2 <Hlookup2 normalize nodelta 2642 [ 1: >(Hglobal (refl ??)) #_ #HB #HA >(HA (refl ??)) normalize 2643 #Habsurd destruct 2644  2: normalize nodelta #Hsim #_ #_ 2645 cases (lookup ?? en1 v) in Hsim; normalize nodelta 2646 [ 1: #Hlookup2 <(Hlookup2 (refl ??)) normalize nodelta 1887 2647 lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym 1888 2648 #H @H 1889  2: #block 1890 cases (lookup ?? en2 v) normalize nodelta 1891 [ 1: #Habsurd destruct (Habsurd) 1892  2: #b #Heq destruct (Heq) #H @H ] 1893 ] 1894 ] 2649  2: #blo #Hlookup2 <(Hlookup2 (refl ??)) #Heq normalize nodelta @Heq ] ] 1895 2650  5: #e #ty whd in ⊢ (% → %); 1896 2651 whd in match (exec_lvalue' ?????); … … 1918 2673 >(Hsim2 ? (refl ??)) 1919 2674 whd in match (m_bind ?????); 1920 lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 Hext)2675 lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 writeable Hext) 1921 2676 cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1) 1922 2677 [ 1: #_ // ] #val #H >(H val (refl ??)) … … 1994 2749 ] qed. 1995 2750 1996 1997 1998 2751 (* 1999 2752 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. … … 2246 2999 qed. 2247 3000 2248 (* Main theorem. To be ported and completed to memory injections. TODO *) 3001 (* Main theorem. To be ported and completed to memory injections. TODO *) 2249 3002 theorem switch_removal_correction : 2250 3003 ∀ge,ge',s1, s1', tr, s2. … … 2254 3007 eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr. 2255 3008 #ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state 3009 @cthulhu 3010 qed. 3011 3012 (* 2256 3013 inversion Hsim_state 2257 3014 [ 1: (* regular state *) 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_hyp3015 #sss_statement #sss_result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars 3016 #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp 2260 3017 #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_vars3018 elim (sim_related_globals … ge ge' 3019 sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars 2263 3020 sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge) 2264 3021 #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_ … … 2284 3041 whd in ⊢ ((??%?) → ?); 2285 3042 [ 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 // 2288 normalize in Heq_env; destruct (Heq_env) 2289 %3 // 2290 (* cut (blocks_of_env e = blocks_of_env e') 2291 [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl; 2292 lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ] 2293 #Heq >Heq %3 // *) 2294  *: #H destruct (H) ] 2295  2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 2296 whd in match (ret ??) in Heq; destruct (Heq) 2297 @(eventually_now ????) whd in match (exec_step ??); 2298 %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try // 2299 %1 try // 2300  3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 2301 @(eventually_now ????) whd in match (exec_step ??); 2302 whd in match (ret ??) in Heq; destruct (Heq) 2303 %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try // 2304 >while_commute %1 try // 2305  4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 2306 @(eventually_now ????) whd in match (exec_step ??); 2307 lapply (Hexpr_related e0) 2308 cases (exec_expr ge e m e0) in Heq; 2309 [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2310  1: * #b #tr whd in match (m_bind ?????); #Heq 2311 * 2312 [ 2: * #error #Habsurd destruct (Habsurd) 2313  1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉))) 2314 whd in match (bindIO ??????); 2315 cases (exec_bool_of_val b (typeof e0)) in Heq; 2316 [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2317  1: * whd in match (bindIO ??????); #Heq destruct (Heq) 2318 whd in match (bindIO ??????); 2319 [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)} 2320 @conj // >dowhile_commute %1 try // 2321  2: %{(State (function_switch_removal f) Sskip k0' e m)} 2322 @conj // %1{us} try // 2323 @(fresh_for_Sskip … Hus_fresh) 2324 ] ] ] ] 2325  5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 2326 @(eventually_now ????) whd in match (exec_step ??); 2327 whd in match (ret ??) in Heq; destruct 2328 %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)} 2329 @conj try // %1{u} try // 2330  6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq 2331 @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq; 2332 destruct (Heq) 2333 %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)} 2334 @conj try // %1 2335 [ 2: @swc_for3 // 2336  1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ] 2337  7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq 2338 @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq; 2339 destruct (Heq) 2340 %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)} 2341 @conj try // <(for_commute ??? u uA) try // %1 2342 [ 2: assumption 2343  1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ] 2344  8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?); 2345 #Heq @(eventually_now ????) whd in match (exec_step ??); 2346 destruct (Heq) 2347 %{(State (function_switch_removal f) Sskip k0' e m)} @conj // 2348 %1{u} // 2349  9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq 2350 @(eventually_now ????) whd in match (exec_step ??); 2351 >fn_return_simplify cases (fn_return f) in Heq; 2352 [ 1:  2: #sz #sg  3: #fsz  4: #rg #ptr_ty  5: #rg #array_ty #array_sz  6: #domain #codomain 2353  7: #structname #fieldspec  8: #unionname #fieldspec  9: #rg #id ] 2354 normalize nodelta 2355 [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H) 2356 %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))} 2357 @conj try // %3 destruct // 2358  *: #H destruct (H) ] 2359 ] 2360  2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????) 2361 whd in match (exec_step ??); 2362 cases lhs in Hu_fresh Heq; #lhs #lhs_type 2363 cases (Hlvalue_related lhs lhs_type) 2364 whd in match (exec_lvalue ge e m (Expr ??)); 2365 whd in match (exec_lvalue ge' e m (Expr ??)); 2366 [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ] 2367 cases (exec_lvalue' ge e m lhs lhs_type) 2368 [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd) 2369  1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??)) 2370 whd in match (m_bind ?????); 2371 cases (Hexpr_related rhs) 2372 [ 2: * #error #Hfail >Hfail #_ 2373 whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2374  1: cases (exec_expr ge e m rhs) 2375 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd) 2376  1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??)) 2377 whd in match (bindIO ??????) in ⊢ (% → % → %); 2378 cases (opt_to_io io_out io_in ???) 2379 [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd) 2380  3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2381  2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq) 2382 %{(State (function_switch_removal f) Sskip k' e mem)} 2383 whd in match (bindIO ??????); @conj // 2384 %1{u} try // @(fresh_for_Sskip … Hfresh) 2385 ] ] ] ] 2386  3: (* Scall *) normalize nodelta #Heq @(eventually_now ????) 2387 whd in match (exec_step ??); 2388 cases (Hexpr_related func) in Heq; 2389 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2390  1: cases (exec_expr ge e m func) 2391 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2392  1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??)) 2393 whd in match (m_bind ?????); normalize nodelta 2394 lapply (related_globals_exprlist_simulation ge ge' e m Hrelated) 2395 #Hexprlist_sim cases (Hexprlist_sim args) 2396 [ 2: * #error #Hfail >Hfail 2397 whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2398  1: cases (exec_exprlist ge e m args) 2399 [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2400  1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??)) 2401 whd in match (bindIO ??????) in ⊢ (% → %); 2402 elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval) 2403 cases (find_funct clight_fundef ge fval) 2404 [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??)) 2405 whd in match (bindIO ??????) in ⊢ (% → %); 2406 >fundef_type_simplify 2407 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func)) 2408 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2409  1: #Heq whd in match (bindIO ??????) in ⊢ (% → %); 2410 cases retv normalize nodelta 2411 [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct 2412 %{(Callstate (fundef_switch_removal clfd) values 2413 (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)} 2414 @conj try // %2 try // @swc_call // 2415  2: * #retval_ed #retval_type 2416 whd in match (exec_lvalue ge ???); 2417 whd in match (exec_lvalue ge' ???); 2418 elim (Hlvalue_related retval_ed retval_type) 2419 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2420  1: cases (exec_lvalue' ge e m retval_ed retval_type) 2421 [ 2: #error #_ whd in match (m_bind ?????); #Habsurd 2422 destruct (Habsurd) 2423  1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??)) 2424 whd in match (m_bind ?????) in ⊢ (% → %); 2425 #Heq destruct (Heq) 2426 %{(Callstate (fundef_switch_removal clfd) values 2427 (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉) 2428 (function_switch_removal f) e k') m)} 2429 @conj try // 2430 %2 @swc_call // 2431 ] ] ] ] 2432  1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %); 2433 whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2434 ] ] ] ] ] 2435  4: (* Ssequence *) normalize nodelta 2436 whd in match (ret ??) in ⊢ (% → ?); #Heq 2437 @(eventually_now ????) 2438 %{(State (function_switch_removal f) 2439 (\fst (\fst (switch_removal stm1 u))) 2440 (Kseq (\fst (\fst (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)} 2441 @conj 2442 [ 2: destruct (Heq) %1 2443 [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // 2444  2: @swc_seq try // @switch_removal_fresh 2445 elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ] 2446  1: whd in match (sw_rem ??); whd in match (switch_removal ??); 2447 cases (switch_removal stm1 u) 2448 * #stm1' #fresh_vars #u' normalize nodelta 2449 cases (switch_removal stm2 u') 2450 * #stm2' #fresh_vars2 #u'' normalize nodelta 2451 whd in match (exec_step ??); 2452 destruct (Heq) @refl 2453 ] 2454  5: (* Ifthenelse *) normalize nodelta 2455 whd in match (ret ??) in ⊢ (% → ?); #Heq 2456 @(eventually_now ????) whd in match (sw_rem ??); 2457 whd in match (switch_removal ??); 2458 elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta 2459 elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta 2460 whd in match (exec_step ??); 2461 cases (Hexpr_related cond) in Heq; 2462 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2463  1: cases (exec_expr ge e m cond) 2464 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2465  1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) 2466 whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); 2467 cases (exec_bool_of_val condval (typeof cond)) 2468 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2469  1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval 2470 destruct (Heq_condval) whd in match (bindIO ??????); 2471 normalize nodelta 2472 [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try // 2473 cut (iftrue' = (\fst (\fst (switch_removal iftrue u)))) 2474 [ 1: >Hiftrue_eq normalize // ] 2475 #Hrewrite >Hrewrite %1 2476 elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) // 2477  2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try // 2478 cut (iffalse' = (\fst (\fst (switch_removal iffalse uA)))) 2479 [ 1: >Hiffalse_eq // ] 2480 #Hrewrite >Hrewrite %1 try // 2481 cut (uA = (\snd (switch_removal iftrue u))) 2482 [ 1: >Hiftrue_eq // 2483  2: #Heq_uA >Heq_uA 2484 elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) 2485 #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh // 2486 ] ] ] ] ] 2487  6: (* While loop *) normalize nodelta 2488 whd in match (ret ??) in ⊢ (% → ?); #Heq 2489 @(eventually_now ????) whd in match (sw_rem ??); 2490 whd in match (switch_removal ??); 2491 elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta 2492 whd in match (exec_step ??); 2493 cases (Hexpr_related cond) in Heq; 2494 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2495  1: cases (exec_expr ge e m cond) 2496 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2497  1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) 2498 whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); 2499 cases (exec_bool_of_val condval (typeof cond)) 2500 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2501  1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval 2502 destruct (Heq_condval) whd in match (bindIO ??????); 2503 normalize nodelta 2504 [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try // 2505 cut (body' = (\fst (\fst (switch_removal body u)))) 2506 [ 1: >Hbody_eq // ] 2507 #Hrewrite >Hrewrite %1 2508 [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) // 2509  2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ] 2510  2: %{(State (function_switch_removal f) Sskip k' e m)} @conj // 2511 %1{u} try // @(fresh_for_Sskip … Hu_fresh) 2512 ] ] ] ] 2513  7: (* Dowhile loop *) normalize nodelta 2514 whd in match (ret ??) in ⊢ (% → ?); #Heq 2515 @(eventually_now ????) whd in match (sw_rem ??); 2516 whd in match (switch_removal ??); 2517 elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta 2518 whd in match (exec_step ??); 2519 destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj 2520 try // 2521 cut (body' = (\fst (\fst (switch_removal body u)))) 2522 [ 1: >Hbody_eq // ] 2523 #Hrewrite >Hrewrite %1 2524 [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) // 2525  2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ] 2526  8: (* For loop *) normalize nodelta 2527 whd in match (ret ??) in ⊢ (% → ?); #Heq 2528 @(eventually_now ????) whd in match (sw_rem ??); 2529 whd in match (switch_removal ??); 2530 cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip 2531 [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta 2532 elim (switch_removal_eq step u) #step' * #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta 2533 elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta 2534 whd in match (exec_step ??); 2535 cases (Hexpr_related cond) 2536 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2537  1: cases (exec_expr ge e m cond) 2538 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2539  1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) 2540 whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); 2541 cases (exec_bool_of_val condval (typeof cond)) 2542 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2543  1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval 2544 destruct (Heq_condval) 2545 [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj 2546 try // 2547 cut (body' = (\fst (\fst (switch_removal body uA)))) 2548 [ 1: >Hbody_eq // ] 2549 #Hrewrite >Hrewrite 2550 cut (uA = (\snd (switch_removal step u))) 2551 [ 1: >Hstep_eq // ] #HuA 2552 elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * * 2553 #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1 2554 [ 1: >HuA @switch_removal_fresh assumption 2555  2: cut (step' = (\fst (\fst (switch_removal step u)))) 2556 [ >Hstep_eq // ] 2557 #Hstep >Hstep @swc_for2 try assumption 2558 @for_fresh_lift try assumption ] 2559  2: %{(State (function_switch_removal f) Sskip k' e m)} @conj 2560 try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption 2561 ] ] ] ] 2562  2: #Heq 2563 elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta 2564 elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta 2565 elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta 2566 whd in match (exec_step ??); 2567 cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ] 2568 #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip) 2569 whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta 2570 whd in match (ret ??); destruct (Heq) 2571 %{(State (function_switch_removal f) (\fst (\fst (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)} 2572 @conj try // 2573 cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep' 2574 cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody' 2575 <for_commute [ 2: >Hstep_eq // ] 2576 elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * * 2577 #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption 2578 @swc_seq try // @for_fresh_lift 2579 cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq 2580 >HuA_eq @switch_removal_fresh assumption 2581 ] 2582  9: (* break *) normalize nodelta 2583 inversion Hsim_cont 2584 [ 1: #Hk #Hk' #_ 2585  2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_ 2586  3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_ 2587  4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_ 2588  5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_ 2589  6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_ 2590  8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_ 2591  9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ] 2592 normalize nodelta #H try (destruct (H)) 2593 whd in match (ret ??) in H; destruct (H) 2594 @(eventually_now ????) 2595 [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: //  2,4: %1{u} // ] 2596  2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ] 2597  10: (* Continue *) normalize nodelta 2598 inversion Hsim_cont 2599 [ 1: #Hk #Hk' #_ 2600  2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_ 2601  3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_ 2602  4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_ 2603  5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_ 2604  6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_ 2605  8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_ 2606  9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ] 2607 normalize nodelta #H try (destruct (H)) 2608 @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H; 2609 destruct (H) 2610 [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption 2611  2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try // 2612 >while_commute %1{u0} try assumption 2613  3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H; 2614 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2615  1: * #condval #trace whd in match (m_bind ?????); 2616 #Heq * 2617 [ 2: * #error #Habsurd destruct (Habsurd) 2618  1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) Hexec #Hexec >Hexec 2619 whd in match (bindIO ??????); 2620 cases (exec_bool_of_val condval (typeof cond)) in Heq; 2621 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2622  1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????); 2623 [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)} 2624 @conj try // >dowhile_commute %1{u0} assumption 2625  2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // 2626 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ] 2627 ] ] ] 2628  4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0} 2629 try // @(fresh_for_Scontinue … Hfor_fresh) 2630  5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)} 2631 @conj try // %1{u0} 2632 elim (substatement_fresh … Hfor_fresh) * * try // 2633 #HSskip #Hcond #Hstep #Hbody 2634 @swc_for3 assumption 2635  6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // 2636 %1{u} try // 2637 ] 2638  11: (* Sreturn *) normalize nodelta #Heq 2639 @(eventually_now ????) 2640 whd in match (exec_step ??) in Heq ⊢ %; 2641 cases retval in Heq; normalize nodelta 2642 [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta 2643 whd in match (ret ??) in ⊢ (% → %); 2644 [ 2: #sz #sg  3: #fl  4: #rg #ty'  5: #rg #ty #n  6: #tl #ty' 2645  7: #id #fl  8: #id #fl  9: #rg #id ] 2646 #H destruct (H) 2647 %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))} 2648 @conj [ 1: //  2: %3 @call_cont_swremoval // ] 2649  2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta 2650 [ 1: #_ #Habsurd destruct (Habsurd) 2651  2: #_ elim (Hexpr_related expr) 2652 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2653  1: cases (exec_expr ??? expr) 2654 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2655  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) 2656 #Hrewrite >Hrewrite 2657 whd in match (m_bind ?????); whd in match (m_bind ?????); 2658 #Heq destruct (Heq) 2659 %{(Returnstate (\fst a) (call_cont k') (free_list m (blocks_of_env e)))} 2660 @conj [ 1: //  2: %3 @call_cont_swremoval // ] 2661 ] ] ] ] 2662  12: (* Sswitch. Main proof case. *) normalize nodelta 2663 (* Case analysis on the outcome of the tested expression *) 2664 cases (exec_expr_int ge e m cond) 2665 [ 2: cases (exec_expr ge e m cond) 2666 [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd) 2667  1: * #val #trace cases val 2668 [ 1:  2: #condsz #condv  3: #condf  4: #condrg  5: #condptr ] 2669 whd in match (m_bind ?????); 2670 [ 1,3,4,5: #_ #Habsurd destruct (Habsurd) 2671  2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ] ] 2672 ] 2673 * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond 2674 whd in match (m_bind ?????); #Heq 2675 destruct (Heq) 2676 @eventually_later 2677 whd in match (sw_rem (Sswitch cond switchcases) u); 2678 whd in match (switch_removal (Sswitch cond switchcases) u); 2679 elim (switch_removal_branches_eq switchcases u) 2680 #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta 2681 cut (uv1 = (\snd (switch_removal_branches switchcases u))) 2682 [ 1: >Hsrb_eq // ] #Huv1_eq 2683 cut (fresh_for_statement (Sswitch cond switchcases) uv1) 2684 [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] Huv1_eq #Huv1_eq 2685 elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq Hfresh_eq #Huv2_eq normalize nodelta 2686 whd in match (simplify_switch ???); 2687 elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq Hfresh_eq #Huv3_eq normalize nodelta 2688 lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq) 2689 elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label) 2690 #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta 2691 #Huv4_eq 2692 whd in match (exec_step ??); 2693 %{(State (function_switch_removal f) 2694 (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond) 2695 (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)} 2696 %{E0} @conj try @refl 2697 %{tr} normalize in match (eq ???); @conj try // 2698 (* execute the conditional *) 2699 @eventually_later 2700 (* lift the result of the previous case analysis from [ge] to [ge'] *) 2701 whd in match (exec_step ??); 2702 whd in match (exec_lvalue ????); 2703 2704 >(exec_expr_related … Hexec_cond (Hexpr_related cond)) 2705 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 2777 3043 @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)} 3044 [ 1: @(lset_difference ? sss_writeable (blocks_of_env sss_env_ext)) 3045  3: @swc_stop 3046  2: 3047 *) 3048
Note: See TracChangeset
for help on using the changeset viewer.