Changeset 2441


Ignore:
Timestamp:
Nov 7, 2012, 6:02:50 PM (7 years ago)
Author:
garnier
Message:

Moved general stuff on memories from switchRemoval to MemProperties?, e.g. on loading, storing and free, as an
attempt to reduce the typechecking time of switchRemoval.ma.
Moved some other generic stuff on vectors from SimplifyCasts? to frontend_misc.

Location:
src/Clight
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2428 r2441  
    66include "Clight/casts.ma".
    77include "Clight/CexecSound.ma".
     8
     9include "Clight/frontend_misc.ma".
    810
    911
     
    302304(* Facts about cast_int_int *)
    303305
    304 (* copied from AssemblyProof *)
    305 lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
    306  #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
    307  #n #hd #tl #abs @⊥ destruct (abs)
    308 qed.
    309 
    310 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
    311  ∃hd.∃tl.v ≃ VCons A n hd tl.
    312  #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
    313  [ #abs @⊥ destruct (abs)
    314  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    315 qed.
    316 
    317 lemma vector_append_zero:
    318   ∀A,m.
    319   ∀v: Vector A m.
    320   ∀q: Vector A 0.
    321     v = q@@v.
    322   #A #m #v #q
    323   >(Vector_O A q) %
    324 qed.
    325 
    326 corollary prod_vector_zero_eq_left:
    327   ∀A, n.
    328   ∀q: Vector A O.
    329   ∀r: Vector A n.
    330     〈q, r〉 = 〈[[ ]], r〉.
    331   #A #n #q #r
    332   generalize in match (Vector_O A q …);
    333   #hyp
    334   >hyp in ⊢ (??%?);
    335   %
    336 qed.
    337  
    338 lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
    339 # A #m #n elim m
    340 [ 1: normalize #v
    341   elim (Vector_Sn ?? v) #hd * #tl #Eq
    342   @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
    343   >Eq normalize //
    344 | 2: #n' #Hind #v
    345   elim (Vector_Sn ?? v) #hd * #tl #Eq
    346   elim (Hind tl)
    347   #tl1 * #tl2 #Eq_tl
    348   @(ex_intro … (hd ::: tl1))
    349   @(ex_intro … tl2) 
    350   destruct normalize //
    351 ] qed.
    352 
    353 lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
    354 # A #m #n elim m
    355 [ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
    356 | 2: #n' #Hind #v
    357   elim (Vector_Sn ?? v) #hd * #tl #Eq
    358   elim (Hind tl)
    359   #tl1 * #tl2 #Eq_tl
    360   @(ex_intro … (hd ::: tl1))
    361   @(ex_intro … tl2) 
    362   destruct normalize //
    363 ] qed.
    364 
    365 lemma vsplit_zero:
    366   ∀A,m.
    367   ∀v: Vector A m.
    368     〈[[]], v〉 = vsplit A 0 m v.
    369   #A #m #v
    370   elim v
    371   [ %
    372   | #n #hd #tl #ih
    373     normalize in ⊢ (???%); %
    374   ]
    375 qed.
    376 
    377 
    378 lemma vsplit_zero2:
    379   ∀A,m.
    380   ∀v: Vector A m.
    381     〈[[]], v〉 = vsplit' A 0 m v.
    382   #A #m #v
    383   elim v
    384   [ %
    385   | #n #hd #tl #ih
    386     normalize in ⊢ (???%); %
    387   ]
    388 qed.
    389 
    390 (* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
    391  * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
    392 axiom vsplit_succ:
    393   ∀A, m, n.
    394   ∀l: Vector A m.
    395   ∀r: Vector A n.
    396   ∀v: Vector A (m + n).
    397   ∀hd.
    398     v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
    399 
    400 axiom vsplit_succ2:
    401   ∀A, m, n.
    402   ∀l: Vector A m.
    403   ∀r: Vector A n.
    404   ∀v: Vector A (m + n).
    405   ∀hd.
    406     v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
    407      
    408 lemma vsplit_prod2:
    409   ∀A,m,n.
    410   ∀p: Vector A (m + n).
    411   ∀v: Vector A m.
    412   ∀q: Vector A n.
    413     p = v@@q → 〈v, q〉 = vsplit' A m n p.
    414   #A #m
    415   elim m
    416   [ #n #p #v #q #hyp
    417     >hyp <(vector_append_zero A n q v)
    418     >(prod_vector_zero_eq_left A …)
    419     @vsplit_zero2
    420   | #r #ih #n #p #v #q #hyp
    421     >hyp
    422     cases (Vector_Sn A r v)
    423     #hd #exists
    424     cases exists
    425     #tl #jmeq >jmeq
    426     @vsplit_succ2 [1: % |2: @ih % ]
    427   ]
    428 qed.
    429 
    430 lemma vsplit_prod:
    431   ∀A,m,n.
    432   ∀p: Vector A (m + n).
    433   ∀v: Vector A m.
    434   ∀q: Vector A n.
    435     p = v@@q → 〈v, q〉 = vsplit A m n p.
    436   #A #m
    437   elim m
    438   [ #n #p #v #q #hyp
    439     >hyp <(vector_append_zero A n q v)
    440     >(prod_vector_zero_eq_left A …)
    441     @vsplit_zero
    442   | #r #ih #n #p #v #q #hyp
    443     >hyp
    444     cases (Vector_Sn A r v)
    445     #hd #exists
    446     cases exists
    447     #tl #jmeq >jmeq
    448     @vsplit_succ [1: % |2: @ih % ]
    449   ]
    450 qed.
    451306
    452307lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)).
     
    746601
    747602lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
    748 * * normalize #H @conj // qed.
     603* * normalize #H @conj try @refl assumption qed.
    749604
    750605(* Operations where it is safe to use a smaller integer type on the assumption
  • src/Clight/frontend_misc.ma

    r2438 r2441  
    7575 match e with
    7676 [ None ⇒ None ?
    77  | Some x ⇒ f x ] = Some ? res → 
     77 | Some x ⇒ f x ] = Some ? res →
    7878 ∃x. e = Some ? x ∧ f x = Some ? res.
    7979 #A #B #e #res #f cases e normalize nodelta
    8080[ 1: #Habsurd destruct (Habsurd)
    81 | 2: #a #Heq %{a} @conj >Heq @refl ] 
     81| 2: #a #Heq %{a} @conj >Heq @refl ]
    8282qed.
    8383
     
    330330lemma mem_append_backwards : ∀A:Type[0]. ∀elt : A. ∀l1,l2. (mem … elt l1) ∨ (mem … elt l2) → mem … elt (l1 @ l2) .
    331331#A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #_ #H' @H' @H qed.
     332
     333(* "Observational" equivalence on list implies concrete equivalence. Useful to
     334 * prove equality from some reasoning on indexings. Needs a particular induction
     335 * principle. *)
     336 
     337let rec double_list_ind
     338  (A : Type[0])
     339  (P : list A → list A → Prop)
     340  (base_nil  : P [ ] [ ])
     341  (base_l1   : ∀hd1,l1. P (hd1::l1) [ ])
     342  (base_l2   : ∀hd2,l2. P [ ] (hd2::l2))
     343  (ind  : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2))
     344  (l1, l2 : list A) on l1 ≝
     345match l1 with
     346[ nil ⇒
     347  match l2 with
     348  [ nil ⇒ base_nil
     349  | cons hd2 tl2 ⇒ base_l2 hd2 tl2 ]
     350| cons hd1 tl1 ⇒ 
     351  match l2 with
     352  [ nil ⇒ base_l1 hd1 tl1
     353  | cons hd2 tl2 ⇒
     354    ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2)
     355  ]
     356]. 
     357
     358lemma nth_eq_tl :
     359  ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2.
     360  (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) →
     361  (∀i. nth_opt A i l1 = nth_opt A i l2).
     362#A #l1 #l2 @(double_list_ind … l1 l2)
     363[ 1: #hd1 #hd2 #_ #i elim i try /2/
     364| 2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
     365| 3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
     366| 4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2
     367     #Hind
     368     @(λi. Hind (S i))
     369] qed.     
     370
     371
     372lemma nth_eq_to_eq :
     373  ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2.
     374#A #l1 elim l1
     375[ 1: #l2 #H lapply (H 0) normalize
     376     cases l2
     377     [ 1: //
     378     | 2: #hd2 #tl2 normalize #Habsurd destruct ]
     379| 2: #hd1 #tl1 #Hind *
     380     [ 1: #H lapply (H 0) normalize #Habsurd destruct
     381     | 2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq)
     382          >(Hind tl2) try @refl @(nth_eq_tl … H)
     383     ]
     384] qed.
     385
     386(* --------------------------------------------------------------------------- *)
     387(* General results on vectors. *)
     388(* --------------------------------------------------------------------------- *)
     389
     390(* copied from AssemblyProof, TODO get rid of the redundant stuff. *)
     391lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
     392 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
     393 #n #hd #tl #abs @⊥ destruct (abs)
     394qed.
     395
     396lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
     397 ∃hd.∃tl.v ≃ VCons A n hd tl.
     398 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
     399 [ #abs @⊥ destruct (abs)
     400 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     401qed.
     402
     403lemma vector_append_zero:
     404  ∀A,m.
     405  ∀v: Vector A m.
     406  ∀q: Vector A 0.
     407    v = q@@v.
     408  #A #m #v #q
     409  >(Vector_O A q) %
     410qed.
     411
     412corollary prod_vector_zero_eq_left:
     413  ∀A, n.
     414  ∀q: Vector A O.
     415  ∀r: Vector A n.
     416    〈q, r〉 = 〈[[ ]], r〉.
     417  #A #n #q #r
     418  generalize in match (Vector_O A q …);
     419  #hyp
     420  >hyp in ⊢ (??%?);
     421  %
     422qed.
     423 
     424lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
     425# A #m #n elim m
     426[ 1: normalize #v
     427  elim (Vector_Sn ?? v) #hd * #tl #Eq
     428  @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
     429  >Eq normalize //
     430| 2: #n' #Hind #v
     431  elim (Vector_Sn ?? v) #hd * #tl #Eq
     432  elim (Hind tl)
     433  #tl1 * #tl2 #Eq_tl
     434  @(ex_intro … (hd ::: tl1))
     435  @(ex_intro … tl2) 
     436  destruct normalize //
     437] qed.
     438
     439lemma vsplit_zero:
     440  ∀A,m.
     441  ∀v: Vector A m.
     442    〈[[]], v〉 = vsplit A 0 m v.
     443  #A #m #v
     444  elim v
     445  [ %
     446  | #n #hd #tl #ih
     447    normalize in ⊢ (???%); %
     448  ]
     449qed.
     450
     451lemma vsplit_zero2:
     452  ∀A,m.
     453  ∀v: Vector A m.
     454    〈[[]], v〉 = vsplit' A 0 m v.
     455  #A #m #v
     456  elim v
     457  [ %
     458  | #n #hd #tl #ih
     459    normalize in ⊢ (???%); %
     460  ]
     461qed.
     462
     463lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
     464# A #m #n elim m
     465[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
     466| 2: #n' #Hind #v
     467  elim (Vector_Sn ?? v) #hd * #tl #Eq
     468  elim (Hind tl)
     469  #tl1 * #tl2 #Eq_tl
     470  @(ex_intro … (hd ::: tl1))
     471  @(ex_intro … tl2) 
     472  destruct normalize //
     473] qed.
     474
     475(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
     476 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
     477axiom vsplit_succ:
     478  ∀A, m, n.
     479  ∀l: Vector A m.
     480  ∀r: Vector A n.
     481  ∀v: Vector A (m + n).
     482  ∀hd.
     483    v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
     484
     485axiom vsplit_succ2:
     486  ∀A, m, n.
     487  ∀l: Vector A m.
     488  ∀r: Vector A n.
     489  ∀v: Vector A (m + n).
     490  ∀hd.
     491    v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
     492     
     493lemma vsplit_prod2:
     494  ∀A,m,n.
     495  ∀p: Vector A (m + n).
     496  ∀v: Vector A m.
     497  ∀q: Vector A n.
     498    p = v@@q → 〈v, q〉 = vsplit' A m n p.
     499  #A #m
     500  elim m
     501  [ #n #p #v #q #hyp
     502    >hyp <(vector_append_zero A n q v)
     503    >(prod_vector_zero_eq_left A …)
     504    @vsplit_zero2
     505  | #r #ih #n #p #v #q #hyp
     506    >hyp
     507    cases (Vector_Sn A r v)
     508    #hd #exists
     509    cases exists
     510    #tl #jmeq >jmeq
     511    @vsplit_succ2 [1: % |2: @ih % ]
     512  ]
     513qed.
     514
     515lemma vsplit_prod:
     516  ∀A,m,n.
     517  ∀p: Vector A (m + n).
     518  ∀v: Vector A m.
     519  ∀q: Vector A n.
     520    p = v@@q → 〈v, q〉 = vsplit A m n p.
     521  #A #m
     522  elim m
     523  [ #n #p #v #q #hyp
     524    >hyp <(vector_append_zero A n q v)
     525    >(prod_vector_zero_eq_left A …)
     526    @vsplit_zero
     527  | #r #ih #n #p #v #q #hyp
     528    >hyp
     529    cases (Vector_Sn A r v)
     530    #hd #exists
     531    cases exists
     532    #tl #jmeq >jmeq
     533    @vsplit_succ [1: % |2: @ih % ]
     534  ]
     535qed.
     536
    332537
    333538(* --------------------------------------------------------------------------- *)
  • src/Clight/switchRemoval.ma

    r2438 r2441  
    77include "Clight/frontend_misc.ma".
    88include "Clight/memoryInjections.ma".
     9include "Clight/MemProperties.ma".
    910include "basics/lists/list.ma".
    1011include "basics/lists/listb.ma".
    11 include "Clight/SimplifyCasts.ma".
     12
    1213
    1314
     
    778779].
    779780
    780 (* --------------------------------------------------------------------------- *)
    781 (* "Observational" memory equivalence. Memories use closures to represent contents,
    782    so we have to use that short of asserting functional extensionality to reason
    783    on reordering of operations on memories, among others. For our
    784    limited purposes, we do not need (at this time of writing, i.e. 22 sept. 2012)
    785    to push the observation in the content_map. *)
    786 (* --------------------------------------------------------------------------- *) 
    787 definition memory_eq ≝ λm1,m2.
    788   nextblock m1 = nextblock m2 ∧
    789   ∀b. blocks m1 b = blocks m2 b.
    790  
    791 (* memory_eq is an equivalence relation. *)
    792 lemma reflexive_memory_eq : reflexive ? memory_eq.
    793 whd * #contents #nextblock #Hpos normalize @conj try //
    794 qed.
    795 
    796 lemma symmetric_memory_eq : symmetric ? memory_eq.
    797 whd * #contents #nextblock #Hpos * #contents' #nextblock' #Hpos'
    798 normalize * #H1 #H2 @conj >H1 try //
    799 qed.
    800 
    801 lemma transitive_memory_eq : transitive ? memory_eq.
    802 whd
    803 * #contents #nextblock #Hpos
    804 * #contents1 #nextblock1 #Hpos1
    805 * #contents2 #nextblock2 #Hpos2
    806 normalize * #H1 #H2 * #H3 #H4 @conj //
    807 qed.
     781
    808782
    809783(* --------------------------------------------------------------------------- *)
     
    811785   properties at the back-end level. *)
    812786(* --------------------------------------------------------------------------- *) 
    813 
    814 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the back-end values are equal. *)
    815 definition load_sim ≝
    816 λ(m1 : mem).λ(m2 : mem).
    817  ∀ptr,bev.
    818   beloadv m1 ptr = Some ? bev →
    819   beloadv m2 ptr = Some ? bev.
    820 
    821 definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.
    822 
    823 lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p.
    824 #m #p @conj
    825 [ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??);
    826      whd in match (do_if_in_bounds); normalize nodelta
    827      cases (Zltb (block_id (pblock p)) (nextblock m))
    828      [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
    829      >andb_lsimpl_true normalize nodelta
    830      cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
    831      [ 2: normalize nodelta #Habsurd destruct (Habsurd) ]
    832      >andb_lsimpl_true normalize nodelta
    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 
    850 lemma 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
    857 lapply (Zleb_true_to_Zle (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
    858 lapply (Zltb_true_to_Zlt (block_id (pblock p)) (nextblock m))
    859 cases (Zltb (block_id (pblock p)) (nextblock m)) in H;
    860 [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
    861 cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
    862 normalize nodelta
    863 [ 2: #Habsurd destruct ]
    864 #Hlt1 #Hlt2 #Hle @conj try @conj
    865 try @(Hlt2 (refl ??)) try @(Hle (refl ??)) @(Zltb_true_to_Zlt … Hlt1)
    866 qed.
    867787
    868788(* A writeable_block is a block that is:
     
    12841204
    12851205(* --------------------------------------------------------------------------- *)
    1286 (* Lift beloadv simulation to the front-end. *)       
    1287 
    1288 (* Lift load_sim to loadn. *)
    1289 lemma load_sim_loadn :
    1290  ∀m1,m2. load_sim m1 m2 →
    1291  ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res.
    1292 #m1 #m2 #Hload_sim #sz
    1293 elim sz
    1294 [ 1: #p #res #H @H
    1295 | 2: #n' #Hind #p #res
    1296      whd in match (loadn ???);
    1297      whd in match (loadn m2 ??);
    1298      lapply (Hload_sim p)
    1299      cases (beloadv m1 p) normalize nodelta
    1300      [ 1: #_ #Habsurd destruct (Habsurd) ]
    1301      #bval #H >(H ? (refl ??)) normalize nodelta
    1302      lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1)))
    1303      cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n')
    1304      normalize nodelta
    1305      [ 1: #_ #Habsurd destruct (Habsurd) ]
    1306      #res' #H >(H ? (refl ??)) normalize
    1307      #H @H
    1308 ] qed.
    1309  
    1310 (* Lift load_sim to front-end values. *)
    1311 lemma load_sim_fe :
    1312   ∀m1,m2. load_sim m1 m2 →
    1313   ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v →
    1314             load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v.
    1315 #m1 #m2 #Hloadsim #ptr #ty #v
    1316 cases ty
    1317 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty
    1318 | 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ]
    1319 whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));
    1320 [ 1,7,8: #Habsurd destruct (Habsurd)
    1321 | 5,6: #H @H
    1322 | 2,3,4,9:
    1323   generalize in match (mk_pointer (pblock ptr) (poff ptr));
    1324   elim (typesize ?)
    1325   [ 1,3,5,7: #p #H @H
    1326   | 2,4,6,8: #n' #Hind #p
    1327       lapply (load_sim_loadn … Hloadsim (S n') p)
    1328       cases (loadn m1 p (S n')) normalize nodelta
    1329       [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ]     
    1330       #bv #H >(H ? (refl ??)) #H @H
    1331   ]
    1332 ] qed.
    1333 
    1334 (* --------------------------------------------------------------------------- *)
    1335 (* Lemmas relating reading and writing operation to memory properties. *)
    1336 
    1337 (* Successful beloadv implies valid_pointer. The converse is *NOT* true. *)
    1338 lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true.
    1339 * #contents #next #nextpos #ptr #res
    1340 whd in match (beloadv ??);
    1341 whd in match (valid_pointer ??);
    1342 cases (Zltb (block_id (pblock ptr)) next)
    1343 normalize nodelta
    1344 [ 2: #Habsurd destruct (Habsurd) ]
    1345 >andb_lsimpl_true
    1346 whd in match (low_bound ??);
    1347 whd in match (high_bound ??);
    1348 cases (Zleb (low (contents (pblock ptr)))
    1349         (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
    1350 [ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
    1351 >andb_lsimpl_true
    1352 normalize nodelta #H
    1353 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
    1354 try // normalize #Habsurd destruct (Habsurd)
    1355 qed.
    1356 
    1357 lemma 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
    1359 whd in match (bestorev ???);
    1360 whd in match (valid_pointer ??);
    1361 cases (Zltb (block_id (pblock ptr)) next)
    1362 normalize nodelta
    1363 [ 2: #Habsurd destruct (Habsurd) ]
    1364 >andb_lsimpl_true
    1365 whd in match (low_bound ??);
    1366 whd in match (high_bound ??);
    1367 cases (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
    1371 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr))))
    1372 normalize nodelta try // #Habsurd destruct (Habsurd)
    1373 qed.
    1374 
    1375 (* --------------------------------------------------------------------------- *)
    13761206(* Lemmas relating memory extensions to [free] *)
    1377 
    1378 lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
    1379 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
    1380 @(eqZb_elim … bid1 bid2)
    1381 [ 1: #Heq >Heq cases br1 cases br2 normalize
    1382      [ 1,4: * #H @(False_ind … (H (refl ??))) ]
    1383      #_ @refl
    1384 | 2: cases br1 cases br2 normalize #_ #_ @refl ]
    1385 qed.
    1386 
    1387 lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
    1388 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
    1389 @(eqZb_elim … bid1 bid2)
    1390 [ 1: #Heq >Heq cases br1 cases br2 normalize
    1391      [ 1,4: * #H @(False_ind … (H (refl ??))) ]
    1392      #_ @refl
    1393 | 2: cases br1 cases br2 normalize #_ #_ @refl ]
    1394 qed.
    1395 
    1396 lemma beloadv_free_blocks_neq :
    1397   ∀m,block,pblock,poff,res.
    1398   beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.
    1399 * #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res
    1400 normalize
    1401 cases (Zltb pbid next) normalize nodelta
    1402 [ 2: #Habsurd destruct (Habsurd) ]
    1403 cases pbr cases br normalize nodelta
    1404 [ 2,3: #_ % #Habsurd destruct (Habsurd) ]
    1405 @(eqZb_elim pbid bid) normalize nodelta
    1406 #Heq destruct (Heq)
    1407 [ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
    1408 #_ % #H destruct (H) elim Heq #H @H @refl
    1409 qed.
    1410 
    1411 lemma beloadv_free_beloadv :
    1412   ∀m,block,ptr,res.
    1413     beloadv (free m block) ptr = Some ? res →
    1414     beloadv m ptr = Some ? res.
    1415 * #contents #next #nextpos #block * #pblock #poff #res
    1416 #H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq
    1417 lapply H
    1418 whd in match (beloadv ??);
    1419 whd in match (beloadv ??) in ⊢ (? → %);
    1420 whd in match (nextblock (free ??));
    1421 cases (Zltb (block_id pblock) next)
    1422 [ 2: normalize #Habsurd destruct (Habsurd) ]
    1423 normalize nodelta
    1424 <(low_free_eq … Hblocks_neq)
    1425 <(high_free_eq … Hblocks_neq)
    1426 whd in match (free ??);
    1427 whd in match (update_block ?????);
    1428 @(eq_block_elim … pblock block)
    1429 [ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ]
    1430 #_ normalize nodelta
    1431 #H @H
    1432 qed.
    1433 
    1434 lemma beloadv_free_beloadv2 :
    1435   ∀m,block,ptr,res.
    1436   pblock ptr ≠ block →
    1437   beloadv m ptr = Some ? res →
    1438   beloadv (free m block) ptr = Some ? res.
    1439 * #contents #next #nextpos #block * #pblock #poff #res #Hneq
    1440 whd in match (beloadv ??);
    1441 whd in match (beloadv ??) in ⊢ (? → %);
    1442 whd in match (nextblock (free ??));
    1443 cases (Zltb (block_id pblock) next)
    1444 [ 2: normalize #Habsurd destruct (Habsurd) ]
    1445 normalize nodelta
    1446 <(low_free_eq … Hneq)
    1447 <(high_free_eq … Hneq)
    1448 whd in match (free ??);
    1449 whd in match (update_block ?????);
    1450 @(eq_block_elim … pblock block)
    1451 [ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ]
    1452 #_ normalize nodelta
    1453 #H @H
    1454 qed.
    14551207
    14561208lemma beloadv_free_simulation :
     
    14691221qed.
    14701222
    1471 (* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *)
    1472 lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.
    1473 #m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);
    1474 #H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);
    1475 elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))
    1476 [ 1: #Hlt >Hlt normalize nodelta
    1477      @(eq_block_elim … b (pblock p))
    1478      [ 1: #Heq >Heq whd in match (free ??);
    1479           whd in match (update_block ?????); >eq_block_b_b
    1480           normalize nodelta normalize in match (low ?);
    1481           >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta
    1482           #Habsurd destruct (Habsurd)
    1483      | 2: #Hblock_neq whd in match (free ? ?);
    1484           whd in match (update_block ?????);
    1485           >(not_eq_block_rev … Hblock_neq) normalize nodelta
    1486           cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
    1487           [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
    1488           >andb_lsimpl_true
    1489           lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p)))
    1490                                      (high (blocks m (pblock p))))
    1491           cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
    1492           [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    1493           normalize nodelta #H #_ /2 by ex_intro/
    1494      ]
    1495 | 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ]
    1496 qed.
    1497 
    1498 (* Cf [in_bounds_free_to_in_bounds] *)
    1499 lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.
    1500 #m #b #p #Hvalid
    1501 cases (valid_pointer_def … m p) #HA #HB
    1502 cases (valid_pointer_def … (free m b) p) #HC #HD
    1503 @HB @(in_bounds_free_to_in_bounds … b)
    1504 @HC @Hvalid
    1505 qed.
    1506 
    1507 (* Making explicit the argument above. *)
    1508 lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.
    1509 #m #b #p
    1510 whd in match (valid_pointer ??);
    1511 whd in match (free ??);
    1512 whd in match (update_block ????);
    1513 whd in match (low_bound ??);
    1514 whd in match (high_bound ??);
    1515 @(eq_block_elim … b (pblock p))
    1516 [ 1: #Heq <Heq >eq_block_b_b normalize nodelta
    1517      whd in match (low ?); whd in match (high ?);
    1518      cases (Zltb ? (nextblock m))
    1519      [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
    1520      >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd)
    1521 | 2: #Hneq #_ @Hneq ]
    1522 qed.
    15231223
    15241224(* Lifting the property of being valid after a free to memory extensions *)
     
    24642164 (* current function after translation *)
    24652165 ∀sss_func_tr    : function.
    2466  (* variables generated during conversion of the function *) 
     2166 (* variables generated during conversion of the function *)
    24672167 ∀sss_new_vars   : list (ident × type).
    2468  (* statement of the transformation *) 
     2168 (* statement of the transformation *)
    24692169 ∀sss_func_hyp   : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func.
    24702170 (* memory state before conversion *)
     
    24862186 (* The extended environment does not interfer with the old one. *)
    24872187 ∀sss_env_hyp    : disjoint_extension sss_env sss_env_ext sss_new_vars.
     2188 (* The new variables are allocated to a size corresponding to their types. *)
     2189 ∀sss_new_alloc  :
     2190    ∀v.meml ? v sss_new_vars →
     2191      ∀vb. lookup … sss_env_ext (\fst v) = Some ? vb →
     2192           low (blocks sss_m_ext vb) = OZ ∧
     2193           high (blocks sss_m_ext vb) = sizeof (\snd v).
    24882194 (* Extension blocks are writeable. *)
    24892195 ∀sss_ext_write  : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable.
     
    31352841   to go back and forth nats, Zs and bitvectors ... *)
    31362842
    3137 lemma 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 
    3163 lemma 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 
    3184 lemma 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 
    3210 lemma 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'
    3213 lapply bv2 lapply bv1 -bv1 -bv2
    3214 elim 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 
    3230 definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs).
     2843       
     2844
    32312845
    32322846(* This axiom looks reasonable to me. But I slept 3 hours last night. *)
     
    32522866* #vec *)
    32532867
    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 *)
    3261 lemma 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
    3274 cases (if_opt_inversion ???? H) #Hlt -H normalize nodelta #H
    3275 cases (if_opt_inversion ???? H) #Hlelt -H #H
    3276 cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj
    3277 destruct 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. *)
    3297 let rec shiftn (off:offset) (i:nat) on i : offset ≝
    3298 match 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. *)
    3306 axiom 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 *)
    3330 lemma 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 
    3392 lemma 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
    3398 lapply (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
    3401 whd in match (beloadv ??); whd in match (nth_opt ???);
    3402 lapply (Hvalid_ptr ?) try //
    3403 whd 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
    3407 whd in match (low_bound ??); whd in match (high_bound ??);
    3408 cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H
    3409 lapply (Hvalid_offs i Hle) * #Hzle #Hzlt
    3410 >(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl
    3411 qed.
    3412 
    3413 lemma 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 
    3441 lemma 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
    3449 lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
    3450 #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
    3451 cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0
    3452 whd in match (loadn ???);
    3453 lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
    3454 whd in match (beloadv ??);
    3455 whd in match (low_bound ??); whd in match (high_bound ??);
    3456 >Hnext
    3457 cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
    3458 normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh
    3459 cases (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
    3462 cases (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
    3465 normalize >Htl' @refl
    3466 qed.
    3467 
    3468 let 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 ≝
    3476 match 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 
    3489 lemma 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 
    3503 lemma 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 *)
    3518 definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop.
    3519 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim.
    3520 
    3521 include alias "arithmetics/nat.ma".
    3522 
    3523 lemma 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 
    3530 lemma 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
    3537 lapply (storen_beloadv_ok m m' …  Hle Hstoren) #Hyp_storen
    3538 cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz
    3539 lapply (loadn_beloadv_ok (|hd::tl|) m' b ofs … Hloadn) #Hyp_loadn
    3540 cut (∀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
    3544 cut (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. *)
    3557 lemma typesize_bounded : ∀ty. typesize ty ≤ 8.
    3558 * try //
    3559 [ 1: * try //
    3560 | 2: * try //
    3561 ] qed.
    3562 
    3563 (* Lifting bound on make_list *)
    3564 lemma 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
    3567 cases 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 
    3574 lemma 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 
    3587 lemma map_bounded :
    3588   ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|.
    3589   #A #B #l elim l try //
    3590 qed.
    3591 
    3592 lemma 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 
    3622 definition 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 
    3639 definition type_consistent_with_value : type → val → Prop ≝ λty,v.
    3640 match 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. *)
    3647 lemma 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. *)
    3675 lemma 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
    3679 whd in match (fe_to_be_values ??);
    3680 cases 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.  *)
    3721 lemma 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
    3727 whd in ⊢ ((??%?) → (??%?)); #Hstoren
    3728 lapply (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 //
    3731 qed.
    3732 
    3733 (* For the arguments exposed before, we restrict the lemma to ints.
    3734  *)
    3735 lemma 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 ⊢ (% → ?);
    3741 cases 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. *)
    3745 whd in match (store_value_of_type ?????); #Hstoren
    3746 lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren)
    3747 whd 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 //
    3750 qed.
    3751 
     2868
     2869(*
     2870lemma valid_pointer_to_storen_ok :
     2871  ∀data,m,p. valid_pointer m p → ∃m'. storen m p data = Some ? m'.
     2872#data elim data try /2 by ex_intro/
     2873#hd #tl #Hind
     2874#m #p #Hvalid_ptr whd in match (storen ???);
     2875cases (valid_pointer_to_bestorev_ok … hd … Hvalid_ptr) #m' #Hbestorev >Hbestorev
     2876normalize nodelta
     2877lapply (Hind m' (shift_pointer 2 p (bitvector_of_nat 2 1)))
     2878#m #p #data *)
     2879
     2880
     2881(*
    37522882lemma load_int_value_inversion :
    37532883  ∀t,m,p,sz,i. load_value_of_type' t m p = Some ? (Vint sz i) → ∃sg. t = Tint sz sg.
     
    38022932[ 2: #err #f #res normalize nodelta #Habsurd destruct
    38032933| 1: #a #f #res normalize nodelta #Heq destruct %{a} @conj try @refl >Heq @refl
    3804 ] qed.
     2934] qed. *)
     2935
     2936(*
     2937lemma valid_pointer_store_succeeds :
     2938  ∀sz,sg,m,p,i.
     2939  valid_pointer m p →
     2940  ∃m'. store_value_of_type (Tint sz sg) m (pblock p) (poff p) (Vint sz i) = Some ? m'.
     2941#sz #sg #m * #b #o #i #Hvalid
     2942whd in match (store_value_of_type' ????);
     2943whd in match (store_value_of_type ?????);
     2944whd in match (storen ???);
     2945*)
     2946
    38052947
    38062948(* In order to prove the consistency of types wrt values, we need the following lemma. *)
     
    39013043  #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars
    39023044  #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp
    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
     3045  #sss_env_hyp #sss_new_alloc #sss_writeable_hyp #sss_result_rec #sss_result_hyp #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge
    39043046  #Hs1_eq #Hs1_eq'
    39053047  elim (sim_related_globals … ge ge'
     
    39733115         #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step)
    39743116         @conj try @refl
    3975          %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try //
     3117         %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // try assumption
    39763118         #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
    39773119    | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
     
    39923134         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
    39933135         %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)}
    3994          try //
     3136         try // try assumption
    39953137         [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize
    39963138              cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize
     
    40293171       * #m_ext' * #Hstore_eq #Hnew_ext >Hstore_eq whd in match (m_bind ?????);
    40303172       whd destruct @conj try @refl
    4031        %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip  sss_lu) } try // try assumption
     3173       %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip  sss_lu) }
     3174       try // try assumption
    40323175       [ 1: @(fresh_for_Sskip … sss_lu_fresh)
    4033        | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     3176       | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
     3177       | 2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * #Hlow #Hhigh
     3178            lapply (me_nonempty … Hnew_ext)
     3179           
     3180              @cthulhu
     3181       ]
    40343182  | 3: (* Call statement *)
    40353183       #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp)
     
    40803228       cases (switch_removal_elim stm1 sss_lu) #stm1' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
    40813229       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 //
     3230       normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA}
     3231       try // try assumption
    40833232       [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * //
    40843233       | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
     
    43273476        #Hexec whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec
    43283477        >sss_result_proj <sss_result_hyp normalize nodelta #Hexec
    4329         cases (bindIO_inversion ??????? Hexec) * #condval #condtrace
     3478        cases (bindIO_inversion ??????? Hexec) * #condval #condtrace -Hexec
    43303479        cases condval normalize nodelta
    43313480        [ 1: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     
    43333482        | 4: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
    43343483        | 5: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
    4335         #sz #i * #Hexec_eq #Heq whd in Heq:(??%%); destruct (Heq)
    4336 
     3484        #sz #i * #Hexec_eq #Heq
     3485        cut (∃sg. typeof cond = Tint sz sg) whd in Heq:(??%%); destruct (Heq)
     3486        [ 1: cases (typeof cond) in Heq; normalize nodelta
     3487             [ 1: | 2: #sz' #sg' | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty
     3488             | 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ]
     3489             [ 2: cases (sz_eq_dec ??) normalize nodelta #H
     3490                  [ 2: #Habsurd destruct
     3491                  | 1: destruct (H) #_ %{sg'} try @refl ]
     3492             | *: #Habsurd destruct (Habsurd) ] ]
     3493        * #sg #Htypeof_cond >Htypeof_cond in Heq; normalize nodelta >sz_eq_identity normalize nodelta
     3494        #Heq whd in Heq:(??%%);
     3495        cases (bindIO_inversion ??????? Heq) #switchcases_truncated * #Heq1 #Heq2 -Heq
     3496        whd in Heq1:(??%%); whd in Heq2:(??%%);
     3497        cut (select_switch sz i switchcases = Some ? switchcases_truncated)
     3498        [ 1: cases (select_switch sz i switchcases) in Heq1; normalize nodelta
     3499             [ 1: #Habsurd destruct | 2: #ls #Heq destruct (Heq) @refl ] ]
     3500        -Heq1 #Heq_select_switch destruct (Heq2)
    43373501        cases (switch_removal_branches_elim … switchcases sss_lu) #switchcases' * #fvs' * #u' #Hbranch_eq
    43383502        >Hbranch_eq normalize nodelta
    43393503        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'''
     3504        cases (simplify_switch_elim (Expr (Evar new) (Tint sz sg)) switchcases' u'') #simplified * #u'''
    43413505        #Hswitch_eq >Hswitch_eq normalize nodelta
    4342         %{1} whd whd in ⊢ (??%?); 
     3506        %{1} whd whd in ⊢ (??%?);
    43433507        (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *)
    43443508        whd in match (exec_lvalue ????);
    43453509        (* 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
     3510        >Hbranch_eq in sss_result_hyp; normalize nodelta
     3511        >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta >Htypeof_cond >Hswitch_eq
     3512        normalize nodelta #sss_result_hyp
    43483513        <sss_result_hyp in sss_incl; whd in match (ret_vars ??); #sss_incl
    43493514        cases sss_env_hyp *
     
    43523517        #Hlookup_old
    43533518        lapply (Hlookup_new_in_new new ?)
    4354           [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem;
     3519        [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem;
    43553520             [ 1: @False_ind
    43563521             | 2: * #hdv #hdty #tl #Hind whd in ⊢ (% →  (??%?)); *
     
    43673532             to set up things so that loading from that fresh location will yield exactly the stored value. *)
    43683533       normalize in match store_value_of_type'; normalize nodelta
     3534       whd in match (typeof ?);
     3535       
    43693536       @cthulhu               
    43703537   | *: @cthulhu ]
Note: See TracChangeset for help on using the changeset viewer.