matita/contribs/assembly/freescale/memory_trees.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/memory_struct.ma".
  28
  29 (* ********************* *)
  30 (* MEMORIA E DESCRITTORE *)
  31 (* ********************* *)
  32
  33 (* tutta la memoria non installata *)
  34 definition mt_out_of_bound_memory ≝
  35 let lev4 ≝ array_16T ?
  36            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  37            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  38            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  39            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  40            in
  41 let lev3 ≝ array_16T ?
  42            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  43            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  44            in
  45 let lev2 ≝ array_16T ?
  46            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  47            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  48            in
  49 let lev1 ≝ array_16T ?
  50            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  51            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  52            in
  53 lev1.
  54
  55 (* tutta la memoria a 0 *)
  56 definition mt_zero_memory ≝
  57 let lev4 ≝ array_16T ?
  58            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  59            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  60            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  61            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  62            in
  63 let lev3 ≝ array_16T ?
  64            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  65            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  66            in
  67 let lev2 ≝ array_16T ?
  68            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  69            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  70            in
  71 let lev1 ≝ array_16T ?
  72            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  73            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  74            in
  75 lev1.
  76
  77 (* visita di un albero da 64KB di elementi: ln16(65536)=4 passaggi *)
  78 definition mt_visit ≝
  79 λT:Type.λdata:Prod16T (Prod16T (Prod16T (Prod16T T))).λaddr:word16.
  80  match addr with
  81   [ mk_word16 wh wl ⇒
  82  getn_array16T (b8l wl) ?
  83   (getn_array16T (b8h wl) ?
  84    (getn_array16T (b8l wh) ?
  85     (getn_array16T (b8h wh) ? data))) ].
  86
  87 (* scrittura di un elemento in un albero da 64KB *)
  88 definition mt_update ≝
  89 λT:Type.λdata:Prod16T (Prod16T (Prod16T (Prod16T T))).λaddr:word16.λv:T.
  90  match addr with
  91   [ mk_word16 wh wl ⇒
  92  let lev2 ≝ getn_array16T (b8h wh) ? data in
  93  let lev3 ≝ getn_array16T (b8l wh) ? lev2 in
  94  let lev4 ≝ getn_array16T (b8h wl) ? lev3 in
  95  setn_array16T (b8h wh) ? data
  96   (setn_array16T (b8l wh) ? lev2
  97    (setn_array16T (b8h wl) ? lev3
  98     (setn_array16T (b8l wl) T lev4 v))) ].
  99
 100 (* scrittura di un range in un albero da 64KB *)
 101 definition mt_update_ranged ≝
 102 λT:Type.λdata:Prod16T (Prod16T (Prod16T (Prod16T T))).λi,s:word16.λv:T.
 103  (* ok i≤s *)
 104  match le_w16 i s with
 105   [ true ⇒
 106  match i with
 107   [ mk_word16 ih il ⇒
 108  match s with
 109   [ mk_word16 sh sl ⇒
 110  let aux_4 ≝ Prod16T T in
 111  let aux_3 ≝ Prod16T (Prod16T T) in
 112  let aux_2 ≝ Prod16T (Prod16T (Prod16T T)) in
 113
 114  let ilev2 ≝ getn_array16T (b8h ih) aux_2 data in
 115  let ilev3 ≝ getn_array16T (b8l ih) aux_3 ilev2 in
 116  let ilev4 ≝ getn_array16T (b8h il) aux_4 ilev3 in
 117
 118  let slev2 ≝ getn_array16T (b8h sh) aux_2 data in
 119  let slev3 ≝ getn_array16T (b8l sh) aux_3 slev2 in
 120  let slev4 ≝ getn_array16T (b8h sl) aux_4 slev3 in
 121
 122  let vlev4 ≝ array_16T T v v v v v v v v v v v v v v v v in
 123  let vlev3 ≝ array_16T aux_4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4
 124                              vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 in
 125  let vlev2 ≝ array_16T aux_3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3
 126                              vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 in
 127
 128  match eq_ex (b8h ih) (b8h sh) with
 129   [ true ⇒ match eq_ex (b8l ih) (b8l sh) with
 130    [ true ⇒ match eq_ex (b8h il) (b8h sl) with
 131     (* caso 0x...(X) a 0x...(Y) *)
 132     [ true ⇒ setn_array16T (b8h ih) aux_2 data
 133               (setn_array16T (b8l ih) aux_3 ilev2
 134                (setn_array16T (b8h il) aux_4 ilev3
 135                 (* cambio a partire da livello 4 *)
 136                 (setmn_array16T (b8l il) (b8l sl) T ilev4 v))) (* ...X,...Y *)
 137     (* caso 0x..(X1)(X2) a 0x..(Y1)(Y2) *)
 138     | false ⇒ setn_array16T (b8h ih) aux_2 data
 139                (setn_array16T (b8l ih) aux_3 ilev2
 140                 (* cambio a partire da livello 3 *)
 141                 (setn_array16T (b8h sl) aux_4 (* ..(Y1)0,..(Y1)(Y2) *)
 142                  (setmn_array16T_succ_pred (b8h il) (b8h sl) aux_4 (* ..(X1+1).,..(Y1-1). *)
 143                   (setn_array16T (b8h il) aux_4 ilev3
 144                    (setmn_array16T (b8l il) xF T ilev4 v)) (* ..(X1)(X2),..(X1)F *)
 145                   vlev4)
 146                  (setmn_array16T x0 (b8l sl) T slev4 v))) ]
 147    (* caso 0x.(X1)(X2)(X3) a 0x..(Y1)(Y2)(Y3) *)
 148    | false ⇒ setn_array16T (b8h ih) aux_2 data
 149               (* cambio a partire da livello 2 *)
 150               (setn_array16T (b8l sh) aux_3
 151                (setmn_array16T_succ_pred (b8l ih) (b8l sh) aux_3 (* .(X1+1)..,.(Y1-1).. *)
 152                 (setn_array16T (b8l ih) aux_3 ilev2
 153                  (setmn_array16T_succ (b8h il) aux_4 (* .(X1)(X2+1).,.(X1)F. *)
 154                   (setn_array16T (b8h il) aux_4 ilev3
 155                    (setmn_array16T (b8l il) xF T ilev4 v)) (* .(X1)(X2)(X3),.(X1)(X2)F *)
 156                   vlev4))
 157                 vlev3)
 158                (setmn_array16T_pred (b8h sl) aux_4 (* .(Y1)0.,.(Y1)(Y2-1). *)
 159                 (setn_array16T (b8h sl) aux_4 slev3
 160                  (setmn_array16T x0 (b8l sl) T slev4 v)) (* .(Y1)(Y2)0,.(Y1)(Y2)(Y3) *)
 161                 vlev4))
 162    ]
 163   (* caso 0x(X1)(X2)(X3)(X4) a 0x(Y1)(Y2)(Y3)(Y4) *)
 164   | false ⇒ setn_array16T (b8h sh) aux_2
 165              (setmn_array16T_succ_pred (b8h ih) (b8h sh) aux_2 (* (X+1)...,(Y-1)... *)
 166               (setn_array16T (b8h ih) aux_2 data
 167                (setmn_array16T_succ (b8l ih) aux_3 (* (X1)(X2+1)..,(X1)F.. *)
 168                 (setn_array16T (b8l ih) aux_3 ilev2
 169                  (setmn_array16T_succ (b8h il) aux_4 (* (X1)(X2)(X3+1).,(X1)(X2)F. *)
 170                   (setn_array16T (b8h il) aux_4 ilev3
 171                    (setmn_array16T (b8l il) xF T ilev4 v)) (* (X1)(X2)(X3)(X4),(X1)(X2)(X3)F *)
 172                   vlev4))
 173                 vlev3))
 174                vlev2)
 175              (setmn_array16T_pred (b8l sh) aux_3 (* (Y1)0..,(Y1)(Y2-1).. *)
 176               (setn_array16T (b8l sh) aux_3 slev2
 177                (setmn_array16T_pred (b8h sl) aux_4 (* (Y1)(Y2)0.,(Y1)(Y2)(Y3-1). *)
 178                 (setn_array16T (b8h sl) aux_4 slev3
 179                  (setmn_array16T x0 (b8l sl) T slev4 v)) (* (Y1)(Y2)(Y3)0,(Y1)(Y2)(Y3)(Y4) *)
 180                 vlev4))
 181               vlev3) ]]]
 182  (* no i>s *)
 183  | false ⇒ data
 184  ].
 185
 186 definition mt_chk_get ≝
 187 λchk:Prod16T (Prod16T (Prod16T (Prod16T memory_type))).λaddr:word16.
 188  match mt_visit ? chk addr with
 189  [ MEM_READ_ONLY ⇒ array_8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
 190  | MEM_READ_WRITE ⇒ array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
 191  | MEM_OUT_OF_BOUND ⇒ array_8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
 192  ].
 193
 194 (* scrivi controllando il tipo di memoria *)
 195 definition mt_mem_update ≝
 196 λmem:Prod16T (Prod16T (Prod16T (Prod16T byte8))).
 197 λchk:Prod8T memory_type.
 198 λaddr:word16.λv:byte8.
 199  match getn_array8T o0 ? chk with
 200   (* ROM? ok, ma il valore viene perso *)
 201   [ MEM_READ_ONLY ⇒ Some ? mem
 202   (* RAM? ok *)
 203   | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
 204   (* NON INSTALLATA? no *)
 205   | MEM_OUT_OF_BOUND ⇒ None ? ].
 206
 207 (* leggi controllando il tipo di memoria *)
 208 definition mt_mem_read ≝
 209 λmem:Prod16T (Prod16T (Prod16T (Prod16T byte8))).
 210 λchk:Prod16T (Prod16T (Prod16T (Prod16T memory_type))).
 211 λaddr:word16.
 212  match  mt_visit ? chk addr with
 213   [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
 214   | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
 215   | MEM_OUT_OF_BOUND ⇒ None ? ].
 216
 217 (* ************************** *)
 218 (* CARICAMENTO PROGRAMMA/DATI *)
 219 (* ************************** *)
 220
 221 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
 222 let rec mt_load_from_source_at (old_mem:Prod16T (Prod16T (Prod16T (Prod16T byte8))))
 223                                (source:list byte8) (addr:word16) on source ≝
 224 match source with
 225  (* fine di source: carica da old_mem *)
 226  [ nil ⇒ old_mem
 227  | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
 228   (* non supera 0xFFFF, ricorsione *)
 229   [ true ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16nc addr 〈〈x0,x0〉:〈x0,x1〉〉)
 230   (* supera 0xFFFF, niente ricorsione *)
 231   | false ⇒ mt_update ? old_mem addr hd
 232   ]].
 233
 234 (* ********************** *)
 235 (* TEOREMI/LEMMMI/ASSIOMI *)
 236 (* ********************** *)
 237
 238 (* lettura da locazione diversa da quella in cui scrivo e' vecchio *)
 239 (* NB: sembra corretto, ma 2^32 casi!!! *)
 240 (*
 241 lemma ok_mt_update :
 242  forall_word16 (λaddr1.
 243  forall_word16 (λaddr2.
 244   (eq_w16 addr1 addr2) ⊙
 245   (eq_b8 (mt_visit ? (mt_update ? mt_zero_memory addr1 〈xF,xF〉) addr2)
 246          (mk_byte8 x0 x0))))
 247   = true.
 248  reflexivity.
 249 qed.
 250 *)
 251
 252 (* verifica scrittura di range *)
 253 (* NB: sembra corretto, ma 2^48 casi!!! *)
 254 (*
 255 lemma ok_mt_update_ranged :
 256  forall_word16 (λaddr1.
 257  forall_word16 (λaddr2.
 258  forall_word16 (λaddr3.
 259   (in_range addr3 addr1 addr2) ⊙
 260   (eq_b8 (mt_visit ? (mt_update_ranged ? mt_zero_memory addr1 addr2 〈xF,xF〉) addr3)
 261          (mk_byte8 x0 x0)))))
 262   = true.
 263  reflexivity.
 264 qed.
 265 *)