Changeset 2176 for src/joint/BEMem.ma


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r1993 r2176  
    2323definition is_address : (beval × beval) → Prop ≝ λa.
    2424  ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
    25     \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧
    26     \snd a = BVptr p p1 ∧ part_no ? p1 = 1.
     25    \fst a = BVptr p p0 ∧ part_no p0 = 0 ∧
     26    \snd a = BVptr p p1 ∧ part_no p1 = 1.
    2727
    2828definition is_addressb : (beval × beval) → bool ≝ λa.
     
    4444  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
    4545#P * *
    46 [4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
     46[4:|*: [|#b0|(*#r0*)#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
    4747#p0 #part0 #a1
    4848whd in match is_addressb; normalize nodelta
     
    5050#H >H
    5151[ @(eqb_elim part0 0) #Heq
    52   [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?);
     52  [ cases a1 [|#b0|(*#r0*)#part0|#p1#part1] whd in match (?∧?);
    5353    [4: @eq_pointer_elim #Heq'
    5454      [ @(eqb_elim part1 1) #Heq''
     
    8989destruct(H0 H4)
    9090qed.
    91 
     91(* For full 8051 memory spaces
    9292definition pointer_compat' ≝ λb,r.
    9393  match b with
     
    116116]
    117117qed.
    118 
     118*)
    119119lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
     120** #a0 #a1 ***** #z #o
     121#Hr
     122(*
    120123** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
    121124cases r in Hr ⊢ %; #Hr *
     125*)
    122126** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
    123127destruct normalize
     
    133137#p
    134138lapply (refl … p)
    135 generalize in match p in ⊢ (???%→%); **
     139generalize in match p in ⊢ (???%→%); *(***)
    136140whd in match (address_of_pointer ?);
    137 #b #H #o #EQp * #a0 #a1
     141#b (*#H*) #o #EQp * #a0 #a1
    138142normalize #EQ destruct(EQ)
     143%{p} >EQp [ cases (block_region b) // | % [2: % [2: % [ % [ % ] ] ] ] %
     144(*
    139145%{p} >EQp [1,3: %]
    140146% [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
     147*)
    141148qed.
    142149
     
    146153lemma address_of_pointer_is_safe :
    147154  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
     155#p normalize % qed.
     156(*
    148157****#z #H
    149158lapply (pointer_compat_from_ind ?? H) * #o
    150159normalize %
    151 qed.
     160qed.*)
    152161
    153162definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
     
    157166
    158167definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
     168cases H -H * #b #o normalize cases b * #z #EQ destruct
     169%{«mk_pointer  (mk_block Code z)  o,I»}
     170% [2: % [2: % [ % [ % ]]]] %
     171qed.
     172(*
    159173cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
    160174lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
    161175%{«mk_pointer ? (mk_block Code z) H o,I»}
    162176% [2: % [2: % [ % [ % ]] % |]|]
    163 qed.
     177qed.*)
    164178
    165179(* Paolo: why only code pointers and not XRAM too? *)
Note: See TracChangeset for help on using the changeset viewer.