Changeset 1882 for src/joint/BEMem.ma


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r1419 r1882  
    4444     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
    4545
     46definition is_addressable : region → bool ≝ λr.match r with
     47  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
     48
     49
     50definition is_address : (beval × beval) → Prop ≝ λa.
     51  ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
     52    \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧
     53    \snd a = BVptr p p1 ∧ part_no ? p1 = 1.
     54
     55definition is_addressb : (beval × beval) → bool ≝ λa.
     56  match a with
     57  [ mk_Prod a0 a1 ⇒
     58    match a0 with
     59    [ BVptr p0 part0 ⇒
     60      is_addressable (ptype p0) ∧ eqb part0 0 ∧
     61        match a1 with
     62        [ BVptr p1 part1 ⇒
     63          eq_pointer p0 p1 ∧ eqb part1 1
     64        | _ ⇒ false
     65        ]
     66    | _ ⇒ false
     67    ]
     68  ].
     69
     70lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
     71  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
     72#P * *
     73[4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
     74#p0 #part0 #a1
     75whd in match is_addressb; normalize nodelta
     76elim (true_or_false_Prop (is_addressable (ptype p0)))
     77#H >H
     78[ @(eqb_elim part0 0) #Heq
     79  [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?);
     80    [4: @eq_pointer_elim #Heq'
     81      [ @(eqb_elim part1 1) #Heq''
     82        [ #Ptrue #_ @Ptrue destruct
     83          %{p1} [assumption] %{part0} %{part1}
     84          % [ % [ % ]] try % assumption
     85        ]
     86      ]
     87    ]
     88  ]
     89]
     90#_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' ***
     91#H0 #H1 #H2 #H3 destruct /2 by absurd/
     92qed.
     93
    4694(* CSC: only pointers to XRAM or code memory ATM *)
    4795definition address ≝ beval × beval.
     96definition safe_address ≝ Sig address is_address.
     97unification hint 0 ≔ ;
     98P ≟ Prod beval beval
     99(*------------------*)⊢
     100safe_address ≡ Sig P is_address.
    48101
    49102definition eq_address: address → address → bool ≝
     
    53106definition pointer_of_address: address → res pointer ≝
    54107 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
    55 definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
    56 
    57 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
     108 
     109definition pointer_of_address_safe : safe_address → pointer ≝
     110  λp.match \fst p return λx.\fst p = x → ? with
     111    [ BVptr ptr _ ⇒ λ_.ptr
     112    | _ ⇒ λabs.⊥
     113    ] (refl …).
     114lapply abs -abs cases p
     115* #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4
     116destruct(H0 H4)
     117qed.
     118
     119definition pointer_compat' ≝ λb,r.
     120  match b with
     121  [ mk_block r' z ⇒
     122    if eq_region r' r then True
     123    else
     124      match r with
     125      [ Any ⇒ True
     126      | XData ⇒ match r' with
     127        [ PData ⇒ True
     128        | _ ⇒ False
     129        ]
     130      | _ ⇒ False
     131      ]
     132   ].
     133
     134lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r.
     135** #z ** //
     136qed.
     137
     138lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r.
     139#b #r #H inversion H
     140[ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region %
     141| #id #EQ1 #EQ2 #EQ3 %
     142| #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) %
     143]
     144qed.
     145
     146lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
     147** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
     148cases r in Hr ⊢ %; #Hr *
     149** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
     150destruct normalize
     151@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     152@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     153#_ #_ normalize %
     154qed.
     155   
     156definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
     157
     158example address_of_pointer_OK_to_safe :
     159  ∀p,a.address_of_pointer p = OK … a → is_address a.
     160#p
     161lapply (refl … p)
     162generalize in match p in ⊢ (???%→%); **
     163whd in match (address_of_pointer ?);
     164#b #H #o #EQp * #a0 #a1
     165normalize #EQ destruct(EQ)
     166%{p} >EQp [1,3: %]
     167% [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
     168qed.
     169
     170definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
     171  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
     172
     173lemma address_of_pointer_is_safe :
     174  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
     175****#z #H
     176lapply (pointer_compat_from_ind ?? H) * #o
     177normalize %
     178qed.
     179
     180definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
     181code_pointer_of_beval_pair.
     182
    58183definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
    59184
     185definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
     186cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
     187lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
     188%{«mk_pointer ? (mk_block Code z) H o,I»}
     189% [2: % [2: % [ % [ % ]] % |]|]
     190qed.
     191
     192(* Paolo: why only code pointers and not XRAM too? *)
    60193definition addr_add: address → nat → res address ≝
    61194 λaddr,n.
     
    65198qed.
    66199
     200definition safe_addr_add: safe_address → nat → res safe_address ≝
     201 λaddr,n.
     202  do ptr ← code_pointer_of_address addr ;
     203  OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
     204normalize cases ptr #p #E @E
     205qed.
     206
    67207definition addr_sub: address → nat → res address ≝
    68208 λaddr,n.
     
    71211normalize cases ptr #p #E @E
    72212qed.
     213
     214definition safe_addr_sub: safe_address → nat → res safe_address ≝
     215 λaddr,n.
     216  do ptr ← code_pointer_of_address addr ;
     217  OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
     218normalize cases ptr #p #E @E
     219qed.
Note: See TracChangeset for help on using the changeset viewer.