Changeset 2438


Ignore:
Timestamp:
Nov 7, 2012, 11:18:56 AM (7 years ago)
Author:
garnier
Message:

Sync of the w.i.p. for switch removal.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2386 r2438  
    22
    33include "Clight/TypeComparison.ma".
     4include "Clight/Csem.ma".
    45include "common/Pointers.ma".
    56include "basics/jmeq.ma".
    67include "basics/star.ma". (* well-founded relations *)
     8include "common/IOMonad.ma".
     9include "common/IO.ma".
    710include "basics/lists/listb.ma".
    811include "basics/lists/list.ma".
    9 
    1012
    1113(* --------------------------------------------------------------------------- *)
     
    3234
    3335lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed.
     36
     37lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.
     38
     39lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c.
     40#A #B #a #b * #a' #b' #H destruct @refl
     41qed.
     42
     43lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c.
     44#A #B #a #b * #a' #b' #H destruct @refl
     45qed.
     46
     47lemma bindIO_Error : ∀err,f. bindIO io_out io_in (val×trace) (trace×state) (Error … err) f = Wrong io_out io_in (trace×state) err.
     48// qed.
     49
     50lemma bindIO_Value : ∀v,f. bindIO io_out io_in (val×trace) (trace×state) (Value … v) f = (f v).
     51// qed.
     52
     53lemma bindIO_elim :
     54         ∀A.
     55         ∀P : (IO io_out io_in A) → Prop.
     56         ∀e : res A. (*IO io_out io_in A.*)
     57         ∀f.
     58         (∀v. (e:IO io_out io_in A) = OK … v →  P (f v)) →
     59         (∀err. (e:IO io_out io_in A) = Error … err →  P (Wrong ??? err)) →
     60         P (bindIO io_out io_in ? A (e:IO io_out io_in A) f).
     61#A #P * try /2/ qed.
     62
     63lemma opt_to_io_Value :
     64  ∀A,B,C,err,x,res. opt_to_io A B C err x = return res → x = Some ? res.
     65#A #B #C #err #x cases x normalize
     66[ 1: #res #Habsurd destruct
     67| 2: #c #res #Heq destruct @refl ]
     68qed. 
     69
     70lemma some_inversion :
     71  ∀A,B:Type[0].
     72  ∀e:option A.
     73  ∀res:B.
     74  ∀f:A → option B.
     75 match e with
     76 [ None ⇒ None ?
     77 | Some x ⇒ f x ] = Some ? res →
     78 ∃x. e = Some ? x ∧ f x = Some ? res.
     79 #A #B #e #res #f cases e normalize nodelta
     80[ 1: #Habsurd destruct (Habsurd)
     81| 2: #a #Heq %{a} @conj >Heq @refl ]
     82qed.
     83
     84lemma cons_inversion :
     85  ∀A,B:Type[0].
     86  ∀e:list A.
     87  ∀res:B.
     88  ∀f:A → list A → option B.
     89 match e with
     90 [ nil ⇒ None ?
     91 | cons hd tl ⇒ f hd tl ] = Some ? res →
     92 ∃hd,tl. e = hd::tl ∧ f hd tl = Some ? res.
     93#A #B #e #res #f cases e normalize nodelta
     94[ 1: #Habsurd destruct (Habsurd)
     95| 2: #hd #tl #Heq %{hd} %{tl} @conj >Heq @refl ]
     96qed.
     97
     98lemma if_opt_inversion :
     99  ∀A:Type[0].
     100  ∀x.
     101  ∀y:A.
     102  ∀e:bool.
     103 (if e then
     104    x
     105  else
     106    None ?) = Some ? y →
     107 e = true ∧ x = Some ? y.
     108#A #x #y * normalize
     109#H destruct @conj @refl
     110qed.
     111
     112lemma andb_inversion :
     113  ∀a,b : bool. andb a b = true → a = true ∧ b = true.
     114* * normalize /2 by conj, refl/ qed. 
     115
     116lemma identifier_eq_i_i : ∀tag,i. ∃pf. identifier_eq tag i i = inl … pf.
     117#tag #i cases (identifier_eq ? i i)
     118[ 1: #H %{H} @refl
     119| 2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ]
     120qed.
    34121
    35122(* --------------------------------------------------------------------------- *)
     
    120207
    121208lemma free_not_valid : ∀x. if Zleb (pos one) x
    122                             then Zleb x OZ 
     209                            then Zltb x OZ 
    123210                            else false = false.
    124211#x
    125 cut (Zle (pos one) x ∧ Zle x OZ → False)
    126 [ * #H1 #H2 lapply (transitive_Zle … H1 H2) #H @H ] #Hguard
    127 cut (Zleb (pos one) x = true ∧ Zleb x OZ = true → False)
    128 [ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ ]
    129 cases (Zleb (pos one) x) cases (Zleb x OZ)
     212cut (Zle (pos one) x ∧ Zlt x OZ → False)
     213[ * #H1 #H2 lapply (transitive_Zle … (monotonic_Zle_Zsucc … H1) (Zlt_to_Zle … H2)) #H @H ] #Hguard
     214cut (Zleb (pos one) x = true ∧ Zltb x OZ = true → False)
     215[ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ @Zltb_true_to_Zlt assumption ]
     216cases (Zleb (pos one) x) cases (Zltb x OZ)
    130217/2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??))))
    131218qed.
     
    219306lemma nil_append : ∀A. ∀(l : list A). [ ] @ l = l. // qed.
    220307
     308alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
     309
    221310lemma mem_append : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) ↔ (mem … elt l1) ∨ (mem … elt l2).
    222311#A #elt #l1 elim l1
    223312[ 1: #l2 normalize @conj [ 1: #H %2 @H | 2: * [ 1: @False_ind | 2: #H @H ] ]
    224313| 2: #hd #tl #Hind #l2 @conj
    225      [ 1: whd in match (mem ???); *
     314     [ 1: whd in match (meml ???); *
    226315          [ 1: #Heq >Heq %1 normalize %1 @refl
    227316          | 2: #H1 lapply (Hind l2) * #HA #HB normalize
  • src/Clight/memoryInjections.ma

    r2385 r2438  
    250250     #H1 #H2 >H1 >H2 @refl
    251251] qed.
     252
     253lemma addition_n_direct_ok2 : ∀n,carry,v1,v2.
     254  (let 〈a,b〉 ≝ add_with_carries n v1 v2 carry in a) = addition_n_direct n v1 v2 carry.
     255#n #carry #v1 #v2 <addition_n_direct_ok
     256cases (add_with_carries ????) //
     257qed.
    252258 
    253259(* trivially lift associativity to our new setting *)     
     
    271277definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
    272278definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
     279
    273280
    274281(* fold andb on a bitvector. *)
     
    500507>neutral_addition_n_direct @refl
    501508qed.
     509
     510lemma increment_direct_ok : ∀n,v. increment_direct n v = increment n v.
     511#n #v whd in match (increment ??);
     512>addition_n_direct_ok <increment_to_carry_zero @refl
     513qed.
    502514
    503515(* Prove -(a + b) = -a + -b *)
     
    10861098#ty #m #b #off #v #Haccess_mode #Hload normalize
    10871099elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
    1088 * #H1 #H2 #H3 >H1 >H2 normalize nodelta
    1089 >Zle_to_Zleb_true try //
    1090 lapply (Zlt_to_Zle … (Zltb_true_to_Zlt … H3)) /2/
    1091 qed.
    1092 
     1100* #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @I
     1101qed.
    10931102
    10941103(* Making explicit the contents of memory_inj for load_value_of_type *)
     
    19962005   cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
    19972006
     2007(* 5 Nov. 2012 : the rest of the stuff doesn't checks anymore. Not a big deal, it was here
     2008 * for historical purposes, and for potential inspiration for Clight to Cminor. I leave the
     2009 * code commented for future reference.
     2010 *)
     2011
     2012(*
    19982013lemma cmp_value_eq :
    19992014  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
     
    20232038     [ 1,3: #Hneq #Habsurd destruct (Habsurd)
    20242039     | 2,4: #Heq destruct (Heq) normalize nodelta
    2025             #Heq destruct (Heq)     
     2040            #Heq destruct (Heq)
    20262041            [ 1: cases (cmp_int ????) whd in match (of_bool ?);
    20272042            | 2: cases (cmpu_int ????) whd in match (of_bool ?); ]
     
    20432058     /3 by ex_intro, conj, vint_eq/
    20442059| 4: #ty1 #ty2 #Habsurd destruct (Habsurd)
    2045 | 2: #optn #typ             
     2060| 2: #optn #typ
    20462061     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
    20472062     [ 1: #v #Habsurd destruct (Habsurd)
     
    20942109          /3 by ex_intro, conj, vint_eq/
    20952110     ]
    2096 ] qed.               
    2097 
     2111] qed.    *)           
     2112
     2113(*
    20982114lemma binary_operation_value_eq :
    20992115  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
     
    21192135| 10: @shr_value_eq try assumption
    21202136| *: @cmp_value_eq try assumption
    2121 ] qed.
    2122 
     2137] qed. *)
     2138
     2139(*
    21232140lemma cast_value_eq :
    21242141 ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 →
     
    22172234| 2: #p1 #p2 #Hembed #H @H ] qed.
    22182235
    2219 
     2236*)
    22202237(*
    22212238lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
  • src/Clight/switchRemoval.ma

    r2391 r2438  
    99include "basics/lists/list.ma".
    1010include "basics/lists/listb.ma".
     11include "Clight/SimplifyCasts.ma".
     12
    1113
    1214
     
    204206     normalize @conj try @conj try @conj try @conj try //
    205207     @(convert_break_lift ?? Hsf)
    206 ] qed.
     208] qed. 
    207209
    208210(* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in
    209211   order to circumvent the associativity problems in notations. *)
     212(*
    210213record swret (A : Type[0]) : Type[0] ≝ {
    211214  ret_st  : A;
    212215  ret_acc : list (ident × type);
    213   ret_fvs : list ident;
    214216  ret_u   : universe SymbolTag
    215217}.
    216218
    217 notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48
    218 for @{ match ${e} with
    219        [ None ⇒ None ?
    220        | Some ${fresh ret} ⇒
    221           (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'})
    222           (ret_st ? ${fresh ret})
    223           (ret_acc ? ${fresh ret})
    224           (ret_fvs ? ${fresh ret})
    225           (ret_u ? ${fresh ret}) ] }.
    226 
    227 notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49
    228 for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4})  }.
     219notation > "vbox('let' 〈ident v1, ident v2, ident v3〉 ≝ e in break e')" with precedence 48
     220for @{ (λ${ident v1}.λ${ident v2}.λ${ident v3}. ${e'})
     221          (ret_st ? ${e})
     222          (ret_acc ? ${e})
     223          (ret_u ? ${e}) }.
     224
     225definition ret ≝ λe1,e2,e3. mk_swret statement e1 e2 e3. *)
    229226     
    230227(* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list
     
    234231let rec switch_removal
    235232  (st : statement)           (* the statement in which we will remove switches *)
    236   (fvs : list ident)         (* a finite list of names usable to create variables. *)
    237   (u : universe SymbolTag)   (* a fresh /label/ generator *)
    238   : option (swret statement) ≝
     233  (u : universe SymbolTag)   (* a fresh label and ident generator *)
     234  : statement × (list (ident × type)) × (universe SymbolTag) ≝
    239235match st with
    240 [ Sskip       ⇒ ret 〈st, [ ], fvs, u〉
    241 | Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉
    242 | Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉
     236[ Sskip       ⇒ 〈st, [ ], u〉
     237| Sassign _ _ ⇒ 〈st, [ ], u〉
     238| Scall _ _ _ ⇒ 〈st, [ ], u〉
    243239| Ssequence s1 s2 ⇒
    244   do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
    245   do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
    246   ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉
     240  let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in
     241  let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in
     242  〈Ssequence s1' s2', acc1 @ acc2, u''〉
    247243| Sifthenelse e s1 s2 ⇒
    248   do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
    249   do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
    250   ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
     244  let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in
     245  let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in
     246  〈Sifthenelse e s1' s2', acc1 @ acc2, u''〉
    251247| Swhile e body ⇒
    252   do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    253   ret 〈Swhile e body', acc, fvs', u'〉
     248  let 〈body', acc, u'〉 ≝ switch_removal body u in
     249  〈Swhile e body', acc, u'〉
    254250| Sdowhile e body ⇒
    255   do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    256   ret 〈Sdowhile e body', acc, fvs', u'〉
     251  let 〈body', acc, u'〉 ≝ switch_removal body u in
     252  〈Sdowhile e body', acc, u'〉
    257253| Sfor s1 e s2 s3 ⇒
    258   do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
    259   do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
    260   do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';
    261   ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉
     254  let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in
     255  let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in
     256  let 〈s3', acc3, u'''〉 ≝ switch_removal s3 u'' in
     257  〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, u'''〉
    262258| Sbreak ⇒
    263   ret 〈st, [ ], fvs, u〉
     259  〈st, [ ], u〉
    264260| Scontinue ⇒
    265   ret 〈st, [ ], fvs, u〉
     261  〈st, [ ], u〉
    266262| Sreturn _ ⇒
    267   ret 〈st, [ ], fvs, u〉
     263  〈st, [ ], u〉
    268264| Sswitch e branches ⇒   
    269    do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u;
    270    match fvs' with
    271    [ nil ⇒ None ?
    272    | cons fresh tl ⇒
    273      (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *)
    274      let ident         ≝ Expr (Evar fresh) (typeof e) in
    275      let assign        ≝ Sassign ident e in
    276      let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in
    277        ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉
    278    ]
     265  let 〈sf_branches, acc, u'〉 ≝ switch_removal_branches branches u in
     266  let 〈switch_tmp, u''〉 ≝ fresh ? u' in
     267  let ident         ≝ Expr (Evar switch_tmp) (typeof e) in
     268  let assign        ≝ Sassign ident e in
     269  let 〈result, u'''〉 ≝ simplify_switch ident sf_branches u'' in
     270  〈Ssequence assign result, (〈switch_tmp, typeof e〉 :: acc), u'''〉
    279271| Slabel label body ⇒
    280   do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    281   ret 〈Slabel label body', acc, fvs', u'〉
     272  let 〈body', acc, u'〉 ≝ switch_removal body u in
     273  〈Slabel label body', acc, u'〉
    282274| Sgoto _ ⇒
    283   ret 〈st, [ ], fvs, u〉
     275  〈st, [ ], u〉
    284276| Scost cost body ⇒
    285   do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    286   ret 〈Scost cost body', acc, fvs', u'〉
     277  let 〈body', acc, u'〉 ≝ switch_removal body u in
     278  〈Scost cost body', acc, u'〉
    287279]
    288280
    289281and switch_removal_branches
    290282  (l : labeled_statements)
    291   (fvs : list ident)
    292283  (u : universe SymbolTag)
    293 (*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
     284 : (labeled_statements × (list (ident × type)) × (universe SymbolTag)) ≝
    294285match l with
    295286[ LSdefault st ⇒
    296   do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;
    297   ret 〈LSdefault st', acc1, fvs', u'〉
    298 | LScase sz int st tl =>
    299   do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u;
    300   do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u';
    301   ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉
     287  let 〈st', acc1, u'〉 ≝ switch_removal st u in
     288  〈LSdefault st', acc1, u'〉
     289| LScase sz int st tl
     290  let 〈tl_result, acc1, u'〉 ≝ switch_removal_branches tl u in
     291  let 〈st', acc2, u''〉 ≝ switch_removal st u' in
     292  〈LScase sz int st' tl_result, acc1 @ acc2, u''〉
    302293].
    303294
    304 let rec mk_fresh_variables
    305   (st : statement)           (* the statement in which we will remove switches *)
    306   (u : universe SymbolTag)   (* a fresh /label/ generator *)
    307   : (list ident) × (universe SymbolTag) ≝
    308 match st with
    309 [ Sskip       ⇒ 〈[ ], u〉
    310 | Sassign _ _ ⇒ 〈[ ], u〉
    311 | Scall _ _ _ ⇒ 〈[ ], u〉
    312 | Ssequence s1 s2 ⇒
    313   let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
    314   let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    315   〈fvs @ fvs', u''〉
    316 | Sifthenelse e s1 s2 ⇒
    317   let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
    318   let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    319   〈fvs @ fvs', u''〉
    320 | Swhile e body ⇒
    321   mk_fresh_variables body u
    322 | Sdowhile e body ⇒
    323   mk_fresh_variables body u
    324 | Sfor s1 e s2 s3 ⇒
    325   let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
    326   let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    327   let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in
    328   〈fvs @ fvs' @fvs'', u'''〉
    329 | Sbreak ⇒
    330   〈[ ], u〉
    331 | Scontinue ⇒
    332   〈[ ], u〉
    333 | Sreturn _ ⇒
    334   〈[ ], u〉
    335 | Sswitch e branches ⇒   
    336    let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *)
    337    let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in
    338    〈fvs @ [ident], u''〉  (* reversing the order to match a proof invariant *)
    339 | Slabel label body ⇒
    340   mk_fresh_variables body u
    341 | Sgoto _ ⇒
    342   〈[ ], u〉
    343 | Scost cost body ⇒
    344   mk_fresh_variables body u
    345 ]
    346 
    347 and mk_fresh_variables_branches
    348   (l : labeled_statements)
    349   (u : universe SymbolTag)
    350 (*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
    351 match l with
    352 [ LSdefault st ⇒
    353   mk_fresh_variables st u
    354 | LScase sz int st tl =>
    355   let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in
    356   let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in
    357   〈fvs @ fvs', u''〉
    358 ].
    359 
    360 (* Copied this from Csyntax.ma, lifted from Prop to Type
    361    (I needed to eliminate something proved with this towards Type)  *)
    362 let rec statement_indT
    363   (P:statement → Type[1]) (Q:labeled_statements → Type[1])
    364   (Ssk:P Sskip)
    365   (Sas:∀e1,e2. P (Sassign e1 e2))
    366   (Sca:∀eo,e,args. P (Scall eo e args))
    367   (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    368   (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    369   (Swh:∀e,s. P s → P (Swhile e s))
    370   (Sdo:∀e,s. P s → P (Sdowhile e s))
    371   (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
    372   (Sbr:P Sbreak)
    373   (Sco:P Scontinue)
    374   (Sre:∀eo. P (Sreturn eo))
    375   (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
    376   (Sla:∀l,s. P s → P (Slabel l s))
    377   (Sgo:∀l. P (Sgoto l))
    378   (Scs:∀l,s. P s → P (Scost l s))
    379   (LSd:∀s. P s → Q (LSdefault s))
    380   (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
    381   (s:statement) on s : P s ≝
    382 match s with
    383 [ Sskip ⇒ Ssk
    384 | Sassign e1 e2 ⇒ Sas e1 e2
    385 | Scall eo e args ⇒ Sca eo e args
    386 | Ssequence s1 s2 ⇒ Ssq s1 s2
    387     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    388     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    389 | Sifthenelse e s1 s2 ⇒ Sif e s1 s2
    390     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    391     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    392 | Swhile e s ⇒ Swh e s
    393     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    394 | Sdowhile e s ⇒ Sdo e s
    395     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    396 | Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
    397     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    398     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    399     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
    400 | Sbreak ⇒ Sbr
    401 | Scontinue ⇒ Sco
    402 | Sreturn eo ⇒ Sre eo
    403 | Sswitch e ls ⇒ Ssw e ls
    404     (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
    405 | Slabel l s ⇒ Sla l s
    406     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    407 | Sgoto l ⇒ Sgo l
    408 | Scost l s ⇒ Scs l s
    409     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    410 ]
    411 and labeled_statements_indT
    412   (P:statement → Type[1]) (Q:labeled_statements → Type[1])
    413   (Ssk:P Sskip)
    414   (Sas:∀e1,e2. P (Sassign e1 e2))
    415   (Sca:∀eo,e,args. P (Scall eo e args))
    416   (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    417   (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    418   (Swh:∀e,s. P s → P (Swhile e s))
    419   (Sdo:∀e,s. P s → P (Sdowhile e s))
    420   (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
    421   (Sbr:P Sbreak)
    422   (Sco:P Scontinue)
    423   (Sre:∀eo. P (Sreturn eo))
    424   (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
    425   (Sla:∀l,s. P s → P (Slabel l s))
    426   (Sgo:∀l. P (Sgoto l))
    427   (Scs:∀l,s. P s → P (Scost l s))
    428   (LSd:∀s. P s → Q (LSdefault s))
    429   (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
    430   (ls:labeled_statements) on ls : Q ls ≝
    431 match ls with
    432 [ LSdefault s ⇒ LSd s
    433     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    434 | LScase sz i s t ⇒ LSc sz i s t
    435     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    436     (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
    437 ].
    438 
    439 lemma switch_removal_ok :
    440   ∀st, u0, u1, post.
    441   Σresult.
    442   (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post).
    443 #st
    444 @(statement_indT ? (λls. ∀u0, u1, post.
    445                           Σresult.
    446                           (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result)
    447                           ∧ (ret_fvs ? result = post)
    448                    ) … st)
    449 [ 1: #u0 #u1 #post normalize
    450      %{(mk_swret statement Sskip [] post u1)} % //
    451 | 2: #e1 #e2 #u0 #u1 #post normalize
    452      %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try //
    453 | 3: #e0 #e #args #u0 #u1 #post normalize
    454      %{(mk_swret statement (Scall e0 e args) [] post u1)} % try //
    455 | 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
    456      elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *     
    457      cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
    458      elim (H2 u' (ret_u ? s1') post) #s2' *
    459      cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
    460      #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
    461      %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2'))
    462         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
    463         (ret_u statement s2'))} % try //
    464 | 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
    465      elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *     
    466      cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
    467      elim (H2 u' (ret_u ? s1') post) #s2' *
    468      cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
    469      #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
    470      %{((mk_swret statement
    471          (Sifthenelse e (ret_st statement s1') (ret_st statement s2'))
    472          (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
    473          (ret_u statement s2')))} % try //
    474 | 6: #e #s #H #u0 #u1 #post normalize
    475      elim (H u0 u1 post) #s1' * normalize
    476      cases (mk_fresh_variables s u0) #fvs #u'
    477      #Heq1 #Heq1_fvs >Heq1 normalize nodelta
    478      %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1')
    479         (ret_fvs statement s1') (ret_u statement s1'))} % try //
    480 | 7: #e #s #H #u0 #u1 #post normalize
    481      elim (H u0 u1 post) #s1' * normalize
    482      cases (mk_fresh_variables s u0) #fvs #u'
    483      #Heq1 #Heq1_fvs >Heq1 normalize nodelta
    484      %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1')
    485         (ret_fvs statement s1') (ret_u statement s1'))} % try //
    486 | 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize
    487      elim (H1 u0 u1
    488                 (\fst (mk_fresh_variables s2 (\snd  (mk_fresh_variables s1 u0))) @
    489                 (\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @
    490                 post)) #s1' *
    491      cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
    492      elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 u')))) @
    493                                  post)) #s2' *
    494      cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
    495      elim (H3 u'' (ret_u ? s2') post) #s3' *
    496      cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta
    497      #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs
    498      >associative_append >associative_append >Heq1 normalize >Heq1_fvs
    499      >Heq2 normalize >Heq2_fvs >Heq3 normalize
    500      %{(mk_swret statement
    501         (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3'))
    502         (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3')
    503         (ret_fvs statement s3') (ret_u statement s3'))} % try //
    504 | 9:  #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % //
    505 | 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % //
    506 | 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % //
    507 | 12: #e #ls #H #u0 #u1 #post
    508       whd in match (mk_fresh_variables ??);
    509       whd in match (switch_removal ???);     
    510       elim (fresh ? u0) #fresh #u'
    511       elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta
    512       cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta     
    513       >associative_append #Heq #Heq_fvs >Heq normalize nodelta
    514       >Heq_fvs normalize nodelta
    515       cases (simplify_switch ???) #st' #u''' normalize nodelta
    516       %{((mk_swret statement
    517           (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st')
    518           (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post)
    519           (ret_u labeled_statements ls')))} % //
    520 | 13: #l #s #H #u0 #u1 #post normalize
    521       elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
    522       %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s')
    523            post (ret_u statement s'))} % //
    524 | 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % //
    525 | 15: #l #s #H #u0 #u1 #post normalize
    526       elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
    527       %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s')
    528            post (ret_u statement s'))} % //
    529 | 16: #s #H #u0 #u1 #post normalize
    530       elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
    531       %{(mk_swret labeled_statements (LSdefault (ret_st statement s'))
    532          (ret_acc statement s') post (ret_u statement s'))} % //
    533 | 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize
    534       elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' *
    535       cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize
    536       elim (H1 u' (ret_u labeled_statements ls') post) #s1' *
    537       cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs
    538       >associative_append >Heql normalize >Heql_fvs >Heq normalize
    539       %{(mk_swret labeled_statements
    540           (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls'))
    541           (ret_acc labeled_statements ls'@ret_acc statement s1')
    542           (ret_fvs statement s1') (ret_u statement s1'))} % //
    543 ] qed.
     295definition ret_st : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → A ≝
     296λA,x.
     297  let 〈s,vars,u〉 ≝ x in s.
     298
     299definition ret_vars : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → list (ident × type) ≝
     300λA,x.
     301  let 〈s,vars,u〉 ≝ x in vars.
     302
     303definition ret_u : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → (universe SymbolTag) ≝
     304λA,x.
     305  let 〈s,vars,u〉 ≝ x in u.
    544306
    545307axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
    546308
    547309(* Proof that switch_removal_switch_free does its job. *)
    548 lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result).
    549 #st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result →
    550                                                  branches_switch_free (ret_st ? ls_result)) … st)
    551 [ 1: #fvs #u #result normalize #Heq destruct (Heq) //
    552 | 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) //
    553 | 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) //
    554 | 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u)
    555      elim (switch_removal s1 fvs u) normalize
    556      [ 1: #_ #Habsurd destruct (Habsurd)
    557      | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1))
    558           elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1))
    559           [ 1: normalize #_ #Habsurd destruct (Habsurd)
    560           | 2: normalize #res2 #Heq2 #Heq destruct (Heq)
    561                normalize @conj
    562                [ 1: @Heq1 // | 2: @Heq2 // ]
    563      ] ]
     310lemma switch_removal_switch_free : ∀st,u. switch_free (ret_st ? (switch_removal st u)).
     311#st @(statement_ind2 ? (λls. ∀u. branches_switch_free (ret_st ? (switch_removal_branches ls u))) … st)
     312try //
     313[ 1: #s1 #s2 #H1 #H2 #u normalize
     314     lapply (H1 u)
     315     cases (switch_removal s1 u) * #st1 #vars1 #u' normalize #HA
     316     lapply (H2 u')
     317     cases (switch_removal s2 u') * #st2 #vars2 #u'' normalize #HB
     318     @conj assumption
    564319| *:
    565320  (* TODO the first few cases show that the lemma is routinely proved. TBF later. *)
     
    623378  max_id (max_of_expr f)
    624379         (max_id retmax
    625                  (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) )
     380                 (foldr ?? (λelt,acc. max_id (max_of_expr elt) acc) least_identifier args) )
    626381| Ssequence s1 s2 ⇒
    627382  max_id (max_of_statement s1) (max_of_statement s2)
     
    663418definition function_switch_removal : function → function × (list (ident × type)) ≝
    664419λf.
    665   (λres_record.
    666     let new_vars ≝ ret_acc ? res_record in
    667     let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in
    668     〈result, new_vars〉)
    669   (let u ≝ universe_of_max (max_id_of_function f) in
    670    let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in
    671    match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with
    672    [ None ⇒ λHsr. ?
    673    | Some res_record ⇒ λ_. res_record
    674    ] (refl ? (switch_removal (fn_body f) fvs u'))).   
    675 lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq
    676 <Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd)
    677 qed.
     420  let u ≝ universe_of_max (max_id_of_function f) in
     421  let 〈st, vars, u'〉 ≝ switch_removal (fn_body f) u in
     422  let result ≝ mk_function (fn_return f) (fn_params f) (vars @ (fn_vars f)) st in
     423  〈result, vars〉.
    678424
    679425let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝
     
    695441  sf_funcs
    696442  (prog_main … p).
    697 
    698443
    699444(* -----------------------------------------------------------------------------
     
    742487#H1 #H2 destruct (H2) /2/ qed.
    743488
    744 lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'.
    745 #u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh)
    746 cases (fresh SymbolTag u)
    747 #fv #u' #H %{fv} %{u'} @conj try // @H //
    748 qed.
     489definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝
     490λu1,u2.
     491  match u1 with
     492  [ mk_universe p1 ⇒
     493    match u2 with
     494    [ mk_universe p2 ⇒ p2 ≤ p1 ] ].
     495   
     496definition fte ≝ fresher_than_or_equal.
     497
     498lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3.
     499* #u1 * #u2 * #u3 normalize /2 by transitive_le/
     500qed.
     501
     502lemma reflexive_fte : ∀u. fte u u.
     503* // qed.
     504
     505lemma fresher_for_univ : ∀u1,u2. fte u1 u2 → ∀i. fresh_for_univ ? i u2 → fresh_for_univ ? i u1.
     506* #p * #p' normalize #H * #i normalize
     507/2 by transitive_le/
     508qed.
     509
     510lemma fresh_fte : ∀u2,u1,fv. fresh ? u2 = 〈fv,u1〉 → fte u1 u2.
     511* #u1 * #u2 * #fv normalize #H1 destruct //
     512qed.
     513
     514lemma produce_cond_fte : ∀e,exit,ls,u. fte (\snd (produce_cond e ls u exit)) u.
     515#e #exit #ls @(branches_ind … ls)
     516[ 1: #st #u normalize lapply (fresh_fte u)
     517     cases (fresh ? u) #lab #u1 #H lapply (H u1 lab (refl ??)) normalize //
     518| 2: #sz #i #hd #tl #Hind #u normalize
     519     lapply (Hind u) cases (produce_cond e tl u exit) *
     520     #subcond #sublabel #u1 #Hfte normalize
     521     lapply (fresh_fte u1)
     522     cases (fresh ? u1) #lab #u2 #H2 lapply (H2 u2 lab (refl ??))
     523     #Hfte' normalize cases u2 in Hfte'; #u2
     524     cases u in Hfte; #u cases u1 #u1 normalize
     525     /2 by transitive_le/
     526] qed.
    749527
    750528lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)).
    751 #e #exit #ls @(branches_ind … ls)
    752 [ 1: #st #u #i #Hfresh normalize
    753      lapply (fresh_for_univ_still_fresh … Hfresh)
    754      cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize //
    755 | 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize
    756      lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) *
    757      #subcond #sublabel #u1 #Hfresh1 normalize
    758      lapply (fresh_for_univ_still_fresh … Hfresh1)
    759      cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize //
    760 ] qed.
    761 
    762 lemma simplify_switch_fresh : ∀u,i,e,ls.
    763  fresh_for_univ ? i u →
     529#e #exit #ls #u #i @fresher_for_univ @produce_cond_fte qed.
     530
     531lemma simplify_switch_fte : ∀u,e,ls.
     532  fte (\snd (simplify_switch e ls u)) u.
     533#u #e #ls normalize
     534lapply (fresh_fte u)
     535cases (fresh ? u)
     536#exit_label #uv1 #Haux lapply (Haux uv1 exit_label (refl ??)) -Haux #Haux
     537normalize
     538lapply (produce_cond_fte e exit_label ls uv1)
     539cases (produce_cond ????) * #stm #label #uv2 normalize nodelta
     540cases uv2 #uv2 cases uv1 in Haux; #uv1 cases u #u normalize
     541/2 by transitive_le/
     542qed.
     543
     544lemma simplify_switch_fresh : ∀u,i,e,ls.
     545 fresh_for_univ ? i u →
    764546 fresh_for_univ ? i (\snd (simplify_switch e ls u)).
    765 #u #i #e #ls #Hfresh
    766 normalize
    767 lapply (fresh_for_univ_still_fresh … Hfresh)
    768 cases (fresh ? u)
    769 #exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux
    770 normalize lapply (produce_cond_fresh e exit_label ls … Haux)
    771 elim (produce_cond ????) * #stm #label #uv2 normalize nodelta //
    772 qed.
     547#u #i #e #ls @fresher_for_univ @simplify_switch_fte qed.
     548
     549lemma switch_removal_fte : ∀st,u.
     550  fte (ret_u ? (switch_removal … st u)) u.
     551#st @(statement_ind2 ? (λls. ∀u. fte (ret_u ? (switch_removal_branches ls u)) u) … st)
     552try /2 by reflexive_fte/
     553[ 1: #s1 #s2 #Hind1 #Hind2 #u normalize
     554     lapply (Hind1 u)
     555     cases (switch_removal s1 u) * #s1' #fvs1 #u'  normalize nodelta
     556     lapply (Hind2 u')
     557     cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize
     558     #HA #HB @(transitive_fte … HA HB)
     559| 2: #e #s1 #s2 #Hind1 #Hind2 #u normalize
     560     lapply (Hind1 u)
     561     cases (switch_removal s1 u) * #s1' #fvs1 #u'  normalize nodelta
     562     lapply (Hind2 u')
     563     cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize
     564     #HA #HB @(transitive_fte … HA HB)
     565| 3,7,8: #e #s #Hind #u normalize
     566     lapply (Hind u)
     567     cases (switch_removal s u) * #s' #fvs #u' normalize #H @H
     568| 4: #e #s #Hind #u normalize
     569     lapply (Hind u)
     570     cases (switch_removal s u) * #s' #fvs #u' normalize #H @H
     571| 5: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #u normalize
     572     lapply (Hind1 u) cases (switch_removal s1 u) * #s1' #fvs1 #u' #Hfte1
     573     normalize nodelta
     574     lapply (Hind2 u') cases (switch_removal s2 u') * #s2' #fvs2 #u'' #Hfte2
     575     normalize nodelta
     576     lapply (Hind3 u'') cases (switch_removal s3 u'') * #s2' #fvs2 #u'' #Hfte3
     577     normalize nodelta
     578     /3 by transitive_fte/
     579| 6: #e #ls #Hind #u whd in match (switch_removal ??);
     580     lapply (Hind u)
     581     cases (switch_removal_branches ls u) * #ls #fvs #u' #Hfte1
     582     normalize nodelta
     583     lapply (fresh_fte … u') cases (fresh ? u') #fv #u'' #H lapply (H u'' fv (refl ??)) #Hfte2
     584     normalize nodelta
     585     lapply (simplify_switch_fte u'' (Expr (Evar fv) (typeof e)) ls)
     586     cases (simplify_switch ???)
     587     normalize nodelta
     588     #st' #u''' #Hfte3
     589     /3 by transitive_fte/
     590| 9: #s #H #u normalize
     591     lapply (H u) cases (switch_removal s u) * #st' #fvs normalize #u' #H @H
     592| 10: #sz #i #st #ls #Hind1 #Hind2 #u normalize
     593     lapply (Hind2 u) cases (switch_removal_branches ls u) * #ls' #fvs' #u'
     594     normalize nodelta #Hfte1
     595     lapply (Hind1 … u') cases (switch_removal st u') * #st' #fvs'' #u''
     596     normalize nodelta #Hfte2
     597     /3 by transitive_fte/
     598] qed.     
     599
     600lemma switch_removal_fresh : ∀u,i,st.
     601  fresh_for_univ ? i u →
     602  fresh_for_univ ? i (ret_u … (switch_removal st u)).
     603#u #i #st @fresher_for_univ @switch_removal_fte qed.
    773604
    774605(* -----------------------------------------------------------------------------
     
    879710] qed.
    880711
     712lemma fresh_to_substatements :
     713  ∀s,u. fresh_for_statement s u →
     714        substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).
     715#s #u cases s
     716whd in match (fresh_for_statement ??);
     717whd in match (substatement_P ???); try /2/
     718[ 1: #e1 #e2
     719     whd in match (fresh_for_statement ??);
     720     whd in match (substatement_P ???);
     721     #H lapply (fresh_max_split … H) * /2 by conj/     
     722| 2: #e1 #e2 #args
     723     whd in match (fresh_for_statement ??);
     724     whd in match (substatement_P ???);
     725     cases e1 normalize nodelta
     726     [ 1: #H lapply (fresh_max_split … H) * #HA #HB @conj try @HA
     727          elim args in HB; try /2 by I/ #hd #tl normalize nodelta #Hind #HB
     728          elim (fresh_max_split … HB) #HC #HD
     729          whd in match (foldr ?????) in HD;
     730          elim (fresh_max_split … HD) #HE #HF
     731          @conj try assumption
     732          @Hind >max_id_commutative >max_id_one_neutral @HF
     733     | 2: #expr #H cases (fresh_max_split … H) #HA normalize nodelta #HB
     734          cases (fresh_max_split … HB) #HC #HD @conj try @conj try // elim args in HD; try //
     735          #e #l #Hind #HD
     736          whd in match (foldr ?????) in HD;
     737          elim (fresh_max_split … HD) #HE #HF
     738          @conj try assumption
     739          @Hind @HF ]
     740| 3: #stmt1 #stmt2 whd in ⊢ (% → %); @fresh_max_split
     741| 4: #e #s1 #s2 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) *
     742     #H1 @fresh_max_split
     743| 5: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H)
     744| 6: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H)
     745| 7: #s1 #e #s2 #s3 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * #H1 #H2
     746     @conj try @conj try @I try @conj try @I
     747     elim (fresh_max_split … H1) elim (fresh_max_split … H2) /2/
     748| 8: #opt cases opt try /2/
     749| 9: #e #ls #H whd @conj lapply (fresh_max_split … H) * #HA #HB try // lapply HB
     750     @(labeled_statements_ind … ls)
     751     [ 1: #s' #H' //
     752     | 2: #sz #i #s' #tl #Hind #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj
     753          [ 1: //
     754          | 2: @Hind @H1 ] ]
     755| 10: #lab #stmt #H whd lapply (fresh_max_split … H) * //
     756] qed.
     757
    881758(* Auxilliary commutation lemma used in [substatement_fresh]. *)
    882 
    883759lemma foldl_max : ∀l,a,b.
    884760  foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l =
     
    945821definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.
    946822
    947 definition outbound_pointer ≝ λm,p.
    948    Zltb (block_id (pblock p)) (nextblock m) = true ∧
    949    Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧
    950    high_bound m (pblock p) = Z_of_unsigned_bitvector … (offv (poff p)).
    951    
    952 (* a valid_pointer is either /inside/ the bounds of the target block xor /one off/ the end.  *)
    953 lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p.
     823lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p.
    954824#m #p @conj
    955825[ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??);
    956      whd in match (outbound_pointer ??);
    957826     whd in match (do_if_in_bounds); normalize nodelta
    958827     cases (Zltb (block_id (pblock p)) (nextblock m))
    959      [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]     
     828     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
    960829     >andb_lsimpl_true normalize nodelta
    961830     cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
    962831     [ 2: normalize nodelta #Habsurd destruct (Habsurd) ]
    963832     >andb_lsimpl_true normalize nodelta
    964      lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p)))
    965      elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p)))
    966      [ 1: #H >H #_ normalize nodelta #_ %1 #A #f /2 by ex_intro/
    967      | 2: * #_ #H1 #_ #H2 >(Zleb_true_to_Zleb_true_to_eq … H1 H2) %2 @conj try @conj @refl ]
    968 | 2: whd in match (valid_pointer ??); *
    969      [ 1: whd in match (in_bounds_pointer ??); #H
    970           lapply (H bool (λblock,contents,off. true))
    971           * #foo whd in match (do_if_in_bounds ????);
    972           cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta
    973           [ 2: #Habsurd destruct (Habsurd) ]
    974           >andb_lsimpl_true
    975           cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
    976           normalize nodelta
    977           [ 2: #Habsurd destruct (Habsurd) ]
    978           >andb_lsimpl_true
    979           elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
    980           [ 1: #H >(Zltb_to_Zleb_true … H) #_ @refl
    981           | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]
    982      | 2: whd in match (outbound_pointer ??); * * #Hlt #Hleb >Hlt >Hleb
    983           #Hhigh >Hhigh >andb_lsimpl_true
    984           lapply (reflexive_Zle … (Z_of_unsigned_bitvector offset_size (offv (poff p))))
    985           #Hle >(Zle_to_Zleb_true … Hle) @refl
    986      ]
    987 ] qed.
     833     #Hlt >Hlt normalize nodelta #A #f /2 by ex_intro/
     834| 2: whd in match (valid_pointer ??);
     835     whd in match (in_bounds_pointer ??); #H
     836     lapply (H bool (λblock,contents,off. true))
     837     * #foo whd in match (do_if_in_bounds ????);
     838     cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta
     839     [ 2: #Habsurd destruct (Habsurd) ]
     840     >andb_lsimpl_true
     841     cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
     842     normalize nodelta
     843     [ 2: #Habsurd destruct (Habsurd) ]
     844     >andb_lsimpl_true
     845     elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))     
     846     [ 1: #H >H //
     847     | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]
     848] qed.
     849
     850lemma valid_pointer_to_Prop :
     851  ∀m,p. valid_pointer m p = true →
     852        (block_id (pblock p)) < (nextblock m) ∧
     853        (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧
     854        (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)).
     855#m #p whd in match (valid_pointer ??);       
     856#H
     857lapply (Zleb_true_to_Zle (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
     858lapply (Zltb_true_to_Zlt (block_id (pblock p)) (nextblock m))
     859cases (Zltb (block_id (pblock p)) (nextblock m)) in H;
     860[ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
     861cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
     862normalize nodelta
     863[ 2: #Habsurd destruct ]
     864#Hlt1 #Hlt2 #Hle @conj try @conj
     865try @(Hlt2 (refl ??)) try @(Hle (refl ??)) @(Zltb_true_to_Zlt … Hlt1)
     866qed.
    988867
    989868(* A writeable_block is a block that is:
     
    995874  wb_valid      : valid_block m b;
    996875  wb_nonempty   : low (blocks m b) < high (blocks m b)
    997 }. 
     876}.
    998877
    999878(* Type stating that m2 is an extension of m1, parameterised by a list of blocks where we can write freely *)
     
    1004883  me_writeable_valid : ∀b. meml ? b writeable → nonempty_block m2 b;
    1005884  (* blocks in [m1] than can be validly pointed to cannot be in [me_writeable]. *)
    1006   me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable);
    1007   (* This field does not entail [me_not_writeable] and is necessary to prove valid
     885  me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable)
     886 
     887  (* This field is not entailed [me_not_writeable] and is necessary to prove valid
    1008888     pointer conservation after a [free]. *)
    1009   me_not_writeable_ptr : ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable);
    1010  
     889
    1011890  (* Extension blocks contain nothing in [m1] *)
    1012891  (* me_not_mapped : ∀b. meml … b me_writeable → blocks m1 b = empty_block OZ OZ;  *)
     
    1019898     compare are valid before being equal).
    1020899  *)
    1021   me_valid_pointers : ∀p. (* ¬ (freed_pointer m1 p) → *)
     900(*  me_valid_pointers : ∀p.
    1022901                       valid_pointer m1 p = true →
    1023                        valid_pointer m2 p = true
     902                       valid_pointer m2 p = true *)
    1024903}.
     904
     905(* Since we removed end_pointers, we can prove some stuff that was previously given as a field of
     906   sr_memext. *)
     907lemma me_not_writeable_ptr :
     908  ∀m1,m2,writeable.
     909  sr_memext m1 m2 writeable →
     910  ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable).
     911#m1 #m2 #writeable #Hext #p #Hvalid
     912cut (nonempty_block m1 (pblock p))
     913[ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % //
     914     /2 by Zle_to_Zlt_to_Zlt/
     915| 2: @(me_not_writeable … Hext) ]
     916qed.
    1025917
    1026918(* If we have a memory extension, we can simulate loads *)
     
    1052944>(Zle_to_Zleb_true … Hlow) >(Zlt_to_Zltb_true … Hhigh) normalize
    1053945>Hres @refl
     946qed.
     947
     948lemma me_valid_pointers :
     949  ∀m1,m2,writeable.
     950  sr_memext m1 m2 writeable →
     951  ∀p. valid_pointer m1 p = true → valid_pointer m2 p = true.
     952* #contents1 #nextblock1 #Hnextblock_pos1
     953* #contents2 #nextblock2 #Hnextblock_pos2 #writeable #Hmemext * #pb #po #Hvalid
     954cut (nonempty_block (mk_mem contents1 nextblock1 Hnextblock_pos1) pb)
     955[ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % //
     956     /2 by Zle_to_Zlt_to_Zlt/ ]
     957#Hnonempty lapply (me_nonempty … Hmemext … Hnonempty) * * #Hvalid_block #Hlow_lt_high
     958#Hcontents_eq normalize >(Zlt_to_Zltb_true … Hvalid_block) normalize nodelta
     959<Hcontents_eq cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt
     960>(Zle_to_Zleb_true … Hle) normalize nodelta
     961>(Zlt_to_Zltb_true … Hlt) @refl
    1054962qed.
    1055963
     
    1087995          lapply (Hsim (p0 id0) res0) normalize #Hsol #H @Hsol @H ]
    1088996] qed.         
    1089            
     997
    1090998lemma environment_sim_invert :
    1091999  ∀en1,en2. environment_sim en1 en2 →
     
    12061114     ]
    12071115] qed.
    1208 
    12091116
    12101117lemma blocks_of_env_cons :
     
    13461253[ 1: #b #H @conj try % elim H try //
    13471254| 2: #b *
    1348 | 3: #b #_ normalize % //
    1349 | 4: #p #Hvalid % *
    1350 (* | 4: #b * *)
    1351 | 5: #p normalize >Hcontents_eq #H @H
    1352 ] qed.
     1255| 3: #b #_ normalize % // ]
     1256qed.
    13531257
    13541258(* memory extensions form a preorder relation *)
     
    13741278          lapply (me_not_writeable … H23 … Hvalid2) * #H #_ @H assumption
    13751279     ]
    1376 | 4: #p #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) *
    1377      [ 1: #Hmem12
    1378           lapply (me_not_writeable_ptr … H12 … Hvalid) * #H @H assumption
    1379      | 2: #Hmem23
    1380           lapply (me_valid_pointers … H12 … Hvalid) #Hvalid2
    1381           lapply (me_not_writeable_ptr … H23 … Hvalid2) * #H @H assumption
    1382      ]         
    1383 | 5: #p #Hvalid @(me_valid_pointers … H23) @(me_valid_pointers … H12) @Hvalid
    1384 ] qed.
    1385 
    1386 lemma memory_ext_reflexive :
    1387   ∀m. sr_memext m m [ ].
     1280] qed.     
     1281
     1282lemma memory_ext_reflexive : ∀m. sr_memext m m [ ].
    13881283#m % /2/ #b * qed.
    13891284
     
    14561351>andb_lsimpl_true
    14571352normalize nodelta #H
    1458 @Zltb_to_Zleb_true
    14591353cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
    14601354try // normalize #Habsurd destruct (Habsurd)
     1355qed.
     1356
     1357lemma bestorev_to_valid_pointer : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer m ptr = true.
     1358* #contents #next #nextpos #ptr #v #res
     1359whd in match (bestorev ???);
     1360whd in match (valid_pointer ??);
     1361cases (Zltb (block_id (pblock ptr)) next)
     1362normalize nodelta
     1363[ 2: #Habsurd destruct (Habsurd) ]
     1364>andb_lsimpl_true
     1365whd in match (low_bound ??);
     1366whd in match (high_bound ??);
     1367cases (Zleb (low (contents (pblock ptr)))
     1368        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
     1369[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
     1370>andb_lsimpl_true
     1371cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr))))
     1372normalize nodelta try // #Habsurd destruct (Habsurd)
    14611373qed.
    14621374
     
    15571469qed.
    15581470
     1471(* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *)
    15591472lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.
    15601473#m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);
    15611474#H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);
    15621475elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))
    1563 [ 1: #Hlt >Hlt normalize nodelta 
     1476[ 1: #Hlt >Hlt normalize nodelta
    15641477     @(eq_block_elim … b (pblock p))
    15651478     [ 1: #Heq >Heq whd in match (free ??);
     
    15831496qed.
    15841497
    1585 lemma outbound_free_to_outbound : ∀m,b,p. outbound_pointer (free m b) p → outbound_pointer m p.
    1586 #m #b #p whd in match (free ??);
    1587 whd in match (outbound_pointer ??) in ⊢ (% → %);
    1588 whd in match (update_block ????);
    1589 whd in match (low_bound ??); whd in match (high_bound ??);
    1590 @(eq_block_elim … (pblock p) b) normalize nodelta
    1591 [ 1: #Heq >Heq cases (Zltb ? (nextblock m))
    1592      [ 2: * * #Habsurd destruct (Habsurd) ]
    1593      * * #_ whd in match (low ?); whd in match (high ?);
    1594      #H1 #H2 <H2 in H1; normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    1595 | 2: #Hneq #H @H ]
    1596 qed.
    1597 
     1498(* Cf [in_bounds_free_to_in_bounds] *)
    15981499lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.
    15991500#m #b #p #Hvalid
    1600 lapply (valid_pointer_def … m p) * #_ #Hdef @Hdef
    1601 elim (valid_pointer_def … (free m b) p) #H #_
    1602 elim (H Hvalid)
    1603 [ 1: #Hin %1 @in_bounds_free_to_in_bounds assumption
    1604 | 2: #Hout %2 @outbound_free_to_outbound assumption ]
    1605 qed.
    1606 
     1501cases (valid_pointer_def … m p) #HA #HB
     1502cases (valid_pointer_def … (free m b) p) #HC #HD
     1503@HB @(in_bounds_free_to_in_bounds … b)
     1504@HC @Hvalid
     1505qed.
     1506
     1507(* Making explicit the argument above. *)
    16071508lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.
    16081509#m #b #p
     
    16131514whd in match (high_bound ??);
    16141515@(eq_block_elim … b (pblock p))
    1615 [ 1: #Heq >Heq >eq_block_b_b normalize nodelta
     1516[ 1: #Heq <Heq >eq_block_b_b normalize nodelta
    16161517     whd in match (low ?); whd in match (high ?);
    16171518     cases (Zltb ? (nextblock m))
     
    16211522qed.
    16221523
     1524(* Lifting the property of being valid after a free to memory extensions *)
    16231525lemma 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.
    16241526#m1 #m2 #writeable #Hext #p #b #Hvalid
     
    17031605          ]
    17041606     ]
    1705 | 4: #p #Hvalid
    1706      lapply (valid_free_to_valid … Hvalid) #Hvalid'
    1707      lapply (me_not_writeable_ptr … Hext … Hvalid') * #HA % #HB @HA     
    1708      elim writeable in HB;
    1709      [ 1: *
    1710      | 2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block
    1711           @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
    1712           [ 1: #Heq #H normalize %2 @(Hind H)
    1713           | 2: #Hblocks_neq whd in match (meml ???); *
    1714                [ 1: #Hneq normalize %1 assumption
    1715                | 2: #Hmem normalize %2 @(Hind Hmem) ]
    1716           ]
    1717      ]
    1718 | 5: #p @(valid_pointer_free … writeable) @Hext
    1719 ] qed.
     1607] qed.     
     1608
    17201609
    17211610(* Freeing from an extension block is ok. *)
     
    17691658     ] ] ] * #Hmem' #Hblocks_neq
    17701659     lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption
    1771 | 4: #p #Hnonempty % #Hmem
    1772      cut (mem block (pblock p) writeable ∧ (pblock p) ≠ b)
    1773      [ elim writeable in Hmem;
    1774        [ 1: normalize @False_ind
    1775        | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block
    1776             @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta
    1777             [ 1: #Heq #H whd in match (meml ???); destruct
    1778                  elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption
    1779             | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); *
    1780                  [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ]
    1781                  | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ]
    1782      ] ] ] * #Hmem' #Hblocks_neq
    1783      lapply (me_not_writeable_ptr … Hext … Hnonempty) * #H @H assumption
    1784 | 5: #p #Hvalid lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_mem
    1785      lapply (mem_not_mem_neq … Hb_writeable … Hnot_mem) #Hneq
    1786      lapply (me_valid_pointers … Hext … Hvalid) #Hvalid'
    1787      whd in match (free ??);
    1788      whd in match (valid_pointer ??) in ⊢ (??%%);
    1789      whd in match (low_bound ??); whd in match (high_bound ??);
    1790      whd in match (update_block ?????);
    1791      >(not_eq_block_rev … Hneq) normalize
    1792      @Hvalid'
    1793 ] qed.
    1794 
    1795 
     1660] qed.
    17961661 
    17971662 
     
    18811746    sr_memext m1 m2 (hd :: writeable) →
    18821747    sr_memext m1 m2 writeable.
    1883 #m1 #m2 #hd #writeable * 
    1884 #Hnonempty #Hwriteable_valid #Hnot_writeable #Hnot_writeable_ptr #Hvalid_pointers %
     1748#m1 #m2 #hd #writeable *
     1749#Hnonempty #Hwriteable_valid #Hnot_writeable %
    18851750try assumption
    18861751[ 1: #b #Hmem @Hwriteable_valid whd %2 assumption
    18871752| 2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem
    1888 | 3: #p #Hvalid % #Hmem elim (Hnot_writeable_ptr … Hvalid) #H @H whd %2 @Hmem
    18891753] qed.
    18901754
     
    19021766     lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem'
    19031767     lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption
    1904 | 4: #p #Hvalid % #Hmem
    1905      lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem'
    1906      lapply (me_not_writeable_ptr … Hext … Hvalid) * #H @H assumption
    1907 | 5: @(me_valid_pointers … Hext) ]
    1908 qed.
    1909 
    1910 axiom lset_inclusion_difference :
     1768] qed.     
     1769
     1770lemma lset_difference_empty :
    19111771  ∀A : DeqSet.
    1912   ∀s1,s2 : lset (carr A).
    1913     lset_inclusion ? s1 s2 →
    1914     ∃s2'. lset_eq ? s2 (s1 @ s2') ∧
    1915           lset_disjoint ? s1 s2' ∧
    1916           lset_eq ? s2' (lset_difference ? s2 s1).
    1917          
    1918 lemma memory_eq_to_memory_ext_pre :
    1919   ∀m1,m1',m2,writeable.
    1920   memory_eq m1 m1' →
    1921   sr_memext m1' m2 writeable →
    1922   sr_memext m1 m2 writeable.
    1923 #m1 #m1' #m2 #writeable #Heq #Hext
    1924 lapply (memory_eq_to_mem_ext … Heq) #Hext'
    1925 @(memory_ext_transitive … Hext' Hext)
    1926 qed.
    1927 
    1928 lemma memory_eq_to_memory_ext_post :
    1929   ∀m1,m2,m2',writeable.
    1930   memory_eq m2' m2 →
    1931   sr_memext m1 m2' writeable →
    1932   sr_memext m1 m2 writeable.
    1933 #m1 #m2 #m2' #writeable #Heq #Hext
    1934 lapply (memory_eq_to_mem_ext … Heq) #Hext'
    1935 lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H
     1772  ∀s1. lset_difference A s1 [ ] = s1.
     1773#A #s1 elim s1 try //
     1774#hd #tl #Hind >lset_difference_unfold >Hind @refl
    19361775qed.
    19371776
     
    19461785     | 1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ]
    19471786] qed.
    1948 
    1949 lemma lset_difference_nil : ∀A,s. lset_difference A s [ ] = s. #A #s elim s //
    1950 #hd #tl #Hind >lset_difference_unfold normalize in match (memb ???); normalize nodelta >Hind @refl
    1951 qed.
    19521787
    19531788lemma lset_mem_inclusion_mem :
     
    20491884                [ 1: %2 @Hind @Hmem
    20501885                | 2: @Hind @Hmem ] ] ]
    2051 ] qed.               
     1886] qed.
     1887
     1888lemma lset_disjoint_dec :
     1889  ∀A : DeqSet.
     1890  ∀s1,elt,s2.
     1891  mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1).
     1892#A #s1 #elt #s2
     1893@(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ?
     1894  with
     1895  [ false ⇒ λHA. ?
     1896  | true ⇒ λHA. ? ] (refl ? (elt ∈ s1)))
     1897[ 1: lapply (memb_to_mem … HA) #Hmem
     1898     %1 @Hmem
     1899| 2: %2 elim s1 in HA;
     1900     [ 1: #_ whd %1 @refl
     1901     | 2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?);
     1902          >lset_difference_unfold
     1903          >lset_difference_unfold2
     1904          lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %);
     1905          cases (elt==hd1) normalize nodelta
     1906          [ 1: #_ #Habsurd destruct
     1907          | 2: #HA #HB >HB normalize nodelta %1 @refl ] ] ]
     1908qed.
     1909
     1910lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2.
     1911  mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l.
     1912#A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/
     1913qed.
     1914
     1915lemma lset_inclusion_difference_aux :
     1916  ∀A : DeqSet. ∀s1,s2.
     1917  lset_inclusion A s1 s2 →
     1918  (lset_eq A s2 (s1@lset_difference A s2 s1)).
     1919#A #s1
     1920@(WF_ind ????? (filtered_list_wf A s1))
     1921*
     1922[ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq
     1923| 2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl
     1924     lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?)
     1925     [ 1: whd normalize
     1926          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ]
     1927     #Hind_wf     
     1928     elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq
     1929     >cons_to_append in ⊢ (???%); >associative_append
     1930     >lset_difference_unfold2
     1931     >nil_append
     1932     >lset_remove_split >lset_remove_split
     1933     normalize in match (lset_remove ? [hd1] hd1);
     1934     >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
     1935     >nil_append <lset_remove_split >lset_difference_lset_remove_commute
     1936     lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?)
     1937     [ 1: lapply (lset_inclusion_remove … Hincl hd1)
     1938          >Heq @lset_inclusion_eq2
     1939          >lset_remove_split >lset_remove_split >lset_remove_split
     1940          normalize in match (lset_remove ? [hd1] hd1);
     1941          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
     1942          >nil_append @reflexive_lset_eq ]
     1943     #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind
     1944     @lset_eq_concrete_to_lset_eq
     1945     lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc
     1946     @(square_lset_eq_concrete ????? Hindc) -Hindc -Hind
     1947     [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B))
     1948          [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete
     1949          | 1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ]
     1950     | 2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …))
     1951          elim (s2A@s2B)
     1952          [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq
     1953          | 2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold
     1954               @(match (hd2∈filter A (λx:A.¬x==hd1) tl1)
     1955                 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ?
     1956                 with
     1957                 [ false ⇒ λH. ?
     1958                 | true ⇒ λH. ?
     1959                 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta
     1960               [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter))
     1961                    normalize nodelta @Hind
     1962               | 2: @(match (hd2∈tl1)
     1963                      return λx. ((hd2∈tl1) = x) → ?
     1964                      with
     1965                      [ false ⇒ λH'. ?
     1966                      | true ⇒ λH'. ?
     1967                      ] (refl ? (hd2∈tl1))) normalize nodelta
     1968                      [ 1: (* We have hd2 = hd1 *)
     1969                            cut (hd2 = hd1)
     1970                            [ elim tl1 in H H';
     1971                              [ 1: normalize #_ #Habsurd destruct (Habsurd)
     1972                              | 2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?);
     1973                                    lapply (eqb_true ? hdtl1 hd1)
     1974                                    cases (hdtl1==hd1) normalize nodelta
     1975                                    [ 1: * #H >(H (refl ??)) #_
     1976                                         lapply (eqb_true ? hd2 hd1)
     1977                                         cases (hd2==hd1) normalize nodelta *
     1978                                         [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl
     1979                                         | 2: #_ #_ @Hind ]
     1980                                    | 2: #_ normalize lapply (eqb_true ? hd2 hdtl1)
     1981                                         cases (hd2 == hdtl1) normalize nodelta *
     1982                                         [ 1: #_ #_ #Habsurd destruct (Habsurd)
     1983                                         | 2: #_ #_ @Hind ] ] ] ]
     1984                           #Heq_hd2hd1 destruct (Heq_hd2hd1)
     1985                           @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind)
     1986                           #Hind' @(square_lset_eq_concrete … Hind')
     1987                           [ 2: @lset_refl
     1988                           | 1: >cons_to_append >cons_to_append in ⊢ (???%);
     1989                                @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
     1990                                [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract
     1991                                | 2: >(cons_to_append … hd1 (lset_difference ???))
     1992                                     @lset_eq_concrete_cons >nil_append >nil_append
     1993                                     @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ]
     1994                        | 2: @(match hd2 == hd1
     1995                               return λx. ((hd2 == hd1) = x) → ?
     1996                               with
     1997                               [ true ⇒ λH''. ?
     1998                               | false ⇒ λH''. ?
     1999                               ] (refl ? (hd2 == hd1)))
     2000                             [ 1: whd in match (lset_remove ???) in ⊢ (???%);
     2001                                  >H'' normalize nodelta >((proj1 … (eqb_true …)) H'')
     2002                                  @(transitive_lset_eq … Hind)
     2003                                  @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
     2004                                  [ 2: @lset_eq_contract ]                                                                   
     2005                                  @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons                                 
     2006                                  @switch_lset_eq_concrete
     2007                             | 2: whd in match (lset_remove ???) in ⊢ (???%);
     2008                                  >H'' >notb_false normalize nodelta
     2009                                  @lset_eq_concrete_to_lset_eq
     2010                                  lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc
     2011                                  lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' -Hindc
     2012                                  @(square_lset_eq_concrete … Hindc')
     2013                                  [ 1: @symmetric_lset_eq_concrete
     2014                                       >cons_to_append >cons_to_append in ⊢ (???%);
     2015                                       >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%);
     2016                                       @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
     2017                                  | 2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
     2018                                  ]
     2019                              ]
     2020                        ]
     2021                    ]
     2022             ]
     2023      ]
     2024] qed.             
     2025                                                       
     2026lemma lset_inclusion_difference :
     2027  ∀A : DeqSet.
     2028  ∀s1,s2 : lset (carr A).
     2029    lset_inclusion ? s1 s2 →
     2030    ∃s2'. lset_eq ? s2 (s1 @ s2') ∧
     2031          lset_disjoint ? s1 s2' ∧
     2032          lset_eq ? s2' (lset_difference ? s2 s1).
     2033#A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj
     2034[ 1: @lset_inclusion_difference_aux @Hincl
     2035| 2: /2 by lset_difference_disjoint/
     2036| 3,4: @reflexive_lset_inclusion ]
     2037qed.
     2038
     2039         
     2040lemma memory_eq_to_memory_ext_pre :
     2041  ∀m1,m1',m2,writeable.
     2042  memory_eq m1 m1' →
     2043  sr_memext m1' m2 writeable →
     2044  sr_memext m1 m2 writeable.
     2045#m1 #m1' #m2 #writeable #Heq #Hext
     2046lapply (memory_eq_to_mem_ext … Heq) #Hext'
     2047@(memory_ext_transitive … Hext' Hext)
     2048qed.
     2049
     2050lemma memory_eq_to_memory_ext_post :
     2051  ∀m1,m2,m2',writeable.
     2052  memory_eq m2' m2 →
     2053  sr_memext m1 m2' writeable →
     2054  sr_memext m1 m2 writeable.
     2055#m1 #m2 #m2' #writeable #Heq #Hext
     2056lapply (memory_eq_to_mem_ext … Heq) #Hext'
     2057lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H
     2058qed.
     2059
    20522060
    20532061lemma memext_free_extended_environment :
     
    21582166] qed.
    21592167
     2168(* --------------------------------------------------------------------------- *)
     2169(* Some lemmas allowing to reason on writes to extended memories. *)
     2170
     2171(* Writing in the extended part of the memory preserves the extension (that's the point) *)
     2172lemma bestorev_writeable_memory_ext :
     2173  ∀m1,m2,writeable.
     2174  ∀Hext:sr_memext m1 m2 writeable.
     2175  ∀wb,wo,v. meml ? wb writeable →
     2176  ∀m2'.bestorev m2 (mk_pointer wb wo) v = Some ? m2' →
     2177  sr_memext m1 m2' writeable.
     2178#m1 * #contents2 #nextblock2 #Hpos2 #writeable #Hext #wb #wo #v #Hmem #m2'
     2179whd in ⊢ ((??%?) → ?);
     2180lapply (me_writeable_valid … Hext ? Hmem) * whd in ⊢ (% → ?); #Hlt
     2181>(Zlt_to_Zltb_true … Hlt) normalize nodelta #Hnonempty2 #H
     2182lapply (if_opt_inversion ???? H) -H * #Hzltb
     2183lapply (andb_inversion … Hzltb) * #Hleb #Hltb -Hzltb
     2184#Heq destruct %
     2185[ 1: #b #Hnonempty1
     2186     lapply (me_nonempty … Hext b Hnonempty1) * * #Hvalid_b #Hnonempty_b
     2187     #Heq @conj
     2188     [ 1: % whd whd in Hvalid_b; try @Hvalid_b
     2189          normalize cases (block_region b) normalize nodelta
     2190          cases (block_region wb) normalize nodelta try //
     2191          @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta
     2192          try //
     2193     | 2: whd in ⊢ (??%%);
     2194          @(eq_block_elim … b wb) normalize nodelta // #Heq_b_wb
     2195          lapply (me_not_writeable … Hext b Hnonempty1) destruct (Heq_b_wb)
     2196          * #H @(False_ind … (H Hmem)) ]
     2197| 2: #b #Hmem_writeable
     2198     lapply (me_writeable_valid … Hext … Hmem_writeable) #H %
     2199     [ 1: normalize cases H //
     2200     | 2: cases H normalize #Hb_lt #Hb_nonempty2
     2201          cases (block_region b)
     2202          cases (block_region wb) normalize nodelta
     2203          //
     2204          @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta
     2205          // ]
     2206| 3: #b #Hnonempty
     2207     lapply (me_not_writeable … Hext … Hnonempty) //
     2208] qed.
     2209
     2210(* If we manage to write in a block, then it is nonempty *)
     2211lemma bestorev_success_nonempty :
     2212  ∀m,wb,wo,v,m'.
     2213  bestorev m (mk_pointer wb wo) v = Some ? m' →
     2214  nonempty_block m wb.
     2215#m #wb #wo #v #m' normalize #Hstore
     2216cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H
     2217cases (if_opt_inversion ???? H) -H #nonempty #H %
     2218[ 1: whd @Zltb_true_to_Zlt assumption
     2219| 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H'
     2220     cut (Zleb (low (blocks m wb)) z = true)
     2221     [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ]
     2222     #Hleb >Hleb in H'; normalize nodelta #Hlt
     2223     lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt)
     2224     /2 by Zle_to_Zlt_to_Zlt/
     2225] qed.
     2226
     2227(* If we manage to write in a block, it is still non-empty after the write *)
     2228lemma bestorev_success_nonempty2 :
     2229  ∀m,wb,wo,v,m'.
     2230  bestorev m (mk_pointer wb wo) v = Some ? m' →
     2231  nonempty_block m' wb.
     2232#m #wb #wo #v #m' normalize #Hstore
     2233cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H
     2234cases (if_opt_inversion ???? H) -H #nonempty #H %
     2235[ 1: whd destruct @Zltb_true_to_Zlt assumption
     2236| 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H'
     2237     cut (Zleb (low (blocks m wb)) z = true)
     2238     [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ]
     2239     #Hleb >Hleb in H'; normalize nodelta #Hlt
     2240     lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt)
     2241     destruct cases (block_region wb) normalize >eqZb_z_z normalize
     2242     /2 by Zle_to_Zlt_to_Zlt/
     2243] qed.
     2244
     2245(* A nonempty block stays nonempty after a write. *)
     2246lemma nonempty_block_update_ok :
     2247  ∀m,b,wb,offset,v.
     2248  nonempty_block m b →
     2249  nonempty_block
     2250    (mk_mem
     2251      (update_block ? wb
     2252        (mk_block_contents (low (blocks m wb)) (high (blocks m wb))
     2253          (update beval offset v (contents (blocks m wb)))) (blocks m))
     2254            (nextblock m) (nextblock_pos m)) b.
     2255#m #b #wb #offset #v * #Hvalid #Hnonempty % //
     2256cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize
     2257cases br normalize nodelta cases wbr normalize nodelta //
     2258@(eqZb_elim … bid wbid) // #Heq #Hlt normalize //
     2259qed.
     2260
     2261lemma nonempty_block_update_ok2 :
     2262  ∀m,b,wb,offset,v.
     2263  nonempty_block
     2264    (mk_mem
     2265      (update_block ? wb
     2266        (mk_block_contents (low (blocks m wb)) (high (blocks m wb))
     2267          (update beval offset v (contents (blocks m wb)))) (blocks m))
     2268            (nextblock m) (nextblock_pos m)) b →
     2269  nonempty_block m b.
     2270#m #b #wb #offset #v * #Hvalid #Hnonempty % //
     2271cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize
     2272cases br normalize nodelta cases wbr normalize nodelta //
     2273@(eqZb_elim … bid wbid) // #Heq #Hlt normalize //
     2274qed.
     2275
     2276(* Writing in the non-extended part of the memory preserves the extension as long
     2277 * as it's done identically in both memories. *)
     2278lemma bestorev_not_writeable_memory_ext :
     2279  ∀m1,m2,writeable.
     2280  ∀Hext:sr_memext m1 m2 writeable.
     2281  ∀wb,wo,v.
     2282  ∀m1'. bestorev m1 (mk_pointer wb wo) v = Some ? m1' → 
     2283  ∃m2'. bestorev m2 (mk_pointer wb wo) v = Some ? m2' ∧
     2284        sr_memext m1' m2' writeable.
     2285#m1 #m2 #writeable #Hext #wb #wo #v #m1' #Hstore1
     2286lapply (bestorev_success_nonempty … Hstore1) #Hwb_nonempty
     2287cases (me_nonempty … Hext … Hwb_nonempty) #Hwb_nonempty2 #Hblocks_eq
     2288cut (∃m2'. bestorev m2 (mk_pointer wb wo) v=Some mem m2')
     2289[ cases Hwb_nonempty2 #Hwb_valid #Hnonempty normalize
     2290  normalize in Hwb_valid; >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
     2291  whd in Hstore1:(??%%); normalize
     2292  cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H
     2293  cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H
     2294  cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1
     2295  >Hblocks_eq in Hleb1 Hltb1 ⊢ %; #Hleb1 #Hltb1 >Hleb1 >Hltb1
     2296  normalize nodelta /2 by ex_intro/ ]
     2297* #m2' #Hstore2 %{m2'} @conj try assumption
     2298whd in Hstore1:(??%%);
     2299whd in Hstore2:(??%%);
     2300cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H
     2301cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H
     2302cases (if_opt_inversion ???? Hstore2) -Hstore2 #block_valid2 #H
     2303cases (if_opt_inversion ???? H) #Hin_bounds2 #Hm2' -H
     2304cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1
     2305cases (andb_inversion … Hin_bounds2) #Hleb2 #Hltb2 -Hin_bounds2
     2306cut (valid_pointer m1 (mk_pointer wb wo))
     2307[ 1: normalize >block_valid1 normalize nodelta >Hleb1 normalize nodelta
     2308     >Hltb1 @I ]
     2309#Hvalid
     2310lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_in_writeable
     2311destruct %
     2312[ 1: #b #Hnonempty lapply (me_nonempty … Hext … (nonempty_block_update_ok2 … Hnonempty)) * #HA #HB
     2313     @conj
     2314     [ 1: @nonempty_block_update_ok //
     2315     | 2: normalize cases b in HB; #br #bid cases wb #wbr #wbid
     2316          cases br cases wbr normalize nodelta
     2317          @(eqZb_elim … bid wbid) normalize nodelta //
     2318          #Hid_eq >Hid_eq #Hblock_eq >Hblock_eq @refl ]
     2319| 2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok
     2320| 3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty)
     2321     @(me_not_writeable … Hext)
     2322] qed.
     2323
     2324(* If we successfuly store something in the first memory, then we can store it in the
     2325 * second one and the memory extension is preserved. *)
     2326lemma memext_store_value_of_type :
     2327       ∀m, m_ext, m', writeable, ty, loc, off, v.
     2328       sr_memext m m_ext writeable →
     2329       store_value_of_type ty m loc off v = Some ? m' →
     2330       ∃m_ext'. store_value_of_type ty m_ext loc off v = Some ? m_ext' ∧
     2331                sr_memext m' m_ext' writeable.
     2332#m #m_ext #m' #writeable #ty #loc #off #v #Hext
     2333(* case analysis on access mode of [ty] *)
     2334cases ty
     2335[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     2336| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     2337whd in ⊢ ((??%?) → (?%?));
     2338[ 1,5,6,7,8: #Habsurd destruct ]
     2339whd in ⊢ (? → (??(λ_.?(??%?)?)));
     2340lapply loc lapply off lapply Hext lapply m_ext lapply m lapply m' -loc -off -Hext -m_ext -m -m'
     2341elim (fe_to_be_values ??)
     2342[ 1,3,5,7: #m' #m #m_ext #Hext #off #loc normalize in ⊢ (% → ?); #Heq destruct (Heq) %{m_ext} @conj normalize //
     2343| 2,4,6,8: #hd #tl #Hind #m' #m #m_ext #Hext #off #loc whd in ⊢ ((??%?) → ?); #H
     2344           cases (some_inversion ????? H) #m'' * #Hstore_eq #Hstoren_eq
     2345           lapply (bestorev_not_writeable_memory_ext … Hext … Hstore_eq)
     2346           * #m_ext'' * #Hstore_eq2 #Hext2
     2347           lapply (Hind … Hext2 … Hstoren_eq) -Hind * #m_ext' *
     2348           #Hstoren' #Hext3
     2349           %{m_ext'} @conj try assumption
     2350           whd in ⊢ (??%%); >Hstore_eq2 normalize nodelta
     2351           @Hstoren'
     2352] qed.
     2353
     2354lemma memext_store_value_of_type' :
     2355       ∀m, m_ext, m', writeable, ty, ptr, v.
     2356       sr_memext m m_ext writeable →
     2357       store_value_of_type' ty m ptr v = Some ? m' →
     2358       ∃m_ext'. store_value_of_type' ty m_ext ptr v = Some ? m_ext' ∧
     2359                sr_memext m' m_ext' writeable.
     2360#m #m_ext #m' #writeable #ty #p #v #Hext cases p #b #o
     2361@memext_store_value_of_type @Hext qed.
    21602362
    21612363(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
     
    21862388
    21872389(* Simulation relations. *)
    2188 inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
    2189 | swc_stop : ∀fvs.
    2190     switch_cont_sim fvs Kstop Kstop
    2191 | swc_seq : ∀fvs,s,k,k',u,result.
     2390inductive switch_cont_sim : list (ident × type) → cont → cont → Prop ≝
     2391| swc_stop :
     2392    ∀new_vars. switch_cont_sim new_vars Kstop Kstop
     2393| swc_seq : ∀s,k,k',u,s',new_vars.
    21922394    fresh_for_statement s u →
    2193     switch_cont_sim fvs k k' →
    2194     switch_removal s fvs u = Some ? result →
    2195     switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
    2196 | swc_while : ∀fvs,e,s,k,k',u,result.
     2395    switch_cont_sim new_vars k k' →
     2396    s' = ret_st ? (switch_removal s u) →
     2397    lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars →
     2398    switch_cont_sim new_vars (Kseq s k) (Kseq s' k')
     2399| swc_while : ∀e,s,k,k',u,s',new_vars.
    21972400    fresh_for_statement (Swhile e s) u →
    2198     switch_cont_sim fvs k k' →
    2199     switch_removal s fvs u = Some ? result →
    2200     switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
    2201 | swc_dowhile : ∀fvs,e,s,k,k',u,result.
     2401    switch_cont_sim new_vars k k' →
     2402    s' = ret_st ? (switch_removal s u) →   
     2403    lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars →   
     2404    switch_cont_sim new_vars (Kwhile e s k) (Kwhile e s' k')
     2405| swc_dowhile : ∀e,s,k,k',u,s',new_vars.
    22022406    fresh_for_statement (Sdowhile e s) u →
    2203     switch_cont_sim fvs k k' →
    2204     switch_removal s fvs u = Some ? result →
    2205     switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
    2206 | swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
     2407    switch_cont_sim new_vars k k' →
     2408    s' = ret_st ? (switch_removal s u) →       
     2409    lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars →   
     2410    switch_cont_sim new_vars (Kdowhile e s k) (Kdowhile e s' k')
     2411| swc_for1 : ∀e,s1,s2,k,k',u,s',new_vars.
    22072412    fresh_for_statement (Sfor Sskip e s1 s2) u →
    2208     switch_cont_sim fvs k k' →
    2209     switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
    2210     switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
    2211 | swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
     2413    switch_cont_sim new_vars k k' →
     2414    s' = (ret_st ? (switch_removal (Sfor Sskip e s1 s2) u)) →
     2415    lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars →   
     2416    switch_cont_sim new_vars (Kseq (Sfor Sskip e s1 s2) k) (Kseq s' k')
     2417| swc_for2 : ∀e,s1,s2,k,k',u,result1,result2,new_vars.
    22122418    fresh_for_statement (Sfor Sskip e s1 s2) u →
    2213     switch_cont_sim fvs k k' →
    2214     switch_removal s1 fvs u = Some ? result1 →
    2215     switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
    2216     switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
    2217 | swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
     2419    switch_cont_sim new_vars k k' →
     2420    result1 = ret_st ? (switch_removal s1 u) →
     2421    result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) →
     2422    lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars →
     2423    switch_cont_sim new_vars (Kfor2 e s1 s2 k) (Kfor2 e result1 result2 k')
     2424| swc_for3 : ∀e,s1,s2,k,k',u,result1,result2,new_vars.
    22182425    fresh_for_statement (Sfor Sskip e s1 s2) u →
    2219     switch_cont_sim fvs k k' →
    2220     switch_removal s1 fvs u = Some ? result1 →
    2221     switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
    2222     switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
    2223 | swc_switch : ∀fvs,k,k'.
    2224     switch_cont_sim fvs k k' →
    2225     switch_cont_sim fvs (Kswitch k) (Kswitch k')
    2226 | swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *)       
    2227     switch_cont_sim fvs k k' →
    2228     (* /!\ Update [en] with [fvs'] ... *)
    2229     switch_cont_sim
    2230       (map … (fst ??) (\snd (function_switch_removal f)))
     2426    switch_cont_sim new_vars k k' →
     2427    result1 = ret_st ? (switch_removal s1 u) →
     2428    result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) →
     2429    lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars →
     2430    switch_cont_sim new_vars (Kfor3 e s1 s2 k) (Kfor3 e result1 result2 k')
     2431| swc_switch : ∀k,k',new_vars.
     2432    switch_cont_sim new_vars k k' →
     2433    switch_cont_sim new_vars (Kswitch k) (Kswitch k')
     2434| swc_call : ∀en,en',r,f,k,k',old_vars,new_vars. (* Warning: possible caveat with environments here. *)       
     2435    switch_cont_sim old_vars k k' →
     2436    old_vars = \snd (function_switch_removal f) →
     2437    disjoint_extension en en' old_vars →
     2438    switch_cont_sim
     2439      new_vars
    22312440      (Kcall r f en k)
    22322441      (Kcall r (\fst (function_switch_removal f)) en' k').
    2233 
    2234 (*
    2235  en' = exec_alloc_variables en m (\snd (function_switch_removal f))
    2236  TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc
    2237         variable dans en'.
    2238 
    2239         1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que
    2240            dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est
    2241            de savoir que :
    2242            si je lookup une variable générée à partir d'un univers frais dans l'environement en',
    2243            alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,
    2244            et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"
    2245            et à etre "(function_switch_removal f)-contained".
    2246 
    2247         2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup
    2248            et l'update n'altèrent pas le comportement du reste du programme.
    2249 
    2250         relation : si un statement S0 est inclus dans un statement S1, alors les variables générées
    2251                    depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.
    2252                    en particulier, si u est frais pour S1 u est frais pour S0.
    2253 
    2254         Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique
    2255                     "environment_extension en en' (\fst (\fst (switch_removal s u)))"
    2256                    
    2257  ---------------------------------------------------------------
    2258  . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction
    2259    et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.
    2260    on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner
    2261    en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.
    2262 *)
    22632442
    22642443record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
     
    22772456 (* current statement *)
    22782457 ∀sss_statement  : statement.
    2279  (* statement after transformation *)
    2280  ∀sss_result     : swret statement.
    22812458 (* label universe *)
    22822459 ∀sss_lu         : universe SymbolTag.
     
    23092486 (* The extended environment does not interfer with the old one. *)
    23102487 ∀sss_env_hyp    : disjoint_extension sss_env sss_env_ext sss_new_vars.
     2488 (* Extension blocks are writeable. *)
     2489 ∀sss_ext_write  : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable.
    23112490 (* conversion of the current statement, using the variables produced during the conversion of the current function *)
    2312  ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result.
     2491 ∀sss_result_rec.
     2492 ∀sss_result_hyp : switch_removal sss_statement sss_lu = sss_result_rec.
     2493 ∀sss_result.
     2494 sss_result = ret_st ? sss_result_rec →
     2495 (* inclusion of the locally produced new variables in the global new variables *)
     2496 lset_inclusion ? (ret_vars ? sss_result_rec) sss_new_vars →
    23132497 (* simulation between the continuations before and after conversion. *)
    2314  ∀sss_k_hyp      : switch_cont_sim (map ?? (fst ??) sss_new_vars) sss_k sss_k_ext. 
     2498 ∀sss_k_hyp      : switch_cont_sim sss_new_vars sss_k sss_k_ext.
    23152499 ext_fresh_for_genv sss_new_vars ge →
    23162500    switch_state_sim
    23172501      ge
    23182502      (State sss_func sss_statement sss_k sss_env sss_m)
    2319       (State sss_func_tr (ret_st … sss_result) sss_k_ext sss_env_ext sss_m_ext)
    2320 | sws_callstate : ∀vars, fd,args,k,k',m.
    2321     switch_cont_sim vars k k' →
    2322     switch_state_sim ge (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m)
    2323 | sws_returnstate :
    2324  ∀ssr_vars.
     2503      (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext)
     2504| sws_callstate :
     2505 ∀ssc_fd.
     2506 ∀ssc_args.
     2507 ∀ssc_k.
     2508 ∀ssc_k_ext.
     2509 ∀ssc_m.
     2510 ∀ssc_m_ext.
     2511 ∀ssc_writeable.
     2512 ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable.
     2513 (match ssc_fd with
     2514  [ CL_Internal ssc_f ⇒
     2515    switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext
     2516  | _ ⇒ True ]) →
     2517    switch_state_sim ge (Callstate ssc_fd ssc_args ssc_k ssc_m)
     2518                        (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
     2519| sws_returnstate :
    23252520 ∀ssr_result.
    23262521 ∀ssr_k       : cont.
     
    23302525 ∀ssr_writeable : list block.
    23312526 ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext ssr_writeable.
     2527 ∀ssr_vars.
    23322528    switch_cont_sim ssr_vars ssr_k ssr_k_ext →
    23332529    switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext)
     
    23352531    switch_state_sim ge (Finalstate r) (Finalstate r).
    23362532
    2337 lemma call_cont_swremoval : ∀fv,k,k'.
    2338   switch_cont_sim fv k k' →
    2339   switch_cont_sim fv (call_cont k) (call_cont k').
    2340 #fv #k0 #k0' #K elim K /2/
     2533lemma call_cont_swremoval : ∀k,k',vars.
     2534  switch_cont_sim vars k k' →
     2535  switch_cont_sim vars (call_cont k) (call_cont k').
     2536#k0 #k0' #vars #K elim K /2/
    23412537qed.
    23422538
     
    24442640qed.
    24452641
    2446 
    2447 (* Conservation of the smenantics of binary operators under memory extensions *)
     2642(* Conservation of the semantics of binary operators under memory extensions.
     2643   Tried to factorise it a bit but the play with indexes just becomes too messy. *)
    24482644lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable.
    24492645  ∀Hext:sr_memext m1 m2 writeable. ∀res.
     
    24542650try //
    24552651whd in match (sem_binary_operation ??????);
     2652lapply (me_valid_pointers … Hmemext)
     2653lapply (me_not_writeable_ptr … Hmemext)
    24562654elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1
    24572655elim m2 #contents2 #nextblocks2 #Hnextpos2
    2458 * #Hptrsim #writeable #Hvalid #Hdisjoint #Hvalid_cons
     2656* #Hnonempty #Hwriteable #Hnot_writeable #Hnot_writeable_ptr #Hvalid
    24592657whd in match (sem_cmp ??????);
    24602658whd in match (sem_cmp ??????);
    2461 [ 1: cases (classify_cmp (typeof e1) (typeof e2))
     2659[ 1,2: cases (classify_cmp (typeof e1) (typeof e2))
    24622660     normalize nodelta
    2463      [ 1: #sz #sg try //
    2464      | 2: #opt #ty
     2661     [ 1,5: #sz #sg try //
     2662     | 2,6: #opt #ty
    24652663          cases v1 normalize nodelta
    2466           [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
    2467           [ 1,2,3: #Habsurd destruct (Habsurd)
    2468           | 4: #H @H ]
     2664          [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
     2665          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
     2666          | 7,8: #H @H ]
    24692667          cases v2 normalize nodelta
    2470           [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
    2471           [ 1,2,3: #Habsurd destruct (Habsurd)
    2472           | 4: #H @H ]
    2473           lapply (Hvalid_cons ptr)
     2668          [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
     2669          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
     2670          | 7,8: #H @H ]
     2671          lapply (Hvalid ptr)
    24742672          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
    2475           [ 2: >andb_lsimpl_false normalize nodelta #_ #Habsurd destruct (Habsurd) ]
    2476           #Hvalid >(Hvalid (refl ??))
    2477           lapply (Hvalid_cons ptr')
     2673          [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ]
     2674          #Hvalid' >(Hvalid' (refl ??))
     2675          lapply (Hvalid ptr')
    24782676          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
    2479           [ 2: >andb_lsimpl_true #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    2480           #H' >(H' (refl ??)) >andb_lsimpl_true #Hres @Hres
    2481      | 3: #fsz #H @H
    2482      | 4: #ty1 #ty2 #H @H ]
    2483 | 2: cases (classify_cmp (typeof e1) (typeof e2))
     2677          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
     2678          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
     2679     | 3,7: #fsz #H @H
     2680     | 4,8: #ty1 #ty2 #H @H ]
     2681| 3,4: cases (classify_cmp (typeof e1) (typeof e2))
    24842682     normalize nodelta
    2485      [ 1: #sz #sg try //
    2486      | 2: #opt #ty
     2683     [ 1,5: #sz #sg try //
     2684     | 2,6: #opt #ty
    24872685          cases v1 normalize nodelta
    2488           [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
    2489           [ 1,2,3: #Habsurd destruct (Habsurd)
    2490           | 4: #H @H ]
     2686          [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
     2687          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
     2688          | 7,8: #H @H ]
    24912689          cases v2 normalize nodelta
    2492           [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
    2493           [ 1,2,3: #Habsurd destruct (Habsurd)
    2494           | 4: #H @H ]
    2495           lapply (Hvalid_cons ptr)
     2690          [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
     2691          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
     2692          | 7,8: #H @H ]
     2693          lapply (Hvalid ptr)
    24962694          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
    2497           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2498           #H >(H (refl ??))
    2499           lapply (Hvalid_cons ptr')
     2695          [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ]
     2696          #Hvalid' >(Hvalid' (refl ??))
     2697          lapply (Hvalid ptr')
    25002698          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
    2501           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2502           #H' >(H' (refl ??)) #Hok @Hok
    2503      | 3: #fsz #H @H
    2504      | 4: #ty1 #ty2 #H @H ]
    2505 | 3: cases (classify_cmp (typeof e1) (typeof e2))
     2699          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
     2700          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
     2701     | 3,7: #fsz #H @H
     2702     | 4,8: #ty1 #ty2 #H @H ]
     2703| 5,6: cases (classify_cmp (typeof e1) (typeof e2))
    25062704     normalize nodelta
    2507      [ 1: #sz #sg try //
    2508      | 2: #opt #ty
     2705     [ 1,5: #sz #sg try //
     2706     | 2,6: #opt #ty
    25092707          cases v1 normalize nodelta
    2510           [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
    2511           [ 1,2,3: #Habsurd destruct (Habsurd)
    2512           | 4: #H @H ]
     2708          [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
     2709          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
     2710          | 7,8: #H @H ]
    25132711          cases v2 normalize nodelta
    2514           [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
    2515           [ 1,2,3: #Habsurd destruct (Habsurd)
    2516           | 4: #H @H ]
    2517           lapply (Hvalid_cons ptr)
     2712          [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
     2713          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
     2714          | 7,8: #H @H ]
     2715          lapply (Hvalid ptr)
    25182716          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
    2519           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2520           #H >(H (refl ??))
    2521           lapply (Hvalid_cons ptr')
     2717          [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ]
     2718          #Hvalid' >(Hvalid' (refl ??))
     2719          lapply (Hvalid ptr')
    25222720          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
    2523           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2524           #H' >(H' (refl ??)) #Hok @Hok
    2525      | 3: #fsz #H @H
    2526      | 4: #ty1 #ty2 #H @H ]
    2527 | 4: cases (classify_cmp (typeof e1) (typeof e2))
    2528      normalize nodelta
    2529      [ 1: #sz #sg #H @H         
    2530      | 2: #opt #ty
    2531           cases v1 normalize nodelta
    2532           [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
    2533           [ 1,2,3: #Habsurd destruct (Habsurd)
    2534           | 4: #H @H ]
    2535           cases v2 normalize nodelta
    2536           [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
    2537           [ 1,2,3: #Habsurd destruct (Habsurd)
    2538           | 4: #H @H ]
    2539           lapply (Hvalid_cons ptr)
    2540           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
    2541           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2542           #H >(H (refl ??))
    2543           lapply (Hvalid_cons ptr')
    2544           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
    2545           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2546           #H' >(H' (refl ??)) #Hok @Hok
    2547      | 3: #fsz #H @H
    2548      | 4: #ty1 #ty2 #H @H ]
    2549 | 5: cases (classify_cmp (typeof e1) (typeof e2))
    2550      normalize nodelta
    2551      [ 1: #sz #sg #H @H         
    2552      | 2: #opt #ty
    2553           cases v1 normalize nodelta
    2554           [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
    2555           [ 1,2,3: #Habsurd destruct (Habsurd)
    2556           | 4: #H @H ]
    2557           cases v2 normalize nodelta
    2558           [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
    2559           [ 1,2,3: #Habsurd destruct (Habsurd)
    2560           | 4: #H @H ]
    2561           lapply (Hvalid_cons ptr)
    2562           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
    2563           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2564           #H >(H (refl ??))
    2565           lapply (Hvalid_cons ptr')
    2566           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
    2567           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2568           #H' >(H' (refl ??)) #Hok @Hok
    2569      | 3: #fsz #H @H
    2570      | 4: #ty1 #ty2 #H @H ]
    2571 | 6: cases (classify_cmp (typeof e1) (typeof e2))
    2572      normalize nodelta
    2573      [ 1: #sz #sg #H @H         
    2574      | 2: #opt #ty
    2575           cases v1 normalize nodelta
    2576           [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
    2577           [ 1,2,3: #Habsurd destruct (Habsurd)
    2578           | 4: #H @H ]
    2579           cases v2 normalize nodelta
    2580           [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
    2581           [ 1,2,3: #Habsurd destruct (Habsurd)
    2582           | 4: #H @H ]
    2583           lapply (Hvalid_cons ptr)
    2584           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
    2585           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2586           #H >(H (refl ??))
    2587           lapply (Hvalid_cons ptr')
    2588           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
    2589           [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
    2590           #H' >(H' (refl ??)) #Hok @Hok
    2591      | 3: #fsz #H @H
    2592      | 4: #ty1 #ty2 #H @H ]
     2721          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
     2722          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
     2723     | 3,7: #fsz #H @H
     2724     | 4,8: #ty1 #ty2 #H @H ]
    25932725] qed.
    25942726
     
    27492881] qed.
    27502882
     2883lemma exec_lvalue_sim_aux : ∀ge,ge',env,env_ext,m,m_ext.
     2884  (∀ed,ty. exec_lvalue_sim (exec_lvalue' ge env m ed ty)
     2885                           (exec_lvalue' ge' env_ext m_ext ed ty)) →
     2886  ∀e. exec_lvalue_sim (exec_lvalue ge env m e)
     2887                      (exec_lvalue ge' env_ext m_ext e).
     2888#ge #ge' #env #env_ext #m #m_ext #H * #ed #ty @H qed.
     2889
     2890lemma exec_expr_sim_to_exec_exprlist :
     2891  ∀ge,ge',en1,en2,m1,m2.
     2892  (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) →
     2893   ∀l. res_sim ? (exec_exprlist ge en1 m1 l) (exec_exprlist ge' en2 m2 l).
     2894#ge #ge' #en1 #en2 #m1 #m2 #Hsim #l elim l
     2895[ 1: whd #a #Heq normalize in Heq ⊢ %; destruct @refl
     2896| 2: #hd #tl #Hind whd * #lv #tr whd in ⊢ ((??%?) → (??%?));
     2897     lapply (Hsim hd)
     2898     cases (exec_expr ge en1 m1 hd)
     2899     [ 2: #error normalize #_ #Habsurd destruct (Habsurd)
     2900     | 1: * #v #vtr whd in ⊢ (% → ?); #Hsim >(Hsim ? (refl ??))
     2901          normalize nodelta
     2902          cases (exec_exprlist ge en1 m1 tl) in Hind;
     2903          [ 2: #error normalize #_ #Habsurd destruct (Habsurd)
     2904          | 1: #a normalize #H >(H ? (refl ??)) #Heq destruct normalize @refl
     2905          ]
     2906     ]
     2907] qed.
     2908
    27512909(*
    27522910lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
     
    27762934(* The return type of any function is invariant under switch removal *)
    27772935lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
    2778 #f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
     2936#f elim f #ty #args #vars #body whd in match (function_switch_removal ?);
     2937cases (switch_removal ??) * #stmt #fvs #u @refl
    27792938qed.
    27802939
    27812940(* Similar stuff for fundefs *)
    27822941lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
    2783 * // qed.
     2942* // * #ty #args #vars #body whd in ⊢ (??%%);
     2943whd in match (function_switch_removal ?); cases (switch_removal ??) * #st #u
     2944normalize nodelta #u @refl
     2945qed.
    27842946
    27852947(*
     
    28202982cases (leb e s) try /2/
    28212983qed.
     2984
    28222985(*
    28232986lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
     
    28613024qed.*)
    28623025
    2863 (*
    2864 lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
     3026lemma simplify_is_not_skip : ∀s. s ≠ Sskip → ∀u. ∃pf. is_Sskip (ret_st ? (switch_removal s u)) = inr ?? pf.
    28653027*
    2866 [ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
    2867 | 2: #e1 #e2 #u #_
    2868      whd in match (sw_rem ??);
    2869      whd in match (is_Sskip ?);
    2870      try /2 by refl, ex_intro/
    2871 | 3: #ret #f #args #u
    2872      whd in match (sw_rem ??);
    2873      whd in match (is_Sskip ?);
    2874      try /2 by refl, ex_intro/
    2875 | 4: #s1 #s2 #u
    2876      whd in match (sw_rem ??);
    2877      whd in match (switch_removal ??);     
    2878      cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
    2879      cases (switch_removal ? ?) * #e #f #g normalize nodelta     
    2880      whd in match (is_Sskip ?);
    2881      try /2 by refl, ex_intro/
    2882 | 5: #e #s1 #s2 #u #_
    2883      whd in match (sw_rem ??);
    2884      whd in match (switch_removal ??);     
    2885      cases (switch_removal ? ?) * #a #b #c normalize nodelta
    2886      cases (switch_removal ? ?) * #e #f #h normalize nodelta
    2887      whd in match (is_Sskip ?);
    2888      try /2 by refl, ex_intro/
    2889 | 6,7: #e #s #u #_
    2890      whd in match (sw_rem ??);
    2891      whd in match (switch_removal ??);     
    2892      cases (switch_removal ? ?) * #a #b #c normalize nodelta
    2893      whd in match (is_Sskip ?);
    2894      try /2 by refl, ex_intro/
    2895 | 8: #s1 #e #s2 #s3 #u #_     
    2896      whd in match (sw_rem ??);
    2897      whd in match (switch_removal ??);     
     3028[ 1: * #H @(False_ind … (H (refl ??))) ]
     3029try /2/
     3030[ 1: #s1 #s2 #_ #u normalize
    28983031     cases (switch_removal ? ?) * #a #b #c normalize nodelta
    28993032     cases (switch_removal ? ?) * #e #f #g normalize nodelta
    2900      cases (switch_removal ? ?) * #i #j #k normalize nodelta
    2901      whd in match (is_Sskip ?);
    2902      try /2 by refl, ex_intro/
    2903 | 9,10: #u #_     
    2904      whd in match (is_Sskip ?);
    2905      try /2 by refl, ex_intro/
    2906 | 11: #e #u #_
    2907      whd in match (is_Sskip ?);
    2908      try /2 by refl, ex_intro/
    2909 | 12: #e #ls #u #_
    2910      whd in match (sw_rem ??);
    2911      whd in match (switch_removal ??);
     3033     /2 by ex_intro/
     3034| 2: #e #s1 #s2 #_ #u normalize
     3035     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     3036     cases (switch_removal ? ?) * #e #f #g normalize nodelta
     3037     /2 by ex_intro/
     3038| 3,4: #e #s #_ #u normalize
     3039     cases (switch_removal ? ?) * #e #f #g normalize nodelta
     3040     /2 by ex_intro/
     3041| 5: #s1 #e #s2 #s3 #_ #u normalize     
     3042     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     3043     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
     3044     cases (switch_removal ? ?) * #h #i #j normalize nodelta
     3045     /2 by ex_intro/
     3046| 6: #e #ls #_ #u normalize
    29123047     cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
    29133048     cases (fresh ??) #e #f normalize nodelta
    2914      normalize in match (simplify_switch ???);
    29153049     cases (fresh ? f) #g #h normalize nodelta
    29163050     cases (produce_cond ????) * #k #l #m normalize nodelta
    2917      whd in match (is_Sskip ?);
    2918      try /2 by refl, ex_intro/
    2919 | 13,15: #lab #st #u #_
    2920      whd in match (sw_rem ??);
    2921      whd in match (switch_removal ??);
    2922      cases (switch_removal ? ?) * #a #b #c normalize nodelta
    2923      whd in match (is_Sskip ?);
    2924      try /2 by refl, ex_intro/
    2925 | 14: #lab #u     
    2926      whd in match (is_Sskip ?);
    2927      try /2 by refl, ex_intro/ ]
    2928 qed.
    2929 *)
     3051     /2 by ex_intro/
     3052| 7,8: #ls #st #_ #u normalize
     3053     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
     3054     /2 by ex_intro/
     3055] qed.
    29303056
    29313057(*
     
    29893115] qed.
    29903116
    2991 lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.
    2992 
    2993 lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c.
    2994 #A #B #a #b * #a' #b' #H destruct @refl
    2995 qed.
    2996 
    2997 lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c.
    2998 #A #B #a #b * #a' #b' #H destruct @refl
    2999 qed.
     3117lemma switch_removal_elim : ∀s,u. ∃s',fvs',u'. switch_removal s u = 〈s',fvs',u'〉.
     3118#s #u cases (switch_removal s u) * #s' #fvs' #u'
     3119%{s'} %{fvs'} %{u'} @refl
     3120qed.
     3121
     3122lemma switch_removal_branches_elim : ∀ls,u. ∃ls',fvs',u'. switch_removal_branches ls u = 〈ls',fvs',u'〉.
     3123#ls #u cases (switch_removal_branches ls u) * * #ls' #fvs' #u' /4 by ex_intro/ qed.
     3124
     3125lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
     3126
     3127lemma simplify_switch_elim : ∀e,ls,u. ∃res,u'. simplify_switch e ls u = 〈res, u'〉.
     3128#e #ls #u cases (simplify_switch e ls u) #res #u /3 by ex_intro/ qed.
     3129
     3130(* ----------------------------------------------------------------------------
     3131   What follows is some rather generic stuff on proving that reading where we 
     3132   just wrote yields what we expect. We have to prove everything at the back-end
     3133   level, and then lift this to the front-end. This entails having to reason on
     3134   invariants bearing on "intervals" of memories, and a lot of annoying stuff
     3135   to go back and forth nats, Zs and bitvectors ... *)
     3136
     3137lemma fold_left_neq_acc_neq :
     3138  ∀m. ∀acc1,acc2. ∀y1,y2:BitVector m.
     3139    acc1 ≠ acc2 →
     3140    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc1 y1 ≠
     3141    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc2 y2.
     3142#m elim m
     3143[ 1: #acc1 #acc2 #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
     3144| 2: #m' #Hind #acc1 #acc2 #y1 #y2
     3145     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
     3146     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
     3147     >Heq1 >Heq2 * #Hneq % whd in ⊢ ((??%%) → ?);
     3148     cases hd1 cases hd2 normalize nodelta #H
     3149     [ 1: lapply (Hind (p1 acc1) (p1 acc2) tl1 tl2 ?)
     3150          [ 1: % #H' @Hneq destruct (H') @refl ]
     3151          * #H' @H' @H
     3152     | 4: lapply (Hind (p0 acc1) (p0 acc2) tl1 tl2 ?)
     3153          [ 1: % #H' @Hneq destruct (H') @refl ]
     3154          * #H' @H' @H
     3155     | 2: lapply (Hind (p1 acc1) (p0 acc2) tl1 tl2 ?)
     3156          [ 1: % #H' destruct ]
     3157          * #H' @H' try @H
     3158     | 3: lapply (Hind (p0 acc1) (p1 acc2) tl1 tl2 ?)
     3159          [ 1: % #H' destruct ]
     3160          * #H' @H' try @H ]
     3161] qed.         
     3162
     3163lemma fold_left_eq :
     3164  ∀m. ∀acc. ∀y1,y2:BitVector m.
     3165    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y1 =
     3166    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y2 →
     3167    y1 = y2.
     3168#m elim m
     3169[ 1: #acc #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
     3170| 2: #m' #Hind #acc #y1 #y2
     3171     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
     3172     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
     3173     >Heq1 >Heq2 whd in ⊢ ((??%%) → ?);
     3174     cases hd1 cases hd2 normalize nodelta
     3175     [ 1,4: #H >(Hind … H) @refl
     3176     | 2: #Habsurd lapply (fold_left_neq_acc_neq ? (p1 acc) (p0 acc) tl1 tl2 ?)
     3177          [ 1: % #H' destruct ]
     3178          * #H @(False_ind … (H Habsurd))
     3179     | 3: #Habsurd lapply (fold_left_neq_acc_neq ? (p0 acc) (p1 acc) tl1 tl2 ?)
     3180          [ 1: % #H' destruct ]
     3181          * #H @(False_ind … (H Habsurd)) ]
     3182] qed.
     3183
     3184lemma bv_neq_Z_neq_aux :
     3185  ∀n. ∀bv1,bv2 : BitVector n. ∀f.
     3186    Z_of_unsigned_bitvector n bv1 ≠
     3187    pos (fold_left Pos bool n (λacc:Pos.λb:bool.if b then p1 acc else p0 acc ) (f one) bv2).
     3188#n elim n
     3189[ 1: #bv1 #bv2 >(BitVector_O … bv1) >(BitVector_O … bv2) #f normalize % #H destruct
     3190| 2: #n' #Hind #bv1 #bv2 #f
     3191     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
     3192     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
     3193     >Heq1 >Heq2 %
     3194     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
     3195     cases hd1 cases hd2 normalize nodelta
     3196     normalize in ⊢ ((??%%) → ?);
     3197     [ 1: #Hpos destruct (Hpos)
     3198          lapply (fold_left_neq_acc_neq ? one (p1 (f one)) tl1 tl2 ?)
     3199          [ 1: % #H destruct ]
     3200          * #H @H @e0
     3201     | 2: #Hpos destruct (Hpos)
     3202          lapply (fold_left_neq_acc_neq ? one (p0 (f one)) tl1 tl2 ?)
     3203          [ 1: % #H destruct ]
     3204          * #H @H @e0
     3205     | 3: #H cases (Hind tl1 tl2 (λx. p1 (f x))) #H' @H' @H
     3206     | 4: #H cases (Hind tl1 tl2 (λx. p0 (f x))) #H' @H' @H
     3207     ]
     3208] qed.     
     3209
     3210lemma bv_neq_Z_neq : ∀n. ∀bv1,bv2: BitVector n.
     3211  bv1 ≠ bv2 → Z_of_unsigned_bitvector n bv1 ≠ Z_of_unsigned_bitvector n bv2.
     3212#n #bv1 #bv2 * #Hneq % #Hneq' @Hneq -Hneq lapply Hneq' -Hneq'
     3213lapply bv2 lapply bv1 -bv1 -bv2
     3214elim n
     3215[ 1: #bv1 #bv2 >(BitVector_O bv1) >(BitVector_O bv2) //
     3216| 2: #n' #Hind #bv1 #bv2
     3217     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
     3218     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
     3219     >Heq1 >Heq2
     3220     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
     3221     cases hd1 cases hd2 normalize nodelta
     3222     [ 1: #Heq destruct (Heq) lapply (fold_left_eq … e0) * @refl
     3223     | 4: #H >(Hind ?? H) @refl
     3224     | 2: #H lapply (sym_eq ??? H) -H #H
     3225          cases (bv_neq_Z_neq_aux ? tl2 tl1 (λx.x)) #H' @(False_ind … (H' H))
     3226     | 3: #H
     3227          cases (bv_neq_Z_neq_aux ? tl1 tl2 (λx.x)) #H' @(False_ind … (H' H)) ]
     3228] qed.
     3229
     3230definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs).
     3231
     3232(* This axiom looks reasonable to me. But I slept 3 hours last night. *)
     3233axiom bv_incr_to_Z : ∀sz.∀bv:BitVector sz.
     3234  Z_of_unsigned_bitvector ? (increment ? bv) = OZ ∨
     3235  Z_of_unsigned_bitvector ? (increment ? bv) = (Zsucc (Z_of_unsigned_bitvector ? bv)).
     3236                                           
     3237(* Note the possibility of overflow of bv. But it should be allright in the big picture. *)
     3238lemma offset_succ_to_Z_succ :
     3239  ∀bv : BitVector 16. ∀x. Z_of_unsigned_bitvector ? bv < x → Z_of_unsigned_bitvector ? (increment ? bv) ≤ x.
     3240#bv #x
     3241cases (bv_incr_to_Z ? bv)
     3242[ 1: #Heq >Heq lapply (Z_of_unsigned_not_neg bv) *
     3243     [ 1: #Heq >Heq elim x //
     3244     | 2: * #p #H >H elim x // ]
     3245| 2: #H >H elim x
     3246     elim (Z_of_unsigned_bitvector 16 bv) try /2/
     3247] qed.
     3248
     3249(*
     3250lemma Z_not_le_shifted : ∀ofs.
     3251  (Z_of_unsigned_bitvector 16 (offv (shift_offset 2 ofs (bitvector_of_nat 2 1))) ≤ Z_of_unsigned_bitvector 16 (offv ofs)) → False.
     3252* #vec *)
     3253
     3254(* We prove the following properties for bestorev :
     3255  1) storing doesn't modify the nextblock
     3256  2) it does not modify the extents of the block written to
     3257  3) since we succeeded in storing, the offset is in the bounds
     3258  4) reading where we wrote yields the obvious result
     3259  5) besides the written offset, the memory contains the same stuff
     3260*)
     3261lemma mem_bounds_invariant_after_bestorev :
     3262∀m,m',b,ofs,bev.
     3263  bestorev m (mk_pointer b ofs) bev = Some ? m' →
     3264  nextblock m' = nextblock m ∧
     3265  (∀b.low (blocks m' b) = low (blocks m b) ∧
     3266      high (blocks m' b) = high (blocks m b)) ∧
     3267  (low (blocks m b) ≤ (Z_of_offset ofs) ∧
     3268   (Z_of_offset ofs) < high (blocks m b)) ∧   
     3269  (contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv ofs)) = bev) ∧
     3270  (∀o. o ≠ ofs → contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv o)) =
     3271                 contents (blocks m b) (Z_of_unsigned_bitvector ? (offv o))).
     3272#m #m' #b #ofs #bev whd in ⊢ ((??%?) → ?);
     3273#H
     3274cases (if_opt_inversion ???? H) #Hlt -H normalize nodelta #H
     3275cases (if_opt_inversion ???? H) #Hlelt -H #H
     3276cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj
     3277destruct try @refl
     3278[ 1:
     3279  #b' normalize cases b #br #bid cases b' #br' #bid'
     3280  cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize
     3281  try /2 by conj, refl/
     3282| 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H
     3283| 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H
     3284| 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize
     3285     >eqZb_z_z @refl
     3286| 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta
     3287     >eqZb_z_z normalize nodelta
     3288     @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs)))
     3289     [ 1,3: lapply Hneq cases o #bv1 cases ofs #bv2
     3290            #Hneq lapply (bv_neq_Z_neq ? bv1 bv2 ?)
     3291            [ 1,3: % #Heq destruct cases Hneq #H @H @refl ]
     3292            * #H #Habsurd @(False_ind … (H Habsurd))
     3293     | 2,4: normalize nodelta #H @refl ]
     3294] qed.
     3295
     3296(* Shifts an offset [i] times. storen uses a similar operation internally. *)
     3297let rec shiftn (off:offset) (i:nat) on i : offset ≝
     3298match i with
     3299[ O ⇒ off
     3300| S n ⇒
     3301  shiftn (shift_offset 2 off (bitvector_of_nat … 1)) n
     3302].
     3303
     3304(* This axioms states that if we do not stray too far, we cannot circle back to ourselves. Pretty trivial, but a
     3305   serious PITA to prove. *)
     3306axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs.
     3307
     3308(* We prove some properties of [storen m ptr data]. Note that [data] is a list of back-end chunks.
     3309   What we expect [storen] to do is to store this list starting at [ptr]. The property we expect to
     3310   have is that the contents of this particular zone (ptr to ptr+|data|-1) match exactly [data], and
     3311   that elsewhere the memory is untouched.
     3312   Not so simple. Some observations:
     3313   A) Pointers are encoded as block+offsets, and offsets are bitvectors, hence limited in range (2^16).
     3314      On the other hand, block extents are encoded on Zs and are unbounded. This entails some problems
     3315      when writing at the edge of the range of offsets and wrapping around, but that can be solved
     3316      resorting to ugliness and trickery.
     3317   B) The [data] list is unbounded. Taking into account the point A), this means that we can lose
     3318      data when writing (exactly as when we write in a circular buffer, overwriting previous stuff).
     3319      The only solution to that is to explicitly bound |data| with something reasonable.
     3320   Taking these observations into account, we prove the following invariants:
     3321  1) storing doesn't modify the nextblock (trivial)
     3322  2) it does not modify the extents of the block written to (trivial)
     3323  3) all the offsets on which we run while writing are legal (trivial)
     3324  3) if we index properly, we hit the stored data in the same order as in the list
     3325  4) If we hit elsewhere, we find the memory unmodified. We have a problem for defining "elsewhere",
     3326     because bitvectors (hence offsets) are limited in their range. For now, we define "elsewhere" as
     3327     "not reachable by shiftn from [ofs] to |data|"
     3328  5) the pointer we write to is valid (trivial)
     3329*)
     3330lemma mem_bounds_invariant_after_storen :
     3331  ∀data,m,m',b,ofs.
     3332    |data| ≤ 8 → (* 8 is the size of a double. *)
     3333    storen m (mk_pointer b ofs) data = Some ? m' →
     3334    (nextblock m' = nextblock m ∧
     3335    (∀b.low (blocks m' b) = low (blocks m b) ∧
     3336        high (blocks m' b) = high (blocks m b)) ∧
     3337    (∀index. index < |data| → low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧
     3338                               Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧
     3339    (∀index. index < |data| → nth_opt ? index data = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧
     3340    (∀o. (∀i. i < |data| → o ≠ shiftn ofs i) →
     3341         contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧
     3342    (|data| > 0 → valid_pointer m (mk_pointer b ofs) = true)).
     3343#l elim l
     3344[ 1: #m #m' #b #ofs #_ normalize #H destruct @conj try @conj try @conj try @conj try @conj try @refl
     3345     [ 1: #b0 @conj try @refl
     3346(*     | 2: #Habsurd @False_ind /2 by le_S_O_absurd/*)
     3347     | 2,3: #i #Habsurd @False_ind elim i in Habsurd; try /2/
     3348     | 4: #o #Hout @refl
     3349     | 5: #H @False_ind /2 by le_S_O_absurd/ ]
     3350| 2: #hd #tl #Hind #m #m' #b #ofs #Hsize_bound #Hstoren
     3351     whd in Hstoren:(??%?);
     3352     cases (some_inversion ????? Hstoren) #m'' * #Hbestorev -Hstoren #Hstoren
     3353     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HI #HJ #HK
     3354     lapply (Hind … Hstoren) [ 1: /2 by le_S_to_le/ ] * * * * *
     3355     #HC #HD #HE #HF #HV #HW @conj try @conj try @conj try @conj try @conj
     3356     [ 1: <HA <HC @refl
     3357     | 2: #b elim (HB b) #HF #HG elim (HD b) #HG #HH @conj try //     
     3358     | 4: *
     3359          [ 1: #_ <HJ whd in match (nth 0 ???);
     3360               lapply (HV ofs ?)
     3361               [ 1: #i #Hlt @sym_neq % #Heq lapply (shiftn_no_wrap (S i) ? ofs)
     3362                    [ 1: normalize in Hsize_bound;
     3363                         cut (|tl| < 8) [ /2 by lt_plus_to_minus_r/ ]
     3364                         #Hlt' lapply (transitive_lt … Hlt Hlt') // ]
     3365                    * #H @H whd in match (shiftn ??); @Heq
     3366               | 2: cases ofs #ofs' normalize // ]
     3367          | 2: #i' #Hlt lapply (HF i' ?)
     3368               [ 1: normalize normalize in Hlt; lapply (monotonic_pred … Hlt) //
     3369               | 2: #H whd in match (nth_opt ???); >H @refl ] ]
     3370     | 5: #o #H >HV
     3371          [ 2: #i #Hlt @(H (S i) ?)
     3372               normalize normalize in Hlt; /2 by le_S_S/
     3373          | 1: @HK @(H 0) // ]     
     3374     | 6: #_ @(bestorev_to_valid_pointer … Hbestorev)
     3375     | 3: *
     3376          [ 1: #_ <HJ whd in match (shiftn ??);
     3377               lapply (Zleb_true_to_Zle (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
     3378               lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
     3379               whd in match (low_bound ??); whd in match (high_bound ??);
     3380               cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
     3381               cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
     3382               [ 2: normalize #Habsurd destruct ] normalize nodelta #Hltb
     3383               lapply (Zltb_true_to_Zlt … Hltb) #Hlt' #Hleb lapply (Hleb (refl ??)) -Hleb #Hleb'
     3384               normalize @conj try assumption
     3385          | 2: #i' #Hlt cases (HB b) #Hlow1 #Hhigh1 cases (HD b) #Hlow2 #Hhigh2
     3386               lapply (HE i' ?) [ 1: normalize in Hlt ⊢ %;lapply (monotonic_pred … Hlt) // ]
     3387               >Hlow1 >Hhigh1 * #H1 #H2 @conj try @H1 try @H2
     3388          ]
     3389     ]
     3390] qed.
     3391
     3392lemma storen_beloadv_ok :
     3393  ∀m,m',b,ofs,hd,tl.
     3394  |hd::tl| ≤ 8 → (* 8 is the size of a double. *)
     3395  storen m (mk_pointer b ofs) (hd::tl) = Some ? m' →
     3396  ∀i. i < |hd::tl| → beloadv m' (mk_pointer b (shiftn ofs i)) = nth_opt ? i (hd::tl).
     3397#m #m' #b #ofs #hd #tl #Hle #Hstoren
     3398lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
     3399#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
     3400#i #Hle lapply (Hdata i Hle) #Helt >Helt
     3401whd in match (beloadv ??); whd in match (nth_opt ???);
     3402lapply (Hvalid_ptr ?) try //
     3403whd in ⊢ ((??%?) → ?);
     3404>Hnext cases (Zltb (block_id b) (nextblock m))
     3405[ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct ]
     3406>andb_lsimpl_true normalize nodelta
     3407whd in match (low_bound ??); whd in match (high_bound ??);
     3408cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H
     3409lapply (Hvalid_offs i Hle) * #Hzle #Hzlt
     3410>(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl
     3411qed.
     3412
     3413lemma loadn_beloadv_ok :
     3414  ∀size,m,b,ofs,result.
     3415  loadn m (mk_pointer b ofs) size = Some ? result →
     3416  ∀i. i < size → beloadv m (mk_pointer b (shiftn ofs i)) = nth_opt ? i result.
     3417#size elim size
     3418[ 1: #m #b #ofs #result #Hloadn *
     3419     [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
     3420     | 2: #i' #Habsurd @False_ind /2 by le_S_O_absurd/ ]
     3421| 2: #size' #Hind_size #m #b #ofs #result #Hloadn #i
     3422     elim i
     3423     [ 1: #_
     3424          cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
     3425          cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq
     3426          destruct (Heq) whd in match (shiftn ofs 0);
     3427          >Hbeloadv @refl
     3428    | 2: #i' #Hind #Hlt
     3429         whd in match (shiftn ofs (S i'));
     3430         lapply (Hind ?)
     3431         [ /2 by lt_S_to_lt/ ] #Hbeloadv_ind
     3432         whd in Hloadn:(??%?);
     3433         cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
     3434         cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq -Hloadn'
     3435         destruct (Heq)
     3436         @Hind_size [ 2: lapply Hlt normalize @monotonic_pred ]
     3437         @Hloadn_tl
     3438    ]
     3439] qed.
     3440
     3441lemma storen_loadn_nonempty :
     3442  ∀data,m,m',b,ofs.
     3443  |data| ≤ 8 →
     3444  storen m (mk_pointer b ofs) data = Some ? m' →
     3445  ∃result. loadn m' (mk_pointer b ofs) (|data|) = Some ? result ∧ |result|=|data|.
     3446#data elim data
     3447[ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ]
     3448#hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren
     3449lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
     3450#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
     3451cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0
     3452whd in match (loadn ???);
     3453lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
     3454whd in match (beloadv ??);
     3455whd in match (low_bound ??); whd in match (high_bound ??);
     3456>Hnext
     3457cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
     3458normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh
     3459cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta
     3460[ 2: #Habsurd destruct ] >andb_lsimpl_true
     3461#Hltb >Hltb normalize nodelta
     3462cases (Hind  … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ]
     3463#tl' * #Hloadn >Hloadn #Htl' normalize nodelta
     3464%{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl
     3465normalize >Htl' @refl
     3466qed.
     3467
     3468let rec double_list_ind
     3469  (A : Type[0])
     3470  (P : list A → list A → Prop)
     3471  (base_nil  : P [ ] [ ])
     3472  (base_l1   : ∀hd1,l1. P (hd1::l1) [ ])
     3473  (base_l2   : ∀hd2,l2. P [ ] (hd2::l2))
     3474  (ind  : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2))
     3475  (l1, l2 : list A) on l1 ≝
     3476match l1 with
     3477[ nil ⇒
     3478  match l2 with
     3479  [ nil ⇒ base_nil
     3480  | cons hd2 tl2 ⇒ base_l2 hd2 tl2 ]
     3481| cons hd1 tl1 ⇒ 
     3482  match l2 with
     3483  [ nil ⇒ base_l1 hd1 tl1
     3484  | cons hd2 tl2 ⇒
     3485    ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2)
     3486  ]
     3487]. 
     3488
     3489lemma nth_eq_tl :
     3490  ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2.
     3491  (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) →
     3492  (∀i. nth_opt A i l1 = nth_opt A i l2).
     3493#A #l1 #l2 @(double_list_ind … l1 l2)
     3494[ 1: #hd1 #hd2 #_ #i elim i try /2/
     3495| 2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
     3496| 3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
     3497| 4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2
     3498     #Hind
     3499     @(λi. Hind (S i))
     3500] qed.     
     3501
     3502
     3503lemma nth_eq_to_eq :
     3504  ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2.
     3505#A #l1 elim l1
     3506[ 1: #l2 #H lapply (H 0) normalize
     3507     cases l2
     3508     [ 1: //
     3509     | 2: #hd2 #tl2 normalize #Habsurd destruct ]
     3510| 2: #hd1 #tl1 #Hind *
     3511     [ 1: #H lapply (H 0) normalize #Habsurd destruct
     3512     | 2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq)
     3513          >(Hind tl2) try @refl @(nth_eq_tl … H)
     3514     ]
     3515] qed.
     3516
     3517(* for leb_elim, shadowed in positive.ma *)
     3518definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop.
     3519(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim.
     3520
     3521include alias "arithmetics/nat.ma".
     3522
     3523lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. |l| ≤ i → nth_opt A i l = None ?.
     3524#A #l elim l //
     3525#hd #tl #H #i elim i
     3526[ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/
     3527| 2: #i' #H' #Hle whd in match (nth_opt ???); @H /2 by monotonic_pred/
     3528] qed.
     3529
     3530lemma storen_loadn_ok :
     3531  ∀data.
     3532  |data| ≤ 8 → (* 8 is the size of a double. *)
     3533  ∀m,m',b,ofs.
     3534  storen m (mk_pointer b ofs) data = Some ? m' →
     3535  loadn m' (mk_pointer b ofs) (|data|) = Some ? data.
     3536#data elim data try // #hd #tl #Hind #Hle #m #m' #b #ofs #Hstoren
     3537lapply (storen_beloadv_ok m m' …  Hle Hstoren) #Hyp_storen
     3538cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz
     3539lapply (loadn_beloadv_ok (|hd::tl|) m' b ofs … Hloadn) #Hyp_loadn
     3540cut (∀i. i < |hd::tl| → nth_opt ? i (hd::tl) = nth_opt ? i result)
     3541[ #i #Hlt lapply (Hyp_storen … i Hlt) #Heq1
     3542  lapply (Hyp_loadn … i Hlt) #Heq2 >Heq1 in Heq2; // ]
     3543#Hyp
     3544cut (result = hd :: tl)
     3545[ 2: #Heq destruct (Heq) @Hloadn ]
     3546@nth_eq_to_eq #i @sym_eq
     3547@(leb_elim' … (S i) (|hd::tl|))
     3548[ 1: #Hle @(Hyp ? Hle)
     3549| 2: #Hnle cut (|hd::tl| ≤ i)
     3550     [ lapply (not_le_to_lt … Hnle) normalize /2 by monotonic_pred/ ]
     3551     #Hle'
     3552     >nth_miss // >nth_miss //
     3553] qed.
     3554
     3555(* In order to prove the lemma on store_value_of_type and load_value_of_type,
     3556   we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *)
     3557lemma typesize_bounded : ∀ty. typesize ty ≤ 8.
     3558* try //
     3559[ 1: * try //
     3560| 2: * try //
     3561] qed.
     3562
     3563(* Lifting bound on make_list *)
     3564lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → |make_list A elt sz| ≤ bound.
     3565#A #sz elim sz try //
     3566#sz' #Hind #bound #elt #Hbound normalize
     3567cases bound in Hbound;
     3568[ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
     3569| 2: #bound' #Hbound' lapply (Hind bound' elt ?)
     3570     [ 1: /2 by monotonic_pred/
     3571     | 2: /2 by le_S_S/ ]
     3572] qed.
     3573
     3574lemma bytes_of_bitvector_bounded :
     3575  ∀sz,bv. |bytes_of_bitvector (size_intsize sz) bv| = size_intsize sz.
     3576* #bv normalize
     3577[ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 //
     3578| 2: cases (vsplit ????) normalize nodelta #bv0 #bv1
     3579     cases (vsplit ????) normalize nodelta #bv2 #bv3 //
     3580| 3: cases (vsplit ????) normalize nodelta #bv0 #bv1
     3581     cases (vsplit ????) normalize nodelta #bv2 #bv3
     3582     cases (vsplit ????) normalize nodelta #bv4 #bv5
     3583     cases (vsplit ????) normalize nodelta #bv6 #bv7
     3584     //
     3585] qed.
     3586
     3587lemma map_bounded :
     3588  ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|.
     3589  #A #B #l elim l try //
     3590qed.
     3591
     3592lemma fe_to_be_values_bounded :
     3593  ∀ty,v. |fe_to_be_values ty v| ≤ 8.
     3594#ty cases ty
     3595[ 3: #fsz #v whd in match (fe_to_be_values ??);
     3596     cases v normalize nodelta
     3597     [ 1: @makelist_bounded @typesize_bounded
     3598     | 2: * normalize nodelta #bv
     3599          >map_bounded >bytes_of_bitvector_bounded //
     3600     | 3: #fl @makelist_bounded @typesize_bounded
     3601     | 4: //
     3602     | 5: #ptr // ]
     3603| 2: #v whd in match (fe_to_be_values ??);
     3604     cases v normalize nodelta
     3605     [ 1: @makelist_bounded @typesize_bounded
     3606     | 2: * normalize nodelta #bv
     3607          >map_bounded >bytes_of_bitvector_bounded //
     3608     | 3: #fl @makelist_bounded @typesize_bounded
     3609     | 4: //
     3610     | 5: #ptr // ]
     3611| 1: #sz #sg #v whd in match (fe_to_be_values ??);
     3612     cases v normalize nodelta
     3613     [ 1: @makelist_bounded @typesize_bounded
     3614     | 2: * normalize nodelta #bv
     3615          >map_bounded >bytes_of_bitvector_bounded //
     3616     | 3: #fl @makelist_bounded @typesize_bounded
     3617     | 4: //
     3618     | 5: #ptr // ]
     3619] qed.
     3620
     3621
     3622definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v.
     3623  match ty with
     3624  [ ASTint sz sg ⇒
     3625    match v with
     3626    [ Vint sz' sg' ⇒ sz = sz' (* The sign does not matter *)
     3627    | _ ⇒ False ]
     3628  | ASTptr ⇒
     3629    match v with
     3630    [ Vptr p ⇒ True
     3631    | _ ⇒ False ]
     3632  | ASTfloat fsz ⇒
     3633    match v with
     3634    [ Vfloat _ ⇒ True
     3635    | _ ⇒ False ]   
     3636  ].
     3637
     3638
     3639definition type_consistent_with_value : type → val → Prop ≝ λty,v.
     3640match access_mode ty with
     3641[ By_value chunk ⇒ ast_typ_consistent_with_value chunk v
     3642| _ ⇒ True
     3643].
     3644
     3645
     3646(* We also need the following property. It is not provable unless [v] and [ty] are consistent. *)
     3647lemma fe_to_be_values_size :
     3648  ∀ty,v. ast_typ_consistent_with_value ty v →
     3649         typesize ty = |fe_to_be_values ty v|.
     3650*
     3651[ 1: #sz #sg #v
     3652     whd in match (fe_to_be_values ??); cases v
     3653     normalize in ⊢ (% → ?);
     3654     [ 1,4: @False_ind
     3655     | 2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta
     3656          >map_bounded >bytes_of_bitvector_bounded cases sz' //
     3657     | 3: #f normalize in ⊢ (% → ?); @False_ind
     3658     | 5: #p normalize in ⊢ (% → ?); @False_ind ]
     3659| 2: #v cases v
     3660     normalize in ⊢ (% → ?);
     3661     [ 1,4: @False_ind
     3662     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
     3663     | 3: #f normalize in ⊢ (% → ?); @False_ind
     3664     | 5: #p #_ // ]
     3665| 3: #fsz #v cases v
     3666     normalize in ⊢ (% → ?);
     3667     [ 1: @False_ind
     3668     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
     3669     | 3: #f #_ cases fsz //
     3670     | 4: @False_ind
     3671     | 5: #p normalize in ⊢ (% → ?); @False_ind ]
     3672] qed.
     3673
     3674(* Not verified for floats atm. Restricting to integers. *)
     3675lemma fe_to_be_to_fe_value : ∀sz,sg,v.
     3676  ast_typ_consistent_with_value (ASTint sz sg) v →
     3677  (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v).
     3678#sz #sg #v
     3679whd in match (fe_to_be_values ??);
     3680cases v normalize in ⊢ (% → ?);
     3681[ 1,4: @False_ind
     3682| 3: #f @False_ind
     3683| 5: #p @False_ind
     3684| 2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta
     3685     cases sz' in i'; #i normalize nodelta
     3686     normalize in i;
     3687     whd in match (be_to_fe_value ??);
     3688     normalize in match (size_intsize ?);
     3689     whd in match (bytes_of_bitvector ??);
     3690     [ 1: lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i
     3691          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
     3692          whd in match (build_integer_val ??);
     3693          >(BitVector_O … ri) //
     3694     | 2: lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i
     3695          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
     3696          whd in match (build_integer_val ??);
     3697          normalize in match (size_intsize ?);
     3698          whd in match (bytes_of_bitvector ??);
     3699          lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri
     3700          <(vsplit_prod … Heq_ri) normalize nodelta >Heq_ri
     3701          whd in match (build_integer_val ??);
     3702          >(BitVector_O … rri) //
     3703     | 3: lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i
     3704          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
     3705          whd in match (build_integer_val ??);
     3706          normalize in match (size_intsize ?);
     3707          whd in match (bytes_of_bitvector ??);
     3708          lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB
     3709          <(vsplit_prod … Heq_iB) normalize nodelta >Heq_iB
     3710          whd in match (bytes_of_bitvector ??);
     3711          lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD
     3712          <(vsplit_prod … Heq_iD) normalize nodelta >Heq_iD
     3713          whd in match (bytes_of_bitvector ??);
     3714          lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF
     3715          <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF
     3716          >(BitVector_O … iH) @refl ]
     3717] qed.                   
     3718
     3719(* It turns out that the following property is not true in general. Floats are converted to
     3720   BVundef, which are converted back to Vundef. But we care only about ints.  *)
     3721lemma storev_loadv_ok :
     3722  ∀sz,sg,m,b,ofs,v,m'.
     3723    ast_typ_consistent_with_value (ASTint sz sg) v →
     3724    store (ASTint sz sg) m (mk_pointer b ofs) v = Some ? m' →
     3725    load (ASTint sz sg) m' (mk_pointer b ofs) = Some ? v.
     3726#sz #sg #m #b #ofs #v #m' #H
     3727whd in ⊢ ((??%?) → (??%?)); #Hstoren
     3728lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren)
     3729>(fe_to_be_values_size … H) #H >H normalize nodelta
     3730>fe_to_be_to_fe_value try //
     3731qed.
     3732
     3733(* For the arguments exposed before, we restrict the lemma to ints.
     3734 *)
     3735lemma store_value_load_value_ok :
     3736  ∀sz,sg,m,b,ofs,v,m'.
     3737    type_consistent_with_value (Tint sz sg) v →
     3738    store_value_of_type (Tint sz sg) m b ofs v = Some ? m' →
     3739    load_value_of_type (Tint sz sg) m' b ofs = Some ? v.
     3740#sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?);
     3741cases v in H; normalize nodelta
     3742[ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #vf #_ @False_ind | 4: #_ @False_ind | 5: #vp #_ @False_ind ]
     3743#Heq >Heq in H; #H
     3744(* The lack of control on unfolds is extremely annoying. *)
     3745whd in match (store_value_of_type ?????); #Hstoren
     3746lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren)
     3747whd in match (load_value_of_type ????);
     3748>(fe_to_be_values_size … H) #H' >H' normalize nodelta
     3749>fe_to_be_to_fe_value try //
     3750qed.
     3751
     3752lemma load_int_value_inversion :
     3753  ∀t,m,p,sz,i. load_value_of_type' t m p = Some ? (Vint sz i) → ∃sg. t = Tint sz sg.
     3754#t #m * #b #o #sz #i whd in match (load_value_of_type' ???);
     3755cases t
     3756[ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     3757| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta
     3758whd in match (load_value_of_type ????);
     3759[ 4,5,6,7,9: #Habsurd destruct ]
     3760whd in match (be_to_fe_value ??);
     3761cases (loadn ???) normalize nodelta
     3762[ 1,3,5,7: #Habsurd destruct ]
     3763*
     3764[ 1,3,5,7: #Heq normalize in Heq; destruct ]
     3765#hd #tl
     3766[ 2,3,4: cases hd
     3767  [ 1,2,7,8,13,14: whd in match (be_to_fe_value ??); #Heq destruct
     3768  | 4,5,10,11,16,17: #HA #Heq destruct (Heq) cases (eqb ??∧?) in e0;
     3769      normalize nodelta #Heq' destruct
     3770  | 6,12,18: #ptr #part #Heq destruct cases (pointer_of_bevals ?) in e0;
     3771             #foo normalize #Habsurd destruct
     3772  | *: #op1 #op2 #part #Heq destruct ]
     3773| 1: #H destruct cases hd in e0; normalize nodelta
     3774  [ 1,2: #Heq destruct
     3775  | 3: #op1 #op2 #part #Habsurd destruct
     3776  | 4: #by whd in match (build_integer_val ??);
     3777       cases (build_integer ??) normalize nodelta
     3778       [ 1: #Heq destruct
     3779       | 2: #bv #Heq destruct /2 by ex_intro/ ]
     3780  | 5: #p cases (eqb ?? ∧ ?) normalize nodelta #Heq destruct
     3781  | 6: #ptr #part cases (pointer_of_bevals ?) #foo normalize nodelta #Heq destruct ]
     3782] qed.
     3783
     3784lemma opt_to_res_load_int_value_inversion :
     3785 ∀t,m,p,sz,i.
     3786 (opt_to_res val (msg FailedLoad) (load_value_of_type' t m p) = OK ? (Vint sz i))
     3787  → ∃sg. t = Tint sz sg.
     3788#t #m #p #sz #i whd in match (opt_to_res ???);
     3789lapply (load_int_value_inversion t m p sz i)
     3790cases (load_value_of_type' t m p)
     3791[ 1: #H normalize nodelta #Habsurd destruct
     3792| 2: #v #H normalize nodelta #Heq destruct lapply (H (refl ??)) *
     3793     #sg #Heq >Heq /2 by ex_intro/
     3794] qed.
     3795
     3796lemma res_inversion : ∀A,B:Type[0]. ∀e:res A. ∀f:A → res B. ∀res:B.
     3797  match e with
     3798  [ OK x ⇒ f x
     3799  | Error msg ⇒ Error ? msg ] = OK ? res → 
     3800  ∃res_e. e = OK ? res_e ∧ OK ? res = f res_e.
     3801#A #B *
     3802[ 2: #err #f #res normalize nodelta #Habsurd destruct
     3803| 1: #a #f #res normalize nodelta #Heq destruct %{a} @conj try @refl >Heq @refl
     3804] qed.
     3805
     3806(* In order to prove the consistency of types wrt values, we need the following lemma. *)
     3807(*
     3808lemma exec_expr_Vint_type_inversion :
     3809  ∀ge,env,m,e,sz,i,tr. (exec_expr ge env m e=return 〈Vint sz i,tr〉) →
     3810                       ∃sg. typeof e = Tint sz sg.
     3811#ge #env #m * #ed #ty
     3812@(expr_ind2 … (λed,ty.∀sz:intsize.∀i:bvint sz.∀tr:trace.
     3813                  exec_expr ge env m (Expr ed ty)=return 〈Vint sz i,tr〉 →
     3814                  ∃sg:signedness.typeof (Expr ed ty)=Tint sz sg) … (Expr ed ty))
     3815[ 1: #e' #ty' #H @H
     3816| 2: #sz #i #t #sz0 #i0 #tr whd in ⊢ ((??%?) → ?); cases t
     3817     [ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     3818     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta
     3819     [ 1: @(eq_intsize_elim … sz tsz) normalize nodelta
     3820          [ 2: #Hsz_eq destruct (Hsz_eq) normalize #Heq destruct (Heq)
     3821               %{tsg} @refl
     3822          | 1: #_ normalize #Habsurd destruct (Habsurd) ]
     3823     | *: #Habsurd normalize in Habsurd; destruct ]
     3824| 3: #f #t #sz #i #tr whd in ⊢ ((??%?) → ?); #H normalize in H; destruct (H)
     3825| 4: #id #t #sz #i #tr whd in ⊢ ((??%?) → ?);
     3826      @(match exec_lvalue' ge env m (Evar id) t
     3827        return λr. r = exec_lvalue' ge env m (Evar id) t → ?
     3828        with
     3829        [ OK x ⇒ λHeq. ?
     3830        | Error msg ⇒ λHeq. ?
     3831        ] (refl ? (exec_lvalue' ge env m (Evar id) t))) normalize nodelta
     3832     [ 2: normalize #Habsurd destruct ] #Hload
     3833     cases (bind_inversion ????? Hload) #loadval * #Heq_loadval #Heq_res
     3834     normalize in Heq_res; destruct (Heq_res)
     3835     -Hload
     3836     whd in Heq_loadval:(??%%); lapply Heq_loadval
     3837      @(match load_value_of_type' t m (\fst  x)
     3838        return λr. r = load_value_of_type' t m (\fst  x) → ?
     3839        with
     3840        [ None ⇒ λHeq. ?
     3841        | Some v' ⇒ λHeq. ?
     3842        ] (refl ? (load_value_of_type' t m (\fst  x)))) normalize nodelta
     3843     [ 1: #Habsurd destruct ]
     3844     #Heq_v' destruct (Heq_v')
     3845     cases (load_int_value_inversion … (sym_eq ??? Heq)) #sg #Htyp_eq
     3846     >Htyp_eq %{sg} @refl
     3847| 5: #e #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?);
     3848     whd in match (exec_lvalue' ?????);
     3849     @(match exec_expr ge env m e
     3850       return λx. x = (exec_expr ge env m e) → ?
     3851       with
     3852       [ OK res ⇒ λH. ?
     3853       | Error msg ⇒ λH. ? ] (refl ? (exec_expr ge env m e)))
     3854      normalize nodelta
     3855     [ 2: #Habsurd destruct ]
     3856     cases res in H; #vres #trres #Hexec #H     
     3857     cases (res_inversion ????? H) -H * * #b' #o' #tr' *
     3858     cases vres in Hexec; normalize nodelta
     3859     [ 1: #_ #Habsurd destruct
     3860     | 2: #sz' #i' #_ #Habsurd destruct
     3861     | 3: #f #_ #Habsurd destruct
     3862     | 4: #_ #Habsurd destruct ]
     3863     #p #Heq_exec_expr #Heq destruct (Heq) #Heq
     3864     lapply (sym_eq ??? Heq) -Heq #Heq
     3865     cases (bind_inversion ????? Heq) -Heq #x * #Hload_value
     3866     #Heq normalize in Heq; destruct (Heq)
     3867     @(opt_to_res_load_int_value_inversion … Hload_value)
     3868| 6: #e #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); #H
     3869     cases (res_inversion ????? H) * * #b #o #tr * #Hexec_lvalue
     3870     cases t
     3871     [ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     3872     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta
     3873     #Habsurd destruct
     3874| 7: #op #arg #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); #H
     3875      cases (res_inversion ????? H) * #v #tr * #Hexec_expr
     3876      #H' lapply (sym_eq ??? H') -H' #H'
     3877      cases (bind_inversion ????? H') #v' * #Hopt_sem #Hvalues
     3878      normalize in Hvalues:(??%%); destruct (Hvalues) -H' -H
     3879     
     3880      lapp
     3881      >Hopt_sem in H';
     3882      destruct (Hvalues)
     3883     
     3884     whd in match (exec_lvalue ????);*)
     3885     
     3886
     3887
    30003888
    30013889(* Main theorem. To be ported and completed to memory injections. TODO *)
    30023890theorem switch_removal_correction :
    3003   ∀ge,ge',s1, s1', tr, s2.
     3891  ∀ge,ge'.
    30043892  switch_removal_globals ? fundef_switch_removal ge ge' →
     3893  ∀s1,s1',tr,s2.
    30053894  switch_state_sim ge s1 s1' →
    3006   exec_step ge s1 = Value … 〈tr,s2〉 →
    3007   eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr.
    3008 #ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state
    3009 @cthulhu
    3010 qed.
    3011 
    3012 (*
     3895  exec_step ge s1 = Value … 〈tr,s2〉 → 
     3896  ∃n. after_n_steps (S n) … clight_exec ge' s1'
     3897  (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2').
     3898#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state
    30133899inversion Hsim_state
    30143900[ 1: (* regular state *)
    3015   #sss_statement #sss_result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars
     3901  #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars
    30163902  #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp
    3017   #sss_env_hyp #sss_result_hyp #sss_k_hyp #Hext_fresh_for_ge
     3903  #sss_env_hyp #sss_writeable_hyp #sss_result_rec #sss_result_hyp #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge
     3904  #Hs1_eq #Hs1_eq'
    30183905  elim (sim_related_globals … ge ge'
    30193906             sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars
    30203907             sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge)
    3021   #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_
     3908  #Hsim_expr #Hsim_lvalue #_
     3909  (* II. Case analysis on the statement. *)
    30223910  cases sss_statement in sss_lu_fresh sss_result_hyp;
    30233911  (* Perform the intros for the statements *)
     
    30263914  | 14: #lab | 15: #cost #body ]
    30273915  #sss_lu_fresh #sss_result_hyp
    3028   [ 1: (* Skip *)
    3029     whd in match (switch_removal ???) in sss_result_hyp;
    3030     <(some_inj ??? sss_result_hyp)
     3916  [ 1: (* Skip statement *)
     3917    whd in match (switch_removal ??) in sss_result_hyp; >sss_result_proj <sss_result_hyp
     3918    (* III. Case analysis on the continuation. *)
    30313919    inversion sss_k_hyp normalize nodelta
    3032     [ 1: #fvs #Hfvs_eq #Hk #Hk' #_ #Hexec_step
    3033          @(eventually_now ????) whd in match (exec_step ??);
     3920    [ 1: #new_vars #Hnew_vars_eq #Hk #Hk' #_ #Hexec_step %{0} whd whd in ⊢ (??%?);
    30343921         >(prod_eq_lproj ????? sss_func_hyp)
    30353922         >fn_return_simplify
    30363923         whd in match (exec_step ??) in Hexec_step;
     3924         (* IV. Case analysis on the return type *)
    30373925         cases (fn_return sss_func) in Hexec_step;
    30383926         [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     
    30403928         normalize nodelta
    30413929         whd in ⊢ ((??%?) → ?);
    3042          [ 1: #H destruct (H) %{(Returnstate Vundef Kstop (free_list sss_m_ext (blocks_of_env sss_env_ext)))}
    3043               @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)}
    3044               [ 1: @(lset_difference ? sss_writeable (blocks_of_env sss_env_ext))
    3045               | 3: @swc_stop
    3046               | 2:
    3047 *)
    3048    
     3930         [ 1: #H destruct (H) % try @refl
     3931              /3 by sws_returnstate, swc_stop, memext_free_extended_environment, memory_ext_writeable_eq/
     3932         | *: #Habsurd destruct (Habsurd) ]
     3933    | 2: #s #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #Hsss_k_hyp
     3934         #Hexec_step %{0} whd
     3935         >(prod_eq_lproj ????? sss_func_hyp)
     3936         whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl
     3937         <sss_func_hyp
     3938         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
     3939         %1{u (refl ? (switch_removal s u))} try assumption try @refl         
     3940         #id #Hmem lapply (Hext_fresh_for_ge id Hmem) #Hfind <(rg_find_symbol … Hrelated id) @Hfind
     3941    | 3: #cond #body #k #k' #fgen #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     3942         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
     3943         #Hexec_step %{0} whd whd in Hexec_step;
     3944         >(prod_eq_lproj ????? sss_func_hyp)
     3945         whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl         
     3946         %1{ ((switch_removal (Swhile cond body) fgen))} try assumption try @refl
     3947         [ 1: <sss_func_hyp @refl
     3948         | 2: destruct normalize cases (switch_removal ??) * #body' #fvs' #u' @refl
     3949         | 3: whd in match (switch_removal ??);
     3950              cases (switch_removal body fgen) in Hincl; * #body' #fvs' #fgen' normalize nodelta #H @H
     3951         | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     3952    | 4: #cond #body #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     3953         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')   
     3954         #Hexec_step %{0} whd whd in Hexec_step:(??%?) ⊢ (??%?);
     3955         cases (bindIO_inversion ??????? Hexec_step) #x1 * #Hexec
     3956         >(Hsim_expr … Hexec)
     3957         >bindIO_Value cases (exec_bool_of_val ??)
     3958         [ 2: #err normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
     3959         #b whd in match (m_bind ?????); whd in match (m_bind ?????);
     3960         cases b normalize nodelta #H whd in H:(??%%) ⊢ %; destruct (H)
     3961         try @conj try @refl
     3962         [ 1: %{u … (switch_removal (Sdowhile cond body) u)} try assumption try //
     3963              [ 1: destruct normalize cases (switch_removal body u) * #body' #fvs' #u' @refl
     3964              | 2: whd in match (switch_removal ??);
     3965                   cases (switch_removal body u) in Hincl; * #body' #fvs' #u' normalize nodelta #H @H
     3966              | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     3967         | 2: %{u … (switch_removal Sskip u) } try assumption try //
     3968              [ 1: @(fresh_for_Sskip … Hfresh)
     3969              | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
     3970    | 5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_
     3971         #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     3972         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
     3973         #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step)
     3974         @conj try @refl
     3975         %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try //
     3976         #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
     3977    | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
     3978         #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     3979         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
     3980         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
     3981         %1{u … new_vars … sss_writeable (switch_removal stmt1 u)} try assumption try //
     3982         [ 1: lapply (fresh_to_substatements … Hfresh) normalize * * //
     3983         | 2: whd in match (switch_removal ??) in Hincl;
     3984              cases (switch_removal stmt1 u) in Hincl; * #stmt1' #fvs1' #u' normalize nodelta
     3985              cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' normalize nodelta
     3986              whd in match (ret_vars ??); /2 by All_append_l/
     3987         | 3: @(swc_for3 … u) //
     3988         | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     3989    | 7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
     3990         #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     3991         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
     3992         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
     3993         %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)}
     3994         try //
     3995         [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize
     3996              cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize
     3997              cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl
     3998         | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     3999    | 8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     4000         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
     4001         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
     4002         %1{sss_lu … new_vars … sss_writeable} try // try assumption
     4003         [ 1: destruct (sss_result_hyp) @refl
     4004         | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     4005    | 9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_
     4006         #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     4007         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
     4008         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; whd in ⊢ (??%?);
     4009         >(prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify
     4010         cases (fn_return sss_func) in Hexec; normalize nodelta
     4011         [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     4012         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     4013         #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl
     4014         /3 by sws_returnstate, swc_call, memext_free_extended_environment/
     4015    ]
     4016  | 2: (* Assign statement *)
     4017       lapply (exec_lvalue_sim_aux … Hsim_lvalue) #Hsim
     4018       #Hexec %{0} whd in sss_result_hyp:(??%?);
     4019       cases (bindIO_inversion ??????? Hexec) #xl * #Heq_lhs #Hexec_lhs
     4020       cases (bindIO_inversion ??????? Hexec_lhs) #xr * #Heq_rhs #Hexec_rhs
     4021       cases (bindIO_inversion ??????? Hexec_rhs) #xs * #Heq_store #Hexec_store
     4022       whd whd in Hexec_store:(??%%) ⊢ (??%?); >sss_result_proj <sss_result_hyp normalize nodelta
     4023       >(Hsim … Heq_lhs) whd in match (m_bind ?????);
     4024       >(Hsim_expr … Heq_rhs) >bindIO_Value
     4025       lapply (memext_store_value_of_type' sss_m sss_m_ext xs sss_writeable (typeof lhs) (\fst  xl) (\fst  xr) sss_mem_hyp ?)
     4026       [ 1: cases (store_value_of_type' ????) in Heq_store;
     4027            [ 1: normalize #Habsurd destruct (Habsurd)
     4028            | 2: #m normalize #Heq destruct (Heq) @refl ] ]
     4029       * #m_ext' * #Hstore_eq #Hnew_ext >Hstore_eq whd in match (m_bind ?????);
     4030       whd destruct @conj try @refl
     4031       %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip  sss_lu) } try // try assumption
     4032       [ 1: @(fresh_for_Sskip … sss_lu_fresh)
     4033       | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     4034  | 3: (* Call statement *)
     4035       #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp)
     4036       whd whd in ⊢ (??%?); >sss_result_proj normalize nodelta
     4037       whd in Hexec:(??%?);
     4038       cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func
     4039       cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args
     4040       cases (bindIO_inversion ??????? Hexec_args) #called_fundef * #Heq_fundef #Hexec_typeeq
     4041       cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret
     4042       >(Hsim_expr … Heq_func) whd in match (m_bind ?????);
     4043       >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args)
     4044       whd in ⊢ (??%?);
     4045       >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef))
     4046       whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert
     4047       whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret
     4048       @(option_ind … retv) normalize nodelta
     4049       [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl
     4050            %2{sss_writeable … sss_mem_hyp}
     4051            cases called_fundef
     4052            [ 2: #id #tl #ty @I
     4053            | 1: #called_function whd
     4054                 cut (sss_func_tr = \fst (function_switch_removal sss_func))
     4055                 [ 1: <sss_func_hyp @refl ] #H >H -H
     4056                 cut (sss_new_vars = \snd (function_switch_removal sss_func))
     4057                 [ 1: <sss_func_hyp @refl ] #H >H -H
     4058                 @(swc_call … sss_k_hyp) try assumption
     4059                 <sss_func_hyp @refl ]
     4060       | 2: #ret_expr #Hexec_ret_expr
     4061            cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret
     4062            whd in ⊢ ((??%%) → (??%%)); #H destruct (H)
     4063            >(exec_lvalue_sim_aux … Hsim_lvalue … Heq_ret)
     4064            whd in ⊢ (??%?); whd @conj try @refl
     4065            cut (sss_func_tr = \fst (function_switch_removal sss_func))
     4066            [ 1: <sss_func_hyp @refl ] #H >H -H
     4067            @(sws_callstate … sss_writeable … sss_mem_hyp)
     4068            cases called_fundef
     4069            [ 2: #id #tl #ty @I
     4070            | 1: #called_function whd
     4071                 cut (sss_func_tr = \fst (function_switch_removal sss_func))
     4072                 [ 1: <sss_func_hyp @refl ] #H >H -H
     4073                 cut (sss_new_vars = \snd (function_switch_removal sss_func))
     4074                 [ 1: <sss_func_hyp @refl ] #H >H -H
     4075                 @(swc_call … sss_k_hyp) try assumption
     4076                 <sss_func_hyp @refl ] ]
     4077  | 4: (* Sequence statement *)
     4078       #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec)
     4079       >sss_result_proj <sss_result_hyp
     4080       cases (switch_removal_elim stm1 sss_lu) #stm1' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
     4081       cases (switch_removal_elim stm2 u') #stm2' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta
     4082       normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try //
     4083       [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * //
     4084       | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
     4085            /2 by All_append_l/
     4086       | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     4087       @(swc_seq … u') try //
     4088       [ 2: >HeqB @refl
     4089       | 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * #_ @fresher_for_univ
     4090            lapply (switch_removal_fte stm1 sss_lu) >HeqA #H @H
     4091       | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
     4092            /2 by All_append_r/
     4093       ]
     4094  | 5: (* If-then-else *)
     4095       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
     4096       cases (switch_removal_elim iftrue sss_lu) #iftrue' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
     4097       cases (switch_removal_elim iffalse u') #iffalse' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta
     4098       whd whd in ⊢ (??%?);
     4099       cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond
     4100       cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hresult
     4101       whd in Hresult:(??%%); destruct (Hresult)
     4102       >(Hsim_expr … Heq_cond) >bindIO_Value
     4103       >Heq_bool whd in match (m_bind ?????); whd @conj try @refl
     4104       cases b normalize nodelta
     4105       [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try //
     4106             [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize //
     4107             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
     4108                  /2 by All_append_l/
     4109             | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     4110       | 2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try //
     4111             [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_
     4112                   @fresher_for_univ lapply (switch_removal_fte iftrue sss_lu) >HeqA #H @H
     4113             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
     4114                  /2 by All_append_r/                   
     4115             | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
     4116  | 6: (* While loop *)
     4117       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
     4118       >sss_result_proj <sss_result_hyp whd
     4119       cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond
     4120       cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool whd in ⊢ ((??%%) → ?);
     4121       cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
     4122       whd in ⊢ (? → (??%?));
     4123       >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool
     4124       whd in match (m_bind ?????); cases b normalize nodelta #Hresult destruct (Hresult)
     4125       whd @conj try @refl
     4126       [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try //
     4127             [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize //
     4128             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H
     4129             | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
     4130             | 3: @(swc_while … sss_lu) try //
     4131                  [ 1: >HeqA @refl
     4132                  | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H ]
     4133             ]
     4134       | 2: %{… sss_func_hyp … (switch_removal Sskip u')} try assumption try //
     4135            [ 1: lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte;
     4136                 @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh)
     4137            | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
     4138  | 7: (* do while loop *)
     4139       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
     4140       >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?);
     4141       cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
     4142       whd @conj try @refl
     4143       %1{sss_lu … sss_func_hyp … (switch_removal body sss_lu) }
     4144       try assumption try //
     4145       [ 1:  lapply (fresh_to_substatements … sss_lu_fresh) normalize * //
     4146       | 2: >HeqA @refl
     4147       | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H
     4148       | 5: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
     4149       | 4: @(swc_dowhile … sss_lu) try assumption try //
     4150            [ 1: >HeqA @refl
     4151            | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H           
     4152            ] ]       
     4153  | 8: (* for loop *)
     4154       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
     4155       >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?);
     4156       cases (switch_removal_elim init sss_lu) #init' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
     4157       cases (switch_removal_elim step u') #step' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta
     4158       cases (switch_removal_elim body u'') #body' * #fvs3' * #u''' #HeqC >HeqC normalize nodelta
     4159       lapply Hexec
     4160       @(match is_Sskip init with
     4161       [ inl Heq ⇒ ?
     4162       | inr Hneq ⇒ ?
     4163       ]) normalize nodelta
     4164       [ 2: lapply (simplify_is_not_skip … Hneq sss_lu) >HeqA * #pf
     4165            whd in match (ret_st ??) in ⊢ ((??%%) → ?); #Hneq >Hneq normalize nodelta
     4166            #Hexec' whd in Hexec':(??%%); destruct (Hexec') whd @conj try @refl
     4167            %1{sss_lu … sss_func_hyp (switch_removal init sss_lu)} try assumption try //
     4168            [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * * * //
     4169            | 2: >HeqA @refl
     4170            | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta
     4171                 >HeqB normalize nodelta >HeqC normalize nodelta
     4172                 /2 by All_append_l/
     4173            | 4: @(swc_for1 … u') try assumption try //
     4174                 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #HW #HX #HY #HZ
     4175                      @for_fresh_lift
     4176                      [ 1: @(fresher_for_univ … HY)
     4177                      | 2: @(fresher_for_univ … HZ)
     4178                      | 3: @(fresher_for_univ … HX) ]
     4179                      lapply (switch_removal_fte init sss_lu) >HeqA #Hs @Hs
     4180                 | 2: normalize >HeqB normalize nodelta >HeqC @refl
     4181                 | 3: lapply sss_incl <sss_result_hyp
     4182                      whd in match (ret_vars ??) in ⊢ (% → %);
     4183                      whd in match (switch_removal ??) in ⊢ (% → %);
     4184                      >HeqA normalize nodelta >HeqB normalize nodelta >HeqC
     4185                      normalize nodelta #H /2 by All_append_r/
     4186                  ] ]
     4187       | 1: -Hexec #Hexec' cases (bindIO_inversion ??????? Hexec') #condres * #Heq_cond #Hexec_cond
     4188            cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool
     4189            destruct (Heq) normalize in HeqA; lapply HeqA #HeqA' destruct (HeqA')
     4190            normalize nodelta
     4191            >(Hsim_expr … Heq_cond) whd in ⊢ ((??%?) → ?); #Hexec'
     4192            whd in match (m_bind ?????); >Heq_bool
     4193            cases b in Hexec'; normalize nodelta whd in match (bindIO ??????);
     4194            normalize #Hexec'' destruct (Hexec'') @conj try @refl
     4195            [ 1: %1{u'' … sss_func_hyp (switch_removal body u'')} try assumption try //
     4196                 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #_ #_ #_
     4197                      @fresher_for_univ lapply (switch_removal_fte step u') >HeqB
     4198                      #H @H
     4199                 | 2: >HeqC @refl
     4200                 | 3: lapply sss_incl <sss_result_hyp
     4201                      whd in match (ret_vars ??) in ⊢ (% → %);
     4202                      whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta
     4203                      >HeqB normalize nodelta >HeqC normalize nodelta
     4204                      /2 by All_append_r/
     4205                 | 4: @(swc_for2 … u') try assumption
     4206                      [ 1: >HeqB @refl
     4207                      | 2: >HeqB >HeqC @refl
     4208                      | 3: lapply sss_incl <sss_result_hyp
     4209                           whd in match (ret_vars ??) in ⊢ (% → %);
     4210                           whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta
     4211                           >HeqB normalize nodelta >HeqC normalize nodelta #H @H
     4212                      ]
     4213                 ]
     4214            | 2: %1{u' … sss_func_hyp … (switch_removal Sskip u')} try assumption try //
     4215                 [ 1: @(fresh_for_Sskip … sss_lu_fresh) ] ] ]
     4216        #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
     4217  | 9: (* break *)
     4218       #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta
     4219       lapply Hexec -Hexec
     4220       inversion sss_k_hyp
     4221       [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd)
     4222       | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq
     4223            #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
     4224            destruct
     4225            %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try //
     4226       | 3,4: #e #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
     4227            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
     4228            destruct
     4229            %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try //
     4230       | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
     4231            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
     4232            destruct
     4233            %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try //
     4234       | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk'
     4235            #Hres1 #Hres2 #Hincl #_ #Hnew_vars
     4236            #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
     4237            destruct
     4238            %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try //
     4239       | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk' #_ #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
     4240            #Heq destruct (Heq) whd @conj try @refl destruct
     4241            %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try //
     4242       | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold #Hdisjoint #_
     4243            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
     4244            #Heq destruct (Heq) ]
     4245       #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
     4246  | 10: (* continue *)
     4247       #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta
     4248       lapply Hexec -Hexec
     4249       inversion sss_k_hyp
     4250       [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd)
     4251       | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq
     4252            #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
     4253            destruct
     4254            %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try //
     4255       | 3: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
     4256            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
     4257            destruct
     4258            %1{uk … (switch_removal (Swhile ek sk) uk)} try assumption try //
     4259            [ 1: normalize cases (switch_removal sk uk) * #sk' #fvs' #uk' @refl
     4260            | 2: whd in match (switch_removal ??); lapply Hincl
     4261                 cases (switch_removal sk uk) * #body' #fvs' #uk'
     4262                 /2 by All_append_r/ ]                 
     4263       | 4: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
     4264            #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Hexec
     4265            cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond
     4266            cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hexec_bool
     4267            >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool whd in match (m_bind ?????);
     4268            cases b in Hexec_bool; normalize nodelta whd in ⊢ ((??%?) → ?);
     4269            #Heq whd whd in Heq:(??%%); destruct (Heq) @conj try @refl
     4270            [ 1: destruct %1{uk … (switch_removal (Sdowhile ek sk) uk)} try assumption try //
     4271                 [ 1: normalize cases (switch_removal sk uk) * #body' #fvs' #uk' @refl
     4272                 | 2: whd in match (switch_removal ??); lapply Hincl cases (switch_removal sk uk)
     4273                      * #body' #fvs' #uk' #H @H
     4274                 ]
     4275            | 2: destruct %1{uk … (switch_removal Sskip uk)} try assumption try //
     4276                 try @(fresh_for_Sskip … Hfresh_suk) ]
     4277       | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
     4278            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
     4279            destruct %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try //
     4280       | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' #Hres1 #Hres2 #Hincl #_
     4281            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
     4282            destruct %1{uk … (switch_removal s1k uk)} try assumption try //
     4283            [ 1: cases (fresh_to_substatements … Hfresh_suk) * * //
     4284            | 2: lapply Hincl whd in match (ret_vars ??) in ⊢ (% → ?);
     4285                 whd in match (switch_removal ??);
     4286                 cases (switch_removal s1k uk) * #s1k' #fvs1' #uk' normalize nodelta
     4287                 cases (switch_removal s2k uk') * #s2k' #fvs2' #uk'' normalize nodelta
     4288                 /2 by All_append_l/
     4289            | 3: @(swc_for3 … uk) try assumption try //
     4290            ]
     4291       | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk #_ #Hnew_vars_eq #Hk #Hk' #_
     4292            whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq)
     4293            whd @conj try @refl destruct
     4294            %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try //
     4295       | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold_vars_eq #Hdisjoint
     4296             #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
     4297            #Heq destruct (Heq) ]
     4298       #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
     4299  | 11: (* return *)
     4300        #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec
     4301        >sss_result_proj <sss_result_hyp normalize nodelta
     4302        cases retval in sss_lu_fresh sss_result_hyp; normalize nodelta
     4303        [ 1: #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?));
     4304             >(prod_eq_lproj ????? sss_func_hyp)
     4305             >fn_return_simplify
     4306             cases (fn_return sss_func) normalize nodelta
     4307             [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     4308             | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     4309             [ 1: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj try @refl
     4310                  /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/
     4311             | *: #Habsurd destruct (Habsurd) ]
     4312        | 2: #ret_expr #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?));
     4313             >(prod_eq_lproj ????? sss_func_hyp)
     4314             >fn_return_simplify
     4315             @(match type_eq_dec (fn_return sss_func) Tvoid with
     4316               [ inl H ⇒ ?
     4317               | inr H ⇒ ? ]) normalize nodelta
     4318             [ 1: #Habsurd destruct (Habsurd)
     4319             | 2: #Hexec
     4320                   cases (bindIO_inversion ??????? Hexec) #retres * #Heq_ret #Hexec_ret
     4321                   whd in Hexec_ret:(??%%); destruct (Hexec_ret)
     4322                   >(Hsim_expr … Heq_ret) whd in match (m_bind ?????); whd
     4323                   @conj try @refl
     4324                   /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/
     4325             ] ]
     4326  | 12: (* switch ! at long last *)
     4327        #Hexec whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec
     4328        >sss_result_proj <sss_result_hyp normalize nodelta #Hexec
     4329        cases (bindIO_inversion ??????? Hexec) * #condval #condtrace
     4330        cases condval normalize nodelta
     4331        [ 1: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     4332        | 3: #f * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     4333        | 4: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     4334        | 5: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
     4335        #sz #i * #Hexec_eq #Heq whd in Heq:(??%%); destruct (Heq)
     4336
     4337        cases (switch_removal_branches_elim … switchcases sss_lu) #switchcases' * #fvs' * #u' #Hbranch_eq
     4338        >Hbranch_eq normalize nodelta
     4339        cases (fresh_elim … u') #new * #u'' #Hfresh_eq >Hfresh_eq normalize nodelta
     4340        cases (simplify_switch_elim (Expr (Evar new) (typeof cond)) switchcases' u'') #simplified * #u'''
     4341        #Hswitch_eq >Hswitch_eq normalize nodelta
     4342        %{1} whd whd in ⊢ (??%?);
     4343        (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *)
     4344        whd in match (exec_lvalue ????);
     4345        (* show that the resulting ident is in the memory extension and that the lookup succeeds *)
     4346        -Hexec >Hbranch_eq in sss_result_hyp; normalize nodelta
     4347        >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta #sss_result_hyp
     4348        <sss_result_hyp in sss_incl; whd in match (ret_vars ??); #sss_incl
     4349        cases sss_env_hyp *
     4350        #Hlookup_new_in_old
     4351        #Hlookup_new_in_new
     4352        #Hlookup_old
     4353        lapply (Hlookup_new_in_new new ?)
     4354          [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem;
     4355             [ 1: @False_ind
     4356             | 2: * #hdv #hdty #tl #Hind whd in ⊢ (% →  (??%?)); *
     4357                  [ 1: #Heq destruct (Heq)
     4358                       cases (identifier_eq_i_i … hdv) #Hrefl #Heq >Heq -Heq normalize nodelta
     4359                       @refl
     4360                  | 2: #Hmem lapply (Hind Hmem) #Hmem_in_tl
     4361                  cases (identifier_eq ? new hdv) normalize nodelta
     4362                  [ 1: #_ @refl | 2: #_ @Hmem_in_tl ] ] ] ]
     4363       * #res #Hlookup >Hlookup normalize nodelta whd in match (bindIO ??????);
     4364       (* B. Reduce rhs of assign, i.e. the condition. Do this using simulation hypothesis. *)
     4365       >(Hsim_expr … Hexec_eq) >bindIO_Value
     4366       (* C. Execute assign. We must prove that this cannot fail. In order for the proof to proceed, we need
     4367             to set up things so that loading from that fresh location will yield exactly the stored value. *)
     4368       normalize in match store_value_of_type'; normalize nodelta
     4369       @cthulhu               
     4370   | *: @cthulhu ]
     4371 | *: @cthulhu ] qed.
Note: See TracChangeset for help on using the changeset viewer.