(*include "basics/lists/list.ma".*) include "basics/lists/listb.ma". include "common/Identifiers.ma". include "utilities/extralib.ma". (*include "Clight/Csyntax.ma".*) include "Clight/fresh.ma". (*include "Clight/Cexec.ma".*) include "Clight/CexecInd.ma". (*include "Clight/frontend_misc.ma".*) include "Clight/memoryInjections.ma". (* include "Clight/MemProperties.ma". *) (* ----------------------------------------------------------------------------- ----------------------------------------------------------------------------*) (* ----------------------------------------------------------------------------- Documentation ----------------------------------------------------------------------------*) (* This file implements transformation of switches to linear sequences of * if/then/else. The implementation roughly follows the lines of the prototype. * /!\ We assume that the program is well-typed (the type of the evaluated * expression must match the constants on each branch of the switch). /!\ *) (* Documentation. Let the follwing be our input switch construct: // --------------------------------- switch(e) { case v1: stmt1 case v2: stmt2 . . . default: stmt_default } // --------------------------------- Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting the switch statement. In the absence of break, the execution falls through each case sequentially. Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos: // --------------------------------- fresh = e; if(fresh == v1) { stmt1'; goto lbl_case2; } if(fresh == v2) { lbl_case2: stmt2'; goto lbl_case2; } ... stmt_default'; exit_label: // --------------------------------- where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels. *) (* ----------------------------------------------------------------------------- Definitions allowing to state that the program resulting of the transformation is switch-free. ---------------------------------------------------------------------------- *) (* Property of a Clight statement of containing no switch. Could be generalized into a kind of * statement_P, if useful elsewhere. *) let rec switch_free (st : statement) : Prop ≝ match st with [ Sskip ⇒ True | Sassign _ _ ⇒ True | Scall _ _ _ ⇒ True | Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2 | Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2 | Swhile e body ⇒ switch_free body | Sdowhile e body ⇒ switch_free body | Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3 | Sbreak ⇒ True | Scontinue ⇒ True | Sreturn _ ⇒ True | Sswitch _ _ ⇒ False | Slabel _ body ⇒ switch_free body | Sgoto _ ⇒ True | Scost _ body ⇒ switch_free body ]. (* Property of a list of labeled statements of being switch-free *) let rec branches_switch_free (sts : labeled_statements) : Prop ≝ match sts with [ LSdefault st => switch_free st | LScase _ _ st tl => switch_free st ∧ branches_switch_free tl ]. let rec branches_ind (sts : labeled_statements) (H : labeled_statements → Prop) (defcase : ∀st. H (LSdefault st)) (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝ match sts with [ LSdefault st ⇒ defcase st | LScase sz int st tl ⇒ indcase sz int st tl (branches_ind tl H defcase indcase) ]. (* ----------------------------------------------------------------------------- Switch-removal code for statements, functions and fundefs. ----------------------------------------------------------------------------*) (* Converts the directly accessible ("free") breaks to gotos toward the [lab] label. *) let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝ match st with [ Sbreak ⇒ Sgoto lab | Ssequence s1 s2 ⇒ Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab) | Sifthenelse e iftrue iffalse ⇒ Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab) | Sfor init e update body ⇒ Sfor (convert_break_to_goto init lab) e update body | Slabel l body ⇒ Slabel l (convert_break_to_goto body lab) | Scost cost body ⇒ Scost cost (convert_break_to_goto body lab) | _ ⇒ st ]. (* Converting breaks preserves switch-freeness. *) lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label). #s elim s // [ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ | 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ | 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize try @conj try @conj /3/ | 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/ | 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/ ] qed. (* (def_case : ident × sf_statement) *) let rec produce_cond (e : expr) (switch_cases : labeled_statements) (u : universe SymbolTag) (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝ match switch_cases with [ LSdefault st ⇒ let 〈lab,u1〉 ≝ fresh ? u in let st' ≝ convert_break_to_goto st exit in 〈Slabel lab st', lab, u1〉 | LScase sz tag st other_cases ⇒ let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in let st' ≝ convert_break_to_goto st exit in let 〈lab, u2〉 ≝ fresh ? u1 in let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in let case_statement ≝ Sifthenelse test (Slabel lab (Ssequence st' (Sgoto sub_label))) Sskip in 〈Ssequence case_statement sub_statements, lab, u2〉 ]. definition simplify_switch ≝ λ(e : expr). λ(switch_cases : labeled_statements). λ(uv : universe SymbolTag). let 〈exit_label, uv1〉 ≝ fresh ? uv in let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in 〈Ssequence result (Slabel exit_label Sskip), uv2〉. lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))). #l @(labeled_statements_ind … l) [ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1 normalize in Hsf ⊢ %; @(convert_break_lift … Hsf) | 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl #e #lab #u normalize lapply (Hind Hsf_tl e lab u) cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta cases (fresh ??) #lab0 #u2 normalize nodelta normalize try @conj try @conj try @conj try // @(convert_break_lift … Hsf_hd) ] qed. lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)). #e #l cases l [ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta whd @conj whd [ 1: @convert_break_lift assumption | 2: @I ] | 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u cases (fresh ? u) #exit_label #uv1 normalize nodelta lapply (produce_cond_switch_free tl Hsftl e exit_label uv1) cases (produce_cond e tl uv1 exit_label) * #cond #lab #u1 #Hsf_cond normalize nodelta cases (fresh ??) #lab0 #u2 normalize nodelta normalize @conj try @conj try @conj try @conj try // @(convert_break_lift ?? Hsf) ] qed. (* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in order to circumvent the associativity problems in notations. *) (* record swret (A : Type[0]) : Type[0] ≝ { ret_st : A; ret_acc : list (ident × type); ret_u : universe SymbolTag }. notation > "vbox('let' 〈ident v1, ident v2, ident v3〉 ≝ e in break e')" with precedence 48 for @{ (λ${ident v1}.λ${ident v2}.λ${ident v3}. ${e'}) (ret_st ? ${e}) (ret_acc ? ${e}) (ret_u ? ${e}) }. definition ret ≝ λe1,e2,e3. mk_swret statement e1 e2 e3. *) (* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another 'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables allows it to proceed without failing. This is all in order to ease the proof of simulation. *) let rec switch_removal (st : statement) (* the statement in which we will remove switches *) (u : universe SymbolTag) (* a fresh label and ident generator *) : statement × (list (ident × type)) × (universe SymbolTag) ≝ match st with [ Sskip ⇒ 〈st, [ ], u〉 | Sassign _ _ ⇒ 〈st, [ ], u〉 | Scall _ _ _ ⇒ 〈st, [ ], u〉 | Ssequence s1 s2 ⇒ let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in 〈Ssequence s1' s2', acc1 @ acc2, u''〉 | Sifthenelse e s1 s2 ⇒ let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in 〈Sifthenelse e s1' s2', acc1 @ acc2, u''〉 | Swhile e body ⇒ let 〈body', acc, u'〉 ≝ switch_removal body u in 〈Swhile e body', acc, u'〉 | Sdowhile e body ⇒ let 〈body', acc, u'〉 ≝ switch_removal body u in 〈Sdowhile e body', acc, u'〉 | Sfor s1 e s2 s3 ⇒ let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in let 〈s3', acc3, u'''〉 ≝ switch_removal s3 u'' in 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, u'''〉 | Sbreak ⇒ 〈st, [ ], u〉 | Scontinue ⇒ 〈st, [ ], u〉 | Sreturn _ ⇒ 〈st, [ ], u〉 | Sswitch e branches ⇒ let 〈sf_branches, acc, u'〉 ≝ switch_removal_branches branches u in let 〈switch_tmp, u''〉 ≝ fresh ? u' in let ident ≝ Expr (Evar switch_tmp) (typeof e) in let assign ≝ Sassign ident e in let 〈result, u'''〉 ≝ simplify_switch ident sf_branches u'' in 〈Ssequence assign result, (〈switch_tmp, typeof e〉 :: acc), u'''〉 | Slabel label body ⇒ let 〈body', acc, u'〉 ≝ switch_removal body u in 〈Slabel label body', acc, u'〉 | Sgoto _ ⇒ 〈st, [ ], u〉 | Scost cost body ⇒ let 〈body', acc, u'〉 ≝ switch_removal body u in 〈Scost cost body', acc, u'〉 ] and switch_removal_branches (l : labeled_statements) (u : universe SymbolTag) : (labeled_statements × (list (ident × type)) × (universe SymbolTag)) ≝ match l with [ LSdefault st ⇒ let 〈st', acc1, u'〉 ≝ switch_removal st u in 〈LSdefault st', acc1, u'〉 | LScase sz int st tl ⇒ let 〈tl_result, acc1, u'〉 ≝ switch_removal_branches tl u in let 〈st', acc2, u''〉 ≝ switch_removal st u' in 〈LScase sz int st' tl_result, acc1 @ acc2, u''〉 ]. definition ret_st : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → A ≝ λA,x. let 〈s,vars,u〉 ≝ x in s. definition ret_vars : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → list (ident × type) ≝ λA,x. let 〈s,vars,u〉 ≝ x in vars. definition ret_u : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → (universe SymbolTag) ≝ λA,x. let 〈s,vars,u〉 ≝ x in u. (* Proof that switch_removal_switch_free does its job. *) lemma switch_removal_switch_free : ∀st,u. switch_free (ret_st ? (switch_removal st u)). #st @(statement_ind2 ? (λls. ∀u. branches_switch_free (ret_st ? (switch_removal_branches ls u))) … st) try // [ 1: #s1 #s2 #H1 #H2 #u normalize lapply (H1 u) cases (switch_removal s1 u) * #st1 #vars1 #u' normalize #HA lapply (H2 u') cases (switch_removal s2 u') * #st2 #vars2 #u'' normalize #HB @conj assumption | *: (* TODO the first few cases show that the lemma is routinely proved. TBF later. *) @cthulhu ] qed. (* ----------------------------------------------------------------------------- Switch-removal code for programs. ----------------------------------------------------------------------------*) (* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to * name clashes for labels. We have no choice but to actually run through the function and to * compute the maximum of labels+identifiers. This way we can generate both fresh variables and * fresh labels using the same univ. While we're at it we also consider record fields. * Cost labels are not considered, though. They already live in a separate universe. * * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes, * but in the end it might be good to move the following functions into fresh.ma. *) (* Least element in the total order of identifiers. *) definition least_identifier ≝ an_identifier SymbolTag one. (* This is certainly overkill: variables adressed in an expression should be declared in the * enclosing function's prototype. *) let rec max_of_expr (e : expr) : ident ≝ match e with [ Expr ed _ ⇒ match ed with [ Econst_int _ _ ⇒ least_identifier | Evar id ⇒ id | Ederef e1 ⇒ max_of_expr e1 | Eaddrof e1 ⇒ max_of_expr e1 | Eunop _ e1 ⇒ max_of_expr e1 | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) | Ecast _ e1 ⇒ max_of_expr e1 | Econdition e1 e2 e3 ⇒ max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3)) | Eandbool e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) | Eorbool e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) | Esizeof _ ⇒ least_identifier | Efield r f ⇒ max_id f (max_of_expr r) | Ecost _ e1 ⇒ max_of_expr e1 ] ]. (* Reasoning about this promises to be a serious pain. Especially the Scall case. *) let rec max_of_statement (s : statement) : ident ≝ match s with [ Sskip ⇒ least_identifier | Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) | Scall r f args ⇒ let retmax ≝ match r with [ None ⇒ least_identifier | Some e ⇒ max_of_expr e ] in max_id (max_of_expr f) (max_id retmax (foldr ?? (λelt,acc. max_id (max_of_expr elt) acc) least_identifier args) ) | Ssequence s1 s2 ⇒ max_id (max_of_statement s1) (max_of_statement s2) | Sifthenelse e s1 s2 ⇒ max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2)) | Swhile e body ⇒ max_id (max_of_expr e) (max_of_statement body) | Sdowhile e body ⇒ max_id (max_of_expr e) (max_of_statement body) | Sfor init test incr body ⇒ max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body)) | Sbreak ⇒ least_identifier | Scontinue ⇒ least_identifier | Sreturn opt ⇒ match opt with [ None ⇒ least_identifier | Some e ⇒ max_of_expr e ] | Sswitch e ls ⇒ max_id (max_of_expr e) (max_of_ls ls) | Slabel lab body ⇒ max_id lab (max_of_statement body) | Sgoto lab ⇒ lab | Scost _ body ⇒ max_of_statement body ] and max_of_ls (ls : labeled_statements) : ident ≝ match ls with [ LSdefault s ⇒ max_of_statement s | LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s) ]. definition max_id_of_function : function → ident ≝ λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f). (* We compute fresh universes on a function-by function basis, since there can't * be cross-functions gotos or stuff like that. *) definition function_switch_removal : function → function × (list (ident × type)) ≝ λf. let u ≝ universe_of_max (max_id_of_function f) in let 〈st, vars, u'〉 ≝ switch_removal (fn_body f) u in let result ≝ mk_function (fn_return f) (fn_params f) (vars @ (fn_vars f)) st in 〈result, vars〉. let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝ match f with [ CL_Internal f ⇒ CL_Internal (\fst (function_switch_removal f)) | CL_External _ _ _ ⇒ f ]. let rec program_switch_removal (p : clight_program) : clight_program ≝ transform_program ??? p (λ_. fundef_switch_removal). (* ----------------------------------------------------------------------------- Applying two relations on all substatements and all subexprs (directly under). ---------------------------------------------------------------------------- *) let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝ match s1 with [ Sskip ⇒ True | Sassign e1 e2 ⇒ Q e1 ∧ Q e2 | Scall r f args ⇒ match r with [ None ⇒ Q f ∧ (All … Q args) | Some r ⇒ Q r ∧ Q f ∧ (All … Q args) ] | Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2 | Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2 | Swhile e sub ⇒ Q e ∧ P sub | Sdowhile e sub ⇒ Q e ∧ P sub | Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3 | Sbreak ⇒ True | Scontinue ⇒ True | Sreturn r ⇒ match r with [ None ⇒ True | Some r ⇒ Q r ] | Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P) | Slabel _ sub ⇒ P sub | Sgoto _ ⇒ True | Scost _ sub ⇒ P sub ] and substatement_ls ls (P : statement → Prop) : Prop ≝ match ls with [ LSdefault sub ⇒ P sub | LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P) ]. (* ----------------------------------------------------------------------------- Freshness conservation results on switch removal. ---------------------------------------------------------------------------- *) (* Similar stuff in toCminor.ma. *) lemma fresh_for_univ_still_fresh : ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'. * #p * #i #H1 #v * #p' lapply H1 normalize #H1 #H2 destruct (H2) /2/ qed. definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝ λu1,u2. match u1 with [ mk_universe p1 ⇒ match u2 with [ mk_universe p2 ⇒ p2 ≤ p1 ] ]. definition fte ≝ fresher_than_or_equal. lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3. * #u1 * #u2 * #u3 normalize /2 by transitive_le/ qed. lemma reflexive_fte : ∀u. fte u u. * // qed. lemma fresher_for_univ : ∀u1,u2. fte u1 u2 → ∀i. fresh_for_univ ? i u2 → fresh_for_univ ? i u1. * #p * #p' normalize #H * #i normalize /2 by transitive_le/ qed. lemma fresh_fte : ∀u2,u1,fv. fresh ? u2 = 〈fv,u1〉 → fte u1 u2. * #u1 * #u2 * #fv normalize #H1 destruct // qed. lemma produce_cond_fte : ∀e,exit,ls,u. fte (\snd (produce_cond e ls u exit)) u. #e #exit #ls @(branches_ind … ls) [ 1: #st #u normalize lapply (fresh_fte u) cases (fresh ? u) #lab #u1 #H lapply (H u1 lab (refl ??)) normalize // | 2: #sz #i #hd #tl #Hind #u normalize lapply (Hind u) cases (produce_cond e tl u exit) * #subcond #sublabel #u1 #Hfte normalize lapply (fresh_fte u1) cases (fresh ? u1) #lab #u2 #H2 lapply (H2 u2 lab (refl ??)) #Hfte' normalize cases u2 in Hfte'; #u2 cases u in Hfte; #u cases u1 #u1 normalize /2 by transitive_le/ ] qed. lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)). #e #exit #ls #u #i @fresher_for_univ @produce_cond_fte qed. lemma simplify_switch_fte : ∀u,e,ls. fte (\snd (simplify_switch e ls u)) u. #u #e #ls normalize lapply (fresh_fte u) cases (fresh ? u) #exit_label #uv1 #Haux lapply (Haux uv1 exit_label (refl ??)) -Haux #Haux normalize lapply (produce_cond_fte e exit_label ls uv1) cases (produce_cond ????) * #stm #label #uv2 normalize nodelta cases uv2 #uv2 cases uv1 in Haux; #uv1 cases u #u normalize /2 by transitive_le/ qed. lemma simplify_switch_fresh : ∀u,i,e,ls. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (simplify_switch e ls u)). #u #i #e #ls @fresher_for_univ @simplify_switch_fte qed. lemma switch_removal_fte : ∀st,u. fte (ret_u ? (switch_removal … st u)) u. #st @(statement_ind2 ? (λls. ∀u. fte (ret_u ? (switch_removal_branches ls u)) u) … st) try /2 by reflexive_fte/ [ 1: #s1 #s2 #Hind1 #Hind2 #u normalize lapply (Hind1 u) cases (switch_removal s1 u) * #s1' #fvs1 #u' normalize nodelta lapply (Hind2 u') cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize #HA #HB @(transitive_fte … HA HB) | 2: #e #s1 #s2 #Hind1 #Hind2 #u normalize lapply (Hind1 u) cases (switch_removal s1 u) * #s1' #fvs1 #u' normalize nodelta lapply (Hind2 u') cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize #HA #HB @(transitive_fte … HA HB) | 3,7,8: #e #s #Hind #u normalize lapply (Hind u) cases (switch_removal s u) * #s' #fvs #u' normalize #H @H | 4: #e #s #Hind #u normalize lapply (Hind u) cases (switch_removal s u) * #s' #fvs #u' normalize #H @H | 5: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #u normalize lapply (Hind1 u) cases (switch_removal s1 u) * #s1' #fvs1 #u' #Hfte1 normalize nodelta lapply (Hind2 u') cases (switch_removal s2 u') * #s2' #fvs2 #u'' #Hfte2 normalize nodelta lapply (Hind3 u'') cases (switch_removal s3 u'') * #s2' #fvs2 #u'' #Hfte3 normalize nodelta /3 by transitive_fte/ | 6: #e #ls #Hind #u whd in match (switch_removal ??); lapply (Hind u) cases (switch_removal_branches ls u) * #ls #fvs #u' #Hfte1 normalize nodelta lapply (fresh_fte … u') cases (fresh ? u') #fv #u'' #H lapply (H u'' fv (refl ??)) #Hfte2 normalize nodelta lapply (simplify_switch_fte u'' (Expr (Evar fv) (typeof e)) ls) cases (simplify_switch ???) normalize nodelta #st' #u''' #Hfte3 /3 by transitive_fte/ | 9: #s #H #u normalize lapply (H u) cases (switch_removal s u) * #st' #fvs normalize #u' #H @H | 10: #sz #i #st #ls #Hind1 #Hind2 #u normalize lapply (Hind2 u) cases (switch_removal_branches ls u) * #ls' #fvs' #u' normalize nodelta #Hfte1 lapply (Hind1 … u') cases (switch_removal st u') * #st' #fvs'' #u'' normalize nodelta #Hfte2 /3 by transitive_fte/ ] qed. lemma switch_removal_fresh : ∀u,i,st. fresh_for_univ ? i u → fresh_for_univ ? i (ret_u … (switch_removal st u)). #u #i #st @fresher_for_univ @switch_removal_fte qed. (* ----------------------------------------------------------------------------- Simulation proof and related voodoo. ----------------------------------------------------------------------------*) (* 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).*) let rec expr_ind2 (P : expr → Prop) (Q : expr_descr → type → Prop) (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) (Ivar : ∀id, t. Q (Evar id) t) (Ideref : ∀e, t. P e → Q (Ederef e) t) (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) (Ifield : ∀e,f,t. P e → Q (Efield e f) t) (Icost : ∀c,e,t. P e → Q (Ecost c e) t) (e : expr) on e : P e ≝ match e with [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ] and expr_desc_ind2 (P : expr → Prop) (Q : expr_descr → type → Prop) (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) (Ivar : ∀id, t. Q (Evar id) t) (Ideref : ∀e, t. P e → Q (Ederef e) t) (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) (Ifield : ∀e,f,t. P e → Q (Efield e f) t) (Icost : ∀c,e,t. P e → Q (Ecost c e) t) (ed : expr_descr) (t : type) on ed : Q ed t ≝ match ed with [ Econst_int sz i ⇒ Iconst_int sz i t | Evar id ⇒ Ivar id t | Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) | Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) | Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) | Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) | Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) | Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e3) | Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) | Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) | Esizeof sizeoft ⇒ Isizeof sizeoft t | Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) | Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) ]. (* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched by a non-constant number of evaluations in the converted program. More precisely, [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *) (* A version of simplify_switch hiding the ugly projs *) definition fresh_for_expression ≝ λe,u. fresh_for_univ SymbolTag (max_of_expr e) u. definition fresh_for_statement ≝ λs,u. fresh_for_univ SymbolTag (max_of_statement s) u. (* needed during mutual induction ... *) definition fresh_for_labeled_statements ≝ λls,u. fresh_for_univ ? (max_of_ls ls) u. definition fresh_for_function ≝ λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u. (* misc properties of the max function on positives. *) lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v. * #p whd in ⊢ (??%?); >max_one_neutral // qed. lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1. * #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%); >commutative_max // qed. lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3). * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max // qed. lemma fresh_max_split : ∀a,b,u. fresh_for_univ SymbolTag (max_id a b) u → fresh_for_univ ? a u ∧ fresh_for_univ ? b u. * #a * #b * #u normalize lapply (pos_compare_to_Prop a b) cases (pos_compare a b) whd in ⊢ (% → ?); #Hab [ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/ | 2: destruct >reflexive_leb /2/ | 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/ ] qed. lemma fresh_to_substatements : ∀s,u. fresh_for_statement s u → substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u). #s #u cases s whd in match (fresh_for_statement ??); whd in match (substatement_P ???); try /2/ [ 1: #e1 #e2 whd in match (fresh_for_statement ??); whd in match (substatement_P ???); #H lapply (fresh_max_split … H) * /2 by conj/ | 2: #e1 #e2 #args whd in match (fresh_for_statement ??); whd in match (substatement_P ???); cases e1 normalize nodelta [ 1: #H lapply (fresh_max_split … H) * #HA #HB @conj try @HA elim args in HB; try /2 by I/ #hd #tl normalize nodelta #Hind #HB elim (fresh_max_split … HB) #HC #HD whd in match (foldr ?????) in HD; elim (fresh_max_split … HD) #HE #HF @conj try assumption @Hind >max_id_commutative >max_id_one_neutral @HF | 2: #expr #H cases (fresh_max_split … H) #HA normalize nodelta #HB cases (fresh_max_split … HB) #HC #HD @conj try @conj try // elim args in HD; try // #e #l #Hind #HD whd in match (foldr ?????) in HD; elim (fresh_max_split … HD) #HE #HF @conj try assumption @Hind @HF ] | 3: #stmt1 #stmt2 whd in ⊢ (% → %); @fresh_max_split | 4: #e #s1 #s2 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * #H1 @fresh_max_split | 5: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H) | 6: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H) | 7: #s1 #e #s2 #s3 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * #H1 #H2 @conj try @conj try @I try @conj try @I elim (fresh_max_split … H1) elim (fresh_max_split … H2) /2/ | 8: #opt cases opt try /2/ | 9: #e #ls #H whd @conj lapply (fresh_max_split … H) * #HA #HB try // lapply HB @(labeled_statements_ind … ls) [ 1: #s' #H' // | 2: #sz #i #s' #tl #Hind #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj [ 1: // | 2: @Hind @H1 ] ] | 10: #lab #stmt #H whd lapply (fresh_max_split … H) * // ] qed. (* Auxilliary commutation lemma used in [substatement_fresh]. *) lemma foldl_max : ∀l,a,b. foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l = max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l). #l elim l [ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl | 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%); max_id_associative >(max_id_commutative b ?) @refl ] qed. (* --------------------------------------------------------------------------- *) (* Memory extensions (limited form on memoryInjection.ma). Note that we state the properties at the back-end level. *) (* --------------------------------------------------------------------------- *) (* A writeable_block is a block that is: . valid . non-empty (i.e. it has been allocated a non-empty size) *) record nonempty_block (m : mem) (b : block) : Prop ≝ { wb_valid : valid_block m b; wb_nonempty : low (blocks m b) < high (blocks m b) }. (* Type stating that m2 is an extension of m1, parameterised by a list of blocks where we can write freely *) record sr_memext (m1 : mem) (m2 : mem) (writeable : list block) : Prop ≝ { (* Non-empty blocks are preserved as they are. This entails [load_sim]. *) me_nonempty : ∀b. nonempty_block m1 b → nonempty_block m2 b ∧ blocks m1 b = blocks m2 b; (* These blocks are valid in [m2] *) me_writeable_valid : ∀b. meml ? b writeable → nonempty_block m2 b; (* blocks in [m1] than can be validly pointed to cannot be in [me_writeable]. *) me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable) (* This field is not entailed [me_not_writeable] and is necessary to prove valid pointer conservation after a [free]. *) (* Extension blocks contain nothing in [m1] *) (* me_not_mapped : ∀b. meml … b me_writeable → blocks m1 b = empty_block OZ OZ; *) (* Valid pointers are still valid in m2. One could think that this is superfluous as being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer to be one off the end of a block bound. The internal check in beloadv does not. valid_pointer should be understood as "pointer making sense" rather than "pointer from which you can load stuff". [mi_valid_pointers] is used for instance when proving the semantics preservation for equality testing (where we check that the pointers we compare are valid before being equal). *) (* me_valid_pointers : ∀p. valid_pointer m1 p = true → valid_pointer m2 p = true *) }. (* Since we removed end_pointers, we can prove some stuff that was previously given as a field of sr_memext. *) lemma me_not_writeable_ptr : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable). #m1 #m2 #writeable #Hext #p #Hvalid cut (nonempty_block m1 (pblock p)) [ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % // /2 by Zle_to_Zlt_to_Zlt/ | 2: @(me_not_writeable … Hext) ] qed. (* If we have a memory extension, we can simulate loads *) lemma sr_memext_load_sim : ∀m1,m2,writeable. sr_memext m1 m2 writeable → load_sim m1 m2. #m1 #m2 #writeable #Hext #ptr #bev whd in match (beloadv ??) in ⊢ (% → %); #H cut (nonempty_block m1 (pblock ptr) ∧ Zle (low (blocks m1 (pblock ptr))) (Z_of_unsigned_bitvector 16 (offv (poff ptr))) ∧ Zlt (Z_of_unsigned_bitvector 16 (offv (poff ptr))) (high (blocks m1 (pblock ptr))) ∧ bev = (contents (blocks m1 (pblock ptr)) (Z_of_unsigned_bitvector 16 (offv (poff ptr))))) [ @conj try @conj try @conj try % [ 1: @Zltb_true_to_Zlt ] cases (Zltb (block_id (pblock ptr)) (nextblock m1)) in H; normalize nodelta [ 1: // | 2,4,6,8,10: #Habsurd destruct ] generalize in match (Z_of_unsigned_bitvector offset_size (offv (poff ptr))); #z lapply (Zleb_true_to_Zle (low (blocks m1 (pblock ptr))) z) lapply (Zltb_true_to_Zlt z (high (blocks m1 (pblock ptr)))) cases (Zleb (low (blocks m1 (pblock ptr))) z) cases (Zltb z (high (blocks m1 (pblock ptr)))) #H1 #H2 [ 2,3,4,6,7,8,10,11,12,14,15,16: normalize #Habsurd destruct ] normalize #Heq lapply (H1 (refl ??)) lapply (H2 (refl ??)) #Hle #Hlt destruct try assumption try @refl @(Zle_to_Zlt_to_Zlt … Hle Hlt) ] * * * #Hnonempty #Hlow #Hhigh #Hres lapply (me_nonempty … Hext … Hnonempty) * * #Hvalid #Hlt #Hblocks_eq >(Zlt_to_Zltb_true … Hvalid) normalize (Zle_to_Zleb_true … Hlow) >(Zlt_to_Zltb_true … Hhigh) normalize >Hres @refl qed. lemma me_valid_pointers : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀p. valid_pointer m1 p = true → valid_pointer m2 p = true. * #contents1 #nextblock1 #Hnextblock_pos1 * #contents2 #nextblock2 #Hnextblock_pos2 #writeable #Hmemext * #pb #po #Hvalid cut (nonempty_block (mk_mem contents1 nextblock1 Hnextblock_pos1) pb) [ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % // /2 by Zle_to_Zlt_to_Zlt/ ] #Hnonempty lapply (me_nonempty … Hmemext … Hnonempty) * * #Hvalid_block #Hlow_lt_high #Hcontents_eq normalize >(Zlt_to_Zltb_true … Hvalid_block) normalize nodelta (Zle_to_Zleb_true … Hle) normalize nodelta >(Zlt_to_Zltb_true … Hlt) @refl qed. (* --------------------------------------------------------------------------- *) (* Some lemmas on environments and their contents *) (* Definition of environment inclusion and equivalence *) (* Environment "inclusion". *) definition environment_sim ≝ λenv1,env2. ∀id, res. lookup SymbolTag block env1 id = Some ? res → lookup SymbolTag block env2 id = Some ? res. lemma environment_sim_invert_aux : ∀en1,en2. (∀id,res. lookup_opt block id en1 = Some ? res → lookup_opt ? id en2 = Some ? res) → ∀id. lookup_opt ? id en2 = None ? → lookup_opt ? id en1 = None ?. #en1 elim en1 try // #opt1 #left1 #right1 #Hindl1 #Hindr1 #en2 #Hsim normalize #id elim id normalize nodelta [ 1: #Hlookup cases opt1 in Hsim; try // #res #Hsim lapply (Hsim one res (refl ??)) #Hlookup2 >Hlookup2 in Hlookup; #H @H | 2: #id' cases en2 in Hsim; [ 1: normalize #Hsim #_ #_ lapply (Hsim (p1 id')) normalize nodelta cases (lookup_opt block id' right1) try // #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct | 2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup' @(Hindr1 right2) try // #id0 #res0 lapply (Hsim (p1 id0) res0) normalize #Hsol #H @Hsol @H ] | 3: #id' cases en2 in Hsim; [ 1: normalize #Hsim #_ #_ lapply (Hsim (p0 id')) normalize nodelta cases (lookup_opt block id' left1) try // #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct | 2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup' @(Hindl1 left2) try // #id0 #res0 lapply (Hsim (p0 id0) res0) normalize #Hsol #H @Hsol @H ] ] qed. lemma environment_sim_invert : ∀en1,en2. environment_sim en1 en2 → ∀id. lookup SymbolTag block en2 id = None ? → lookup SymbolTag block en1 id = None ?. * #en1 * #en2 #Hsim * #id @environment_sim_invert_aux #id' #res #Hlookup normalize in Hsim; lapply (Hsim (an_identifier … id') res) normalize #Hsol @Hsol @Hlookup qed. (* Environment equivalence. *) definition environment_eq ≝ λenv1,env2. environment_sim env1 env2 ∧ environment_sim env2 env1. lemma symmetric_environment_eq : ∀env1,env2. environment_eq env1 env2 → environment_eq env2 env1. #env1 #env2 * #Hsim1 #Hsim2 % // qed. lemma reflexive_environment_eq : ∀env. environment_eq env env. #env % // qed. (* An environment [e2] is a disjoint extension of [e1] iff (the new bindings are fresh and [e2] is equivalent to adding extension blocks to [e1]). *) definition disjoint_extension ≝ λ(e1, e2 : env). λ(new_vars : list (ident × type)). (∀id. mem_assoc_env id new_vars = true → lookup ?? e1 id = None ?) ∧ (* extension not in e1 *) (∀id. mem_assoc_env id new_vars = true → ∃res.lookup ?? e2 id = Some ? res) ∧ (* all of the extension is in e2 *) (∀id. mem_assoc_env id new_vars = false → lookup ?? e1 id = lookup ?? e2 id). (* only [new_vars] extends e2 *) lemma disjoint_extension_to_inclusion : ∀e1,e2,vars. disjoint_extension e1 e2 vars → environment_sim e1 e2. #e1 #e2 #vars * * #HA #HB #HC whd #id #res @(match (mem_assoc_env id vars) return λx.(mem_assoc_env id vars = x) → ? with [ true ⇒ λH. ? | false ⇒ λH. ? ] (refl ? (mem_assoc_env id vars))) [ 1: #Hlookup lapply (HA ? H) #Habsurd >Habsurd in Hlookup; #H destruct | 2: #Hlookup <(HC ? H) assumption ] qed. (* Small aux lemma to decompose folds on maps with list accumulators *) lemma fold_to_concat : ∀A:Type[0].∀m:positive_map A.∀l.∀f. (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m l) = (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m []) @ l. #A #m elim m [ 1: #l #f normalize @refl | 2: #optblock #left #right #Hind1 #Hind2 #l #f whd in match (fold ?????) in ⊢ (??%%); cases optblock [ 1: normalize (* XXX nodelta not enough here *) >Hind1 >Hind2 >Hind2 in ⊢ (???%); >associative_append @refl | 2: #block normalize (* XXX nodelta not enough here *) >Hind1 >Hind2 >Hind2 in ⊢ (???%); >Hind1 in ⊢ (???%); >append_cons fold_to_concat >fold_to_concat in ⊢ (???%); fold_to_concat >fold_to_concat in ⊢ (???%); (fold_to_concat ?? (〈an_identifier SymbolTag one,elt〉::l)) >(fold_to_concat ?? (〈an_identifier SymbolTag (f one),elt〉::l)) fold_to_concat in ⊢ (? → %); fold_to_concat in ⊢ (? → %); fold_to_concat fold_to_concat fold_to_concat fold_to_concat fold_to_concat fold_to_concat in ⊢ (???%); fold_to_concat >fold_to_concat in ⊢ (???%); fold_to_concat fold_to_concat in ⊢ (???%); Heq normalize nodelta @mem_append_backwards %2 >fold_to_concat Heq normalize nodelta @mem_append_backwards %2 >fold_to_concat Hblocks_eq >Hblocks_eq' @refl | 2: #b #Hmem lapply (mem_append_forward ???? Hmem) * [ 1: #Hmem12 lapply (me_writeable_valid … H12 b Hmem12) #Hnonempty2 elim (me_nonempty … H23 … Hnonempty2) // | 2: #Hmem23 @(me_writeable_valid … H23 b Hmem23) ] | 3: #b #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) * [ 1: #Hmem12 lapply (me_not_writeable … H12 … Hvalid) * #H @H assumption | 2: #Hmem23 lapply (me_nonempty … H12 … Hvalid) * #Hvalid2 lapply (me_not_writeable … H23 … Hvalid2) * #H #_ @H assumption ] ] qed. lemma memory_ext_reflexive : ∀m. sr_memext m m [ ]. #m % /2/ #b * qed. (* --------------------------------------------------------------------------- *) (* Lemmas relating memory extensions to [free] *) lemma beloadv_free_simulation : ∀m1,m2,writeable,block,ptr,res. ∀mem_hyp : sr_memext m1 m2 writeable. beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res. * #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 #writeable * (* #br *) #bid * * (* #pr *) #pid #poff #res #Hext (*#Hme_nonempty #Hme_writeable #Hme_nonempty #Hvalid_conserv*) #Hload lapply (beloadv_free_beloadv … Hload) #Hload_before_free lapply (beloadv_free_blocks_neq … Hload) #Hblocks_neq @beloadv_free_beloadv2 [ 1: @Hblocks_neq ] @(sr_memext_load_sim … Hext) assumption qed. (* Lifting the property of being valid after a free to memory extensions *) lemma valid_pointer_free : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true. #m1 #m2 #writeable #Hext #p #b #Hvalid lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free lapply (me_valid_pointers … Hext … Hvalid_before_free) lapply (valid_after_free … Hvalid) #Hneq whd in match (free ??); whd in match (update_block ????); whd in match (valid_pointer ??) in ⊢ (% → %); whd in match (low_bound ??) in ⊢ (% → %); whd in match (high_bound ??) in ⊢ (% → %); >(not_eq_block_rev … Hneq) normalize nodelta #H @H qed. lemma nonempty_block_mismatch : ∀m,b,bl. nonempty_block (free m bl) b → nonempty_block m b ∧ b ≠ bl. #m #b #bl #Hnonempty @(eq_block_elim … b bl) [ 1: #Heq >Heq in Hnonempty; * #_ normalize cases (block_region bl) normalize >eqZb_reflexive normalize * | 2: #Hneq @conj try assumption elim Hnonempty #Hvalid #Hlh % [ 1: lapply Hvalid normalize // | 2: lapply Hlh normalize @(eqZb_elim … (block_id b) (block_id bl)) [ 1,3: * normalize * | 2,4: #_ // ] ] ] qed. lemma eqb_to_eq_block : ∀a,b : block. a == b = eq_block a b. #a #b lapply (eqb_true ? a b) @(eq_block_elim … a b) #H #I try /2 by neq_block_eq_block_false, true_to_andb_true/ cases I #J #K @K @H qed. (* We can free in both sides of a memory extension if we take care of removing the freed block from the set of writeable blocks. *) lemma free_memory_ext : ∀m1,m2,writeable,bl. sr_memext m1 m2 writeable → sr_memext (free m1 bl) (free m2 bl) (lset_remove ? writeable bl). #m1 #m2 #writeable #bl #Hext % [ 1: #b #Hnonempty lapply (nonempty_block_mismatch … Hnonempty) * #Hnonempty' #Hblocks_neq lapply (me_nonempty … Hext … Hnonempty') * #Hnonempty2 #Hcontents_eq @conj [ 1: % try @(wb_valid … Hnonempty2) whd in match (free ??); whd in match (update_block ?????); >(neq_block_eq_block_false … Hblocks_neq) normalize try @(wb_nonempty … Hnonempty2) | 2: whd in match (free ??) in ⊢ (??%%); whd in match (update_block ?????) in ⊢ (??%%); >(neq_block_eq_block_false … Hblocks_neq) normalize nodelta assumption ] | 2: #b #Hmem cut (mem block b writeable ∧ b ≠ bl) [ elim writeable in Hmem; [ 1: normalize * | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta [ 1: #Heq #H whd in match (meml ???); elim (Hind H) #H0 #H1 @conj [ 1: %2 ] assumption | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * [ 1: #H destruct /3 by conj, or_introl, refl/ | 2: #H elim (Hind H) #H1 #H2 /3 by conj, or_intror, refl/ ] ] ] ] * #Hmem2 #Hblocks_neq lapply (me_writeable_valid … Hext … Hmem2) * #Hvalid #Hnonempty % try assumption whd in match (free ??); whd in match (update_block ?????); >(neq_block_eq_block_false … Hblocks_neq) @Hnonempty | 3: #p #Hvalid lapply (nonempty_block_mismatch … Hvalid) * #Hnonempty #Hblocks_neq % #Hmem lapply (me_not_writeable … Hext … Hnonempty) * #H @H elim writeable in Hmem; [ 1: * | 2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta [ 1: #Heq #H normalize %2 @(Hind H) | 2: #Hblocks_neq whd in match (meml ???); * [ 1: #Hneq normalize %1 assumption | 2: #Hmem normalize %2 @(Hind Hmem) ] ] ] ] qed. (* Freeing from an extension block is ok. *) lemma memext_free_extended_conservation : ∀m1,m2 : mem. ∀writeable. ∀mem_hyp : sr_memext m1 m2 writeable. ∀b. meml ? b writeable → sr_memext m1 (free m2 b) (lset_remove … writeable b). #m1 #m2 #writeable #Hext #b #Hb_writeable % [ 1: #bl #Hnonempty lapply (me_not_writeable … Hext … Hnonempty) #Hnot_mem lapply (mem_not_mem_neq … Hb_writeable Hnot_mem) #Hblocks_neq @conj [ 2: whd in match (free ??); whd in match (update_block ?????); >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize elim (me_nonempty … Hext … Hnonempty) // | 1: % elim (me_nonempty … Hext … Hnonempty) * try // #Hvalid2 #Hlh #Hcontents_eq whd in match (free ??); whd in match (update_block ?????); >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize assumption ] | 2: #b' #Hmem (* contradiction in first premise *) cut (mem block b' writeable ∧ b' ≠ b) [ elim writeable in Hmem; [ 1: normalize @False_ind | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta [ 1: #Heq #H whd in match (meml ???); destruct elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] ] ] ] * #Hb' #Hneq lapply (me_writeable_valid … Hext … Hb') #Hvalid % [ 1: @(wb_valid … Hvalid) | 2: whd in match (free ??); whd in match (update_block ?????); >(neq_block_eq_block_false … Hneq) @(wb_nonempty … Hvalid) ] | 3: #b' #Hnonempty % #Hmem cut (mem block b' writeable ∧ b' ≠ b) [ elim writeable in Hmem; [ 1: normalize @False_ind | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta [ 1: #Heq #H whd in match (meml ???); destruct elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] ] ] ] * #Hmem' #Hblocks_neq lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption ] qed. lemma disjoint_extension_nil_eq_set : ∀env1,env2. disjoint_extension env1 env2 [ ] → lset_eq ? (blocks_of_env env1) (blocks_of_env env2). #env1 #env whd in ⊢ (% → ?); * * #_ #_ #H normalize in H; @environment_eq_blocks_eq whd @conj #id #res >(H id) // qed. lemma free_list_equivalent_sets : ∀m,set1,set2. lset_eq ? set1 set2 → memory_eq (free_list m set1) (free_list m set2). #m #set1 #set2 #Heq whd in match (free_list ??) in ⊢ (?%%); @(lset_eq_fold block_DeqSet mem memory_eq … Heq) [ 1: @reflexive_memory_eq | 2: @transitive_memory_eq | 3: @symmetric_memory_eq | 4: #x #acc1 #acc2 whd in match (free ??) in ⊢ (? → (?%%)); whd in match (memory_eq ??) in ⊢ (% → %); * #Hnextblock_eq #Hcontents_eq @conj try assumption #b normalize >Hcontents_eq @refl | 5: #x1 #x2 #acc normalize @conj try @refl * (* * *) #id normalize nodelta cases (block_region x1) cases (block_region x2) normalize nodelta @(eqZb_elim id (block_id x1)) #Hx1 normalize nodelta @(eqZb_elim id (block_id x2)) #Hx2 normalize nodelta try @refl | 6: * (* #r *) #i * #contents #nextblock #Hpos @conj [ 1: @refl | 2: #b normalize (* cases (block_region b) normalize cases r normalize *) cases (eqZb (block_id b) i) normalize @refl ] ] qed. lemma foldr_identity : ∀A:Type[0]. ∀l:list A. foldr A ? (λx:A.λl0.x::l0) [] l = l. #A #l elim l // #hd #tl #Hind whd in match (foldr ?????); >Hind @refl qed. lemma mem_not_mem_diff_aux : ∀s1,s2,s3,hd. mem ? hd s1 → ¬(mem ? hd s2) → mem block hd (lset_difference ? s1 (s2@(filter block_DeqSet (λx:block_DeqSet.¬x==hd) s3))). #s1 #s2 #s3 #hd #Hmem #Hnotmem lapply Hmem lapply s1 -s1 elim s3 [ 1: #s1 >append_nil elim s1 try // #hd' #tl' #Hind * [ 1: #Heq >lset_difference_unfold @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with [ true ⇒ λH. ? | false ⇒ λH. ? ] (refl ? (hd'∈s2))) normalize nodelta [ 1: lapply (memb_to_mem … H) #Hmem elim Hnotmem #H' destruct @(False_ind … (H' Hmem)) | 2: whd %1 assumption ] | 2: #Hmem >lset_difference_unfold @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with [ true ⇒ λH. ? | false ⇒ λH. ? ] (refl ? (hd'∈s2))) normalize nodelta [ 1: @Hind @Hmem | 2: %2 @Hind @Hmem ] ] | 2: #hd' #tl' #H #s1 #Hmem >filter_cons_unfold >eqb_to_eq_block @(eq_block_elim … hd' hd) [ 1: >notb_true normalize nodelta #Heq @H @Hmem | 2: #Hneq >notb_false normalize nodelta >lset_difference_permute >(cons_to_append … hd') >associative_append >lset_difference_unfold2 >nil_append >lset_difference_permute @H elim s1 in Hmem; try // #hd'' #tl'' #Hind * [ 1: #Heq destruct whd in match (lset_remove ???); >eqb_to_eq_block >(neq_block_eq_block_false … (sym_neq … Hneq)) >notb_false normalize nodelta %1 @refl | 2: #Hmem whd in match (lset_remove ???); cases (¬(hd''==hd')) normalize nodelta [ 1: %2 @Hind @Hmem | 2: @Hind @Hmem ] ] ] ] qed. (* freeing equivalent sets of blocks on memory extensions yields memory extensions *) lemma free_equivalent_sets : ∀m1,m2,writeable,set1,set2. lset_eq ? set1 set2 → sr_memext m1 m2 writeable → sr_memext (free_list m1 set1) (free_list m2 set2) (lset_difference ? writeable set1). #m1 #m2 #writeable #set1 #set2 #Heq #Hext lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq)) #Heq lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext' lapply (memory_ext_transitive (free_list m1 set1) (free_list m2 set1) (free_list m2 set2) (filter block_eq (λwb:block_eq.¬wb∈set1) writeable) [ ] ? Hext') [ 2: >append_nil #H @H ] elim set1 [ 1: whd in match (free_list ??); whd in match (free_list ??); normalize >foldr_identity @Hext | 2: #hd #tl #Hind >free_list_cons >free_list_cons lapply (free_memory_ext … hd … Hind) cut ((lset_remove block_eq (filter block_eq (λwb:block_eq.¬wb∈tl) writeable) hd) = (filter block_eq (λwb:block_eq.¬wb∈hd::tl) writeable)) [ whd in match (lset_remove ???); elim writeable // #hd' #tl' #Hind_cut >filter_cons_unfold >filter_cons_unfold whd in match (memb ???) in ⊢ (???%); >eqb_to_eq_block (* elim (eqb_true block_DeqSet hd' hd)*) @(eq_block_elim … hd' hd) normalize nodelta [ 1: #Heq cases (¬hd'∈tl) normalize nodelta [ 1: whd in match (foldr ?????); >Heq >eqb_to_eq_block >eq_block_b_b normalize in match (notb ?); normalize nodelta lapply Hind_cut destruct #H @H | 2: lapply Hind_cut destruct #H @H ] | 2: #Hneq cases (¬hd'∈tl) normalize nodelta try assumption whd in match (foldr ?????); >eqb_to_eq_block >(neq_block_eq_block_false … Hneq) normalize in match (notb ?); normalize nodelta >Hind_cut @refl ] ] #Heq >Heq #H @H ] qed. (* Remove a writeable block. *) lemma memory_ext_weaken : ∀m1,m2,hd,writeable. sr_memext m1 m2 (hd :: writeable) → sr_memext m1 m2 writeable. #m1 #m2 #hd #writeable * #Hnonempty #Hwriteable_valid #Hnot_writeable % try assumption [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption | 2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem ] qed. (* Perform a "rewrite" using lset_eq on the writeable blocks *) lemma memory_ext_writeable_eq : ∀m1,m2,wr1,wr2. sr_memext m1 m2 wr1 → lset_eq ? wr1 wr2 → sr_memext m1 m2 wr2. #m1 #m2 #wr1 #wr2 #Hext #Hset_eq % [ 1: @(me_nonempty … Hext) | 2: #b #Hmem lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) @(me_writeable_valid … Hext) | 3: #b #Hnonempty % #Hmem lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem' lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption ] qed. lemma memory_eq_to_memory_ext_pre : ∀m1,m1',m2,writeable. memory_eq m1 m1' → sr_memext m1' m2 writeable → sr_memext m1 m2 writeable. #m1 #m1' #m2 #writeable #Heq #Hext lapply (memory_eq_to_mem_ext … Heq) #Hext' @(memory_ext_transitive … Hext' Hext) qed. lemma memory_eq_to_memory_ext_post : ∀m1,m2,m2',writeable. memory_eq m2' m2 → sr_memext m1 m2' writeable → sr_memext m1 m2 writeable. #m1 #m2 #m2' #writeable #Heq #Hext lapply (memory_eq_to_mem_ext … Heq) #Hext' lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H qed. lemma memext_free_extended_environment : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀env,env_ext,vars. disjoint_extension env env_ext vars → lset_inclusion ? (lset_difference ? (blocks_of_env env_ext) (blocks_of_env env)) writeable → sr_memext (free_list m1 (blocks_of_env env)) (free_list m2 (blocks_of_env env_ext)) (lset_difference ? writeable (blocks_of_env env_ext)). #m1 #m2 #writeable #Hext #env #env_ext #vars #Hdisjoint #Hext_in_writeable (* Disjoint extension induces environment "inclusion", i.e. simulation *) lapply (disjoint_extension_to_inclusion … Hdisjoint) #Hincl (* Environment inclusion entails set inclusion on the mapped blocks *) lapply (environment_sim_blocks_inclusion … Hincl) #Hblocks_incl (* This set inclusion can be decomposed on a common part and an extended part. *) lapply (lset_inclusion_difference ??? Hblocks_incl) * #extended_part * * #Hset_eq #Henv_disjoint_ext #Hextended_eq lapply (lset_difference_lset_eq … writeable … Hset_eq) #HeqA cut (lset_inclusion ? extended_part writeable) [ 1: cases Hextended_eq #HinclA #_ @(transitive_lset_inclusion … HinclA … Hext_in_writeable) ] -Hext_in_writeable #Hext_in_writeable @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqA)) lapply (free_list_equivalent_sets m2 ?? Hset_eq) #Hmem_eq @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq)) (* Add extended ⊆ (lset_difference block_eq writeable (blocks_of_env env @ tl)) in Hind *) cut (∀x. mem ? x extended_part → ¬ (mem ? x (blocks_of_env env))) [ 1: cases Hextended_eq #Hincl_ext #_ @(lset_not_mem_difference … Hincl_ext) ] lapply (proj2 … Hset_eq) lapply Hext_in_writeable @(WF_rect ????? (filtered_list_wf block_DeqSet extended_part)) * [ 1: #_ #_ #_ #_ #_ >append_nil @(free_equivalent_sets ???? (blocks_of_env env) (reflexive_lset_eq ??) Hext) | 2: #hd #tl #Hwf_step #Hind_wf #Hext_in_writeable #Hset_incl #Hin_ext_not_in_env cut (lset_eq ? (blocks_of_env env@hd::tl) (hd::(blocks_of_env env@tl))) [ 1: >cons_to_append >cons_to_append in ⊢ (???%); @lset_eq_concrete_to_lset_eq // ] #Hpermute lapply (free_list_equivalent_sets m2 ?? Hpermute) #Hmem_eq2 @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq2)) >free_list_cons lapply (lset_difference_lset_eq … writeable … Hpermute) #HeqB @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqB)) >lset_difference_unfold2 lapply (lset_difference_lset_remove_commute ? hd writeable (blocks_of_env env@tl)) #Heq_commute >Heq_commute (* lapply (memory_ext_writeable_eq ????? (symmetric_lset_eq … Heq_commute)) *) lapply (Hind_wf (filter … (λx.¬(x==hd)) tl) ????) [ 2: @(transitive_lset_inclusion … Hset_incl) @lset_inclusion_concat_monotonic @cons_preserves_inclusion @lset_inclusion_filter_self | 3: @(transitive_lset_inclusion … Hext_in_writeable) @cons_preserves_inclusion @lset_inclusion_filter_self | 4: whd whd in ⊢ (???%); lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?); normalize nodelta @refl | 1: #x #H @Hin_ext_not_in_env %2 elim tl in H; // #hd' #tl' #Hind >filter_cons_unfold >eqb_to_eq_block @(eq_block_elim … hd' hd) >notb_true >notb_false normalize nodelta [ 1: #Heq >Heq #H %2 @Hind @H | 2: #Hneq * [ 1: #Heq destruct %1 @refl | 2: #H %2 @Hind @H ] ] ] #Hext_ind lapply (Hin_ext_not_in_env … hd (or_introl … (refl ??))) #Hnot_in_env lapply (memext_free_extended_conservation … Hext_ind hd ?) [ 1: @mem_not_mem_diff_aux try assumption elim Hext_in_writeable #H #_ @H ] -Hext_ind #Hext_ind cut (memory_eq (free (free_list m2 (blocks_of_env env@filter block_DeqSet (λx:block_DeqSet.¬x==hd) tl)) hd) (free (free_list m2 (blocks_of_env env@tl)) hd)) [ 1: cons_to_append >cons_to_append in ⊢ (???%); @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????)) @symmetric_lset_eq_concrete @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????)) @lset_eq_to_lset_eq_concrete elim (blocks_of_env env) [ 1: @symmetric_lset_eq @lset_eq_filter | 2: #hd0 #tl0 #Hind >cons_to_append >associative_append in ⊢ (??%%); >associative_append in ⊢ (??%%); @cons_monotonic_eq @Hind ] ] #Hmem_eq3 @(memory_eq_to_memory_ext_post … Hmem_eq3) @(memory_ext_writeable_eq … Hext_ind) cons_to_append >cons_to_append in ⊢ (???%); @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????)) @symmetric_lset_eq_concrete @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????)) @lset_eq_to_lset_eq_concrete elim (blocks_of_env env) [ 1: @symmetric_lset_eq @lset_eq_filter | 2: #hd0 #tl0 #Hind >cons_to_append >associative_append in ⊢ (??%%); >associative_append in ⊢ (??%%); @cons_monotonic_eq @Hind ] ] qed. (* --------------------------------------------------------------------------- *) (* Some lemmas allowing to reason on writes to extended memories. *) (* Writing in the extended part of the memory preserves the extension (that's the point) *) lemma bestorev_writeable_memory_ext : ∀m1,m2,writeable. ∀Hext:sr_memext m1 m2 writeable. ∀wb,wo,v. meml ? wb writeable → ∀m2'.bestorev m2 (mk_pointer wb wo) v = Some ? m2' → sr_memext m1 m2' writeable. #m1 * #contents2 #nextblock2 #Hpos2 #writeable #Hext #wb #wo #v #Hmem #m2' whd in ⊢ ((??%?) → ?); lapply (me_writeable_valid … Hext ? Hmem) * whd in ⊢ (% → ?); #Hlt >(Zlt_to_Zltb_true … Hlt) normalize nodelta #Hnonempty2 #H lapply (if_opt_inversion ???? H) -H * #Hzltb lapply (andb_inversion … Hzltb) * #Hleb #Hltb -Hzltb #Heq destruct % [ 1: #b #Hnonempty1 lapply (me_nonempty … Hext b Hnonempty1) * * #Hvalid_b #Hnonempty_b #Heq @conj [ 1: % whd whd in Hvalid_b; try @Hvalid_b normalize cases (block_region b) normalize nodelta cases (block_region wb) normalize nodelta try // @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta try // | 2: whd in ⊢ (??%%); @(eq_block_elim … b wb) normalize nodelta // #Heq_b_wb lapply (me_not_writeable … Hext b Hnonempty1) destruct (Heq_b_wb) * #H @(False_ind … (H Hmem)) ] | 2: #b #Hmem_writeable lapply (me_writeable_valid … Hext … Hmem_writeable) #H % [ 1: normalize cases H // | 2: cases H normalize #Hb_lt #Hb_nonempty2 (* cases (block_region b) cases (block_region wb) *) @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta // ] | 3: #b #Hnonempty lapply (me_not_writeable … Hext … Hnonempty) // ] qed. (* If we manage to write in a block, then it is nonempty *) lemma bestorev_success_nonempty : ∀m,wb,wo,v,m'. bestorev m (mk_pointer wb wo) v = Some ? m' → nonempty_block m wb. #m #wb #wo #v #m' normalize #Hstore cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H cases (if_opt_inversion ???? H) -H #nonempty #H % [ 1: whd @Zltb_true_to_Zlt assumption | 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H' cut (Zleb (low (blocks m wb)) z = true) [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ] #Hleb >Hleb in H'; normalize nodelta #Hlt lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt) /2 by Zle_to_Zlt_to_Zlt/ ] qed. (* If we manage to write in a block, it is still non-empty after the write *) lemma bestorev_success_nonempty2 : ∀m,wb,wo,v,m'. bestorev m (mk_pointer wb wo) v = Some ? m' → nonempty_block m' wb. #m #wb #wo #v #m' normalize #Hstore cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H cases (if_opt_inversion ???? H) -H #nonempty #H % [ 1: whd destruct @Zltb_true_to_Zlt assumption | 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H' cut (Zleb (low (blocks m wb)) z = true) [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ] #Hleb >Hleb in H'; normalize nodelta #Hlt lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt) destruct cases (block_region wb) normalize >eqZb_z_z normalize /2 by Zle_to_Zlt_to_Zlt/ ] qed. (* A nonempty block stays nonempty after a write. *) lemma nonempty_block_update_ok : ∀m,b,wb,offset,v. nonempty_block m b → nonempty_block (mk_mem (update_block ? wb (mk_block_contents (low (blocks m wb)) (high (blocks m wb)) (update beval offset v (contents (blocks m wb)))) (blocks m)) (nextblock m) (nextblock_pos m)) b. #m #b #wb #offset #v * #Hvalid #Hnonempty % // cases b in Hvalid Hnonempty; (* #br *) #bid cases wb (* #wbr *) #wbid normalize (* cases br *) normalize nodelta (* cases wbr normalize nodelta // *) @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // qed. lemma nonempty_block_update_ok2 : ∀m,b,wb,offset,v. nonempty_block (mk_mem (update_block ? wb (mk_block_contents (low (blocks m wb)) (high (blocks m wb)) (update beval offset v (contents (blocks m wb)))) (blocks m)) (nextblock m) (nextblock_pos m)) b → nonempty_block m b. #m #b #wb #offset #v * #Hvalid #Hnonempty % // cases b in Hvalid Hnonempty; (* #br *) #bid cases wb (* #wbr *) #wbid normalize (* cases br normalize nodelta cases wbr normalize nodelta // *) @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // qed. (* Writing in the non-extended part of the memory preserves the extension as long * as it's done identically in both memories. *) lemma bestorev_not_writeable_memory_ext : ∀m1,m2,writeable. ∀Hext:sr_memext m1 m2 writeable. ∀wb,wo,v. ∀m1'. bestorev m1 (mk_pointer wb wo) v = Some ? m1' → ∃m2'. bestorev m2 (mk_pointer wb wo) v = Some ? m2' ∧ sr_memext m1' m2' writeable. #m1 #m2 #writeable #Hext #wb #wo #v #m1' #Hstore1 lapply (bestorev_success_nonempty … Hstore1) #Hwb_nonempty cases (me_nonempty … Hext … Hwb_nonempty) #Hwb_nonempty2 #Hblocks_eq cut (∃m2'. bestorev m2 (mk_pointer wb wo) v=Some mem m2') [ cases Hwb_nonempty2 #Hwb_valid #Hnonempty normalize normalize in Hwb_valid; >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta whd in Hstore1:(??%%); normalize cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 >Hblocks_eq in Hleb1 Hltb1 ⊢ %; #Hleb1 #Hltb1 >Hleb1 >Hltb1 normalize nodelta /2 by ex_intro/ ] * #m2' #Hstore2 %{m2'} @conj try assumption whd in Hstore1:(??%%); whd in Hstore2:(??%%); cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H cases (if_opt_inversion ???? Hstore2) -Hstore2 #block_valid2 #H cases (if_opt_inversion ???? H) #Hin_bounds2 #Hm2' -H cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 cases (andb_inversion … Hin_bounds2) #Hleb2 #Hltb2 -Hin_bounds2 cut (valid_pointer m1 (mk_pointer wb wo)) [ 1: normalize >block_valid1 normalize nodelta >Hleb1 normalize nodelta >Hltb1 @I ] #Hvalid lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_in_writeable destruct % [ 1: #b #Hnonempty lapply (me_nonempty … Hext … (nonempty_block_update_ok2 … Hnonempty)) * #HA #HB @conj [ 1: @nonempty_block_update_ok // | 2: normalize (* cases b in HB; #br #bid cases wb #wbr #wbid cases br cases wbr normalize nodelta *) @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta // #Hid_eq cut (b = wb) [ cases b in Hid_eq; cases wb #wid #bid #H >H @refl ] #Hblock_eq destruct (Hblock_eq) >HB @refl ] | 2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok | 3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty) @(me_not_writeable … Hext) ] qed. (* If we successfuly store something in the first memory, then we can store it in the * second one and the memory extension is preserved. *) lemma memext_store_value_of_type : ∀m, m_ext, m', writeable, ty, loc, off, v. sr_memext m m_ext writeable → store_value_of_type ty m loc off v = Some ? m' → ∃m_ext'. store_value_of_type ty m_ext loc off v = Some ? m_ext' ∧ sr_memext m' m_ext' writeable. #m #m_ext #m' #writeable #ty #loc #off #v #Hext (* case analysis on access mode of [ty] *) cases ty [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] whd in ⊢ ((??%?) → (?%?)); [ 1,4,5,6,7: #Habsurd destruct ] whd in ⊢ (? → (??(λ_.?(??%?)?))); lapply loc lapply off lapply Hext lapply m_ext lapply m lapply m' -loc -off -Hext -m_ext -m -m' elim (fe_to_be_values ??) [ 1,3,5: #m' #m #m_ext #Hext #off #loc normalize in ⊢ (% → ?); #Heq destruct (Heq) %{m_ext} @conj normalize // | 2,4,6: #hd #tl #Hind #m' #m #m_ext #Hext #off #loc whd in ⊢ ((??%?) → ?); #H cases (some_inversion ????? H) #m'' * #Hstore_eq #Hstoren_eq lapply (bestorev_not_writeable_memory_ext … Hext … Hstore_eq) * #m_ext'' * #Hstore_eq2 #Hext2 lapply (Hind … Hext2 … Hstoren_eq) -Hind * #m_ext' * #Hstoren' #Hext3 %{m_ext'} @conj try assumption whd in ⊢ (??%%); >Hstore_eq2 normalize nodelta @Hstoren' ] qed. lemma memext_store_value_of_type' : ∀m, m_ext, m', writeable, ty, ptr, v. sr_memext m m_ext writeable → store_value_of_type' ty m ptr v = Some ? m' → ∃m_ext'. store_value_of_type' ty m_ext ptr v = Some ? m_ext' ∧ sr_memext m' m_ext' writeable. #m #m_ext #m' #writeable #ty #p #v #Hext cases p #b #o @memext_store_value_of_type @Hext qed. lemma memext_store_value_of_type_writeable : ∀m1,m2,writeable. ∀Hext:sr_memext m1 m2 writeable. ∀wb. meml ? wb writeable → ∀ty,off,v,m2'. store_value_of_type ty m2 wb off v = Some ? m2' → sr_memext m1 m2' writeable. #m1 #m2 #writeable #Hext #wb #Hmem #ty #off #v #m2' cases ty [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] whd in ⊢ ((??%?) → ?); [ 1,4,5,6,7: #Habsurd destruct ] lapply Hext lapply m1 lapply m2 lapply m2' lapply off -Hext -m1 -m2 -m2' -off -ty elim (fe_to_be_values ??) [ 1,3,5: #o #m2' #m2 #m1 #Hext normalize #Heq destruct assumption | *: #hd #tl #Hind #o #m2_end #m2 #m1 #Hext whd in match (storen ???); #Hbestorev cases (some_inversion ????? Hbestorev) #m2' * #Hbestorev #Hstoren lapply (bestorev_writeable_memory_ext … Hext … o hd Hmem … Hbestorev) #Hext' @(Hind … Hstoren) // ] qed. (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if * the variable is not in a local environment, then we search into the global one. * A proper "extension" of a local environment should be such that the extension * does not collide with a given global env. * To see the details of why we need that, see [exec_lvalue'], Evar id case. *) definition ext_fresh_for_genv ≝ λ(ext : list (ident × type)). λ(ge : genv). ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?. (* "generic" simulation relation on [res ?] *) definition res_sim ≝ λ(A : Type[0]). λ(r1, r2 : res A). ∀a. r1 = OK ? a → r2 = OK ? a. (* Specialisation of [res_sim] to match [exec_expr] *) definition exec_expr_sim ≝ res_sim (val × trace). (* Specialisation of [res_sim] to match [exec_lvalue] *) definition exec_lvalue_sim ≝ res_sim (block × offset × trace). lemma load_value_of_type_dec : ∀ty, m, b, o. load_value_of_type ty m b o = None ? ∨ ∃r. load_value_of_type ty m b o = Some ? r. #ty #m #b #o cases (load_value_of_type ty m b o) [ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed. (* Simulation relations. *) inductive switch_cont_sim : list (ident × type) → cont → cont → Prop ≝ | swc_stop : ∀new_vars. switch_cont_sim new_vars Kstop Kstop | swc_seq : ∀s,k,k',u,s',new_vars. fresh_for_statement s u → switch_cont_sim new_vars k k' → s' = ret_st ? (switch_removal s u) → lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → switch_cont_sim new_vars (Kseq s k) (Kseq s' k') | swc_while : ∀e,s,k,k',u,s',new_vars. fresh_for_statement (Swhile e s) u → switch_cont_sim new_vars k k' → s' = ret_st ? (switch_removal s u) → lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → switch_cont_sim new_vars (Kwhile e s k) (Kwhile e s' k') | swc_dowhile : ∀e,s,k,k',u,s',new_vars. fresh_for_statement (Sdowhile e s) u → switch_cont_sim new_vars k k' → s' = ret_st ? (switch_removal s u) → lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → switch_cont_sim new_vars (Kdowhile e s k) (Kdowhile e s' k') | swc_for1 : ∀e,s1,s2,k,k',u,s',new_vars. fresh_for_statement (Sfor Sskip e s1 s2) u → switch_cont_sim new_vars k k' → s' = (ret_st ? (switch_removal (Sfor Sskip e s1 s2) u)) → lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → switch_cont_sim new_vars (Kseq (Sfor Sskip e s1 s2) k) (Kseq s' k') | swc_for2 : ∀e,s1,s2,k,k',u,result1,result2,new_vars. fresh_for_statement (Sfor Sskip e s1 s2) u → switch_cont_sim new_vars k k' → result1 = ret_st ? (switch_removal s1 u) → result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) → lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → switch_cont_sim new_vars (Kfor2 e s1 s2 k) (Kfor2 e result1 result2 k') | swc_for3 : ∀e,s1,s2,k,k',u,result1,result2,new_vars. fresh_for_statement (Sfor Sskip e s1 s2) u → switch_cont_sim new_vars k k' → result1 = ret_st ? (switch_removal s1 u) → result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) → lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → switch_cont_sim new_vars (Kfor3 e s1 s2 k) (Kfor3 e result1 result2 k') | swc_switch : ∀k,k',new_vars. switch_cont_sim new_vars k k' → switch_cont_sim new_vars (Kswitch k) (Kswitch k') | swc_call : ∀en,en',r,f,k,k',old_vars,new_vars. (* Warning: possible caveat with environments here. *) switch_cont_sim old_vars k k' → old_vars = \snd (function_switch_removal f) → disjoint_extension en en' old_vars → switch_cont_sim new_vars (Kcall r f en k) (Kcall r (\fst (function_switch_removal f)) en' k'). inductive switch_state_sim (ge : genv) : state → state → Prop ≝ | sws_state : (* current statement *) ∀sss_statement : statement. (* label universe *) ∀sss_lu : universe SymbolTag. (* [sss_lu] must be fresh *) ∀sss_lu_fresh : fresh_for_statement sss_statement sss_lu. (* current function *) ∀sss_func : function. (* current function after translation *) ∀sss_func_tr : function. (* variables generated during conversion of the function *) ∀sss_new_vars : list (ident × type). (* statement of the transformation *) ∀sss_func_hyp : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func. (* memory state before conversion *) ∀sss_m : mem. (* memory state after conversion *) ∀sss_m_ext : mem. (* environment before conversion *) ∀sss_env : env. (* environment after conversion *) ∀sss_env_ext : env. (* continuation before conversion *) ∀sss_k : cont. (* continuation after conversion *) ∀sss_k_ext : cont. (* writeable blocks *) ∀sss_writeable : list block. (* memory "injection" *) ∀sss_mem_hyp : sr_memext sss_m sss_m_ext sss_writeable. (* The extended environment does not interfer with the old one. *) ∀sss_env_hyp : disjoint_extension sss_env sss_env_ext sss_new_vars. (* The new variables are allocated to a size corresponding to their types. *) ∀sss_new_alloc : (∀v.meml ? v sss_new_vars → ∀vb. lookup … sss_env_ext (\fst v) = Some ? vb → valid_block sss_m_ext vb ∧ low (blocks sss_m_ext vb) = OZ ∧ high (blocks sss_m_ext vb) = sizeof (\snd v)). (* Exit label for the enclosing switch, if any. Use for [break] conversion in switches. *) ∀sss_enclosing_label : option label. (* Extension blocks are writeable. *) ∀sss_ext_write : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable. (* conversion of the current statement, using the variables produced during the conversion of the current function *) ∀sss_result_rec. ∀sss_result_hyp : switch_removal sss_statement sss_lu = sss_result_rec. ∀sss_result. sss_result = ret_st ? sss_result_rec → (* inclusion of the locally produced new variables in the global new variables *) lset_inclusion ? (ret_vars ? sss_result_rec) sss_new_vars → (* simulation between the continuations before and after conversion. *) ∀sss_k_hyp : switch_cont_sim sss_new_vars sss_k sss_k_ext. ext_fresh_for_genv sss_new_vars ge → switch_state_sim ge (State sss_func sss_statement sss_k sss_env sss_m) (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext) | sws_callstate : ∀ssc_vf. ∀ssc_fd. ∀ssc_args. ∀ssc_k. ∀ssc_k_ext. ∀ssc_m. ∀ssc_m_ext. ∀ssc_writeable. ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable. switch_cont_sim (match ssc_fd with [ CL_Internal ssc_f ⇒ (\snd (function_switch_removal ssc_f)) | _ ⇒ [ ] ]) ssc_k ssc_k_ext → switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m) (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext) | sws_returnstate : ∀ssr_result. ∀ssr_k : cont. ∀ssr_k_ext : cont. ∀ssr_m : mem. ∀ssr_m_ext : mem. ∀ssr_writeable : list block. ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext ssr_writeable. ∀ssr_vars. switch_cont_sim ssr_vars ssr_k ssr_k_ext → switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext) | sws_finalstate : ∀r. switch_state_sim ge (Finalstate r) (Finalstate r). lemma call_cont_swremoval : ∀k,k',vars. switch_cont_sim vars k k' → switch_cont_sim vars (call_cont k) (call_cont k'). #k0 #k0' #vars #K elim K /2/ qed. (* [eventually ge P s tr] states that after a finite number of [exec_step], the property P on states will be verified. *) inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝ | eventually_base : ∀s,t,s'. exec_step ge s = Value io_out io_in ? 〈t, s'〉 → P s' → eventually ge P s t | eventually_step : ∀s,t,s',t',trace. exec_step ge s = Value io_out io_in ? 〈t, s'〉 → eventually ge P s' t' → trace = (t ⧺ t') → eventually ge P s trace. (* [eventually] is not so nice to use directly, we would like to make the mandatory * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *) lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → eventually ge P s t. #ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP} (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *) qed. lemma eventually_later : ∀ge,P,s,t. (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) → eventually ge P s t. #ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq} try assumption qed. lemma exec_lvalue_expr_elim : ∀r1,r2,Pok,Qok. exec_lvalue_sim r1 r2 → (∀val,trace. match Pok 〈val,trace〉 with [ Error err ⇒ True | OK pvt ⇒ let 〈pval,ptrace〉 ≝ pvt in match Qok 〈val,trace〉 with [ Error err ⇒ False | OK qvt ⇒ let 〈qval,qtrace〉 ≝ qvt in ptrace = qtrace ∧ pval = qval ] ]) → exec_expr_sim (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); elim r1 [ 2: #error #_ #_ normalize #a #Habsurd destruct (Habsurd) | 1: normalize nodelta #a #H lapply (H a (refl ??)) #Hr2 >Hr2 normalize #H #a' elim a * #b #o #tr lapply (H 〈b, o〉 tr) #H1 #H2 >H2 in H1; normalize nodelta elim a' in H2; #pval #ptrace #Hpok normalize nodelta cases (Qok 〈b,o,tr〉) [ 2: #error normalize #Habsurd @(False_ind … Habsurd) | 1: * #qval #qtrace normalize nodelta * #Htrace #Hval destruct @refl ] ] qed. lemma exec_expr_expr_elim : ∀r1,r2,Pok,Qok. exec_expr_sim r1 r2 → (∀val,trace. match Pok 〈val,trace〉 with [ Error err ⇒ True | OK pvt ⇒ let 〈pval,ptrace〉 ≝ pvt in match Qok 〈val,trace〉 with [ Error err ⇒ False | OK qvt ⇒ let 〈qval,qtrace〉 ≝ qvt in ptrace = qtrace ∧ pval = qval ] ]) → exec_expr_sim (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); elim r1 [ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd) | 1: normalize nodelta #a #H lapply (H a (refl ??)) #Hr2 >Hr2 normalize nodelta #H elim a in Hr2; #val #trace lapply (H … val trace) cases (Pok 〈val, trace〉) [ 2: #error normalize #_ #_ #a' #Habsurd destruct (Habsurd) | 1: * #pval #ptrace normalize nodelta cases (Qok 〈val,trace〉) [ 2: #error normalize #Hfalse @(False_ind … Hfalse) | 1: * #qval #qtrace normalize nodelta * #Htrace_eq #Hval_eq #Hr2_eq destruct #a #H @H ] ] ] qed. lemma load_value_of_type_inj : ∀m1,m2,writeable,b,off,ty. sr_memext m1 m2 writeable → ∀v. load_value_of_type ty m1 b off = Some ? v → load_value_of_type ty m2 b off = Some ? v. #m1 #m2 #writeable #b #off #ty #Hinj #v @(load_sim_fe ?? (sr_memext_load_sim … Hinj) (mk_pointer b off)) qed. (* Conservation of the semantics of binary operators under memory extensions. Tried to factorise it a bit but the play with indexes just becomes too messy. *) lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,target_type,writeable. ∀Hext:sr_memext m1 m2 writeable. ∀res. sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 target_type = Some ? res → sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 target_type = Some ? res. #op #v1 #v2 #e1 #e2 #m1 #m2 #target_type #writeable #Hmemext #res cases op whd in match (sem_binary_operation ???????); try // whd in match (sem_binary_operation ???????); lapply (me_valid_pointers … Hmemext) lapply (me_not_writeable_ptr … Hmemext) elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1 elim m2 #contents2 #nextblocks2 #Hnextpos2 * #Hnonempty #Hwriteable #Hnot_writeable #Hnot_writeable_ptr #Hvalid whd in match (sem_cmp ??????); whd in match (sem_cmp ??????); [ 1,2: cases (classify_cmp (typeof e1) (typeof e2)) normalize nodelta [ 1,4: #sz #sg try // | 2,5: #opt #ty cases v1 normalize nodelta [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ] [ 1,2,3,4: #Habsurd destruct (Habsurd) | 5,6: #H @H ] cases v2 normalize nodelta [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ] [ 1,2,3,4: #Habsurd destruct (Habsurd) | 5,6: #H @H ] lapply (Hvalid ptr) cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] #Hvalid' >(Hvalid' (refl ??)) lapply (Hvalid ptr') cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H | 3,6: #ty1 #ty2 #H @H ] | 3,4: cases (classify_cmp (typeof e1) (typeof e2)) normalize nodelta [ 1,4: #sz #sg try // | 2,5: #opt #ty cases v1 normalize nodelta [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ] [ 1,2,3,4: #Habsurd destruct (Habsurd) | 5,6: #H @H ] cases v2 normalize nodelta [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ] [ 1,2,3,4: #Habsurd destruct (Habsurd) | 5,6: #H @H ] lapply (Hvalid ptr) cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] #Hvalid' >(Hvalid' (refl ??)) lapply (Hvalid ptr') cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H | 3,6: #ty1 #ty2 #H @H ] | 5,6: cases (classify_cmp (typeof e1) (typeof e2)) normalize nodelta [ 1,4: #sz #sg try // | 2,5: #opt #ty cases v1 normalize nodelta [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ] [ 1,2,3,4: #Habsurd destruct (Habsurd) | 5,6: #H @H ] cases v2 normalize nodelta [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ] [ 1,2,3,4: #Habsurd destruct (Habsurd) | 5,6: #H @H ] lapply (Hvalid ptr) cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] #Hvalid' >(Hvalid' (refl ??)) lapply (Hvalid ptr') cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H | 3,6: #ty1 #ty2 #H @H ] ] qed. (* Simulation relation on expressions *) lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,writeable,ext. ∀Hext:sr_memext m1 m2 writeable. related_globals … fundef_switch_removal ge ge' → disjoint_extension en1 en2 ext → (* disjoint_extension en1 en2 ext Hext → *) ext_fresh_for_genv ext ge → (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ (∀ed, ty. exec_lvalue_sim (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)). #ge #ge' #en1 #m1 #en2 #m2 #writeable #ext #Hext #Hrelated #Hdisjoint (* #Hdisjoint *) #Hext_fresh_for_genv @expr_lvalue_ind_combined [ 1: #csz #cty #i #a1 whd in match (exec_expr ????); elim cty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] normalize nodelta [ 2: cases (eq_intsize csz sz) normalize nodelta [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/ | 2: #Habsurd destruct (Habsurd) ] | 3,4,5: #_ #H destruct (H) | *: #H destruct (H) ] | 2: * [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1 | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] #ty whd in ⊢ (% → ?); #Hind try @I whd in match (Plvalue ???); [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1 cases (exec_lvalue' ge en1 m1 ? ty) in Hind; [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) | 1,3,5: normalize nodelta #b1 #H lapply (H b1 (refl ??)) #Heq >Heq normalize nodelta elim b1 * #bl1 #o1 #tr1 (* elim b2 * #bl2 #o2 #tr2 *) whd in match (load_value_of_type' ???); whd in match (load_value_of_type' ???); lapply (load_value_of_type_inj m1 m2 writeable bl1 o1 ty Hext) cases (load_value_of_type ty m1 bl1 o1) [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) | 2,4,6: #v #H normalize in ⊢ (% → ?); #Heq destruct (Heq) >(H v (refl ??)) @refl ] ] ] | 3: #v #ty whd * * #b #o #tr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); cases Hdisjoint * #HA #HB #HC lapply (HA v) lapply (HB v) lapply (HC v) -HA -HB -HC lapply (Hext_fresh_for_genv v) cases (mem_assoc_env v ext) #Hglobal [ 1: >(Hglobal (refl ??)) #_ #HB #HA >(HA (refl ??)) normalize #Habsurd destruct | 2: normalize nodelta #Hsim #_ #_ cases (lookup ?? en1 v) in Hsim; normalize nodelta [ 1: #Hlookup2 <(Hlookup2 (refl ??)) normalize nodelta lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym #H @H | 2: #blo #Hlookup2 <(Hlookup2 (refl ??)) #Heq normalize nodelta @Heq ] ] | 4: #e #ty whd in ⊢ (% → %); whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); cases (exec_expr ge en1 m1 e) [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' #H @H | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] | 5: #ty #e #ty' #Hsim @(exec_lvalue_expr_elim … Hsim) cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] * #b #o normalize nodelta try /2 by I/ #tr @conj try @refl | 6: #ty #op #e #Hsim @(exec_expr_expr_elim … Hsim) #v #trace cases (sem_unary_operation op v (typeof e)) normalize nodelta try @I #v @conj @refl | 7: #ty #op #e1 #e2 #Hsim1 #Hsim2 @(exec_expr_expr_elim … Hsim1) #v #trace cases (exec_expr ge en1 m1 e2) in Hsim2; [ 2: #error // ] * #pval #ptrace normalize in ⊢ (% → ?); #Hsim2 whd in match (m_bind ?????); >(Hsim2 ? (refl ??)) whd in match (m_bind ?????); lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 ty writeable Hext) cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1 ty) [ 1: #_ // ] #val #H >(H val (refl ??)) normalize destruct @conj @refl | 8: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) #v #tr cut (exec_cast m1 v (typeof e) cast_ty = exec_cast m2 v (typeof e) cast_ty) [ @refl ] #Heq >Heq cases (exec_cast m2 v (typeof e) cast_ty) [ 2: // | 1: #v normalize @conj @refl ] | 9: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 @(exec_expr_expr_elim … Hsim1) #v #tr cases (exec_bool_of_val ? (typeof e1)) #b [ 2: normalize @I ] cases b normalize nodelta whd in match (m_bind ?????); whd in match (m_bind ?????); normalize nodelta [ 1: (* true branch *) cases (exec_expr ge en1 m1 e2) in Hsim2; [ 2: #error normalize #_ @I | 1: * #e2v #e2tr normalize #H >(H ? (refl ??)) normalize nodelta @conj @refl ] | 2: (* false branch *) cases (exec_expr ge en1 m1 e3) in Hsim3; [ 2: #error normalize #_ @I | 1: * #e3v #e3tr normalize #H >(H ? (refl ??)) normalize nodelta @conj @refl ] ] | 10,11: #ty #e1 #e2 #Hsim1 #Hsim2 @(exec_expr_expr_elim … Hsim1) #v #tr cases (exec_bool_of_val v (typeof e1)) [ 2,4: #error normalize @I ] * whd in match (m_bind ?????); whd in match (m_bind ?????); [ 2,3: cases (cast_bool_to_target ty ?) normalize // #v @conj try @refl ] cases (exec_expr ge en1 m1 e2) in Hsim2; [ 2,4: #error #_ normalize @I ] * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta >(H2 ? (refl ??)) normalize nodelta cases (exec_bool_of_val v2 (typeof e2)) [ 2,4: #error normalize @I ] * whd in match (m_bind ?????); cases (cast_bool_to_target ty ?) normalize // #v @conj try @refl | 12: #ty #ty' cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] whd in match (exec_expr ????); whd #a #H @H | 13: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty); whd in match (typeof ?); cases aggregty in Hsim; [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] normalize nodelta #Hsim [ 1,2,3,4,5,8: #Habsurd destruct (Habsurd) ] whd in match (m_bind ?????); whd in match (m_bind ?????); whd in match (exec_lvalue ge en1 m1 (Expr ed ?)); cases (exec_lvalue' ge en1 m1 ed ?) in Hsim; [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H whd in match (exec_lvalue ge' en2 m2 (Expr ed ?)); >(H ? (refl ??)) normalize nodelta #H @H | 14: #ty #l #e #Hsim @(exec_expr_expr_elim … Hsim) #v #tr normalize nodelta @conj // | 15: * [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1 | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] #ty normalize in ⊢ (% → ?); [ 2,3,12: @False_ind | *: #_ normalize #a1 #Habsurd @Habsurd ] ] qed. lemma exec_lvalue_sim_aux : ∀ge,ge',env,env_ext,m,m_ext. (∀ed,ty. exec_lvalue_sim (exec_lvalue' ge env m ed ty) (exec_lvalue' ge' env_ext m_ext ed ty)) → ∀e. exec_lvalue_sim (exec_lvalue ge env m e) (exec_lvalue ge' env_ext m_ext e). #ge #ge' #env #env_ext #m #m_ext #H * #ed #ty @H qed. lemma exec_expr_sim_to_exec_exprlist : ∀ge,ge',en1,en2,m1,m2. (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) → ∀l. res_sim ? (exec_exprlist ge en1 m1 l) (exec_exprlist ge' en2 m2 l). #ge #ge' #en1 #en2 #m1 #m2 #Hsim #l elim l [ 1: whd #a #Heq normalize in Heq ⊢ %; destruct @refl | 2: #hd #tl #Hind whd * #lv #tr whd in ⊢ ((??%?) → (??%?)); lapply (Hsim hd) cases (exec_expr ge en1 m1 hd) [ 2: #error normalize #_ #Habsurd destruct (Habsurd) | 1: * #v #vtr whd in ⊢ (% → ?); #Hsim >(Hsim ? (refl ??)) normalize nodelta cases (exec_exprlist ge en1 m1 tl) in Hind; [ 2: #error normalize #_ #Habsurd destruct (Habsurd) | 1: #a normalize #H >(H ? (refl ??)) #Heq destruct normalize @refl ] ] ] qed. (* The return type of any function is invariant under switch removal *) lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f. #f elim f #ty #args #vars #body whd in match (function_switch_removal ?); cases (switch_removal ??) * #stmt #fvs #u @refl qed. (* Similar stuff for fundefs *) lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd). * // * #ty #args #vars #body whd in ⊢ (??%%); whd in match (function_switch_removal ?); cases (switch_removal ??) * #st #u normalize nodelta #u @refl qed. lemma while_fresh_lift : ∀e,s,u. fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u. #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??)); cases (max_of_expr e) #e cases (max_of_statement s) #s normalize cases (leb e s) try /2/ qed. (* lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0). #e0 #s0 #us0 normalize cases (switch_removal s0 us0) * #body #newvars #u' normalize // qed.*) lemma dowhile_fresh_lift : ∀e,s,u. fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u. #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??)); cases (max_of_expr e) #e cases (max_of_statement s) #s normalize cases (leb e s) try /2/ qed. (* lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0). #e0 #s0 #us0 normalize cases (switch_removal s0 us0) * #body #newvars #u' normalize // qed.*) lemma for_fresh_lift : ∀cond,step,body,u. fresh_for_statement step u → fresh_for_statement body u → fresh_for_expression cond u → fresh_for_statement (Sfor Sskip cond step body) u. #cond #step #body #u whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????)); cases (max_of_statement step) #s cases (max_of_statement body) #b cases (max_of_expr cond) #c whd in match (max_of_statement Sskip); >(max_id_commutative least_identifier) >max_id_one_neutral normalize nodelta normalize elim u #u cases (leb s b) cases (leb c b) cases (leb c s) try /2/ qed. (* lemma for_commute : ∀e,stm1,stm2,u,uA. (uA=\snd  (switch_removal stm1 u)) → sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)). #e #stm1 #stm2 #u #uA #HuA whd in match (sw_rem (Sfor ????) u); whd in match (switch_removal ??); destruct normalize in match (\snd (switch_removal Sskip u)); whd in match (sw_rem stm1 u); cases (switch_removal stm1 u) * #stm1' #fresh_vars #uA normalize nodelta whd in match (sw_rem stm2 uA); cases (switch_removal stm2 uA) * #stm2' #fresh_vars2 #uB normalize nodelta // qed.*) lemma simplify_is_not_skip : ∀s. s ≠ Sskip → ∀u. ∃pf. is_Sskip (ret_st ? (switch_removal s u)) = inr ?? pf. * [ 1: * #H @(False_ind … (H (refl ??))) ] try /2/ [ 1: #s1 #s2 #_ #u normalize cases (switch_removal ? ?) * #a #b #c normalize nodelta cases (switch_removal ? ?) * #e #f #g normalize nodelta /2 by ex_intro/ | 2: #e #s1 #s2 #_ #u normalize cases (switch_removal ? ?) * #a #b #c normalize nodelta cases (switch_removal ? ?) * #e #f #g normalize nodelta /2 by ex_intro/ | 3,4: #e #s #_ #u normalize cases (switch_removal ? ?) * #e #f #g normalize nodelta /2 by ex_intro/ | 5: #s1 #e #s2 #s3 #_ #u normalize cases (switch_removal ? ?) * #a #b #c normalize nodelta cases (switch_removal ? ?) * #e #f #g normalize nodelta cases (switch_removal ? ?) * #h #i #j normalize nodelta /2 by ex_intro/ | 6: #e #ls #_ #u normalize cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta cases (fresh ??) #e #f normalize nodelta cases (fresh ? f) #g #h normalize nodelta cases (produce_cond ????) * #k #l #m normalize nodelta /2 by ex_intro/ | 7,8: #ls #st #_ #u normalize cases (switch_removal ? ?) * #e #f #g normalize nodelta /2 by ex_intro/ ] qed. (* lemma sw_rem_commute : ∀stm,u. (\fst (\fst (switch_removal stm u))) = sw_rem stm u. #stm #u whd in match (sw_rem stm u); // qed. *) lemma fresh_for_statement_inv : ∀u,s. fresh_for_statement s u → match u with [ mk_universe p ⇒ le (p0 one) p ]. * #p #s whd in match (fresh_for_statement ??); cases (max_of_statement s) #s normalize /2/ qed. lemma fresh_for_Sskip : ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u. #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. lemma fresh_for_Sbreak : ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u. #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. lemma fresh_for_Scontinue : ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u. #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. (* lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉. #s #u elim (switch_removal s u) * #res #fvs #u' %{res} %{fvs} %{u'} // qed. lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉. #switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u' %{res} %{fvs} %{u'} // qed. *) lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉. #e #ls #u #exit_label cases (produce_cond e ls u exit_label) * #s #lab #u' %{s} %{lab} %{u'} // qed. (* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *) lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false. * * * [ 1,5,9: #H @(False_ind … (H (refl ??))) | *: #_ normalize @refl ] qed. lemma exec_expr_int : ∀ge,e,m,expr. (∃sz,n,tr. exec_expr ge e m expr = (OK ? 〈Vint sz n, tr〉)) ∨ (∀sz,n,tr. exec_expr ge e m expr ≠ (OK ? 〈Vint sz n, tr〉)). #ge #e #m #expr cases (exec_expr ge e m expr) [ 2: #error %2 #sz #n #tr % #H destruct (H) | 1: * #val #trace cases val [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl | 3: | 4: #ptr ] %2 #sz #n #tr % #H destruct (H) ] qed. lemma switch_removal_elim : ∀s,u. ∃s',fvs',u'. switch_removal s u = 〈s',fvs',u'〉. #s #u cases (switch_removal s u) * #s' #fvs' #u' %{s'} %{fvs'} %{u'} @refl qed. lemma switch_removal_branches_elim : ∀ls,u. ∃ls',fvs',u'. switch_removal_branches ls u = 〈ls',fvs',u'〉. #ls #u cases (switch_removal_branches ls u) * * #ls' #fvs' #u' /4 by ex_intro/ qed. lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed. lemma simplify_switch_elim : ∀e,ls,u. ∃res,u'. simplify_switch e ls u = 〈res, u'〉. #e #ls #u cases (simplify_switch e ls u) #res #u /3 by ex_intro/ qed. lemma store_int_success : ∀b,m,sz,sg,i. valid_block m b → low (blocks m b) = OZ → high (blocks m b) = sizeof (Tint sz sg) → ∃m'. store_value_of_type (Tint sz sg) m b zero_offset (Vint sz i) = Some ? m'. #b #m #sz #sg cases sz [ 1: #i #Hvalid #Hlow #Hhigh whd in match (store_value_of_type ?????); whd in match (fe_to_be_values ??); normalize nodelta normalize in match (size_intsize ?); whd in match (bytes_of_bitvector ??); lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i <(vsplit_prod … Heq_i) normalize nodelta >(BitVector_O … ri) whd in match (storen ???); lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte li) ?) [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true >unfold_low_bound >unfold_high_bound >Hlow >Hhigh >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta @Zlt_to_Zltb_true // ] * #m' #Hbestorev >Hbestorev %{m'} @refl | 2: #i #Hvalid #Hlow #Hhigh whd in match (store_value_of_type ?????); whd in match (fe_to_be_values ??); normalize nodelta normalize in match (size_intsize ?); whd in match (bytes_of_bitvector ??); lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i <(vsplit_prod … Heq_i) normalize nodelta whd in match (storen ???); lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte li) ?) [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true >unfold_low_bound >unfold_high_bound >Hlow >Hhigh >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta @Zlt_to_Zltb_true // ] * #m0 #Hbestorev >Hbestorev normalize nodelta whd in match (bytes_of_bitvector ??); lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri <(vsplit_prod … Heq_ri) normalize nodelta cases (mem_bounds_invariant_after_bestorev … Hbestorev) * * * #Hnext0 #Hblocks0 #_ #_ #_ lapply (valid_pointer_to_bestorev_ok m0 (mk_pointer b (mk_offset [[false; false; false; false; false; false; false; false;  false; false; false; false; false; false; false; true]])) (BVByte rli) ?) [ 1: whd in match (valid_pointer ??); >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true cases (Hblocks0 b) #HA #HB >unfold_low_bound >unfold_high_bound >HA >HB >Hlow >Hhigh normalize nodelta @Zlt_to_Zltb_true normalize // ] * #m1 #Hbestorev1 %{m1} whd in ⊢ (??(???%)?); whd in match (storen ???); normalize in match (shift_pointer ???); >Hbestorev1 normalize nodelta @refl | 3: #i #Hvalid #Hlow #Hhigh whd in match (store_value_of_type ?????); whd in match (fe_to_be_values ??); normalize nodelta normalize in match (size_intsize ?); whd in match (bytes_of_bitvector ??); lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i <(vsplit_prod … Heq_i) normalize nodelta whd in match (storen ???); lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte iA) ?) [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true >unfold_low_bound >unfold_high_bound >Hlow >Hhigh >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta @Zlt_to_Zltb_true // ] * #m0 #Hbestorev >Hbestorev normalize nodelta whd in match (bytes_of_bitvector ??); lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB <(vsplit_prod … Heq_iB) normalize nodelta cases (mem_bounds_invariant_after_bestorev … Hbestorev) * * * #Hnext0 #Hblocks0 #_ #_ #_ lapply (valid_pointer_to_bestorev_ok m0 (shift_pointer 2 (mk_pointer b zero_offset) (bitvector_of_nat 2 1)) (BVByte iC) ?) [ 1: whd in match (valid_pointer ??); >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true cases (Hblocks0 b) #HA #HB >unfold_low_bound >unfold_high_bound >HA >HB >Hlow >Hhigh normalize nodelta @Zlt_to_Zltb_true normalize // ] * #m1 #Hbestorev1 whd in ⊢ (??(λ_.??(???%)?)); whd in match (storen ???); normalize in match (shift_pointer 2 (mk_pointer b zero_offset) (bitvector_of_nat 2 1)); >Hbestorev1 normalize nodelta lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD whd in match (bytes_of_bitvector ??); <(vsplit_prod … Heq_iD) normalize nodelta whd in ⊢ (??(λ_.??(???%)?)); whd in match (storen ???); cases (mem_bounds_invariant_after_bestorev … Hbestorev1) * * * #Hnext1 #Hblocks1 #_ #_ #_ lapply (valid_pointer_to_bestorev_ok m1 (shift_pointer 2 (mk_pointer b (mk_offset [[ false; false; false; false; false; false; false; false; false; false;   false; false; false; false; false; true ]])) (bitvector_of_nat 2 1)) (BVByte iE) ?) [ 1: normalize in match (shift_pointer ???); whd in match (valid_pointer ??); >Hnext1 >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true cases (Hblocks1 b) #HA #HB cases (Hblocks0 b) #HC #HD >unfold_low_bound >unfold_high_bound >HA >HB >HC >HD >Hlow >Hhigh normalize nodelta @Zlt_to_Zltb_true normalize // ] * #m2 #Hbestorev2 >Hbestorev2 normalize nodelta whd in match (bytes_of_bitvector ??); lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF <(vsplit_prod … Heq_iF) normalize nodelta >(BitVector_O … iH) whd in ⊢ (??(λ_.??(???%)?)); whd in match (storen ???); cases (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * #Hnext2 #Hblocks2 #_ #_ #_ lapply (valid_pointer_to_bestorev_ok m2 (shift_pointer 2 (shift_pointer 2 (mk_pointer b (mk_offset [[ false; false; false; false; false; false; false; false; false; false;   false; false; false; false; false; true ]])) (bitvector_of_nat 2 1)) (bitvector_of_nat 2 1)) (BVByte iG) ?) [ 1: normalize in match (shift_pointer ???); whd in match (valid_pointer ??); >Hnext2 >Hnext1 >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true cases (Hblocks2 b) #HA #HB cases (Hblocks1 b) #HC #HD cases (Hblocks0 b) #HE #HF >unfold_low_bound >unfold_high_bound >HA >HB >HC >HD >HE >HF >Hlow >Hhigh normalize nodelta @Zlt_to_Zltb_true normalize // ] * #m3 #Hbestorev3 >Hbestorev3 normalize nodelta %{m3} @refl ] qed. (* Main theorem. 9th November 2012 We decided to interrupt the development of this particular proof. What follows is a description of what has to be done in order to finish it. What has been done up to now is the simulation proof for all "easy" cases, that do not interact with the switch removal per se, plus a bit of switch. This still implies propagating the memory extension through each statement (except switch), as well as various invariants that are needed for the switch case. The proof for the switch case has been started. Here is how I picture the simulation proof. The simulation proof must be broken down in several steps. The source statement executes as this for the first step : mem, env, k ----------------------------------------------------- switch(e) case_list ===> e ⇓ Vint i, case_list' ← select_switch i case_list; Result = State (seq_of_labeled_statement case_list') (Kswitch k) env mem The resulting statement executes like this. mem ⊕ writeable, env ⊕ ext, k' fresh ∈ dom(ext) ext(fresh) ∈ writeable ----------------------------------------------------- fresh = e; if(e == case0) { --- substatement0; | goto next0; | } else { }; | if(e == case1) { |- = converted_cases label next0: | substatement1; | goto next1; | } else { }; --- ... ===> Result = State (fresh = e) (Kseq converted_cases k) (env ⊕ ext) (mem ⊕ writeable) ===> fresh ⇓ Loc l; e ⇓ Vint i; m' → store_value_of_type' (typeof a1) m l (Vint i) Result = State Sskip (Kseq converted_cases k) (env ⊕ ext) (m' ⊕ writeable) ===> Result = State converted_cases k (env ⊕ ext) (m' ⊕ writeable) This has been done. But this state is still not equivalent with the source one. TODO 1: we must prove that after a finite number of Ssequence in [converted_cases], we stumble upon a "if(e == casen) { blahblah } else {}; foo" that corresponds to "(seq_of_labeled_statement case_list')" (remember that "case_list'" has been truncated to the case corresponding to "i"). TODO 2: the resulting pair of states will not be in the standard simulation relation currently defined in [switch_state_sim]. We must come up with an additional set of relations with enough informations to handle the gotos : 1. the gotos from one if to the other avoiding the execution of conditions 2. most importantly, the gotos into which "break"s have been converted ! This particular subset of the simulation will need some equations allowing to prove that the current continuation actually contains a label corresponding to the break. Note that when encountering e.g. a while loop inside a converted case, breaks should stop beeing converted to gotos and we should go to the 'standard' simulation relation. TODO 3: some standard cases remain after that, nothing special (halt case ...). This should be about it. TODO 1 and 2 will probably require some form of induction over switch cases ... *) theorem switch_removal_correction : ∀ge,ge'. related_globals … fundef_switch_removal ge ge' → ∀s1,s1',tr,s2. switch_state_sim ge s1 s1' → exec_step ge s1 = Value … 〈tr,s2〉 → ∃n. after_n_steps (S n) … clight_exec ge' s1' (λ_. true) (λtr',s2'. tr = tr' ∧ switch_state_sim ge s2 s2'). #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state inversion Hsim_state [ 1: (* regular state *) #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp #sss_env_hyp #sss_new_alloc #sss_enclosing_label #sss_writeable_hyp #sss_result_rec #sss_result_hyp #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge #Hs1_eq #Hs1_eq' elim (sim_related_globals … ge ge' sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge) #Hsim_expr #Hsim_lvalue #_ (* II. Case analysis on the statement. *) cases sss_statement in sss_lu_fresh sss_result_hyp; (* Perform the intros for the statements *) [ 1: | 2: #lhs #rhs | 3: #retv #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 ] #sss_lu_fresh #sss_result_hyp [ 1: (* Skip statement *) whd in match (switch_removal ??) in sss_result_hyp; >sss_result_proj (prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify whd in match (exec_step ??) in Hexec_step; (* IV. Case analysis on the return type *) cases (fn_return sss_func) in Hexec_step; [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta whd in ⊢ ((??%?) → ?); [ 1: #H destruct (H) % try @refl /3 by sws_returnstate, swc_stop, memext_free_extended_environment, memory_ext_writeable_eq/ | *: #Habsurd destruct (Habsurd) ] | 2: #s #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #Hsss_k_hyp #Hexec_step %{0} whd >(prod_eq_lproj ????? sss_func_hyp) whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl (prod_eq_lproj ????? sss_func_hyp) whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl %1{ ((switch_removal (Swhile cond body) fgen))} try assumption try @refl [ 1: (Hsim_expr … Hexec) >bindIO_Value cases (exec_bool_of_val ??) [ 2: #err normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] #b whd in match (m_bind ?????); whd in match (m_bind ?????); cases b normalize nodelta #H whd in H:(??%%) ⊢ %; destruct (H) try @conj try @refl [ 1: %{u … (switch_removal (Sdowhile cond body) u)} try assumption try // [ 1: destruct normalize cases (switch_removal body u) * #body' #fvs' #u' @refl | 2: whd in match (switch_removal ??); cases (switch_removal body u) in Hincl; * #body' #fvs' #u' normalize nodelta #H @H ] | 2: %{u … (switch_removal Sskip u) } try assumption try // @(fresh_for_Sskip … Hfresh) ] | 5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step) @conj try @refl %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // assumption | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl %1{u … new_vars … sss_writeable (switch_removal stmt1 u)} try assumption try // [ 1: lapply (fresh_to_substatements … Hfresh) normalize * * // | 2: whd in match (switch_removal ??) in Hincl; cases (switch_removal stmt1 u) in Hincl; * #stmt1' #fvs1' #u' normalize nodelta cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' normalize nodelta whd in match (ret_vars ??); /2 by All_append_l/ | 3: @(swc_for3 … u) // ] | 7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // try assumption whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl | 8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl %1{sss_lu … new_vars … sss_writeable} try // try assumption destruct (sss_result_hyp) @refl | 9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') #Hexec %{0} whd in Hexec:(??%?) ⊢ %; whd in ⊢ (??%?); >(prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify cases (fn_return sss_func) in Hexec; normalize nodelta [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] (* [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] *) #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl (* JHM: do this mostly by hand, to avoid broken automation *) @(sws_returnstate ??????? (memext_free_extended_environment …) … (swc_call …)) assumption ] | 2: (* Assign statement *) lapply (exec_lvalue_sim_aux … Hsim_lvalue) #Hsim #Hexec %{0} whd in sss_result_hyp:(??%?); cases (bindIO_inversion ??????? Hexec) #xl * #Heq_lhs #Hexec_lhs cases (bindIO_inversion ??????? Hexec_lhs) #xr * #Heq_rhs #Hexec_rhs -Hexec_lhs cases (bindIO_inversion ??????? Hexec_rhs) #m' * #Heq_store #Hexec_store -Hexec_rhs whd whd in Hexec_store:(??%%) ⊢ (??%?); >sss_result_proj (Hsim … Heq_lhs) whd in match (m_bind ?????); >(Hsim_expr … Heq_rhs) >bindIO_Value lapply (memext_store_value_of_type' sss_m sss_m_ext m' sss_writeable (typeof lhs) (\fst  xl) (\fst  xr) sss_mem_hyp ?) [ 1: cases (store_value_of_type' ????) in Heq_store; [ 1: normalize #Habsurd destruct (Habsurd) | 2: #m normalize #Heq destruct (Heq) @refl ] ] * #m_ext' * #Heq_store' #Hnew_ext >Heq_store' whd in match (m_bind ?????); whd destruct @conj try @refl %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip sss_lu) } try // try assumption [ 1: @(fresh_for_Sskip … sss_lu_fresh) | 2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * * #Hvb #Hlow #Hhigh cut (store_value_of_type' (typeof lhs) sss_m (\fst  xl) (\fst  xr) = Some ? m') [ cases (store_value_of_type' (typeof lhs) sss_m (\fst  xl) (\fst  xr)) in Heq_store; [ whd in ⊢ ((??%%) → ?); #Habsurd destruct | #m0 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl ] ] #Hstore lapply (mem_bounds_after_store_value_of_type' … Heq_store') * #HA #HB cases (HB vb) #Hlow' #Hhigh' @conj try @conj [ 2: >Hlow' in Hlow; // | 3: >Hhigh' in Hhigh; // | 1: whd >HA @Hvb ] ] | 3: (* Call statement *) #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp) whd whd in ⊢ (??%?); >sss_result_proj normalize nodelta whd in Hexec:(??%?); cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args cases (bindIO_inversion ??????? Hexec_args) * #called_fundef #fid * #Heq_fundef #Hexec_typeeq cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret >(Hsim_expr … Heq_func) whd in match (m_bind ?????); >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args) whd in ⊢ (??%?); >(rg_find_funct_id … Hrelated … (opt_to_io_Value … Heq_fundef)) whd in ⊢ (??%?); Heq_assert whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret @(option_ind … retv) normalize nodelta [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl %2{sss_writeable … sss_mem_hyp} cut (sss_func_tr = \fst (function_switch_removal sss_func)) [ 1: H -H cut (sss_new_vars = \snd (function_switch_removal sss_func)) [ 1: H -H @(swc_call … sss_k_hyp) try assumption (exec_lvalue_sim_aux … Hsim_lvalue … Heq_ret) whd in ⊢ (??%?); whd @conj try @refl cut (sss_func_tr = \fst (function_switch_removal sss_func)) [ 1: H -H @(sws_callstate … sss_writeable … sss_mem_hyp) cut (sss_func_tr = \fst (function_switch_removal sss_func)) [ 1: H -H cut (sss_new_vars = \snd (function_switch_removal sss_func)) [ 1: H -H @(swc_call … sss_k_hyp) try assumption sss_result_proj HeqA normalize nodelta cases (switch_removal_elim stm2 u') #stm2' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try // try assumption [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // | 2: lapply sss_incl HeqA normalize nodelta >HeqB normalize nodelta /2 by All_append_l/ ] @(swc_seq … u') try // [ 2: >HeqB @refl | 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * #_ @fresher_for_univ lapply (switch_removal_fte stm1 sss_lu) >HeqA #H @H | 3: lapply sss_incl HeqA normalize nodelta >HeqB normalize nodelta /2 by All_append_r/ ] | 5: (* If-then-else *) #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj HeqA normalize nodelta cases (switch_removal_elim iffalse u') #iffalse' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta whd whd in ⊢ (??%?); cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hresult whd in Hresult:(??%%); destruct (Hresult) >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool whd in match (m_bind ?????); whd @conj try @refl cases b normalize nodelta [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try // [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // | 2: lapply sss_incl HeqA normalize nodelta >HeqB normalize nodelta /2 by All_append_l/ ] | 2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try // [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_ @fresher_for_univ lapply (switch_removal_fte iftrue sss_lu) >HeqA #H @H | 2: lapply sss_incl HeqA normalize nodelta >HeqB normalize nodelta /2 by All_append_r/ ] ] | 6: (* While loop *) #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj sss_result_proj HeqA normalize nodelta whd in ⊢ (? → (??%?)); >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool whd in match (m_bind ?????); cases b normalize nodelta #Hresult destruct (Hresult) whd @conj try @refl [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try // [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // | 2: lapply sss_incl HeqA normalize nodelta #H @H | 3: @(swc_while … sss_lu) try // [ 1: >HeqA @refl | 2: lapply sss_incl HeqA normalize nodelta #H @H ] ] | 2: %{… sss_func_hyp … (switch_removal Sskip u')} try assumption try // lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte; @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh) ] | 7: (* do while loop *) #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj sss_result_proj HeqA normalize nodelta whd @conj try @refl %1{sss_lu … sss_func_hyp … (switch_removal body sss_lu) } try assumption try // [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // | 2: >HeqA @refl | 3: lapply sss_incl HeqA normalize nodelta #H @H | 4: @(swc_dowhile … sss_lu) try assumption try // [ 1: >HeqA @refl | 2: lapply sss_incl HeqA normalize nodelta #H @H ] ] | 8: (* for loop *) #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj sss_result_proj HeqA normalize nodelta cases (switch_removal_elim step u') #step' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta cases (switch_removal_elim body u'') #body' * #fvs3' * #u''' #HeqC >HeqC normalize nodelta lapply Hexec @(match is_Sskip init with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ]) normalize nodelta [ 2: lapply (simplify_is_not_skip … Hneq sss_lu) >HeqA * #pf whd in match (ret_st ??) in ⊢ ((??%%) → ?); #Hneq >Hneq normalize nodelta #Hexec' whd in Hexec':(??%%); destruct (Hexec') whd @conj try @refl %1{sss_lu … sss_func_hyp (switch_removal init sss_lu)} try assumption try // [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * * * // | 2: >HeqA @refl | 3: lapply sss_incl HeqA normalize nodelta >HeqB normalize nodelta >HeqC normalize nodelta /2 by All_append_l/ | 4: @(swc_for1 … u') try assumption try // [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #HW #HX #HY #HZ @for_fresh_lift [ 1: @(fresher_for_univ … HY) | 2: @(fresher_for_univ … HZ) | 3: @(fresher_for_univ … HX) ] lapply (switch_removal_fte init sss_lu) >HeqA #Hs @Hs | 2: normalize >HeqB normalize nodelta >HeqC @refl | 3: lapply sss_incl HeqA normalize nodelta >HeqB normalize nodelta >HeqC normalize nodelta #H /2 by All_append_r/ ] ] | 1: -Hexec #Hexec' cases (bindIO_inversion ??????? Hexec') #condres * #Heq_cond #Hexec_cond cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool destruct (Heq) normalize in HeqA; lapply HeqA #HeqA' destruct (HeqA') normalize nodelta >(Hsim_expr … Heq_cond) whd in ⊢ ((??%?) → ?); #Hexec' whd in match (m_bind ?????); >Heq_bool cases b in Hexec'; normalize nodelta whd in match (bindIO ??????); normalize #Hexec'' destruct (Hexec'') @conj try @refl [ 1: %1{u'' … sss_func_hyp (switch_removal body u'')} try assumption try // [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #_ #_ #_ @fresher_for_univ lapply (switch_removal_fte step u') >HeqB #H @H | 2: >HeqC @refl | 3: lapply sss_incl HeqB normalize nodelta >HeqC normalize nodelta /2 by All_append_r/ | 4: @(swc_for2 … u') try assumption [ 1: >HeqB @refl | 2: >HeqB >HeqC @refl | 3: lapply sss_incl HeqB normalize nodelta >HeqC normalize nodelta #H @H ] ] | 2: %1{u' … sss_func_hyp … (switch_removal Sskip u')} try assumption try // @(fresh_for_Sskip … sss_lu_fresh) ] ] | 9: (* break *) (* sss_enclosing_label TODO : switch case *) #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj sss_result_proj (Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool whd in match (m_bind ?????); cases b in Hexec_bool; normalize nodelta whd in ⊢ ((??%?) → ?); #Heq whd whd in Heq:(??%%); destruct (Heq) @conj try @refl [ 1: destruct %1{uk … (switch_removal (Sdowhile ek sk) uk)} try assumption try // [ 1: normalize cases (switch_removal sk uk) * #body' #fvs' #uk' @refl | 2: whd in match (switch_removal ??); lapply Hincl cases (switch_removal sk uk) * #body' #fvs' #uk' #H @H ] | 2: destruct %1{uk … (switch_removal Sskip uk)} try assumption try // try @(fresh_for_Sskip … Hfresh_suk) ] | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl destruct %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' #Hres1 #Hres2 #Hincl #_ #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl destruct %1{uk … (switch_removal s1k uk)} try assumption try // [ 1: cases (fresh_to_substatements … Hfresh_suk) * * // | 2: lapply Hincl whd in match (ret_vars ??) in ⊢ (% → ?); whd in match (switch_removal ??); cases (switch_removal s1k uk) * #s1k' #fvs1' #uk' normalize nodelta cases (switch_removal s2k uk') * #s2k' #fvs2' #uk'' normalize nodelta /2 by All_append_l/ | 3: @(swc_for3 … uk) try assumption try // ] | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl destruct %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold_vars_eq #Hdisjoint #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) ] | 11: (* return *) #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec >sss_result_proj (prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify cases (fn_return sss_func) normalize nodelta [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] [ 1: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj try @refl /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/ | *: #Habsurd destruct (Habsurd) ] | 2: #ret_expr #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?)); >(prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify @(match type_eq_dec (fn_return sss_func) Tvoid with [ inl H ⇒ ? | inr H ⇒ ? ]) normalize nodelta [ 1: #Habsurd destruct (Habsurd) | 2: #Hexec cases (bindIO_inversion ??????? Hexec) #retres * #Heq_ret #Hexec_ret whd in Hexec_ret:(??%%); destruct (Hexec_ret) >(Hsim_expr … Heq_ret) whd in match (m_bind ?????); whd @conj try @refl /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/ ] ] | 12: (* switch ! at long last *) #Hexec whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec >sss_result_proj Htypeof_cond in Heq; normalize nodelta >sz_eq_identity normalize nodelta #Heq whd in Heq:(??%%); cases (bindIO_inversion ??????? Heq) #switchcases_truncated * #Heq1 #Heq2 -Heq whd in Heq1:(??%%); whd in Heq2:(??%%); cut (select_switch sz i switchcases = Some ? switchcases_truncated) [ 1: cases (select_switch sz i switchcases) in Heq1; normalize nodelta [ 1: #Habsurd destruct | 2: #ls #Heq destruct (Heq) @refl ] ] -Heq1 #Heq_select_switch destruct (Heq2) cases (switch_removal_branches_elim … switchcases sss_lu) #switchcases' * #fvs' * #u' #Hbranch_eq >Hbranch_eq normalize nodelta cases (fresh_elim … u') #new * #u'' #Hfresh_eq >Hfresh_eq normalize nodelta cases (simplify_switch_elim (Expr (Evar new) (Tint sz sg)) switchcases' u'') #simplified * #u''' #Hswitch_eq >Hswitch_eq normalize nodelta %{2} whd whd in ⊢ (??%?); (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *) whd in match (exec_lvalue ????); (* show that the resulting ident is in the memory extension and that the lookup succeeds *) >Hbranch_eq in sss_result_hyp; normalize nodelta >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta >Htypeof_cond >Hswitch_eq normalize nodelta #sss_result_hyp Heq -Heq normalize nodelta @refl | 2: #Hmem lapply (Hind Hmem) #Hmem_in_tl cases (identifier_eq ? new hdv) normalize nodelta [ 1: #_ @refl | 2: #_ @Hmem_in_tl ] ] ] ] #Hnew_in_new_vars lapply (Hlookup_new_in_new new Hnew_in_new_vars) * #res #Hlookup >Hlookup normalize nodelta whd in match (bindIO ??????); (* B. Reduce rhs of assign, i.e. the condition. Do this using simulation hypothesis. *) >(Hsim_expr … Hexec_eq) >bindIO_Value (* C. Execute assign. We must prove that this cannot fail. In order for the proof to proceed, we need to set up things so that loading from that fresh location will yield exactly the stored value. *) normalize in match store_value_of_type'; normalize nodelta whd in match (typeof ?); lapply (sss_new_alloc 〈new,Tint sz sg〉 ? res Hlookup) [ 1: cases sss_incl // ] * * #Hvalid #Hlow #Hhigh lapply (store_int_success … i … Hvalid Hlow Hhigh) * #m_ext' #Hstore lapply (store_value_load_value_compatible … Hstore) // #Hload_value_correct >Hstore whd in match (m_bind ?????); whd @conj try // cut (mem block res sss_writeable) [ 1: @cthulhu ] (* lapply (memext_store_value_of_type_writeable … sss_mem_hyp … Hstore) *) @cthulhu | *: @cthulhu ] | *: @cthulhu ] qed. lemma initial_state_in_switch_simulation : ∀p,s. make_initial_state p = OK ? s → ∃s'. make_initial_state (program_switch_removal p) = OK ? s' ∧ related_globals … fundef_switch_removal (make_global p) (make_global (program_switch_removal p)) ∧ switch_state_sim (make_global p) s s'. * #vars #fns #main #s whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX cases (bind_inversion ????? EX) -EX #m * #Em #EX cases (bind_inversion ????? EX) -EX #b * #Emain #EX cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX whd in EX:(??%%); destruct whd in match (make_initial_state ?); letin ge' ≝ (make_global ?) cut (related_globals … fundef_switch_removal ge ge') [ // ] #RG lapply (rg_find_funct_ptr … RG … Emain') #FFP % [2: % [ % [whd in ⊢ (??%?); change with (transform_program ??? (mk_program …) (λ_.?)) in match (mk_program ??? (transf_program ????) ?); >(init_mem_transf … (mk_program ?? vars fns main)) >Em in ⊢ (??%?); whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?); whd in ⊢ (??%?); >FFP in ⊢ (??%?); whd in ⊢ (??%?); @refl | /3/ ] | /3/ ] | skip ] qed. lemma switch_final_related : ∀ge1,s1,s2. switch_state_sim ge1 s1 s2 → is_final s1 = is_final s2. #Xge #Xs1 #Xs2 * // qed.