(* This file is dedicated to general properties of memory w.r.t. writing and reading to it.
   It also contains facts about related functions and predicates, such as valid_pointer. *)
   
include "Clight/frontend_misc.ma".
include "common/FrontEndMem.ma".

(* for store_value_of_type' *)
include "Clight/Cexec.ma".


(* --------------------------------------------------------------------------- *)
(* Stuff on [valid_pointer m p].                                               *)
(* --------------------------------------------------------------------------- *)

(* [do_if_in_bounds] is used to check consistency when reading and storing stuff. *)
definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.

lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p.
#m #p @conj
[ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??);
     whd in match (do_if_in_bounds); normalize nodelta
     cases (Zltb (block_id (pblock p)) (nextblock m))
     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
     >andb_lsimpl_true normalize nodelta
     cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
     [ 2: normalize nodelta #Habsurd destruct (Habsurd) ]
     >andb_lsimpl_true normalize nodelta
     #Hlt >Hlt normalize nodelta #A #f /2 by ex_intro/
| 2: whd in match (valid_pointer ??);
     whd in match (in_bounds_pointer ??); #H
     lapply (H bool (λblock,contents,off. true))
     * #foo whd in match (do_if_in_bounds ????);
     cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta
     [ 2: #Habsurd destruct (Habsurd) ]
     >andb_lsimpl_true 
     cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
     normalize nodelta
     [ 2: #Habsurd destruct (Habsurd) ]
     >andb_lsimpl_true
     elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))     
     [ 1: #H >H //
     | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]
] qed.

lemma valid_pointer_to_Prop : 
  ∀m,p. valid_pointer m p = true →
        (block_id (pblock p)) < (nextblock m) ∧
        (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧
        (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)).
#m #p whd in match (valid_pointer ??);        
#H 
lapply (Zleb_true_to_Zle (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
lapply (Zltb_true_to_Zlt (block_id (pblock p)) (nextblock m)) 
cases (Zltb (block_id (pblock p)) (nextblock m)) in H;
[ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
normalize nodelta
[ 2: #Habsurd destruct ]
#Hlt1 #Hlt2 #Hle @conj try @conj
try @(Hlt2 (refl ??)) try @(Hle (refl ??)) @(Zltb_true_to_Zlt … Hlt1)
qed.

lemma valid_pointer_of_Prop : 
  ∀m,p. (block_id (pblock p)) < (nextblock m) ∧
        (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧
        (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)) →
        valid_pointer m p = true.
#m #p * * #Hnextblock #Hlowbound #Hhighbound whd in match (valid_pointer ??);
>(Zle_to_Zleb_true … Hlowbound)
>(Zlt_to_Zltb_true … Hhighbound)
>(Zlt_to_Zltb_true … Hnextblock) @refl
qed.

(* --------------------------------------------------------------------------- *)
(* "Observational" memory equivalence. Memories use closures to represent contents,
   so we have to use that short of asserting functional extensionality to reason
   on reordering of operations on memories, among others. For our
   limited purposes, we do not need (at this time of writing, i.e. 22 sept. 2012)
   to push the observation in the content_map. *)
(* --------------------------------------------------------------------------- *)  
definition memory_eq ≝ λm1,m2.
  nextblock m1 = nextblock m2 ∧
  ∀b. blocks m1 b = blocks m2 b.
  
(* memory_eq is an equivalence relation. *)
lemma reflexive_memory_eq : reflexive ? memory_eq.
whd * #contents #nextblock #Hpos normalize @conj try //
qed.

lemma symmetric_memory_eq : symmetric ? memory_eq.
whd * #contents #nextblock #Hpos * #contents' #nextblock' #Hpos'
normalize * #H1 #H2 @conj >H1 try //
qed.

lemma transitive_memory_eq : transitive ? memory_eq.
whd 
* #contents #nextblock #Hpos 
* #contents1 #nextblock1 #Hpos1
* #contents2 #nextblock2 #Hpos2
normalize * #H1 #H2 * #H3 #H4 @conj //
qed.

(* --------------------------------------------------------------------------- *)
(* Some definitions and results useful for simulation proofs. *)
(* --------------------------------------------------------------------------- *)

(* [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.
 * This is allright for switch removal but false for Clight to Cminor *)
definition load_sim ≝
λ(m1 : mem).λ(m2 : mem).
 ∀ptr,bev.
  beloadv m1 ptr = Some ? bev → 
  beloadv m2 ptr = Some ? bev.
    
(* --------------------------------------------------------------------------- *)
(* Lift beloadv simulation to the front-end. *)       

(* Lift load_sim to loadn. *)
lemma load_sim_loadn :
 ∀m1,m2. load_sim m1 m2 →
 ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res.
#m1 #m2 #Hload_sim #sz
elim sz
[ 1: #p #res #H @H
| 2: #n' #Hind #p #res
     whd in match (loadn ???);
     whd in match (loadn m2 ??);
     lapply (Hload_sim p)
     cases (beloadv m1 p) normalize nodelta
     [ 1: #_ #Habsurd destruct (Habsurd) ]
     #bval #H >(H ? (refl ??)) normalize nodelta
     lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1)))
     cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n')
     normalize nodelta
     [ 1: #_ #Habsurd destruct (Habsurd) ]
     #res' #H >(H ? (refl ??)) normalize
     #H @H
] qed.
 
(* Lift load_sim to front-end values. *)
lemma load_sim_fe :
  ∀m1,m2. load_sim m1 m2 →
  ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v →
            load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v.
#m1 #m2 #Hloadsim #ptr #ty #v
cases ty
[ 1: | 2: #sz #sg | 3: #ptrty | 4: #arrayty #arraysz | 5: #argsty #retty
| 6: #sid #fields | 7: #uid #fields | 8: #cptr_id ]
whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));
[ 1,6,7: #Habsurd destruct (Habsurd)
| 4,5: #H @H
| 2,3,8: 
  generalize in match (mk_pointer (pblock ptr) (poff ptr));
  elim (typesize ?)
  [ 1,3,5: #p #H @H
  | *: #n' #Hind #p
      lapply (load_sim_loadn … Hloadsim (S n') p)
      cases (loadn m1 p (S n')) normalize nodelta
      [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ]      
      #bv #H >(H ? (refl ??)) #H @H
  ]
] qed.
  
(* --------------------------------------------------------------------------- *)
(* Lemmas relating reading and writing operation to memory properties. *)

(* Successful beloadv implies valid_pointer. The converse is *NOT* true. *)
lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true.
* #contents #next #nextpos #ptr #res
whd in match (beloadv ??);
whd in match (valid_pointer ??);
cases (Zltb (block_id (pblock ptr)) next)
normalize nodelta
[ 2: #Habsurd destruct (Habsurd) ]
>andb_lsimpl_true
whd in match (low_bound ??);
whd in match (high_bound ??); 
cases (Zleb (low (contents (pblock ptr)))
        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
>andb_lsimpl_true
normalize nodelta #H
cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
try // normalize #Habsurd destruct (Habsurd)
qed.

lemma bestorev_to_valid_pointer : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer m ptr = true.
* #contents #next #nextpos #ptr #v #res
whd in match (bestorev ???);
whd in match (valid_pointer ??);
cases (Zltb (block_id (pblock ptr)) next)
normalize nodelta
[ 2: #Habsurd destruct (Habsurd) ]
>andb_lsimpl_true
whd in match (low_bound ??);
whd in match (high_bound ??);
cases (Zleb (low (contents (pblock ptr)))
        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
>andb_lsimpl_true
cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr))))
normalize nodelta try // #Habsurd destruct (Habsurd)
qed.

lemma bestorev_to_valid_pointer_after : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer res ptr = true.
* #contents #next #nextpos #ptr #v #res
whd in match (bestorev ???);
whd in match (valid_pointer ??); #Hvalid
cases (if_opt_inversion ???? Hvalid) #Hnextblock normalize nodelta -Hvalid #Hvalid
cases (if_opt_inversion ???? Hvalid) #Hin_bounds #Heq destruct (Heq) normalize
>Hnextblock normalize nodelta cases (block_region (pblock ptr)) normalize nodelta
>eqZb_z_z normalize nodelta @Hin_bounds
qed.

(* valid pointer implies successful bestorev *)
lemma valid_pointer_to_bestorev_ok : ∀m,ptr,v. valid_pointer m ptr = true → ∃m'. bestorev m ptr v = Some ? m'.
#m * #b #o #v #Hvalid cases (valid_pointer_to_Prop … Hvalid) *
#Hnext #Hlow #Hhigh normalize
>(Zlt_to_Zltb_true … Hnext) normalize nodelta
>(Zle_to_Zleb_true … Hlow) normalize nodelta
>(Zlt_to_Zltb_true … Hhigh) normalize nodelta
/2 by ex_intro/
qed.

(* --------------------------------------------------------------------------- *)
(* Some facts on [free] *)

lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
@(eqZb_elim … bid1 bid2)
[ 1: #Heq >Heq cases br1 cases br2 normalize 
     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
     #_ @refl
| 2: cases br1 cases br2 normalize #_ #_ @refl ]
qed.

lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
@(eqZb_elim … bid1 bid2)
[ 1: #Heq >Heq cases br1 cases br2 normalize 
     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
     #_ @refl
| 2: cases br1 cases br2 normalize #_ #_ @refl ]
qed.

lemma beloadv_free_blocks_neq :
  ∀m,block,pblock,poff,res.
  beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.
* #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res
normalize
cases (Zltb pbid next) normalize nodelta
[ 2: #Habsurd destruct (Habsurd) ]
cases pbr cases br normalize nodelta
[ 2,3: #_ % #Habsurd destruct (Habsurd) ]
@(eqZb_elim pbid bid) normalize nodelta
#Heq destruct (Heq)
[ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
#_ % #H destruct (H) elim Heq #H @H @refl
qed.

lemma beloadv_free_beloadv :
  ∀m,block,ptr,res.
    beloadv (free m block) ptr = Some ? res →
    beloadv m ptr = Some ? res.
* #contents #next #nextpos #block * #pblock #poff #res
#H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq
lapply H
whd in match (beloadv ??);
whd in match (beloadv ??) in ⊢ (? → %);
whd in match (nextblock (free ??));
cases (Zltb (block_id pblock) next)
[ 2: normalize #Habsurd destruct (Habsurd) ]
normalize nodelta
<(low_free_eq … Hblocks_neq)
<(high_free_eq … Hblocks_neq)
whd in match (free ??);
whd in match (update_block ?????);
@(eq_block_elim … pblock block)
[ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ]
#_ normalize nodelta
#H @H
qed.

lemma loadn_free_loadn :
  ∀n,m,block,ptr,res.
    loadn (free m block) ptr n = Some ? res →
    loadn m ptr n = Some ? res.
#n elim n
[ 1: normalize //
| 2: #n' #Hind #m #block #ptr #res #Hloadn
     whd in Hloadn:(??%?);
     cases (some_inversion ????? Hloadn) -Hloadn
     #be * #Hbeloadv #Hloadn
     cases (some_inversion ????? Hloadn) -Hloadn
     #res' * #Hloadn #Heq destruct (Heq)
     whd in match (loadn ???);
     >(beloadv_free_beloadv … Hbeloadv) normalize nodelta
     >(Hind … Hloadn) normalize nodelta @refl
] qed.     

lemma load_value_of_type_free_load_value_of_type :
  ∀ty,m,block,b,o,res.
    load_value_of_type ty (free m block) b o = Some ? res →
    load_value_of_type ty m b o = Some ? res.
#ty
cases ty
[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
| #structname #fieldspec | #unionname #fieldspec | #id ]
#m #block #b #o #res
whd in ⊢ ((??%?) → (??%?)); // #H
cases (some_inversion ????? H) #be * #Hloadn #Heq
>(loadn_free_loadn … Hloadn)
normalize nodelta assumption
qed.

lemma beloadv_free_beloadv2 :
  ∀m,block,ptr,res.
  pblock ptr ≠ block →
  beloadv m ptr = Some ? res →
  beloadv (free m block) ptr = Some ? res.
* #contents #next #nextpos #block * #pblock #poff #res #Hneq
whd in match (beloadv ??);
whd in match (beloadv ??) in ⊢ (? → %);
whd in match (nextblock (free ??));
cases (Zltb (block_id pblock) next)
[ 2: normalize #Habsurd destruct (Habsurd) ]
normalize nodelta
<(low_free_eq … Hneq)
<(high_free_eq … Hneq)
whd in match (free ??);
whd in match (update_block ?????);
@(eq_block_elim … pblock block)
[ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ]
#_ normalize nodelta
#H @H
qed.

(* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *)
lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.
#m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);
#H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);
elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))
[ 1: #Hlt >Hlt normalize nodelta
     @(eq_block_elim … b (pblock p))
     [ 1: #Heq >Heq whd in match (free ??);
          whd in match (update_block ?????); >eq_block_b_b
          normalize nodelta normalize in match (low ?);
          >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta
          #Habsurd destruct (Habsurd)
     | 2: #Hblock_neq whd in match (free ? ?);
          whd in match (update_block ?????);
          >(not_eq_block_rev … Hblock_neq) normalize nodelta
          cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
          [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
          >andb_lsimpl_true
          lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p)))
                                     (high (blocks m (pblock p))))
          cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
          normalize nodelta #H #_ /2 by ex_intro/
     ]
| 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ]
qed.

(* Cf [in_bounds_free_to_in_bounds] *)
lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.
#m #b #p #Hvalid
cases (valid_pointer_def … m p) #HA #HB
cases (valid_pointer_def … (free m b) p) #HC #HD
@HB @(in_bounds_free_to_in_bounds … b)
@HC @Hvalid
qed.

(* Making explicit the argument above. *)
lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.
#m #b #p
whd in match (valid_pointer ??);
whd in match (free ??);
whd in match (update_block ????);
whd in match (low_bound ??);
whd in match (high_bound ??);
@(eq_block_elim … b (pblock p))
[ 1: #Heq <Heq >eq_block_b_b normalize nodelta
     whd in match (low ?); whd in match (high ?);
     cases (Zltb ? (nextblock m))
     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
     >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd)
| 2: #Hneq #_ @Hneq ]
qed.

(* --------------------------------------------------------------------------- *)
(* loading and storing are inverse operations for integers. (Paolo's work 
 * contain a proof of this fact for pointers)                                  *)
(* --------------------------------------------------------------------------- *)

lemma fold_left_neq_acc_neq : 
  ∀m. ∀acc1,acc2. ∀y1,y2:BitVector m.
    acc1 ≠ acc2 → 
    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc1 y1 ≠
    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc2 y2.
#m elim m
[ 1: #acc1 #acc2 #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
| 2: #m' #Hind #acc1 #acc2 #y1 #y2
     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
     >Heq1 >Heq2 * #Hneq % whd in ⊢ ((??%%) → ?);
     cases hd1 cases hd2 normalize nodelta #H
     [ 1: lapply (Hind (p1 acc1) (p1 acc2) tl1 tl2 ?)
          [ 1: % #H' @Hneq destruct (H') @refl ] 
          * #H' @H' @H
     | 4: lapply (Hind (p0 acc1) (p0 acc2) tl1 tl2 ?)
          [ 1: % #H' @Hneq destruct (H') @refl ] 
          * #H' @H' @H
     | 2: lapply (Hind (p1 acc1) (p0 acc2) tl1 tl2 ?)
          [ 1: % #H' destruct ]
          * #H' @H' try @H
     | 3: lapply (Hind (p0 acc1) (p1 acc2) tl1 tl2 ?)
          [ 1: % #H' destruct ]
          * #H' @H' try @H ]
] qed.

lemma fold_left_aux :
  ∀m. ∀acc. ∀y1,y2:BitVector m.
    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y1 =
    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y2 →
    y1 = y2.
#m elim m
[ 1: #acc #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
| 2: #m' #Hind #acc #y1 #y2
     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
     >Heq1 >Heq2 whd in ⊢ ((??%%) → ?);
     cases hd1 cases hd2 normalize nodelta
     [ 1,4: #H >(Hind … H) @refl
     | 2: #Habsurd lapply (fold_left_neq_acc_neq ? (p1 acc) (p0 acc) tl1 tl2 ?)
          [ 1: % #H' destruct ]
          * #H @(False_ind … (H Habsurd))
     | 3: #Habsurd lapply (fold_left_neq_acc_neq ? (p0 acc) (p1 acc) tl1 tl2 ?)
          [ 1: % #H' destruct ]
          * #H @(False_ind … (H Habsurd)) ]
] qed.


lemma bv_neq_Z_neq_aux : 
  ∀n. ∀bv1,bv2 : BitVector n. ∀f.
    Z_of_unsigned_bitvector n bv1 ≠ 
    pos (fold_left Pos bool n (λacc:Pos.λb:bool.if b then p1 acc else p0 acc ) (f one) bv2).
#n elim n
[ 1: #bv1 #bv2 >(BitVector_O … bv1) >(BitVector_O … bv2) #f normalize % #H destruct
| 2: #n' #Hind #bv1 #bv2 #f
     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
     >Heq1 >Heq2 %
     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
     cases hd1 cases hd2 normalize nodelta
     normalize in ⊢ ((??%%) → ?);
     [ 1: #Hpos destruct (Hpos)
          lapply (fold_left_neq_acc_neq ? one (p1 (f one)) tl1 tl2 ?)
          [ 1: % #H destruct ]
          * #H @H @e0
     | 2: #Hpos destruct (Hpos)
          lapply (fold_left_neq_acc_neq ? one (p0 (f one)) tl1 tl2 ?)
          [ 1: % #H destruct ]
          * #H @H @e0
     | 3: #H cases (Hind tl1 tl2 (λx. p1 (f x))) #H' @H' @H
     | 4: #H cases (Hind tl1 tl2 (λx. p0 (f x))) #H' @H' @H
     ]
] qed.

(* Some aux. lemmas (and axioms ...) first *)
lemma bv_neq_Z_neq : ∀n. ∀bv1,bv2: BitVector n. 
  bv1 ≠ bv2 → Z_of_unsigned_bitvector n bv1 ≠ Z_of_unsigned_bitvector n bv2.
#n #bv1 #bv2 * #Hneq % #Hneq' @Hneq -Hneq lapply Hneq' -Hneq'
lapply bv2 lapply bv1 -bv1 -bv2
elim n
[ 1: #bv1 #bv2 >(BitVector_O bv1) >(BitVector_O bv2) //
| 2: #n' #Hind #bv1 #bv2
     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
     >Heq1 >Heq2
     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
     cases hd1 cases hd2 normalize nodelta
     [ 1: #Heq destruct (Heq) lapply (fold_left_aux … e0) * @refl
     | 4: #H >(Hind ?? H) @refl
     | 2: #H lapply (sym_eq ??? H) -H #H
          cases (bv_neq_Z_neq_aux ? tl2 tl1 (λx.x)) #H' @(False_ind … (H' H))
     | 3: #H
          cases (bv_neq_Z_neq_aux ? tl1 tl2 (λx.x)) #H' @(False_ind … (H' H)) ]
] qed.

definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs).


(* We prove the following properties for bestorev :
  1) storing doesn't modify the nextblock
  2) it does not modify the extents of the block written to
  3) since we succeeded in storing, the offset is in the bounds
  4) reading where we wrote yields the obvious result
  5) besides the written offset, the memory contains the same stuff
*)
lemma mem_bounds_invariant_after_bestorev :
∀m,m',b,ofs,bev.
  bestorev m (mk_pointer b ofs) bev = Some ? m' →
  nextblock m' = nextblock m ∧
  (∀b.low (blocks m' b) = low (blocks m b) ∧
      high (blocks m' b) = high (blocks m b)) ∧
  (low (blocks m b) ≤ (Z_of_offset ofs) ∧
   (Z_of_offset ofs) < high (blocks m b)) ∧   
  (contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv ofs)) = bev) ∧
  (∀o. o ≠ ofs → contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv o)) = 
                 contents (blocks m b) (Z_of_unsigned_bitvector ? (offv o))).
#m #m' #b #ofs #bev whd in ⊢ ((??%?) → ?);
#H
cases (if_opt_inversion ???? H) #Hlt -H normalize nodelta #H
cases (if_opt_inversion ???? H) #Hlelt -H #H
cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj
destruct try @refl
[ 1:
  #b' normalize cases b #br #bid cases b' #br' #bid'
  cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize
  try /2 by conj, refl/
| 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H
| 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H
| 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize
     >eqZb_z_z @refl
| 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta
     >eqZb_z_z normalize nodelta
     @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs)))
     [ 1,3: lapply Hneq cases o #bv1 cases ofs #bv2
            #Hneq lapply (bv_neq_Z_neq ? bv1 bv2 ?)
            [ 1,3: % #Heq destruct cases Hneq #H @H @refl ]
            * #H #Habsurd @(False_ind … (H Habsurd))
     | 2,4: normalize nodelta #H @refl ]
] qed.

(* Shifts an offset [i] times. storen uses a similar operation internally. *)
let rec shiftn (off:offset) (i:nat) on i : offset ≝
match i with
[ O ⇒ off
| S n ⇒
  shiftn (shift_offset 2 off (bitvector_of_nat … 1)) n
].

(* This axioms states that if we do not stray too far, we cannot circle back to ourselves. Pretty trivial, but a
   serious PITA to prove. *)
axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs.

(* Some stuff bunding the size of what we can write in memory *)

(* for leb_elim, shadowed in positive.ma *)
definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop. 
(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim.

(*include alias "arithmetics/nat.ma".*)

lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. |l| ≤ i → nth_opt A i l = None ?.
#A #l elim l //
#hd #tl #H #i elim i
[ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/
| 2: #i' #H' #Hle whd in match (nth_opt ???); @H lapply (monotonic_pred … Hle) //
] qed.

(* In order to prove the lemma on store_value_of_type and load_value_of_type,
   we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *)
lemma typesize_bounded : ∀ty. typesize ty ≤ 8.
* try // * try // qed.

(* Lifting bound on make_list *)
lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → |make_list A elt sz| ≤ bound.
#A #sz elim sz try //
#sz' #Hind #bound #elt #Hbound normalize
cases bound in Hbound;
[ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
| 2: #bound' #Hbound' lapply (Hind bound' elt ?)
     [ 1: @(monotonic_pred … Hbound')
     | 2: /2 by le_S_S/ ]
] qed.

lemma bytes_of_bitvector_bounded :
  ∀sz,bv. |bytes_of_bitvector (size_intsize sz) bv| = size_intsize sz.
* #bv normalize
[ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 //
| 2: cases (vsplit ????) normalize nodelta #bv0 #bv1
     cases (vsplit ????) normalize nodelta #bv2 #bv3 //
| 3: cases (vsplit ????) normalize nodelta #bv0 #bv1
     cases (vsplit ????) normalize nodelta #bv2 #bv3
     cases (vsplit ????) normalize nodelta #bv4 #bv5
     cases (vsplit ????) normalize nodelta #bv6 #bv7
     //
] qed.

lemma map_bounded :
  ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|.
  #A #B #l elim l try //
qed.


lemma fe_to_be_values_bounded : 
  ∀ty,v. |fe_to_be_values ty v| ≤ 8.
#ty cases ty
[ 1: #sz #sg ]
#v whd in match (fe_to_be_values ??);
     cases v normalize nodelta
     [ 1,5: @makelist_bounded @typesize_bounded
     | 2,6: * normalize nodelta #bv
          >map_bounded >bytes_of_bitvector_bounded //
     | 3,7: //
     | 4,8: #ptr // ]
qed.     

lemma fe_to_be_values_nonempty : ∀typ,v. ∃hd,tl. fe_to_be_values typ v = hd :: tl.
*
[ 2:  * /3 by ex_intro/ * #i
      [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize
           lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq
           <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/
      | 2: whd in match (fe_to_be_values ??); normalize nodelta normalize
           lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq
           <(vsplit_prod … Heq) normalize nodelta
           lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq'
            /3 by ex_intro/
      | 3: whd in match (fe_to_be_values ??); normalize nodelta normalize
           lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq
           <(vsplit_prod … Heq) normalize nodelta
           lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq'
           <(vsplit_prod … Heq') normalize nodelta
           lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq''
           <(vsplit_prod … Heq'') normalize nodelta
           lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq'''
            /3 by ex_intro/ ]
| 1: #sz #sg * /3 by ex_intro/ * #i
      [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize
           lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq
           <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/
      | 2: whd in match (fe_to_be_values ??); normalize nodelta normalize
           lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq
           <(vsplit_prod … Heq) normalize nodelta
           lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq'
            /3 by ex_intro/
      | 3: whd in match (fe_to_be_values ??); normalize nodelta normalize
           lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq
           <(vsplit_prod … Heq) normalize nodelta
           lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq'
           <(vsplit_prod … Heq') normalize nodelta
           lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq''
           <(vsplit_prod … Heq'') normalize nodelta
           lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq'''
            /3 by ex_intro/ ]
] qed.       


(* /!\ TODO the following proof is extremely ugly and indirect. I expect it to be
 *      hugely improvable.
 * /!\ *)

(* We prove some properties of [storen m ptr data]. Note that [data] is a list of back-end chunks.
   What we expect [storen] to do is to store this list starting at [ptr]. The property we expect to
   have is that the contents of this particular zone (ptr to ptr+|data|-1) match exactly [data], and
   that elsewhere the memory is untouched.
   Not so simple. Some observations:
   A) Pointers are encoded as block+offsets, and offsets are bitvectors, hence limited in range (2^16).
      On the other hand, block extents are encoded on Zs and are unbounded. This entails some problems
      when writing at the edge of the range of offsets and wrapping around, but that can be solved 
      resorting to ugliness and trickery.
   B) The [data] list is unbounded. Taking into account the point A), this means that we can lose
      data when writing (exactly as when we write in a circular buffer, overwriting previous stuff).
      The only solution to that is to explicitly bound |data| with something reasonable.
   Taking these observations into account, we prove the following invariants:
  1) storing doesn't modify the nextblock (trivial)
  2) it does not modify the extents of the block written to (trivial)
  3) all the offsets on which we run while writing are legal (trivial)
  3) if we index properly, we hit the stored data in the same order as in the list
  4) If we hit elsewhere, we find the memory unmodified. We have a problem for defining "elsewhere",
     because bitvectors (hence offsets) are limited in their range. For now, we define "elsewhere" as 
     "not reachable by shiftn from [ofs] to |data|"
  5) the pointer we write to is valid (trivial)
*)
lemma mem_bounds_invariant_after_storen :
  ∀data,m,m',b,ofs.
    |data| ≤ 8 → (* 8 is the size of a double. *)
    storen m (mk_pointer b ofs) data = Some ? m' →
    (nextblock m' = nextblock m ∧
    (∀b.low (blocks m' b) = low (blocks m b) ∧
        high (blocks m' b) = high (blocks m b)) ∧
    (∀index. index < |data| → low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧
                               Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧
    (∀index. index < |data| → nth_opt ? index data = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧
    (∀o. (∀i. i < |data| → o ≠ shiftn ofs i) →
         contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧
    (|data| > 0 → valid_pointer m (mk_pointer b ofs) = true)).
#l elim l
[ 1: #m #m' #b #ofs #_ normalize #H destruct @conj try @conj try @conj try @conj try @conj try @refl
     [ 1: #b0 @conj try @refl
(*     | 2: #Habsurd @False_ind /2 by le_S_O_absurd/*)
     | 2,3: #i #Habsurd @False_ind elim i in Habsurd; try /2/
     | 4: #o #Hout @refl
     | 5: #H @False_ind /2 by le_S_O_absurd/ ]
| 2: #hd #tl #Hind #m #m' #b #ofs #Hsize_bound #Hstoren
     whd in Hstoren:(??%?);
     cases (some_inversion ????? Hstoren) #m'' * #Hbestorev -Hstoren #Hstoren
     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HI #HJ #HK
     lapply (Hind … Hstoren) [ 1: /2 by le_S_to_le/ ] * * * * * 
     #HC #HD #HE #HF #HV #HW @conj try @conj try @conj try @conj try @conj
     [ 1: <HA <HC @refl
     | 2: #b elim (HB b) #HF #HG elim (HD b) #HG #HH @conj try //     
     | 4: *
          [ 1: #_ <HJ whd in match (nth 0 ???);
               lapply (HV ofs ?)
               [ 1: #i #Hlt @sym_neq % #Heq lapply (shiftn_no_wrap (S i) ? ofs)
                    [ 1: normalize in Hsize_bound;
                         cut (|tl| < 8) [ /2 by lt_plus_to_minus_r/ ]
                         #Hlt' lapply (transitive_lt … Hlt Hlt') // ]
                    * #H @H whd in match (shiftn ??); @Heq
               | 2: cases ofs #ofs' normalize // ]
          | 2: #i' #Hlt lapply (HF i' ?)
               [ 1: normalize normalize in Hlt; lapply (monotonic_pred … Hlt) //
               | 2: #H whd in match (nth_opt ???); >H @refl ] ]
     | 5: #o #H >HV
          [ 2: #i #Hlt @(H (S i) ?) 
               normalize normalize in Hlt; /2 by le_S_S/
          | 1: @HK @(H 0) // ]     
     | 6: #_ @(bestorev_to_valid_pointer … Hbestorev)
     | 3: *
          [ 1: #_ <HJ whd in match (shiftn ??);
               lapply (Zleb_true_to_Zle (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
               lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
               whd in match (low_bound ??); whd in match (high_bound ??);
               cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
               cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
               [ 2: normalize #Habsurd destruct ] normalize nodelta #Hltb
               lapply (Zltb_true_to_Zlt … Hltb) #Hlt' #Hleb lapply (Hleb (refl ??)) -Hleb #Hleb'
               normalize @conj try assumption
          | 2: #i' #Hlt cases (HB b) #Hlow1 #Hhigh1 cases (HD b) #Hlow2 #Hhigh2
               lapply (HE i' ?) [ 1: normalize in Hlt ⊢ %;lapply (monotonic_pred … Hlt) // ]
               >Hlow1 >Hhigh1 * #H1 #H2 @conj try @H1 try @H2
          ]
     ]
] qed.

(* Adapting the lemma above to (fe_to_be_values ty v) *)
lemma mem_bounds_invariant_after_storen_bis :
  ∀ty,v,m,m',b,ofs.
    storen m (mk_pointer b ofs) (fe_to_be_values ty v) = Some ? m' →
    (nextblock m' = nextblock m ∧
    (∀b.low (blocks m' b) = low (blocks m b) ∧
        high (blocks m' b) = high (blocks m b)) ∧
    (∀index. index < |fe_to_be_values ty v| → 
             low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧
             Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧
    (∀index. index < |(fe_to_be_values ty v)| → 
             nth_opt ? index (fe_to_be_values ty v) = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧
    (∀o. (∀i. i < |fe_to_be_values ty v| → o ≠ shiftn ofs i) →
         contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧
    (valid_pointer m (mk_pointer b ofs) = true)).
#ty #v #m #m' #b #ofs #Hstoren    
lapply (mem_bounds_invariant_after_storen … Hstoren)
[ @fe_to_be_values_bounded ]
* * * * * #H1 #H2 #H3 #H4 #H5 #H6 @conj try @conj try @conj try @conj try @conj
try assumption @H6 
cases (fe_to_be_values_nonempty ty v) #hd * #tl #H >H //
qed.

(* extension of [bestorev_to_valid_pointer] to storen *)
lemma storen_to_valid_pointer : 
  ∀data,xd,m,ptr,m'. storen m ptr (xd::data) = Some ? m' → 
    (∀b.low (blocks m' b) = low (blocks m b) ∧
         high (blocks m' b) = high (blocks m b)) ∧
    nextblock m' = nextblock m ∧         
    valid_pointer m ptr = true ∧
    valid_pointer m' ptr = true.
#data elim data
[ 1: #xd #m #ptr #res #Hstoren whd in Hstoren:(??%?);
     cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren'
     normalize in Hstoren'; destruct (Hstoren')
     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF
     lapply (bestorev_to_valid_pointer … Hbestorev) #Hvalid_ptr @conj try @conj try @conj try assumption
     @(bestorev_to_valid_pointer_after … Hbestorev)
| 2: #hd #tl #Hind #xd #m #ptr #res whd in match (storen ???); #Hstoren
     cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren' -Hstoren
     whd in match (shift_pointer ???) in Hstoren';
     lapply (bestorev_to_valid_pointer … Hbestorev) #H @conj try @conj try @conj try //
     lapply (Hind … Hstoren') * * * #Hbounds #Hnext #Hvalid1 #Hvalid2
     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF
     [ 1: #b @conj cases (Hbounds b) #HG #HH cases (HB b) #HI #HJ try //
     | 2: >Hnext >HA @refl ]
     @valid_pointer_of_Prop @conj try @conj try @conj
     cases (Hbounds (pblock ptr)) #HG #HH cases (HB (pblock ptr)) #HI #HJ
     [ 2: cases HC #Hlow #_ whd in match (low_bound ??);
           whd in match (Z_of_offset ?) in Hlow;
           >HG >HI @Hlow
     | 3: cases HC #_ #Hhigh whd in match (high_bound ??); >HH >HJ @Hhigh ]
     lapply (valid_pointer_to_Prop … Hvalid2) * * #Hnext #Hlow #Hhigh //
] qed.

     

lemma storen_to_valid_pointer_fe_to_be :
  ∀typ,v,m,ptr,m'. storen m ptr (fe_to_be_values typ v) = Some ? m' → 
    (∀b.low (blocks m' b) = low (blocks m b) ∧
         high (blocks m' b) = high (blocks m b)) ∧
    nextblock m' = nextblock m ∧         
    valid_pointer m ptr = true ∧
    valid_pointer m' ptr = true.
#typ #v cases (fe_to_be_values_nonempty … typ v) #hd * #tl #Heq >Heq
@storen_to_valid_pointer
qed.

lemma storen_beloadv_ok :
  ∀m,m',b,ofs,hd,tl.
  |hd::tl| ≤ 8 → (* 8 is the size of a double. *)
  storen m (mk_pointer b ofs) (hd::tl) = Some ? m' →
  ∀i. i < |hd::tl| → beloadv m' (mk_pointer b (shiftn ofs i)) = nth_opt ? i (hd::tl).
#m #m' #b #ofs #hd #tl #Hle #Hstoren
lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * 
#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
#i #Hle lapply (Hdata i Hle) #Helt >Helt
whd in match (beloadv ??); whd in match (nth_opt ???);
lapply (Hvalid_ptr ?) try //
whd in ⊢ ((??%?) → ?);
>Hnext cases (Zltb (block_id b) (nextblock m))
[ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct ]
>andb_lsimpl_true normalize nodelta
whd in match (low_bound ??); whd in match (high_bound ??);
cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H
lapply (Hvalid_offs i Hle) * #Hzle #Hzlt
>(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl
qed.

lemma storen_loadn_nonempty :
  ∀data,m,m',b,ofs.
  |data| ≤ 8 →
  storen m (mk_pointer b ofs) data = Some ? m' →
  ∃result. loadn m' (mk_pointer b ofs) (|data|) = Some ? result ∧ |result|=|data|.
#data elim data
[ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ]
#hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren
lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0
whd in match (loadn ???);
lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
whd in match (beloadv ??);
whd in match (low_bound ??); whd in match (high_bound ??);
>Hnext
cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh
cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta
[ 2: #Habsurd destruct ] >andb_lsimpl_true
#Hltb >Hltb normalize nodelta
cases (Hind  … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ]
#tl' * #Hloadn >Hloadn #Htl' normalize nodelta
%{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl
normalize >Htl' @refl
qed.


lemma loadn_beloadv_ok :
  ∀size,m,b,ofs,result.
  loadn m (mk_pointer b ofs) size = Some ? result →
  ∀i. i < size → beloadv m (mk_pointer b (shiftn ofs i)) = nth_opt ? i result.
#size elim size
[ 1: #m #b #ofs #result #Hloadn *
     [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
     | 2: #i' #Habsurd @False_ind /2 by le_S_O_absurd/ ]
| 2: #size' #Hind_size #m #b #ofs #result #Hloadn #i
     elim i
     [ 1: #_
          cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
          cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq
          destruct (Heq) whd in match (shiftn ofs 0);
          >Hbeloadv @refl
    | 2: #i' #Hind #Hlt
         whd in match (shiftn ofs (S i'));
         lapply (Hind ?)
         [ /2 by lt_S_to_lt/ ] #Hbeloadv_ind
         whd in Hloadn:(??%?);
         cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
         cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq -Hloadn'
         destruct (Heq)
         @Hind_size [ 2: lapply Hlt normalize @monotonic_pred ]
         @Hloadn_tl
    ]
] qed.



lemma storen_loadn_ok :
  ∀data.
  |data| ≤ 8 → (* 8 is the size of a double. *)
  ∀m,m',b,ofs.
  storen m (mk_pointer b ofs) data = Some ? m' →
  loadn m' (mk_pointer b ofs) (|data|) = Some ? data.
#data elim data try // #hd #tl #Hind #Hle #m #m' #b #ofs #Hstoren
lapply (storen_beloadv_ok m m' …  Hle Hstoren) #Hyp_storen
cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz
lapply (loadn_beloadv_ok (|hd::tl|) m' b ofs … Hloadn) #Hyp_loadn
cut (∀i. i < |hd::tl| → nth_opt ? i (hd::tl) = nth_opt ? i result)
[ #i #Hlt lapply (Hyp_storen … i Hlt) #Heq1
  lapply (Hyp_loadn … i Hlt) #Heq2 >Heq1 in Heq2; // ]
#Hyp
cut (result = hd :: tl)
[ 2: #Heq destruct (Heq) @Hloadn ]
@nth_eq_to_eq #i @sym_eq
@(leb_elim' … (S i) (|hd::tl|))
[ 1: #Hle @(Hyp ? Hle)
| 2: #Hnle cut (|hd::tl| ≤ i)
     [ lapply (not_le_to_lt … Hnle) normalize 
       @monotonic_pred ]
     #Hle'
     >nth_miss // >nth_miss //
] qed.
 

lemma mem_bounds_after_store_value_of_type :
  ∀m,m',ty,b,o,v.
  store_value_of_type ty m b o v = Some ? m' →
  (nextblock m' = nextblock m ∧
   (∀b.low (blocks m' b) = low (blocks m b) ∧
       high (blocks m' b) = high (blocks m b))).
#m #m' #ty #b #o #v
lapply (fe_to_be_values_bounded (typ_of_type ty) v)
cases ty
[ 1: | 2: #sz #sg | 3: #ptrty | 4: #arrayty #arraysz | 5: #argsty #retty
| 6: #sid #fields | 7: #uid #fields | 8: #cptr_id ]
whd in match (typ_of_type ?); #Hbounded
whd in match (store_value_of_type ?????);
[ 1,4,5,6,7: #Habsurd destruct (Habsurd)
| *: #Hstoren lapply (mem_bounds_invariant_after_storen … Hbounded Hstoren)
     * * * * * #Hnextblock #Hbounds_eq #Hnonempty 
     #Hcontents_upd #Hcontents_inv #Hvalid_ptr
     >Hnextblock @conj //
] qed.

lemma mem_bounds_after_store_value_of_type' :
  ∀m,m',ty,p,v.
  store_value_of_type' ty m p v = Some ? m' →
  (nextblock m' = nextblock m ∧
   (∀b.low (blocks m' b) = low (blocks m b) ∧
       high (blocks m' b) = high (blocks m b))).
#m #m' #ty * #b #o #v whd in match (store_value_of_type' ????);
@mem_bounds_after_store_value_of_type
qed.


definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v.
  match ty with
  [ ASTint sz sg ⇒
    match v with
    [ Vint sz' sg' ⇒ sz = sz' (* The sign does not matter *)
    | _ ⇒ False ]
  | ASTptr ⇒
    match v with
    [ Vptr p ⇒ True
    | _ ⇒ False ]
  ].


definition type_consistent_with_value : type → val → Prop ≝ λty,v.
match access_mode ty with
[ By_value chunk ⇒ ast_typ_consistent_with_value chunk v
| _ ⇒ True
].

(* We also need the following property. It is not provable unless [v] and [ty] are consistent. *)
lemma fe_to_be_values_size :
  ∀ty,v. ast_typ_consistent_with_value ty v →
         typesize ty = |fe_to_be_values ty v|.
*
[ 1: #sz #sg #v
     whd in match (fe_to_be_values ??); cases v
     normalize in ⊢ (% → ?);
     [ 1,3: @False_ind
     | 2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta
          >map_bounded >bytes_of_bitvector_bounded cases sz' //
     | 4: #p normalize in ⊢ (% → ?); @False_ind ]
| 2: #v cases v
     normalize in ⊢ (% → ?);
     [ 1,3: @False_ind
     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
     | 4: #p #_ // ]
] qed.

(* Not verified for floats atm. Restricting to integers. *)
lemma fe_to_be_to_fe_value_int : ∀sz,sg,v. 
  ast_typ_consistent_with_value (ASTint sz sg) v →
  (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v).
#sz #sg #v
whd in match (fe_to_be_values ??);
cases v normalize in ⊢ (% → ?);
[ 1,3: @False_ind
| 4: #p @False_ind
| 2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta
     cases sz' in i'; #i normalize nodelta
     normalize in i;
     whd in match (be_to_fe_value ??);
     normalize in match (size_intsize ?);
     whd in match (bytes_of_bitvector ??);
     [ 1: lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i
          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
          whd in match (build_integer_val ??);
          >(BitVector_O … ri) //
     | 2: lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i
          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
          whd in match (build_integer_val ??);
          normalize in match (size_intsize ?);
          whd in match (bytes_of_bitvector ??);
          lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri
          <(vsplit_prod … Heq_ri) normalize nodelta >Heq_ri
          whd in match (build_integer_val ??);
          >(BitVector_O … rri) //
     | 3: lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i
          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
          whd in match (build_integer_val ??);
          normalize in match (size_intsize ?);
          whd in match (bytes_of_bitvector ??);
          lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB
          <(vsplit_prod … Heq_iB) normalize nodelta >Heq_iB
          whd in match (bytes_of_bitvector ??);
          lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD
          <(vsplit_prod … Heq_iD) normalize nodelta >Heq_iD
          whd in match (bytes_of_bitvector ??);
          lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF
          <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF
          >(BitVector_O … iH) @refl ]
] qed.

lemma fe_to_be_to_fe_value_ptr :
  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
#b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta
cases br normalize nodelta >eqZb_z_z normalize nodelta
cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
* //
qed.

(* It turns out that the following property is not true in general. Floats are converted to
   BVundef, which are converted back to Vundef. But we care only about ints.  *)
lemma storev_loadv_int_compatible :
  ∀sz,sg,m,b,ofs,v,m'.
    ast_typ_consistent_with_value (ASTint sz sg) v →
    store (ASTint sz sg) m (mk_pointer b ofs) v = Some ? m' →
    load (ASTint sz sg) m' (mk_pointer b ofs) = Some ? v.
#sz #sg #m #b #ofs #v #m' #H
whd in ⊢ ((??%?) → (??%?)); #Hstoren
lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren)
>(fe_to_be_values_size … H) #H >H normalize nodelta
>fe_to_be_to_fe_value_int try //
qed.

(* For the arguments exposed before, we restrict the lemma to ints. *)
lemma store_value_load_value_int_compatible :
  ∀sz,sg,m,b,ofs,v,m'.
    type_consistent_with_value (Tint sz sg) v →
    store_value_of_type (Tint sz sg) m b ofs v = Some ? m' →
    load_value_of_type (Tint sz sg) m' b ofs = Some ? v.
#sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?);
cases v in H; normalize nodelta
[ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #_ @False_ind | 4: #vp #_ @False_ind ]
#Heq >Heq in H; #H
(* The lack of control on unfolds is extremely annoying. *)
whd in match (store_value_of_type ?????); #Hstoren
lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren)
whd in match (load_value_of_type ????);
>(fe_to_be_values_size … H) #H' >H' normalize nodelta
>fe_to_be_to_fe_value_int try //
qed.

lemma store_value_load_value_compatible :
  ∀ty,m,b,ofs,v,m'.
    type_consistent_with_value ty v →
    store_value_of_type ty m b ofs v = Some ? m' →
    load_value_of_type ty m' b ofs = Some ? v.
#ty #m #b #ofs #v #m' #H lapply H cases ty
[ | #sz #sg | #ty' | #ty' #n | #tl #ty' | #id #fl | #id #fl | #id ]
[ 1,4,5,6,7: normalize in ⊢ (? → % → ?); #_ #Habsurd destruct
| 2: @store_value_load_value_int_compatible
| 3: #Hconsistent whd in match (store_value_of_type ?????);
     whd in match (load_value_of_type ????); #Hstoren
     lapply (storen_loadn_ok … Hstoren)
     [ @fe_to_be_values_bounded ]
     #Hloadn >(fe_to_be_values_size … Hconsistent)
     >Hloadn normalize nodelta
     cases v in Hconsistent;
     [ @False_ind | #sz' #i' @False_ind | 3: @False_ind ]
     * #pb #poff #Hconsistent >fe_to_be_to_fe_value_ptr @refl
| 8: #Hconsistent whd in match (store_value_of_type ?????);
     whd in match (load_value_of_type ????); #Hstoren
     lapply (storen_loadn_ok … Hstoren)
     [ @fe_to_be_values_bounded ]
     #Hloadn >(fe_to_be_values_size … Hconsistent)
     >Hloadn normalize nodelta
     cases v in Hconsistent;
     [ @False_ind | #sz' #i' @False_ind | 3: @False_ind ]
     * #pb #poff #Hconsistent >fe_to_be_to_fe_value_ptr @refl
] qed.

(* storing something somewhere and loading at a disjoint loc yields the 
   same result as before the store. *)
lemma store_value_load_disjoint :
  ∀ty1,ty2,m,b1,ofs1,b2,ofs2,v,m'.
    ty1 ≠ ty2 →
    type_consistent_with_value ty1 v →
    store_value_of_type ty1 m b1 ofs1 v = Some ? m' →
    (b1 ≠ b2
     ∨ ((Z_of_offset ofs1) + (Z_of_nat (typesize (typ_of_type ty1))) ≤ (Z_of_offset ofs2))
     ∨ ((Z_of_offset ofs2) + (Z_of_nat (typesize (typ_of_type ty2))) ≤ (Z_of_offset ofs1))) →
    load_value_of_type ty2 m b2 ofs2 = load_value_of_type ty2 m' b2 ofs2.
#ty1 #ty2 #m #b1 #ofs1 #b2 #ofs2 #v #m' 
@cthulhu (*  Provable using the invariants provided by storen (see prev. lemma) *)
qed. 

(* Can we say anything about what we load in the overlap case ?  *)
(*
lemma store_value_load_overlap :
  ∀ty1,ty2,m,b,ofs1,ofs2,v,m'.
    ty1 ≠ ty2 →
    type_consistent_with_value ty1 v →
    store_value_of_type ty1 m b1 ofs1 v = Some ? m' →
    (Z_of_offset ofs2 < (Z_of_offset ofs1) + (Z_of_nat (typesize (typ_of_type ty1)))
     ∨ Z_of_offset ofs1 < (Z_of_offset ofs2) + (Z_of_nat (typesize (typ_of_type ty2)))) →
    load_value_of_type ty2 m b2 ofs2 = load_value_of_type ty2 m' b2 ofs2.
*)