Changeset 2578


Ignore:
Timestamp:
Jan 11, 2013, 9:36:21 PM (7 years ago)
Author:
garnier
Message:

Progress on CL to CM, fixed some stuff in memory injections.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2572 r2578  
    648648qed.
    649649
     650(* --------------------------------------------------------------------------- *)
     651(* Some more stuff on bitvectors. *)
     652(* --------------------------------------------------------------------------- *)
     653
    650654axiom commutative_multiplication :
    651655  ∀n. ∀v1,v2:BitVector n.
    652656  multiplication ? v1 v2 = multiplication ? v2 v1.
    653  
     657
    654658lemma commutative_short_multiplication :
    655659  ∀n. ∀v1,v2:BitVector n.
     
    670674axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
    671675
     676(* lemma eq_v_to_eq_Z : ∀n. ∀v1,v2:BitVector n. (Z_of_bitvector … v1) = (Z_of_bitvector eq_bv … v1 v2. *)
    672677
    673678
  • src/Clight/memoryInjections.ma

    r2572 r2578  
    3434(* --------------------------------------------------------------------------- *)
    3535
    36 definition Zoub ≝ Z_of_unsigned_bitvector.
    37 definition boZ ≝ bitvector_of_Z.
    38 
    39 (* Offsets are just bitvectors packed inside some useless and annoying constructor. *)
    40 definition Zoo ≝ λx. Zoub ? (offv x).
    41 definition boo ≝ λx. mk_offset (boZ ? x).
     36(* Offsets are just bitvectors packed inside some annoying constructor. *)
     37definition Zoo ≝ λx. Z_of_unsigned_bitvector ? (offv x).
     38definition boo ≝ λx. mk_offset (bitvector_of_Z ? x).
    4239
    4340(* --------------------------------------------------------------------------- *)   
     
    6562lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
    6663#a #b @(eq_block_elim … a b) /2/ qed.
     64
     65lemma block_decidable_eq : ∀a,b:block. (a = b) + (a ≠ b).
     66* #ra #ida * #rb #idb
     67cases ra cases rb
     68[ 2: %2 % #H destruct
     69| 3: %2 % #H destruct
     70| *: cases (decidable_eq_Z_Type ida idb)
     71  [ 1,3: * %1 @refl
     72  | 2,4: #Hneq %2 % #H destruct (H) cases Hneq #H @H @refl ]
     73] qed.
    6774
    6875lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
     
    218225         ]
    219226     | *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ]
    220 ] qed.     
     227] qed.
    221228
    222229(* Well in fact a valid pointer can be valid even after a free. Ah. *)
     
    286293].
    287294
     295(* Definition of embedding compatibility. *)
     296definition embedding_compatible : embedding → embedding → Prop ≝
     297λE,E'.
     298  ∀b:block. E b = None ? ∨
     299            E b = E' b.
     300
    288301(* We parameterise the "equivalence" relation on values with an embedding. *)
    289302(* Front-end values. *)
     
    320333λm,b.
    321334  high_bound m b ≤ low_bound m b.
     335 
     336(* Definition of a 16 bit bitvector-implementable Z *)
     337definition z_implementable_bv : Z → Prop ≝
     338  λz:Z.
     339    0 ≤ z ∧ z < Z_two_power_nat 16.
     340
     341(* Characterizing implementable blocks *)
     342definition block_implementable_bv ≝
     343  λm:mem.λb:block.
     344   z_implementable_bv (low_bound m b) ∧
     345   z_implementable_bv (high_bound m b).  (* FIXME this is slightly restrictive. We could allow the high bound to be 2^16.*)
     346
     347(* Characterizing blocks compatible with an embedding. This condition ensures
     348 * that we do not stray out of memory. *)
     349(*
     350definition block_ok_with_embedding ≝ λE:embedding.λb,m.
     351  ∀b',delta.
     352    E b = Some ? 〈b', delta〉 →
     353    (high_bound m b) + (Zoo delta) < Z_two_power_nat 16. *)
     354
     355(* We have to prove that the blocks we allocate are compatible with a given embedding.
     356   This amounts to proving that the embedding cannot shift the new block outside the 2^16 bound.
     357   Notice that the following def. only constraints block mapped through the embedding.
     358*)
     359definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝
     360λE.λb.λm,m'.
     361  match E b with
     362  [ None ⇒ True
     363  | Some loc ⇒
     364    let 〈b', delta〉 ≝ loc in
     365    block_implementable_bv m b ∧
     366    block_implementable_bv m' b' ∧
     367    (high_bound m b) + (Zoo delta) < Z_two_power_nat 16
     368  ].
     369   
    322370
    323371(* Adapted from Compcert's Memory *)
     
    326374  ∀b1,b2,b1',b2',delta1,delta2.
    327375  b1 ≠ b2 →
    328   block_region b1 = block_region b2 →
     376  (* block_region b1 = block_region b2 →  *) (* let's be generous with this one *)
    329377  E b1 = Some ? 〈b1',delta1〉 →
    330378  E b2 = Some ? 〈b2',delta2〉 →
    331   (b1' ≠ b2') ∨
    332   block_is_empty m b1' ∨
    333   block_is_empty m b2' ∨
    334   high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
    335   high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1).
    336  
     379  match block_decidable_eq b1' b2' with
     380  [ inl Heq ⇒
     381(*    block_is_empty m b1' ∨ *)
     382    high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
     383    high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1)
     384  | inr Hneq ⇒ True
     385  ].
     386
     387
     388(* Adapted from Compcert's "Memory" *)
     389
    337390(* Definition of a memory injection *)
    338391record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Prop ≝
     
    341394  (* Invalid blocks are not mapped *)
    342395  (* mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; *)
    343   (* Valid pointers are mapped to valid pointers*)
     396  (* Valid pointers are mapped to valid pointers *)
    344397  mi_valid_pointers : ∀p,p'.
    345398                       valid_pointer m1 p = true →
     
    347400                       valid_pointer m2 p' = true;
    348401  (* Blocks in the codomain are valid *)
    349   (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *)
     402  mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
    350403  (* Regions are preserved *)
    351404  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
    352405  (* sub-blocks do not overlap (non-aliasing property) *)
    353   mi_nonalias : non_aliasing E m1
     406  mi_nonalias : non_aliasing E m1;
     407  (* mapped blocks are bitvector-implementable *)
     408  (*  mi_implementable :
     409    ∀b,b',o'.
     410      E b = Some ? 〈b',o'〉 →
     411      block_implementable_bv m1 b ∧
     412      block_implementable_bv m2 b'; *)
     413  (* The offset produced by the embedding shifts data within the 2^16 bound ...
     414   * We need this to rule out the following case: consider a huge block taking up
     415   * all the space [0; 2^16[. We can come up with an embedding that keeps the same block
     416   * but which shifts the data by some value, effectively rotating all the data around the
     417   * 2^16 offset limit. Valid pointers stay valid, the block is implementable ... But we
     418   * obviously can't prove that the semantics of pointer comparisons is preserved. *)
     419  mi_nowrap :
     420    ∀b. block_in_bounds_if_mapped E b m1 m2
    354421}.
    355422
     
    363430     normalize in Hptr_trans; destruct
    364431| 2: * #b #o #p' #_ normalize #Habsurd destruct
    365 | 3: #b #b' #o' #Habsurd destruct
    366 | 4: normalize #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct ]
    367 qed.
     432| 3: #b #b' #off #Habsurd destruct
     433| 4: #b #b' #o' #Habsurd destruct
     434| 5: whd #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct
     435| 6: #b whd @I
     436] qed.
    368437
    369438(* ---------------------------------------------------------------------------- *)
    370439(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
     440(* ---------------------------------------------------------------------------- *)
     441
     442
     443
     444(**** Lemmas on value_eq. *)
    371445
    372446(* particulars inversions. *)
     
    419493qed. 
    420494
     495(* embedding compatibility preserves value equivalence *)
     496(* This is lemma 65 of Leroy&Blazy. *)
     497lemma embedding_compatibility_value_eq :
     498  ∀E,E'. embedding_compatible E E' → ∀v1,v2. value_eq E v1 v2 → value_eq E' v1 v2.
     499#E #E' #Hcompat #v1 #v2 #Hvalue_eq
     500@(value_eq_inversion … Hvalue_eq) try //
     501#p1 #p2 whd in match (pointer_translation ??); cases p1 #b1 #o1 normalize nodelta
     502cases (Hcompat b1)
     503[ #Hnone >Hnone normalize nodelta #Habsurd destruct
     504| #Heq >Heq #Hres %4 @Hres ]
     505qed.
     506
     507
     508
     509
     510(**** Lemmas on pointer validity wrt loads. *)
    421511
    422512(* If we succeed to load something by value from a 〈b,off〉 location,
     
    492582qed.
    493583
     584
     585
     586(**** Lemmas related to memory injections. *)
     587
    494588(* Making explicit the contents of memory_inj for load_value_of_type.
    495589 * Equivalent to Lemma 59 of Leroy & Blazy *)
     
    512606qed.
    513607
    514 (* -------------------------------------- *)
     608
    515609(* Lemmas pertaining to memory allocation *)
    516610
     
    577671  ∀H:memory_inj E m1 m2.
    578672  alloc m2 z1 z2 r = 〈m2', new_block〉 →
     673  block_implementable_bv m2' new_block →
    579674  memory_inj E m1 m2'.
    580 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
     675#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc #Himpl
    581676%
    582677[ whd
     
    612707     #Hbid_neq >Hbid_neq
    613708     cases (eq_region br' r) normalize #H @H
     709| #b #b' #o' #Hembed lapply (mi_nodangling … Hmemory_inj b b' o' Hembed) #H
     710  @(alloc_valid_block_conservation … Halloc … H)
    614711| @(mi_region … Hmemory_inj)
    615 |  @(mi_nonalias … Hmemory_inj)
    616 qed.
     712| @(mi_nonalias … Hmemory_inj)
     713| #b lapply (mi_nowrap … Hmemory_inj b)
     714   whd in ⊢ (% → %);
     715   lapply (mi_nodangling … Hmemory_inj b)
     716   cases (E b) normalize nodelta try //
     717   * #B #OFF normalize nodelta #Hguard
     718   * * #H1 #H2 #Hinbounds @conj try @conj try assumption
     719   @(eq_block_elim … new_block B)
     720     [ #H destruct try //
     721     | #H cases m2 in Halloc H2; #contents #nextblock #notnull
     722       whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) *
     723       >unfold_low_bound >unfold_high_bound #HA #HB
     724       @conj
     725       >unfold_low_bound >unfold_high_bound
     726       whd in match (update_block ?????);
     727       >(not_eq_block … (sym_neq ??? H)) normalize nodelta
     728       try assumption ]
     729] qed.
     730(*       
     731   | @(eq_block_elim … new_block B)
     732     [ 2: #H cases m2 in Halloc Hinbounds; #contents #nextblock #notnull
     733       whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     734       >unfold_high_bound in Himpl ⊢ %;
     735       whd in ⊢ (% → % → %);
     736       >unfold_low_bound >unfold_high_bound
     737       whd in match (update_block ?????); >eq_block_b_b
     738       normalize nodelta * #HA #HB
     739       >unfold_high_bound       
     740       whd in match (update_block ?????) in ⊢ (% → %);
     741       >(not_eq_block … (sym_neq ??? H)) normalize nodelta
     742       try //
     743     | (* absurd case *) #Heq destruct (Heq)
     744       lapply (Hguard ?? (refl ??)) #Hvalid
     745       (* hence new_block ≠ B *)
     746       cases m2 in Halloc Hvalid; #contents #nextblock #notnull
     747       whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     748       whd in ⊢ (% → ?); #Habsurd
     749       lapply (irreflexive_Zlt nextblock) *
     750       #H @False_ind @H @Habsurd
     751     ]
     752   ]
     753]
     754qed. *)
     755
     756
     757(* TODO: these axioms are not enough for memory injections. We need the updated embedding as a byproduct
     758 * of the allocation. *)
    617759
    618760(* Allocating in m1 such that the resulting block has no image in m2 preserves
     
    686828             normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl
    687829             %4 @Htrans ]
    688 #Hload <Hfree 
     830#Hload <Hfree
    689831(* routine *)
    690832@cthulhu
     
    727869#E #m1 #m2 #m1' #Hinj #b #Hfree
    728870cases Hinj
    729 #Hload_sim #Hvalid #Hregion #Hnonalias
     871#Hload_sim #Hvalid #Hnodangling #Hregion #Hnonalias #Himplementable
    730872% try assumption
    731873[ @(free_load_sim_ptr_m1 … Hload_sim … Hfree)
    732874| #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation)
    733875  <Hfree in Hvalid_m1'; @valid_free_to_valid
    734 | @(free_non_aliasing_m1 … Hinj … Hfree) ]
    735 qed.
     876| @(free_non_aliasing_m1 … Hinj … Hfree)
     877| #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?);
     878  cases (E bb) normalize nodelta try //
     879  * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj
     880  try //
     881  @(eq_block_elim … b bb)
     882  [ 2,4:
     883      #Hneq destruct (Hfree)
     884      whd in match (free ??);
     885      whd >unfold_low_bound >unfold_high_bound
     886      whd in match (update_block ?????); >(not_eq_block … (sym_neq ??? Hneq))
     887      try @conj normalize nodelta cases HA try //
     888  | 1,3:
     889      #H destruct whd in match (free ??);
     890      whd [ >unfold_low_bound ] >unfold_high_bound
     891      whd in match (update_block ?????); >eq_block_b_b
     892      normalize nodelta try @conj try // % try //
     893  ]
     894] qed.   
     895
     896(*
     897  #b0 #b' #o' #Hembed lapply (Himplementable b0 b' o' Hembed) *
     898  #HA #HB @conj try //
     899  cases m1 in Hfree HA; #contents1 #nextblock1 #Hpos1
     900  whd in ⊢ ((??%%) → ? → ?); #Heq destruct (Heq)
     901  whd in ⊢ (% → %); *
     902  whd in match (low_bound ??) in ⊢ (% → % → %);
     903  whd in match (high_bound ??) in ⊢ (% → % → %); #HA #HB
     904  @(eq_block_elim … b0 b)
     905  [ #H whd in match (update_block ?????); >H >eq_block_b_b @conj
     906    normalize nodelta
     907    normalize @conj try //
     908  | #H whd in match (update_block ?????); >(not_eq_block … H) @conj
     909    try // ] ]
     910qed.*)
    736911
    737912(* Lifting lemma 47 to memory injs *)
     
    745920#E #m1 #m2 #m2' #Hinj #b #Hfree #b1_not_mapped
    746921% cases Hinj try //
    747 #Hload_sim #Hvalid #Hregion #Hnonalias
     922#Hload_sim #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl
    748923[ (* We succed performing a load from m1. Case analysis: if by-value, cannot map to freed block [b]
    749924     (otherwise contradiction), hence simulation proceeds through Hinj.
     
    757932     if (pblock p') ≠ b then straightforward simulation *)
    758933  @cthulhu
    759 | @Hregion ]
    760 qed.
     934| #bb #b' #o' #Hembed
     935  lapply (Hnodangling bb b' o' Hembed) #Hvalid_before_free
     936  (* cf case above *)
     937  @cthulhu
     938| @Hregion
     939| #bb lapply (Himpl bb)
     940  whd in ⊢ (% → %); cases (E bb) normalize nodelta try //
     941  * #BLO #OFF normalize nodelta * * destruct (Hfree)
     942  #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption
     943  cases Hbb try // #Hlow_bb #Hhigh_bb
     944  [ >unfold_low_bound
     945  | *: >unfold_high_bound ]
     946  whd in match (update_block ?????);
     947  @(eq_block_elim … BLO b)
     948  #H [ 1,3,5: destruct (H) normalize nodelta try //
     949               @conj try //
     950     | *: normalize nodelta cases HBLO try // ]     
     951] qed.
     952
    761953
    762954(* Lemma 64 of L&B on [freelist] *)
     
    9691161cases storety
    9701162[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    971 | #structname #fieldspec | #unionname #fieldspec | #id ]#Hout #storeval #Hstore whd
     1163| #structname #fieldspec | #unionname #fieldspec | #id ] #Hout #storeval #Hstore whd
    9721164#b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value
    9731165whd in Hstore:(??%?);
     
    10241216#E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore %
    10251217lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try //
    1026 cases Hinj #Hsim' #Hvalid #Hregion #Hnonalias try assumption
    1027 #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid
    1028 cases ty in Hstore;
    1029 [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
    1030 | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
    1031 whd in ⊢ ((??%?) → ?);
    1032 [ 1,4,5,6,7: #Habsurd destruct ]
    1033 cases (fe_to_be_values ??)
    1034 [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid -Hvalid destruct @refl
    1035 | *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_
    1036      @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh
    1037      @conj try @conj try assumption >Hnext try //
    1038      cases (Hbounds (pblock p')) #HA #HB
    1039      whd in match (low_bound ??); whd in match (high_bound ??);
    1040      >HA >HB try assumption
     1218cases Hinj #Hsim' #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl try assumption
     1219[
     1220  #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid
     1221  cases ty in Hstore;
     1222  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
     1223  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
     1224  whd in ⊢ ((??%?) → ?);
     1225  [ 1,4,5,6,7: #Habsurd destruct ]
     1226  cases (fe_to_be_values ??)
     1227  [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid -Hvalid destruct @refl
     1228  | *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_
     1229       @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh
     1230       @conj try @conj try assumption >Hnext try //
     1231       cases (Hbounds (pblock p')) #HA #HB
     1232       whd in match (low_bound ??); whd in match (high_bound ??);
     1233       >HA >HB try assumption
     1234  ]
     1235| lapply (mem_bounds_after_store_value_of_type … Hstore)
     1236  * #Hnext_eq #Hb
     1237  #b #b' #o' cases (Hb b') #Hlow_eq #Hhigh_eq #Hembed
     1238  lapply (mi_nodangling … Hinj … Hembed)
     1239  whd in match (valid_block ??) in ⊢ (% → %);
     1240  >(Hnext_eq) try //
     1241| #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %);
     1242  cases (E b) try //
     1243  * #BLO #OFF normalize nodelta * *
     1244  #Hb #HBLO #Hbound try @conj try @conj try assumption
     1245  lapply (mem_bounds_after_store_value_of_type … Hstore) *
     1246  #_ #Hbounds
     1247  cases (Hbounds BLO) #Hlow #Hhigh whd %
     1248  [ >unfold_low_bound | >unfold_high_bound ]
     1249  >Hlow >Hhigh cases HBLO try //
    10411250] qed.
    10421251
     
    12021411   The memory model of Cerco is in a sense much more realistic. When storing a front-end
    12031412   value fv, the story is the following :
    1204    1) the value fv is marshelled into a list of back-end values (byte-sized) which correspond
     1413   1) the value fv is marshalled into a list of back-end values (byte-sized) which correspond
    12051414      to the actual size of the data in-memory. This list is then stored as-is at the
    12061415      location 〈block, offset〉.
     
    12971506  load_sim_ptr E m1' m2.
    12981507#E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore
    1299 cases Hinj #Hsim #Hvalid #Hregion_eq #Hnonalias
     1508cases Hinj #Hsim #Hvalid #Hnodangling #Hregion_eq #Hnonalias #Himpl
    13001509cases ty in Hstore;
    13011510[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     
    13091518         destruct ]
    13101519#Heq <Heq in Hload; #Hload
    1311 (* Three times the same proof, but computing the indices is a PITA *)
     1520(* Three times the same proof, but computing the indices for the subcases is a PITA *)
    13121521[ 1:
    13131522  cases ty' in Hload;
     
    13371546  #Hload @(Hsim … Hembed' … Hload)
    13381547  @(load_by_value_success_valid_pointer … Hload) //
    1339 ] qed.  
     1548] qed.
    13401549
    13411550lemma store_value_of_type_memory_inj :
     
    13491558%
    13501559[ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore)
    1351 | 2: (* trivial *) @cthulhu
    1352 | 3: (* easy *) @cthulhu
    1353 | 4: (* writing doesn't alter the bound, straightforward *) @cthulhu ]
    1354 qed.
     1560| *: (* writing doesn't alter the bound, straightforward *) @cthulhu  ]
     1561qed. (* TODO *)
    13551562
    13561563(* ------------------------------------------------------------------------- *)
     
    18822089] qed.
    18832090
    1884 
    1885 (* /!\ Here is the source of all sadness (op = lt) /!\ *)
    1886 axiom cmp_offset_translation : ∀op,delta,x,y.
    1887    cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
    1888 
    1889 (* 5 Nov. 2012 : the rest of the stuff doesn't checks anymore. Not a big deal, it was here
    1890  * for historical purposes, and for potential inspiration for Clight to Cminor. I leave the
    1891  * code commented for future reference.
    1892  *)
    1893 
    1894 (*
     2091(* /!\ Warning TODO Warning /!\ *)
     2092
     2093(* Note that x and y are bounded below and above, similarly for the shifted offsets.
     2094   This is enough to prove that there is no "wrap-around-the-end" problem,
     2095   /provided we know that the block bounds are implementable by 2^16 bitvectors/.
     2096   We axiomatize it for now. Notice that this axiom is in fact not provable and implies False.
     2097   In order to be true, we need to prove that the (x+delta) and (y+delta) do not overflow.
     2098   This is provable from the fact that the original pointers in which the offsets reside are "valid".
     2099   This in turn is ensured by the memory injection.
     2100   /DO NOT USE IT ELSEWHERE, this is just a temporary stopgap./ *)
     2101axiom cmp_offset_translation :
     2102  ∀op,delta,x,y.
     2103  (Zoo x) + (Zoo delta) < Z_two_power_nat 16 →
     2104  (Zoo y) + (Zoo delta) < Z_two_power_nat 16 →
     2105  cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
     2106
     2107(* TODO: move in frontend_misc *)
     2108lemma Zlt_to_Zneq : ∀x,y:Z. x < y → x ≠ y.
     2109#x #y /3 by absurd, nmk/
     2110qed.
     2111
     2112lemma Zlt_translate : ∀x,y,delta:Z. x < y → x + delta < y + delta.
     2113#x #y #delta /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle/
     2114qed.
     2115
     2116lemma Zlt_weaken : ∀x,y,delta:Z. delta ≥ 0 → x < y → x < y + delta.
     2117#x #y #delta cases delta try // #p
     2118[ 2: #Habsurd @(False_ind … Habsurd) ]
     2119/3 by Zlt_to_Zle_to_Zlt, Zplus_le_pos/
     2120qed.
     2121
     2122lemma Zlt_sum_weaken : ∀a,a',b,c:Z. a+b < c → a' < a → a'+b < c.
     2123#a #a' #b #c /3 by transitive_Zlt, Zlt_translate/ qed.
     2124
     2125(* TODO: move in frontend_misc. This axiom states that for small bitvectors, bitvector addition
     2126 * commutes with conversion to Z, i.e. there is no overflow. *)
     2127axiom Z_addition_bv_commute :
     2128  ∀n. ∀v1,v2:BitVector n.
     2129        (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2) < Z_two_power_nat n →
     2130        Z_of_unsigned_bitvector ? (addition_n ? v1 v2) =
     2131        (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2).
     2132
     2133lemma valid_pointer_of_implementable_block_is_implementable :
     2134  ∀m,b.
     2135    block_implementable_bv m b →
     2136    ∀o. valid_pointer m (mk_pointer b o) = true →
     2137        Zoo o < Z_two_power_nat 16.
     2138#m #b whd in ⊢ (% → ?); * #Hlow #Hhigh
     2139* #o #Hvalid cases (valid_pointer_to_Prop … Hvalid) * #_
     2140#Hlow' #Hhigh'
     2141cases Hlow -Hlow #Hlow0 #Hlow16
     2142cases Hhigh -Hhigh #Hhigh0 #Hhigh16
     2143whd in match (Zoo ?);
     2144@(transitive_Zlt … Hhigh' Hhigh16)
     2145qed.
     2146
    18952147lemma cmp_value_eq :
    18962148  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
    18972149   value_eq E v1 v2 →
    18982150   value_eq E v1' v2' →
    1899    memory_inj E m1 m2 →   
    1900    ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1
     2151   memory_inj E m1 m2 →
     2152   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1 
    19012153           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
    19022154#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
     
    19062158[ 1: #tsz #tsg
    19072159     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
    1908      [ 1: #v #Habsurd destruct (Habsurd)
    1909      | 3: #f #Habsurd destruct (Habsurd)
    1910      | 4: #Habsurd destruct (Habsurd)
    1911      | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
     2160     [ 1: #Habsurd destruct (Habsurd)
     2161     | 3: #Habsurd destruct (Habsurd)
     2162     | 4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
    19122163     #sz #i
    19132164     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1914      [ 1: #v #Habsurd destruct (Habsurd)
    1915      | 3: #f #Habsurd destruct (Habsurd)
    1916      | 4: #Habsurd destruct (Habsurd)
    1917      | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
     2165     [ 1: #Habsurd destruct (Habsurd)
     2166     | 3: #Habsurd destruct (Habsurd)
     2167     | 4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
    19182168     #sz' #i' cases tsg normalize nodelta
    19192169     @intsize_eq_elim_elim
     
    19242174            | 2: cases (cmpu_int ????) whd in match (of_bool ?); ]
    19252175              /3 by ex_intro, conj, vint_eq/ ]
    1926 | 3: #fsz
     2176| 3: #ty1 #ty2 #Habsurd destruct (Habsurd)
     2177| 2: lapply Hinj -Hinj
     2178     generalize in match (mk_mem contmap1 ??); #m1
     2179     generalize in match (mk_mem contmap2 ??); #m2
     2180     #Hinj #optn #typ
    19272181     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
    1928      [ 1: #v #Habsurd destruct (Habsurd)
     2182     [ 1: #Habsurd destruct (Habsurd)
    19292183     | 2: #sz #i #Habsurd destruct (Habsurd)
    1930      | 4: #Habsurd destruct (Habsurd)
    1931      | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
    1932      #f
     2184     | 4: #p1 #p2 #Hembed ]
    19332185     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1934      [ 1: #v #Habsurd destruct (Habsurd)
    1935      | 2: #sz #i #Habsurd destruct (Habsurd)
    1936      | 4: #Habsurd destruct (Habsurd)
    1937      | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
    1938      #f'
    1939      #Heq destruct (Heq) cases (Fcmp op f f')
    1940      /3 by ex_intro, conj, vint_eq/
    1941 | 4: #ty1 #ty2 #Habsurd destruct (Habsurd)
    1942 | 2: #optn #typ
    1943      @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
    1944      [ 1: #v #Habsurd destruct (Habsurd)
    1945      | 2: #sz #i #Habsurd destruct (Habsurd)
    1946      | 3: #f #Habsurd destruct (Habsurd)
    1947      | 5: #p1 #p2 #Hembed ]
    1948      @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    1949      [ 1,6: #v #Habsurd destruct (Habsurd)
    1950      | 2,7: #sz #i #Habsurd destruct (Habsurd)
    1951      | 3,8: #f #Habsurd destruct (Habsurd)
    1952      | 5,10: #p1' #p2' #Hembed' ]
     2186     [ 1,5: #Habsurd destruct (Habsurd)
     2187     | 2,6: #sz #i #Habsurd destruct (Habsurd)
     2188     | 4,8: #q1 #q2 #Hembed' ]
    19532189     [ 2,3: cases op whd in match (sem_cmp_mismatch ?);
    19542190          #Heq destruct (Heq)
     
    19592195          [ 2,4: %{Vfalse} @conj try @refl @vint_eq
    19602196          | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ]
    1961      lapply (mi_valid_pointers … Hinj p1' p2')
    1962      lapply (mi_valid_pointers … Hinj p1 p2)         
    1963      cases (valid_pointer (mk_mem ???) p1')
    1964      [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    1965      cases (valid_pointer (mk_mem ???) p1)
    1966      [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    1967      #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
    1968      >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
    1969      elim p1 in Hembed; #b1 #o1
    1970      elim p1' in Hembed'; #b1' #o1'
     2197     #Hvalid
     2198     lapply (if_opt_inversion ???? Hvalid) -Hvalid * #Hconj
     2199     lapply (andb_inversion … Hconj) -Hconj * #Hvalid #Hvalid'
     2200     lapply (mi_valid_pointers … Hinj q1 q2 Hvalid' Hembed') #Hvalid2' >Hvalid2'
     2201     lapply (mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) #Hvalid2 >Hvalid2
     2202     normalize nodelta
     2203(*   >(mi_valid_pointers … Hinj p1' p2' Hvalid' Hembed')
     2204     >(mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) normalize nodelta *)
     2205     elim p1 in Hvalid Hembed; #bp1 #op1
     2206     elim q1 in Hvalid' Hembed'; #bq1 #oq1
     2207     #Hvalid' #Htmp #Hvalid lapply Htmp -Htmp
    19712208     whd in match (pointer_translation ??);
    19722209     whd in match (pointer_translation ??);
    1973      @(eq_block_elim … b1 b1')
    1974      [ 1: #Heq destruct (Heq)
    1975           cases (E b1') normalize nodelta
    1976           [ 1: #Habsurd destruct (Habsurd) ]
    1977           * #eb1' #eo1' normalize nodelta
     2210     @(eq_block_elim … bp1 bq1)
     2211     [ 1: #Heq destruct (Heq) normalize nodelta
     2212          lapply (mi_nowrap … Hinj bq1)
     2213          whd in ⊢ (% → ?);
     2214          cases (E bq1) normalize nodelta
     2215          [ #_ #Habsurd destruct ]
     2216          * #BLO #OFF normalize nodelta * *         
     2217          #Hbq1_implementable #HBLO_implementable #Hno_wrap
    19782218          #Heq1 #Heq2 #Heq3 destruct
    19792219          >eq_block_b_b normalize nodelta
    1980           <cmp_offset_translation
    1981           cases (cmp_offset ???) normalize nodelta         
    1982           /3 by ex_intro, conj, vint_eq/
    1983      | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
    1984           cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    1985           * #eb1 #eo1
    1986           cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
    1987           * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
    1988           lapply (H ???? Hneq (refl ??) (refl ??))
    1989           #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
    1990           elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
    1991           /3 by ex_intro, conj, vint_eq/
    1992      ]
    1993 ] qed.    *)           
    1994 
    1995 (*
    1996 lemma binary_operation_value_eq :
    1997   ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
    1998    value_eq E v1 v2 →
    1999    value_eq E v1' v2' →
    2000    memory_inj E m1 m2 →
    2001    ∀r1.
    2002    sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
    2003    ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
    2004 #E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
    2005 cases op
    2006 whd in match (sem_binary_operation ??????);
    2007 whd in match (sem_binary_operation ??????);
    2008 [ 1: @add_value_eq try assumption
    2009 | 2: @sub_value_eq try assumption
    2010 | 3: @mul_value_eq try assumption
    2011 | 4: @div_value_eq try assumption
    2012 | 5: @mod_value_eq try assumption
    2013 | 6: @and_value_eq try assumption
    2014 | 7: @or_value_eq try assumption
    2015 | 8: @xor_value_eq try assumption
    2016 | 9: @shl_value_eq try assumption
    2017 | 10: @shr_value_eq try assumption
    2018 | *: @cmp_value_eq try assumption
    2019 ] qed. *)
    2020 
    2021 (*
    2022 lemma cast_value_eq :
    2023  ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 →
    2024   ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res →
    2025   ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'.
    2026 #E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res
    2027 @(value_eq_inversion … Hvalue_eq)
    2028 [ 1: #v normalize #Habsurd destruct (Habsurd)
    2029 | 2: #vsz #vi whd in match (exec_cast ????);
    2030      cases ty
    2031      [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
    2032      normalize nodelta
    2033      [ 1,3,7,8,9: #Habsurd destruct (Habsurd)
    2034      | 2: @intsize_eq_elim_elim
    2035           [ 1: #Hneq #Habsurd destruct (Habsurd)
    2036           | 2: #Heq destruct (Heq) normalize nodelta
    2037                cases cast_ty
    2038                [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
    2039                | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
    2040                normalize nodelta
    2041                [ 1,7,8,9: #Habsurd destruct (Habsurd)
    2042                | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
    2043                | 3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/
    2044                | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
    2045                     @eq_bv_elim
    2046                     [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta
    2047                          whd in match (m_bind ?????);
    2048                          #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
    2049                     | 2,4,6: #Hneq >eq_intsize_identity normalize nodelta
    2050                          whd in match (m_bind ?????);
    2051                          #Habsurd destruct (Habsurd) ] ]
    2052           ]
    2053      | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
    2054           @eq_bv_elim
    2055           [ 1,3,5: #Heq destruct (Heq) normalize nodelta
    2056                whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
    2057           | 2,4,6: #Hneq normalize nodelta
    2058                whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ]
    2059      ]
    2060 | 3: #f whd in match (exec_cast ????);
    2061      cases ty
    2062      [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
    2063      | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
    2064      normalize nodelta
    2065      [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
    2066      cases cast_ty
    2067      [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
    2068      | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
    2069      normalize nodelta
    2070      [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
    2071      #Heq destruct (Heq)
    2072      [ 1: /3 by ex_intro, conj, vint_eq/
    2073      | 2: /3 by ex_intro, conj, vfloat_eq/ ]
    2074 | 4: whd in match (exec_cast ????);
    2075      cases ty
    2076      [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
    2077      | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
    2078      normalize
    2079      [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
    2080      cases cast_ty normalize nodelta
    2081      [ 1,10,19: #Habsurd destruct (Habsurd)
    2082      | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
    2083      | 3,12,21: #cfl #Habsurd destruct (Habsurd)
    2084      | 4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
    2085      | 5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
    2086      | 6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
    2087      | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
    2088      | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
    2089      | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
    2090 | 5: #p1 #p2 #Hembed whd in match (exec_cast ????);
    2091      cases ty
    2092      [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
    2093      | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
    2094      normalize
    2095      [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
    2096      cases cast_ty normalize nodelta
    2097      [ 1,10,19: #Habsurd destruct (Habsurd)
    2098      | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
    2099      | 3,12,21: #cfl #Habsurd destruct (Habsurd)
    2100      | 4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption
    2101      | 5,14,23: #carrayty #cn #Heq destruct (Heq)
    2102                 %{(Vptr p2)} @conj try @refl @vptr_eq assumption
    2103      | 6,15,24: #ctl #cretty #Heq destruct (Heq)
    2104                 %{(Vptr p2)} @conj try @refl @vptr_eq assumption
    2105      | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
    2106      | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
    2107      | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
    2108 qed.
    2109 
    2110 lemma bool_of_val_value_eq :
    2111  ∀E,v1,v2. value_eq E v1 v2 →
    2112    ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b.
    2113 #E #v1 #v2 #Hvalue_eq #ty #b
    2114 @(value_eq_inversion … Hvalue_eq) //
    2115 [ 1: #v #H normalize in H; destruct (H)
    2116 | 2: #p1 #p2 #Hembed #H @H ] qed.
    2117 
    2118 *)
    2119 (*
    2120 lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
    2121   ∀E:embedding.
    2122   ∀Hext:memory_ext E m1 m2.
    2123   switch_removal_globals E ? fundef_switch_removal ge ge' →
    2124   disjoint_extension en1 m1 en2 m2 ext E Hext →
    2125   ext_fresh_for_genv ext ge →
    2126   (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
    2127   (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
    2128 #ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
    2129 @expr_lvalue_ind_combined
    2130 [ 1: #csz #cty #i #a1
    2131      whd in match (exec_expr ????); elim cty
    2132      [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    2133      normalize nodelta
    2134      [ 2: cases (eq_intsize csz sz) normalize nodelta
    2135           [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
    2136           | 2: #Habsurd destruct (Habsurd) ]
    2137      | 4,5,6: #_ #H destruct (H)
    2138      | *: #H destruct (H) ]
    2139 | 2: #ty #fl #a1
    2140      whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
    2141 | 3: *
    2142   [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    2143   | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
    2144   #ty whd in ⊢ (% → ?); #Hind try @I
    2145   whd in match (Plvalue ???);
    2146   [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
    2147        cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
    2148        [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    2149        | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
    2150            elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
    2151            #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
    2152            whd in match (load_value_of_type' ???);
    2153            whd in match (load_value_of_type' ???);
    2154            lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
    2155            cases (load_value_of_type ty m1 bl1 o1)
    2156            [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
    2157            | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
    2158                     elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
    2159                     normalize /4 by ex_intro, conj/
    2160   ] ] ]
    2161 | 4: #v #ty whd * * #b1 #o1 #tr1
    2162      whd in match (exec_lvalue' ?????);
    2163      whd in match (exec_lvalue' ?????);
    2164      lapply (Hdisjoint v)
    2165      lapply (Hext_fresh_for_genv v)
    2166      cases (mem_assoc_env v ext) #Hglobal
    2167      [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
    2168           >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
    2169           >(Hglobal (refl ??)) normalize
    2170           #Habsurd destruct (Habsurd)
    2171      | 2: normalize nodelta
    2172           cases (lookup ?? en1 v) normalize nodelta
    2173           [ 1: #Hlookup2 >Hlookup2 normalize nodelta
    2174                lapply (rg_find_symbol … Hrelated v)
    2175                cases (find_symbol ???) normalize
    2176                [ 1: #_ #Habsurd destruct (Habsurd)
    2177                | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
    2178                     [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
    2179                     | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
    2180                          %{〈block',mk_offset (zero offset_size),[]〉} @conj try @refl
    2181                          normalize /2/
    2182                 ] ]
    2183          | 2: #block
    2184               cases (lookup ?? en2 v) normalize nodelta
    2185               [ 1: #Hfalse @(False_ind … Hfalse)
    2186               | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
    2187                    %{〈b, zero_offset, E0〉} @conj try @refl
    2188                    normalize /2/
    2189     ] ] ]
    2190 | 5: #e #ty whd in ⊢ (% → %);
    2191      whd in match (exec_lvalue' ?????);
    2192      whd in match (exec_lvalue' ?????);
    2193      cases (exec_expr ge en1 m1 e)
    2194      [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
    2195           * elim v1 normalize nodelta
    2196           [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
    2197           | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
    2198           | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
    2199           | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
    2200           | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
    2201                >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
    2202                #Hvalue_eq normalize
    2203                cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    2204                * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
    2205                * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
    2206                %{〈b2,mk_offset (addition_n ? (offv o1') (offv o2')),tr1''〉} @conj try @refl
    2207                normalize @conj // ]
    2208      | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
    2209 | 6: #ty #e #ty'
    2210      #Hsim @(exec_lvalue_expr_elim … Hsim)
    2211      cases ty
    2212      [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    2213      * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
    2214      #tr #H @conj try @refl try assumption
    2215 | 7: #ty #op #e
    2216      #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
    2217      lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
    2218      cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
    2219      [ 1: #_ @I
    2220      | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
    2221            normalize /2/ ]
    2222 | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2
    2223      @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
    2224      cases (exec_expr ge en1 m1 e2) in Hsim2;
    2225      [ 2: #error // ]
    2226      * #val #trace normalize in ⊢ (% → ?); #Hsim2
    2227      elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec2
    2228      whd in match (m_bind ?????); whd in match (m_bind ?????);
    2229      lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext))
    2230      cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1)
    2231      [ 1: #_ // ]
    2232      #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq  #Hvalue_eq_opval
    2233      >Hopval_eq normalize destruct /2 by conj/
    2234 | 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
    2235      #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty)
    2236      cases (exec_cast m1 v1 (typeof e) cast_ty)
    2237      [ 2: #error #_ normalize @I
    2238      | 1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????);
    2239           * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta
    2240           @conj // ]
    2241 | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
    2242      @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
    2243      lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1))
    2244      cases (exec_bool_of_val ? (typeof e1)) #b
    2245      [ 2: #_ normalize @I ]
    2246      #H lapply (H ? (refl ??)) #Hexec >Hexec normalize
    2247      cases b normalize nodelta
    2248      [ 1: (* true branch *)
    2249           cases (exec_expr ge en1 m1 e2) in Hsim2;
    2250           [ 2: #error normalize #_ @I
    2251           | 1: * #e2v #e2tr normalize #H elim (H ? (refl ??))
    2252                * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize
    2253                     destruct @conj try // ]
    2254      | 2: (* false branch *)
    2255           cases (exec_expr ge en1 m1 e3) in Hsim3;
    2256           [ 2: #error normalize #_ @I
    2257           | 1: * #e3v #e3tr normalize #H elim (H ? (refl ??))
    2258                * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize
    2259                destruct @conj // ] ]
    2260 | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2
    2261      @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq
    2262      lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1))     
    2263      cases (exec_bool_of_val v1 (typeof e1))
    2264      [ 2,4:  #error #_ normalize @I ]
    2265      #b cases b #H lapply (H ? (refl ??)) #Heq >Heq
    2266      whd in match (m_bind ?????);
    2267      whd in match (m_bind ?????);
    2268      [ 2,3: normalize @conj try @refl try @vint_eq ]
    2269      cases (exec_expr ge en1 m1 e2) in Hsim2;
    2270      [ 2,4: #error #_ normalize @I ]
    2271      * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??))
    2272      * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta
    2273      lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2))
    2274      cases (exec_bool_of_val v2 (typeof e2))
    2275      [ 2,4: #error #_ normalize @I ]
    2276      #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta
    2277      destruct @conj try @conj //
    2278      cases b2 whd in match (of_bool ?); @vint_eq
    2279 | 13: #ty #ty' cases ty
    2280      [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n
    2281      | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    2282      whd in match (exec_expr ????); whd
    2283      * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉}
    2284      @conj try @refl @conj //
    2285 | 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta
    2286     whd in match (exec_lvalue' ?????);
    2287     whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty);
    2288     whd in match (typeof ?);
    2289     cases aggregty in Hsim;
    2290     [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n'
    2291     | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ]
    2292     normalize nodelta #Hsim
    2293     [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ]
    2294     whd in match (m_bind ?????);
    2295     whd in match (m_bind ?????);
    2296     whd in match (exec_lvalue ge en1 m1 (Expr ed ?));
    2297     cases (exec_lvalue' ge en1 m1 ed ?) in Hsim;
    2298     [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    2299     * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??))
    2300     * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq
    2301     whd in match (exec_lvalue ????); >Hexec normalize nodelta
    2302     [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj //
    2303          normalize @conj // ]
    2304     cases (field_offset i fl')
    2305     [ 2: #error normalize #Habsurd destruct (Habsurd) ]
    2306     #offset whd in match (m_bind ?????); #Heq destruct (Heq)
    2307     whd in match (m_bind ?????);
    2308     %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj
    2309     destruct // normalize nodelta @conj try @refl @vptr_eq
    2310     -H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq
    2311     whd in match (pointer_translation ??);     
    2312     whd in match (pointer_translation ??);
    2313     cases (E b)
    2314     [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
    2315     * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq)
    2316     cut (offset_plus (mk_offset (addition_n offset_size
    2317                                       (offv o1)
    2318                                       (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 offset)))) o'
    2319           = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset)))
    2320     [ whd in match (shift_offset ???) in ⊢ (???%);
    2321       whd in match (offset_plus ??) in ⊢ (??%%);
    2322       /3 by associative_addition_n, commutative_addition_n, refl/ ]
    2323     #Heq >Heq @refl
    2324 | 15: #ty #l #e #Hsim
    2325      @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq normalize nodelta @conj //
    2326 | 16: *
    2327   [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    2328   | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
    2329   #ty normalize in ⊢ (% → ?);
    2330   [ 3,4,13: @False_ind
    2331   | *: #_ normalize #a1 #Habsurd destruct (Habsurd) ]
    2332 ] qed. *)
     2220          lapply (cmp_offset_translation op OFF op1 oq1 ??)
     2221          [ @(Zlt_sum_weaken … Hno_wrap)
     2222            cases (valid_pointer_to_Prop … Hvalid') * #_ #_ try //
     2223          | @(Zlt_sum_weaken … Hno_wrap)
     2224            cases (valid_pointer_to_Prop … Hvalid) * #_ #_ try // ]
     2225          #Heq <Heq
     2226          cases (cmp_offset op op1 oq1)
     2227          normalize nodelta
     2228          try /3 by ex_intro, conj, refl, vint_eq/
     2229     | 2: #Hneq lapply (mi_nonalias … Hinj bp1 bq1)
     2230          normalize nodelta
     2231          lapply (mi_nowrap … Hinj bp1) whd in ⊢ (% → ?);
     2232          lapply (mi_nowrap … Hinj bq1) whd in ⊢ (% → ?);
     2233          cases (E bq1) [ 1: #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
     2234          * #BLOq #DELTAq normalize nodelta
     2235          cases (E bp1) [ 1: #_ #_ #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
     2236          * #BLOp #DELTAp normalize nodelta #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
     2237          cases op
     2238          whd in ⊢ ((??%?) → ?); #H' destruct (H')
     2239          whd in match (sem_cmp_mismatch ?);
     2240          lapply (H ???? Hneq (refl ??) (refl ??)) -H
     2241          cases (block_decidable_eq BLOp BLOq) normalize nodelta
     2242          #H
     2243          [ 2: #_ >(not_eq_block … H) normalize nodelta %{Vfalse} @conj try @refl %2
     2244          | 4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ]         
     2245          destruct (H) generalize in match BLOq in Hnowrap1 Hnowrap2 Hvalid2 Hvalid2' ⊢ %;
     2246          #target_block * * #Himplq1 #Himpltarget #Hnowrap_q1
     2247          * * #Himplp1 #_ #Hnowrap_p1 #Hvalid2 #Hvalid2'
     2248          lapply (valid_pointer_to_Prop … Hvalid)
     2249          lapply (valid_pointer_to_Prop … Hvalid')
     2250          * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp
     2251          >eq_block_b_b normalize nodelta
     2252          *
     2253          #Hdisjoint
     2254          whd in match (cmp_offset); normalize nodelta
     2255          whd in match (eq_offset); normalize nodelta
     2256          whd in match (offset_plus ??);
     2257          whd in match (offset_plus ??);
     2258          lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2)
     2259          lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2')
     2260          #Himpl1 #Himpl2
     2261          [ 1,3:
     2262              (* We show the non-equality of the rhs by exhibiting disjointness of blocks. This is made
     2263               * painful by invariants on non-overflowing offsets. We exhibit [a]+[b] < [c]+[d], then
     2264               * cut [a+b]<[c+d] (using a subcut for needed consistency hypotheses) and conclude easily
     2265               * [a+b] ≠ [c+d]. *)
     2266              cut ((Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp))
     2267                   < (Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq)))
     2268              [ 1,3:
     2269                @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bp1 + Zoo DELTAp) ?)
     2270                [ 1,3: @Zlt_translate assumption
     2271                | 2,4: @(transitive_Zle ? (low_bound m1 bq1+Zoo DELTAq) ?) try assumption
     2272                       @monotonic_Zle_Zplus_l try assumption ]
     2273              ]
     2274              #Hlt_stepA
     2275              cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp))
     2276                   < Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq)))
     2277              [ 1,3:
     2278                >Z_addition_bv_commute
     2279                [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ]
     2280                >Z_addition_bv_commute
     2281                [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ]
     2282                try assumption ] -Hlt_stepA
     2283           | 2,4:
     2284              cut ((Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq))
     2285                   < (Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp)))
     2286              [ 1,3:
     2287                @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bq1 + Zoo DELTAq) ?)
     2288                [ 1,3: @Zlt_translate assumption
     2289                | 2,4: @(transitive_Zle ? (low_bound m1 bp1+Zoo DELTAp) ?) try assumption
     2290                       @monotonic_Zle_Zplus_l try assumption ]
     2291              ]
     2292              #Hlt_stepA
     2293              cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq))
     2294                   < Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp)))
     2295              [ 1,3:
     2296                >Z_addition_bv_commute
     2297                [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ]
     2298                >Z_addition_bv_commute
     2299                [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ]
     2300                try assumption ] -Hlt_stepA
     2301            ]
     2302            generalize in match (addition_n ? (offv op1) ?); #lhs
     2303            generalize in match (addition_n ? (offv oq1) ?); #rhs
     2304            #Hlt_stepB lapply (Zlt_to_Zneq … Hlt_stepB)
     2305            @(eq_bv_elim … lhs rhs)
     2306            [ 1,3,5,7: #Heq destruct * #H @(False_ind … (H (refl ??)))
     2307            | 2,4,6,8: #Hneq #_ /3 by ex_intro, conj, vint_eq/ ]
     2308    ]
     2309] qed.
     2310   
  • src/Clight/toCminorCorrectness.ma

    r2572 r2578  
    10531053qed.
    10541054
     1055(*
    10551056lemma pointer_translation_cmp_offset :
    10561057  ∀E,p1,p2,p1',p2',op.
     
    10711072| @cthulhu (* !!!! TODO !!!! *)
    10721073| @cthulhu (* !!!! TODO !!!! *)
    1073 ] qed.
     1074] qed. *)
    10741075
    10751076(* The two following lemmas are just noise. *)
     
    11301131      (we might wrap up the rhs and end SNAFU).
    11311132 *)
     1133 
    11321134lemma eval_expr_sim :
    1133   ∀(inv:clight_cminor_inv).
    1134   ∀(f:function).
    1135   ∀(vars:var_types).
    1136   ∀stacksize.
    1137   characterise_vars (globals inv) f = 〈vars, stacksize〉 →
    1138   ∀(cl_env:cl_env).
    1139   (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
    1140   ∀(cl_m:mem).
    1141   ∀(cm_env:cm_env).
    1142   ∀(sp:block).
    1143   ∀(cm_m:mem).
    1144   ∀E:embedding.
    1145   ∀minj:memory_inj E cl_m cm_m.
    1146   memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
     1135  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
     1136  ∀cl_cm_inv  : clight_cminor_inv.
     1137  (* current function (defines local environment) *)
     1138  ∀f          : function.
     1139  (* [alloctype] maps variables to their allocation type (global, stack, register) *)
     1140  ∀alloctype  : var_types.
     1141  ∀stacksize  : ℕ.
     1142  ∀alloc_hyp  : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
     1143  (* environments *)
     1144  ∀cl_env     : cl_env.
     1145  ∀cm_env     : cm_env.
     1146  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
     1147  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
     1148  (* CL and CM memories *)
     1149  ∀cl_m       : mem.
     1150  ∀cm_m       : mem.
     1151  (* memory injection and matching *)
     1152  ∀embed      : embedding.
     1153  ∀injection  : memory_inj embed cl_m cm_m.
     1154  ∀stackptr   : block.
     1155  ∀matching   : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
    11471156  (* clight expr to cminor expr *)
    11481157  (∀(e:expr).
    11491158   ∀(e':CMexpr (typ_of_type (typeof e))).
    11501159   ∀Hexpr_vars.
    1151    translate_expr vars e = OK ? («e', Hexpr_vars») →
     1160   translate_expr alloctype e = OK ? («e', Hexpr_vars») →
    11521161   ∀cl_val,trace,Hyp_present.
    1153    exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
    1154    ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
    1155             value_eq E cl_val cm_val) ∧
     1162   exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
     1163   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
     1164            value_eq embed cl_val cm_val) ∧
    11561165   (* clight /lvalue/ to cminor /expr/ *)
    11571166  (∀ed,ty.
    11581167   ∀(e':CMexpr ASTptr).
    11591168   ∀Hexpr_vars.
    1160    translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
     1169   translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
    11611170   ∀cl_blo,cl_off,trace,Hyp_present.
    1162    exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
    1163    ∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
    1164             value_eq E (Vptr (mk_pointer cl_blo cl_off)) cm_val).
    1165 #inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching
     1171   exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
     1172   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
     1173            value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).
     1174#inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
    11661175@expr_lvalue_ind_combined
    11671176[ 7: (* binary ops *)
     
    16261635            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
    16271636            * #Hyp_present_lhs #Hyp_present_rhs
    1628             #Hind_rhs #Hind_lhs                        
     1637            #Hind_rhs #Hind_lhs
    16291638            lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
    16301639            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     
    16671676            lapply (opt_to_res_inversion ???? Hsem) -Hsem
    16681677            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
    1669             #Hsem_cmp lapply (sem_cmp_ptr_inversion … Hsem_cmp) -Hsem_cmp
     1678            #Hsem_cmp (* cut > *)
     1679            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
     1680            * #Hyp_present_lhs #Hyp_present_rhs
     1681            #Hind_rhs #Hind_lhs
     1682            lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
     1683            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1684            lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
     1685            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
     1686            lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp)
     1687            -Hvalue_eq_lhs -Hvalue_eq_rhs
     1688            * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res %{cm_val} @conj try assumption
     1689            lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm -Hsem_cmp
    16701690            *
    16711691            [ 2,4,6,8,10,12:
     
    16791699                | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct
    16801700            ] ] ]
    1681            
    1682 (*            #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %); *)
    1683             #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
    1684             * #Hyp_present_lhs #Hyp_present_rhs
    1685             #Hind_rhs #Hind_lhs
    1686             lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
    1687             * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
    1688             lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
    1689             * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    16901701            whd in match (eval_expr ???????);
    16911702            whd in match (eval_expr ???????);
     1703            whd in Hsem_cmp:(??%?);
     1704            destruct (Hsem_cmp)                       
    16921705            >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
    16931706            >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
    16941707            whd in match (m_bind ?????);
    1695             -Heval_lhs -Heval_rhs -Hyp_present_rhs -Hyp_present_lhs
    1696             -Hexpr_vars_lhs -Hexpr_vars_rhs
    16971708            whd in match (eval_binop ???????);
    1698             [ 1,2,3,4,5,6:
    1699               whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)           
    1700               >(value_eq_null_inversion … Hvalue_eq_lhs)
    1701               >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta
    1702               whd in match (eval_unop ????);
    1703               whd in match (opt_to_res ???);
    1704               whd in match (m_bind ?????);
    1705               (* same glitch with integer widths *)
     1709            [ 1,2,3,4,5,6:
     1710              (* qed modulo integer width glitch *)
    17061711              @cthulhu
    1707             | 7,8,9,10,11,12:
    1708               whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
    1709               >(value_eq_null_inversion … Hvalue_eq_lhs) normalize nodelta
    1710               cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2'
    1711               * #Hcm_rhs_val #Hpointer_translation >Hcm_rhs_val normalize nodelta
    1712               whd in match (eval_unop ????);
    1713               whd in match (opt_to_res ???);
    1714               whd in match (m_bind ?????);
    1715               (* same glitch with integer widths *)
    1716               @cthulhu
    1717             | 13,14,15,16,17,18:
    1718               whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
    1719               >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta
    1720               cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1'
    1721               * #Hcm_lhs_val #Hpointer_translation >Hcm_lhs_val normalize nodelta
    1722               whd in match (eval_unop ????);
    1723               whd in match (opt_to_res ???);
    1724               whd in match (m_bind ?????);
    1725               (* same glitch with integer widths *)
    1726               @cthulhu
    1727             | *:
    1728               cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1' * #Hcm_lhs #Hptr_translation_lhs
    1729               cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2' * #Hcm_rhs #Hptr_translation_rhs
    1730               destruct (Hcm_lhs Hcm_rhs) normalize nodelta
    1731               -Hvalue_eq_lhs -Hvalue_eq_rhs -Hexec_lhs -Hexec_rhs
    1732               >(mi_valid_pointers … Hinj … Hvalid_p1 … Hptr_translation_lhs)
    1733               >(mi_valid_pointers … Hinj … Hvalid_p2 … Hptr_translation_rhs) normalize nodelta
    1734               lapply Heq_block_outcome -Heq_block_outcome
    1735               @(match eq_block (pblock p1) (pblock p2)
    1736                 return λb. (eq_block (pblock p1) (pblock p2)) = b → ?
    1737                 with
    1738                 [ true ⇒ λH. ?
    1739                 | false ⇒ λH. ?
    1740                 ] (refl ? (eq_block (pblock p1) (pblock p2)))) normalize nodelta
    1741               [ 1,3,5,7,9,11:
    1742                  (* block equality in the Clight memory *)
    1743                  (* entails block equality in the Cminor memory *)
    1744                  >(pointer_translation_eq_block … Hptr_translation_lhs Hptr_translation_rhs H) normalize nodelta                 
    1745                  #Hsem_cmp whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
    1746                  whd in match (eval_unop ????);
    1747                  whd in match (opt_to_res ???);
    1748                  whd in match (m_bind ?????);
    1749                  (* TODO !!! In order to finish this, we need an invariant on the fact that we don't blow the stack during
    1750                   * transformation *)
    1751                  @cthulhu
    1752               | *: (* TBF. In the case of block inequality, we will have to use the no_aliasing property of the memory injection. *)
    1753                  @cthulhu
    1754               ]
    1755             ]
     1712            | *: >Hvalid_p1 >Hvalid_p2 normalize nodelta
     1713                 lapply Heq_block_outcome -Heq_block_outcome
     1714                 @(eq_block_elim … (pblock p1) (pblock p2))
     1715                 normalize nodelta
     1716                 [ 1,3,5,7,9,11:
     1717                   #Hbocks_eq #Heq_cmp destruct (Heq_cmp)
     1718                   whd in match (eval_unop ????);
     1719                   whd in match (m_bind ?????);
     1720                   cases (cmp_offset ???) normalize nodelta
     1721                   (* glitch *)
     1722                   @cthulhu
     1723                 | *:
     1724                   #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     1725                   whd in match (eval_unop ????);
     1726                   whd in match (m_bind ?????);
     1727                   @cthulhu
     1728                 ]
     1729           ]
    17561730       ]
    1757  ]
    1758      
     1731    ]
     1732
    17591733| 1: (* Integer constant *)
    17601734  #csz #ty cases ty
Note: See TracChangeset for help on using the changeset viewer.