Changeset 2286 for src/joint/BEMem.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r2185 r2286  
    2020  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
    2121
    22 
    2322definition is_address : (beval × beval) → Prop ≝ λa.
    24   ∃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.
    27 
     23  ∃b : Σb.bool_to_Prop (is_addressable (block_region b)).
     24  ∃p0,p1,o0,o1.
     25    \fst a = BVptr b p0 o0 ∧ part_no … p0 = 0 ∧
     26    \snd a = BVptr b p1 o1 ∧ part_no … p1 = 1 ∧
     27    bool_to_Prop (vsuffix … (eq_bv 8) o0 o1).
     28
     29(*
    2830definition is_addressb : (beval × beval) → bool ≝ λa.
    29   match a with
    30   [ mk_Prod a0 a1 ⇒
    31     match a0 with
    32     [ BVptr p0 part0 ⇒
    33       is_addressable (ptype p0) ∧ eqb part0 0 ∧
     31  let 〈a0,a1〉 ≝ a in
     32  match a0 with
     33  [ BVptr b0 part0 o0 ⇒
     34      is_addressable (block_region b0) ∧ eqb part0 0 ∧
    3435        match a1 with
    35         [ BVptr p1 part1 ⇒
    36           eq_pointer p0 p1 ∧ eqb part1 1
     36        [ BVptr b1 part1 o1 ⇒
     37          eq_block b0 b1 ∧ eqb part1 1 ∧ subvector_with … (eq_bv 8) o0 o1
    3738        | _ ⇒ false
    3839        ]
    39     | _ ⇒ false
    40     ]
     40  | _ ⇒ false
    4141  ].
    4242
    4343lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
    4444  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
    45 #P * *
    46 [4:|*: [|#b0|(*#r0*)#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
    47 #p0 #part0 #a1
    48 whd in match is_addressb; normalize nodelta
    49 elim (true_or_false_Prop (is_addressable (ptype p0)))
    50 #H >H
    51 [ @(eqb_elim part0 0) #Heq
    52   [ cases a1 [|#b0|(*#r0*)#part0|#p1#part1] whd in match (?∧?);
    53     [4: @eq_pointer_elim #Heq'
    54       [ @(eqb_elim part1 1) #Heq''
    55         [ #Ptrue #_ @Ptrue destruct
    56           %{p1} [assumption] %{part0} %{part1}
    57           % [ % [ % ]] try % assumption
     45#P * * [||#b0|(*#r0*)#part0|#b0#part0#o0] #a1
     46[5: whd in match is_addressb; normalize nodelta
     47  elim (true_or_false_Prop (is_addressable (block_region b0)))
     48  #H >H
     49  [ @(eqb_elim part0 0) #Heq
     50    [ cases a1 [||#b1|(*#r1*)#part1|#b1#part1#o1] whd in match (?∧?);
     51      [5: @eq_block_elim #Heq'
     52        [ @(eqb_elim part1 1) #Heq''
     53          [ elim (true_or_false_Prop (subvector_with … (eq_bv 8) o0 o1)) #Heq''' >Heq'''
     54            [ #Ptrue #_ @Ptrue destruct
     55              %{b1} [assumption] %{part0} %{part1} %{o0} %{o1}
     56              % [ % [ % [ % ]]] try assumption %
     57            ]
     58          ]
    5859        ]
    5960      ]
     
    6162  ]
    6263]
    63 #_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' ***
    64 #H0 #H1 #H2 #H3 destruct /2 by absurd/
    65 qed.
     64#_ #Pfalse @Pfalse % ** #b0' #H' * #part0' * #part1' * #o0' * #o1' ****
     65#H0 #H1 #H2 #H3 #H4 destruct /2 by absurd/
     66qed.
     67*)
    6668
    6769(* CSC: only pointers to XRAM or code memory ATM *)
    6870definition address ≝ beval × beval.
    69 definition safe_address ≝ Sig address is_address.
     71
     72(* definition safe_address ≝ Sig address is_address.
    7073unification hint 0 ≔ ;
    7174P ≟ Prod beval beval
    7275(*------------------*)⊢
    73 safe_address ≡ Sig P is_address.
     76safe_address ≡ Sig P is_address. *)
    7477
    7578definition eq_address: address → address → bool ≝
     
    7982definition pointer_of_address: address → res pointer ≝
    8083 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
    81  
    82 definition pointer_of_address_safe : safe_address → pointer ≝
    83   λp.match \fst p return λx.\fst p = x → ? with
    84     [ BVptr ptr _ ⇒ λ_.ptr
    85     | _ ⇒ λabs.⊥
    86     ] (refl …).
    87 lapply abs -abs cases p
    88 * #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4
    89 destruct(H0 H4)
    90 qed.
     84
     85lemma bevals_of_pointer_is_address :
     86  ∀p.is_address (list_to_pair … (bevals_of_pointer p) (refl …)).
     87* #b * #o whd in ⊢ (?%); whd
     88%{b} [ elim (block_region b) % ] %{(mk_part 0 ?)} [ %2 %1 ] %{(mk_part 1 ?)} [ %1 ]
     89@(vsplit_elim … 8 8 o) #o1 #o0 #EQ >EQ -o
     90%{[[o0]]} %{[[o1;o0]]}
     91% [2: change with (bool_to_Prop (if eq_bv ??? then ? else ?))
     92      >eq_bv_refl % ]
     93%%[2: normalize nodelta @vsplit_elim #pre >(Vector_O … pre) #post #EQ
     94      normalize in EQ; <EQ -pre -post
     95      whd in match (rvsplit ????);
     96      <(vsplit_prod … (refl …)) normalize nodelta
     97  | % [2: % ]
     98  ]
     99whd in match (rvsplit ????);
     100try <(vector_append_empty … o0) in ⊢ (??%?);
     101<(vsplit_prod … (refl …)) normalize nodelta %
     102qed.
     103
     104lemma is_address_to_pointer : ∀a.is_address a → ∃p.pointer_of_address a = return p.
     105* #a0 #a1 ** #bl #bl_prf ** #p0 #p0_prf ** #p1 #p1_prf * #o0' * #o1o0 ****
     106#EQ1 #EQ2 #EQ3 #EQ4 destruct
     107@(Vector_pair_elim … o1o0) #o1 #o0 #EQ >EQ -o1o0
     108@(Vector_singl_elim … o0') #o0'' #EQ >EQ -o0'
     109whd in ⊢ (?%→?);
     110@eq_bv_elim #EQ * >EQ -o0''
     111whd in match (pointer_of_address ?);
     112>eq_block_b_b >(eqb_n_n 1)
     113>vsuffix_vflatten
     114[2: change with (bool_to_Prop (vsuffix ????? ([[?]]@@[[?]])))
     115  @vsuffix_true change with (bool_to_Prop (if eq_bv ? o0 o0 then ? else ?))
     116  >eq_bv_refl % ]
     117normalize nodelta
     118whd in ⊢ (??(λ_.??%?));
     119% [2: % |]
     120qed.
     121
    91122(* For full 8051 memory spaces
    92123definition pointer_compat' ≝ λb,r.
     
    117148qed.
    118149*)
    119 lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
     150(*lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
    120151** #a0 #a1 ***** #z #o
    121152#Hr
     
    130161@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
    131162#_ #_ normalize %
    132 qed.
     163qed.*)
    133164   
    134165definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
     
    136167example address_of_pointer_OK_to_safe :
    137168  ∀p,a.address_of_pointer p = OK … a → is_address a.
    138 #p
    139 lapply (refl … p)
    140 generalize in match p in ⊢ (???%→%); *(***)
    141 whd in match (address_of_pointer ?);
    142 #b (*#H*) #o #EQp * #a0 #a1
    143 normalize #EQ destruct(EQ)
    144 %{p} >EQp [ cases (block_region b) // | % [2: % [2: % [ % [ % ] ] ] ] %
    145 (*
    146 %{p} >EQp [1,3: %]
    147 % [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
    148 *)
    149 qed.
    150 
    151 definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
     169#p #a whd in match address_of_pointer; normalize nodelta
     170#EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
     171//
     172qed.
     173
     174(*definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
    152175  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
    153176
     
    177200% [2: % [2: % [ % [ % ]] % |]|]
    178201qed.*)
     202*)
    179203
    180204(* Paolo: why only code pointers and not XRAM too? *)
    181 definition addr_add: address → nat → res address ≝
     205(*definition addr_add: address → nat → res address ≝
    182206 λaddr,n.
    183207  do ptr ← code_pointer_of_address addr ;
     
    206230normalize cases ptr #p #E @E
    207231qed.
     232*)
Note: See TracChangeset for help on using the changeset viewer.