Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (7 years ago)
Author:
garnier
Message:

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2600 r2608  
    33include "Clight/frontend_misc.ma".
    44
    5 (* This file contains some definitions and lemmas related to memory injections.
    6    Could be useful for the Clight → Cminor. Needs revision: the definitions are
    7    too lax and allow inconsistent embeddings (more precisely, these embeddings do
    8    not allow to prove that the semantics for pointer less-than comparisons is
    9    conserved). *)
    10 
     5(* This file contains some definitions and lemmas related to memory injections. 
     6 * The whole development is quite similar to the one described in the article by
     7 * Leroy & Blazy in J.A.R., except that in Cerco, we describe data down to the byte
     8 * level (similar to the memory model of CompCert v2 but not to the aforementioned
     9 * paper).
     10 * *)
    1111
    1212(* --------------------------------------------------------------------------- *)   
     
    2929
    3030lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
     31
     32lemma eqZb_symmetric : ∀x,y:Z. eqZb x y = eqZb y x.
     33#x #y @(eqZb_elim … x y)
     34[ * >eqZb_z_z @refl
     35| #Hneq >(eqZb_false … (sym_neq ??? Hneq)) @refl ]
     36qed.
    3137
    3238(* --------------------------------------------------------------------------- *)
     
    6066qed.
    6167
     68
    6269lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
    63 #a #b @(eq_block_elim … a b) /2/ qed.
     70* #a * #b
     71cases (decidable_eq_Z … a b)
     72[ * %1 @refl
     73| #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed.
    6474
    6575lemma block_decidable_eq : ∀a,b:block. (a = b) + (a ≠ b).
    66 * #ra #ida * #rb #idb
    67 cases 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.
     76* #a * #b
     77cases (decidable_eq_Z_Type … a b)
     78[ * %1 @refl
     79| #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed.
    7480
    7581lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
     
    8288        [ 1: #Heq >Heq /2 by not_to_not/
    8389        | 2: #x @x ]
    84    | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
     90   | 2: #Hmem1 cases (mem_dec ? block_eq_dec ? tl)
    8591        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
    8692        | 2: #Hmem2 @Hind //
     
    103109   pblock ptr ≠ b →
    104110   valid_pointer (free m b) ptr = true.
    105 * #br #bid * #contents #next #posnext * * #pbr #pbid #poff
     111* (* #br *) #bid * #contents #next #posnext * * (* #pbr *) #pbid #poff
    106112normalize
    107113@(eqZb_elim pbid bid)
    108 [ 1: #Heqid >Heqid cases pbr cases br normalize
    109      [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
     114[ 1: #Heqid >Heqid (* cases pbr cases br normalize *)
    110115     cases (Zltb bid next) normalize nodelta
    111      [ 2,4: #Habsurd destruct (Habsurd) ]
    112      //
    113 | 2: #Hneqid cases pbr cases br normalize try // ]
     116     [ 2: #Habsurd destruct (Habsurd) ]
     117     #_ #H @False_ind @(absurd … (refl ??) H)
     118| 2: #Hneqid (* cases pbr cases br normalize *) try // ]
    114119qed.
    115120
     
    118123whd in match (free ??); @refl qed.
    119124
     125(*
    120126lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.
    121127   valid_pointer (free m b) ptr = true →
     
    148154     [ 2: % #Heq @Hguard %2 @Heq
    149155     | 1: @H % #Heq @Hguard %1 @Heq ]
    150 ] qed.
     156] qed. *)
    151157
    152158(* An alternative version without the gard on the equality of blocks. *)
     159(*
    153160lemma valid_pointer_free_ok_alt : ∀b : block. ∀m,ptr.
    154161   valid_pointer (free m b) ptr = true →
     
    165172         ]
    166173     | *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ]
    167 ] qed.
     174] qed. *)
    168175
    169176(* Well in fact a valid pointer can be valid even after a free. Ah. *)
     
    207214
    208215(* An embedding is a function from block ids to (blocks × offset). *)
    209 definition embedding ≝ Z → option (block × offset).
     216definition embedding ≝ block → option (block × offset).
    210217
    211218definition offset_plus : offset → offset → offset ≝
     
    224231match p with
    225232[ mk_pointer pblock poff ⇒
    226    match E (block_id pblock) with
     233   match E pblock with
    227234   [ None ⇒ None ?
    228235   | Some loc ⇒
     
    236243definition embedding_compatible : embedding → embedding → Prop ≝
    237244λE,E'.
    238   ∀b:block. E (block_id b) = None ? ∨
    239             E (block_id b) = E' (block_id b).
     245  ∀b:block. E b = None ? ∨
     246            E b = E' b.
    240247
    241248(* We parameterise the "equivalence" relation on values with an embedding. *)
     
    258265 ∀b1,off1,b2,off2,ty,v1.
    259266  valid_block m1 b1 →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
    260   E (block_id b1) = Some ? 〈b2,off2〉 →
     267  E b1 = Some ? 〈b2,off2〉 →
    261268  load_value_of_type ty m1 b1 off1 = Some ? v1 →
    262269  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
     
    299306definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝
    300307λE.λb.λm,m'.
    301   match E (block_id b) with
     308  match E b with
    302309  [ None ⇒ True
    303310  | Some loc ⇒
     
    313320  ∀b1,b2,b1',b2',delta1,delta2.
    314321  b1 ≠ b2 → (* note that two blocks can be different only becuase of this region *)
    315   E (block_id b1) = Some ? 〈b1',delta1〉 →
    316   E (block_id b2) = Some ? 〈b2',delta2〉 →
    317   (if eqZb (block_id b1') (block_id b2') then
     322  E b1 = Some ? 〈b1',delta1〉 →
     323  E b2 = Some ? 〈b2',delta2〉 →
     324  (if eq_block b1' b2' then
    318325    (* block_is_empty m b1' ∨ *)
    319326    high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
     
    332339  mi_inj : load_sim_ptr E m1 m2;
    333340  (* Invalid blocks are not mapped *)
    334   mi_freeblock : ∀b. ¬ (valid_block m1 b) → E (block_id b) = None ?;
     341  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
    335342  (* Valid pointers are mapped to valid pointers *)
    336343  mi_valid_pointers : ∀p,p'.
     
    340347  (* Blocks in the codomain are valid *)
    341348  mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
    342   (* Regions are preserved *)
    343   mi_region : ∀b,b',o'. E (block_id b) = Some ? 〈b',o'〉 → block_region b = block_region b';
     349  (* Regions are preserved - this might be superfluous now ?. *)
     350  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
    344351  (* sub-blocks do not overlap (non-aliasing property) *)
    345352  mi_nonalias : non_aliasing E m1;
     
    468475(* If we succeed to load something by value from a 〈b,off〉 location,
    469476   [b] is a valid block. *)
     477(*   
    470478lemma load_by_value_success_valid_block_aux :
    471479  ∀ty,m,b,off,v.
     
    487495     try // #Habsurd destruct (Habsurd)
    488496| *: normalize in Hmode; destruct (Hmode)
    489 ] qed.
     497] qed. *)
    490498
    491499(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
     
    497505    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
    498506    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
    499 #ty #m * #brg #bid #off #v
     507#ty #m * (* #brg *) #bid #off #v
    500508cases ty
    501509[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     
    509517     whd in match (beloadv ??);
    510518     cases (Zltb bid (nextblock m)) normalize nodelta
    511      cases (Zleb (low (blocks m (mk_block brg bid)))
     519     cases (Zleb (low (blocks m (mk_block (*brg*) bid)))
    512520                  (Z_of_unsigned_bitvector offset_size (offv off)))
    513      cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brg bid))))
     521     cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block (*brg*) bid))))
    514522     normalize nodelta
    515523     #Heq destruct (Heq)
     
    567575(* A valid block stays valid after an alloc. *)
    568576lemma alloc_valid_block_conservation :
    569   ∀m,m',z1,z2,r,new_block.
    570   alloc m z1 z2 r = 〈m', new_block〉 →
     577  ∀m,m',z1,z2,(*r,*)new_block.
     578  alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    571579  ∀b. valid_block m b → valid_block m' b.
    572 #m #m' #z1 #z2 #r * #b' #Hregion_eq
    573 elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
     580#m #m' #z1 #z2 (* #r*) * #b' (* #Hregion_eq *)
     581elim m #contents #nextblock #Hcorrect whd in match (alloc ???(*?*));
    574582#Halloc destruct (Halloc)
    575583#b whd in match (valid_block ??) in ⊢ (% → %); /2/
     
    609617
    610618lemma alloc_valid_pointer_conservation :
    611   ∀m,m',z1,z2,r,new_block.
    612   alloc m z1 z2 r=〈m',new_block〉 →
    613   ∀p. block_id (pblock p) ≠ block_id (pi1 … new_block)
     619  ∀m,m',z1,z2,(*r,*)new_block.
     620  alloc m z1 z2 (*r*) = 〈m',new_block〉 →
     621  ∀p. (pblock p) ≠ new_block
    614622      valid_pointer m' p = true →
    615623      valid_pointer m p = true.
    616 #m #m' #z1 #z2 #r * #new_block #Hregion
     624#m #m' #z1 #z2 (*#r*) #new_block
    617625cases m #cont #next #Hnext
    618626whd in ⊢ ((??%%) → ?);
     
    625633whd in match (update_block ?????);
    626634whd in match (update_block ?????);
    627 cut (b ≠ (mk_block r next))
    628 [ @(eq_block_elim … b (mk_block r next)) #H destruct try //
     635cut (b ≠ (mk_block (*r*) next))
     636[ @(eq_block_elim … b (mk_block (*r*) next)) #H destruct try //
    629637  @False_ind
    630638  @(absurd … (refl ??) Hneq) ] #Hneqb
    631639>(not_eq_block … Hneqb) normalize nodelta
    632640#HA #HB % [ % ] try assumption
    633 cases b in Hneqb Hneq Hblock_id; #r' #id * #Hnext_not_id #Hneq
     641cases b in Hneqb Hneq Hblock_id; (* #r'*) #id * #Hnext_not_id #Hneq
    634642#Hlt cut (id ≤ next)
    635643[ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ]
    636 #Hle @Zle_split try @Hle @Hneq
     644#Hle @Zle_split try @Hle % #Heq destruct
     645@(absurd … (refl ??) Hneq)
    637646qed.
    638647
    639648(* Allocating a new zone produces a valid block. *)
    640649lemma alloc_valid_new_block :
    641   ∀m,m',z1,z2,r,new_block.
    642   alloc m z1 z2 r = 〈m', new_block〉 →
     650  ∀m,m',z1,z2(*,r*),new_block.
     651  alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    643652  valid_block m' new_block.
    644 * #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
    645 whd in match (alloc ????); whd in match (valid_block ??);
     653* #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *)
     654whd in match (alloc ???(*?*)); whd in match (valid_block ??);
    646655#Halloc destruct (Halloc) /2/
    647656qed.
     
    649658(* All data in a valid block is unchanged after an alloc. *)
    650659lemma alloc_beloadv_conservation :
    651   ∀m,m',block,offset,z1,z2,r,new_block.
     660  ∀m,m',block,offset,z1,z2,(*r,*)new_block.
    652661    valid_block m block →
    653     alloc m z1 z2 r = 〈m', new_block〉 →
     662    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    654663    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
    655 * #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
     664* #contents #next #Hcorrect #m' #block #offset #z1 #z2 (* #r*) #new_block #Hvalid #Halloc
    656665whd in Halloc:(??%?); destruct (Halloc)
    657666whd in match (beloadv ??) in ⊢ (??%%);
     
    661670cut (eqZb (block_id block) next = false)
    662671[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq
    663 >Hneq cases (eq_region ??) normalize nodelta  @refl
     672>Hneq @refl
    664673qed.
    665674
    666675(* Lift [alloc_beloadv_conservation] to loadn *)
    667676lemma alloc_loadn_conservation :
    668   ∀m,m',z1,z2,r,new_block.
    669     alloc m z1 z2 r = 〈m', new_block〉 →
     677  ∀m,m',z1,z2,(*r,*)new_block.
     678    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    670679    ∀n. ∀block,offset.
    671680    valid_block m block →
    672681    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
    673 #m #m' #z1 #z2 #r #new_block #Halloc #n
     682#m #m' #z1 #z2 (*#r*) #new_block #Halloc #n
    674683elim n try //
    675684#n' #Hind #block #offset #Hvalid_block
     
    682691
    683692lemma alloc_load_value_of_type_conservation :
    684   ∀m,m',z1,z2,r,new_block.
    685     alloc m z1 z2 r = 〈m', new_block〉 →
     693  ∀m,m',z1,z2(*,r*),new_block.
     694    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    686695    ∀block,offset.
    687696    valid_block m block →
    688697    ∀ty. load_value_of_type ty m block offset =
    689698         load_value_of_type ty m' block offset.
    690 #m #m' #z1 #z2 #r #new_block #Halloc #block #offset #Hvalid         
     699#m #m' #z1 #z2 (*#r*) #new_block #Halloc #block #offset #Hvalid         
    691700#ty cases ty
    692701[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     
    701710lemma alloc_memory_inj_m2 :
    702711  ∀E:embedding.
    703   ∀m1,m2,m2',z1,z2,r,new_block.
     712  ∀m1,m2,m2',z1,z2(*,r*),new_block.
    704713  ∀H:memory_inj E m1 m2.
    705   alloc m2 z1 z2 r = 〈m2', new_block〉 →
     714  alloc m2 z1 z2 (*r*) = 〈m2', new_block〉 →
    706715  block_implementable_bv m2' new_block →
    707716  memory_inj E m1 m2'.
    708 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc #Himpl
     717#E #m1 #m2 #m2' #z1 #z2 (*#r*) * #new_block (* #Hregion *) #Hmemory_inj #Halloc #Himpl
    709718%
    710719[ whd
     
    727736| #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
    728737     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
    729      elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
     738     elim p' * (*#br'*) #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
    730739     whd in match (valid_pointer ??) in ⊢ (% → %);
    731740     @Zltb_elim_Type0
    732741     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
    733      #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
     742     #Hbid' cut (Zltb bid' (Zsucc new_block) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
    734743     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
    735744     whd in match (high_bound ??) in ⊢ (% → %);
    736745     whd in match (update_block ?????);
    737746     whd in match (eq_block ??);
    738      cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]
    739      #Hbid_neq >Hbid_neq
    740      cases (eq_region br' r) normalize #H @H
     747     cut (eqZb bid' new_block = false) [ 1: @eqZb_false /2 by not_to_not/ ]
     748     #Hbid_neq >Hbid_neq #H @H
     749(*     cases (eq_region br' r) normalize #H @H*)
    741750| #b #b' #o' #Hembed lapply (mi_nodangling … Hmemory_inj b b' o' Hembed) #H
    742751  @(alloc_valid_block_conservation … Halloc … H)
     
    745754| #b lapply (mi_nowrap … Hmemory_inj b)
    746755   whd in ⊢ (% → %);
    747    lapply (mi_nodangling … Hmemory_inj (block_id b))
    748    cases (E (block_id b)) normalize nodelta try //
     756   lapply (mi_nodangling … Hmemory_inj b)
     757   cases (E b) normalize nodelta try //
    749758   * #B #OFF normalize nodelta #Hguard
    750759   * * #H1 #H2 #Hinbounds @conj try @conj try assumption
    751    @(eq_block_elim … new_block B)
     760   @(eq_block_elim … (mk_block new_block) B)
    752761   [ #H <H assumption
    753762   | #H cases m2 in Halloc H2; #contents #nextblock #notnull
     
    767776lemma alloc_memory_inj_m1 :
    768777  ∀E:embedding.
    769   ∀m1,m2,m1',z1,z2,r,new_block.
     778  ∀m1,m2,m1',z1,z2,(*r,*)new_block.
    770779  ∀H:memory_inj E m1 m2.
    771   alloc m1 z1 z2 r = 〈m1', new_block〉 →
    772   memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then None ? else E x) m1' m2 ∧
    773   embedding_compatible E (λx. if eqZb (block_id (pi1 … new_block)) x then None ? else E x).
    774 #E #m1 #m2 #m1' #z1 #z2 #r * #new_block #Hregion_eq #Hinj #Halloc
    775 cut (E (block_id new_block) = None ?)
     780  alloc m1 z1 z2 (*r*) = 〈m1', new_block〉 →
     781  memory_inj (λx. if eq_block new_block x then None ? else E x) m1' m2 ∧
     782  embedding_compatible E (λx. if eq_block new_block x then None ? else E x).
     783#E #m1 #m2 #m1' #z1 #z2 (* #r*) #new_block (* #Hregion_eq *) #Hinj #Halloc
     784cut (E new_block = None ?)
    776785[ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?);
    777786  #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
    778787#Hempty
    779788cut (embedding_compatible E
    780      (λx:Z.
    781        if eqZb (block_id new_block) x
    782        then None (block×offset) 
    783        else E x ))
    784 [ whd #b @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try // #Heq <Heq %1 @Hempty ]
     789     (λx.
     790       if eq_block new_block x
     791       then None (block×offset)
     792       else E x))
     793[ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 @Hempty ]
    785794#Hembedding_compatible @conj try assumption
    786795%
    787796[ whd #b1 #off1 #b2 #off2 #ty #v1
    788797  @(eq_block_elim … b1 new_block)
    789   [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eqZb_z_z normalize nodelta
     798  [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta
    790799    #Habsurd destruct ]
    791800  #Hneq #Hvalid
    792801  whd in ⊢ ((??%?) → ?);
    793   @(eqZb_elim … (block_id new_block) (block_id b1))
     802  @(eq_block_elim … new_block b1)
    794803  normalize nodelta
    795804  [ #Heq #Habsurd destruct (Habsurd) ]
     
    806815  %{v2} @conj try assumption
    807816  @(embedding_compatibility_value_eq … Hveq2) assumption
    808 | #b #Hnot_valid @(eqZb_elim … (block_id new_block) (block_id b))
     817| #b #Hnot_valid @(eq_block_elim … new_block b)
    809818  normalize nodelta
    810819  [ #Heq @refl
     
    814823  cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1'
    815824  whd in ⊢ ((??%%) → ?); 
    816   @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta
     825  @(eq_block_elim … new_block b) normalize nodelta
    817826  [ #Heq #Habsurd destruct ]
    818827  #Hneq #Hembed
     
    820829  #Hvalid1
    821830  @(Hvalidptr Hvalid1 Hembed)
    822 | #b #b' #o' @(eqZb_elim … (block_id new_block) b)
     831| #b #b' #o' @(eq_block_elim … new_block b)
    823832  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
    824833  normalize nodelta #Henq
    825834  @(mi_nodangling … Hinj)
    826 | #b #b' #o' @(eqZb_elim … (block_id new_block) (block_id b))
     835| #b #b' #o' @(eq_block_elim … new_block b)
    827836  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
    828837  #Hneq @(mi_region … Hinj)
    829838| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
    830   @(eqZb_elim … (block_id new_block) (block_id b1))
     839  @(eq_block_elim … new_block b1)
    831840  normalize nodelta
    832841  [ #Heq #Habsurd destruct (Habsurd) ]
    833842  #Hneq1 #Hembed1
    834   @(eqZb_elim … (block_id new_block) (block_id b2))
     843  @(eq_block_elim … new_block b2)
    835844  normalize nodelta
    836845  [ #Heq #Habsurd destruct (Habsurd) ]
    837846  #Hneq2 #Hembed2
    838   @(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta try //
     847  @(eq_block_elim … b1' b2') normalize nodelta try //
    839848  #Heq
    840849  lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq
    841   >eqZb_z_z normalize nodelta
     850  >eq_block_b_b normalize nodelta
    842851  cases m1 in Halloc; #contents #next #Hnext
    843852  >unfold_high_bound >unfold_low_bound
     
    845854  >unfold_high_bound >unfold_low_bound
    846855  >unfold_high_bound >unfold_low_bound
    847   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    848   cut (eq_block b1 (mk_block r next) = false)
    849   [ whd in ⊢ (??%%);
    850     >(eqZb_false … (sym_neq ??? Hneq1))
    851     cases (eq_region ??) @refl ]
    852   cut (eq_block b2 (mk_block r next) = false)
    853   [ whd in ⊢ (??%%);
    854     >(eqZb_false … (sym_neq ??? Hneq2))
    855     cases (eq_region ??) @refl ]
     856  whd in ⊢ ((??%%) → ?); destruct (Heq) #Heq destruct (Heq)
     857  lapply (neq_block_eq_block_false … (sym_neq ??? Hneq1))
     858  lapply (neq_block_eq_block_false … (sym_neq ??? Hneq2))
    856859  #Heq_block_2
    857860  #Heq_block_1
     
    876879    >Heq_block_1 >Heq_block_2 @H
    877880  ]
    878 | #b whd @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try //
     881| #b whd @(eq_block_elim … new_block b) normalize nodelta try //
    879882  #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
    880   cases (E (block_id b)) normalize nodelta try //
     883  cases (E b) normalize nodelta try //
    881884  * #bb #oo normalize nodelta
    882885  * * * #HA #HB * #HC #HD #HE @conj try @conj
     
    892895 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try //
    893896 whd in match (update_block ?????);
    894  cut (eq_block b (mk_block r next) = false)
    895  [ 1,3,5: whd in ⊢ (??%%);
    896           >(eqZb_false … (sym_neq ??? Hneq))
    897           cases (eq_region ??) @refl
     897 cut (eq_block b (mk_block next) = false)
     898 [ 1,3,5: @neq_block_eq_block_false @(sym_neq … Hneq)
    898899 | 2,4,6: #Heq_block >Heq_block // ]
    899 ] qed.
    900  
    901        
     900] qed.
     901
     902(* In CompCert, "∀v. value_eq Vundef v" holds. Not in our developments. In order
     903 * to prove the equivalent of lemma 68 of L&B, we need to provide an additional
     904 * property of the target memory: the /target/ portion of memory we are going to map a block
     905 * to must only contains BVundef (whereas in CompCert, the fact that the source block
     906 * contains BVundefs is enough to proceed).
     907 *
     908 * The following definition expresses the fact that a portion of memory [z1; z2] contains only
     909 * BVundefs.
     910 * Note that the bounds are /inclusive/. We do not check for their validity. *)
     911definition undef_memory_zone : mem → block → Z → Z → Prop ≝
     912  λm,b,z1,z2.
     913    ∀i. z1 ≤ i → i ≤ z2 → contents (blocks m b) i = BVundef.
     914
     915(* Explictly stating the properties of alloc. *)
     916lemma alloc_properties :
     917  ∀m,m',z1,z2(*,r*),b.
     918   alloc m z1 z2 (* r *) = 〈m',b〉 →
     919   low_bound m' b = z1 ∧
     920   high_bound m' b = z2 ∧
     921   undef_memory_zone m' b z1 z2.
     922#m #m'  #z1 #z2 * (* #br *) #bid
     923cases m #contents #next #Hnext
     924whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     925>unfold_low_bound >unfold_high_bound
     926@conj try @conj
     927/2 by refl, pair_destruct_2/
     928whd
     929#i #H1 #H2 whd in match (update_block ?????);
     930>eq_block_b_b normalize nodelta @refl
     931qed.
     932
     933(* Embed a fresh block inside an unmapped portion of the target block.
     934 * This is the equivalent of lemma 68 of Leroy&Blazy.
     935 * Compared to L&B, an additional "undef_memory_zone" proof object must be provided.
     936 *)
     937lemma alloc_memory_inj_m1_to_m2 :
     938  ∀E:embedding.
     939  ∀m1,m2,m1':mem.
     940  ∀z1,z2:Z.
     941  ∀target,new_block.
     942  ∀delta:offset.
     943  valid_block m2 target →
     944  alloc m1 z1 z2 = 〈m1', new_block〉 →
     945  low_bound m2 target ≤ z1 + Zoo delta →
     946  z2 + Zoo delta ≤ high_bound m2 target →
     947  undef_memory_zone m2 target (z1 + Zoo delta) (z2 + Zoo delta) →
     948  (∀b,delta'. b ≠ new_block →
     949              E b = Some ? 〈target, delta'〉 →
     950              high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨
     951              z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) →
     952  memory_inj E m1 m2 →
     953  memory_inj (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x) m1' m2.
     954#E #m1 #m2 #m1' #z1 #z2 (* * #tr *) #tid (* * * #newr *) #newid (* * *) #delta
     955#Hvalid #Halloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj
     956cut (E newid = (None ?))
     957[ @(mi_freeblock ??? Hinj newid) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj
     958  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
     959@cthulhu
     960qed.
     961(*
     962#Hnew_not_mapped
     963cut (embedding_compatible E (λx. if eqZb newid x then Some ? 〈mk_block newr tid, delta〉 else E x))
     964[ whd #b @(eqZb_elim … newid (block_id b)) normalize nodelta try // #Heq <Heq %1 assumption ]
     965#Hembedding_compatible
     966%
     967[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid' #Hembed #Hload
     968  @(eqZb_elim … newid (block_id b1))
     969  [ 2: (* we do not load from the newly allocated block *)
     970     #Hneq
     971     (* prove that we can equivalently load from the memory before alloc *)
     972     cases (some_inversion ????? Hembed) * #target' #delta'
     973     >(eqZb_false … Hneq) normalize nodelta
     974     * #Hembed #Heq destruct (Heq)
     975     cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block' #Hlow #Hhigh
     976     lapply (alloc_valid_block_conservation2 … Halloc … (sym_neq ??? Hneq) Hvalid_block')
     977     #Hvalid_block
     978     lapply (alloc_load_value_of_type_conservation … Halloc b1 off1 … Hvalid_block ty)
     979     #Heq_load <Heq_load in Hload; #Hload
     980     lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … (sym_neq ??? Hneq) Hvalid')     
     981     #Hvalid_ptr
     982     lapply (mi_inj … Hinj b1 off1 b2 (offset_plus off1 delta') … Hvalid_ptr … Hload)
     983     [ whd in ⊢ (??%?); >Hembed @refl ]
     984     (* conclude *)
     985     * #v2 * #Hload2 #Hvalue_eq %{v2} @conj
     986     [ @Hload2
     987     | @(embedding_compatibility_value_eq … Hvalue_eq) @Hembedding_compatible ]
     988  | 1: (* we allegedly performed a load from a block with the same id as
     989        * the newly allocated block (which by def. of alloc contains only BVundefs) *)
     990     #Heq destruct (Heq)
     991     whd in Hembed:(??%?); >eqZb_z_z in Hembed; normalize nodelta
     992     #Heq_ptr
     993     (* cull out all boring cases *)
     994     lapply Hload -Hload cases ty
     995     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     996     | #structname #fieldspec | #unionname #fieldspec | #id ]
     997     [ 1,6,7: whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
     998     | 4,5: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq_ptr Heq)
     999            %{(Vptr (mk_pointer (mk_block newr tid) (offset_plus off1 delta)))}
     1000            @conj
     1001            [ 1,3: @refl
     1002            | *: %4 whd in ⊢ (??%?); >eqZb_z_z @refl ] ]
     1003     (* Now: load-by-value cases. Outcome is either None or Undef. *)
     1004     lapply (load_by_value_after_alloc_undef m1 m1' z1 z2 b1 ?)
     1005     [ 1,3,5:
     1006     #Hload_eq
     1007     [ lapply (Hload_eq (Tint sz sg) (refl ??) off1)
     1008     | lapply (Hload_eq (Tpointer ptr_ty) (refl ??) off1)
     1009     | lapply (Hload_eq (Tcomp_ptr id) (refl ??) off1) ]
     1010     *
     1011     (* None case: absurd *)
     1012     [ 2,4,6: >Hload #Habsurd destruct (Habsurd) ]
     1013         >Hload #Heq destruct (Heq) %{Vundef}
     1014         @conj try //
     1015         cut (valid_pointer m2 (mk_pointer b2 (offset_plus off1 delta))=true)
     1016         [ 1,3,5: @valid_pointer_of_Prop @conj try @conj
     1017            [ 1,4,7: assumption
     1018            | 2,5,8: >unfold_low_bound
     1019         lapply (alloc_properties … Halloc) * *
     1020         >unfold_low_bound >unfold_high_bound #Hlow #Hhigh #Hundef
     1021         lapply (valid_pointer_to_Prop … Hvalid') * *
     1022         #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow >Hhigh
     1023*)
    9021024
    9031025(* Embed a fresh block inside an unmapped portion of the target block.
    9041026 * This is the equivalent of lemma 68 for Leroy&Blazy. *)
     1027(*
    9051028axiom alloc_memory_inj_m1_to_m2 :
    9061029  ∀E:embedding.
     
    9191042  memory_inj E m1 m2 →
    9201043  memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then Some ? 〈b2, delta〉 else E x) m1' m2.
     1044*)
    9211045
    9221046(* -------------------------------------- *)
     
    9691093  load_sim_ptr E m1 m2 →
    9701094  ∀b. free m2 b = m2' →
    971       (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
     1095      (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
    9721096      load_sim_ptr E m1 m2'.     
    9731097#E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped
     
    10541178#b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
    10551179#Hembed1 #Hembed2
    1056 @(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta
     1180@(eq_block_elim … b1' b2') normalize nodelta
    10571181[ 2: try // ]
    10581182#Hblocks_eq
     
    10601184lapply Hembed1 -Hembed1
    10611185lapply Hblocks_eq -Hblocks_eq
    1062 cases b1' #r1' #bid1'
    1063 cases b2' #r2' #bid2'
     1186(*cases b1' #r1' #bid1'
     1187  cases b2' #r2' #bid2' *)
    10641188#Heq destruct (Heq)
    1065 generalize in match bid2';
     1189generalize in match b2';
    10661190#target #Hembed1 #Hembed2
    10671191lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2)
    1068 >eqZb_z_z normalize nodelta
     1192>eq_block_b_b normalize nodelta
    10691193normalize nodelta <Hfree
    10701194@(eq_block_elim … b1 b)
     
    11121236| @(free_non_aliasing_m1 … Hinj … Hfree)
    11131237| #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?);
    1114   cases (E (block_id bb)) normalize nodelta try //
     1238  cases (E bb) normalize nodelta try //
    11151239  * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj
    11161240  try //
     
    11401264  memory_inj E m1 m2 →
    11411265  ∀b. free m2 b = m2' →
    1142       (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 →
     1266      (∀b1,delta. E b1 = Some ? 〈b, delta〉 →
    11431267      (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 
    11441268      memory_inj E m1 m2'.
     
    11711295| @Hregion
    11721296| #bb lapply (Himpl bb)
    1173   whd in ⊢ (% → %); cases (E (block_id bb)) normalize nodelta try //
     1297  whd in ⊢ (% → %); cases (E bb) normalize nodelta try //
    11741298  * #BLO #OFF normalize nodelta * * destruct (Hfree)
    11751299  #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption
     
    11911315  memory_inj E m1 m2 →
    11921316  ∀blocklist,b2.
    1193   (∀b1,delta. E (block_id b1) = Some ? 〈b2, delta〉 → meml ? b1 blocklist) →
     1317  (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) →
    11941318  free m2 b2 = m2' →
    11951319  free_list m1 blocklist = m1' →
     
    12531377       else false) normalize nodelta
    12541378[ 2: #Habsurd destruct (Habsurd) ]
    1255 #Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
    1256 cases rr cases wr normalize try //
    1257 @(eqZb_elim … rid wid)
    1258 [ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
    1259 try //
     1379#Heq destruct (Heq)
     1380cases (Zltb (block_id rb) (nextblock mA)) normalize nodelta try //
     1381cut (eqZb (block_id rb) (block_id wb) = false)
     1382[ >eqZb_symmetric @Hblock_neq ]
     1383#Heqzb >Heqzb normalize nodelta @refl
    12601384qed.
    12611385
     
    13271451    memory_inj E mA mB →
    13281452    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
    1329     ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 →
     1453    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
    13301454    high_bound mA b1 + Zoo delta < Zoo wo →
    13311455    ∀ty,off.
     
    14051529    memory_inj E mA mB →
    14061530    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
    1407     ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 →
     1531    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
    14081532    Zoo wo < low_bound mA b1 + Zoo delta →
    14091533    ∀ty,off.
     
    14221546  ∀block2. ∀i : offset. ∀ty : type.
    14231547  (∀block1,delta.
    1424     E (block_id block1) = Some ? 〈block2, delta〉 →
     1548    E block1 = Some ? 〈block2, delta〉 →
    14251549    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
    14261550  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
     
    14781602  ∀block2. ∀i : offset. ∀ty : type.
    14791603  (∀block1,delta.
    1480     E (block_id block1) = Some ? 〈block2, delta〉 →
     1604    E block1 = Some ? 〈block2, delta〉 →
    14811605    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
    14821606  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
     
    15081632  >(Hnext_eq) try //
    15091633| #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %);
    1510   cases (E (block_id b)) try //
     1634  cases (E b) try //
    15111635  * #BLO #OFF normalize nodelta * *
    15121636  #Hb #HBLO #Hbound try @conj try @conj try assumption
     
    15261650lemma be_to_fe_value_ptr :
    15271651  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
    1528 #b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta
    1529 cases br normalize nodelta >eqZb_z_z normalize nodelta
     1652#b * #o whd in ⊢ (??%%); normalize cases b (* #br *) #bid normalize nodelta
     1653(*cases br normalize nodelta *) >eqZb_z_z normalize nodelta
    15301654cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
    15311655<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
     
    15701694  ∀E,m1,m2.
    15711695  memory_inj E m1 m2 →
    1572   ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 →
     1696  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
    15731697  ∀v1,v2. value_eq E v1 v2 →
    15741698  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
     
    16391763  ∀E,m1,m2.
    16401764  memory_inj E m1 m2 →
    1641   ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 →
     1765  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
    16421766  ∀v1,v2. value_eq E v1 v2 →
    16431767  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
     
    16621786  ∀Hinj:memory_inj E m1 m2.
    16631787  ∀v1,v2. value_eq E v1 v2 →
    1664   ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 →
     1788  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
    16651789  ∀ty,i,m1'.
    16661790  ast_typ_consistent_with_value ty v1 →
     
    17501874  ∀Hinj:memory_inj E m1 m2.
    17511875  ∀v1,v2. value_eq E v1 v2 →
    1752   ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 →
     1876  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
    17531877  ∀ty,i,m1'.
    17541878  type_consistent_with_value ty v1 →
     
    17701894  ∀Hinj:memory_inj E m1 m2.
    17711895  ∀ty,b,i,v.
    1772   E (block_id b) = None ? →
     1896  E b = None ? →
    17731897  store_value_of_type ty m1 b i v = Some ? m1' →
    17741898  load_sim_ptr E m1' m2.
     
    18201944  ∀Hinj:memory_inj E m1 m2.
    18211945  ∀ty,b,i,v.
    1822   E (block_id b) = None ? →
     1946  E b = None ? →
    18231947  store_value_of_type ty m1 b i v = Some ? m1' →
    18241948  memory_inj E m1' m2.
     
    18491973    | #bb whd
    18501974      lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?);
    1851       cases (E (block_id bb)) normalize nodelta try // * #bb' #off
     1975      cases (E bb) normalize nodelta try // * #bb' #off
    18521976      normalize nodelta
    18531977      whd in match (block_implementable_bv ??);     
     
    19522076          @(ex_intro … (conj … (refl …) ?))
    19532077          @vptr_eq whd in match (pointer_translation ??);
    1954           cases (E (block_id b1')) in Hembed;
     2078          cases (E b1') in Hembed;
    19552079          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    19562080          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    19942118     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    19952119     elim p1 in Hembed; #b1 #o1 normalize nodelta
    1996      cases (E (block_id b1))
     2120     cases (E b1)
    19972121     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    19982122     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    20932217          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    20942218          elim p1 in Hembed; #b1 #o1 normalize nodelta
    2095           cases (E (block_id b1))
     2219          cases (E b1)
    20962220          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    20972221          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    21092233               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
    21102234               whd in ⊢ ((??%?) → (??%?) → ?);
    2111                cases (E (block_id b1')) normalize nodelta
     2235               cases (E b1') normalize nodelta
    21122236               [ 1: #Habsurd destruct (Habsurd) ]
    21132237               * #dest_block #dest_off normalize nodelta
     
    25152639          lapply (mi_nowrap … Hinj bq1)
    25162640          whd in ⊢ (% → ?);
    2517           cases (E (block_id bq1)) normalize nodelta
     2641          cases (E bq1) normalize nodelta
    25182642          [ #_ #Habsurd destruct ]
    25192643          * #BLO #OFF normalize nodelta * *         
     
    25362660          lapply (mi_region … Hinj bq1)
    25372661          lapply (mi_region … Hinj bp1)
    2538           cases (E (block_id bq1)) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
     2662          cases (E bq1) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    25392663          * #BLOq #DELTAq normalize nodelta
    2540           cases (E (block_id bp1)) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
     2664          cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
    25412665          * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
    25422666          lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) -Hregion1 -Hregion2
     
    25562680          lapply (valid_pointer_to_Prop … Hvalid')
    25572681          * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp
    2558           >eqZb_z_z >eq_block_b_b normalize nodelta
     2682          >eq_block_b_b normalize nodelta
    25592683          *
    25602684          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
Note: See TracChangeset for help on using the changeset viewer.