include "joint/BEMem.ma". include "common/FrontEndVal.ma". definition mem ≝ bemem. let rec loadn (m:bemem) (ptr:pointer) (n:nat) on n : option (list beval) ≝ match n with [ O ⇒ Some ? ([ ]) | S n' ⇒ match beloadv m ptr with [ None ⇒ None ? | Some v ⇒ match loadn m (shift_pointer 2 ptr (bitvector_of_nat … 1)) n' with [ None ⇒ None ? | Some vs ⇒ Some ? (v::vs) ] ] ]. definition load : typ → mem → pointer → option val ≝ λt,m,ptr. match loadn m ptr (typesize t) with [ None ⇒ None ? | Some vs ⇒ Some ? (be_to_fe_value t vs) ]. let rec loadv (t:typ) (m:bemem) (addr:val) on addr : option val ≝ match addr with [ Vptr ptr ⇒ load t m ptr | _ ⇒ None ? ]. let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option bemem ≝ match vs with [ nil ⇒ Some ? m | cons v tl ⇒ match bestorev m ptr v with [ None ⇒ None ? | Some m' ⇒ storen m' (shift_pointer 2 ptr (bitvector_of_nat … 1)) tl ] ]. definition store : typ → bemem → pointer → val → option bemem ≝ λt,m,ptr,v. storen m ptr (fe_to_be_values t v). definition storev : typ → bemem → val → val → option bemem ≝ λt,m,addr,v. match addr with [ Vptr ptr ⇒ store t m ptr v | _ ⇒ None ? ]. (* Only used by Clight semantics for pointer comparisons. So in contrast to CompCert, we allow a pointer-to-one-off-the-end. *) definition valid_pointer : mem → pointer → bool ≝ λm,ptr. Zltb (block_id (pblock ptr)) (nextblock ? m) ∧ Zleb (low_bound ? m (pblock ptr)) (offv (poff ptr)) ∧ Zleb (offv (poff ptr)) (high_bound ? m (pblock ptr)). (* (* *********************************************************************) (* *) (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) (* Sandrine Blazy, ENSIIE and INRIA Paris-Rocquencourt *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU General Public License as published by *) (* the Free Software Foundation, either version 2 of the License, or *) (* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (* * This file develops the memory model that is used in the dynamic semantics of all the languages used in the compiler. It defines a type [mem] of memory states, the following 4 basic operations over memory states, and their properties: - [load]: read a memory chunk at a given address; - [store]: store a memory chunk at a given address; - [alloc]: allocate a fresh memory block; - [free]: invalidate a memory block. *) include "arithmetics/nat.ma". (*include "binary/Z.ma".*) (*include "datatypes/sums.ma".*) (*include "datatypes/lists/list.ma".*) (*include "Plogic/equality.ma".*) (*include "Coqlib.ma".*) include "common/Values.ma". (*include "AST.ma".*) include "utilities/binary/division.ma". definition update : ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z → A. Z → A ≝ λA,x,v,f. λy.match eqZb y x with [ true ⇒ v | false ⇒ f y ]. lemma update_s: ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A. update … x v f x = v. #A #x #v #f whd in ⊢ (??%?); >(eqZb_z_z …) //; qed. lemma update_o: ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A. ∀y: Z. x ≠ y → update … x v f y = f y. #A #x #v #f #y #H whd in ⊢ (??%?); @eqZb_elim //; #H2 cases H;#H3 elim (H3 ?);//; qed. (* FIXME: workaround for lack of nunfold *) lemma unfold_update : ∀A,x,v,f,y. update A x v f y = match eqZb y x with [ true ⇒ v | false ⇒ f y ]. //; qed. definition update_block : ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block → A. block → A ≝ λA,x,v,f. λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ]. lemma update_block_s: ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. update_block … x v f x = v. #A * * #ix #v #f whd in ⊢ (??%?); >eq_block_b_b // qed. lemma update_block_o: ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. ∀y: block. x ≠ y → update_block … x v f y = f y. #A #x #v #f #y #H whd in ⊢ (??%?); @eq_block_elim //; #H2 cases H;#H3 elim (H3 ?);//; qed. (* FIXME: workaround for lack of nunfold *) lemma unfold_update_block : ∀A,x,v,f,y. update_block A x v f y = match eq_block y x with [ true ⇒ v | false ⇒ f y ]. //; qed. (* * Structure of memory states *) (* A memory state is organized in several disjoint blocks. Each block has a low and a high bound that defines its size. Each block map byte offsets to the contents of this byte. *) (* The possible contents of a byte-sized memory cell. To give intuitions, a 4-byte value [v] stored at offset [d] will be represented by the content [Datum(4, v)] at offset [d] and [Cont] at offsets [d+1], [d+2] and [d+3]. The [Cont] contents enable detecting future writes that would partially overlap the 4-byte value. *) inductive content : Type[0] ≝ | Undef: content (*r undefined contents *) | Datum: nat → val → content (*r first byte of a value *) | Cont: content. (*r continuation bytes for a multi-byte value *) definition contentmap : Type[0] ≝ Z → content. (* A memory block comprises the dimensions of the block (low and high bounds) plus a mapping from byte offsets to contents. *) record block_contents : Type[0] ≝ { low: Z; high: Z; contents: contentmap }. (* A memory state is a mapping from block addresses (represented by memory regions and integers) to blocks. We also maintain the address of the next unallocated block, and a proof that this address is positive. *) record mem : Type[0] ≝ { blocks: block -> block_contents; nextblock: Z; nextblock_pos: OZ < nextblock }. (* * Operations on memory stores *) definition pred_size_chunk : typ → nat ≝ λchunk. match chunk with [ ASTint sz _ ⇒ pred (size_intsize sz) | ASTptr r ⇒ pred (size_pointer r) | ASTfloat sz ⇒ pred (size_floatsize sz) ]. lemma size_chunk_pred: ∀chunk. typesize chunk = 1 + pred_size_chunk chunk. * // qed. (* Memory reads and writes must respect alignment constraints: the byte offset of the location being addressed should be an exact multiple of the natural alignment for the chunk being addressed. This natural alignment is defined by the following [align_chunk] function. Some target architectures (e.g. the PowerPC) have no alignment constraints, which we could reflect by taking [align_chunk chunk = 1]. However, other architectures have stronger alignment requirements. The following definition is appropriate for PowerPC and ARM. *) definition align_chunk : typ → Z ≝ λchunk.match chunk return λ_.Z with [ ASTint _ _ ⇒ 1 | ASTptr _ ⇒ 1 | ASTfloat _ ⇒ 1 ]. lemma align_chunk_pos: ∀chunk. OZ < align_chunk chunk. #chunk cases chunk;normalize;//; qed. lemma align_size_chunk_divides: ∀chunk. (align_chunk chunk ∣ typesize chunk). #chunk cases chunk * [ 1,2,3: * ] normalize /3 by witness/ qed. lemma align_chunk_compat: ∀chunk1,chunk2. typesize chunk1 = typesize chunk2 → align_chunk chunk1 = align_chunk chunk2. * * [ 1,2,3: * ] * * [ 1,2,3,12,13,14,23,24,25: * ] normalize // qed. (* The initial store. *) definition oneZ ≝ pos one. lemma one_pos: OZ < oneZ. //; qed. definition empty_block : Z → Z → block_contents ≝ λlo,hi.mk_block_contents lo hi (λy. Undef). definition empty: mem ≝ mk_mem (λx.empty_block OZ OZ) (pos one) one_pos. definition nullptr: block ≝ mk_block Any OZ. (* Allocation of a fresh block with the given bounds. Return an updated memory state and the address of the fresh block, which initially contains undefined cells. Note that allocation never fails: we model an infinite memory. *) lemma succ_nextblock_pos: ∀m. OZ < Zsucc (nextblock m). (* XXX *) #m lapply (nextblock_pos m);normalize; cases (nextblock m);//; #n cases n;//; qed. definition alloc : mem → Z → Z → region → mem × block ≝ λm,lo,hi,r. let b ≝ mk_block r (nextblock m) in 〈mk_mem (update_block … b (empty_block lo hi) (blocks m)) (Zsucc (nextblock m)) (succ_nextblock_pos m), b〉. (* Freeing a block. Return the updated memory state where the given block address has been invalidated: future reads and writes to this address will fail. Note that we make no attempt to return the block to an allocation pool: the given block address will never be allocated later. *) definition free ≝ λm,b.mk_mem (update_block … b (empty_block OZ OZ) (blocks m)) (nextblock m) (nextblock_pos m). (* Freeing of a list of blocks. *) definition free_list ≝ λm,l.foldr ?? (λb,m.free m b) m l. (* XXX hack for lack of reduction with restricted unfolding *) lemma unfold_free_list : ∀m,h,t. free_list m (h::t) = free (free_list m t) h. normalize; //; qed. (* Return the low and high bounds for the given block address. Those bounds are 0 for freed or not yet allocated address. *) definition low_bound : mem → block → Z ≝ λm,b.low (blocks m b). definition high_bound : mem → block → Z ≝ λm,b.high (blocks m b). definition block_region: mem → block → region ≝ λm,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *) (* A block address is valid if it was previously allocated. It remains valid even after being freed. *) (* TODO: should this check for region? *) definition valid_block : mem → block → Prop ≝ λm,b.block_id b < nextblock m. (* FIXME: hacks to get around lack of nunfold *) lemma unfold_low_bound : ∀m,b. low_bound m b = low (blocks m b). //; qed. lemma unfold_high_bound : ∀m,b. high_bound m b = high (blocks m b). //; qed. lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock m). //; qed. (* Reading and writing [N] adjacent locations in a [contentmap]. We define two functions and prove some of their properties: - [getN n ofs m] returns the datum at offset [ofs] in block contents [m] after checking that the contents of offsets [ofs+1] to [ofs+n+1] are [Cont]. - [setN n ofs v m] updates the block contents [m], storing the content [v] at offset [ofs] and the content [Cont] at offsets [ofs+1] to [ofs+n+1]. *) let rec check_cont (n: nat) (p: Z) (m: contentmap) on n : bool ≝ match n return λ_.bool with [ O ⇒ true | S n1 ⇒ match m p with [ Cont ⇒ check_cont n1 (Zplus p 1) m (* FIXME: cannot disambiguate + properly *) | _ ⇒ false ] ]. (* XXX : was +, not ∨ logical or is used when eqb is expected, coq idiom, is it necessary?? *) definition eq_nat: ∀p,q: nat. p=q ∨ p≠q. @decidable_eq_nat (* // not working, why *) qed. definition getN : nat → Z → contentmap → val ≝ λn,p,m.match m p with [ Datum n' v ⇒ match andb (eqb n n') (check_cont n (p + oneZ) m) with [ true ⇒ v | false ⇒ Vundef ] | _ ⇒ Vundef ]. let rec set_cont (n: nat) (p: Z) (m: contentmap) on n : contentmap ≝ match n with [ O ⇒ m | S n1 ⇒ update ? p Cont (set_cont n1 (p + oneZ) m) ]. definition setN : nat → Z → val → contentmap → contentmap ≝ λn,p,v,m.update ? p (Datum n v) (set_cont n (p + oneZ) m). (* Nonessential properties that may require arithmetic (* XXX: the daemons *) axiom daemon : ∀A:Prop.A. lemma check_cont_spec: ∀n,m,p. match (check_cont n p m) with [ true ⇒ ∀q.p ≤ q → q < p + n → m q = Cont | false ⇒ ∃q. p ≤ q ∧ q < (p + n) ∧ m q ≠ Cont ]. #n elim n; [#m #p #q #Hl #Hr (* derive contradiction from Hl, Hr; needs: - p + O = p - p ≤ q → q < p → False *) napply daemon |#n1 #IH #m #p (* whd : doesn't work either *) cut (check_cont (S n1) p m = match m p with [ Undef ⇒ false | Datum _ _ ⇒ false | Cont ⇒ check_cont n1 (Zplus p oneZ) m ]) [@ |#Heq >Heq lapply (refl ? (m p)); cases (m p) in ⊢ (???% → %); [#Heq1 % [napply p |% [napply daemon |@nmk #Hfalse >Hfalse in Heq1 #Heq1 destruct ] ] |#n2 #v #Heq1 % [napply p | % [ (* refl≤ and p < p + S n1 *)napply daemon |@nmk #Hfalse >Hfalse in Heq1 #Heq1 destruct ] ] |#Heq1 lapply (IH m (p + 1)); lapply (refl ? (check_cont n1 (p + 1) m)); (* napply daemon *) cases (check_cont n1 (p + 1) m) in ⊢ (???% → %); whd in ⊢ (? → % → %); [#H #H1 #q #Hl #Hr cut (p = q ∨ p + 1 ≤ q) [(* Hl *) napply daemon |*; [// |#Hl2 @H1 //;(*Hr*)napply daemon ] ] |#H #H1 cases H1;#x *;*;#Hl #Hr #Hx %{ x} @ [@ [(*Hl*) napply daemon |(*Hr*) napply daemon ] |//]]]] qed. lemma check_cont_true: ∀n:nat.∀m,p. (∀q. p ≤ q → q < p + n → m q = Cont) → check_cont n p m = true. #n #m #p #H lapply (check_cont_spec n m p); cases (check_cont n p m);//; whd in ⊢ (%→?);*; #q *;*;#Hl #Hr #Hfalse cases Hfalse;#H1 elim (H1 ?);@H //; qed. lemma check_cont_false: ∀n:nat.∀m,p,q. p ≤ q → q < p + n → m q ≠ Cont → check_cont n p m = false. #n #m #p #q lapply (check_cont_spec n m p); cases (check_cont n p m);//; whd in ⊢ (%→?);#H #Hl #Hr #Hfalse cases Hfalse;#H1 elim (H1 ?);@H //; qed. lemma set_cont_inside: ∀n:nat.∀p:Z.∀m.∀q:Z. p ≤ q → q < p + n → (set_cont n p m) q = Cont. #n elim n; [#p #m #q #Hl #Hr (* by Hl, Hr → False *)napply daemon |#n1 #IH #p #m #q #Hl #Hr cut (p = q ∨ p+1 ≤ q) [napply daemon |*; [#Heq >Heq @update_s |#Hl2 whd in ⊢ (??%?);nrewrite > (? : eqZb q p = false) [whd in ⊢ (??%?);napply IH [napply Hl2 |(* Hr *) napply daemon ] |(*Hl2*)napply daemon ] ] ] ] qed. lemma set_cont_outside: ∀n:nat.∀p:Z.∀m.∀q:Z. q < p ∨ p + n ≤ q → (set_cont n p m) q = m q. #n elim n [#p #m #q #_ @ |#n1 #IH #p #m #q #H whd in ⊢ (??%?);>(? : eqZb q p = false) [whd in ⊢ (??%?);@IH cases H; [#Hl % napply daemon |#Hr %{2} napply daemon] |(*H*)napply daemon ] ] qed. lemma getN_setN_same: ∀n,p,v,m. getN n p (setN n p v m) = v. #n #p #v #m nchange in ⊢ (??(???%)?) with (update ????); whd in ⊢ (??%?); >(update_s content p ??) whd in ⊢ (??%?); >(eqb_n_n n) nrewrite > (check_cont_true ????) [@ |#q #Hl #Hr >(update_o content …) [/2/; |(*Hl*)napply daemon ] ] qed. lemma getN_setN_other: ∀n1,n2:nat.∀p1,p2:Z.∀v,m. p1 + n1 < p2 ∨ p2 + n2 < p1 → getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m. #n1 #n2 #p1 #p2 #v #m #H ngeneralize in match (check_cont_spec n2 m (p2 + oneZ)); lapply (refl ? (check_cont n2 (p2+oneZ) m)); cases (check_cont n2 (p2+oneZ) m) in ⊢ (???% → %); #H1 whd in ⊢ (% →?); whd in ⊢ (?→(???%)); >H1 [#H2 nchange in ⊢ (??(???%)?) with (update ????); whd in ⊢(??%%);>(check_cont_true …) [ >(check_cont_true … H2) >(update_o content ?????) [ >(set_cont_outside ?????) //; (* arith *) napply daemon | (* arith *) napply daemon ] | #q #Hl #Hh >(update_o content ?????) [ >(set_cont_outside ?????) /2/; (* arith *) napply daemon | (* arith *) napply daemon ] ] | *; #q *;#A #B nchange in ⊢ (??(???%)?) with (update ????); whd in ⊢(??%%); >(check_cont_false n2 (update ? p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) q …) [ >(update_o content ?????) [ >(set_cont_outside ?????) //; (* arith *) napply daemon | napply daemon ] | >(update_o content ?????) [ >(set_cont_outside ?????) //; (* arith *) napply daemon | napply daemon ] | napply daemon | napply daemon ] ] qed. lemma getN_setN_overlap: ∀n1,n2,p1,p2,v,m. p1 ≠ p2 → p2 ≤ p1 + Z_of_nat n1 → p1 ≤ p2 + Z_of_nat n2 → getN n2 p2 (setN n1 p1 v m) = Vundef. #n1 #n2 #p1 #p2 #v #m #H #H1 #H2 nchange in ⊢ (??(???%)?) with (update ????); whd in ⊢(??%?);>(update_o content ?????) [lapply (Z_compare_to_Prop p2 p1); lapply (refl ? (Z_compare p2 p1)); cases (Z_compare p2 p1) in ⊢ (???% → %);#H3 [nchange in ⊢ (% → ?) with (p2 < p1);#H4 (* [p1] belongs to [[p2, p2 + n2 - 1]], therefore [check_cont n2 (p2 + 1) ...] is false. *) >(check_cont_false …) [cases (set_cont n1 (p1+oneZ) m p2) [1,3:@ |#n3 #v1 whd in ⊢ (??%?); cases (eqb n2 n3);@ ] |>(update_s content …) @nmk #Hfalse destruct |(*H2*) napply daemon |(*H4*) napply daemon |##skip ] |whd in ⊢ (% → ?);#H4 elim H;#H5 elim (H5 ?);//; |nchange in ⊢ (% → ?) with (p1 < p2);#H4 (* [p2] belongs to [[p1 + 1, p1 + n1 - 1]], therefore [ set_cont n1 (p1 + 1) m p2] is [Cont]. *) >(set_cont_inside …) [@ |(*H1*)napply daemon |(*H4*)napply daemon] ] |//] qed. lemma getN_setN_mismatch: ∀n1,n2,p,v,m. n1 ≠ n2 → getN n2 p (setN n1 p v m) = Vundef. #n1 #n2 #p #v #m #H nchange in ⊢ (??(???%)?) with (update ????); whd in ⊢(??%?);>(update_s content …) whd in ⊢(??%?);>(not_eq_to_eqb_false … (sym_neq … H)) //; qed. lemma getN_setN_characterization: ∀m,v,n1,p1,n2,p2. getN n2 p2 (setN n1 p1 v m) = v ∨ getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m ∨ getN n2 p2 (setN n1 p1 v m) = Vundef. #m #v #n1 #p1 #n2 #p2 lapply (eqZb_to_Prop p1 p2); cases (eqZb p1 p2); #Hp [>Hp @(eqb_elim n1 n2) #Hn [>Hn % % //; |%{2} /2/] |lapply (Z_compare_to_Prop (p1 + n1) p2); cases (Z_compare (p1 + n1) p2);#Hcmp [% %{2} @getN_setN_other /2/ |lapply (Z_compare_to_Prop (p2 + n2) p1); cases (Z_compare (p2 + n2) p1);#Hcmp2 [% %{2} @getN_setN_other /2/ |%{2} @getN_setN_overlap [// |*:(* arith *) napply daemon] |%{2} @getN_setN_overlap [// |*:(* arith *) napply daemon] ] |lapply (Z_compare_to_Prop (p2 + n2) p1); cases (Z_compare (p2 + n2) p1);#Hcmp2 [% %{2} @getN_setN_other /2/ |%{2} @getN_setN_overlap [// |*:(* arith *) napply daemon] |%{2} @getN_setN_overlap [// |*:(* arith *) napply daemon] ] ] ] qed. lemma getN_init: ∀n,p. getN n p (λ_.Undef) = Vundef. #n #p //; qed. *) (* [valid_access m chunk r b ofs] holds if a memory access (load or store) of the given chunk is possible in [m] at address [b, ofs]. This means: - The block [b] is valid. - The range of bytes accessed is within the bounds of [b]. - The offset [ofs] is aligned. - The pointer representation (i.e., region) [r] is compatible with the class of [b]. *) inductive valid_access (m: mem) (chunk: typ) (r: region) (b: block) (ofs: Z) : Prop ≝ | valid_access_intro: valid_block m b → low_bound m b ≤ ofs → ofs + typesize chunk ≤ high_bound m b → (align_chunk chunk ∣ ofs) → pointer_compat b r → valid_access m chunk r b ofs. (* The following function checks whether accessing the given memory chunk at the given offset in the given block respects the bounds of the block. *) (* XXX: Using + and ¬ instead of Sum and Not causes trouble *) let rec in_bounds (m:mem) (chunk:typ) (r:region) (b:block) (ofs:Z) on b : Sum (valid_access m chunk r b ofs) (Not (valid_access m chunk r b ofs)) ≝ ?. cases b #br #bi @(Zltb_elim_Type0 bi (nextblock m)) #Hnext [ @(Zleb_elim_Type0 (low_bound m (mk_block br bi)) ofs) #Hlo [ @(Zleb_elim_Type0 (ofs + typesize chunk) (high_bound m (mk_block br bi))) #Hhi [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal [ cases (pointer_compat_dec (mk_block br bi) r); #Hcl [ %1 % // @Hnext ] ] ] ] ] %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' [ @(absurd ? Hcl' Hcl) | @(absurd ? Hal' Hal) | @(absurd ? Hhi' Hhi) | @(absurd ? Hlo' Hlo) | @(absurd ? Hval Hnext) ] qed. lemma in_bounds_true: ∀m,chunk,r,b,ofs. ∀A: Type[0]. ∀a1,a2: A. valid_access m chunk r b ofs -> (match in_bounds m chunk r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2 ]) = a1. #m #chunk #r #b #ofs #A #a1 #a2 #H cases (in_bounds m chunk r b ofs);normalize;#H1 [// |elim (?:False); @(absurd ? H H1)] qed. (* [valid_pointer] holds if the given block address is valid (and can be represented in a pointer with the region [r]) and the given offset falls within the bounds of the corresponding block. *) definition valid_pointer : mem → pointer → bool ≝ λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧ Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧ Zltb (offv (poff ptr)) (high_bound m (pblock ptr)). (* [load chunk m r b ofs] perform a read in memory state [m], at address [b] and offset [ofs]. [None] is returned if the address is invalid or the memory access is out of bounds or the address cannot be represented by a pointer with region [r]. *) definition load : typ → mem → region → block → Z → option val ≝ λchunk,m,r,b,ofs. match in_bounds m chunk r b ofs with [ inl _ ⇒ Some ? (load_result chunk (getN (pred_size_chunk chunk) ofs (contents (blocks m b)))) | inr _ ⇒ None ? ]. lemma load_inv: ∀chunk,m,r,b,ofs,v. load chunk m r b ofs = Some ? v → valid_access m chunk r b ofs ∧ v = load_result chunk (getN (pred_size_chunk chunk) ofs (contents (blocks m b))). #chunk #m #r #b #ofs #v whd in ⊢ (??%? → ?); cases (in_bounds m chunk r b ofs); #Haccess whd in ⊢ ((??%?) → ?); #H [ % //; destruct; //; | destruct ] qed. (* [loadv chunk m addr] is similar, but the address and offset are given as a single value [addr], which must be a pointer value. *) let rec loadv (chunk:typ) (m:mem) (addr:val) on addr : option val ≝ match addr with [ Vptr ptr ⇒ load chunk m (ptype ptr) (pblock ptr) (offv (poff ptr)) | _ ⇒ None ? ]. (* The memory state [m] after a store of value [v] at offset [ofs] in block [b]. *) definition unchecked_store : typ → mem → block → Z → val → mem ≝ λchunk,m,b,ofs,v. let c ≝ (blocks m b) in mk_mem (update_block ? b (mk_block_contents (low c) (high c) (setN (pred_size_chunk chunk) ofs v (contents c))) (blocks m)) (nextblock m) (nextblock_pos m). (* [store chunk m r b ofs v] perform a write in memory state [m]. Value [v] is stored at address [b] and offset [ofs]. Return the updated memory store, or [None] if the address is invalid or the memory access is out of bounds or the address cannot be represented by a pointer with region [r]. *) definition store : typ → mem → region → block → Z → val → option mem ≝ λchunk,m,r,b,ofs,v. match in_bounds m chunk r b ofs with [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v) | inr _ ⇒ None ? ]. lemma store_inv: ∀chunk,m,r,b,ofs,v,m'. store chunk m r b ofs v = Some ? m' → valid_access m chunk r b ofs ∧ m' = unchecked_store chunk m b ofs v. #chunk #m #r #b #ofs #v #m' whd in ⊢ (??%? → ?); (*9*) cases (in_bounds m chunk r b ofs);#Hv whd in ⊢(??%? → ?);#Heq [% [//|destruct;//] |destruct] qed. (* [storev chunk m addr v] is similar, but the address and offset are given as a single value [addr], which must be a pointer value. *) definition storev : typ → mem → val → val → option mem ≝ λchunk,m,addr,v. match addr with [ Vptr ptr ⇒ store chunk m (ptype ptr) (pblock ptr) (offv (poff ptr)) v | _ ⇒ None ? ]. (* * Properties of the memory operations *) (* ** Properties related to block validity *) lemma valid_not_valid_diff: ∀m,b,b'. valid_block m b → ¬(valid_block m b') → b ≠ b'. #m #b #b' #H #H' @nmk #e >e in H; #H @(absurd ? H H') qed. lemma valid_access_valid_block: ∀m,chunk,r,b,ofs. valid_access m chunk r b ofs → valid_block m b. #m #chunk #r #b #ofs #H elim H;//; qed. lemma valid_access_aligned: ∀m,chunk,r,b,ofs. valid_access m chunk r b ofs → (align_chunk chunk ∣ ofs). #m #chunk #r #b #ofs #H elim H;//; qed. lemma valid_access_compat: ∀m,chunk1,chunk2,r,b,ofs. typesize chunk1 = typesize chunk2 → valid_access m chunk1 r b ofs → valid_access m chunk2 r b ofs. #m #chunk #chunk2 #r #b #ofs #H1 #H2 elim H2;#H3 #H4 #H5 #H6 #H7 >H1 in H5; #H5 % //; <(align_chunk_compat … H1) //; qed. (* Hint Resolve valid_not_valid_diff valid_access_valid_block valid_access_aligned: mem.*) (* ** Properties related to [load] *) theorem valid_access_load: ∀m,chunk,r,b,ofs. valid_access m chunk r b ofs → ∃v. load chunk m r b ofs = Some ? v. #m #chunk #r #b #ofs #H % [2:whd in ⊢ (??%?);@in_bounds_true //; |skip] qed. theorem load_valid_access: ∀m,chunk,r,b,ofs,v. load chunk m r b ofs = Some ? v → valid_access m chunk r b ofs. #m #chunk #r #b #ofs #v #H cases (load_inv … H);//; qed. (* Hint Resolve load_valid_access valid_access_load.*) (* ** Properties related to [store] *) lemma valid_access_store: ∀m1,chunk,r,b,ofs,v. valid_access m1 chunk r b ofs → ∃m2. store chunk m1 r b ofs v = Some ? m2. #m1 #chunk #r #b #ofs #v #H % [2:@in_bounds_true // |skip] qed. (* section STORE *) lemma low_bound_store: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀b'.low_bound m2 b' = low_bound m1 b'. #chunk #m1 #r #b #ofs #v #m2 #STORE #b' cases (store_inv … STORE) #H1 #H2 >H2 whd in ⊢ (??(?%?)?); whd in ⊢ (??%?); whd in ⊢ (??(?%)?); @eq_block_elim #E normalize // qed. lemma nextblock_store : ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → nextblock m2 = nextblock m1. #chunk #m1 #r #b #ofs #v #m2 #STORE cases (store_inv … STORE); #Hvalid #Heq >Heq % qed. lemma high_bound_store: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀b'. high_bound m2 b' = high_bound m1 b'. #chunk #m1 #r #b #ofs #v #m2 #STORE #b' cases (store_inv … STORE); #Hvalid #H >H whd in ⊢ (??(?%?)?);whd in ⊢ (??%?); whd in ⊢ (??(?%)?); @eq_block_elim #E normalize;//; qed. lemma region_store: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀b'. block_region m2 b' = block_region m1 b'. #chunk #m1 #r #b #ofs #v #m2 #STORE * #r #b' // qed. lemma store_valid_block_1: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀b'. valid_block m1 b' → valid_block m2 b'. #chunk #m1 #r #b #ofs #v #m2 #STORE #b' whd in ⊢ (% → %);#Hv >(nextblock_store … STORE) //; qed. lemma store_valid_block_2: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀b'. valid_block m2 b' → valid_block m1 b'. #chunk #m1 #r #b #ofs #v #m2 #STORE #b' whd in ⊢ (%→%); >(nextblock_store … STORE) //; qed. (*Hint Resolve store_valid_block_1 store_valid_block_2: mem.*) lemma store_valid_access_1: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk',r',b',ofs'. valid_access m1 chunk' r' b' ofs' → valid_access m2 chunk' r' b' ofs'. #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #r' #b' #ofs' * as Hv #Hvb #Hl #Hr #Halign #Hptr % //; [@(store_valid_block_1 … STORE) // |>(low_bound_store … STORE …) // |>(high_bound_store … STORE …) // ] qed. lemma store_valid_access_2: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk',r',b',ofs'. valid_access m2 chunk' r' b' ofs' → valid_access m1 chunk' r' b' ofs'. #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #r' #b' #ofs' * as Hv #Hvb #Hl #Hr #Halign #Hcompat % //; [@(store_valid_block_2 … STORE) // |<(low_bound_store … STORE …) // |<(high_bound_store … STORE …) // ] qed. lemma store_valid_access_3: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → valid_access m1 chunk r b ofs. #chunk #m1 #r #b #ofs #v #m2 #STORE cases (store_inv … STORE);//; qed. (*Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3: mem.*) lemma load_compat_pointer: ∀chunk,m,r,r',b,ofs,v. pointer_compat b r' → load chunk m r b ofs = Some ? v → load chunk m r' b ofs = Some ? v. #chunk #m #r #r' #b #ofs #v #Hcompat #LOAD lapply (load_valid_access … LOAD); #Hvalid cut (valid_access m chunk r' b ofs); [ % elim Hvalid; //; | #Hvalid' (in_bounds_true … (option val) ?? Hvalid) >(in_bounds_true … (option val) ?? Hvalid') // ] qed. (* Nonessential properties that may require arithmetic theorem load_store_similar: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk'. size_chunk chunk' = size_chunk chunk → load chunk' m2 r b ofs = Some ? (load_result chunk' v). #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #Hsize cases (store_inv … STORE); #Hv #Heq whd in ⊢ (??%?); nrewrite > (in_bounds_true m2 chunk' r b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b))))) (None ?) ?); [>Heq whd in ⊢ (??(??(? ? (? ? ? (? (? % ?)))))?); >(update_s ? b ? (blocks m1)) (* XXX too many metas for my taste *) >(? : pred_size_chunk chunk = pred_size_chunk chunk') [//; |>(size_chunk_pred …) in Hsize #Hsize >(size_chunk_pred …) in Hsize #Hsize @injective_Z_of_nat @(injective_Zplus_r 1) //;] |@(store_valid_access_1 … STORE) cases Hv;#H1 #H2 #H3 #H4 #H5 % //; >(align_chunk_compat … Hsize) //] qed. theorem load_store_same: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → load chunk m2 r b ofs = Some ? (load_result chunk v). #chunk #m1 #r #b #ofs #v #m2 #STORE @load_store_similar //; qed. theorem load_store_other: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk',r',b',ofs'. b' ≠ b ∨ ofs' + size_chunk chunk' ≤ ofs ∨ ofs + size_chunk chunk ≤ ofs' → load chunk' m2 r' b' ofs' = load chunk' m1 r' b' ofs'. #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #r' #b' #ofs' #H cases (store_inv … STORE); #Hvalid #Heq whd in ⊢ (??%%); cases (in_bounds m1 chunk' r' b' ofs'); [#Hvalid1 >(in_bounds_true m2 chunk' r' b' ofs' ? (Some ? ?) ??) [whd in ⊢ (???%); @(eq_f … (Some val)) @(eq_f … (load_result chunk')) >Heq whd in ⊢ (??(???(? (? % ?)))?); whd in ⊢ (??(???(? %))?); lapply (eqZb_to_Prop b' b);cases (eqZb b' b); whd in ⊢ (% → ?); [#Heq1 >Heq1 whd in ⊢ (??(??? (? %))?); >(size_chunk_pred …) in H >(size_chunk_pred …) #H @(getN_setN_other …) cases H [* [#Hfalse elim Hfalse;#H1 elim (H1 Heq1) |#H1 %{2} (*H1*)napply daemon ] |#H1 % (*H1*)napply daemon ] |#Hneq @ ] |@(store_valid_access_1 … STORE) //] |whd in ⊢ (? → ???%);lapply (in_bounds m2 chunk' r' b' ofs'); #H1 cases H1; [#H2 #H3 lapply (store_valid_access_2 … STORE … H2);#Hfalse cases H3;#H4 elim (H4 Hfalse) |#H2 #H3 @] ] qed. theorem load_store_overlap: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk',ofs',v'. load chunk' m2 r b ofs' = Some ? v' → ofs' ≠ ofs → ofs < ofs' + size_chunk chunk' → ofs' < ofs + size_chunk chunk → v' = Vundef. #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #ofs' #v' #H #H1 #H2 #H3 cases (store_inv … STORE); cases (load_inv … H); #Hvalid #Heq #Hvalid1 #Heq1 >Heq >Heq1 nchange in ⊢ (??(??(???(?(?%?))))?) with (mk_mem ???); >(update_s block_contents …) >(getN_setN_overlap …) [cases chunk';// |>(size_chunk_pred …) in H2 (*arith*) napply daemon |>(size_chunk_pred …) in H3 (*arith*) napply daemon |@sym_neq //] qed. theorem load_store_overlap': ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk',ofs'. valid_access m1 chunk' r b ofs' → ofs' ≠ ofs → ofs < ofs' + size_chunk chunk' → ofs' < ofs + size_chunk chunk → load chunk' m2 r b ofs' = Some ? Vundef. #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #ofs' #Hvalid #H #H1 #H2 cut (∃v'.load chunk' m2 r b ofs' = Some ? v') [@valid_access_load @(store_valid_access_1 … STORE) // |#H3 cases H3; #x #Hx >Hx @(eq_f … (Some val)) @(load_store_overlap … STORE … Hx) //;] qed. theorem load_store_mismatch: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk',v'. load chunk' m2 r b ofs = Some ? v' → size_chunk chunk' ≠ size_chunk chunk → v' = Vundef. #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #v' #H #H1 cases (store_inv … STORE); cases (load_inv … H); #Hvalid #H2 #Hvalid1 #H3 >H2 nchange in H3:(???%) with (mk_mem ???); >H3 >(update_s block_contents …) >(getN_setN_mismatch …) [cases chunk';//; |>(size_chunk_pred …) in H1 >(size_chunk_pred …) #H1 @nmk #Hfalse elim H1;#H4 @H4 @(eq_f ?? (λx.1 + x) ???) //] qed. theorem load_store_mismatch': ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk'. valid_access m1 chunk' r b ofs → size_chunk chunk' ≠ size_chunk chunk → load chunk' m2 r b ofs = Some ? Vundef. #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #Hvalid #Hsize cut (∃v'.load chunk' m2 r b ofs = Some ? v') [@(valid_access_load …) napply (store_valid_access_1 … STORE);// |*;#x #Hx >Hx @(eq_f … (Some val)) @(load_store_mismatch … STORE … Hsize) //;] qed. inductive load_store_cases (chunk1: memory_chunk) (b1: block) (ofs1: Z) (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type[0] ≝ | lsc_similar: b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 = size_chunk chunk2 → load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 | lsc_other: b1 ≠ b2 ∨ ofs2 + size_chunk chunk2 ≤ ofs1 ∨ ofs1 + size_chunk chunk1 ≤ ofs2 → load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 | lsc_overlap: b1 = b2 -> ofs1 ≠ ofs2 -> ofs1 < ofs2 + size_chunk chunk2 → ofs2 < ofs1 + size_chunk chunk1 -> load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 | lsc_mismatch: b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 ≠ size_chunk chunk2 -> load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2. definition load_store_classification: ∀chunk1,b1,ofs1,chunk2,b2,ofs2. load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2. #chunk1 #b1 #ofs1 #chunk2 #b2 #ofs2 cases (decidable_eq_Z_Type b1 b2);#H [cases (decidable_eq_Z_Type ofs1 ofs2);#H1 [cases (decidable_eq_Z_Type (size_chunk chunk1) (size_chunk chunk2));#H2 [@lsc_similar //; |@lsc_mismatch //;] |lapply (Z_compare_to_Prop (ofs2 + size_chunk chunk2) ofs1); cases (Z_compare (ofs2+size_chunk chunk2) ofs1); [nchange with (Zlt ? ? → ?);#H2 @lsc_other % %{2} (*trivial Zlt_to_Zle BUT the statement is strange*) napply daemon |nchange with (? = ? → ?);#H2 @lsc_other % %{2} (*trivial eq_to_Zle not defined *) napply daemon |nchange with (Zlt ? ? → ?);#H2 lapply (Z_compare_to_Prop (ofs1 + size_chunk chunk1) ofs2); cases (Z_compare (ofs1 + size_chunk chunk1) ofs2); [nchange with (Zlt ? ? → ?);#H3 @lsc_other %{2} (*trivial as previously*) napply daemon |nchange with (? = ? → ?);#H3 @lsc_other %{2} (*trivial as previously*) napply daemon |nchange with (Zlt ? ? → ?);#H3 @lsc_overlap //;] ] ] |@lsc_other % % (* XXX // doesn't spot this! *) napply H ] qed. theorem load_store_characterization: ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → ∀chunk',r',b',ofs'. valid_access m1 chunk' r' b' ofs' → load chunk' m2 r' b' ofs' = match load_store_classification chunk b ofs chunk' b' ofs' with [ lsc_similar _ _ _ ⇒ Some ? (load_result chunk' v) | lsc_other _ ⇒ load chunk' m1 r' b' ofs' | lsc_overlap _ _ _ _ ⇒ Some ? Vundef | lsc_mismatch _ _ _ ⇒ Some ? Vundef ]. #chunk #m1 #r #b #ofs #v #m2 #STORE #chunk' #r' #b' #ofs' #Hvalid cut (∃v'. load chunk' m2 r' b' ofs' = Some ? v') [@valid_access_load @(store_valid_access_1 … STORE … Hvalid) |*;#x #Hx cases (load_store_classification chunk b ofs chunk' b' ofs') [#H1 #H2 #H3 whd in ⊢ (???%);

(region_store … STORE b) cases Hvalid; //; | @(load_store_similar … STORE) //; ] |#H1 @(load_store_other … STORE) cases H1 [* [#H2 % % @sym_neq // |#H2 % %{2} //] |#H2 %{2} //] |#H1 #H2 #H3 #H4 lapply (load_compat_pointer … r … Hx); [ >(region_store … STORE b') >H1 elim (store_valid_access_3 … STORE); // |

Hx @(eq_f … (Some val)) @(load_store_overlap … STORE … Hx') /2/; ] |#H1 #H2 #H3 lapply (load_compat_pointer … r … Hx); [ >(region_store … STORE b') >H1 elim (store_valid_access_3 … STORE); // |

Hx @(eq_f … (Some val)) @(load_store_mismatch … STORE … Hx') /2/ ] ] ] qed. (*lemma d : ∀a,b,c,d:nat.∀e:〈a,b〉 = 〈c,d〉. ∀P:(∀a,b,c,d,e.Prop). P a b c d e → P a b a b (refl ??). #a #b #c #d #e #P #H1 destruct;*) (* Section ALLOC. Variable m1: mem. Variables lo hi: Z. Variable m2: mem. Variable b: block. Hypothesis ALLOC: alloc m1 lo hi = (m2, b). *) definition pairdisc ≝ λA,B.λx,y:Prod A B. match x with [(pair t0 t1) ⇒ match y with [(pair u0 u1) ⇒ ∀P: Type[1]. (∀e0: (eq A (R0 ? t0) u0). ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ]. lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y. #A #B #x #y #e >e cases y; #a #b normalize;#P #PH @PH % qed. lemma nextblock_alloc: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → nextblock m2 = Zsucc (nextblock m1). #m1 #lo #hi #bcl #m2 #b #ALLOC whd in ALLOC:(??%%); destruct; //; qed. lemma alloc_result: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → b = nextblock m1. #m1 #lo #hi #bcl #m2 #b #ALLOC whd in ALLOC:(??%%); destruct; //; qed. lemma valid_block_alloc: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀b'. valid_block m1 b' → valid_block m2 b'. #m1 #lo #hi #bcl #m2 #b #ALLOC #b' >(unfold_valid_block m1 b') >(unfold_valid_block m2 b') >(nextblock_alloc … ALLOC) (* arith *) @daemon qed. lemma fresh_block_alloc: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ¬(valid_block m1 b). #m1 #lo #hi #bcl #m2 #b #ALLOC >(unfold_valid_block m1 b) >(alloc_result … ALLOC) (* arith *) @daemon qed. lemma valid_new_block: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → valid_block m2 b. #m1 #lo #hi #bcl #m2 #b #ALLOC >(unfold_valid_block m2 b) >(alloc_result … ALLOC) >(nextblock_alloc … ALLOC) (* arith *) @daemon qed. (* Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. *) lemma valid_block_alloc_inv: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀b'. valid_block m2 b' → b' = b ∨ valid_block m1 b'. #m1 #lo #hi #bcl #m2 #b #ALLOC #b' >(unfold_valid_block m2 b') >(unfold_valid_block m1 b') >(nextblock_alloc … ALLOC) #H >(alloc_result … ALLOC) (* arith *) @daemon qed. lemma low_bound_alloc: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀b'. low_bound m2 b' = if eqZb b' b then lo else low_bound m1 b'. #m1 #lo #hi #bcl #m2 #b #ALLOC whd in ALLOC:(??%%); destruct; #b' >(unfold_update block_contents ????) cases (eqZb b' (nextblock m1)); //; qed. lemma low_bound_alloc_same: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → low_bound m2 b = lo. #m1 #lo #hi #bcl #m2 #b #ALLOC >(low_bound_alloc … ALLOC b) >(eqZb_z_z …) //; qed. lemma low_bound_alloc_other: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀b'. valid_block m1 b' → low_bound m2 b' = low_bound m1 b'. #m1 #lo #hi #bcl #m2 #b #ALLOC #b' >(low_bound_alloc … ALLOC b') @eqZb_elim #Hb [ >Hb #bad @False_ind @(absurd ? bad) napply (fresh_block_alloc … ALLOC) | // ] qed. lemma high_bound_alloc: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀b'. high_bound m2 b' = if eqZb b' b then hi else high_bound m1 b'. #m1 #lo #hi #bcl #m2 #b #ALLOC whd in ALLOC:(??%%); destruct; #b' >(unfold_update block_contents ????) cases (eqZb b' (nextblock m1)); //; qed. lemma high_bound_alloc_same: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → high_bound m2 b = hi. #m1 #lo #hi #bcl #m2 #b #ALLOC >(high_bound_alloc … ALLOC b) >(eqZb_z_z …) //; qed. lemma high_bound_alloc_other: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀b'. valid_block m1 b' → high_bound m2 b' = high_bound m1 b'. #m1 #lo #hi #bcl #m2 #b #ALLOC #b' >(high_bound_alloc … ALLOC b') @eqZb_elim #Hb [ >Hb #bad @False_ind @(absurd ? bad) napply (fresh_block_alloc … ALLOC) | // ] qed. lemma class_alloc: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀b'.block_region m2 b' = if eqZb b' b then bcl else block_region m1 b'. #m1 #lo #hi #bcl #m2 #b #ALLOC whd in ALLOC:(??%%); destruct; #b' cases (eqZb b' (nextblock m1)); //; qed. lemma class_alloc_same: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → block_region m2 b = bcl. #m1 #lo #hi #bcl #m2 #b #ALLOC whd in ALLOC:(??%%); destruct; >(eqZb_z_z ?) //; qed. lemma class_alloc_other: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀b'. valid_block m1 b' → block_region m2 b' = block_region m1 b'. #m1 #lo #hi #bcl #m2 #b #ALLOC #b' >(class_alloc … ALLOC b') @eqZb_elim #Hb [ >Hb #bad @False_ind @(absurd ? bad) napply (fresh_block_alloc … ALLOC) | // ] qed. lemma valid_access_alloc_other: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀chunk,r,b',ofs. valid_access m1 chunk r b' ofs → valid_access m2 chunk r b' ofs. #m1 #lo #hi #bcl #m2 #b #ALLOC #chunk #r #b' #ofs #H cases H; #Hvalid #Hlow #Hhigh #Halign #Hcompat % [ @(valid_block_alloc … ALLOC) // | >(low_bound_alloc_other … ALLOC b' Hvalid) // | >(high_bound_alloc_other … ALLOC b' Hvalid) // | // | >(class_alloc_other … ALLOC b' Hvalid) //; ] qed. lemma valid_access_alloc_same: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀chunk,r,ofs. lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) → pointer_compat bcl r → valid_access m2 chunk r b ofs. #m1 #lo #hi #bcl #m2 #b #ALLOC #chunk #r #ofs #Hlo #Hhi #Halign #Hcompat % [ napply (valid_new_block … ALLOC) | >(low_bound_alloc_same … ALLOC) // | >(high_bound_alloc_same … ALLOC) // | // | >(class_alloc_same … ALLOC) // ] qed. (* Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. *) lemma valid_access_alloc_inv: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀chunk,r,b',ofs. valid_access m2 chunk r b' ofs → valid_access m1 chunk r b' ofs ∨ (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl r)). #m1 #lo #hi #bcl #m2 #b #ALLOC #chunk #r #b' #ofs *;#Hblk #Hlo #Hhi #Hal #Hct elim (valid_block_alloc_inv … ALLOC ? Hblk);#H [ (low_bound_alloc_same … ALLOC') in Hlo #Hlo' >(high_bound_alloc_same … ALLOC') in Hhi #Hhi' >(class_alloc_same … ALLOC') in Hct #Hct %{2} /4/; | %{1} % //; [ >(low_bound_alloc_other … ALLOC ??) in Hlo // | >(high_bound_alloc_other … ALLOC ??) in Hhi // | >(class_alloc_other … ALLOC ??) in Hct // ] ] qed. theorem load_alloc_unchanged: ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 → ∀chunk,r,b',ofs. valid_block m1 b' → load chunk m2 r b' ofs = load chunk m1 r b' ofs. #m1 #lo #hi #bcl #m2 #b #ALLOC #chunk #r #b' #ofs #H whd in ⊢ (??%%); cases (in_bounds m2 chunk r b' ofs); #H' [ elim (valid_access_alloc_inv … ALLOC ???? H'); [ #H'' (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error >(in_bounds_true ???? ??? H'') *) >(in_bounds_true … ? (option val) ?? H'') whd in ⊢ (??%?); (* XXX: if you do this at the point below the proof term is ill-typed. *) cut (b' ≠ b); [ @(valid_not_valid_diff … H) @(fresh_block_alloc … ALLOC) | whd in ALLOC:(??%%); destruct; >(update_o block_contents ?????) /2/; ] | *;*;#A #B #C H1 whd in ALLOC:(??%%); (* XXX destruct; ??? *) @(pairdisc_elim … ALLOC) whd in ⊢ (??%% → ?);#e0 (update_s ? ? (empty_block lo hi bcl) ?) normalize; cases chunk; //; qed. theorem load_alloc_same': ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → ∀chunk,r,ofs. lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) → pointer_compat bcl r → load chunk m2 r b ofs = Some ? Vundef. #m1 #lo #hi #bcl #m2 #b #ALLOC #chunk #r #ofs #Hlo #Hhi #Hal #Hct cut (∃v. load chunk m2 r b ofs = Some ? v); [ @valid_access_load % //; [ @(valid_new_block … ALLOC) | >(low_bound_alloc_same … ALLOC) // | >(high_bound_alloc_same … ALLOC) // | >(class_alloc_same … ALLOC) // ] | *; #v #LOAD >LOAD @(eq_f … (Some val)) @(load_alloc_same … ALLOC … LOAD) ] qed. (* End ALLOC. Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. Hint Resolve load_alloc_unchanged: mem. *) (* ** Properties related to [free]. *) (* Section FREE. Variable m: mem. Variable bf: block. *) lemma valid_block_free_1: ∀m,bf,b. valid_block m b → valid_block (free m bf) b. normalize;//; qed. lemma valid_block_free_2: ∀m,bf,b. valid_block (free m bf) b → valid_block m b. normalize;//; qed. (* Hint Resolve valid_block_free_1 valid_block_free_2: mem. *) lemma low_bound_free: ∀m,bf,b. b ≠ bf -> low_bound (free m bf) b = low_bound m b. #m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); >(update_o block_contents …) //; @sym_neq //; qed. lemma high_bound_free: ∀m,bf,b. b ≠ bf → high_bound (free m bf) b = high_bound m b. #m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); >(update_o block_contents …) //; @sym_neq //; qed. lemma low_bound_free_same: ∀m,b. low_bound (free m b) b = 0. #m #b whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); >(update_s block_contents …) //; qed. lemma high_bound_free_same: ∀m,b. high_bound (free m b) b = 0. #m #b whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); >(update_s block_contents …) //; qed. lemma class_free: ∀m,bf,b. b ≠ bf → block_region (free m bf) b = block_region m b. #m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); >(update_o block_contents …) //; @sym_neq //; qed. lemma valid_access_free_1: ∀m,bf,chunk,r,b,ofs. valid_access m chunk r b ofs → b ≠ bf → valid_access (free m bf) chunk r b ofs. #m #bf #chunk #r #b #ofs *;#Hval #Hlo #Hhi #Hal #Hcompat #Hneq % //; [ @valid_block_free_1 // | >(low_bound_free … Hneq) // | >(high_bound_free … Hneq) // | >(class_free … Hneq) // ] qed. lemma valid_access_free_2: ∀m,r,bf,chunk,ofs. ¬(valid_access (free m bf) chunk r bf ofs). #m #r #bf #chunk #ofs @nmk *; #Hval #Hlo #Hhi #Hal #Hct whd in Hlo:(?%?);whd in Hlo:(?(?(?%?))?); >(update_s block_contents …) in Hlo whd in Hhi:(??%);whd in Hhi:(??(?(?%?))); >(update_s block_contents …) in Hhi whd in ⊢ ((??%)→(?%?)→?); (* arith *) @daemon qed. (* Hint Resolve valid_access_free_1 valid_access_free_2: mem. *) lemma valid_access_free_inv: ∀m,bf,chunk,r,b,ofs. valid_access (free m bf) chunk r b ofs → valid_access m chunk r b ofs ∧ b ≠ bf. #m #bf #chunk #r #b #ofs elim (decidable_eq_Z_Type b bf); [ #e >e #H @False_ind @(absurd ? H (valid_access_free_2 …)) | #ne *; >(low_bound_free … ne) >(high_bound_free … ne) >(class_free … ne) #Hval #Hlo #Hhi #Hal #Hct % [ % /2/; | /2/ ] ] qed. theorem load_free: ∀m,bf,chunk,r,b,ofs. b ≠ bf → load chunk (free m bf) r b ofs = load chunk m r b ofs. #m #bf #chunk #r #b #ofs #ne whd in ⊢ (??%%); elim (in_bounds m chunk r b ofs); [ #Hval whd in ⊢ (???%); >(in_bounds_true ????? (option val) ???) [ whd in ⊢ (??(??(??(???(?(?%?)))))?); >(update_o block_contents …) //; @sym_neq // | @valid_access_free_1 //; @ne ] | elim (in_bounds (free m bf) chunk r b ofs); (* XXX just // used to work *) [ 2: normalize; //; ] #H #H' @False_ind @(absurd ? ? H') elim (valid_access_free_inv …H); //; ] qed. (* End FREE. *) (* ** Properties related to [free_list] *) lemma valid_block_free_list_1: ∀bl,m,b. valid_block m b → valid_block (free_list m bl) b. #bl elim bl; [ #m #b #H whd in ⊢ (?%?); // | #h #t #IH #m #b #H >(unfold_free_list m h t) @valid_block_free_1 @IH // ] qed. lemma valid_block_free_list_2: ∀bl,m,b. valid_block (free_list m bl) b → valid_block m b. #bl elim bl; [ #m #b #H whd in H:(?%?); // | #h #t #IH #m #b >(unfold_free_list m h t) #H @IH @valid_block_free_2 // ] qed. lemma valid_access_free_list: ∀chunk,r,b,ofs,m,bl. valid_access m chunk r b ofs → ¬in_list ? b bl → valid_access (free_list m bl) chunk r b ofs. #chunk #r #b #ofs #m #bl elim bl; [ whd in ⊢ (?→?→(?%????)); // | #h #t #IH #H #notin >(unfold_free_list m h t) @valid_access_free_1 [ @IH //; @(not_to_not ??? notin) #Ht napply (in_list_cons … Ht) | @nmk #e @(absurd ?? notin) >e // ] ] qed. lemma valid_access_free_list_inv: ∀chunk,r,b,ofs,m,bl. valid_access (free_list m bl) chunk r b ofs → ¬in_list ? b bl ∧ valid_access m chunk r b ofs. #chunk #r #b #ofs #m #bl elim bl; [ whd in ⊢ ((?%????)→?); #H % // | #h #t #IH >(unfold_free_list m h t) #H elim (valid_access_free_inv … H); #H' #ne elim (IH H'); #notin #H'' % //; @(not_to_not ??? notin) #Ht (* WTF? this is specialised to nat! @(in_list_tail t b h) *) napply daemon ] qed. (* ** Properties related to pointer validity *) lemma valid_pointer_valid_access: ∀m,r,b,ofs. valid_pointer m r b ofs = true ↔ valid_access m Mint8unsigned r b ofs. #m #r #b #ofs whd in ⊢ (?(??%?)?); % [ #H lapply (andb_true_l … H); #H' lapply (andb_true_l … H'); #H'' lapply (andb_true_l … H''); #H1 lapply (andb_true_r … H''); #H2 lapply (andb_true_r … H'); #H3 lapply (andb_true_r … H); #H4 % [ >(unfold_valid_block m b) napply (Zltb_true_to_Zlt … H1) | napply (Zleb_true_to_Zle … H2) | whd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon | cases ofs; /2/; | whd in H4:(??%?); elim (pointer_compat_dec (block_region m b) r) in H4; [ //; | #Hn #e whd in e:(??%%); destruct ] ] | *; #Hval #Hlo #Hhi #Hal #Hct >(Zlt_to_Zltb_true … Hval) >(Zle_to_Zleb_true … Hlo) whd in Hhi:(?(??%)?); >(Zlt_to_Zltb_true … ?) [ whd in ⊢ (??%?); elim (pointer_compat_dec (block_region m b) r); [ //; | #Hct' @False_ind @(absurd … Hct Hct') ] | (* arith *) napply daemon ] ] qed. theorem valid_pointer_alloc: ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,r. ∀b,b': block. ∀ofs: Z. alloc m1 lo hi bcl = 〈m2, b'〉 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true. #m1 #m2 #lo #hi #bcl #r #b #b' #ofs #ALLOC #VALID lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval @(proj2 ?? (valid_pointer_valid_access ????)) @(valid_access_alloc_other … ALLOC … Hval) qed. theorem valid_pointer_store: ∀chunk: memory_chunk. ∀m1,m2: mem. ∀r,r': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val. store chunk m1 r' b' ofs' v = Some ? m2 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true. #chunk #m1 #m2 #r #r' #b #b' #ofs #ofs' #v #STORE #VALID lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval @(proj2 ?? (valid_pointer_valid_access ????)) @(store_valid_access_1 … STORE … Hval) qed. (* * * Generic injections between memory states. *) (* (* Section GENERIC_INJECT. *) definition meminj : Type[0] ≝ block → option (block × Z). (* Variable val_inj: meminj -> val -> val -> Prop. Hypothesis val_inj_undef: ∀mi. val_inj mi Vundef Vundef. *) definition mem_inj ≝ λval_inj.λmi: meminj. λm1,m2: mem. ∀chunk, b1, ofs, v1, b2, delta. mi b1 = Some ? 〈b2, delta〉 → load chunk m1 b1 ofs = Some ? v1 → ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2. (* FIXME: another nunfold hack*) lemma unfold_mem_inj : ∀val_inj.∀mi: meminj. ∀m1,m2: mem. (mem_inj val_inj mi m1 m2) = (∀chunk, b1, ofs, v1, b2, delta. mi b1 = Some ? 〈b2, delta〉 → load chunk m1 b1 ofs = Some ? v1 → ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2). //; qed. lemma valid_access_inj: ∀val_inj. ∀mi,m1,m2,chunk,b1,ofs,b2,delta. mi b1 = Some ? 〈b2, delta〉 → mem_inj val_inj mi m1 m2 → valid_access m1 chunk b1 ofs → valid_access m2 chunk b2 (ofs + delta). #val_inj #mi #m1 #m2 #chunk #b1 #ofs #b2 #delta #H #Hinj #Hval cut (∃v1. load chunk m1 b1 ofs = Some ? v1); [ /2/; | *;#v1 #LOAD1 elim (Hinj … H LOAD1);#v2 *;#LOAD2 #VCP /2/ ] qed. (*Hint Resolve valid_access_inj: mem.*) *) (* FIXME: can't use destruct below *) lemma grumpydestruct : ∀A,v. None A = Some A v → False. #A #v #H destruct; qed. (* lemma store_unmapped_inj: ∀val_inj. ∀mi,m1,m2,r,b,ofs,v,chunk,m1'. mem_inj val_inj mi m1 m2 → mi b = None ? → store chunk m1 r b ofs v = Some ? m1' → mem_inj val_inj mi m1' m2. #val_inj #mi #m1 #m2 #r #b #ofs #v #chunk #m1' #Hinj #Hmi #Hstore whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload cut (load chunk0 m1 b1 ofs0 = Some ? v1); [ eq in Hmi0 >Hmi #H destruct; | #Hload' @(Hinj … Hmi0 Hload') ] qed. lemma store_outside_inj: ∀val_inj. ∀mi,m1,m2,chunk,r,b,ofs,v,m2'. mem_inj val_inj mi m1 m2 → (∀b',delta. mi b' = Some ? 〈b, delta〉 → high_bound m1 b' + delta ≤ ofs ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) → store chunk m2 r b ofs v = Some ? m2' → mem_inj val_inj mi m1 m2'. #val_inj #mi #m1 #m2 #chunk #r #b #ofs #v #m2' #Hinj #Hbounds #Hstore whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload lapply (Hinj … Hmi0 Hload);*;#v2 *;#LOAD2 #VINJ %{ v2} % //; Heq in Hmi0 LOAD2 #Hmi0 #LOAD2 lapply (Hbounds … Hmi0); #Hb cut (valid_access m1 chunk0 b1 ofs0); /2/; #Hv elim Hv; #Hv1 #Hlo1 #Hhi1 #Hal1 elim Hb; #Hb [ %{1} %{2} (* arith *) napply daemon | %{2} (* arith *) napply daemon ] | #ineq %{1} %{1} @ineq ] qed. (* XXX: use Or rather than ∨ to bring resource usage under control. *) definition meminj_no_overlap ≝ λmi: meminj. λm: mem. ∀b1,b1',delta1,b2,b2',delta2. b1 ≠ b2 → mi b1 = Some ? 〈b1', delta1〉 → mi b2 = Some ? 〈b2', delta2〉 → Or (Or (Or (b1' ≠ b2') (low_bound m b1 ≥ high_bound m b1)) (low_bound m b2 ≥ high_bound m b2)) (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2) (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)). *) (* FIXME *) lemma grumpydestruct1 : ∀A,x1,x2. Some A x1 = Some A x2 → x1 = x2. #A #x1 #x2 #H destruct;//; qed. lemma grumpydestruct2 : ∀A,B,x1,y1,x2,y2. Some (A×B) 〈x1,y1〉 = Some (A×B) 〈x2,y2〉 → x1 = x2 ∧ y1 = y2. #A #B #x1 #y1 #x2 #y2 #H destruct;/2/; qed. (* lemma store_mapped_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef. ∀mi,m1,m2,b1,ofs,b2,delta,v1,v2,chunk,m1'. mem_inj val_inj mi m1 m2 → meminj_no_overlap mi m1 → mi b1 = Some ? 〈b2, delta〉 → store chunk m1 b1 ofs v1 = Some ? m1' → (∀chunk'. size_chunk chunk' = size_chunk chunk → val_inj mi (load_result chunk' v1) (load_result chunk' v2)) → ∃m2'. store chunk m2 b2 (ofs + delta) v2 = Some ? m2' ∧ mem_inj val_inj mi m1' m2'. #val_inj #val_inj_undef #mi #m1 #m2 #b1 #ofs #b2 #delta #v1 #v2 #chunk #m1' #Hinj #Hnoover #Hb1 #STORE #Hvalinj cut (∃m2'.store chunk m2 b2 (ofs + delta) v2 = Some ? m2'); [ @valid_access_store @(valid_access_inj ? mi ??????? Hb1 Hinj ?) (* XXX why do I have to give mi here? *) /2/ | *;#m2' #STORE2 %{ m2'} % //; whd; #chunk' #b1' #ofs' #v #b2' #delta' #CP #LOAD1 cut (valid_access m1 chunk' b1' ofs'); [ @(store_valid_access_2 … STORE) @(load_valid_access … LOAD1) | #Hval lapply (load_store_characterization … STORE … Hval); elim (load_store_classification chunk b1 ofs chunk' b1' ofs'); [ #e #e0 #e1 #H (* similar *) >e in Hb1 #Hb1 >CP in Hb1 #Hb1 (* XXX destruct expands proof state too much;*) elim (grumpydestruct2 ?????? Hb1); #e2 #e3 e2 >e3 %{ (load_result chunk' v2)} % [ @(load_store_similar … STORE2) // | >LOAD1 in H #H whd in H:(??%%); destruct; @Hvalinj //; ] | #Hdis #H (* disjoint *) >LOAD1 in H #H lapply (Hinj … CP ?); [ @sym_eq @H | *: ] *;#v2' *;#LOAD2 #VCP %{ v2'} % //; CP in Hb1 #eb2d elim (grumpydestruct2 ?????? eb2d); #eb2 #ed elim Hdis; [ #Hdis elim Hdis; [ #eb1' @False_ind @(absurd ? eb1 eb1') | #Hdis %{1} %{2} (* arith *) napply daemon ] | #Hdis %{2} (* arith *) napply daemon ] | cut (valid_access m1 chunk b1 ofs); /2/; #Hval' lapply (Hnoover … eb1 Hb1 CP); #Ha elim Ha; #Ha [ elim Ha; #Ha [ elim Ha; #Ha [ %{1} %{1} /2/ | elim Hval'; lapply (size_chunk_pos chunk); (* arith *) napply daemon ] | elim Hval; lapply (size_chunk_pos chunk'); (* arith *) napply daemon ] | elim Hval'; elim Hval; (* arith *) napply daemon ] ] | #eb1 #Hofs1 #Hofs2 #Hofs3 #H (* overlapping *) CP in Hb1 #eb2d elim (grumpydestruct2 ?????? eb2d); #eb2 #ed cut (∃v2'. load chunk' m2' b2 (ofs' + delta) = Some ? v2'); [ @valid_access_load @(store_valid_access_1 … STORE2) @(valid_access_inj … Hinj Hval) >eb1 // | *;#v2' #LOAD2' cut (v2' = Vundef); [ @(load_store_overlap … STORE2 … LOAD2') (* arith *) napply daemon | ] #ev2' %{ v2'} % //; >LOAD1 in H #H whd in H:(??%%); >(grumpydestruct1 … H) >ev2' @val_inj_undef ] | #eb1 #Hofs CP in Hb1 #eb2d elim (grumpydestruct2 ?????? eb2d); #eb2 #ed cut (∃v2'. load chunk' m2' b2 (ofs + delta) = Some ? v2'); [ @valid_access_load @(store_valid_access_1 … STORE2) @(valid_access_inj … Hinj Hval) >eb1 // | *;#v2' #LOAD2' cut (v2' = Vundef); [ @(load_store_mismatch … STORE2 … LOAD2' ?) @sym_neq // | ] #ev2' %{ v2'} % //; >LOAD1 in H #H whd in H:(??%%); >(grumpydestruct1 … H) >ev2' @val_inj_undef ] ] ] ] qed. definition inj_offset_aligned ≝ λdelta: Z. λsize: Z. ∀chunk. size_chunk chunk ≤ size → (align_chunk chunk ∣ delta). lemma alloc_parallel_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef. ∀mi,m1,m2,lo1,hi1,m1',b1,lo2,hi2,m2',b2,delta. mem_inj val_inj mi m1 m2 → alloc m1 lo1 hi1 = 〈m1', b1〉 → alloc m2 lo2 hi2 = 〈m2', b2〉 → mi b1 = Some ? 〈b2, delta〉 → lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 → inj_offset_aligned delta (hi1 - lo1) → mem_inj val_inj mi m1' m2'. #val_inj #val_inj_undef #mi #m1 #m2 #lo1 #hi1 #m1' #b1 #lo2 #hi2 #m2' #b2 #delta #Hinj #ALLOC1 #ALLOC2 #Hbinj #Hlo #Hhi #Hal whd; #chunk #b1' #ofs #v #b2' #delta' #Hbinj' #LOAD lapply (valid_access_alloc_inv … m1 … ALLOC1 chunk b1' ofs ?); /2/; *; [ #A cut (load chunk m1 b1' ofs = Some ? v); [ A in Hbinj' LOAD #Hbinj' #LOAD >Hbinj in Hbinj' #Hbinj' elim (grumpydestruct2 ?????? Hbinj'); #eb2 #edelta ev cut (∃v2. load chunk m2' b2 (ofs + delta) = Some ? v2); [ @valid_access_load @(valid_access_alloc_same … ALLOC2) [ 1,2: (*arith*) @daemon | (* arith using Hal *) napply daemon ] ] *;#v2 #LOAD2 cut (v2 = Vundef); [ napply (load_alloc_same … ALLOC2 … LOAD2) ] #ev2 >ev2 %{ Vundef} % //; ] qed. lemma alloc_right_inj: ∀val_inj. ∀mi,m1,m2,lo,hi,b2,m2'. mem_inj val_inj mi m1 m2 → alloc m2 lo hi = 〈m2', b2〉 → mem_inj val_inj mi m1 m2'. #val_inj #mi #m1 #m2 #lo #hi #b2 #m2' #Hinj #ALLOC whd; #chunk #b1 #ofs #v1 #b2' #delta #Hbinj #LOAD lapply (Hinj … Hbinj LOAD); *; #v2 *;#LOAD2 #VINJ %{ v2} % //; cut (valid_block m2 b2'); [ @(valid_access_valid_block ? chunk ? (ofs + delta)) /2/ ] #Hval A in Hbinj' LOAD #Hbinj' #LOAD >Hbinj in Hbinj' #bad destruct; ] qed. lemma alloc_left_mapped_inj: ∀val_inj.∀val_inj_undef_any:∀mi,v. val_inj mi Vundef v. ∀mi,m1,m2,lo,hi,b1,m1',b2,delta. mem_inj val_inj mi m1 m2 → alloc m1 lo hi = 〈m1', b1〉 → mi b1 = Some ? 〈b2, delta〉 → valid_block m2 b2 → low_bound m2 b2 ≤ lo + delta → hi + delta ≤ high_bound m2 b2 → inj_offset_aligned delta (hi - lo) → mem_inj val_inj mi m1' m2. #val_inj #val_inj_undef_any #mi #m1 #m2 #lo #hi #b1 #m1' #b2 #delta #Hinj #ALLOC #Hbinj #Hval #Hlo #Hhi #Hal whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD lapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/; *; [ #A @(Hinj … Hbinj') A in Hbinj' LOAD #Hbinj' #LOAD >Hbinj in Hbinj' #Hbinj' (* XXX destruct normalizes too much here *) elim (grumpydestruct2 ?????? Hbinj'); #eb2 #edelta ev1 cut (∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2); [ @valid_access_load % //; [ (* arith *) napply daemon | (* arith *) napply daemon | (* arith *) napply daemon ] ] *;#v2 #LOAD2 %{ v2} % //; ] qed. lemma free_parallel_inj: ∀val_inj. ∀mi,m1,m2,b1,b2,delta. mem_inj val_inj mi m1 m2 → mi b1 = Some ? 〈b2, delta〉 → (∀b,delta'. mi b = Some ? 〈b2, delta'〉 → b = b1) → mem_inj val_inj mi (free m1 b1) (free m2 b2). #val_inj #mi #m1 #m2 #b1 #b2 #delta #Hinj #Hb1inj #Hbinj whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD lapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A #B cut (load chunk m1 b1' ofs = Some ? v1); [ e in Hbinj' #Hbinj' @(Hbinj ?? Hbinj') | // ] qed. lemma free_left_inj: ∀val_inj. ∀mi,m1,m2,b1. mem_inj val_inj mi m1 m2 → mem_inj val_inj mi (free m1 b1) m2. #val_inj #mi #m1 #m2 #b1 #Hinj whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD lapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A #B @(Hinj … Hbinj') (unfold_free_list m1 h t) @free_left_inj @IH // ] qed. lemma free_right_inj: ∀val_inj. ∀mi,m1,m2,b2. mem_inj val_inj mi m1 m2 → (∀b1,delta,chunk,ofs. mi b1 = Some ? 〈b2, delta〉 → ¬(valid_access m1 chunk b1 ofs)) → mem_inj val_inj mi m1 (free m2 b2). #val_inj #mi #m1 #m2 #b2 #Hinj #Hinval whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD cut (b2' ≠ b2); [ @nmk #e >e in Hbinj' #Hbinj' @(absurd ?? (Hinval … Hbinj')) @(load_valid_access … LOAD) ] #ne lapply (Hinj … Hbinj' LOAD); *;#v2 *;#LOAD2 #INJ %{ v2} % //; (Zplus_z_OZ ofs) //; | // ] qed. theorem alloc_extends: ∀m1,m2,m1',m2': mem. ∀lo1,hi1,lo2,hi2: Z. ∀b1,b2: block. extends m1 m2 → lo2 ≤ lo1 → hi1 ≤ hi2 → alloc m1 lo1 hi1 = 〈m1', b1〉 → alloc m2 lo2 hi2 = 〈m2', b2〉 → b1 = b2 ∧ extends m1' m2'. #m1 #m2 #m1' #m2' #lo1 #hi1 #lo2 #hi2 #b1 #b2 *;#Hnext #Hinj #Hlo #Hhi #ALLOC1 #ALLOC2 cut (b1 = b2); [ @(transitive_eq … (nextblock m1)) [ @(alloc_result … ALLOC1) | @sym_eq >Hnext napply (alloc_result … ALLOC2) ] ] #eb (nextblock_alloc … ALLOC1) >(nextblock_alloc … ALLOC2) //; | @(alloc_parallel_inj ??????????????? ALLOC1 ALLOC2 ????) [ 1,4: normalize; //; | 3,5,6: // | 7: whd; #chunk #Hsize (* divides 0 *) napply daemon ] ] qed. theorem free_extends: ∀m1,m2: mem. ∀b: block. extends m1 m2 → extends (free m1 b) (free m2 b). #m1 #m2 #b *;#Hnext #Hinj % [ normalize; //; | @(free_parallel_inj … Hinj) [ 2: //; | 3: normalize; #b' #delta #ee destruct; // ] ] qed. theorem load_extends: ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val. extends m1 m2 → load chunk m1 r b ofs = Some ? v → load chunk m2 r b ofs = Some ? v. #chunk #m1 #m2 #r #b #ofs #v *;#Hnext #Hinj #LOAD lapply (Hinj … LOAD); [ normalize; // | 2,3: ] *;#v2 *; >(Zplus_z_OZ ofs) #LOAD2 #EQ whd in EQ; //; qed. theorem store_within_extends: ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val. extends m1 m2 → store chunk m1 r b ofs v = Some ? m1' → ∃m2'. store chunk m2 r b ofs v = Some ? m2' ∧ extends m1' m2'. #chunk #m1 #m2 #m1' #b #ofs #v *;#Hnext #Hinj #STORE1 lapply (store_mapped_inj … Hinj ?? STORE1 ?); [ 1,2,7: normalize; // | (* TODO: unfolding, etc ought to tidy this up *) whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb #Hinj1 #Hinj2 normalize in Hinj1 Hinj2; %{1} %{1} %{1} destruct; // | 4,5,6: ##skip ] *;#m2' *;#STORE #MINJ %{ m2'} % >(Zplus_z_OZ ofs) in STORE #STORE //; % [ >(nextblock_store … STORE1) >(nextblock_store … STORE) // | // ] qed. theorem store_outside_extends: ∀chunk: memory_chunk. ∀m1,m2,m2': mem. ∀b: block. ∀ofs: Z. ∀v: val. extends m1 m2 → ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs → store chunk m2 r b ofs v = Some ? m2' → extends m1 m2'. #chunk #m1 #m2 #m2' #b #ofs #v *;#Hnext #Hinj #Houtside #STORE % [ >(nextblock_store … STORE) // | @(store_outside_inj … STORE) //; #b' #delta #einj normalize in einj; destruct; elim Houtside; [ #lo %{ 2} >(Zplus_z_OZ ?) /2/ | #hi %{ 1} >(Zplus_z_OZ ?) /2/ ] ] qed. theorem valid_pointer_extends: ∀m1,m2,b,ofs. extends m1 m2 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true. #m1 #m2 #b #ofs *;#Hnext #Hinj #VALID <(Zplus_z_OZ ofs) @(valid_pointer_inj … Hinj VALID) //; qed. (* * The ``less defined than'' relation over memory states *) (* A memory state [m1] is less defined than [m2] if, for all addresses, the value [v1] read in [m1] at this address is less defined than the value [v2] read in [m2], that is, either [v1 = v2] or [v1 = Vundef]. *) definition val_inj_lessdef ≝ λmi: meminj. λv1,v2: val. Val_lessdef v1 v2. definition lessdef ≝ λm1,m2: mem. nextblock m1 = nextblock m2 ∧ mem_inj val_inj_lessdef inject_id m1 m2. lemma lessdef_refl: ∀m. lessdef m m. #m % //; whd; #chunk #b1 #ofs #v1 #b2 #delta #H #LOAD whd in H:(??%?); elim (grumpydestruct2 ?????? H); #eb1 #edelta %{ v1} % //; qed. lemma load_lessdef: ∀m1,m2,chunk,b,ofs,v1. lessdef m1 m2 → load chunk m1 r b ofs = Some ? v1 → ∃v2. load chunk m2 r b ofs = Some ? v2 ∧ Val_lessdef v1 v2. #m1 #m2 #chunk #b #ofs #v1 *;#Hnext #Hinj #LOAD0 lapply (Hinj … LOAD0); [ whd in ⊢ (??%?); // | 2,3:##skip ] *;#v2 *;#LOAD #INJ %{ v2} % //; qed. lemma loadv_lessdef: ∀m1,m2,chunk,addr1,addr2,v1. lessdef m1 m2 → Val_lessdef addr1 addr2 → loadv chunk m1 addr1 = Some ? v1 → ∃v2. loadv chunk m2 addr2 = Some ? v2 ∧ Val_lessdef v1 v2. #m1 #m2 #chunk #addr1 #addr2 #v1 #H #H0 #LOAD inversion H0; [ #v #e1 #e2 >e1 in LOAD cases v; [ whd in ⊢ ((??%?)→?); #H' destruct; | 2,3: #v' whd in ⊢ ((??%?)→?); #H' destruct; | #b' #off @load_lessdef // ] | #v #e >e in LOAD #LOAD whd in LOAD:(??%?); destruct; ] qed. lemma store_lessdef: ∀m1,m2,chunk,b,ofs,v1,v2,m1'. lessdef m1 m2 → Val_lessdef v1 v2 → store chunk m1 r b ofs v1 = Some ? m1' → ∃m2'. store chunk m2 r b ofs v2 = Some ? m2' ∧ lessdef m1' m2'. #m1 #m2 #chunk #b #ofs #v1 #v2 #m1' *;#Hnext #Hinj #Hvless #STORE0 lapply (store_mapped_inj … Hinj … STORE0 ?); [ #chunk' #Hsize whd;@load_result_lessdef napply Hvless | whd in ⊢ (??%?); // | whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neq whd in ⊢ ((??%?)→(??%?)→?); #e1 #e2 destruct; % % % // | 7: #mi whd; //; | 8: *;#m2' *;#STORE #MINJ %{ m2'} % /2/; % >(nextblock_store … STORE0) >(nextblock_store … STORE) //; ] qed. lemma storev_lessdef: ∀m1,m2,chunk,addr1,v1,addr2,v2,m1'. lessdef m1 m2 → Val_lessdef addr1 addr2 → Val_lessdef v1 v2 → storev chunk m1 addr1 v1 = Some ? m1' → ∃m2'. storev chunk m2 addr2 v2 = Some ? m2' ∧ lessdef m1' m2'. #m1 #m2 #chunk #addr1 #v1 #addr2 #v2 #m1' #Hmless #Haless #Hvless #STORE inversion Haless; [ #v #e1 #e2 >e1 in STORE cases v; [ whd in ⊢ ((??%?)→?); #H' @False_ind destruct; | 2,3: #v' whd in ⊢ ((??%?)→?); #H' destruct; | #b' #off @store_lessdef // ] | #v #e >e in STORE #STORE whd in STORE:(??%?); destruct ] qed. lemma alloc_lessdef: ∀m1,m2,lo,hi,b1,m1',b2,m2'. lessdef m1 m2 → alloc m1 lo hi = 〈m1', b1〉 → alloc m2 lo hi = 〈m2', b2〉 → b1 = b2 ∧ lessdef m1' m2'. #m1 #m2 #lo #hi #b1 #m1' #b2 #m2' *;#Hnext #Hinj #ALLOC1 #ALLOC2 cut (b1 = b2); [ >(alloc_result … ALLOC1) >(alloc_result … ALLOC2) // ] #e (nextblock_alloc … ALLOC1) >(nextblock_alloc … ALLOC2) // | @(alloc_parallel_inj … Hinj ALLOC1 ALLOC2) [ // | 3: whd in ⊢ (??%?); // | 4,5: //; | 6: whd; #chunk #_ cases chunk;//; ] qed. lemma free_lessdef: ∀m1,m2,b. lessdef m1 m2 → lessdef (free m1 b) (free m2 b). #m1 #m2 #b *;#Hnext #Hinj % [ whd in ⊢ (??%%); // | @(free_parallel_inj … Hinj) //; #b' #delta #H whd in H:(??%?); elim (grumpydestruct2 ?????? H); // ] qed. lemma free_left_lessdef: ∀m1,m2,b. lessdef m1 m2 → lessdef (free m1 b) m2. #m1 #m2 #b *;#Hnext #Hinj % Hnext //; @free_right_inj //; #b1 #delta #chunk #ofs #H whd in H:(??%?); destruct; @nmk *; #H1 #H2 #H3 #H4 (* arith H2 and H3 contradict Hbounds. *) @daemon qed. lemma valid_block_lessdef: ∀m1,m2,b. lessdef m1 m2 → valid_block m1 b → valid_block m2 b. #m1 #m2 #b *;#Hnext #Hinj >(unfold_valid_block …) >(unfold_valid_block m2 b) //; qed. lemma valid_pointer_lessdef: ∀m1,m2,b,ofs. lessdef m1 m2 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true. #m1 #m2 #b #ofs *;#Hnext #Hinj #VALID <(Zplus_z_OZ ofs) @(valid_pointer_inj … Hinj VALID) //; qed. (* ** Memory injections *) (* A memory injection [f] is a function from addresses to either [None] or [Some] of an address and an offset. It defines a correspondence between the blocks of two memory states [m1] and [m2]: - if [f b = None], the block [b] of [m1] has no equivalent in [m2]; - if [f b = Some〈b', ofs〉], the block [b] of [m2] corresponds to a sub-block at offset [ofs] of the block [b'] in [m2]. *) (* A memory injection defines a relation between values that is the identity relation, except for pointer values which are shifted as prescribed by the memory injection. *) inductive val_inject (mi: meminj): val → val → Prop := | val_inject_int: ∀i. val_inject mi (Vint i) (Vint i) | val_inject_float: ∀f. val_inject mi (Vfloat f) (Vfloat f) | val_inject_ptr: ∀b1,ofs1,b2,ofs2,x. mi b1 = Some ? 〈b2, x〉 → ofs2 = add ofs1 (repr x) → val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2) | val_inject_undef: ∀v. val_inject mi Vundef v. (* Hint Resolve val_inject_int val_inject_float val_inject_ptr val_inject_undef. *) inductive val_list_inject (mi: meminj): list val → list val→ Prop:= | val_nil_inject : val_list_inject mi (nil ?) (nil ?) | val_cons_inject : ∀v,v',vl,vl'. val_inject mi v v' → val_list_inject mi vl vl'→ val_list_inject mi (v :: vl) (v' :: vl'). (* Hint Resolve val_nil_inject val_cons_inject. *) (* A memory state [m1] injects into another memory state [m2] via the memory injection [f] if the following conditions hold: - loads in [m1] must have matching loads in [m2] in the sense of the [mem_inj] predicate; - unallocated blocks in [m1] must be mapped to [None] by [f]; - if [f b = Some〈b', delta〉], [b'] must be valid in [m2]; - distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2]; - the sizes of [m2]'s blocks are representable with signed machine integers; - the offsets [delta] are representable with signed machine integers. *) record mem_inject (f: meminj) (m1,m2: mem) : Prop ≝ { mi_inj: mem_inj val_inject f m1 m2; mi_freeblocks: ∀b. ¬(valid_block m1 b) → f b = None ?; mi_mappedblocks: ∀b,b',delta. f b = Some ? 〈b', delta〉 → valid_block m2 b'; mi_no_overlap: meminj_no_overlap f m1; mi_range_1: ∀b,b',delta. f b = Some ? 〈b', delta〉 → min_signed ≤ delta ∧ delta ≤ max_signed; mi_range_2: ∀b,b',delta. f b = Some ? 〈b', delta〉 → delta = 0 ∨ (min_signed ≤ low_bound m2 b' ∧ high_bound m2 b' ≤ max_signed) }. (* The following lemmas establish the absence of machine integer overflow during address computations. *) lemma address_inject: ∀f,m1,m2,chunk,b1,ofs1,b2,delta. mem_inject f m1 m2 → valid_access m1 chunk b1 (signed ofs1) → f b1 = Some ? 〈b2, delta〉 → signed (add ofs1 (repr delta)) = signed ofs1 + delta. #f #m1 #m2 #chunk #b1 #ofs1 #b2 #delta *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 #Hvalid #Hb1inj elim (mi_range_2 ??? Hb1inj); [ (* delta = 0 *) #edelta >edelta >(?:repr O = zero) [ 2: // ] >(add_zero ?) >(Zplus_z_OZ …) //; | (* delta ≠ 0 *) #Hrange >(add_signed ??) >(signed_repr delta ?) [ >(signed_repr ??) [ // | cut (valid_access m2 chunk b2 (signed ofs1 + delta)); [ @(valid_access_inj … Hvalid) //; | *; #_ #Hlo #Hhi #_ (* arith *) napply daemon ] ] | /2/ ] ] qed. lemma valid_pointer_inject_no_overflow: ∀f,m1,m2,b,ofs,b',x. mem_inject f m1 m2 → valid_pointer m1 b (signed ofs) = true → f b = Some ? 〈b', x〉 → min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed. #f #m1 #m2 #b #ofs #b' #x *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 #Hvalid #Hb1inj lapply ((proj1 ?? (valid_pointer_valid_access ???)) Hvalid); #Hvalid' cut (valid_access m2 Mint8unsigned b' (signed ofs + x)); [ @(valid_access_inj … Hvalid') // ] *; >(?:size_chunk Mint8unsigned = 1) [ 2: // ] #_ #Hlo #Hhi #_ >(signed_repr ??) [ 2: /2/; ] lapply (mi_range_2 … Hb1inj); *; [ #ex >ex >(Zplus_z_OZ ?) @signed_range | (* arith *) napply daemon ] qed. (* XXX: should use destruct, but reduces large definitions *) lemma vptr_eq: ∀b,b',i,i'. Vptr b i = Vptr b' i' → b = b' ∧ i = i'. #b #b' #i #i' #e destruct; /2/; qed. lemma valid_pointer_inject: ∀f,m1,m2,b,ofs,b',ofs'. mem_inject f m1 m2 → valid_pointer m1 b (signed ofs) = true → val_inject f (Vptr r b ofs) (Vptr b' ofs') → valid_pointer m2 b' (signed ofs') = true. #f #m1 #m2 #b #ofs #b' #ofs' #Hinj #Hvalid #Hvinj inversion Hvinj; [ 1,2,4: #x #H destruct; ] #b0 #i #b0' #i' #delta #Hb #Hi' #eptr #eptr' <(proj1 … (vptr_eq ???? eptr)) in Hb <(proj1 … (vptr_eq ???? eptr')) <(proj2 … (vptr_eq ???? eptr)) in Hi' <(proj2 … (vptr_eq ???? eptr')) #Hofs #Hbinj >Hofs lapply (valid_pointer_inject_no_overflow … Hinj Hvalid Hbinj); #NOOV elim Hinj;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 >(add_signed ??) >(signed_repr ??) //; >(signed_repr ??) /2/; @(valid_pointer_inj … mi_inj Hvalid) //; qed. lemma different_pointers_inject: ∀f,m,m',b1,ofs1,b2,ofs2,b1',delta1,b2',delta2. mem_inject f m m' → b1 ≠ b2 → valid_pointer m b1 (signed ofs1) = true → valid_pointer m b2 (signed ofs2) = true → f b1 = Some ? 〈b1', delta1〉 → f b2 = Some ? 〈b2', delta2〉 → b1' ≠ b2' ∨ signed (add ofs1 (repr delta1)) ≠ signed (add ofs2 (repr delta2)). #f #m #m' #b1 #ofs1 #b2 #ofs2 #b1' #delta1 #b2' #delta2 #Hinj #neb #Hval1 #Hval2 #Hf1 #Hf2 lapply ((proj1 ?? (valid_pointer_valid_access …)) Hval1); #Hval1' lapply ((proj1 ?? (valid_pointer_valid_access …)) Hval2); #Hval2' >(address_inject … Hinj Hval1' Hf1) >(address_inject … Hinj Hval2' Hf2) elim Hval1'; #Hbval #Hlo #Hhi #Hal whd in Hhi:(?(??%)?); elim Hval2'; #Hbval2 #Hlo2 #Hhi2 #Hal2 whd in Hhi2:(?(??%)?); lapply (mi_no_overlap ??? Hinj … Hf1 Hf2 …); //; *; [ *; [ *; [ /2/; | (* arith contradiction *) napply daemon ] | (* arith contradiction *) napply daemon ] | *; [ #H %{2} (* arith *) napply daemon | #H %{2} (* arith *) napply daemon ] ] qed. (* Relation between injections and loads. *) lemma load_inject: ∀f,m1,m2,chunk,b1,ofs,b2,delta,v1. mem_inject f m1 m2 → load chunk m1 b1 ofs = Some ? v1 → f b1 = Some ? 〈b2, delta〉 → ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inject f v1 v2. #f #m1 #m2 #chunk #b1 #ofs #b2 #delta #v1 *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 #LOAD #Hbinj @mi_inj //; qed. lemma loadv_inject: ∀f,m1,m2,chunk,a1,a2,v1. mem_inject f m1 m2 → loadv chunk m1 a1 = Some ? v1 → val_inject f a1 a2 → ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_inject f v1 v2. #f #m1 #m2 #chunk #a1 #a2 #v1 #Hinj #LOADV #Hvinj inversion Hvinj; [ 1,2,4: #x #ex #ex' @False_ind destruct; ] #b #ofs #b' #ofs' #delta #Hbinj #Hofs #ea1 #ea2 >ea1 in LOADV #LOADV lapply (load_inject … Hinj LOADV … Hbinj); *; #v2 *; #LOAD #INJ %{ v2} % //; >Hofs <(?:signed (add ofs (repr delta)) = signed ofs + delta) in LOAD [ #H @H (* XXX: used to work with /2/ *) | @(address_inject … chunk … Hinj ? Hbinj) @(load_valid_access …) [ 2: @LOADV ] ] qed. (* Relation between injections and stores. *) inductive val_content_inject (f: meminj): memory_chunk → val → val → Prop ≝ | val_content_inject_base: ∀chunk,v1,v2. val_inject f v1 v2 → val_content_inject f chunk v1 v2 | val_content_inject_8: ∀chunk,n1,n2. chunk = Mint8unsigned ∨ chunk = Mint8signed → zero_ext 8 n1 = zero_ext 8 n2 → val_content_inject f chunk (Vint n1) (Vint n2) | val_content_inject_16: ∀chunk,n1,n2. chunk = Mint16unsigned ∨ chunk = Mint16signed → zero_ext 16 n1 = zero_ext 16 n2 → val_content_inject f chunk (Vint n1) (Vint n2) | val_content_inject_32: ∀f1,f2. singleoffloat f1 = singleoffloat f2 → val_content_inject f Mfloat32 (Vfloat f1) (Vfloat f2). (*Hint Resolve val_content_inject_base.*) lemma load_result_inject: ∀f,chunk,v1,v2,chunk'. val_content_inject f chunk v1 v2 → size_chunk chunk = size_chunk chunk' → val_inject f (load_result chunk' v1) (load_result chunk' v2). #f #chunk #v1 #v2 #chunk' #Hvci inversion Hvci; [ #chunk'' #v1' #v2' #Hvinj #_ #_ #_ #Hsize inversion Hvinj; [ cases chunk'; #i #_ #_ [ 1,2,3,4,5: @ | 6,7: @4 ] | cases chunk'; #f #_ #_ [ 1,2,3,4,5: @4 | 6,7: @2 ] | cases chunk'; #b1 #ofs1 #b2 #ofs2 #delta #Hmap #Hofs #_ #_ [ 5: %{3} // | *: @4 ] | cases chunk'; #v #_ #_ %{4} ] (* FIXME: the next two cases are very similar *) | #chunk'' #i #i' *;#echunk >echunk #Hz #_ #_ #_ elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct; [ 2,4: whd in ⊢ (??%%); >Hz @ | 1,3: whd in ⊢ (??%%); >(sign_ext_equal_if_zero_equal … Hz) % [ 1,3: @I | 2,4: @leb_true_to_le % ] ] | #chunk'' #i #i' *;#echunk >echunk #Hz #_ #_ #_ elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct; [ 2,4: whd in ⊢ (??%%); >Hz @ | 1,3: whd in ⊢ (??%%); >(sign_ext_equal_if_zero_equal … Hz) % [ 1,3: @I | 2,4: @leb_true_to_le % ] ] | #f #f' #float #echunk >echunk #_ #_ elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct; [ %{4} | >float @2 ] ] qed. lemma store_mapped_inject_1 : ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2. mem_inject f m1 m2 → store chunk m1 b1 ofs v1 = Some ? n1 → f b1 = Some ? 〈b2, delta〉 → val_content_inject f chunk v1 v2 → ∃n2. store chunk m2 b2 (ofs + delta) v2 = Some ? n2 ∧ mem_inject f n1 n2. #f #chunk #m1 #b1 #ofs #v1 #n1 #m2 #b2 #delta #v2 *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 #STORE1 #INJb1 #Hvcinj lapply (store_mapped_inj … mi_inj mi_no_overlap INJb1 STORE1 ?); //; [ #chunk' #Hchunksize @(load_result_inject … chunk …) //; | ##skip ] *;#n2 *;#STORE #MINJ %{ n2} % //; % [ (* inj *) // | (* freeblocks *) #b #notvalid @mi_freeblocks @(not_to_not ??? notvalid) @(store_valid_block_1 … STORE1) | (* mappedblocks *) #b #b' #delta' #INJb' @(store_valid_block_1 … STORE) /2/; | (* no_overlap *) whd; #b1' #b1'' #delta1' #b2' #b2'' #delta2' #neqb' #fb1' #fb2' >(low_bound_store … STORE1 ?) >(low_bound_store … STORE1 ?) >(high_bound_store … STORE1 ?) >(high_bound_store … STORE1 ?) @mi_no_overlap //; | (* range *) /2/; | (* range 2 *) #b #b' #delta' #INJb >(low_bound_store … STORE ?) >(high_bound_store … STORE ?) @mi_range_2 //; ] qed. lemma store_mapped_inject: ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2. mem_inject f m1 m2 → store chunk m1 b1 ofs v1 = Some ? n1 → f b1 = Some ? 〈b2, delta〉 → val_inject f v1 v2 → ∃n2. store chunk m2 b2 (ofs + delta) v2 = Some ? n2 ∧ mem_inject f n1 n2. #f #chunk #m1 #b1 #ofs #v1 #n1 #m2 #b2 #delta #v2 #MINJ #STORE #INJb1 #Hvalinj @(store_mapped_inject_1 … STORE) //; @val_content_inject_base //; qed. lemma store_unmapped_inject: ∀f,chunk,m1,b1,ofs,v1,n1,m2. mem_inject f m1 m2 → store chunk m1 b1 ofs v1 = Some ? n1 → f b1 = None ? → mem_inject f n1 m2. #f #chunk #m1 #b1 #ofs #v1 #n1 #m2 *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 #STORE #INJb1 % [ (* inj *) @(store_unmapped_inj … STORE) // | (* freeblocks *) #b #notvalid @mi_freeblocks @(not_to_not ??? notvalid) @(store_valid_block_1 … STORE) | (* mappedblocks *) #b #b' #delta #INJb @mi_mappedblock //; | (* no_overlap *) whd; #b1' #b1'' #delta1' #b2' #b2'' #delta2' #neqb' #fb1' #fb2' >(low_bound_store … STORE ?) >(low_bound_store … STORE ?) >(high_bound_store … STORE ?) >(high_bound_store … STORE ?) @mi_no_overlap //; | (* range *) /2/ | /2/ ] qed. lemma storev_mapped_inject_1: ∀f,chunk,m1,a1,v1,n1,m2,a2,v2. mem_inject f m1 m2 → storev chunk m1 a1 v1 = Some ? n1 → val_inject f a1 a2 → val_content_inject f chunk v1 v2 → ∃n2. storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2. #f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2 #MINJ #STORE #Hvinj #Hvcinj inversion Hvinj; [ 1,2,4:#x #ex1 #ex2 >ex1 in STORE whd in ⊢ ((??%?)→?); #H @False_ind destruct; ] #b #ofs #b' #ofs' #delta #INJb #Hofs #ea1 #ea2 >Hofs >ea1 in STORE #STORE lapply (store_mapped_inject_1 … MINJ STORE … INJb Hvcinj); <(?:signed (add ofs (repr delta)) = signed ofs + delta) //; @(address_inject … chunk … MINJ ? INJb) @(store_valid_access_3 … STORE) qed. lemma storev_mapped_inject: ∀f,chunk,m1,a1,v1,n1,m2,a2,v2. mem_inject f m1 m2 → storev chunk m1 a1 v1 = Some ? n1 → val_inject f a1 a2 → val_inject f v1 v2 → ∃n2. storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2. #f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2 #MINJ #STOREV #Hvinj #Hvinj' @(storev_mapped_inject_1 … STOREV) /2/; qed. (* Relation between injections and [free] *) lemma meminj_no_overlap_free: ∀mi,m,b. meminj_no_overlap mi m → meminj_no_overlap mi (free m b). #mi #m #b #H whd;#b1 #b1' #delta1 #b2 #b2' #delta2 #Hne #mi1 #mi2 cut (low_bound (free m b) b ≥ high_bound (free m b) b); [ >(low_bound_free_same …) >(high_bound_free_same …) // ] #Hbounds cases (decidable_eq_Z b1 b);#e1 [ >e1 in Hne mi1 ⊢ % #Hne #mi1 ] cases (decidable_eq_Z b2 b);#e2 [ 1,3: >e2 in Hne mi2 ⊢ % #Hne #mi2 ] [ @False_ind elim Hne; /2/ | % %{2} //; | % % %{2} // | >(low_bound_free …) //; >(low_bound_free …) //; >(high_bound_free …) //; >(high_bound_free …) //; /2/; ] qed. lemma meminj_no_overlap_free_list: ∀mi,m,bl. meminj_no_overlap mi m → meminj_no_overlap mi (free_list m bl). #mi #m #bl elim bl; [ #H whd in ⊢ (??%); // | #h #t #IH #H @meminj_no_overlap_free @IH // ] qed. lemma free_inject: ∀f,m1,m2,l,b. (∀b1,delta. f b1 = Some ? 〈b, delta〉 → in_list ? b1 l) → mem_inject f m1 m2 → mem_inject f (free_list m1 l) (free m2 b). #f #m1 #m2 #l #b #mappedin *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 % [ (* inj *) @free_right_inj [ @free_list_left_inj //; ] #b1 #delta #chunk #ofs #INJb1 @nmk #Hvalid elim (valid_access_free_list_inv … Hvalid); #b1ni #Haccess @(absurd ? (mappedin ?? INJb1) b1ni) | (* freeblocks *) #b' #notvalid @mi_freeblocks @(not_to_not ??? notvalid) #H @valid_block_free_list_1 // | (* mappedblocks *) #b1 #b1' #delta #INJb1 @valid_block_free_1 /2/ | (* overlap *) @meminj_no_overlap_free_list // | (* range *) /2/ | #b1 #b2 #delta #INJb1 cases (decidable_eq_Z b2 b); #eb [ >eb >(low_bound_free_same ??) >(high_bound_free_same ??) %{2} (* arith *) napply daemon | >(low_bound_free …) //; >(high_bound_free …) /2/; ] ] qed. (* Monotonicity properties of memory injections. *) definition inject_incr : meminj → meminj → Prop ≝ λf1,f2. ∀b. f1 b = f2 b ∨ f1 b = None ?. lemma inject_incr_refl : ∀f. inject_incr f f . #f whd;#b % //; qed. lemma inject_incr_trans : ∀f1,f2,f3. inject_incr f1 f2 → inject_incr f2 f3 → inject_incr f1 f3 . #f1 #f2 #f3 whd in ⊢ (%→%→%);#H1 #H2 #b elim (H1 b); elim (H2 b); /2/; qed. lemma val_inject_incr: ∀f1,f2,v,v'. inject_incr f1 f2 → val_inject f1 v v' → val_inject f2 v v'. #f1 #f2 #v #v' #Hincr #Hvinj inversion Hvinj; [ 1,2,4: #x #_ #_ //; |#b #ofs #b' #ofs' #delta #INJb #Hofs #_ #_ elim (Hincr b); #H [ @(val_inject_ptr ??????? Hofs) /2/; | @False_ind >INJb in H #H destruct; ] qed. lemma val_list_inject_incr: ∀f1,f2,vl,vl'. inject_incr f1 f2 → val_list_inject f1 vl vl' → val_list_inject f2 vl vl'. #f1 #f2 #vl elim vl; [ #vl' #Hincr #H inversion H; //; #v #v' #l #l0 #_ #_ #_ #H destruct; | #h #t #IH #vl' #Hincr #H1 inversion H1; [ #H destruct | #h' #h'' #t' #t'' #Hinj1 #Hintt #_ #e1 #e2 destruct; %{2} /2/; @IH //; @Hincr ] ] qed. (* Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr. *) (* Properties of injections and allocations. *) definition extend_inject ≝ λb: block. λx: option (block × Z). λf: meminj. λb': block. if eqZb b' b then x else f b'. lemma extend_inject_incr: ∀f,b,x. f b = None ? → inject_incr f (extend_inject b x f). #f #b #x #INJb whd;#b' whd in ⊢ (?(???%)?); @(eqZb_elim b' b) #eb /2/; qed. lemma alloc_right_inject: ∀f,m1,m2,lo,hi,m2',b. mem_inject f m1 m2 → alloc m2 lo hi = 〈m2', b〉 → mem_inject f m1 m2'. #f #m1 #m2 #lo #hi #m2' #b *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 #ALLOC % [ @(alloc_right_inj … ALLOC) //; | /2/; | #b1 #b2 #delta #INJb1 @(valid_block_alloc … ALLOC) /2/; | //; | /2/; |#b1 #b2 #delta #INJb1 >(?:low_bound m2' b2 = low_bound m2 b2) [ >(?:high_bound m2' b2 = high_bound m2 b2) /2/; @high_bound_alloc_other /2/; | @low_bound_alloc_other /2/ ] ] qed. lemma alloc_unmapped_inject: ∀f,m1,m2,lo,hi,m1',b. mem_inject f m1 m2 → alloc m1 lo hi = 〈m1', b〉 → mem_inject (extend_inject b (None ?) f) m1' m2 ∧ inject_incr f (extend_inject b (None ?) f). #f #m1 #m2 #lo #hi #m1' #b *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 #ALLOC cut (inject_incr f (extend_inject b (None ?) f)); [ @extend_inject_incr @mi_freeblocks /2/; ] #Hinject_incr % //; % [ (* inj *) @(alloc_left_unmapped_inj … ALLOC) [ 2: whd in ⊢ (??%?); >(eqZb_z_z …) /2/; ] whd; #chunk #b1 #ofs #v1 #b2 #delta whd in ⊢ ((??%?)→?→?); @eqZb_elim #e whd in ⊢ ((??%?)→?→?); #Hextend #LOAD [ destruct; | lapply (mi_inj … Hextend LOAD); *; #v2 *; #LOAD2 #VINJ %{ v2} % //; @val_inject_incr //; ] | (* freeblocks *) #b' #Hinvalid whd in ⊢ (??%?); @(eqZb_elim b' b) //; #neb @mi_freeblocks @(not_to_not ??? Hinvalid) @valid_block_alloc //; | (* mappedblocks *) #b1 #b2 #delta whd in ⊢ (??%?→?); @(eqZb_elim b1 b) #eb [ #H destruct; | #H @(mi_mappedblock … H) ] | (* overlap *) whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢ (??%?→??%?→?); >(low_bound_alloc … ALLOC ?) >(low_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?) lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 [ destruct | lapply (eqZb_to_Prop b2 b); elim (eqZb b2 b); #e2 #INJb2 [ destruct | @mi_no_overlap /2/; ] ] | (* range *) #b1 #b2 #delta whd in ⊢ (??%?→?); lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 [ destruct | @(mi_range_1 … INJb1) ] | #b1 #b2 #delta whd in ⊢ (??%?→?); lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 [ destruct | @(mi_range_2 … INJb1) ] ] qed. lemma alloc_mapped_inject: ∀f,m1,m2,lo,hi,m1',b,b',ofs. mem_inject f m1 m2 → alloc m1 lo hi = 〈m1', b〉 → valid_block m2 b' → min_signed ≤ ofs ∧ ofs ≤ max_signed → min_signed ≤ low_bound m2 b' → high_bound m2 b' ≤ max_signed → low_bound m2 b' ≤ lo + ofs → hi + ofs ≤ high_bound m2 b' → inj_offset_aligned ofs (hi-lo) → (∀b0,ofs0. f b0 = Some ? 〈b', ofs0〉 → high_bound m1 b0 + ofs0 ≤ lo + ofs ∨ hi + ofs ≤ low_bound m1 b0 + ofs0) → mem_inject (extend_inject b (Some ? 〈b', ofs〉) f) m1' m2 ∧ inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f). #f #m1 #m2 #lo #hi #m1' #b #b' #ofs *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 #ALLOC #validb' #rangeofs #rangelo #rangehi #boundlo #boundhi #injaligned #boundmapped cut (inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f)); [ @extend_inject_incr @mi_freeblocks /2/; ] #Hincr % //; % [ (* inj *) @(alloc_left_mapped_inj … ALLOC … validb' boundlo boundhi) /2/; [ 2:whd in ⊢ (??%?); >(eqZb_z_z …) /2/; ] whd; #chunk #b1 #ofs' #v1 #b2 #delta #Hextend #LOAD whd in Hextend:(??%?); >(eqZb_false b1 b ?) in Hextend [ #Hextend lapply (mi_inj … Hextend LOAD); *; #v2 *; #LOAD2 #VINJ %{ v2} % //; @val_inject_incr //; | @(valid_not_valid_diff m1) /2/; @(valid_access_valid_block … chunk … ofs') /2/; ] | (* freeblocks *) #b' #Hinvalid whd in ⊢ (??%?); >(eqZb_false b' b ?) [ @mi_freeblocks @(not_to_not ??? Hinvalid) @valid_block_alloc //; | @sym_neq @(valid_not_valid_diff m1') //; @(valid_new_block … ALLOC) ] | (* mappedblocks *) #b1 #b2 #delta whd in ⊢ (??%?→?); @(eqZb_elim b1 b) #eb #einj [ destruct; //; | @(mi_mappedblock … einj) ] | (* overlap *) whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢ (??%?→??%?→?); >(low_bound_alloc … ALLOC ?) >(low_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?) lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 [ elim (grumpydestruct2 ?????? INJb1); #eb1' #eofs1 ] lapply (eqZb_to_Prop b2 b); elim (eqZb b2 b); #e2 #INJb2 [ elim (grumpydestruct2 ?????? INJb2); #eb2' #eofs2 ] [ @False_ind >e in neb1 >e2 /2/; | elim (decidable_eq_Z b1' b2'); #e' [ (low_bound_alloc_same … ALLOC2) // | >(high_bound_alloc_same … ALLOC2) // | >(low_bound_alloc_same … ALLOC2) // | >(high_bound_alloc_same … ALLOC2) // | whd; (* arith *) napply daemon | #b #ofs #INJb0 @False_ind elim Hminj;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 lapply (mi_mappedblock … INJb0); #H @(absurd ? H ?) /2/; ] qed. definition meminj_init ≝ λm: mem. λb: block. if Zltb b (nextblock m) then Some ? 〈b, OZ〉 else None ?. definition mem_inject_neutral ≝ λm: mem. ∀f,chunk,b,ofs,v. load chunk m b ofs = Some ? v → val_inject f v v. lemma init_inject: ∀m. mem_inject_neutral m → mem_inject (meminj_init m) m m. #m #neutral % [ (* inj *) whd; #chunk #b1 #ofs #v1 #b2 #delta whd in ⊢ (??%?→?→?); @Zltb_elim_Type0 #ltb1 [ #H elim (grumpydestruct2 ?????? H); #eb1 #edelta (unfold_valid_block …) whd in ⊢ (?→??%?); #notvalid @Zltb_elim_Type0 #ltb1 [ @False_ind napply (absurd ? ltb1 notvalid) | // ] | (* mapped blocks *) #b #b' #delta whd in ⊢ (??%?→?); >(unfold_valid_block …) @Zltb_elim_Type0 #ltb #H whd in H:(??%?); destruct; // | (* overlap *) whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢(??%?→??%?→?); @Zltb_elim_Type0 #ltb1 [ #H whd in H:(??%?); destruct; @Zltb_elim_Type0 #ltb2 #H2 whd in H2:(??%?); destruct; % % % /2/; | #H whd in H:(??%?); destruct; ] | (* range *) #b #b' #delta whd in ⊢ (??%?→?); @Zltb_elim_Type0 #ltb [ #H elim (grumpydestruct2 ?????? H); #eb #edelta A //; qed. lemma getN_contents_init_data_inject: ∀f,n,ofs,id,pos. val_inject f (getN n ofs (contents_init_data pos id)) (getN n ofs (contents_init_data pos id)). #f #n #ofs #id elim id; [ #pos >(getN_init …) // | #h #t #IH #pos cases h; [ 1,2,3,4,5: #x @getN_setN_inject // | 6,8: #x @IH | #x #y napply IH ] (* XXX // doesn't work? *) qed. lemma alloc_init_data_neutral: ∀m,id,m',b. mem_inject_neutral m → alloc_init_data m id = 〈m', b〉 → mem_inject_neutral m'. #m #id #m' #b #Hneutral #INIT whd in INIT:(??%?); (* XXX: destruct makes a bit of a mess *) @(pairdisc_elim … INIT) whd in ⊢ (??%% → ?);#B A >(unfold_update block_contents …) @eqZb_elim [ #eb' #D whd in D:(???(??(???%))); >D @(load_result_inject … chunk) //; % @getN_contents_init_data_inject | #neb' #D @(Hneutral ? chunk b' ofs ??) whd in ⊢ (??%?); >(in_bounds_true m chunk b' ofs (option ?) …) [ (unfold_valid_block …) >(unfold_valid_block …) in Cval (?:low_bound m b' = low_bound m' b') //; whd in ⊢ (??%%); A >(update_o block_contents …) //; @sym_neq //; | >(?:high_bound m b' = high_bound m' b') //; whd in ⊢ (??%%); A >(update_o block_contents …) //; @sym_neq //; | //; ] ] qed. (* ** Memory shifting *) (* A special case of memory injection where blocks are not coalesced: each source block injects in a distinct target block. *) definition memshift ≝ block → option Z. definition meminj_of_shift : memshift → meminj ≝ λmi: memshift. λb. match mi b with [ None ⇒ None ? | Some x ⇒ Some ? 〈b, x〉 ]. definition val_shift ≝ λmi: memshift. λv1,v2: val. val_inject (meminj_of_shift mi) v1 v2. record mem_shift (f: memshift) (m1,m2: mem) : Prop := { ms_inj: mem_inj val_inject (meminj_of_shift f) m1 m2; ms_samedomain: nextblock m1 = nextblock m2; ms_domain: ∀b. match f b with [ Some _ ⇒ b < nextblock m1 | None ⇒ b ≥ nextblock m1 ]; ms_range_1: ∀b,delta. f b = Some ? delta → min_signed ≤ delta ∧ delta ≤ max_signed; ms_range_2: ∀b,delta. f b = Some ? delta → min_signed ≤ low_bound m2 b ∧ high_bound m2 b ≤ max_signed }. (* * The following lemmas establish the absence of machine integer overflow during address computations. *) lemma address_shift: ∀f,m1,m2,chunk,b,ofs1,delta. mem_shift f m1 m2 → valid_access m1 chunk b (signed ofs1) → f b = Some ? delta → signed (add ofs1 (repr delta)) = signed ofs1 + delta. #f #m1 #m2 #chunk #b #ofs1 #delta *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 #Hvalid_access #INJb elim (ms_range_2 … INJb); #Hlo #Hhi >(add_signed …) >(signed_repr …) >(signed_repr …) /2/; cut (valid_access m2 chunk b (signed ofs1 + delta)); [ @(valid_access_inj ? (meminj_of_shift f) … ms_inj Hvalid_access) whd in ⊢ (??%?); >INJb // ] *; (* arith *) @daemon qed. lemma valid_pointer_shift_no_overflow: ∀f,m1,m2,b,ofs,x. mem_shift f m1 m2 → valid_pointer m1 b (signed ofs) = true → f b = Some ? x → min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed. #f #m1 #m2 #b #ofs #x *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 #VALID #INJb lapply (proj1 ?? (valid_pointer_valid_access …) VALID); #Hvalid_access cut (valid_access m2 Mint8unsigned b (signed ofs + x)); [ @(valid_access_inj … ms_inj Hvalid_access) whd in ⊢ (??%?); >INJb // ] *;#Hvalid_block #Hlo #Hhi #Hal whd in Hhi:(?(??%)?); >(signed_repr …) /2/; lapply (ms_range_2 … INJb);*;#A #B (* arith *) @daemon qed. (* FIXME to get around destruct problems *) lemma vptr_eq_1 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → b = b'. #b #b' #ofs #ofs' #H destruct;//; qed. lemma vptr_eq_2 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → ofs = ofs'. #b #b' #ofs #ofs' #H destruct;//; qed. lemma valid_pointer_shift: ∀f,m1,m2,b,ofs,b',ofs'. mem_shift f m1 m2 → valid_pointer m1 b (signed ofs) = true → val_shift f (Vptr b ofs) (Vptr b' ofs') → valid_pointer m2 b' (signed ofs') = true. #f #m1 #m2 #b #ofs #b' #ofs' #Hmem_shift #VALID #Hval_shift whd in Hval_shift; inversion Hval_shift; [ 1,2,4: #a #H destruct; ] #b1 #ofs1 #b2 #ofs2 #delta #INJb1 #Hofs #eb1 #eb2 <(vptr_eq_1 … eb1) in INJb1 <(vptr_eq_1 … eb2) #INJb' <(vptr_eq_2 … eb1) in Hofs <(vptr_eq_2 … eb2) #Hofs >Hofs cut (f b = Some ? delta); [ whd in INJb':(??%?); cases (f b) in INJb' ⊢ %; [ #H @(False_ind … (grumpydestruct … H)) | #delta' #H elim (grumpydestruct2 ?????? H); // ] ] #INJb lapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV elim Hmem_shift;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 >(add_signed …) >(signed_repr …) //; >(signed_repr …) /2/; @(valid_pointer_inj … VALID) /2/; qed. (* Relation between shifts and loads. *) lemma load_shift: ∀f,m1,m2,chunk,b,ofs,delta,v1. mem_shift f m1 m2 → load chunk m1 b ofs = Some ? v1 → f b = Some ? delta → ∃v2. load chunk m2 b (ofs + delta) = Some ? v2 ∧ val_shift f v1 v2. #f #m1 #m2 #chunk #b #ofs #delta #v1 *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 #LOAD #INJb whd in ⊢ (??(λ_.??%)); @(ms_inj … LOAD) whd in ⊢ (??%?); >INJb //; qed. lemma loadv_shift: ∀f,m1,m2,chunk,a1,a2,v1. mem_shift f m1 m2 → loadv chunk m1 a1 = Some ? v1 → val_shift f a1 a2 → ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_shift f v1 v2. #f #m1 #m2 #chunk #a1 #a2 #v1 #Hmem_shift #LOADV #Hval_shift inversion Hval_shift; [ 1,2,4: #x #H >H in LOADV #H' whd in H':(??%?);@False_ind destruct; ] #b1 #ofs1 #b2 #ofs2 #delta #INJb1 #Hofs #ea1 #ea2 >ea1 in LOADV #LOADV lapply INJb1; whd in ⊢ (??%? → ?); lapply (refl ? (f b1)); cases (f b1) in ⊢ (???% → %); [ #_ whd in ⊢ (??%? → ?); #H @False_ind @(False_ind … (grumpydestruct … H)) | #delta' #DELTA whd in ⊢ (??%? → ?); #H elim (grumpydestruct2 ?????? H); #eb #edelta ] lapply (load_shift … Hmem_shift LOADV DELTA); *; #v2 *;#LOAD #INJ %{ v2} % //; >Hofs >eb in LOAD >edelta <(?:signed (add ofs1 (repr delta)) = signed ofs1 + delta) [#H' @H' (* XXX // doesn't work *) | INJb (* XXX: // has stopped working *) napply refl | whd; #b1 #b1' #delta1 #b2 #b2' #delta2 whd in ⊢ (? → ??%? → ??%? → ?); elim (f b1); elim (f b2); [#_ #e1 whd in e1:(??%?);destruct; |#z #_ #e1 whd in e1:(??%?);destruct; |#z #_ #_ #e2 whd in e2:(??%?);destruct; |#delta1' #delta2' #neb #e1 #e2 whd in e1:(??%?) e2:(??%?); destruct; %{1} %{1} %{1} //; ] | 7: //; | 4,5,6: ##skip ] *;#n2 *;#STORE #MINJ %{ n2} % //; % [ (* inj *) // | (* samedomain *) >(nextblock_store … STORE1) >(nextblock_store … STORE) //; | (* domain *) >(nextblock_store … STORE1) // | (* range *) /2/ | #b1 #delta1 #INJb1 >(low_bound_store … STORE b1) >(high_bound_store … STORE b1) @ms_range_2 //; ] qed. lemma store_outside_shift: ∀f,chunk,m1,b,ofs,m2,v,m2',delta. mem_shift f m1 m2 → f b = Some ? delta → high_bound m1 b + delta ≤ ofs ∨ ofs + size_chunk chunk ≤ low_bound m1 b + delta → store chunk m2 b ofs v = Some ? m2' → mem_shift f m1 m2'. #f #chunk #m1 #b #ofs #m2 #v #m2' #delta *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 #INJb #Hbounds #STORE % [ (* inj *) @(store_outside_inj … STORE) //; #b' #d' whd in ⊢ (??%? → ?); lapply (refl ? (f b')); elim (f b') in ⊢ (???% → %); [ #_ #e whd in e:(??%?); destruct; | #d'' #ef #e elim (grumpydestruct2 ?????? e); #eb #ed >eb in ef ⊢ % >ed >INJb #ed' <(grumpydestruct1 ??? ed') // ] | (* samedomain *) >(nextblock_store … STORE) // | (* domain *) // | (* range *) /2/ | #b1 #delta1 #INJb1 >(low_bound_store … STORE b1) >(high_bound_store … STORE b1) @ms_range_2 //; ] qed. lemma storev_shift: ∀f,chunk,m1,a1,v1,n1,m2,a2,v2. mem_shift f m1 m2 → storev chunk m1 a1 v1 = Some ? n1 → val_shift f a1 a2 → val_shift f v1 v2 → ∃n2. storev chunk m2 a2 v2 = Some ? n2 ∧ mem_shift f n1 n2. #f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2 #Hmem_shift #STOREV #Hval_shift_a #Hval_shift_v inversion Hval_shift_a; [ 1,2,4: #x #H >H in STOREV #H' whd in H':(??%?); @False_ind destruct; ] #b1 #ofs1 #b2 #ofs2 #delta whd in ⊢ (??%? → ?); lapply (refl ? (f b1)); elim (f b1) in ⊢ (???% → %); [#_ #e whd in e:(??%?); destruct; ] #x #INJb1 #e elim (grumpydestruct2 ?????? e); #eb #ex >ex in INJb1 #INJb1 #OFS #ea1 #ea2 >ea1 in STOREV #STOREV lapply (store_within_shift … Hmem_shift STOREV INJb1 Hval_shift_v); *; #n2 *; #A #B %{ n2} % //; >OFS >eb in A <(?:signed (add ofs1 (repr delta)) = signed ofs1 + delta) [ #H @H (* XXX /2/ *) | @(address_shift … chunk … Hmem_shift ? INJb1) @(store_valid_access_3 … STOREV) ] qed. (* Relation between shifts and [free]. *) lemma free_shift: ∀f,m1,m2,b. mem_shift f m1 m2 → mem_shift f (free m1 b) (free m2 b). #f #m1 #m2 #b *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 % [ (* inj *) @free_right_inj [ @free_left_inj // | #b1 #delta #chunk #ofs whd in ⊢ (??%? → ?); lapply (refl ? (f b1)); elim (f b1) in ⊢ (???% → %); [ #_ #e whd in e:(??%?); destruct; | #delta' #INJb1 #e whd in e:(??%?); destruct; napply valid_access_free_2 ] ] | (* samedomain *) whd in ⊢ (??%%); // | (* domain *) >(?:nextblock (free m1 b) = nextblock m1) // | (* range *) /2/ | #b' #delta #INJb' cases (decidable_eq_Z b' b); #eb [ >eb >(low_bound_free_same ??) >(high_bound_free_same ??) (* arith *) napply daemon | >(low_bound_free …) //; >(high_bound_free …) /2/; ] ] qed. (* Relation between shifts and allocation. *) definition shift_incr : memshift → memshift → Prop ≝ λf1,f2: memshift. ∀b. f1 b = f2 b ∨ f1 b = None ?. lemma shift_incr_inject_incr: ∀f1,f2. shift_incr f1 f2 → inject_incr (meminj_of_shift f1) (meminj_of_shift f2). #f1 #f2 #Hshift whd in ⊢ (?%%); whd; #b elim (Hshift b); #INJ >INJ /2/; qed. lemma val_shift_incr: ∀f1,f2,v1,v2. shift_incr f1 f2 → val_shift f1 v1 v2 → val_shift f2 v1 v2. #f1 #f2 #v1 #v2 #Hshift_incr whd in ⊢ (% → %); @val_inject_incr @shift_incr_inject_incr //; qed. (* * Remark mem_inj_incr: ∀f1,f2,m1,m2. inject_incr f1 f2 → mem_inj val_inject f1 m1 m2 → mem_inj val_inject f2 m1 m2. Proof. intros; red; intros. destruct (H b1). rewrite <- H3 in H1. exploit H0; eauto. intros [v2 [A B]]. exists v2; split. auto. apply val_inject_incr with f1; auto. congruence. ***) lemma alloc_shift: ∀f,m1,m2,lo1,hi1,m1',b,delta,lo2,hi2. mem_shift f m1 m2 → alloc m1 lo1 hi1 = 〈m1', b〉 → lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 → min_signed ≤ delta ∧ delta ≤ max_signed → min_signed ≤ lo2 → hi2 ≤ max_signed → inj_offset_aligned delta (hi1-lo1) → ∃f'. ∃m2'. alloc m2 lo2 hi2 = 〈m2', b〉 ∧ mem_shift f' m1' m2' ∧ shift_incr f f' ∧ f' b = Some ? delta. #f #m1 #m2 #lo1 #hi1 #m1' #b #delta #lo2 #hi2 *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 #ALLOC #Hlo_delta #Hhi_delta #Hdelta_range #Hlo_range #Hhi_range #Hinj_aligned lapply (refl ? (alloc m2 lo2 hi2)); elim (alloc m2 lo2 hi2) in ⊢ (???% → %); #m2' #b' #ALLOC2 cut (b' = b); [ >(alloc_result … ALLOC) >(alloc_result … ALLOC2) // ] #eb >eb cut (f b = None ?); [ lapply (ms_domain b); >(alloc_result … ALLOC) elim (f (nextblock m1)); //; #z (* arith *) napply daemon ] #FB letin f' ≝ (λb':block. if eqZb b' b then Some ? delta else f b'); cut (shift_incr f f'); [ whd; #b0 whd in ⊢ (?(???%)?); @eqZb_elim /2/; ] #Hshift_incr cut (f' b = Some ? delta); [ whd in ⊢ (??%?); >(eqZb_z_z …) // ] #efb' %{ f'} %{ m2'} % //; % //; % //; % [ (* inj *) cut (mem_inj val_inject (meminj_of_shift f') m1 m2); [ whd; #chunk #b1 #ofs #v1 #b2 #delta2 #MINJf' #LOAD cut (meminj_of_shift f b1 = Some ? 〈b2, delta2〉); [ eb cut (valid_block m1 b); [ @valid_access_valid_block [ 3: @load_valid_access // ] ] cut (¬valid_block m1 b); [ /2/ ] #H #H' @False_ind napply (absurd ? H' H) ] #MINJf lapply (ms_inj … MINJf LOAD); *; #v2 *; #A #B %{ v2} % //; @(val_inject_incr … B) @shift_incr_inject_incr // ] #Hmem_inj @(alloc_parallel_inj … delta Hmem_inj ALLOC ALLOC2 ?) /2/; whd in ⊢ (??%?); >efb' /2/; | (* samedomain *) >(nextblock_alloc … ALLOC) >(nextblock_alloc … ALLOC2) //; | (* domain *) #b0 (* FIXME: unfold *) >(refl ? (f' b0):f' b0 = if eqZb b0 b then Some ? delta else f b0) >(nextblock_alloc … ALLOC) >(alloc_result … ALLOC) @eqZb_elim #eb0 [ >eb0 (* arith *) napply daemon | lapply (ms_domain b0); elim (f b0); (* arith *) napply daemon ] | (* range *) #b0 #delta0 whd in ⊢ (??%? → ?); @eqZb_elim [ #_ #e <(grumpydestruct1 ??? e) // | #neb #e @(ms_range_1 … b0) @e ] | #b0 #delta0 whd in ⊢ (??%? → ?); >(low_bound_alloc … ALLOC2 ?) >(high_bound_alloc … ALLOC2 ?) @eqZb_elim #eb0 >eb [ >eb0 #ed <(grumpydestruct1 ??? ed) >(eqZb_z_z ?) /3/; | #edelta0 >(eqZb_false … eb0) @ms_range_2 whd in edelta0:(??%?); //; ] ] qed. *)*) (* ** Relation between signed and unsigned loads and stores *) (* Target processors do not distinguish between signed and unsigned stores of 8- and 16-bit quantities. We show these are equivalent. *) (* Signed 8- and 16-bit stores can be performed like unsigned stores. *) lemma in_bounds_equiv: ∀chunk1,chunk2,m,r,b,ofs.∀A:Type[0].∀a1,a2: A. typesize chunk1 = typesize chunk2 → (match in_bounds m chunk1 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) = (match in_bounds m chunk2 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]). #chunk1 #chunk2 #m #r #b #ofs #A #a1 #a2 #Hsize elim (in_bounds m chunk1 r b ofs); [ #H whd in ⊢ (??%?); >(in_bounds_true … A a1 a2 ?) //; @valid_access_compat //; | #H whd in ⊢ (??%?); elim (in_bounds m chunk2 r b ofs); //; #H' @False_ind @(absurd ?? H) @valid_access_compat //; ] qed. lemma storev_8_signed_unsigned: ∀m,a,v. storev (ASTint I8 Signed) m a v = storev (ASTint I8 Unsigned) m a v. #m #a #v whd in ⊢ (??%%); elim a // #ptr whd in ⊢ (??%%); >(in_bounds_equiv (ASTint I8 Signed) (ASTint I8 Unsigned) … (option mem) ???) // qed. lemma storev_16_signed_unsigned: ∀m,a,v. storev (ASTint I16 Signed) m a v = storev (ASTint I16 Unsigned) m a v. #m #a #v whd in ⊢ (??%%); elim a // #ptr whd in ⊢ (??%%); >(in_bounds_equiv (ASTint I16 Signed) (ASTint I16 Unsigned) … (option mem) ???) // qed. (* Likewise, some target processors (e.g. the PowerPC) do not have a ``load 8-bit signed integer'' instruction. We show that it can be synthesized as a ``load 8-bit unsigned integer'' followed by a sign extension. *) (* Nonessential properties that may require arithmetic lemma loadv_8_signed_unsigned: ∀m,a. loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a). #m #a whd in ⊢ (??%(????(%))); elim a; //; #r #b #ofs whd in ⊢ (??%(????%)); >(in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???) //; elim (in_bounds m Mint8unsigned r b (signed ofs)); /2/; #H whd in ⊢ (??%%); elim (getN 0 (signed ofs) (contents (blocks m b))); [ 1,3: //; | #i whd in ⊢ (??(??%)(??%)); >(sign_ext_zero_ext ?? i) [ @refl (* XXX: // ? *) | (* arith *) @daemon ] | #sp cases sp; //; ] qed. *) *)