Ignore:
Timestamp:
Sep 12, 2012, 12:36:46 PM (9 years ago)
Author:
garnier
Message:

Some progress on switch removal. Small fix in the definition of free, in GenMem?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/switchRemoval.ma

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