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