Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/memoryInjections.ma

    r2448 r2468  
    11include "Clight/Cexec.ma".
     2include "Clight/MemProperties.ma". 
    23include "Clight/frontend_misc.ma".
    34
    … …  
    78   not allow to prove that the semantics for pointer less-than comparisons is
    89   conserved). *)
    9 
    10 (* --------------------------------------------------------------------------- *)   
    11 (* Some general lemmas on bitvectors (offsets /are/ bitvectors) *)
    12 (* --------------------------------------------------------------------------- *)
    13  
    14 lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.
    15 #n #bv whd in match (add_with_carries ????); elim bv //
    16 #n #hd #tl #Hind whd in match (fold_right2_i ????????);
    17 >Hind normalize
    18 cases n in tl;
    19 [ 1: #tl cases hd normalize @refl
    20 | 2: #n' #tl cases hd normalize @refl ]
    21 qed.
    22 
    23 lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.
    24 #n #bv whd in match (addition_n ???);
    25 >add_with_carries_n_O //
    26 qed.
    27 
    28 lemma replicate_Sn : ∀A,sz,elt.
    29   replicate A (S sz) elt = elt ::: (replicate A sz elt).
    30 // qed.
    31 
    32 lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.
    33 
    34 lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).
    35 #n #xa #a normalize @refl qed.
    36 
    37 (* useful facts on carry_of *)
    38 lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.
    39 lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.
    40 lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.
    41 lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.
    42 lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.
    43 
    44 
    45 
    46 definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).
    47 
    48 lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n).
    49     add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →
    50     add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.
    51 #n elim n
    52 [ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
    53      elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags
    54      >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)
    55      normalize #Heq destruct (Heq) @refl
    56 | 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
    57      destruct #Hind >add_with_carries_Sn >replicate_Sn
    58      whd in match (zero ?) in Hind; lapply Hind
    59      elim (add_with_carries (S (S n'))
    60             (false:::replicate bool (S n') false)
    61             (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct
    62             normalize >add_with_carries_Sn in Hind;
    63      elim (add_with_carries (S n') (replicate bool (S n') false)
    64                     (replicate bool (S n') false) true) #flags' #bits'
    65      normalize
    66      cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
    67             [VEmpty⇒true|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
    68      normalize #Heq destruct @refl
    69 ] qed.     
    70 
    71 lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).
    72 #n lapply (one_bv_Sn_aux n)
    73 whd in match (one_bv ?) in ⊢ (? → (??%%));
    74 elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags
    75 #H lapply (H bits flags (refl ??)) #H2 >H2 @refl
    76 qed.
    77 
    78 lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n.
    79     add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.
    80 #n   
    81 elim n
    82 [ 1: #a >(BitVector_O … a) normalize @refl
    83 | 2: #n' cases n'
    84      [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
    85           >(BitVector_O … tl) normalize cases xa @refl
    86      | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
    87           >one_bv_Sn >zero_Sn
    88           lapply (Hind tl)
    89           >add_with_carries_Sn >add_with_carries_Sn
    90           #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags
    91           normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq
    92           normalize nodelta @refl
    93 ] qed.         
    94 
    95 (* In order to use associativity on increment, we hide it under addition_n. *)
    96 lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).
    97 #n
    98 whd in match (increment ??) in ⊢ (∀_.??%?);
    99 whd in match (addition_n ???) in ⊢ (∀_.???%);
    100 #a lapply (increment_to_addition_n_aux n a)
    101 #Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl
    102 qed.
    103 
    104 (* Explicit formulation of addition *)
    105 
    106 (* Explicit formulation of the last carry bit *)
    107 let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝
    108 match n return λx. BitVector x → BitVector x → bool with
    109 [ O ⇒ λ_,_. init
    110 | S x ⇒ λa',b'.
    111   let hd_a ≝ head' … a' in
    112   let hd_b ≝ head' … b' in
    113   let tl_a ≝ tail … a' in
    114   let tl_b ≝ tail … b' in
    115   carry_of hd_a hd_b (ith_carry x tl_a tl_b init)
    116 ] a b.
    117 
    118 lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
    119   ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).
    120 #n #init #a #b @refl qed.
    121 
    122 lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
    123   ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.
    124 
    125 (* correction of [ith_carry] *)
    126 lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
    127   〈res_ab,flags_ab〉 = add_with_carries ? a b init →
    128   head' … flags_ab = ith_carry ? a b init.
    129 #n elim n
    130 [ 1: #init #a #b #res_ab #flags_ab
    131      elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
    132      elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
    133      elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
    134      elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
    135      destruct
    136      >(BitVector_O … tl_a) >(BitVector_O … tl_b)
    137      cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)
    138      @refl
    139 | 2: #n' #Hind #init #a #b #res_ab #flags_ab
    140      elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
    141      elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
    142      elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
    143      elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
    144      destruct
    145      lapply (Hind … init tl_a tl_b tl_res tl_flags)
    146      >add_with_carries_Sn >(ith_carry_Sn (S n'))
    147      elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab
    148      elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
    149      normalize nodelta cases hd_flags_ab normalize nodelta
    150      whd in match (head' ? (S n') ?); #H1 #H2
    151      destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl
    152 ] qed.
    153 
    154 (* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)
    155 definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.
    156 match n return λx. BitVector x → BitVector x → bool with
    157 [ O ⇒ λ_,_. init
    158 | S x ⇒ λa',b'.
    159   let hd_a ≝ head' … a' in
    160   let hd_b ≝ head' … b' in
    161   let tl_a ≝ tail … a' in
    162   let tl_b ≝ tail … b' in
    163   xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)
    164 ] a b.
    165 
    166 lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
    167   ith_bit ? a b init =  xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).
    168 #n #a #b // qed.
    169 
    170 lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
    171   ith_bit ? (xa ::: a) (xb ::: b) init =  xorb (xorb xa xb) (ith_carry ? a b init). // qed.
    172 
    173 (* correction of ith_bit *)
    174 lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
    175   〈res_ab,flags_ab〉 = add_with_carries ? a b init →
    176   head' … res_ab = ith_bit ? a b init.
    177 #n
    178 cases n
    179 [ 1: #init #a #b #res_ab #flags_ab
    180      elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
    181      elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
    182      elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
    183      elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
    184      destruct
    185      >(BitVector_O … tl_a) >(BitVector_O … tl_b)
    186      >(BitVector_O … tl_flags) >(BitVector_O … tl_res)
    187      normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl
    188 | 2: #n' #init #a #b #res_ab #flags_ab
    189      elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
    190      elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
    191      elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
    192      elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
    193      destruct
    194      lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)
    195      #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;
    196      #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'
    197      >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)
    198      cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;
    199      <(H1 (refl ??)) @refl
    200 ] qed.
    201 
    202 (* Transform a function from bit-vectors to bits into a vector by folding *)
    203 let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝
    204 match v with
    205 [ VEmpty ⇒ VEmpty ?
    206 | VCons sz elt tl ⇒
    207   let bit ≝ f ? v in
    208   bit ::: (bitvector_fold ? tl f)
    209 ].
    210 
    211 (* Two-arguments version *)
    212 let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝
    213 match v1  with
    214 [ VEmpty ⇒ λ_. VEmpty ?
    215 | VCons sz elt tl ⇒ λv2'.
    216   let bit ≝ f ? v1 v2 in
    217   bit ::: (bitvector_fold2 ? tl (tail … v2') f)
    218 ] v2.
    219 
    220 lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f.
    221   bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.
    222 
    223 (* These functions pack all the relevant information (including carries) directly. *)
    224 definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).
    225 
    226 lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init.
    227   addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.
    228  
    229 lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.
    230 
    231 (* Prove the equivalence of addition_n_direct with add_with_carries *)
    232 lemma addition_n_direct_ok : ∀n,carry,v1,v2.
    233   (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.
    234 #n elim n
    235 [ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl
    236 | 2: #n' #Hind #carry #v1 #v2
    237      elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1
    238      elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2
    239      lapply (Hind carry tl1 tl2)
    240      lapply (ith_bit_ok ? carry v1 v2)
    241      lapply (ith_carry_ok ? carry v1 v2)
    242      destruct
    243      #Hind >addition_n_direct_Sn
    244      >ith_bit_Sn >add_with_carries_Sn
    245      elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta
    246      cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
    247             [VEmpty⇒carry|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
    248      normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))
    249      whd in match head'; normalize nodelta
    250      #H1 #H2 >H1 >H2 @refl
    251 ] qed.
    252 
    253 lemma addition_n_direct_ok2 : ∀n,carry,v1,v2.
    254   (let 〈a,b〉 ≝ add_with_carries n v1 v2 carry in a) = addition_n_direct n v1 v2 carry.
    255 #n #carry #v1 #v2 <addition_n_direct_ok
    256 cases (add_with_carries ????) //
    257 qed.
    258  
    259 (* trivially lift associativity to our new setting *)     
    260 lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.
    261   addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =
    262   addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.
    263 #n #carry1 #carry2 #v1 #v2 #v3
    264 <addition_n_direct_ok <addition_n_direct_ok
    265 <addition_n_direct_ok <addition_n_direct_ok
    266 lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)
    267 elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta
    268 elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta
    269 #H @(sym_eq … H)
    270 qed.
    271 
    272 lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.
    273   addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.
    274 #n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/
    275 qed.
    276 
    277 definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
    278 definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
    279 
    280 
    281 (* fold andb on a bitvector. *)
    282 let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝
    283 match b with
    284 [ VEmpty ⇒ true
    285 | VCons sz elt tl ⇒
    286   andb elt (andb_fold ? tl)
    287 ].
    288 
    289 lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.
    290 
    291 lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.
    292 #n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl
    293 qed.
    294 
    295 lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).
    296   ith_carry … a (one_bv ?) false = andb_fold … a.
    297 #n elim n
    298 [ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)
    299      cases hd normalize @refl
    300 | 2: #n' #Hind #a
    301      elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
    302      lapply (Hind … tl) #Hind >one_bv_Sn
    303      >ith_carry_Sn whd in match (andb_fold ??);
    304      cases hd >Hind @refl
    305 ] qed.
    306 
    307 lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).
    308   ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).
    309 #n #a
    310 elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
    311 whd in match (head' ???);
    312 -a cases n in tl;
    313 [ 1: #tl >(BitVector_O … tl) cases hd normalize try //
    314 | 2: #n' #tl >one_bv_Sn >ith_bit_Sn
    315      >ith_increment_carry >tail_Sn
    316      cases hd try //
    317 ] qed.
    318 
    319 (* Lemma used to prove involutivity of two-complement negation *)
    320 lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).
    321    (andb_fold (S n) (negation_bv (S n) v) =
    322     andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).
    323 #n elim n
    324 [ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl
    325 | 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
    326      lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn
    327      >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind
    328      cases hd normalize nodelta
    329      [ 1: >xorb_false >(xorb_comm false ?) >xorb_false
    330      | 2: >xorb_false >(xorb_comm true ?) >xorb_true ]
    331      >ith_increment_carry
    332      cases (andb_fold (S n') (negation_bv (S n') tl)) @refl
    333 ] qed.
    334    
    335 (* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *)
    336 lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.
    337 #n elim n
    338 [ 1: #v >(BitVector_O v) @refl
    339 | 2: #n' cases n'
    340      [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
    341           >(BitVector_O … tl) normalize cases hd @refl
    342      | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
    343           lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%);
    344           whd in match twocomp_neg_direct; normalize nodelta
    345           whd in match increment_direct; normalize nodelta
    346           >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)
    347           >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
    348           generalize in match (addition_n_direct (S n'')
    349                                                    (negation_bv (S n'')
    350                                                    (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))
    351                                                    (one_bv (S n'')) false); #tail
    352           >ith_increment_carry >ith_increment_carry
    353           cases hd normalize nodelta
    354           [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false
    355           | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]
    356           <twocomp_neg_involutive_aux
    357           cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl
    358       ]
    359 ] qed.
    360 
    361 lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.
    362 #n #a #b #va #vb #H destruct (H) @conj @refl qed.
    363 
    364 lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.
    365 
    366 (* Injectivity of increment *)
    367 lemma increment_inj : ∀n. ∀a,b : BitVector n.
    368   increment_direct ? a = increment_direct ? b →
    369   a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).
    370 #n whd in match increment_direct; normalize nodelta elim n
    371 [ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //
    372 | 2: #n' cases n'
    373    [ 1: #_ #a #b
    374         elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
    375         elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
    376         >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b
    377         normalize #H @conj try //
    378    | 2: #n'' #Hind #a #b
    379         elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
    380         elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
    381         lapply (Hind … tl_a tl_b) -Hind #Hind
    382         >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
    383         >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false
    384         #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2
    385         lapply (Hind Heq2) * #Heq3 #Heq4
    386         cut (hd_a = hd_b)
    387         [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)
    388              * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm  ? hd_b) #Heq6 >(Heq6 Heq5)
    389              @refl ]
    390         #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]
    391         >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl
    392 ] qed.
    393 
    394 (* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)
    395 lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.
    396   a = b → increment_direct ? a = increment_direct ? b. // qed.
    397 
    398 (* A more general result. *)
    399 lemma addition_n_direct_inj : ∀n. ∀x,y,delta: BitVector n.
    400   addition_n_direct ? x delta false = addition_n_direct ? y delta false →
    401   x = y ∧ (ith_carry n x delta false = ith_carry n y delta false).
    402 #n elim n
    403 [ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * @conj @refl
    404 | 2: #n' #Hind #x #y #delta
    405      elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
    406      elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
    407      elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
    408      >addition_n_direct_Sn >ith_bit_Sn
    409      >addition_n_direct_Sn >ith_bit_Sn
    410      >ith_carry_Sn >ith_carry_Sn
    411      lapply (Hind … tlx tly tld) -Hind #Hind #Heq
    412      elim (bitvector_cons_inj_inv … Heq) #Heq_hd #Heq_tl
    413      lapply (Hind Heq_tl) -Hind * #HindA #HindB
    414      >HindA >HindB >HindB in Heq_hd; #Heq_hd
    415      cut (hdx = hdy)
    416      [ 1: cases hdd in Heq_hd; cases (ith_carry n' tly tld false)
    417           cases hdx cases hdy normalize #H try @H try @refl
    418           >H try @refl ]
    419      #Heq_hd >Heq_hd @conj @refl
    420 ] qed.
    421 
    422 (* We also need it the other way around. *)
    423 lemma addition_n_direct_inj_inv : ∀n. ∀x,y,delta: BitVector n.
    424   x ≠ y → (* ∧ (ith_carry n x delta false = ith_carry n y delta false). *)
    425    addition_n_direct ? x delta false ≠ addition_n_direct ? y delta false.
    426 #n elim n
    427 [ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * #H @(False_ind … (H (refl ??)))
    428 | 2: #n' #Hind #x #y #delta
    429      elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
    430      elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
    431      elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
    432      #Hneq
    433      cut (hdx ≠ hdy ∨ tlx ≠ tly)
    434      [ @(eq_bv_elim … tlx tly)
    435        [ #Heq_tl >Heq_tl >Heq_tl in Hneq;
    436          #Hneq cut (hdx ≠ hdy) [ % #Heq_hd >Heq_hd in Hneq; *
    437                                  #H @H @refl ]
    438          #H %1 @H
    439        | #H %2 @H ] ]
    440      -Hneq #Hneq
    441      >addition_n_direct_Sn >addition_n_direct_Sn
    442      >ith_bit_Sn >ith_bit_Sn cases Hneq
    443      [ 1: #Hneq_hd
    444           lapply (addition_n_direct_inj … tlx tly tld)         
    445           @(eq_bv_elim … (addition_n_direct ? tlx tld false) (addition_n_direct ? tly tld false))
    446           [ 1: #Heq -Hind #Hind elim (Hind Heq) #Heq_tl >Heq_tl #Heq_carry >Heq_carry
    447                % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) -Habsurd
    448                lapply Hneq_hd
    449                cases hdx cases hdd cases hdy cases (ith_carry ? tly tld false)
    450                normalize in ⊢ (? → % → ?); #Hneq_hd #Heq_hd #_
    451                try @(absurd … Heq_hd Hneq_hd)
    452                elim Hneq_hd -Hneq_hd #Hneq_hd @Hneq_hd
    453                try @refl try assumption try @(sym_eq … Heq_hd)
    454           | 2: #Htl_not_eq #_ % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
    455                elim Htl_not_eq -Htl_not_eq #HA #HB @HA @HB ]
    456      | 2: #Htl_not_eq lapply (Hind tlx tly tld Htl_not_eq) -Hind #Hind
    457           % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
    458           elim Hind -Hind #HA #HB @HA @HB ]
    459 ] qed.
    460 
    461 lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.
    462 
    463 lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).
    464    ith_carry (S n) a (one_bv (S n)) false
    465    = ith_carry (S n) a (zero (S n)) true.
    466 #n elim n
    467 [ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl
    468 | 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq
    469      lapply (Hind tl_a) #Hind
    470      >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl
    471 ] qed.
    472 
    473 lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.
    474 #n elim n //
    475 #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn
    476 >ith_carry_Sn >(Hind tl) cases hd @refl.
    477 qed.
    478 
    479 lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.
    480   addition_n_direct ? v (zero ?) false = v.
    481 #n elim n
    482 [ 1: #v >(BitVector_O … v) normalize @refl
    483 | 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
    484      lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn
    485      >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux
    486      >xorb_false @refl
    487 ] qed.
    488 
    489 lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.
    490 #n elim n
    491 [ 1: #a >(BitVector_O … a) normalize @refl
    492 | 2: #n' cases n'
    493      [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl
    494      | 2: #n'' #Hind #a
    495           elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq
    496           lapply (Hind tl_a) -Hind #Hind
    497           >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn
    498           >addition_n_direct_Sn >ith_bit_Sn
    499           >xorb_false >Hind @bitvector_cons_eq
    500           >increment_to_carry_aux @refl
    501      ]
    502 ] qed.
    503 
    504 lemma increment_to_carry : ∀n. ∀a,b : BitVector n.
    505   addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.
    506 #n #a #b >increment_to_carry_zero <associative_addition_n_direct
    507 >neutral_addition_n_direct @refl
    508 qed.
    509 
    510 lemma increment_direct_ok : ∀n,v. increment_direct n v = increment n v.
    511 #n #v whd in match (increment ??);
    512 >addition_n_direct_ok <increment_to_carry_zero @refl
    513 qed.
    514 
    515 (* Prove -(a + b) = -a + -b *)
    516 lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n.
    517   twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.
    518 whd in match twocomp_neg_direct; normalize nodelta
    519 lapply increment_inj_inv
    520 whd in match increment_direct; normalize nodelta
    521 #H #n #a #b
    522 <associative_addition_n_direct @H
    523 >associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))
    524 >increment_to_carry
    525 -H lapply b lapply a -b -a
    526 cases n
    527 [ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl
    528 | 2: #n' #a #b
    529      cut (negation_bv ? (addition_n_direct ? a b false)
    530            = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧
    531           notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))
    532      [ -n lapply b lapply a elim n'
    533      [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)
    534           elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)
    535           cases hd_a cases hd_b normalize @conj @refl
    536      | 2: #n #Hind #a #b
    537           elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa
    538           elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb
    539           lapply (Hind tl_a tl_b) * #H1 #H2
    540           @conj
    541           [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn
    542                >carry_notb >H2 @refl
    543           | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn
    544                >negation_bv_Sn >negation_bv_Sn
    545                >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq
    546                >xorb_lneg >xorb_rneg >notb_notb
    547                <xorb_rneg >H2 @refl
    548           ]
    549       ] ]
    550       * #H1 #H2 @H1
    551 ] qed.
    552 
    553 lemma addition_n_direct_neg : ∀n. ∀a.
    554  (addition_n_direct n a (negation_bv n a) false) = replicate ?? true
    555  ∧ (ith_carry n a (negation_bv n a) false = false).
    556 #n elim n
    557 [ 1: #a >(BitVector_O … a) @conj @refl
    558 | 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
    559      lapply (Hind … tl) -Hind * #HA #HB
    560      @conj
    561      [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl
    562      | 1: >negation_bv_Sn >addition_n_direct_Sn
    563           >ith_bit_Sn >HB >xorb_false >HA
    564           @bitvector_cons_eq elim hd @refl
    565      ]
    566 ] qed.
    567 
    568 (* -a + a = 0 *)
    569 lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).
    570 whd in match twocomp_neg_direct;
    571 whd in match increment_direct;
    572 normalize nodelta
    573 #n #a <associative_addition_n_direct
    574 elim (addition_n_direct_neg … a) #H #_ >H
    575 -H -a
    576 cases n try //
    577 #n'
    578 cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))
    579        ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))
    580 [ elim n'
    581      [ 1: @conj @refl
    582      | 2: #n' * #HA #HB @conj
    583           [ 1: >replicate_Sn >one_bv_Sn  >addition_n_direct_Sn
    584                >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl
    585           | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]
    586      ]
    587 ] * #H1 #H2 @H1
    588 qed.
    589 
    590 (* Lift back the previous result to standard operations. *)
    591 lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.
    592 #n #v whd in match twocomp_neg_direct; normalize nodelta
    593 whd in match increment_direct; normalize nodelta
    594 whd in match two_complement_negation; normalize nodelta
    595 >increment_to_addition_n <addition_n_direct_ok
    596 whd in match addition_n; normalize nodelta
    597 elim (add_with_carries ????) #a #b @refl
    598 qed.
    599 
    600 lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.
    601   two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).
    602 #n #a #b
    603 lapply (twocomp_neg_plus ? a b)
    604 >twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok
    605 <addition_n_direct_ok <addition_n_direct_ok
    606 whd in match addition_n; normalize nodelta
    607 elim (add_with_carries n a b false) #bits #flags normalize nodelta
    608 elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'
    609 normalize nodelta #H @H
    610 qed.
    611 
    612 lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).
    613 #n #a lapply (bitvector_opp_direct ? a)
    614 >twocomp_neg_direct_ok <addition_n_direct_ok
    615 whd in match (addition_n ???);
    616 elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H
    617 qed.
    618 
    619 lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.
    620 #n #a
    621 lapply (neutral_addition_n_direct n a)
    622 <addition_n_direct_ok
    623 whd in match (addition_n ???);
    624 elim (add_with_carries n a (zero n) false) #bits #flags #H @H
    625 qed.
    626 
    627 lemma injective_addition_n : ∀n. ∀x,y,delta : BitVector n.
    628   addition_n ? x delta = addition_n ? y delta → x = y. 
    629 #n #x #y #delta 
    630 lapply (addition_n_direct_inj … x y delta)
    631 <addition_n_direct_ok <addition_n_direct_ok
    632 whd in match addition_n; normalize nodelta
    633 elim (add_with_carries n x delta false) #bitsx #flagsx
    634 elim (add_with_carries n y delta false) #bitsy #flagsy
    635 normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq
    636 qed.
    637 
    638 lemma injective_inv_addition_n : ∀n. ∀x,y,delta : BitVector n.
    639   x ≠ y → addition_n ? x delta ≠ addition_n ? y delta. 
    640 #n #x #y #delta 
    641 lapply (addition_n_direct_inj_inv … x y delta)
    642 <addition_n_direct_ok <addition_n_direct_ok
    643 whd in match addition_n; normalize nodelta
    644 elim (add_with_carries n x delta false) #bitsx #flagsx
    645 elim (add_with_carries n y delta false) #bitsy #flagsy
    646 normalize #H1 #H2 @(H1 H2)
    647 qed.
    64810
    64911
    … …  
    66729
    66830lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
     31
     32(* --------------------------------------------------------------------------- *)
     33(* Some shorthands for conversion functions from BitVectorZ. *)
     34(* --------------------------------------------------------------------------- *)
     35
     36definition Zoub ≝ Z_of_unsigned_bitvector.
     37definition boZ ≝ bitvector_of_Z.
     38
     39(* Offsets are just bitvectors packed inside some useless and annoying constructor. *)
     40definition Zoo ≝ λx. Zoub ? (offv x).
     41definition boo ≝ λx. mk_offset (boZ ? x).
    66942
    67043(* --------------------------------------------------------------------------- *)   
    … …  
    915288(* Front-end values. *)
    916289inductive value_eq (E : embedding) : val → val → Prop ≝
    917 | undef_eq : ∀v.
    918   value_eq E Vundef v
     290| undef_eq :
     291  value_eq E Vundef Vundef
    919292| vint_eq : ∀sz,i.
    920293  value_eq E (Vint sz i) (Vint sz i)
    921 | vfloat_eq : ∀f.
    922   value_eq E (Vfloat f) (Vfloat f)
    923294| vnull_eq :
    924295  value_eq E Vnull Vnull
    … …  
    944315  load_value_of_type ty m1 b1 off1 = Some ? v1 →
    945316  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
    946 
     317 
     318(* Adapted from Compcert's Memory *)
     319definition non_aliasing : embedding → mem → Prop ≝
     320  λE,m.
     321  ∀b1,b2,b1',b2',delta1,delta2.
     322  b1 ≠ b2 →
     323  E b1 = Some ? 〈b1',delta1〉 →
     324  E b2 = Some ? 〈b2',delta2〉 →
     325  (b1' ≠ b2') ∨
     326  high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
     327  high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1).
     328 
    947329(* Definition of a memory injection *)
    948 record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
     330record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Prop ≝
    949331{ (* Load simulation *)
    950332  mi_inj : load_sim_ptr E m1 m2;
    … …  
    960342  (* Regions are preserved *)
    961343  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
    962   (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's.
    963    * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where
    964    * all variables are allocated in the same block. *)
    965   mi_disjoint : ∀b1,b2,b1',b2',o1',o2'.
    966                 b1 ≠ b2 →
    967                 E b1 = Some ? 〈b1',o1'〉 →
    968                 E b2 = Some ? 〈b2',o2'〉 →
    969                 b1' ≠ b2'
    970 }.
    971 
    972 (* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\
    973  * A memory extension is a [memory_inj] with some particular blocks designated as
    974  * being writeable. *)
    975 
    976 alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
    977 
    978 record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
    979 { me_inj : memory_inj E m1 m2;
    980   (* A list of blocks where we can write freely *)
    981   me_writeable : list block;
    982   (* These blocks are valid *)
    983   me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
    984   (* And pointers to m1 are oblivious to these blocks *)
    985   me_writeable_ok : ∀p,p'.
    986                      valid_pointer m1 p = true →
    987                      pointer_translation p E = Some ? p' →
    988                      ¬ (meml ? (pblock p') me_writeable)
     344  (* sub-blocks do not overlap (non-aliasing property) *)
     345  mi_nonalias : non_aliasing E m1
    989346}.
    990347
    … …  
    996353  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
    997354#E #p1 #v #Heq inversion Heq
    998 [ 1: #v #Habsurd destruct (Habsurd)
     355[ 1: #Habsurd destruct (Habsurd)
    999356| 2: #sz #i #Habsurd destruct (Habsurd)
    1000 | 3: #f #Habsurd destruct (Habsurd)
    1001 | 4:  #Habsurd destruct (Habsurd)
    1002 | 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct
     357| 3:  #Habsurd destruct (Habsurd)
     358| 4: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct
    1003359     %{p2} @conj try @refl try assumption
    1004360] qed.
    … …  
    1007363lemma value_eq_inversion :
    1008364  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
    1009   (∀v. P Vundef v) →
     365  (P Vundef Vundef) →
    1010366  (∀sz,i. P (Vint sz i) (Vint sz i)) →
    1011   (∀f. P (Vfloat f) (Vfloat f)) →
    1012367  (P Vnull Vnull) →
    1013368  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
    1014369  P v1 v2.
    1015 #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
     370#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4
    1016371inversion Heq
    1017 [ 1: #v #Hv1 #Hv2 #_ destruct @H1
     372[ 1: #Hv1 #Hv2 #_ destruct @H1
    1018373| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
    1019 | 3: #f #Hv1 #Hv2 #_ destruct @H3
    1020 | 4: #Hv1 #Hv2 #_ destruct @H4
    1021 | 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
    1022  
     374| 3: #Hv1 #Hv2 #_ destruct @H3
     375| 4: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H4 // ] qed.
     376
    1023377(* If we succeed to load something by value from a 〈b,off〉 location,
    1024378   [b] is a valid block. *)
    … …  
    1030384#ty #m * #brg #bid #off #v
    1031385cases ty
    1032 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1033 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     386[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     387| #structname #fieldspec | #unionname #fieldspec | #id ]
    1034388whd in match (load_value_of_type ????);
    1035 [ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
     389[ 1,6,7: #_ #Habsurd destruct (Habsurd) ]
    1036390#Hmode
    1037 [ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
     391[ 1,2,5: [ 1: elim sz ]
    1038392     normalize in match (typesize ?);
    1039393     whd in match (loadn ???);
    … …  
    1054408#ty #m * #brg #bid #off #v
    1055409cases ty
    1056 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1057 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     410[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     411| #structname #fieldspec | #unionname #fieldspec | #id ]
    1058412whd in match (load_value_of_type ????);
    1059 [ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
     413[ 1,6,7: #_ #Habsurd destruct (Habsurd) ]
    1060414#Hmode
    1061 [ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
     415[ 1,2,5: [ 1: elim sz ]
    1062416     normalize in match (typesize ?);
    1063417     whd in match (loadn ???);
    … …  
    1073427] qed.
    1074428
    1075 
    1076 lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
    1077 * #rg #id #m normalize
    1078 elim id /2/ qed.
    1079 
    1080 lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
    1081 * #rg #id #m normalize
    1082 elim id /2/ qed.
    1083 
    1084429lemma load_by_value_success_valid_block :
    1085430  ∀ty,m,b,off,v.
    … …  
    1088433    valid_block m b.
    1089434#ty #m #b #off #v #Haccess_mode #Hload
    1090 @valid_block_from_bool
     435@Zltb_true_to_Zlt
    1091436elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //
    1092437qed.
    … …  
    1102447qed.
    1103448
    1104 (* Making explicit the contents of memory_inj for load_value_of_type *)
     449(* Making explicit the contents of memory_inj for load_value_of_type.
     450 * Equivalent to Lemma 59 of Leroy & Blazy *)
    1105451lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
    1106452    memory_inj E m1 m2 →
    … …  
    1112458lapply (refl ? (access_mode ty))
    1113459cases ty
    1114 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1115 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     460[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     461| #structname #fieldspec | #unionname #fieldspec | #id ]
    1116462normalize in ⊢ ((???%) → ?); #Hmode #Hyp
    1117 [ 1,7,8: normalize in Hyp; destruct (Hyp)
    1118 | 5,6: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
     463[ 1,6,7: normalize in Hyp; destruct (Hyp)
     464| 4,5: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
    1119465lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer
    1120466lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H
    1121 qed.     
     467qed.
    1122468
    1123469(* -------------------------------------- *)
    … …  
    1154500whd in Halloc:(??%?); destruct (Halloc)
    1155501whd in match (beloadv ??) in ⊢ (??%%);
    1156 lapply (valid_block_to_bool … Hvalid) #Hlt
     502lapply (Zlt_to_Zltb_true … Hvalid) #Hlt
    1157503>Hlt >(zlt_succ … Hlt)
    1158504normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
    1159505cut (eqZb (block_id block) next = false)
    1160 [ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
     506[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq
    1161507>Hneq cases (eq_region ??) normalize nodelta  @refl
    1162508qed.
    … …  
    1181527(* Memory allocation preserves [memory_inj] *)
    1182528lemma alloc_memory_inj :
    1183   ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
     529  ∀E:embedding.
     530  ∀m1,m2,m2',z1,z2,r,new_block.
     531  ∀H:memory_inj E m1 m2.
    1184532  alloc m2 z1 z2 r = 〈m2', new_block〉 →
    1185533  memory_inj E m1 m2'.
    … …  
    1193541  lapply (refl ? (access_mode ty))
    1194542  cases ty in Hload_eq;
    1195   [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1196   | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     543  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     544  | #structname #fieldspec | #unionname #fieldspec | #id ]
    1197545  #Hload normalize in ⊢ ((???%) → ?); #Haccess
    1198   [ 1,7,8: normalize in Hload; destruct (Hload)
    1199   | 2,3,4,9: whd in match (load_value_of_type ????);
     546  [ 1,6,7: normalize in Hload; destruct (Hload)
     547  | 2,3,8: whd in match (load_value_of_type ????);
    1200548     whd in match (load_value_of_type ????);
    1201549     lapply (load_by_value_success_valid_block … Haccess Hload)
    … …  
    1204552     <(alloc_loadn_conservation … Halloc … Hvalid_block)
    1205553     @Hload
    1206   | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
     554  | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
    1207555| 2: @(mi_freeblock … Hmemory_inj)
    1208556| 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
    … …  
    1221569     cases (eq_region br' r) normalize #H @H
    1222570| 4: @(mi_region … Hmemory_inj)
    1223 | 5: @(mi_disjoint … Hmemory_inj)
    1224 ] qed.
    1225 
    1226 (* Memory allocation induces a memory extension. *)
    1227 lemma alloc_memory_ext :
    1228   ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
    1229   alloc m2 z1 z2 r = 〈m2', new_block〉 →
    1230   memory_ext E m1 m2'.
    1231 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
    1232 lapply (alloc_memory_inj … Hmemory_inj Halloc)
    1233 #Hinj' %
    1234 [ 1: @Hinj'
    1235 | 2: @[new_block]
    1236 | 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
    1237       #Heq destruct (Heq) whd elim m2 in Halloc;
    1238       #Hcontents #nextblock #Hnextblock
    1239       whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    1240       /2/
    1241 | 4: * #b #o * #b' #o' #Hvalid_ptr #Hembed %
    1242      normalize in ⊢ (% → ?); * [ 2: #H @H ]
    1243      #Heq destruct (Heq)
    1244      lapply (mi_valid_pointers … Hmemory_inj … Hvalid_ptr Hembed)
    1245      whd in ⊢ (% → ?);
    1246      (* contradiction because ¬ (valid_block m2 new_block)  *)
    1247      elim m2 in Halloc;
    1248      #contents_m2 #nextblock_m2 #Hnextblock_m2
    1249      whd in ⊢ ((??%?) → ?);
    1250      #Heq_alloc destruct (Heq_alloc)
    1251      normalize
    1252      lapply (irreflexive_Zlt nextblock_m2)
    1253      @Zltb_elim_Type0
    1254      [ #H * #Habsurd @(False_ind … (Habsurd H)) ] #_ #_ normalize #Habsurd destruct (Habsurd)
    1255 ] qed.
     571| 5: @(mi_nonalias … Hmemory_inj)
     572qed.
     573
     574(* ---------------------------------------------------------- *)
     575(* Lemma 40 of the paper of Leroy & Blazy on the memory model
     576 * and related lemmas *)
    1256577
    1257578lemma bestorev_beloadv_conservation :
    … …  
    1300621#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
    1301622cases ty
    1302 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1303 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try //
    1304 [ 1: elim sz | 2: elim fsz | 3: | 4: ]
     623[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     624| #structname #fieldspec | #unionname #fieldspec | #id ]
     625//
     626[ 1: elim sz ]
    1305627whd in ⊢ (??%%);
    1306628>(bestorev_loadn_conservation … Hstore … Hneq) @refl
    1307629qed.
    1308630
    1309 (* Writing in the "extended" part of a memory preserves the underlying injection *)
    1310 lemma bestorev_memory_ext_to_load_sim :
     631(* lift [bestorev_load_value_of_type_conservation] to storen *)
     632lemma storen_load_value_of_type_conservation :
     633  ∀l,mA,mB,wb,wo.
     634    storen mA (mk_pointer wb wo) l = Some ? mB →
     635    ∀rb,ro. eq_block wb rb = false →
     636    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
     637#l elim l
     638[ 1: #mA #mB #wb #wo normalize #Heq destruct //
     639| 2: #hd #tl #Hind #mA #mB #wb #wo #Hstoren
     640     cases (some_inversion ????? Hstoren) #mA' * #Hbestorev #Hstoren'
     641     whd in match (shift_pointer ???) in Hstoren':(??%?); #rb #ro #Hneq_block #ty
     642     lapply (Hind ???? Hstoren' … ro … Hneq_block ty) #Heq1
     643     lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2
     644     //
     645] qed.     
     646
     647definition typesize' ≝ λty. typesize (typ_of_type ty).
     648
     649lemma storen_load_value_of_type_conservation_in_block_high :
     650  ∀E,mA,mB,mC,wo,l.
     651    memory_inj E mA mB →
     652    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
     653    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
     654    high_bound mA b1 + Zoo delta < Zoo wo →
     655    ∀ty,off.
     656       Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 →
     657       low_bound … mA b1 ≤ Zoo off →
     658       Zoo off < high_bound … mA b1 →
     659       load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) =
     660       load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))).
     661#E #mA #mB #mC #wo #data #Hinj #blo #Hstoren #b1 #delta #Hembed #Hhigh #ty
     662(* need some stuff asserting that if a ptr is valid at the start of a write it's valid at the end. *)
     663cases data in Hstoren;
     664[ 1: normalize in ⊢ (% → ?); #Heq destruct //
     665| 2: #xd #data ]
     666#Hstoren
     667cases ty
     668[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     669| #structname #fieldspec | #unionname #fieldspec | #id ]#off #Hofflt #Hlow_load #Hhigh_load try @refl
     670whd in match (load_value_of_type ????) in ⊢ (??%%);
     671[ 1: lapply (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hbefore #Hafter
     672     lapply Hofflt -Hofflt lapply Hlow_load -Hlow_load lapply Hhigh_load -Hhigh_load
     673     lapply off -off whd in match typesize'; normalize nodelta     
     674     generalize in match (typesize ?); #n elim n try //
     675     #n' #Hind #o #Hhigh_load #Hlow_load #Hlt
     676     whd in match (loadn ???) in ⊢ (??%%);
     677     whd in match (beloadv ??) in ⊢ (??%%);
     678     cases (valid_pointer_to_Prop … Hbefore) * #HltB_store #HlowB_store #HhighB_store
     679     cases (valid_pointer_to_Prop … Hafter) * #HltC_store #HlowC_store #HhighC_store
     680     >(Zlt_to_Zltb_true … HltB_store) >(Zlt_to_Zltb_true … HltC_store) normalize nodelta
     681     cut (Zleb (low (blocks mB blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true)
     682     [ 1: (* Notice that:
     683                low mA b1 ≤ o < high mA b1
     684             hence, since E b1 = 〈blo, delta〉 with delta >= 0
     685                low mB blo ≤ (low mA b1 + delta) ≤ o+delta < (high mA b1 + delta) ≤ high mB blo *)
     686          @cthulhu ]
     687     #HA >HA >andb_lsimpl_true -HA
     688     cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mB blo)) = true)
     689     [ 1: (* Same argument as above *) @cthulhu ]
     690     #HA >HA normalize nodelta -HA
     691     cut (Zleb (low (blocks mC blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true)
     692     [ 1: (* Notice that storen does not modify the bounds of a block. Related lemma present in [MemProperties].
     693             This cut follows from this lemma (which needs some info on the size of the data written, which we
     694             have but must make explicit) and from the first cut. *)
     695          @cthulhu ]         
     696     #HA >HA >andb_lsimpl_true -HA
     697     cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mC blo)) = true)
     698     [ 1: (* Same argument as above *) @cthulhu ]
     699     #HA >HA normalize nodelta -HA
     700     normalize in match (bitvector_of_nat ??); whd in match (shift_pointer ???);
     701     whd in match (shift_offset ???); >commutative_addition_n >associative_addition_n
     702     lapply (Hind (mk_offset (addition_n offset_size (sign_ext 2 ? [[false; true]]) (offv o))) ???)
     703     [ 1: (* Provable from Hlt *) @cthulhu
     704     | 2: (* Provable from Hlow_load, need to make a "succ" commute from bitvector to Z *) @cthulhu
     705     | 3: (* Provable from Hlt, again *) @cthulhu ]
     706     cases (loadn mB (mk_pointer blo
     707              (mk_offset (addition_n ? (addition_n ?
     708                 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n')
     709     normalize nodelta                 
     710     cases (loadn mC (mk_pointer blo
     711              (mk_offset (addition_n ? (addition_n ?
     712                 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n')
     713     normalize nodelta try //
     714     [ 1,2: #l #Habsurd destruct ]
     715     #l1 #l2 #Heq
     716     cut (contents (blocks mB blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) =
     717          contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))))
     718     [ 1: (* Follows from Hhigh, indirectly *) @cthulhu ]
     719     #Hcontents_eq >Hcontents_eq whd in match (be_to_fe_value ??) in ⊢ (??%%);
     720     cases (contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))))
     721     normalize nodelta try //
     722     (* Ok this is going to be more painful than what I thought. *)
     723     @cthulhu
     724| *: @cthulhu
     725] qed.
     726
     727lemma storen_load_value_of_type_conservation_in_block_low :
     728  ∀E,mA,mB,mC,wo,l.
     729    memory_inj E mA mB →
     730    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
     731    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
     732    Zoo wo < low_bound mA b1 + Zoo delta →
     733    ∀ty,off.
     734       Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 →
     735       low_bound … mA b1 ≤ Zoo off →
     736       Zoo off < high_bound … mA b1 →
     737       load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) =
     738       load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))).
     739@cthulhu
     740qed.
     741
     742(* Writing in the "extended" part of a memory preserves the underlying injection. *)
     743lemma bestorev_memory_inj_to_load_sim :
    1311744  ∀E,mA,mB,mC.
    1312   ∀Hext:memory_ext E mA mB.
    1313   ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
    1314   bestorev mB (mk_pointer wb wo) v = Some ? mC →
     745  ∀Hext:memory_inj E mA mB.
     746  ∀block2. ∀i : offset. ∀ty : type.
     747  (∀block1,delta.
     748    E block1 = Some ? 〈block2, delta〉 →
     749    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
     750  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
    1315751  load_sim_ptr E mA mC.
    1316 #E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
    1317 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
    1318 (* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *)
    1319 lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb2
    1320 lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
    1321 cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
    1322 <(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
    1323 @(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
    1324 qed.
    1325 
    1326 (* Writing in the "extended" part of a memory preserves the whole memory injection *)
    1327 lemma bestorev_memory_ext_to_memory_inj :
     752#E #mA #mB #mC #Hinj #block2 #i #storety
     753cases storety
     754[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     755| #structname #fieldspec | #unionname #fieldspec | #id ]#Hout #storeval #Hstore whd
     756#b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value
     757whd in Hstore:(??%?);
     758[  1,5,6,7,8: destruct ]
     759[ 1:
     760lapply (mi_inj … Hinj … Hvalid … Hptr_trans … Hload_value)
     761lapply Hload_value -Hload_value
     762cases ty
     763[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
     764| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
     765#Hload_value
     766(* Prove that the contents of mB where v1 was were untouched. *)
     767* #readval' * #Hload_value2 #Hvalue_eq %{readval'} @conj try assumption
     768cases (some_inversion ????? Hptr_trans) * #b2' #delta' * #Hembed -Hptr_trans normalize nodelta
     769#Heq destruct (Heq)
     770@(eq_block_elim  … b2 block2)
     771[ 2,4,6,8: #Hblocks_neq <Hload_value2 @sym_eq @(storen_load_value_of_type_conservation … Hstore)
     772           @not_eq_block @sym_neq @Hblocks_neq
     773| 1,3,5,7: #Heq destruct (Heq) lapply (Hout … Hembed) *
     774           [ 1,3,5,7: #Hhigh <Hload_value2 -Hload_value2 @sym_eq
     775                      lapply (load_by_value_success_valid_ptr_aux … Hload_value) //
     776                      * * #Hlt #Hlowb_off1 #Hhighb_off1
     777                      lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1
     778                      lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1
     779                      @(storen_load_value_of_type_conservation_in_block_high … Hinj … Hstore … Hembed)
     780                      try //
     781                      (* remaining stuff provable from Hload_value  *)
     782                      @cthulhu
     783           | 2,4,6,8: #Hlow <Hload_value2 -Hload_value2 @sym_eq
     784                      lapply (load_by_value_success_valid_ptr_aux … Hload_value) //
     785                      * * #Hlt #Hlowb_off1 #Hhighb_off1
     786                      lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1
     787                      lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1
     788                      @(storen_load_value_of_type_conservation_in_block_low … Hinj … Hstore … Hembed)
     789                      try //
     790                      [ 1,3,5,7: (* deductible from Hlow + (sizeof ?) > 0 *) @cthulhu
     791                      | 2,4,6,8: (* deductible from Hload_value *) @cthulhu ]
     792           ]
     793]
     794| *: (* exactly the same proof as above  *) @cthulhu ]
     795qed.
     796
     797(* Lift the above result to memory_inj
     798 * This is Lemma 40 of Leroy & Blazy *)
     799lemma bestorev_memory_inj_to_memory_inj :
    1328800  ∀E,mA,mB,mC.
    1329   ∀Hext:memory_ext E mA mB.
    1330   ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
    1331   bestorev mB (mk_pointer wb wo) v = Some ? mC →
     801  ∀Hext:memory_inj E mA mB.
     802  ∀block2. ∀i : offset. ∀ty : type.
     803  (∀block1,delta.
     804    E block1 = Some ? 〈block2, delta〉 →
     805    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
     806  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
    1332807  memory_inj E mA mC.
    1333 #E #mA * #contentsB #nextblockB #HnextblockB #mC
    1334 #Hext #wb #wo #v #Hwb #Hstore
    1335 %
    1336 [ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
    1337 elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
    1338 #Hmem
    1339 [ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] -Hvalid -Hregion -Hdisjoint
    1340 whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
    1341 normalize in ⊢ (% → ?); #Hlt_wb
    1342 #p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) -Hcodomain
    1343 normalize in match (valid_pointer ??) in ⊢ (% → %);
    1344 >(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
    1345 cases (Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector offset_size (offv wo))
    1346        ∧Zltb (Z_of_unsigned_bitvector offset_size (offv wo)) (high (contentsB wb)))
    1347 normalize nodelta
    1348 [ 2: #Habsurd destruct (Habsurd) ]
    1349 #Heq destruct (Heq)
    1350 cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta
    1351 [ 2: #H @H ]
    1352 whd in match (update_block ?????);
    1353 cut (eq_block (pblock p') wb = false)
    1354 [ 2: #Heq >Heq normalize nodelta #H @H ]
    1355 @neq_block_eq_block_false @sym_neq
    1356 @(mem_not_mem_neq writeable … Hmem)
    1357 @(Hwriteable_ok … HvalidA Hembed)
    1358 qed.
    1359 
    1360 (* It even preserves memory extensions, with the same writeable blocks.  *)
    1361 lemma bestorev_memory_ext_to_memory_ext :
    1362   ∀E,mA,mB.
    1363   ∀Hext:memory_ext E mA mB.
    1364   ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
    1365   ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
    1366   ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
    1367 #E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
    1368 %{(mk_memory_ext …
    1369       (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
    1370       (me_writeable … Hext)
    1371       ?
    1372       (me_writeable_ok … Hext)
    1373  )} try @refl
    1374 #b #Hmemb
    1375 lapply (me_writeable_valid … Hext b Hmemb)
    1376 lapply (me_writeable_valid … Hext wb Hmem)
    1377 elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
    1378 lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
    1379 >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
    1380 cases (if Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector 16 (offv wo))
    1381        then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (contentsB wb)) 
    1382        else false)
    1383 normalize [ 2: #Habsurd destruct (Habsurd) ]
    1384 #Heq destruct (Heq) @Hb_valid
    1385 qed.
    1386 
    1387 (* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
    1388 lemma storen_memory_ext_to_memory_ext :
    1389   ∀E,mA,l,mB,mC.
    1390   ∀Hext:memory_ext E mA mB.
    1391   ∀wb,wo. meml ? wb (me_writeable … Hext) →
    1392   storen mB (mk_pointer wb wo) l = Some ? mC →
    1393   memory_ext E mA mC.
    1394 #E #mA #l elim l
    1395 [ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
    1396      @Hext
    1397 | 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
    1398      whd in ⊢ ((??%?) → ?);
    1399      lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
    1400      cases (bestorev mB (mk_pointer wb wo) hd)
    1401      normalize nodelta
    1402      [ 1: #H #Habsurd destruct (Habsurd) ]
    1403      #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
    1404      @(Hind … HextD … Hstore)
    1405      <Heq @Hmem
    1406 ] qed.     
    1407 
    1408 (* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
    1409 lemma store_value_of_type_memory_ext_to_memory_ext :
    1410   ∀E,mA,mB,mC.
    1411   ∀Hext:memory_ext E mA mB.
    1412   ∀wb,wo. meml ? wb (me_writeable … Hext) →
    1413   ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
    1414   memory_ext E mA mC.
    1415 #E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
    1416 cases ty
    1417 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1418 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
    1419 whd in ⊢ ((??%?) → ?);
    1420 [ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]
    1421 #Hstore
    1422 @(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
    1423 qed.
    1424 
    1425 (* Commutation results of standard binary operations with value_eq. *)
     808#E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore %
     809lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try //
     810cases Hinj #Hsim' #Hnot_valid #Hvalid #Hregion #Hnonalias try assumption
     811#p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid
     812cases ty in Hstore;
     813[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
     814| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
     815whd in ⊢ ((??%?) → ?);
     816[ 1,4,5,6,7: #Habsurd destruct ]
     817cases (fe_to_be_values ??)
     818[ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid -Hvalid destruct @refl
     819| *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_
     820     @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh
     821     @conj try @conj try assumption >Hnext try //
     822     cases (Hbounds (pblock p')) #HA #HB
     823     whd in match (low_bound ??); whd in match (high_bound ??);
     824     >HA >HB try assumption
     825] qed.
     826
     827(* ---------------------------------------------------------- *)
     828(* Lemma 41 of the paper of Leroy & Blazy on the memory model
     829 * and related lemmas *)
     830
     831(* The back-end might contain something similar to this lemma. *)
     832lemma be_to_fe_value_ptr :
     833  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
     834#b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta
     835cases br normalize nodelta >eqZb_z_z normalize nodelta
     836cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
     837<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
     838* //
     839qed.
     840
     841lemma value_eq_to_be_and_back_again :
     842  ∀E,ty,v1,v2.
     843  value_eq E v1 v2 →
     844  ast_typ_consistent_with_value ty v1 →
     845  ast_typ_consistent_with_value ty v2 →
     846  value_eq E (be_to_fe_value ty (fe_to_be_values ty v1 )) (be_to_fe_value ty (fe_to_be_values ty v2)).
     847#E #ty #v1 #v2 #Hvalue_eq
     848@(value_eq_inversion … Hvalue_eq) try //
     849[ 1: cases ty //
     850| 2: #sz #i cases ty
     851     [ 2: @False_ind
     852     | 1: #sz' #sg #H whd in ⊢ (% → ?); #Heq
     853          lapply (fe_to_be_to_fe_value … H) #H >H // ]
     854| 3: #p1 #p2 #Hembed cases ty
     855     [ 1: #sz #sg @False_ind
     856     | 2: #_ #_
     857          cases p1 in Hembed; #b1 #o1
     858          cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H
     859          cases (some_inversion ????? H) * #b3 #o3 * #Hembed
     860          normalize nodelta #Heq >be_to_fe_value_ptr >be_to_fe_value_ptr
     861          destruct %4 whd in match (pointer_translation ??);
     862          >Hembed normalize nodelta @refl
     863     ]
     864] qed.
     865
     866lemma storen_parallel_memory_exists :
     867  ∀E,m1,m2,m1',b1,i,b2,delta,ty,v1,v2.
     868  memory_inj E m1 m2 →
     869  value_eq E v1 v2 →
     870  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
     871  E b1 = Some ? 〈b2, delta〉 →
     872  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'.
     873@cthulhu qed.
     874  (*
     875#E #m1 #m2 #m1' #b1 #i #b2 #delta #ty #v1 #v2 #Hinj #Hvalue_eq
     876@(value_eq_inversion … Hvalue_eq)
     877[ 1: #v #Hstoren *)
     878     
     879
     880lemma storen_parallel_aux :
     881  ∀E,m1,m2.
     882  ∀Hinj:memory_inj E m1 m2.
     883  ∀v1,v2. value_eq E v1 v2 →
     884  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
     885  ∀ty,i,m1'.
     886  ast_typ_consistent_with_value ty v1 →
     887  ast_typ_consistent_with_value ty v2 → 
     888  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
     889  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
     890        memory_inj E m1' m2'.
     891#E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hok1 #Hok2
     892#Hstoren lapply (storen_to_valid_pointer_fe_to_be … Hstoren)
     893* * * #Hblocks_eq1 #Hnextblock1 #Hvalid_m1 #Hvalid_m1'
     894lapply (mi_valid_pointers … Hinj … (mk_pointer b1 i) (mk_pointer b2 (offset_plus i delta)) Hvalid_m1 ?)
     895[ 1: whd in ⊢ (??%%); >Hembed @refl ]
     896#Hvalid_m2
     897cases (valid_pointer_to_Prop … Hvalid_m2) * #Hnextblock2 #Hlow2 #Hhigh2
     898@cthulhu
     899qed.
     900
     901lemma foo :
     902  ∀E,m1,m2.
     903  ∀Hinj:memory_inj E m1 m2.
     904  ∀v1,v2. value_eq E v1 v2 →
     905  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
     906  ∀ty,i,m1'. store_value_of_type ty m1 b1 i v1 = Some ? m1' →
     907  ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧
     908         memory_inj E m1' m2'.
     909#E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hstore
     910@cthulhu qed.
     911
     912(* ------------------------------------------------------------------------- *)
     913(* Commutation results of standard unary and binary operations with value_eq. *)
     914
    1426915lemma unary_operation_value_eq :
    1427916  ∀E,op,v1,v2,ty.
    … …  
    1432921#E #op #v1 #v2 #ty #Hvalue_eq #r1
    1433922inversion Hvalue_eq
    1434 [ 1: #v #Hv1 #Hv2 #_ destruct
     923[ 1: #v #Hv1 #Hv2 destruct
    1435924     cases op normalize
    1436      [ 1: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     925     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    1437926          normalize #Habsurd destruct (Habsurd)
    1438      | 3: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     927     | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    1439928          normalize #Habsurd destruct (Habsurd)
    1440929     | 2: #Habsurd destruct (Habsurd) ]
    1441930| 2: #vsz #i #Hv1 #Hv2 #_
    1442931     cases op
    1443      [ 1: cases ty
    1444           [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     932     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    1445933          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
    1446934          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
    … …  
    1452940          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
    1453941     | 3: whd in match (sem_unary_operation ???);
    1454           cases ty
    1455           [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     942          cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    1456943          normalize nodelta
    1457944          whd in ⊢ ((??%?) → ?);
    … …  
    1459946               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
    1460947          | *: #Habsurd destruct (Habsurd) ] ]
    1461 | 3: #f #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
     948| 3: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
    1462949     cases op normalize nodelta
    1463      [ 1: cases ty
    1464           [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    1465           whd in match (sem_notbool ??);
    1466           #Heq1 destruct
    1467           cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/
    1468      | 2: normalize #Habsurd destruct (Habsurd)
    1469      | 3: cases ty
    1470           [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    1471           whd in match (sem_neg ??);
    1472           #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ]
    1473 | 4: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
    1474      cases op normalize nodelta
    1475      [ 1: cases ty
    1476           [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     950     [ 1: cases ty   [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    1477951          whd in match (sem_notbool ??);
    1478952          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
    1479953     | 2: normalize #Habsurd destruct (Habsurd)
    1480      | 3: cases ty
    1481           [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     954     | 3: cases ty    [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    1482955          whd in match (sem_neg ??);
    1483956          #Heq1 destruct ]
    1484 | 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
     957| 4: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
    1485958     cases op normalize nodelta
    1486      [ 1: cases ty
    1487           [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     959     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    1488960          whd in match (sem_notbool ??);         
    1489961          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
    1490962     | 2: normalize #Habsurd destruct (Habsurd)
    1491      | 3: cases ty
    1492           [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     963     | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    1493964          whd in match (sem_neg ??);         
    1494965          #Heq1 destruct ]
    … …  
    1506977#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
    1507978@(value_eq_inversion E … Hvalue_eq1)
    1508 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     979[ 1: | 2: #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    1509980[ 1: whd in match (sem_add ????); normalize nodelta
    1510981     cases (classify_add ty1 ty2) normalize nodelta
    1511      [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
     982     [ 1: #sz #sg | 2: #n #ty #sz #sg | 3: #n #sz #sg #ty | 4: #ty1' #ty2' ]
    1512983     #Habsurd destruct (Habsurd)
    1513984| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
    1514      cases (classify_add ty1 ty2) normalize nodelta     
    1515      [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
    1516      [ 2,3,5: #Habsurd destruct (Habsurd) ]
     985     cases (classify_add ty1 ty2) normalize nodelta
     986     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     987     [ 2,4: #Habsurd destruct (Habsurd) ]
    1517988     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1518      [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
    1519      [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
     989     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
     990     [ 1,2,4,5,7: #Habsurd destruct (Habsurd) ]
    1520991     [ 1: @intsize_eq_elim_elim
    1521992          [ 1: #_ #Habsurd destruct (Habsurd)
    … …  
    15411012               #Heq >Heq @refl ]
    15421013     ]
     1014(* | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     1015     cases (classify_add ty1 ty2) normalize nodelta
     1016     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     1017     [ 1,3,4: #Habsurd destruct (Habsurd) ]
     1018     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     1019     [ 1: | 2: #sz' #i'| 3: | 4: #p1' #p2' #Hembed' ]
     1020     [ 1,3,4,5,7: #Habsurd destruct (Habsurd) ]
     1021     #Heq >Heq %{r1} @conj //
     1022     /3 by ex_intro, conj, vfloat_eq/ *)
    15431023| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
    1544      cases (classify_add ty1 ty2) normalize nodelta     
    1545      [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     1024     cases (classify_add ty1 ty2) normalize nodelta
     1025     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     1026     [ 1,3,4: #Habsurd destruct (Habsurd) ]
     1027     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     1028     [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ]
    15461029     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
    1547      @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1548      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
    1549      [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
    1550      #Heq destruct (Heq)
    1551      /3 by ex_intro, conj, vfloat_eq/
    1552 | 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
    1553      cases (classify_add ty1 ty2) normalize nodelta     
    1554      [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
    1555      [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
    1556      @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1557      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
    1558      [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
    1559      @eq_bv_elim
     1030     @eq_bv_elim
    15601031     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
    15611032     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    1562 | 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     1033| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
    15631034     cases (classify_add ty1 ty2) normalize nodelta
    1564      [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
    1565      [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     1035     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     1036     [ 1,3,4: #Habsurd destruct (Habsurd) ]
    15661037     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1567      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     1038     [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ]
    15681039     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
    15691040     #Heq destruct (Heq)
    … …  
    16181089#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
    16191090@(value_eq_inversion E … Hvalue_eq1)
    1620 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     1091[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    16211092[ 1: whd in match (sem_sub ????); normalize nodelta
    16221093     cases (classify_sub ty1 ty2) normalize nodelta
    1623      [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
     1094     [ #sz #sg | #n #ty #sz #sg | #n #sz #sg #ty |#ty1' #ty2' ]
    16241095     #Habsurd destruct (Habsurd)
    16251096| 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
    16261097     cases (classify_sub ty1 ty2) normalize nodelta     
    1627      [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
    1628      [ 2,3,5: #Habsurd destruct (Habsurd) ]
     1098     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     1099     [ 2,3,4: #Habsurd destruct (Habsurd) ]
    16291100     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1630      [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
    1631      [ 1,2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ]
     1101     [  | #sz' #i' | | #p1' #p2' #Hembed' ]
     1102     [ 1,3,4: #Habsurd destruct (Habsurd) ]
    16321103     @intsize_eq_elim_elim
    16331104      [ 1: #_ #Habsurd destruct (Habsurd)
    … …  
    16361107          /3 by ex_intro, conj, vint_eq/           
    16371108      ]
    1638 | 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
    1639      cases (classify_sub ty1 ty2) normalize nodelta     
    1640      [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
    1641      [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     1109(*| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1110     cases (classify_sub ty1 ty2) normalize nodelta
     1111     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     1112     [ 1,4: #Habsurd destruct (Habsurd) ]
    16421113     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1643      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     1114     [  | #sz' #i' |  | #p1' #p2' #Hembed' ]
    16441115     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
    16451116     #Heq destruct (Heq)
    1646      /3 by ex_intro, conj, vfloat_eq/
    1647 | 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1117     /3 by ex_intro, conj, vfloat_eq/ *)
     1118| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
    16481119     cases (classify_sub ty1 ty2) normalize nodelta
    1649      [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
    1650      [ 1,2,5: #Habsurd destruct (Habsurd) ]
     1120     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     1121     [ 1,4: #Habsurd destruct (Habsurd) ]
    16511122     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1652      [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
    1653      [ 1,2,4,5,6,7,9,10: #Habsurd destruct (Habsurd) ]         
     1123     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
     1124     [ 1,2,4,5,7,8: #Habsurd destruct (Habsurd) ]
    16541125     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
    16551126                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    16561127     | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
    1657 | 5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1128| 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
    16581129     cases (classify_sub ty1 ty2) normalize nodelta
    1659      [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
    1660      [ 1,2,5: #Habsurd destruct (Habsurd) ]
     1130     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     1131     [ 1,4: #Habsurd destruct (Habsurd) ]
    16611132     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1662      [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
    1663      [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
     1133     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
     1134     [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ]
    16641135     #Heq destruct (Heq)
    16651136     [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
    … …  
    17071178#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
    17081179@(value_eq_inversion E … Hvalue_eq1)
    1709 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     1180[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    17101181[ 1: whd in match (sem_mul ????); normalize nodelta
    17111182     cases (classify_aop ty1 ty2) normalize nodelta
    1712      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     1183     [ 1: #sz #sg | 2: #ty1' #ty2' ]
    17131184     #Habsurd destruct (Habsurd)
    17141185| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
    17151186     cases (classify_aop ty1 ty2) normalize nodelta
    1716      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1717      [ 2,3: #Habsurd destruct (Habsurd) ]
     1187     [ 1: #sz #sg | 2: #ty1' #ty2' ]
     1188     [ 2: #Habsurd destruct (Habsurd) ]
    17181189     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1719      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
    1720      [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     1190     [  | #sz' #i' |  | #p1' #p2' #Hembed' ]
     1191     [ 1,3,4: #Habsurd destruct (Habsurd) ]
    17211192     @intsize_eq_elim_elim
    17221193      [ 1: #_ #Habsurd destruct (Habsurd)
    … …  
    17271198| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
    17281199     cases (classify_aop ty1 ty2) normalize nodelta
    1729      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1730      [ 1,3: #Habsurd destruct (Habsurd) ]
    1731      @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
    1732      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
    1733      [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
    1734      #Heq destruct (Heq)
    1735      /3 by ex_intro, conj, vfloat_eq/
     1200     [ 1: #sz #sg | 2: #ty1' #ty2' ]
     1201     [ 1,2: #Habsurd destruct (Habsurd) ]
    17361202| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
    17371203     cases (classify_aop ty1 ty2) normalize nodelta
    1738      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     1204     [ 1: #sz #sg | 2: #ty1' #ty2' ]
    17391205     #Habsurd destruct (Habsurd)
    1740 | 5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
    1741      cases (classify_aop ty1 ty2) normalize nodelta
    1742      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
    1743      #Habsurd destruct (Habsurd)
    1744 ] qed.
     1206] qed.     
    17451207
    17461208lemma div_value_eq :
    … …  
    17521214#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
    17531215@(value_eq_inversion E … Hvalue_eq1)
    1754 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     1216[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    17551217[ 1: whd in match (sem_div ????); normalize nodelta
    17561218     cases (classify_aop ty1 ty2) normalize nodelta
    1757      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     1219     [ 1: #sz #sg | 2: #ty1' #ty2' ]
    17581220     #Habsurd destruct (Habsurd)
    17591221| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
    17601222     cases (classify_aop ty1 ty2) normalize nodelta
    1761      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1762      [ 2,3: #Habsurd destruct (Habsurd) ]
     1223     [ 1: #sz #sg | 2: #ty1' #ty2' ]
     1224     [ 2: #Habsurd destruct (Habsurd) ]
    17631225     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1764      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
    1765      [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     1226     [  | #sz' #i' |  | #p1' #p2' #Hembed' ]
     1227     [ 1,3,4: #Habsurd destruct (Habsurd) ]
    17661228     elim sg normalize nodelta
    17671229     @intsize_eq_elim_elim
    … …  
    17851247| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
    17861248     cases (classify_aop ty1 ty2) normalize nodelta
    1787      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1788      [ 1,3: #Habsurd destruct (Habsurd) ]
    1789      @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
    1790      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
    1791      [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
    1792      #Heq destruct (Heq)
    1793      /3 by ex_intro, conj, vfloat_eq/
     1249     [ 1: #sz #sg | 2: #ty1' #ty2' ]
     1250     [ 1,2: #Habsurd destruct (Habsurd) ]
    17941251| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
    17951252     cases (classify_aop ty1 ty2) normalize nodelta
    1796      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     1253     [ 1: #sz #sg | 2: #ty1' #ty2' ]
    17971254     #Habsurd destruct (Habsurd)
    1798 | 5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
    1799      cases (classify_aop ty1 ty2) normalize nodelta
    1800      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
    1801      #Habsurd destruct (Habsurd)
    1802 ] qed.
     1255] qed.     
    18031256
    18041257lemma mod_value_eq :
    … …  
    18101263#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
    18111264@(value_eq_inversion E … Hvalue_eq1)
    1812 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     1265[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    18131266[ 1: whd in match (sem_mod ????); normalize nodelta
    18141267     cases (classify_aop ty1 ty2) normalize nodelta
    1815      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     1268     [ 1: #sz #sg | 2: #ty1' #ty2' ]
    18161269     #Habsurd destruct (Habsurd)
    18171270| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
    18181271     cases (classify_aop ty1 ty2) normalize nodelta
    1819      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1820      [ 2,3: #Habsurd destruct (Habsurd) ]
     1272     [ 1: #sz #sg | 2: #ty1' #ty2' ]
     1273     [ 2: #Habsurd destruct (Habsurd) ]
    18211274     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1822      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
    1823      [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     1275     [  | #sz' #i' |  | #p1' #p2' #Hembed' ]
     1276     [ 1,3,4: #Habsurd destruct (Habsurd) ]
    18241277     elim sg normalize nodelta
    18251278     @intsize_eq_elim_elim
    … …  
    18391292                   #H destruct (H)
    18401293                  /3 by ex_intro, conj, vint_eq/ ]
    1841      ]
    1842 | 3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
    1843      cases (classify_aop ty1 ty2) normalize nodelta
    1844      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1845      #Habsurd destruct (Habsurd)
    1846 | 4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
    1847      cases (classify_aop ty1 ty2) normalize nodelta
    1848      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1849      #Habsurd destruct (Habsurd)
    1850 | 5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
    1851      cases (classify_aop ty1 ty2) normalize nodelta
    1852      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
    1853      #Habsurd destruct (Habsurd)
     1294     ]     
     1295| *: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
     1296     cases (classify_aop ty1 ty2) normalize nodelta #foo #bar #Habsurd destruct (Habsurd)
    18541297] qed.
    18551298
    … …  
    19291372#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
    19301373@(value_eq_inversion E … Hvalue_eq1)
    1931 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     1374[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    19321375[ 2:
    19331376     @(value_eq_inversion E … Hvalue_eq2)
    1934      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     1377     [  | #sz' #i' |  | #p1' #p2' #Hembed' ]
    19351378     [ 2: whd in match (sem_shl ??);
    19361379          cases (lt_u ???) normalize nodelta
    … …  
    19501393#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
    19511394@(value_eq_inversion E … Hvalue_eq1)
    1952 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     1395[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    19531396whd in match (sem_shr ????); whd in match (sem_shr ????);
    19541397[ 1: cases (classify_aop ty ty') normalize nodelta
    1955      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     1398     [ 1: #sz #sg | 2: #ty1' #ty2' ]
    19561399     #Habsurd destruct (Habsurd)
    19571400| 2: cases (classify_aop ty ty') normalize nodelta
    1958      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1959      [ 2,3: #Habsurd destruct (Habsurd) ]
     1401     [ 1: #sz #sg | 2: #ty1' #ty2' ]
     1402     [ 2: #Habsurd destruct (Habsurd) ]
    19601403     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1961      [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
    1962      [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     1404     [  | #sz' #i' |  | #p1' #p2' #Hembed' ]
     1405     [ 1,3,4: #Habsurd destruct (Habsurd) ]
    19631406     elim sg normalize nodelta
    19641407     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
    19651408     /3 by ex_intro, conj, refl, vint_eq/
    1966 | 3: cases (classify_aop ty ty') normalize nodelta
    1967      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     1409| *: cases (classify_aop ty ty') normalize nodelta
     1410     #foo #bar
    19681411     #Habsurd destruct (Habsurd)
    1969 | 4: cases (classify_aop ty ty') normalize nodelta
    1970      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1971      #Habsurd destruct (Habsurd)
    1972 | 5: cases (classify_aop ty ty') normalize nodelta
    1973      [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
    1974      #Habsurd destruct (Habsurd)
    1975 ] qed.
     1412] qed.     
    19761413
    19771414lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
Note: See TracChangeset for help on using the changeset viewer.