Changeset 2387


Ignore:
Timestamp:
Oct 3, 2012, 1:27:38 PM (8 years ago)
Author:
garnier
Message:

Revamped memory extensions, proved stuff on freeing blocks and on environment extensions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2353 r2387  
    11include "Clight/Csyntax.ma".
    22include "Clight/fresh.ma".
    3 include "basics/lists/list.ma".
    4 include "basics/lists/listb.ma".
    53include "common/Identifiers.ma".
    64include "utilities/extralib.ma".
     
    97include "Clight/frontend_misc.ma".
    108include "Clight/memoryInjections.ma".
     9include "basics/lists/list.ma".
     10include "basics/lists/listb.ma".
     11
    1112
    1213(* -----------------------------------------------------------------------------
     
    901902].
    902903
    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(* --------------------------------------------------------------------------- *) 
     911definition 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. *)
     916lemma reflexive_memory_eq : reflexive ? memory_eq.
     917whd * #contents #nextblock #Hpos normalize @conj try //
     918qed.
     919
     920lemma symmetric_memory_eq : symmetric ? memory_eq.
     921whd * #contents #nextblock #Hpos * #contents' #nextblock' #Hpos'
     922normalize * #H1 #H2 @conj >H1 try //
     923qed.
     924
     925lemma transitive_memory_eq : transitive ? memory_eq.
     926whd
     927* #contents #nextblock #Hpos
     928* #contents1 #nextblock1 #Hpos1
     929* #contents2 #nextblock2 #Hpos2
     930normalize * #H1 #H2 * #H3 #H4 @conj //
     931qed.
    913932
    914933(* --------------------------------------------------------------------------- *)
     
    916935   properties at the back-end level. *)
    917936(* --------------------------------------------------------------------------- *) 
    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. *)
    929937
    930938(* [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. *)
     
    935943  beloadv m2 ptr = Some ? bev.
    936944
    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 
    944945definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.
    945946
     
    948949   Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧
    949950   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.  *)
    951953lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p.
    952954#m #p @conj
     
    985987] qed.
    986988
    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   . non-empty (i.e. it has been allocated a non-empty size)
     992*)
     993record 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 *)
     1000record sr_memext (m1 : mem) (m2 : mem) (writeable : list block) : Prop ≝
     1001{ (*  Non-empty 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;  *)
    10081013  (* Valid pointers are still valid in m2. One could think that this is superfluous as
    10091014     being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer
     
    10181023                       valid_pointer m2 p = true
    10191024}.
     1025
     1026(* If we have a memory extension, we can simulate loads *)
     1027lemma 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
     1054qed.
     1055
     1056(* --------------------------------------------------------------------------- *)
     1057(* Some lemmas on environments and their contents *)
     1058
     1059
     1060(* Definition of environment inclusion and equivalence *)
     1061(* Environment "inclusion". *)
     1062definition environment_sim ≝ λenv1,env2.
     1063  ∀id, res. lookup SymbolTag block env1 id = Some ? res →
     1064            lookup SymbolTag block env2 id = Some ? res.
     1065           
     1066lemma 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
     1071normalize #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           
     1090lemma 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;
     1096lapply (Hsim (an_identifier … id') res) normalize #Hsol @Hsol @Hlookup
     1097qed.
     1098
     1099(* Environment equivalence. *)
     1100definition environment_eq ≝ λenv1,env2. environment_sim env1 env2 ∧ environment_sim env2 env1.
     1101
     1102lemma symmetric_environment_eq : ∀env1,env2. environment_eq env1 env2 → environment_eq env2 env1.
     1103#env1 #env2 * #Hsim1 #Hsim2 % // qed.
     1104
     1105lemma 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]).  *)
     1110definition 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 *)
    10201116 
    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        
     1117lemma 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) → ?
     1122with
     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 ]
     1128qed.
     1129
     1130(* Small aux lemma to decompose folds on maps with list accumulators *)
     1131lemma 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
     1147lemma 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
     1166lemma 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
     1170whd in match (blocks_of_env ?);
     1171whd in match (elements ???);
     1172whd in match (lookup ????);
     1173normalize nodelta
     1174lapply res lapply id -id -res
     1175elim 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
     1210lemma 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)
     1213cases id #p elim p try /2/ qed.
     1214
     1215lemma 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
     1240let 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 ≝
     1248match 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. *)
     1261lemma 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)  *)
     1324lemma 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
     1329qed.
     1330
     1331(* [env_codomain env vars] is the image of vars through env seen as a function. *)
     1332definition 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. *)
     1343lemma 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
     1356lemma 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
     1386lemma memory_ext_reflexive :
     1387  ∀m. sr_memext m m [ ].
     1388#m % /2/ #b * qed.
     1389
     1390(* --------------------------------------------------------------------------- *)
     1391(* Lift beloadv simulation to the front-end. *)       
     1392
    10351393(* Lift load_sim to loadn. *)
    10361394lemma load_sim_loadn :
     
    10791437] qed.
    10801438
    1081 (* Lemmas relating memory extensions to [free] *)
     1439(* --------------------------------------------------------------------------- *)
     1440(* Lemmas relating reading and writing operation to memory properties. *)
    10821441
    10831442(* Successful beloadv implies valid_pointer. The converse is *NOT* true. *)
     
    10991458@Zltb_to_Zleb_true
    11001459cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
    1101 try // normalize #Habsurd destruct (Habsurd) qed.
     1460try // normalize #Habsurd destruct (Habsurd)
     1461qed.
     1462
     1463(* --------------------------------------------------------------------------- *)
     1464(* Lemmas relating memory extensions to [free] *)
    11021465
    11031466lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
     
    11331496#_ % #H destruct (H) elim Heq #H @H @refl
    11341497qed.
    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 *)
    11481498
    11491499lemma beloadv_free_beloadv :
     
    11931543
    11941544lemma 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.
    11971547  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*)
    12011551#Hload
    12021552lapply (beloadv_free_beloadv … Hload) #Hload_before_free
     
    12041554@beloadv_free_beloadv2
    12051555[ 1: @Hblocks_neq ]
    1206 @Hload_sim assumption
     1556@(sr_memext_load_sim … Hext) assumption
    12071557qed.
    12081558
     
    12711621qed.
    12721622
    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
     1623lemma 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
    12751625lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free
    12761626lapply (me_valid_pointers … Hext … Hvalid_before_free)
     
    12841634qed.
    12851635
    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
     1636lemma 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: #_ // ] ] ]
     1651qed.
     1652
     1653lemma 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/
     1656qed.
     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. *)
     1660lemma 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
    13021686            | 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
    13321719] qed.
    13331720
    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. *)
     1722lemma 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'
    13431793] qed.
    13441794
    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 
     1798lemma 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) //
     1805qed.
     1806
     1807lemma 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
     1834lemma 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
     1837qed.
     1838
     1839(* freeing equivalent sets of blocks on memory extensions yields memory extensions *)
     1840lemma 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
     1846lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq))
     1847#Heq
     1848lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext'
     1849lapply (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 ]
     1851elim 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. *)
     1879lemma 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 %
     1885try 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 *)
     1892lemma 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) ]
     1908qed.
     1909
     1910axiom 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         
     1918lemma 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
     1924lapply (memory_eq_to_mem_ext … Heq) #Hext'
     1925@(memory_ext_transitive … Hext' Hext)
     1926qed.
     1927
     1928lemma 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
     1934lapply (memory_eq_to_mem_ext … Heq) #Hext'
     1935lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H
     1936qed.
     1937
     1938lemma 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
     1941lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3
     1942elim 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
     1949lemma 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
     1951qed.
     1952
     1953lemma 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 ] ] ] ]
     1965qed.
     1966
     1967lemma 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
     1972lemma 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
     1979lemma 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
     1991whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?);
     1992whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%));
     1993elim 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
     2011lemma 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
     2017elim 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
     2053lemma 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 *)
     2065lapply (disjoint_extension_to_inclusion … Hdisjoint) #Hincl
     2066(* Environment inclusion entails set inclusion on the mapped blocks *)
     2067lapply (environment_sim_blocks_inclusion … Hincl) #Hblocks_incl
     2068(* This set inclusion can be decomposed on a common part and an extended part. *)
     2069lapply (lset_inclusion_difference ??? Hblocks_incl)
     2070* #extended_part * * #Hset_eq #Henv_disjoint_ext #Hextended_eq
     2071lapply (lset_difference_lset_eq … writeable … Hset_eq) #HeqA
     2072cut (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))
     2076lapply (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 *)
     2079cut (∀x. mem ? x extended_part → ¬ (mem ? x (blocks_of_env env)))
     2080[ 1: cases Hextended_eq #Hincl_ext #_ @(lset_not_mem_difference … Hincl_ext) ]
     2081lapply (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.
    13682159
    13692160
     
    13782169  ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?.
    13792170
    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 #id
    1384 normalize in match (mem_assoc_env id []); normalize nodelta
    1385 cases (lookup ?? e id) try //
    1386 #b normalize nodelta
    1387 % #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 
    13922171(* "generic" simulation relation on [res ?] *)
    13932172definition res_sim ≝
     
    14152194    switch_removal s fvs u = Some ? result →
    14162195    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 →
    14192198    switch_cont_sim fvs k k' →
    14202199    switch_removal s fvs u = Some ? result →
    1421     switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) cl k')
     2200    switch_cont_sim fvs (Kwhile e s optlab k) (Kwhile e (ret_st ? result) optlab k')
    14222201| swc_dowhile : ∀fvs,e,s,k,k',u,result.
    14232202    fresh_for_statement (Sdowhile e s) u →
     
    14832262*)
    14842263
    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))) →  *)
    14872264record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    14882265  rg_find_symbol: ∀s.
     
    14962273}.
    14972274
    1498 (* This record aims to shorten the definition of the simulation relation on states more readeable. *)
    14992275inductive switch_state_sim (ge : genv) : state → state → Prop ≝
    15002276| sws_state :
     
    15272303 (* continuation after conversion *)
    15282304 ∀sss_k_ext      : cont.
     2305 (* writeable blocks *)
     2306 ∀sss_writeable  : list block.
    15292307 (* 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.
    15312309 (* 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.
    15332311 (* conversion of the current statement, using the variables produced during the conversion of the current function *)
    15342312 ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result.
     
    15502328 ∀ssr_m       : mem.
    15512329 ∀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.
    15532332    switch_cont_sim ssr_vars ssr_k ssr_k_ext →
    15542333    switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext)
     
    15742353    trace = (t ⧺ t') →
    15752354    eventually ge P s trace.
    1576 
     2355   
    15772356(* [eventually] is not so nice to use directly, we would like to make the mandatory
    15782357 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
     
    15892368#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
    15902369try assumption
    1591 qed.
     2370qed.   
    15922371
    15932372lemma exec_lvalue_expr_elim :
     
    16572436] ] ] qed.
    16582437
    1659 
    1660 lemma load_value_of_type_inj : ∀m1,m2,b,off,ty.
    1661     sr_memext m1 m2 → ∀v.
     2438lemma load_value_of_type_inj : ∀m1,m2,writeable,b,off,ty.
     2439    sr_memext m1 m2 writeable → ∀v.
    16622440    load_value_of_type ty m1 b off = Some ? v →
    16632441    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))
     2444qed.
     2445
     2446
     2447(* Conservation of the smenantics of binary operators under memory extensions *)
     2448lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable.
     2449  ∀Hext:sr_memext m1 m2 writeable. ∀res.
    16712450  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res →
    16722451  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
     2452#op #v1 #v2 #e1 #e2 #m1 #m2 #writeable #Hmemext #res cases op
    16742453whd in match (sem_binary_operation ??????);
    16752454try //
     
    16932472          | 4: #H @H ]
    16942473          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
    17192481     | 3: #fsz #H @H
    17202482     | 4: #ty1 #ty2 #H @H ]
     
    18312593] qed.
    18322594
    1833 
    18342595(* Simulation relation on expressions *)
    1835 lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
    1836   ∀Hext:sr_memext m1 m2.
     2596lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,writeable,ext.
     2597  ∀Hext:sr_memext m1 m2 writeable.
    18372598  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 → *)
    18392601  ext_fresh_for_genv ext ge →
    18402602  (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
    18412603  (∀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
     2604#ge #ge' #en1 #m1 #en2 #m2 #writeable #ext #Hext #Hrelated #Hdisjoint (* #Hdisjoint *) #Hext_fresh_for_genv
    18432605@expr_lvalue_ind_combined
    18442606[ 1: #csz #cty #i #a1
     
    18662628           whd in match (load_value_of_type' ???);
    18672629           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)
    18692631           cases (load_value_of_type ty m1 bl1 o1)
    18702632           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     
    18742636| 4: #v #ty whd * * #b #o #tr
    18752637     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
    18782640     lapply (Hext_fresh_for_genv v)
    18792641     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
    18872647               lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym
    18882648               #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 ] ]
    18952650| 5: #e #ty whd in ⊢ (% → %);
    18962651     whd in match (exec_lvalue' ?????);
     
    19182673     >(Hsim2 ? (refl ??))
    19192674     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)
    19212676     cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1)
    19222677     [ 1: #_ // ] #val #H >(H val (refl ??))
     
    19942749] qed.
    19952750
    1996 
    1997 
    19982751(*
    19992752lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
     
    22462999qed.
    22473000
    2248 (* Main theorem. To be ported and completed to memory injections. TODO *) 
     3001(* Main theorem. To be ported and completed to memory injections. TODO *)
    22493002theorem switch_removal_correction :
    22503003  ∀ge,ge',s1, s1', tr, s2.
     
    22543007  eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr.
    22553008#ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state
     3009@cthulhu
     3010qed.
     3011
     3012(*
    22563013inversion Hsim_state
    22573014[ 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_hyp
     3015  #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
    22603017  #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
     3018  elim (sim_related_globals … ge ge'
     3019             sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars
    22633020             sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge)
    22643021  #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_
     
    22843041         whd in ⊢ ((??%?) → ?);
    22853042         [ 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: (* If-then-else *) 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.