include "Clight/Csyntax.ma". include "Clight/TypeComparison.ma". (* IG: used to prove preservation of the semantics. *) include "Clight/Cexec.ma". include "Clight/casts.ma". include "Clight/CexecSound.ma". (* include "ASM/AssemblyProof.ma". *) (* I had to manually copy some of the lemmas in this file, including an axiom ... *) (* Attempt to remove unnecessary integer casts in Clight programs. This differs from the OCaml prototype by attempting to recursively determine whether subexpressions can be changed rather than using a fixed size pattern. As a result more complex expressions such as (char)((int)x + (int)y + (int)z) where x,y and z are chars can be simplified. A possible improvement that doesn't quite fit into this scheme would be to spot that casts can be removed in expressions like (int)x == (int)y where x and y have some smaller integer type. *) (* Attempt to squeeze integer constant into a given type. This might be too conservative --- if we're going to cast it anyway, can't I just ignore the fact that the integer doesn't fit? *) (* [reduce_bits n m exp v] takes avector of size n + m + 1 and returns (if all goes well) a vector of size * m+1 (an empty vector of bits makes no sense). It proceeds by removing /all/ the [n] leading bits equal * to [exp]. If it fails, it returns None. *) let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝ match n return λn. BitVector (n+S m) → option (BitVector (S m)) with [ O ⇒ λv. Some ? v | S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ? ] v. lemma reduce_bits_ok : ∀n,m.∀exp.∀v,v'. reduce_bits (S n) m exp v = Some ? v'→ reduce_bits n m exp (tail ?? v) = Some ? v'. #n #m #exp #v #v' #H whd in H:(??%?); lapply H -H cases (eq_b ? exp) [ 1: #H whd in H:(??%?); // | 2: #H normalize in H; destruct ] qed. lemma reduce_bits_trunc : ∀n,m.∀exp.∀v:(BitVector (plus n (S m))).∀v'. reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v. #n #m elim n [ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n // | 2: #n' #Hind #exp #v #v' #H >truncate_tail > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed. lemma reduce_bits_dec : ∀n,m.∀exp.∀v. (∃v'.reduce_bits n m exp v = Some ? v') ∨ reduce_bits n m exp v = None ?. #n #m #exp #v elim (reduce_bits n m exp v) [ 1: %2 // | 2: #v' %1 @(ex_intro … v') // ] qed. (* pred_bitsize_of_intsize I32 = 31, … *) definition pred_bitsize_of_intsize : intsize → nat ≝ λsz. pred (bitsize_of_intsize sz). definition signed : signedness → bool ≝ λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ]. (* [simplify_int sz sz' sg sg' i] tries to convert an integer [i] of width [sz] and signedness [sg] * into an integer of size [sz'] of signedness [sg']. * - It first proceeds by comparing the source and target width: if the target width is strictly superior * to the source width, the conversion fails. * - If the size is equal, the argument is returned as-is. * - If the target type is strictly smaller than the source, it tries to squeeze the integer to * the desired size. *) let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝ let bit ≝ signed sg ∧ head' … i in (* [nat_compare] does more than an innocent post-doc might think. It also computes the difference between the two args. * if x < y, nat_compare x y = lt(x, y-(x+1)) * if x = y, nat_compare x y = eq x * if x > y, nat_compare x y = gt(x-(y+1), y) *) match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz') return λn,m,x.BitVector (S n) → option (BitVector (S m)) with [ nat_lt _ _ ⇒ λi. None ? (* refuse to make constants larger *) | nat_eq _ ⇒ λi. Some ? i | nat_gt x y ⇒ λi. (* Here, we have [x]=31-([y]+1) and [y] ∈ {15; 7} OR [x] = 15-(7+1) and [y] = 7. I.e.: x=15,y=15 or x=23,y=7 or x=7,y=7. * In [reduce_bits n m bit i], [i] is supposed to have type BitVector n + (S m). Since its type is here (S x) + (S y), * we deduce that the actual arguments of [reduce_bits] are (S x) and (S y), which is consistent. * If [i] is of signed type and if it is negative, then it tries to remove the (S x) first "1" bits. * Otherwise, it tries to remove the (S x) first "0" bits. *) match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with [ Some i' ⇒ if signed sg' then if eq_b bit (head' … i') then Some ? i' else None ? else Some ? i' | None ⇒ None ? ] ] i. >(commutative_plus_faster (S x)) @refl qed. lemma eq_intsize_identity : ∀id. eq_intsize id id = true. * normalize // qed. lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s). * normalize // qed. lemma type_eq_identity : ∀t. type_eq t t = true. #t normalize elim (type_eq_dec t t) [ 1: #Heq normalize // | 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed. lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false. #t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2) [ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2)) | 2: #Hneq' normalize // ] qed. definition size_le ≝ λsz1,sz2. match sz1 with [ I8 ⇒ True | I16 ⇒ match sz2 with [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ] | I32 ⇒ match sz2 with [ I32 ⇒ True | _ ⇒ False ] ]. definition size_lt ≝ λsz1,sz2. match sz1 with [ I8 ⇒ match sz2 with [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ] | I16 ⇒ match sz2 with [ I32 ⇒ True | _ ⇒ False ] | I32 ⇒ False ]. lemma size_lt_to_le : ∀sz1,sz2. size_lt sz1 sz2 → size_le sz1 sz2. #sz1 #sz2 elim sz1 elim sz2 normalize // qed. lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)). * * normalize /2/ /3/ qed. lemma size_not_lt_to_ge : ∀sz1,sz2. ¬(size_lt sz1 sz2) → (sz1 = sz2) + (size_lt sz2 sz1). * * normalize /2/ /3/ qed. (* This function already exists in prop, we want it in type. *) definition sign_eq_dect : ∀sg1,sg2:signedness. (sg1 = sg2) + (sg1 ≠ sg2). * * normalize // qed. lemma size_absurd : ∀a,b. size_le a b → size_lt b a → False. * * normalize #H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed. (* This defines necessary conditions for [src_expr] to be coerced to "target_ty". * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *) definition necessary_conditions ≝ λsrc_sz.λsrc_sg.λtarget_sz.λtarget_sg. match size_lt_dec target_sz src_sz with [ inl Hlt ⇒ true | inr Hnlt ⇒ match sz_eq_dec target_sz src_sz with [ inl Hsz_eq ⇒ match sign_eq_dect src_sg target_sg with [ inl Hsg_eq ⇒ false | inr Hsg_neq ⇒ true ] | inr Hsz_neq ⇒ false ] ]. (* Inversion on necessary_conditions *) lemma necessary_conditions_spec : ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) → ((size_lt target_sz src_sz) ∨ (src_sz = target_sz ∧ src_sg ≠ target_sg)). #src_sz #src_sg #target_sz #target_sg whd in match (necessary_conditions ????); cases (size_lt_dec target_sz src_sz) normalize nodelta [ 1: #Hlt #_ %1 // | 2: #Hnlt cases (sz_eq_dec target_sz src_sz) normalize nodelta [ 2: #_ #Hcontr destruct | 1: #Heq cases (sign_eq_dect src_sg target_sg) normalize nodelta [ 1: #_ #Hcontr destruct | 2: #Hsg_neq #_ %2 destruct /2/ ] ] ] qed. (* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an * integer value smaller but containing the same stuff than [r2] then all is well. * If the first evaluation is erroneous, we don't care about anything else. *) definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res(val×trace). match r1 with [ OK res1 ⇒ let 〈val1, tr1〉 ≝ res1 in ∀v1. val1 = Vint src_sz v1 → match r2 with [ OK res2 ⇒ let 〈val2, tr2〉 ≝ res2 in ∃v2. (val2 = Vint dst_sz v2 ∧ v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz) | _ ⇒ False ] | Error errmsg1 ⇒ True ]. (* Simulation relation used for expression evaluation. *) inductive simulate (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝ | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → simulate A r1 r2 | SimFail : (∃err. r1 = Error ? err) → simulate A r1 r2. (* Invariant of simplify_expr *) inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝ (* Inv_eq states a standard simulation result. We enforce some needed equations on types to prove the cast cases. *) | Inv_eq : ∀result_flag. result_flag = false → typeof e1 = typeof e2 → simulate ? (exec_expr ge en m e1) (exec_expr ge en m e2) → simulate ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) → simplify_inv ge en m e1 e2 target_sz target_sg result_flag (* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *) | Inv_coerce_ok : ∀src_sz,src_sg. (typeof e1) = (Tint src_sz src_sg) → (typeof e2) = (Tint target_sz target_sg) → (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) → simplify_inv ge en m e1 e2 target_sz target_sg true. (* Invariant of simplify_inside *) definition conservation ≝ λe,result:expr. ∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) ∧ typeof e = typeof result. (* This lemma proves that simplify_int actually implements an integer cast. *) (* The case 4 can be merged with cases 7 and 8. *) lemma simplify_int_implements_cast : ∀sz,sz'.∀sg,sg'.∀i,i'. simplify_int sz sz' sg sg' i = Some ? i' → i' = cast_int_int sz sg sz' i. * * [ 1: #sg #sg' #i #i' #Hsimp normalize in Hsimp ⊢ %; elim sg normalize destruct // | 2,3,6: #sg #sg' #i #i' #Hsimp normalize in Hsimp; destruct (* ⊢ %; destruct destruct whd in Hsimp:(??%?); destruct *) | 4: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %; normalize in match (signed ?) in Hsimp; normalize in match (S (plus ??)) in Hsimp; normalize in match (plus 7 8) in Hsimp; lapply Hsimp -Hsimp cases (head' bool 15 i) normalize in match (andb ??); [ 1,3: elim (reduce_bits_dec 8 7 true i) [ 1,3: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta [ 1: cases (eq_b true ?) normalize #H destruct normalize @refl | 2: #H destruct normalize @refl ] | 2,4: #Heq >Heq normalize nodelta #H destruct ] | 2,4,5,6,7,8: elim (reduce_bits_dec 8 7 false i) [ 1,3,5,7,9,11: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq) [ 1,3,4: cases (eq_b false ?) normalize nodelta #H destruct normalize @refl | 2,5,6: #H destruct normalize @refl ] | 2,4,6,8,10,12: #Heq >Heq normalize nodelta #H destruct ] ] | 5,9: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); destruct @refl | 7, 8: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %; normalize in match (signed ?) in Hsimp; normalize in match (S (plus ??)) in Hsimp; normalize in match (plus 7 24) in Hsimp; lapply Hsimp -Hsimp cases (head' bool ? i) normalize in match (andb ??); [ 1,3,9,11: [ 1,2: (elim (reduce_bits_dec 24 7 true i)) | 3,4: (elim (reduce_bits_dec 16 15 true i)) ] [ 1,3,5,7: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta [ 1,3: cases (eq_b true ?) normalize #H destruct normalize @refl | 2,4: #H destruct normalize @refl ] | 2,4,6,8: #Heq >Heq normalize nodelta #H destruct ] | 2,4,5,6,7,8,10,12,13,14,15,16: [ 1,2,3,4,5,6: elim (reduce_bits_dec 24 7 false i) | 6,7,8,9,10,11,12: elim (reduce_bits_dec 16 15 false i) ] [ 1,3,5,7,9,11,13,15,17,19,21,23: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq) [ 1,3,4,7,9,10: cases (eq_b false ?) normalize nodelta #H destruct normalize @refl | 2,5,6,8,11,12: #H destruct normalize @refl ] | 2,4,6,8,10,12,14,16,18,20,22,24: #Heq >Heq normalize nodelta #H destruct ] ] ] qed. (* Facts about cast_int_int *) (* copied from AssemblyProof *) lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A. #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); // #n #hd #tl #abs @⊥ destruct (abs) qed. lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n). ∃hd.∃tl.v ≃ VCons A n hd tl. #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); [ #abs @⊥ destruct (abs) | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] qed. lemma vector_append_zero: ∀A,m. ∀v: Vector A m. ∀q: Vector A 0. v = q@@v. #A #m #v #q >(Vector_O A q) % qed. corollary prod_vector_zero_eq_left: ∀A, n. ∀q: Vector A O. ∀r: Vector A n. 〈q, r〉 = 〈[[ ]], r〉. #A #n #q #r generalize in match (Vector_O A q …); #hyp >hyp in ⊢ (??%?); % qed. lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n). ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2. # A #m #n elim m [ 1: normalize #v elim (Vector_Sn ?? v) #hd * #tl #Eq @(ex_intro … (hd ::: [[]])) @(ex_intro … tl) >Eq normalize // | 2: #n' #Hind #v elim (Vector_Sn ?? v) #hd * #tl #Eq elim (Hind tl) #tl1 * #tl2 #Eq_tl @(ex_intro … (hd ::: tl1)) @(ex_intro … tl2) destruct normalize // ] qed. lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n). ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2. # A #m #n elim m [ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize // | 2: #n' #Hind #v elim (Vector_Sn ?? v) #hd * #tl #Eq elim (Hind tl) #tl1 * #tl2 #Eq_tl @(ex_intro … (hd ::: tl1)) @(ex_intro … tl2) destruct normalize // ] qed. lemma vsplit_zero: ∀A,m. ∀v: Vector A m. 〈[[]], v〉 = vsplit A 0 m v. #A #m #v elim v [ % | #n #hd #tl #ih normalize in ⊢ (???%); % ] qed. lemma vsplit_zero2: ∀A,m. ∀v: Vector A m. 〈[[]], v〉 = vsplit' A 0 m v. #A #m #v elim v [ % | #n #hd #tl #ih normalize in ⊢ (???%); % ] qed. (* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma. * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *) axiom vsplit_succ: ∀A, m, n. ∀l: Vector A m. ∀r: Vector A n. ∀v: Vector A (m + n). ∀hd. v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)). axiom vsplit_succ2: ∀A, m, n. ∀l: Vector A m. ∀r: Vector A n. ∀v: Vector A (m + n). ∀hd. v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)). lemma vsplit_prod2: ∀A,m,n. ∀p: Vector A (m + n). ∀v: Vector A m. ∀q: Vector A n. p = v@@q → 〈v, q〉 = vsplit' A m n p. #A #m elim m [ #n #p #v #q #hyp >hyp <(vector_append_zero A n q v) >(prod_vector_zero_eq_left A …) @vsplit_zero2 | #r #ih #n #p #v #q #hyp >hyp cases (Vector_Sn A r v) #hd #exists cases exists #tl #jmeq >jmeq @vsplit_succ2 [1: % |2: @ih % ] ] qed. lemma vsplit_prod: ∀A,m,n. ∀p: Vector A (m + n). ∀v: Vector A m. ∀q: Vector A n. p = v@@q → 〈v, q〉 = vsplit A m n p. #A #m elim m [ #n #p #v #q #hyp >hyp <(vector_append_zero A n q v) >(prod_vector_zero_eq_left A …) @vsplit_zero | #r #ih #n #p #v #q #hyp >hyp cases (Vector_Sn A r v) #hd #exists cases exists #tl #jmeq >jmeq @vsplit_succ [1: % |2: @ih % ] ] qed. lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)). #s1 #v normalize elim s1 normalize nodelta normalize in v; elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) [ 2,4: // | 1,3: #l * #r normalize nodelta #Eq1 <(vsplit_prod bool 16 16 … Eq1) elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) [ 2,4: // | 1,3: #lr * #rr normalize nodelta #Eq2 <(vsplit_prod bool 8 8 … Eq2) cut (v = (l @@ lr) @@ rr) [ 1,3 : destruct >(vector_associative_append ? 16 8) // | 2,4: #Hrewrite destruct <(vsplit_prod bool 24 8 … Hrewrite) @refl ] ] ] qed. lemma cast_idempotent : ∀s1,s2,sz1,sz2,v. size_lt sz1 sz2 → cast_int_int sz2 s1 sz1 (cast_int_int sz1 s2 sz2 v) = v. #s1 #s2 * * #v elim s1 elim s2 normalize #H try @refl @(False_ind … H) qed. lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v. * * #v normalize // qed. lemma cast_collapse : ∀s1,s2,v. cast_int_int I32 s1 I8 (cast_int_int I16 s2 I32 v) = (cast_int_int I16 s1 I8 v). #s1 #s2 #v >cast_decompose >cast_idempotent [ 1: @refl | 2: // ] qed. lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val. size_lt c_sz a_sz → size_lt c_sz b_sz → (cast_int_int a_sz a_sg c_sz val = cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)). * #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??); #Hlt1 #Hlt2 [ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27: @(False_ind … Hlt1) @(False_ind … Hlt2) | 13,25,26: >cast_identity elim a_sg elim b_sg normalize // | 22: normalize elim b_sg elim a_sg normalize normalize in val; elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) [ 2,4,6,8: normalize // | 1,3,5,7: #left * #right normalize #Eq1 <(vsplit_prod bool 16 16 … Eq1) elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) [ 2,4,6,8: // | 1,3,5,7: #rightleft * #rightright normalize #Eq2 <(vsplit_prod bool 8 8 … Eq2) cut (val = (left @@ rightleft) @@ rightright) [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) // | 2,4,6,8: #Hrewrite destruct <(vsplit_prod bool 24 8 … Hrewrite) @refl ] ] ] | 16: elim b_sg elim a_sg >cast_collapse @refl ] qed. lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val. size_le c_sz a_sz → size_le c_sz b_sz → (cast_int_int a_sz a_sg c_sz val = cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)). #a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b cases (size_lt_dec c_sz a_sz) cases (size_lt_dec c_sz b_sz) [ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb) | 2: #Hnltb #Hlta cases (size_not_lt_to_ge … Hnltb) [ 1: #Heq destruct >cast_identity // | 2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb)) ] | 3: #Hltb #Hnlta cases (size_not_lt_to_ge … Hnlta) [ 1: #Heq destruct >cast_idempotent // | 2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) ] | 4: #Hnltb #Hnlta cases (size_not_lt_to_ge … Hnlta) cases (size_not_lt_to_ge … Hnltb) [ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity // | 2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb)) | 3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) | 4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) ] ] qed. let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝ match v with [ None ⇒ None ? | Some v ⇒ match v with [ Vint sz i ⇒ match sz_eq_dec sz expected_size with [ inl Heq ⇒ Some ?? | inr _ ⇒ None ? ] | _ ⇒ None ? ] ]. >Heq in i; #i @i qed. (* cast_int_int behaves as truncate (≃ vsplit) when downsizing *) (* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *) lemma vsplit_to_truncate : ∀m,n,i. (\snd  (vsplit bool m n i)) = truncate m n i. #m #n #i normalize // qed. (* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *) lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz → (addition_n (bitsize_of_intsize target_sz) (cast_int_int src_sz sg target_sz lhs_int) (cast_int_int src_sz sg target_sz rhs_int) = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). #src_sz #target_sz #sg #lhs_int #rhs_int #Hlt elim src_sz in Hlt lhs_int rhs_int; elim target_sz [ 1,2,3,5,6,9: normalize #H @(False_ind … H) | *: elim sg #_ normalize in match (bitsize_of_intsize ?); normalize in match (bitsize_of_intsize ?); #lint #rint normalize in match (cast_int_int ????); normalize in match (cast_int_int ????); whd in match (addition_n ???); whd in match (addition_n ???) in ⊢ (???%); >vsplit_to_truncate >vsplit_to_truncate cast_identity >cast_identity >cast_identity // qed. lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz → (addition_n (bitsize_of_intsize target_sz) (cast_int_int src_sz sg target_sz lhs_int) (cast_int_int src_sz sg target_sz rhs_int) = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). #src_sz #target_sz #sg #lhs_int #rhs_int #Hle cases (sz_eq_dec target_sz src_sz) [ 1: #Heq @(integer_add_cast_eq … Heq) | 2: #Hneq cut (size_lt target_sz src_sz) [ 1: elim target_sz in Hle Hneq; elim src_sz normalize // #_ * #H @(H … (refl ??)) | 2: #Hlt @(integer_add_cast_lt … Hlt) ] ] qed. lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl. #l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len @(ex_intro … tl) >Heq >Heq elim (vsplit_eq2 … tl) #l * #r #Eq normalize <(vsplit_prod bool n m tl l r Eq) <(vsplit_prod2 bool n m tl l r Eq) normalize // qed. lemma integer_neg_trunc : ∀m,n. ∀i: BitVector (m+n). two_complement_negation n (truncate m n i) = truncate m n (two_complement_negation (m+n) i). #m elim m [ 1: #n #i normalize in i; whd in match (truncate ???); whd in match (truncate ???) in ⊢ (???%); Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?); whd in match (two_complement_negation ??) in ⊢ (??%?); lapply (Hind ? tl) #H whd in match (two_complement_negation ??) in H; (* trying to reduce add_with_carries *) normalize in match (S m'+n); whd in match (zero ?) in ⊢ (???%); >Heq in match (negation_bv ??) in ⊢ (???%); whd in match (negation_bv ??) in ⊢ (???%); >add_with_carries_unfold in ⊢ (???%); normalize in ⊢ (???%); cases hd normalize nodelta [ 1,2: (vsplit_to_truncate (S m')) >truncate_tail cases b normalize nodelta normalize in match (tail ???); @H ] ] qed. (* This was painful. *) lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz → (subtraction (bitsize_of_intsize target_sz) (cast_int_int src_sz sg target_sz lhs_int) (cast_int_int src_sz sg target_sz rhs_int) = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). #src_sz #target_sz #sg #lhs_int #rhs_int #Hlt elim src_sz in Hlt lhs_int rhs_int; elim target_sz [ 1,2,3,5,6,9: normalize #H @(False_ind … H) | *: elim sg #_ normalize in match (bitsize_of_intsize ?); normalize in match (bitsize_of_intsize ?); #lint #rint normalize in match (cast_int_int ????); normalize in match (cast_int_int ????); whd in match (subtraction ???); whd in match (subtraction ???) in ⊢ (???%); >vsplit_to_truncate >vsplit_to_truncate >integer_neg_trunc cast_identity >cast_identity >cast_identity // qed. lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz → (subtraction (bitsize_of_intsize target_sz) (cast_int_int src_sz sg target_sz lhs_int) (cast_int_int src_sz sg target_sz rhs_int) = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). #src_sz #target_sz #sg #lhs_int #rhs_int #Hle cases (sz_eq_dec target_sz src_sz) [ 1: #Heq @(integer_sub_cast_eq … Heq) | 2: #Hneq cut (size_lt target_sz src_sz) [ 1: elim target_sz in Hle Hneq; elim src_sz normalize // #_ * #H @(H … (refl ??)) | 2: #Hlt @(integer_sub_cast_lt … Hlt) ] ] qed. lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le sz' sz. * #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed. lemma smaller_integer_val_identity : ∀sz,sg,x. smaller_integer_val sz sz sg x x. #sz #sg * [ 2: #error // | 1: * #val #trace whd in match (smaller_integer_val ?????); #v1 #Hval %{v1} @conj try @conj try @conj // elim sz // ] qed. (* Inversion on exec_cast *) lemma exec_cast_inv : ∀castee_val,src_sz,src_sg,cast_sz,cast_sg,m,result. exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg) = OK ? result → ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i). #castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result elim castee_val [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] [ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ] whd in ⊢ ((??%?) → ?); cases (sz_eq_dec sz' src_sz) [ 1: #Heq destruct >intsize_eq_elim_true normalize nodelta #Heq destruct %{i} /2/ | 2: #Hneq >intsize_eq_elim_false; try assumption #H destruct ] qed. (* Lemmas related to the Ebinop case *) lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg. * * // qed. lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg. * * // qed. lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true. * * normalize #H @conj // qed. (* Operations where it is safe to use a smaller integer type on the assumption that we would cast it down afterwards anyway. *) definition binop_simplifiable ≝ λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ]. (* Inversion principle for integer addition *) lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)). #sz #sg #v1 #v2 #m #r elim v1 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] whd in ⊢ ((??%?) → ?); normalize nodelta >classify_add_int normalize nodelta #H destruct elim v2 in H; [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ] whd in ⊢ ((??%?) → ?); #H destruct elim (sz_eq_dec sz' sz'') [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct ] qed. (* Inversion principle for integer subtraction. *) lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)). #sz #sg #v1 #v2 #m #r elim v1 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] whd in ⊢ ((??%?) → ?); normalize nodelta >classify_sub_int normalize nodelta #H destruct elim v2 in H; [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ] whd in ⊢ ((??%?) → ?); #H destruct elim (sz_eq_dec sz' sz'') [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct ] qed. definition is_int : val → Prop ≝ λv. match v with [ Vint _ _ ⇒ True | _ ⇒ False ]. (* "negative" (in the sense of ¬ Some) inversion principle for integer addition *) lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? → ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. #sz #sg #v1 #v2 #m elim v1 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] [ 2: | *: #_ %1 %1 % #H @H ] elim v2 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ] [ 2: | *: #_ %1 %2 % #H @H ] whd in ⊢ ((??%?) → ?); normalize nodelta >classify_add_int normalize nodelta elim (sz_eq_dec sz' sz'') [ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd) | 2: #Hneq >intsize_eq_elim_false try assumption #_ %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // ] qed. (* "negative" inversion principle for integer subtraction *) lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? → ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. #sz #sg #v1 #v2 #m elim v1 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] [ 2: | *: #_ %1 %1 % #H @H ] elim v2 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ] [ 2: | *: #_ %1 %2 % #H @H ] whd in ⊢ ((??%?) → ?); normalize nodelta >classify_sub_int normalize nodelta elim (sz_eq_dec sz' sz'') [ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd) | 2: #Hneq >intsize_eq_elim_false try assumption #_ %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // ] qed. lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m. ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?. #op #sz #sg #v1 #v2 #m #H elim op normalize in match (binop_simplifiable ?); #H destruct elim v1 in H; [ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: #r | 5,10: #ptr ] #_ whd in match (sem_binary_operation ??????); normalize nodelta >classify_add_int normalize nodelta // >classify_sub_int normalize nodelta // qed. notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)" with precedence 10 for @{ match \$t return λx.x = \$t → ? with [ mk_Sig \${ident x} \${ident y} ⇒ λ\${ident E}.\$s ] (refl ? \$t) }. notation > "hvbox('let' « 〈ident x1,ident x2〉, ident y» 'as' ident E, ident F ≝ t 'in' s)" with precedence 10 for @{ match \$t return λx.x = \$t → ? with [ mk_Sig \${fresh a} \${ident y} ⇒ λ\${ident E}. match \${fresh a} return λx.x = \${fresh a} → ? with [ mk_Prod \${ident x1} \${ident x2} ⇒ λ\${ident F}. \$s ] (refl ? \${fresh a}) ] (refl ? \$t) }. (* This function will make your eyes bleed. You've been warned. * Implements a correct-by-construction version of Brian's original cast-removal code. Does so by * threading an invariant defined in [simplify_inv], which says roughly "simplification yields either what you hoped for, i.e. an integer value of the right size, OR something equivalent to the original expression". [simplify_expr] is not to be called directly: simplify inside is the proper wrapper. * TODO: proper doc. Some cases are simplifiable. Some type equality tests are maybe dispensable. * This function is slightly more conservative than the original one, but this should be incrementally * modifiable (replacing calls to simplify_inside by calls to simplify_expr, + proving correction). * Also, I think that the proofs are factorizable to a great deal, but I'd rather have something * more or less "modular", case-by-case wise. *) let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ match e return λx. x = e → ? with [ Expr ed ty ⇒ λHexpr_eq. match ed return λx. ed = x → ? with [ Econst_int cst_sz i ⇒ λHdesc_eq. match ty return λx. x=ty → ? with [ Tint ty_sz sg ⇒ λHexprtype_eq. (* Ensure that the displayed type size [cst_sz] and actual size [sz] are equal ... *) match sz_eq_dec cst_sz ty_sz with [ inl Hsz_eq ⇒ match type_eq_dec ty (Tint target_sz target_sg) with [ inl Hdonothing ⇒ «〈true, e〉, ?» | inr Hdosomething ⇒ (* Do the actual useful work *) match simplify_int cst_sz target_sz sg target_sg i return λx. (simplify_int cst_sz target_sz sg target_sg i) = x → ? with [ Some i' ⇒ λHsimpl_eq. «〈true, Expr (Econst_int target_sz i') (Tint target_sz target_sg)〉, ?» | None ⇒ λ_. «〈false, e〉, ?» ] (refl ? (simplify_int cst_sz target_sz sg target_sg i)) ] | inr _ ⇒ (* The expression is ill-typed. *) «〈false, e〉, ?» ] | _ ⇒ λ_. «〈false, e〉, ?» ] (refl ? ty) | Ederef e1 ⇒ λHdesc_eq. let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in «〈false, Expr (Ederef e2) ty〉, ?» | Eaddrof e1 ⇒ λHdesc_eq. let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in «〈false, Expr (Eaddrof e2) ty〉, ?» | Eunop op e1 ⇒ λHdesc_eq. let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in «〈false, Expr (Eunop op e2) ty〉, ?» | Ebinop op lhs rhs ⇒ λHdesc_eq. (* Type equality is enforced to prove the equalities needed in return by the invariant. *) match binop_simplifiable op return λx. (binop_simplifiable op) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) with [ true ⇒ λHop_simplifiable_eq. match assert_type_eq ty (typeof lhs) with [ OK Hty_eq_lhs ⇒ match assert_type_eq (typeof lhs) (typeof rhs) with [ OK Htylhs_eq_tyrhs ⇒ let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr lhs target_sz target_sg in let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr rhs target_sz target_sg in match desired_type_lhs ∧ desired_type_rhs return λx. (desired_type_lhs ∧ desired_type_rhs) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) with [ true ⇒ λHdesired_eq. «〈true, Expr (Ebinop op lhs1 rhs1) (Tint target_sz target_sg)〉, ?» | false ⇒ λHdesired_eq. let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» ] (refl ? (desired_type_lhs ∧ desired_type_rhs)) | Error _ ⇒ let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» ] | Error _ ⇒ let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» ] | false ⇒ λHop_simplifiable_eq. let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» ] (refl ? (binop_simplifiable op)) | Ecast cast_ty castee ⇒ λHdesc_eq. match cast_ty return λx. x = cast_ty → ? with [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. match type_eq_dec ty cast_ty with [ inl Hcast_eq ⇒ match necessary_conditions cast_sz cast_sg target_sz target_sg return λx. x = (necessary_conditions cast_sz cast_sg target_sz target_sg) → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) with [ true ⇒ λHconditions. let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr castee target_sz target_sg in match desired_type return λx. desired_type = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) with [ true ⇒ λHdesired_eq. «〈true, castee1〉, ?» | false ⇒ λHdesired_eq. let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) with [ true ⇒ λHdesired2_eq. «〈false, castee2〉, ?» | false ⇒ λHdesired2_eq. «〈false, Expr (Ecast ty castee2) cast_ty〉, ?» ] (refl ? desired_type2) ] (refl ? desired_type) | false ⇒ λHconditions. let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) with [ true ⇒ λHdesired2_eq. «〈false, castee2〉, ?» | false ⇒ λHdesired2_eq. «〈false, Expr (Ecast ty castee2) cast_ty〉, ?» ] (refl ? desired_type2) ] (refl ? (necessary_conditions cast_sz cast_sg target_sz target_sg)) | inr Hcast_neq ⇒ (* inconsistent types ... *) let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in «〈false, Expr (Ecast cast_ty castee1) ty〉, ?» ] | _ ⇒ λHcast_ty_eq. let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in «〈false, Expr (Ecast cast_ty castee1) ty〉, ?» ] (refl ? cast_ty) | Econdition cond iftrue iffalse ⇒ λHdesc_eq. let «cond1, Hcond_equiv» as Hsimplify ≝ simplify_inside cond in match assert_type_eq ty (typeof iftrue) with [ OK Hty_eq_iftrue ⇒ match assert_type_eq (typeof iftrue) (typeof iffalse) with [ OK Hiftrue_eq_iffalse ⇒ let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue ≝ simplify_expr iftrue target_sz target_sg in let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr iffalse target_sz target_sg in match desired_true ∧ desired_false return λx. (desired_true ∧ desired_false) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) with [ true ⇒ λHdesired_eq. «〈true, Expr (Econdition cond1 iftrue1 iffalse1) (Tint target_sz target_sg)〉, ?» | false ⇒ λHdesired_eq. let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» ] (refl ? (desired_true ∧ desired_false)) | _ ⇒ let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» ] | _ ⇒ let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» ] (* Could probably do better with these, too. *) | Eandbool lhs rhs ⇒ λHdesc_eq. let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in «〈false, Expr (Eandbool lhs1 rhs1) ty〉, ?» | Eorbool lhs rhs ⇒ λHdesc_eq. let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in «〈false, Expr (Eorbool lhs1 rhs1) ty〉,?» (* Could also improve Esizeof *) | Efield rec_expr f ⇒ λHdesc_eq. let «rec_expr1, Hrec_expr_equiv» as Hsimplify ≝ simplify_inside rec_expr in «〈false,Expr (Efield rec_expr1 f) ty〉, ?» | Ecost l e1 ⇒ λHdesc_eq. (* The invariant requires that the toplevel [ty] type matches the type of [e1]. *) (* /!\ XXX /!\ We assume that the type of a cost-labelled expr is the type of the underlying expr. *) match type_eq_dec ty (typeof e1) with [ inl Heq ⇒ let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr e1 target_sz target_sg in «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?» | inr Hneq ⇒ let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in «〈false, Expr (Ecost l e2) ty〉, ?» ] | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» (* | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *) (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact require to alter the semantics of [load_value_of_type]. *) | Evar id ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» | Esizeof t ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» ] (refl ? ed) ] (refl ? e) and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝ match e return λx. x = e → ? with [ Expr ed ty ⇒ λHexpr_eq. match ed return λx. x = ed → ? with [ Ederef e1 ⇒ λHdesc_eq. let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in «Expr (Ederef e2) ty, ?» | Eaddrof e1 ⇒ λHdesc_eq. let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in «Expr (Eaddrof e2) ty, ?» | Eunop op e1 ⇒ λHdesc_eq. let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in «Expr (Eunop op e2) ty, ?» | Ebinop op lhs rhs ⇒ λHdesc_eq. let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in «Expr (Ebinop op lhs1 rhs1) ty, ?» | Ecast cast_ty castee ⇒ λHdesc_eq. match type_eq_dec ty cast_ty with [ inl Hcast_eq ⇒ match cast_ty return λx. x = cast_ty → Σresult:expr. conservation e result with [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr castee cast_sz cast_sg in match success return λx. x = success → Σresult:expr. conservation e result with [ true ⇒ λHsuccess_eq. «castee1, ?» | false ⇒ λHsuccess_eq. «Expr (Ecast cast_ty castee1) ty, ?» ] (refl ? success) | _ ⇒ λHcast_ty_eq. «e, ?» ] (refl ? cast_ty) | inr Hcast_neq ⇒ «e, ?» ] | Econdition cond iftrue iffalse ⇒ λHdesc_eq. let «cond1, Hequiv_cond» as Eq_cond ≝ simplify_inside cond in let «iftrue1, Hequiv_iftrue» as Eq_iftrue ≝ simplify_inside iftrue in let «iffalse1, Hequiv_iffalse» as Eq_iffalse ≝ simplify_inside iffalse in «Expr (Econdition cond1 iftrue1 iffalse1) ty, ?» | Eandbool lhs rhs ⇒ λHdesc_eq. let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in «Expr (Eandbool lhs1 rhs1) ty, ?» | Eorbool lhs rhs ⇒ λHdesc_eq. let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in «Expr (Eorbool lhs1 rhs1) ty, ?» | Efield rec_expr f ⇒ λHdesc_eq. let «rec_expr1, Hequiv_rec» as Eq_rec ≝ simplify_inside rec_expr in «Expr (Efield rec_expr1 f) ty, ?» | Ecost l e1 ⇒ λHdesc_eq. let «e2, Hequiv» as Eq ≝ simplify_inside e1 in «Expr (Ecost l e2) ty, ?» | _ ⇒ λHdesc_eq. «e, ?» ] (refl ? ed) ] (refl ? e). #ge #en #m [ 1,3,5,6,7,8,9,10,11,12: %1 try @refl cases (exec_expr ge en m e) #res try (@(SimOk ???) //) | 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/ (* whd in match (exec_expr ????); >eq_intsize_identity whd >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ] *) | 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/ whd in match (exec_expr ????); whd in match (exec_expr ????); >eq_intsize_identity >eq_intsize_identity whd #v1 #Heq destruct (Heq) %{i'} try @conj try @conj try @conj // [ 1: @(simplify_int_implements_cast … Hsimpl_eq) | 2: @(simplify_int_success_lt … Hsimpl_eq) ] | 13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res try (@(SimOk ???) //) | 14: elim (type_eq_dec ty (Tint target_sz target_sg)) [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg) destruct [ 1,2: // | 3: @smaller_integer_val_identity ] | 2: #Hneq >(type_neq_not_identity … Hneq) %1 // destruct @(SimOk ???) // ] | 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq [ 1: (* Proving preservation of the semantics for expressions. *) cases Hexpr_sim [ 2: (* Case where the evaluation of e1 as an expression fails *) normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/ | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) #Hsim %1 * #val #trace normalize #Hstep cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ (load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val)) [ 1: lapply Hstep -Hstep cases (exec_expr ge en m e1) [ 1: * #val' #trace' normalize nodelta cases val' normalize nodelta [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq; normalize nodelta [ 1: #Heq destruct | 2: #val2 #Heq destruct @conj // ] ] | 2: normalize nodelta #errmesg #Hcontr destruct ] | 2: * #e1_ptr * #He1_eq_ptr #Hloadptr cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) ∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val)) [ 1: @(ex_intro … e1_ptr) @conj [ 1: @Hsim // | 2: // ] | 2: * #e2_ptr * #He2_exec #Hload_e2_ptr normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl ] ] ] | 2: (* Proving the preservation of the semantics for lvalues. *) cases Hexpr_sim [ 2: (* Case where the evaluation of e1 as an lvalue fails *) normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/ | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) #Hsim %1 * * #block #offset #trace normalize #Hstep cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset) [ 1: lapply Hstep -Hstep cases (exec_expr ge en m e1) [ 1: * #val' #trace' normalize nodelta cases val' normalize nodelta [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) destruct try @conj try @conj // ] | 2: normalize nodelta #errmesg #Hcontr destruct ] | 2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) ∧ pblock ptr1 = block ∧ poff ptr1 = offset) [ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim // | 2: * #e2_ptr * * #He2_exec #Hblock #Hoffset normalize >He2_exec normalize nodelta // ] ] ] ] | 16: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq [ 1: (* Proving preservation of the semantics for expressions. *) cases Hlvalue_sim [ 2: (* Case where the evaluation of e1 as an expression fails *) * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2 by ex_intro/ | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep cut (∃block,offset,r,ptype,pc. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧ (pointer_compat_dec block r = inl ?? pc) ∧ (ty = Tpointer r ptype) ∧ val = Vptr (mk_pointer r block pc offset)) [ 1: lapply Hstep -Hstep cases (exec_lvalue ge en m e1) [ 1: * * #block #offset #trace' normalize nodelta cases ty [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ] normalize nodelta try (#Heq destruct) @(ex_intro … block) @(ex_intro … offset) @(ex_intro … rg) @(ex_intro … ptr_ty) cases (pointer_compat_dec block rg) in Heq; normalize [ 2: #Hnotcompat #Hcontr destruct | 1: #compat #Heq @(ex_intro … compat) try @conj try @conj try @conj destruct // ] | 2: normalize nodelta #errmesg #Hcontr destruct ] | 2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta >Hptr_compat // ] ] | 2: (* Proving preservation of the semantics of lvalues. *) @SimFail /2 by ex_intro/ ] | 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq [ 1: whd in match (exec_expr ge en m (Expr ??)); whd in match (exec_expr ge en m (Expr ??)); cases Hexpr_sim [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e1) [ 2: #error #Hexec normalize nodelta @SimFail /2 by ex_intro/ | 1: * #val #trace #Hexec >(Hexec ? (refl ? (OK ? 〈val,trace〉))) normalize nodelta @SimOk #a >Htype_eq #H @H ] ] | 2: @SimFail /2 by ex_intro/ ] | 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq inversion (Hinv_lhs ge en m) [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true #Hinv Hdesired_lhs #Habsurd destruct | 2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_ inversion (Hinv_rhs ge en m) [ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_ Hdesired_rhs #Habsurd destruct | 2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_ @(Inv_coerce_ok ge en m … target_sz target_sg lhs_src_sz lhs_src_sg) [ 1: >Htype_lhs // | 2: // | 3: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); (* Tidy up the type equations *) >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Heq destruct lapply Hsmaller_rhs lapply Hsmaller_lhs generalize in match rhs_src_sz; #src_sz generalize in match rhs_src_sg; #src_sg -Hsmaller_lhs -Hsmaller_rhs -Htype_lhs -Htype_rhs -Hinv_lhs -Hinv_rhs >Htype_lhs1 >Htype_rhs1 -Htype_lhs1 -Htype_rhs1 (* Enumerate all the cases for the evaluation of the source expressions ... *) cases (exec_expr ge en m lhs); try // * #val_lhs #trace_lhs normalize nodelta cases (exec_expr ge en m rhs); try // * #val_rhs #trace_rhs normalize nodelta whd in match (m_bind ?????); (* specialize to the actual simplifiable operations. *) cases op in Hop_simplifiable_eq; [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_ [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m) | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ] cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m) [ 1,3: #_ #_ #_ normalize @I ] #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result))) #src_result_sz * #i1 * #i2 * * #Hval_lhs_eq #Hval_rhs_eq #Hsrc_result_eq whd in match (opt_to_res ???); whd in match (m_bind ?????); normalize nodelta >Hval_lhs_eq >Hval_rhs_eq #Hsmaller_rhs #Hsmaller_lhs whd #result_int #Hsrc_result >Hsrc_result in Hsrc_result_eq; #Hsrc_result_eq lapply (sym_eq ??? Hsrc_result_eq) -Hsrc_result_eq #Hsrc_result_eq cut (src_result_sz = src_sz) [ 1,3: destruct // ] #Hsz_eq lapply Hsmaller_lhs lapply Hsmaller_rhs cases (exec_expr ge en m lhs1) normalize nodelta [ 2,4: destruct #error normalize in ⊢ (% → ?); #H @(False_ind … (H i1 (refl ? (Vint src_sz i1)))) ] * #val_lhs1 #trace_lhs1 cases (exec_expr ge en m rhs1) [ 2,4: destruct #error #_ normalize in ⊢ (% → ?); #H @(False_ind … (H i2 (refl ? (Vint src_sz i2)))) ] * #val_rhs1 #trace_rhs1 whd in match (m_bind ?????); normalize nodelta [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m) lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ] cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m) [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?))) (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *) * [ 1,4: whd in ⊢ (? → % → ?); normalize nodelta #Habsurd #Hcounterexample elim (Hcounterexample i1 (refl ? (Vint src_sz i1))) #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd @(False_ind … (Habsurd I)) | 2,5: whd in ⊢ (? → ? → % → ?); normalize nodelta #Habsurd #_ #Hcounterexample elim (Hcounterexample i2 (refl ? (Vint src_sz i2))) #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd @(False_ind … (Habsurd I)) | 3,6: #dsz1 * #dsz2 * #j1 * #j2 * * #Hval_lhs1 #Hval_rhs1 #Hsz_neq whd in ⊢ (% → % → ?); normalize nodelta #Hsmaller_lhs #Hsmaller_rhs elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2))) #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_ destruct elim Hsz_neq #Habsurd @(Habsurd (refl ? target_sz)) ] | 2,4: destruct #result #Hinversion #_ #Hsmaller_lhs #Hsmaller_rhs normalize nodelta elim (Hinversion result (refl ? (Some ? result))) #result_sz * #lhs_int * #rhs_int * * #Hlhs1_eq #Hrhs1_eq #Hop_eq elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2))) #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_ destruct [ 1: %{(addition_n (bitsize_of_intsize target_sz) (cast_int_int src_sz src_sg target_sz i1) (cast_int_int src_sz src_sg target_sz i2))} try @conj try @conj try @conj // >integer_add_cast_le try // | 2: %{(subtraction (bitsize_of_intsize target_sz) (cast_int_int src_sz src_sg target_sz i1) (cast_int_int src_sz src_sg target_sz i2))} try @conj try @conj try @conj // >integer_sub_cast_le try // ] ] ] ] ] | 19,20,21,22: destruct %1 try @refl elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs [ 1,3,5,7: whd in match (exec_expr ????); whd in match (exec_expr ????); cases Hexpr_sim_lhs [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/ | *: cases (exec_expr ge en m lhs) [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/ | *: * #lval #ltrace #Hsim_lhs normalize nodelta cases Hexpr_sim_rhs [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/ | *: cases (exec_expr ge en m rhs) [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/ | *: * #rval #rtrace #Hsim_rhs whd in match (exec_expr ??? (Expr (Ebinop ???) ?)); >(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉))) >(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉))) normalize nodelta >Htype_eq_lhs >Htype_eq_rhs @SimOk * #val #trace #H @H ] ] ] ] | *: @SimFail /2 by refl, ex_intro/ ] (* Jump to the cast cases *) | 23,30,31,32,33,34,35,36: %1 try @refl [ 1,4,7,10,13,16,19,22: destruct // ] elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq (* exec_expr simulation *) [ 1,3,5,7,9,11,13,15: cases Hexec_sim [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail @SimFail whd in match (exec_expr ge en m ?); >Hexec_fail /2 by refl, ex_intro/ | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace Hdesc_eq whd in match (exec_expr ge en m ?); #Hstep cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉 ∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val) [ 1,3,5,7,9,11,13,15: lapply Hstep -Hstep cases (exec_expr ge en m castee) [ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct | 1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta #Hstep @(ex_intro … val1) cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep; [ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct | 1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct @conj @refl ] ] | 2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast whd in match (exec_expr ge en m ?); >(Hsim … Hexec_expr ) normalize nodelta Hexec_cast // ] ] | 2,4,6,8,10,12,14,16: destruct @SimFail /2 by refl, ex_intro/ ] | 24: destruct inversion (Hcastee_inv ge en m) [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2 Htype_castee (* Simplify the goal by culling impossible cases, using Hsmaller_val *) cases (exec_expr ge en m castee) in Hsmaller_eval; [ 2: #error // | 1: * #castee_val #castee_trace #Hsmaller normalize nodelta lapply (exec_cast_inv castee_val src_sz src_sg cast_sz cast_sg m) cases (exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) [ 2: #error #_ @I | 1: #result #Hinversion elim (Hinversion result (refl ? (OK ? result))) #castee_int * #Hcastee_val_eq #Hresult_eq whd in match (m_bind ?????); #result_int #Hresult_eq2 cases (exec_expr ge en m castee1) in Hsmaller; [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd castee_int Hcastee_val_eq)) | 1: * #val1 #trace1 whd in ⊢ (% → ?); normalize nodelta #Hsmaller elim (Hsmaller castee_int Hcastee_val_eq) #val1_int * * * #Hval1_eq #Hval1_int_eq #Hcastee_trace_eq destruct #Hle %{(cast_int_int src_sz src_sg target_sz castee_int)} try @conj try @conj try @conj try // [ 1: @cast_composition ] try assumption elim (necessary_conditions_spec … (sym_eq … Hconditions)) [ 2,4: * #Heq >Heq #_ elim target_sz // | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ] ] ] ] ] ] | 25,27: destruct inversion (Hcast2 ge en m) [ 1,3: (* Impossible case. *) #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr Htype_castee2 // | 2,5: (* Prove simulation for exec_expr *) whd in match (exec_expr ??? (Expr ??)); cases (exec_expr ge en m castee) in Hsmaller_eval; [ 2,4: (* erroneous evaluation of the original expression *) #error #Hsmaller_eval @SimFail @(ex_intro … error) // | 1,3: * #val #trace normalize nodelta >Htype_castee lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) [ 2,4: #error #_ #_ @SimFail /2 by ex_intro/ | 1,3: #result #Hinversion elim (Hinversion result (refl ??)) #val_int * #Hval_eq #Hresult_eq cases (exec_expr ge en m castee2) [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … (Hsmaller_eval val_int Hval_eq)) | 1,3: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq) #val1_int * * * #Hval1_eq #Hcast_eq #Htrace_eq #Hle destruct @SimOk normalize #a #H @H ] ] ] | 3,6: @SimFail /2 by refl, ex_intro/ ] ] | 26,28: destruct inversion (Hcast2 ge en m) [ 2,4: (* Impossible case. *) #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq (* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *) letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq -Habsurd_eq -Habsurd #Habsurd destruct | 1,3: (* All our attempts at casting down the expression have failed. We still use the resulting expression, as we may have discovered and simplified unrelated casts. *) #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv @(Inv_eq ???????) // [ 1,3: (* Simulation for exec_expr *) whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim_expr [ 2,4: * #error #Hexec_err >Hexec_err @SimFail @(ex_intro … error) // | 1,3: #Hexec_ok cases (exec_expr ge en m castee) in Hexec_ok; [ 2,4: #error #Hsim @SimFail normalize nodelta /2/ | 1,3: * #val #trace #Hsim normalize nodelta >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta @SimOk #a #H @H ] ] | 2,4: @SimFail /2 by refl, ex_intro/ ] ] | 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq @(Inv_eq ???????) // whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); [ 1: cases Hsim_expr [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/ | 1: #Hexec_ok @SimOk * #val #trace cases (exec_expr ge en m castee) in Hexec_ok; [ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct | 1: * #val #trace #Hexec_ok normalize nodelta >(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉))) >Htype_eq normalize nodelta #H @H ] ] | 2: @SimFail /2 by refl, ex_intro/ ] | 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq inversion (Htrue_inv ge en m) [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false #Hinv Hdesired_true #Habsurd destruct | 2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true inversion (Hfalse_inv ge en m) [ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false #Hinv Hdesired_false #Habsurd destruct | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg) [ 1,2: // | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??)); elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq cases Hexec_cond_sim [ 2: * #error #Herror >Herror normalize @I | 1: cases (exec_expr ge en m cond) [ 2: #error #_ normalize @I | 1: * #cond_val #cond_trace #Hcond_sim >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) normalize nodelta >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1)) * [ 3,4: normalize // | 1,2: normalize in match (m_bind ?????); normalize in match (m_bind ?????); -Hexec_cond_sim -Hcond_sim -cond_val [ 1: (* true branch taken *) cases (exec_expr ge en m iftrue) in Hsmaller_true; [ 2: #error #_ @I | 1: * #val_true_branch #trace_true_branch #Hsmaller #val_true_branch #Hval_true_branch lapply Hsmaller -Hsmaller cases (exec_expr ge en m iftrue1) [ 2: #error normalize in ⊢ (% → ?); #Hsmaller @(False_ind … (Hsmaller val_true_branch Hval_true_branch)) | 1: * #val_true1_branch #trace_true1_branch #Hsmaller normalize nodelta elim (Hsmaller val_true_branch Hval_true_branch) #val_true1_int * * * #val_true1_branch #Hval_cast_eq #Htrace_eq #Hle %{val_true1_int} try @conj try @conj try @conj // ] ] | 2: (* false branch taken. Same proof as above, different arguments ... *) cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg) [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq destruct (Htype_eq) @conj @refl ] * #Hsz_eq #Hsg_eq destruct cases (exec_expr ge en m iffalse) in Hsmaller_false; [ 2: #error #_ @I | 1: destruct * #val_false_branch #trace_false_branch #Hsmaller #val_false_branch #Hval_false_branch lapply Hsmaller -Hsmaller cases (exec_expr ge en m iffalse1) [ 2: #error normalize in ⊢ (% → ?); #Hsmaller @(False_ind … (Hsmaller val_false_branch Hval_false_branch)) | 1: * #val_false1_branch #trace_false1_branch #Hsmaller normalize nodelta elim (Hsmaller val_false_branch Hval_false_branch) #val_false1_int * * * #val_false1_branch #Hval_cast_eq #Htrace_eq #Hle %{val_false1_int} try @conj try @conj try @conj // ] ] ] ] ] ] ] ] ] | 38,39,40: destruct elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq %1 try @refl [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases (exec_expr ge en m cond) in Hsim_expr_cond; [ 2,4,6: #error #_ @SimFail /2 by ex_intro/ | 1,3,5: * #cond_val #cond_trace normalize nodelta cases (exec_expr ge en m cond1) [ 2,4,6: #error * [ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) #Habsurd destruct | *: * #error #Habsurd destruct ] | 1,3,5: * #cond_val1 #cond_trace1 * [ 2,4,6: * #error #Habsurd destruct | 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) #Hcond_eq normalize nodelta destruct (Hcond_eq) >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1)) [ 2,4,6: #error @SimFail normalize /2 by refl, ex_intro / | 1,3,5: * (* true branch *) [ 1,3,5: normalize in match (m_bind ?????); normalize in match (m_bind ?????); cases Hsim_expr_true [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/ | 1,3,5: cases (exec_expr ge en m iftrue) [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/ | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉))) normalize nodelta @SimOk #a #H @H ] ] | 2,4,6: normalize in match (m_bind ?????); normalize in match (m_bind ?????); cases Hsim_expr_false [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/ | 1,3,5: cases (exec_expr ge en m iffalse) [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/ | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉))) normalize nodelta @SimOk #a #H @H ] ] ] ] ] ] ] | 2,4,6: @SimFail /2 by ex_intro/ ] | 41,42: destruct elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs %1 try @refl [ 1,3: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim_expr_lhs [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/ | 1,3: cases (exec_expr ge en m lhs) [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/ | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉))) normalize nodelta >Htype_eq_lhs cases (exec_bool_of_val lhs_val (typeof lhs1)) [ 2,4: #error normalize @SimFail /2 by refl, ex_intro/ | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); [ 2,3: (* lhs evaluates to true *) @SimOk #a #H @H | 1,4: cases Hsim_expr_rhs [ 2,4: * #error #Hexec >Hexec @SimFail /2 by refl, ex_intro/ | 1,3: cases (exec_expr ge en m rhs) [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/ | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉))) normalize nodelta >Htype_eq_rhs @SimOk #a #H @H ] ] ] ] ] ] | 2,4: @SimFail /2 by ex_intro/ ] | 43: destruct cases (type_eq_dec ty (Tint target_sz target_sg)) [ 1: #Htype_eq >Htype_eq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg) [ 1,2: // | 3: @smaller_integer_val_identity ] | 2: #Hneq >(type_neq_not_identity … Hneq) %1 // @SimOk #a #H @H ] | 44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq %1 try @refl [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); whd in match (exec_lvalue ????) in Hsim_lvalue; whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); >Htype_eq cases (typeof rec_expr1) normalize nodelta [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ] [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/ | 6,7: cases Hsim_lvalue [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/ | 1,3: cases (exec_lvalue ge en m rec_expr) [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/ | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) whd in match (m_bind ?????); @SimOk #a #H @H ] ] ] | 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??)); >Htype_eq cases (typeof rec_expr1) normalize nodelta [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ] [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/ | 6,7: cases Hsim_lvalue [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/ | 1,3: cases (exec_lvalue ge en m rec_expr) [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/ | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) whd in match (m_bind ?????); @SimOk #a #H @H ] ] ] ] | 45: destruct inversion (Hinv ge en m) [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_ @(Inv_coerce_ok ??????? src_sz src_sg) [ 1: >Htypeof_e1 // | 2: >Htypeof_e2 // | 3: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases (exec_expr ge en m e1) in Hsmaller; [ 2: #error normalize // | 1: * #val1 #trace1 #Hsmaller #val1_int #Hval1_eq cases (exec_expr ge en m e2) in Hsmaller; [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd val1_int Hval1_eq)) | 1: * #val2 #trace #Hsmaller elim (Hsmaller val1_int Hval1_eq) #val2_int * * * #Hval2_eq #Hcast #Htrace #Hle normalize nodelta %{val2_int} try @conj try @conj try @conj // ] ] ] | 1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_ >Hresult %1 try @refl [ 1: >Htype_eq // | 2: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim_expr [ 2: * #error #Hexec_error >Hexec_error @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e1) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec @SimOk #a #H @H ] ] | 3: @SimFail /2 by ex_intro/ ] ] | 46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq %1 try @refl [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim_expr [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e1) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ] ] | 2: @SimFail /2 by ex_intro/ ] (* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls * simplify_expr *) | 47, 48, 49: (* trivial const_int, const_float and var cases *) try @conj try @conj try @refl @SimOk #a #H @H | 50: (* Deref case *) destruct elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq try @conj try @conj [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); | 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??)); ] [ 1,2: cases Hsim_expr [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1,3: cases (exec_expr ge en m e1) [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] | 3: // ] | 51: (* Addrof *) destruct elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq try @conj try @conj [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim_lvalue [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ | 1: cases (exec_lvalue ge en m e1) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] | 2: @SimFail /2 by ex_intro/ | 3: // ] | 52: (* Unop *) destruct elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq try @conj try @conj [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim_expr [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e1) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk >Htype_eq #a #H @H ] ] | 2: @SimFail /2 by ex_intro/ | 3: // ] | 53: (* Binop *) destruct elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs try @conj try @conj [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim_expr_lhs [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m lhs) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m rhs) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #rhs_value #Hsim_rhs lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value))) lapply (Hsim_rhs rhs_value (refl ? (OK ? rhs_value))) #Hrhs >Hrhs #Hlhs >Hlhs >Htype_eq_rhs >Htype_eq_lhs @SimOk #a #H @H ] ] ] ] | 2: @SimFail /2 by ex_intro/ | 3: // ] | 54: (* Cast, fallback case *) try @conj try @conj try @refl @SimOk #a #H @H | 55: (* Cast, success case *) destruct inversion (Htrans_inv ge en m) [ 1: (* contradiction *) #result_flag #Hresult_flag #Htype_eq #Hsim_epr #Hsim_lvalue #Hresult_flag_true Hsrc_type_eq lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) cases (exec_cast m val ??) [ 2: #error #_ #_ @SimFail /2 by ex_intro/ | 1: #result #Hinversion elim (Hinversion result (refl ??)) #val_int * #Hval_eq #Hcast cases (exec_expr ge en m castee1) [ 2: #error #Habsurd normalize in Habsurd; @(False_ind … (Habsurd val_int Hval_eq)) | 1: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq) #val1_int * * * #Hval1_int #Hval18int #Htrace #Hle @SimOk destruct normalize // ] ] ] | 2: @SimFail /2 by ex_intro/ | 3: >Htarget_type_eq // ] ] | 56: (* Cast, "failure" case *) destruct inversion (Htrans_inv ge en m) [ 2: (* contradiction *) #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller #Habsurd lapply (jmeq_to_eq ??? Habsurd) -Habsurd #Herror destruct | 1: #result_flag #Hresult_flag #Htype_eq #Hsim_expr #Hsim_lvalue #_ #_ try @conj try @conj try @conj [ 1: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??)); cases Hsim_expr [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ??? castee) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok @SimOk >Htype_eq #a #H @H ] ] | 2: @SimFail /2 by ex_intro/ | 3: // ] ] | 57,58,59,60,61,62,63,64,68: try @conj try @conj try @refl @SimOk #a #H @H | 65: destruct elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true elim (Hequiv_iffalse ge en m) * #Hsim_exec_false #Hsim_lvalue_false #Htype_eq_false try @conj try @conj [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim_exec_cond [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ??? cond) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉))) #Hcond_ok >Hcond_ok >Htype_eq_cond normalize nodelta cases (exec_bool_of_val condb (typeof cond1)) [ 2: #error @SimFail /2 by ex_intro/ | 1: * whd in match (m_bind ?????); whd in match (m_bind ?????); normalize nodelta [ 1: (* true branch taken *) cases Hsim_exec_true [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ??? iftrue) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] | 2: (* false branch taken *) cases Hsim_exec_false [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ??? iffalse) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] ] ] ] ] | 2: @SimFail /2 by ex_intro/ | 3: // ] | 66,67: destruct elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs try @conj try @conj whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); [ 1,4: cases Hsim_exec_lhs [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1,3: cases (exec_expr ??? lhs) [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs normalize nodelta elim a #lhs_val #lhs_trace cases (exec_bool_of_val lhs_val (typeof lhs1)) [ 2,4: #error @SimFail /2 by ex_intro/ | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); [ 2,3: @SimOk // | 1,4: cases Hsim_exec_rhs [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ | 1,3: cases (exec_expr ??? rhs) [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs @SimOk #a #H @H ] ] ] ] ] ] | 2,5: @SimFail /2 by ex_intro/ | 3,6: // ] | 69: (* record field *) destruct elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq try @conj try @conj whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); whd in match (exec_lvalue' ??? (Efield rec_expr f) ty); whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty' | 7: #id #fl | 8: #id #fl | 9: #rg #id ] try (@SimFail /2 by ex_intro/) cases Hsim_lvalue [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ | 1,3: cases (exec_lvalue ge en m rec_expr) [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec @SimOk #a #H @H ] ] | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *) >Htype_eq cases (typeof rec_expr1) normalize nodelta [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty' | 7: #id #fl | 8: #id #fl | 9: #rg #id ] try (@SimFail /2 by ex_intro/) cases Hsim_lvalue [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ | 1,3: cases (exec_lvalue ge en m rec_expr) [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec @SimOk #a #H @H ] ] | 3: // ] | 70: (* cost label *) destruct elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq try @conj try @conj whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); [ 1: cases Hsim_expr [ 2: * #error #Hexec >Hexec @SimFail /2 by ex_intro/ | 1: cases (exec_expr ??? e1) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] | 2: @SimFail /2 by ex_intro/ | 3: // ] ] qed. (* Propagate cast simplification through statements and programs. *) definition simplify_e ≝ λe. pi1 … (simplify_inside e). let rec simplify_statement (s:statement) : statement ≝ match s with [ Sskip ⇒ Sskip | Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2) | Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es) | Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2) | Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *) | Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) | Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) | Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *) | Sbreak ⇒ Sbreak | Scontinue ⇒ Scontinue | Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo) | Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls) | Slabel l s1 ⇒ Slabel l (simplify_statement s1) | Sgoto l ⇒ Sgoto l | Scost l s1 ⇒ Scost l (simplify_statement s1) ] and simplify_ls ls ≝ match ls with [ LSdefault s ⇒ LSdefault (simplify_statement s) | LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls') ]. definition simplify_function : function → function ≝ λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)). definition simplify_fundef : clight_fundef → clight_fundef ≝ λf. match f with [ CL_Internal f ⇒ CL_Internal (simplify_function f) | _ ⇒ f ]. definition simplify_program : clight_program → clight_program ≝ λp. transform_program … p simplify_fundef. (* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *) inductive cont_cast : cont → cont → Prop ≝ | cc_stop : cont_cast Kstop Kstop | cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k') | cc_while : ∀e,s,k,k'. cont_cast k k' → cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') | cc_dowhile : ∀e,s,k,k'. cont_cast k k' → cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') | cc_for1 : ∀e,s1,s2,k,k'. cont_cast k k' → cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k') | cc_for2 : ∀e,s1,s2,k,k'. cont_cast k k' → cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k') | cc_for3 : ∀e,s1,s2,k,k'. cont_cast k k' → cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k') | cc_switch : ∀k,k'. cont_cast k k' → cont_cast (Kswitch k) (Kswitch k') | cc_call : ∀r,f,en,k,k'. cont_cast k k' → cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k'). lemma call_cont_cast : ∀k,k'. cont_cast k k' → cont_cast (call_cont k) (call_cont k'). #k0 #k0' #K elim K /2/ qed. inductive state_cast : state → state → Prop ≝ | swc_state : ∀f,s,k,k',e,m. cont_cast k k' → state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m) | swc_callstate : ∀fd,args,k,k',m. cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m) | swc_returnstate : ∀res,k,k',m. cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m) | swc_finalstate : ∀r. state_cast (Finalstate r) (Finalstate r) . record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { rg_find_symbol: ∀s. find_symbol ? ge s = find_symbol ? ge' s; rg_find_funct: ∀v,f. find_funct ? ge v = Some ? f → find_funct ? ge' v = Some ? (t f); rg_find_funct_ptr: ∀b,f. find_funct_ptr ? ge b = Some ? f → find_funct_ptr ? ge' b = Some ? (t f) }. (* The return type of any function is invariant under cast simplification *) lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f. // qed. definition expr_lvalue_ind_combined ≝ λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. conj ?? (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2. #A #r0 #r1 #r2 * [ 2: * #error #H >H #_ @SimFail /2 by ex_intro/ | 1: cases r0 [ 2: #error #_ #_ @SimFail /2 by ex_intro/ | 1: #elt #Hsim lapply (Hsim elt (refl ? (OK ? elt))) #H >H // ] ] qed. lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → (∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ (∀ed, ty. simulate ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). #ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined [ 1: #sz #ty #i @SimOk #a normalize // | 2: #ty #f @SimOk #a normalize // | 3: * [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] #ty #Hsim_lvalue try // whd in match (Plvalue ???); whd in match (exec_expr ????); whd in match (exec_expr ????); cases Hsim_lvalue [ 2,4,6: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ | *: cases (exec_lvalue' ge en m ? ty) [ 2,4,6: #error #_ @SimFail /2 by ex_intro/ | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] | 4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); cases (lookup SymbolTag block en v) normalize nodelta [ 2: #block @SimOk // | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk // ] | 5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); cases Hsim_expr [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] | 6: #ty #ed #ty' #Hsim_lvalue whd in match (exec_expr ????); whd in match (exec_expr ????); whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); cases Hsim_lvalue [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ | 1: cases (exec_lvalue' ge en m ed ty') [ 2: #error #_ @SimFail /2 by ex_intro/ | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] | 7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim1 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e1) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite cases Hsim2 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e2) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] ] ] | 9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] (* mergeable with 7 modulo intros *) | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim1 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e1) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta cases (exec_bool_of_val (\fst a) (typeof e1)) [ 2: #error @SimFail /2 by ex_intro/ | 1: * [ 1: (* true branch *) cases Hsim2 | 2: (* false branch *) cases Hsim3 ] [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e2) | 3: cases (exec_expr ge en m e3) ] [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] ] ] | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim1 [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1,3: cases (exec_expr ge en m e1) [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta cases (exec_bool_of_val ??) [ 2,4: #erro @SimFail /2 by ex_intro/ | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); [ 2,3: @SimOk // | 1,4: cases Hsim2 [ 2,4: * #error #Hfail >Hfail normalize nodelta @SimFail /2 by ex_intro/ | 1,3: cases (exec_expr ge en m e2) [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] ] ] ] ] | 13: #ty #sizeof_ty @SimOk normalize // | 14: #ty #e #ty' #field #Hsim_lvalue whd in match (exec_lvalue' ? en m (Efield ??) ty); whd in match (exec_lvalue' ge' en m (Efield ??) ty); normalize in match (typeof (Expr ??)); cases ty' in Hsim_lvalue; normalize nodelta [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ] #Hsim_lvalue try (@SimFail /2 by ex_intro/) normalize in match (exec_lvalue ge en m ?); normalize in match (exec_lvalue ge' en m ?); cases Hsim_lvalue [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1,3: cases (exec_lvalue' ge en m e ?) [ 2,4: #error #_ @SimFail /2 by ex_intro/ | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk /2 by ex_intro/ ] ] | 15: #ty #lab #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); cases Hsim [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ | 1: cases (exec_expr ge en m e) [ 2: #error #_ @SimFail /2 by ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] ] (* cf case 7, again *) | 16: * [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] #ty normalize in match (is_not_lvalue ?); [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_ @SimFail /2 by ex_intro/ ] qed. lemma related_globals_expr_simulation : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → ∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧ typeof e = typeof (simplify_e e). #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); cases e #ed #ty cases ed [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) * * try // cases (exec_expr ge en m (Expr ??)) try (#error #_ #_ #_ @SimFail /2 by ex_intro/) * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?)) qed. lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → ∀e. simulate ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧ typeof e = typeof (simplify_e e). #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); cases e #ed #ty cases ed [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) * * try // cases (exec_lvalue ge en m (Expr ??)) try (#error #_ #_ #_ @SimFail /2 by ex_intro/) * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq (* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *) cases e' in Hsim_lvalue ⊢ %; #ed' #ty' whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); lapply (proj2 ?? (sim_related_globals ge ge' en m Hrelated) ed' ty') #Hsim_lvalue2 #Hsim_lvalue1 try @(simulation_transitive ???? Hsim_lvalue1 Hsim_lvalue2) qed. lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → ∀args. simulate ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)). #ge #ge' #en #m #Hrelated #args elim args [ 1: /3/ | 2: #hd #tl #Hind normalize elim (related_globals_expr_simulation ge ge' en m Hrelated hd) * [ 2: * #error #Hfail >Hfail #_ @SimFail /2 by refl, ex_intro/ | 1: cases (exec_expr ge en m hd) [ 2: #error #_ #_ @SimFail /2 by refl, ex_intro/ | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq cases Hind normalize [ 2: * #error #Hfail >Hfail @SimFail /2 by refl, ex_intro/ | 1: cases (exec_exprlist ??? tl) [ 2: #error #_ @SimFail /2 by refl, ex_intro/ | 1: * #values #trace #Hsim lapply (Hsim 〈values, trace〉 (refl ? (OK ? 〈values, trace〉))) #Heq >Heq @SimOk // ] ] ] ] ] qed. lemma simplify_type_of_fundef_eq : ∀clfd. (type_of_fundef (simplify_fundef clfd)) = (type_of_fundef clfd). * // qed. lemma simplify_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. typeof (simplify_e func) = typeof func. #ge #en #m #func whd in match (simplify_e func); elim (simplify_inside func) #func' #H lapply (H ge en m) * * #_ #_ // qed. lemma simplify_fun_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. fun_typeof (simplify_e func) = fun_typeof func. #ge #en #m #func whd in match (simplify_e func); whd in match (fun_typeof ?) in ⊢ (??%%); >simplify_typeof_eq whd in match (simplify_e func); // qed. lemma simplify_is_not_skip: ∀s.s ≠ Sskip → ∃pf. is_Sskip (simplify_statement s) = inr … pf. * [ 1: * #Habsurd elim (Habsurd (refl ? Sskip)) | *: #a try #b try #c try #d try #e whd in match (simplify_statement ?); whd in match (is_Sskip ?); try /2 by refl, ex_intro/ ] qed. lemma call_cont_simplify : ∀k,k'. cont_cast k k' → cont_cast (call_cont k) (call_cont k'). #k0 #k0' #K elim K /2/ qed. lemma simplify_ls_commute : ∀l. (simplify_statement (seq_of_labeled_statement l)) = (seq_of_labeled_statement (simplify_ls l)). #l @(labeled_statements_ind … l) [ 1: #default_statement // | 2: #sz #i #s #tl #Hind whd in match (seq_of_labeled_statement ?) in ⊢ (??%?); whd in match (simplify_ls ?) in ⊢ (???%); whd in match (seq_of_labeled_statement ?) in ⊢ (???%); whd in match (simplify_statement ?) in ⊢ (??%?); >Hind // ] qed. lemma select_switch_commute : ∀sz,i,l. select_switch sz i (simplify_ls l) = simplify_ls (select_switch sz i l). #sz #i #l @(labeled_statements_ind … l) [ 1: #default_statement // | 2: #sz' #i' #s #tl #Hind whd in match (simplify_ls ?) in ⊢ (??%?); whd in match (select_switch ???) in ⊢ (??%%); cases (sz_eq_dec sz sz') [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta whd in match (simplify_ls ?) in ⊢ (???%); [ 1: // | 2: @Hind ] | 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq) @Hind ] ] qed. lemma elim_IH_aux : ∀lab. ∀s:statement.∀k,k'. cont_cast k k' → ∀Hind:(∀k:cont.∀k':cont. cont_cast k k' → match find_label lab s k with  [ None ⇒ find_label lab (simplify_statement s) k'=None (statement×cont) | Some (r:(statement×cont))⇒ let 〈s',ks〉 ≝r in  ∃ks':cont. find_label lab (simplify_statement s) k' = Some (statement×cont) 〈simplify_statement s',ks'〉 ∧ cont_cast ks ks']). (find_label lab s k = None ? ∧ find_label lab (simplify_statement s) k' = None ?) ∨ (∃st,kst,kst'. find_label lab s k = Some ? 〈st,kst〉 ∧ find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement st,kst'〉 ∧ cont_cast kst kst'). #lab #s #k #k' #Hcont_cast #Hind lapply (Hind k k' Hcont_cast) cases (find_label lab s k) [ 1: normalize nodelta #Heq >Heq /3/ | 2: * #st #kst normalize nodelta * #kst' * #Heq #Hcont_cast' >Heq %2 %{st} %{kst} %{kst'} @conj try @conj // ] qed. lemma cast_find_label : ∀lab,s,k,k'. cont_cast k k' → match find_label lab s k with [ Some r ⇒ let 〈s',ks〉 ≝ r in ∃ks'. find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement s', ks'〉 ∧ cont_cast ks ks' | None ⇒ find_label lab (simplify_statement s) k' = None ? ]. #lab #s @(statement_ind2 ? (λls. ∀k:cont .∀k':cont .cont_cast k k' →match find_label_ls lab ls k with  [None⇒ find_label_ls lab (simplify_ls ls) k' = None ? |Some r ⇒ let 〈s',ks〉 ≝r in  ∃ks':cont .find_label_ls lab (simplify_ls ls) k' =Some (statement×cont) 〈simplify_statement s',ks'〉 ∧cont_cast ks ks'] ) … s) [ 1: #k #k' #Hcont_cast whd in match (find_label ? Sskip ?); normalize nodelta @refl | 2: #e1 #e2 #k #k' #Hcont_cast whd in match (find_label ? (Sassign e1 e2) ?); normalize nodelta @refl | 3: #e0 #e #args #k #k' #Hcont_cast whd in match (find_label ? (Scall e0 e args) ?); normalize nodelta @refl | 4: #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast whd in match (find_label ? (Ssequence s1 s2) ?); whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?); elim (elim_IH_aux lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1) [ 3: try ( @cc_seq // ) | 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2) [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // ] ] | 5: #e #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast whd in match (find_label ???); whd in match (find_label ? (simplify_statement ?) ?); elim (elim_IH_aux lab s1 k k' Hcont_cast Hind_s1) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2) [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // ] ] | 6: #e #s #Hind_s #k #k' #Hcont_cast whd in match (find_label ???); whd in match (find_label ? (simplify_statement ?) ?); elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // | 3: @cc_while // ] | 7: #e #s #Hind_s #k #k' #Hcont_cast whd in match (find_label ???); whd in match (find_label ? (simplify_statement ?) ?); elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // | 3: @cc_dowhile // ] | 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast whd in match (find_label ???); whd in match (find_label ? (simplify_statement ?) ?); elim (elim_IH_aux lab s1 (Kseq (Sfor Sskip cond s2 s3) k) (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k') ? Hind_s1) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 3: @cc_for1 // | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta elim (elim_IH_aux lab s3 (Kfor2 cond s2 s3 k) (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') ? Hind_s3) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 3: @cc_for2 // | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta elim (elim_IH_aux lab s2 (Kfor3 cond s2 s3 k) (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') ? Hind_s2) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 3: @cc_for3 // | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // ] ] ] | 9,10: #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta // | 11: #e #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta // | 12: #e #ls #Hind #k #k' #Hcont_cast whd in match (find_label ???); whd in match (find_label ? (simplify_statement ?) ?); (* We can't elim the Hind on a list of labeled statements. We must proceed more manually. *) lapply (Hind (Kswitch k) (Kswitch k') ?) [ 1: @cc_switch // | 2: cases (find_label_ls lab ls (Kswitch k)) normalize nodelta [ 1: // | 2: * #st #kst normalize nodelta // ] ] | 13: #lab' #s0 #Hind #k #k' #Hcont_cast whd in match (find_label ???); whd in match (find_label ? (simplify_statement ?) ?); cases (ident_eq lab lab') normalize nodelta [ 1: #_ %{k'} /2/ | 2: #_ elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] ] | 14: #l #k #k' #Hcont_cast // | 15: #l #s0 #Hind #k #k' #Hcont_cast whd in match (find_label ???); whd in match (find_label ? (simplify_statement ?) ?); elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] | 16: #s0 #Hind #k #k' #Hcont_cast whd in match (find_label ???); whd in match (find_label ? (simplify_statement ?) ?); elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' normalize nodelta %{kst'} /2/ | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] | 17: #sz #i #s0 #t #Hind_s0 #Hind_ls #k #k' #Hcont_cast whd in match (simplify_ls ?); whd in match (find_label_ls ???); lapply Hind_ls @(labeled_statements_ind … t) [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?); elim (elim_IH_aux lab s0 (Kseq default_case k) (Kseq (simplify_statement default_case) k') ? Hind_s0) [ 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast' >Hrewrite >Hrewrite1 normalize nodelta whd in match (find_label_ls ???); >Hrewrite >Hrewrite1 normalize nodelta %{kst'} /2/ | 3: @cc_seq // | 1: * #Hrewrite #Hrewrite1 >Hrewrite normalize nodelta lapply (Hind_ls k k' Hcont_cast) cases (find_label_ls lab (LSdefault default_case) k) [ 1: normalize nodelta #Heq1 whd in match (simplify_ls ?); whd in match (find_label_ls lab ??); whd in match (seq_of_labeled_statement ?); whd in match (find_label_ls lab ??); >Hrewrite1 normalize nodelta @Heq1 | 2: * #st #kst normalize nodelta #H whd in match (find_label_ls lab ??); whd in match (simplify_ls ?); whd in match (seq_of_labeled_statement ?); >Hrewrite1 normalize nodelta @H ] ] | 2: #sz' #i' #s' #tl' #Hind #A whd in match (seq_of_labeled_statement ?); elim (elim_IH_aux lab s0 (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k) (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k') ? Hind_s0) [ 3: @cc_seq // | 1: * #Heq #Heq2 >Heq >Heq2 normalize nodelta lapply (A k k' Hcont_cast) cases (find_label_ls lab (LScase sz' i' s' tl') k) normalize nodelta [ 1: #H whd in match (find_label_ls ???); Heq2 normalize nodelta assumption | 2: * #st #kst normalize nodelta #H whd in match (find_label_ls ???); Heq2 normalize nodelta @H ] | 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast' >Hrewrite normalize nodelta %{kst'} @conj try // whd in match (find_label_ls ???); Hrewrite1 // ] ] ] qed. lemma cast_find_label_fn : ∀lab,f,k,k',s,ks. cont_cast k k' → find_label lab (fn_body f) k = Some ? 〈s,ks〉 → ∃ks'. find_label lab (fn_body (simplify_function f)) k' = Some ? 〈simplify_statement s,ks'〉 ∧ cont_cast ks ks'. #lab * #rettype #args #vars #body #k #k' #s #ks #Hcont_cast #Hfind_lab whd in match (simplify_function ?); lapply (cast_find_label lab body ?? Hcont_cast) >Hfind_lab normalize nodelta // qed. theorem cast_correction : ∀ge, ge'. related_globals ? simplify_fundef ge ge' → ∀s1, s1', tr, s2. state_cast s1 s1' → exec_step ge s1 = Value … 〈tr,s2〉 → ∃s2'. exec_step ge' s1' = Value … 〈tr,s2'〉 ∧ state_cast s2 s2'. #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hs1_sim_s1' #Houtcome inversion Hs1_sim_s1' [ 1: (* regular state *) #f #stm #k #k' #en #m #Hcont_cast lapply (related_globals_expr_simulation ge ge' en m Hrelated) #Hsim_related lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related cases stm (* Perform the intros for the statements*) [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body | 14: #lab | 15: #cost #body ] [ 1: (* Skip *) #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 whd in match (exec_step ??); whd in match (exec_step ??); inversion Hcont_cast [ 1: (* Kstop *) #Hk #Hk' #_ >fn_return_simplify cases (fn_return f) normalize nodelta [ 1: >Heq_s1 in Hs1_sim_s1'; >Heq_s1' #Hsim inversion Hsim [ 1: #f0 #s #k0 #k0' #e #m0 #Hcont_cast0 #Hstate_eq #Hstate_eq' #_ #Eq whd in match (ret ??) in Eq; destruct (Eq) %{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj [ 1: // | 2: %3 %1 ] | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd) | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd) | 4: #r #Habsurd destruct (Habsurd) ] | 3: #irrelevant #Habsurd destruct | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct | *: #irrelevant1 #irrelevant2 #Habsurd destruct ] | 2: (* Kseq stm' k' *) #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq whd in match (ret ??) in Eq; destruct (Eq) %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj [ 1: // | 2: %1 // ] | 3: (* Kwhile *) #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq whd in match (ret ??) in Eq; destruct (Eq) %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj [ 1: // | 2: %1 // ] | 4: (* Kdowhile *) #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct | 1: cases (exec_expr ge en m cond) in Eq; [ 2: #error whd in match (m_bind ?????) in ⊢ (% → ?); #Habsurd destruct | 1: * #val #trace whd in match (m_bind ?????) in ⊢ (% → ?); Hrewrite_cond whd in match (m_bind ?????); (* case analysis on the outcome of the conditional *) cases (exec_bool_of_val val (typeof cond)) in Eq ⊢ %; [ 2: (* evaluation of the conditional fails *) #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????); #Eq destruct (Eq) [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj [ 1: // | 2: %1 // ] | 2: %{(State (simplify_function f) Sskip k0' en m)} @conj [ 1: // | 2: %1 // ] ] ] ] ] | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq) [ 1: %{(State (simplify_function f) (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k0' en m)} @conj [ 1: // | 2: %1 // ] | 2: %{(State (simplify_function f) (simplify_statement step) (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj [ 1: // | 2: %1 @cc_for3 // ] | 3: %{(State (simplify_function f) (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k0' en m)} @conj [ 1: // | 2: %1 // ] ] | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq) %{(State (simplify_function f) Sskip k0' en m)} @conj [ 1: // | 2: %1 // ] | 9: (* Call *) #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ #Eq >fn_return_simplify cases (fn_return f) in Eq; normalize nodelta [ 1: #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq) %{(Returnstate Vundef (Kcall r (simplify_function f0) en0 k0') (free_list m (blocks_of_env en)))} @conj [ 1: // | 2: %3 @cc_call // ] | 3: #irrelevant #Habsurd destruct (Habsurd) | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct (Habsurd) | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ] ] | 2: (* Assign *) #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 whd in match (simplify_statement ?); #Heq whd in match (exec_step ??) in Heq ⊢ %; (* Begin by making the simplify_e disappear using Hsim_related *) elim (Hsim_lvalue_related lhs) * [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_lvalue ge en m lhs) in Heq; [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: * * #block #offset #trace whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_lhs lapply (Hsim 〈block, offset, trace〉 (refl ? (OK ? 〈block, offset, trace〉))) #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????); (* After [lhs], treat [rhs] *) elim (Hsim_related rhs) * [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_expr ge en m rhs) in Heq; [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: * #val #trace whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_rhs lapply (Hsim 〈val, trace〉 (refl ? (OK ? 〈val, trace〉))) #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????); Heq_s1 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; elim (Hsim_related func) in Heq; * [ 2: * #error #Hfail >Hfail #Htype_eq #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_expr ??? func) [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq whd in match (bindIO ??????) in ⊢ (% → %); elim (related_globals_exprlist_simulation ge ge' en m Hrelated args) [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_exprlist ge en m args) [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq whd in match (bindIO ??????) in ⊢ (% → %); elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a)) cases (find_funct clight_fundef ge (\fst a)); [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq whd in match (bindIO ??????) in ⊢ (% → %); >simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m) cases (assert_type_eq (type_of_fundef clfd) (fun_typeof func)) [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #Htype_eq cases ret [ 1: whd in match (bindIO ??????) in ⊢ (% → %); #Eq destruct (Eq) %{(Callstate (simplify_fundef clfd) (\fst  l) (Kcall (None (block×offset×type)) (simplify_function f) en k') m)} @conj [ 1: // | 2: %2 @cc_call // ] | 2: #fptr whd in match (bindIO ??????) in ⊢ (% → %); elim (Hsim_lvalue_related fptr) * [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_lvalue ge en m fptr) [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a))) whd in match (bindIO ??????) in ⊢ (% → %); #Heq destruct (Heq) %{(Callstate (simplify_fundef clfd) (\fst  l) (Kcall (Some (block×offset×type) 〈\fst  a,typeof (simplify_e fptr)〉) (simplify_function f) en k') m)} @conj [ 1: // | 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ] ] ] ] ] ] ] ] ] ] | 4: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; destruct (Heq) %{(State (simplify_function f) (simplify_statement stm1) (Kseq (simplify_statement stm2) k') en m)} @conj [ 1: // | 2: %1 @cc_seq // ] | 5: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; elim (Hsim_related cond) in Heq; * [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_expr ge en m cond) [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq #Htype_eq_cond whd in match (bindIO ??????) in ⊢ (% → %); >(simplify_typeof_eq ge en m) cases (exec_bool_of_val condval (typeof cond)) [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; [ 1: destruct skip (condtrace) %{(State (simplify_function f) (simplify_statement iftrue) k' en m)} @conj [ 1: // | 2: Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; elim (Hsim_related cond) in Heq; * [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_expr ge en m cond) [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq #Htype_eq_cond whd in match (bindIO ??????) in ⊢ (% → %); >(simplify_typeof_eq ge en m) cases (exec_bool_of_val condval (typeof cond)) [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; [ 1: destruct skip (condtrace) %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)} @conj [ 1: // | 2: Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; destruct (Heq) %{(State (simplify_function f) (simplify_statement body) (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj [ 1: // | 2: %1 @cc_dowhile // ] | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; cases (is_Sskip init) in Heq; [ 2: #Hinit_neq_Sskip elim (simplify_is_not_skip init Hinit_neq_Sskip) #pf #Hrewrite >Hrewrite normalize nodelta whd in match (ret ??) in ⊢ (% → %); #Eq destruct (Eq) %{(State (simplify_function f) (simplify_statement init) (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj [ 1: // | 2: %1 @cc_for1 // ] | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip whd in match (simplify_statement ?); whd in match (is_Sskip ?); normalize nodelta elim (Hsim_related cond) * [ 2: * #error #Hfail #_ >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_expr ge en m cond) [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite #Htype_eq_cond >Hrewrite whd in match (m_bind ?????); whd in match (m_bind ?????); Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; inversion Hcont_cast in Heq; normalize nodelta [ 1: #Hk #Hk' #_ | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] #H whd in match (ret ??) in H ⊢ %; destruct (H) [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ] | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ] | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; inversion Hcont_cast in Heq; normalize nodelta [ 1: #Hk #Hk' #_ | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] #H whd in match (ret ??) in H ⊢ %; destruct (H) [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 // | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj try // %1 // | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H; [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_expr ??? cond) [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite whd in match (m_bind ?????) in ⊢ (% → %); Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; cases retval in Heq; normalize nodelta [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta whd in match (ret ??) in ⊢ (% → %); [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty' | 7: #id #fl | 8: #id #fl | 9: #rg #id ] #H destruct (H) %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))} @conj [ 1: // | 2: %3 @call_cont_simplify // ] | 2: #e >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta [ 1: #_ #Habsurd destruct (Habsurd) | 2: #_ elim (Hsim_related e) * [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_expr ??? e) [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #a #Hsim #Htype_eq_e lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite whd in match (m_bind ?????); whd in match (m_bind ?????); #Heq destruct (Heq) %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env en)))} @conj [ 1: // | 2: %3 @call_cont_simplify // ] ] ] ] ] | 12: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; elim (Hsim_related cond) in Heq; * [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: cases (exec_expr ??? cond) [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #a #Hsim #Htype_eq_cond lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite whd in match (bindIO ??????); whd in match (bindIO ??????); cases (\fst a) normalize nodelta [ 1,3,4,5: #a destruct (a) #b destruct (b) | 2: #sz #i whd in match (ret ??) in ⊢ (% → %); #Heq destruct (Heq) %{(State (simplify_function f) (seq_of_labeled_statement (select_switch sz i (simplify_ls switchcases))) (Kswitch k') en m)} @conj [ 1: // | 2: @(labeled_statements_ind … switchcases) [ 1: #default_s whd in match (simplify_ls ?); whd in match (select_switch sz i ?) in ⊢ (?%%); whd in match (seq_of_labeled_statement ?) in ⊢ (?%%); %1 @cc_switch // | 2: #sz' #i' #top_case #tail #Hind cut ((seq_of_labeled_statement (select_switch sz i (simplify_ls (LScase sz' i' top_case tail)))) = (simplify_statement (seq_of_labeled_statement (select_switch sz i (LScase sz' i' top_case tail))))) [ 1: >select_switch_commute >simplify_ls_commute @refl | 2: #Hrewrite >Hrewrite %1 @cc_switch // ] ] ] ] ] ] | 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; destruct (Heq) %{(State (simplify_function f) (simplify_statement body) k' en m)} @conj %1 // | 14: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; lapply (cast_find_label_fn lab f (call_cont k) (call_cont k')) cases (find_label lab (fn_body f) (call_cont k)) in Heq; normalize nodelta [ 1: #Habsurd destruct (Habsurd) | 2: * #st #kst normalize nodelta #Heq whd in match (ret ??) in Heq; #H lapply (H st kst (call_cont_simplify ???) (refl ? (Some ? 〈st,kst〉))) try // * #kst' * #Heq2 #Hcont_cast' >Heq2 normalize nodelta destruct (Heq) %{(State (simplify_function f) (simplify_statement st) kst' en m)} @conj [ 1: // | 2: %1 // ] ] | 15: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (simplify_statement ?) in Heq ⊢ %; #Heq whd in match (exec_step ??) in Heq ⊢ %; destruct (Heq) %{(State (simplify_function f) (simplify_statement body) k' en m)} @conj [ 1: // | 2: %1 // ] ] | 2: (* Call state *) #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (exec_step ??) in ⊢ (% → %); elim fd in Heq_s1'; normalize nodelta [ 1: * #rettype #args #vars #body #Heq_s1' whd in match (simplify_function ?); cases (exec_alloc_variables empty_env ??) #local_env #new_mem normalize nodelta cases (exec_bind_parameters ????) [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #new_mem_init whd in match (m_bind ?????); whd in match (m_bind ?????); #Heq destruct (Heq) %{(State (mk_function rettype args vars (simplify_statement body)) (simplify_statement body) k' local_env new_mem_init)} @conj [ 1: // | 2: %1 // ] ] | 2: #id #argtypes #rettype #Heq_s1' cases (check_eventval_list args ?) [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) | 1: #l whd in match (m_bind ?????); whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ] ] | 3: (* Return state *) #res #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (exec_step ??) in ⊢ (% → %); inversion Hcont_cast [ 1: #Hk #Hk' #_ | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] normalize nodelta [ 1: cases res normalize nodelta [ 2: * normalize nodelta #i [ 3: #Heq whd in match (ret ??) in Heq; destruct (Heq) %{(Finalstate i)} @conj [ 1: // | 2: // ] | * : #Habsurd destruct (Habsurd) ] | *: #a try #b destruct ] | 9: elim r normalize nodelta [ 2: * * #block #offset #typ normalize nodelta cases (opt_to_io io_out io_in mem ? (store_value_of_type' ????)) [ 2: #mem whd in match (m_bind ?????); whd in match (m_bind ?????); #Heq destruct (Heq) %{(State (simplify_function f0) Sskip k0' en0 mem)} @conj [ 1: // | 2: %1 // ] | 1: #output #resumption whd in match (m_bind ?????); #Habsurd destruct (Habsurd) | 3: #eror #Habsurd normalize in Habsurd; destruct (Habsurd) ] | 1: #Heq whd in match (ret ??) in Heq; destruct (Heq) %{(State (simplify_function f0) Sskip k0' en0 m)} @conj [ 1: // | 2: %1 // ] ] | *: #Habsurd destruct (Habsurd) ] | 4: (* Final state *) #r #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; whd in match (exec_step ??) in ⊢ (% → %); #Habsurd destruct (Habsurd) ]