matitaB/matita/contribs/ng_assembly2/emulator/memory/memory_abs.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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/memory/memory_func.ma".
  24 include "emulator/memory/memory_trees.ma".
  25 include "emulator/memory/memory_bits.ma".
  26
  27 (* ********************************************* *)
  28 (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
  29 (* ********************************************* *)
  30
  31 (* se si disattiva l'implementazione a funzione
  32    la memoria diventa un'oggetto confrontabile! *)
  33
  34 (* tipi di implementazione della memoria *)
  35 ninductive memory_impl : Type ≝
  36   (*MEM_FUNC: memory_impl
  37 |*) MEM_TREE: memory_impl
  38 | MEM_BITS: memory_impl.
  39
  40 (* ausiliario per il tipo della memoria *)
  41 ndefinition aux_mem_type ≝
  42 λt:memory_impl.match t with
  43  [ (*MEM_FUNC ⇒ oct → word16 → byte8
  44  |*) MEM_TREE ⇒ aux_20B_type byte8
  45  | MEM_BITS ⇒ aux_20B_type (Array8T bool)
  46  ].
  47
  48 (* ausiliario per il tipo del checker *)
  49 ndefinition aux_chk_type ≝
  50 λt:memory_impl.match t with
  51  [ (*MEM_FUNC ⇒ oct → word16 → memory_type
  52  |*) MEM_TREE ⇒ aux_20B_type memory_type
  53  | MEM_BITS ⇒ aux_20B_type (Array8T memory_type)
  54  ].
  55
  56 (* unificazione di out_of_bound_memory *)
  57 ndefinition out_of_bound_memory ≝
  58 λt:memory_impl.
  59  match t
  60   return λt.aux_chk_type t
  61  with
  62   [ (*MEM_FUNC ⇒ mf_out_of_bound_memory
  63   |*) MEM_TREE ⇒ mt_out_of_bound_memory
  64   | MEM_BITS ⇒ mb_out_of_bound_memory
  65   ].
  66
  67 (* unificazione di zero_memory *)
  68 ndefinition zero_memory ≝
  69 λt:memory_impl.
  70  match t
  71   return λt.aux_mem_type t
  72  with
  73   [ (*MEM_FUNC ⇒ mf_zero_memory
  74   |*) MEM_TREE ⇒ mt_zero_memory
  75   | MEM_BITS ⇒ mb_zero_memory
  76   ].
  77
  78 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
  79 ndefinition mem_read_abs ≝
  80 λt:memory_impl.
  81  match t
  82   return λt.aux_mem_type t → oct → word16 → byte8
  83  with
  84   [ (*MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
  85                m
  86   |*) MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
  87                mt_visit ? m
  88   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
  89                λsel:oct.λaddr:word16.
  90                byte8_of_bits (mt_visit ? m sel addr)
  91   ].
  92
  93 (* unificazione del chk *)
  94 ndefinition chk_get ≝
  95 λt:memory_impl.
  96  match t
  97   return λt.aux_chk_type t → oct → word16 → Array8T memory_type
  98  with
  99   [ (*MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.λsel:oct.λaddr:word16.
 100    match c sel addr with
 101     [ MEM_READ_ONLY ⇒ mk_Array8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
 102     | MEM_READ_WRITE ⇒ mk_Array8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
 103     | MEM_OUT_OF_BOUND ⇒ mk_Array8T ? 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
 104     ]
 105   |*) MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.λsel:oct.λaddr:word16.
 106    match mt_visit ? c sel addr with
 107     [ MEM_READ_ONLY ⇒ mk_Array8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
 108     | MEM_READ_WRITE ⇒ mk_Array8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
 109     | MEM_OUT_OF_BOUND ⇒ mk_Array8T ? 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
 110     ]
 111   | MEM_BITS ⇒ mt_visit ?
 112   ].
 113
 114 (* unificazione della lettura con chk: mem_read mem chk addr *)
 115 ndefinition mem_read ≝
 116 λt:memory_impl.
 117  match t
 118   return λt.aux_mem_type t → aux_chk_type t → oct → word16 → option byte8
 119  with
 120   [ (*MEM_FUNC ⇒ mf_mem_read
 121   |*) MEM_TREE ⇒ mt_mem_read
 122   | MEM_BITS ⇒ mb_mem_read
 123   ].
 124
 125 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
 126 ndefinition mem_read_bit ≝
 127 λt:memory_impl.
 128  match t
 129   return λt.aux_mem_type t → aux_chk_type t → oct → word16 → oct → option bool
 130  with
 131   [ (*MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 132                λc:aux_chk_type MEM_FUNC.
 133                λsel:oct.λaddr:word16.
 134                λo:oct.
 135                opt_map … (mf_mem_read m c sel addr)
 136                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
 137   |*) MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 138                λc:aux_chk_type MEM_TREE.
 139                λsel:oct.λaddr:word16.
 140                λo:oct.
 141                opt_map … (mt_mem_read m c sel addr)
 142                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
 143   | MEM_BITS ⇒ mb_mem_read_bit
 144   ].
 145
 146 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
 147 ndefinition mem_update ≝
 148 λt:memory_impl.
 149  match t
 150   return λt.aux_mem_type t → aux_chk_type t → oct → word16 → byte8 → option (aux_mem_type t)
 151  with
 152   [ (*MEM_FUNC ⇒ mf_mem_update
 153   |*) MEM_TREE ⇒ mt_mem_update
 154   | MEM_BITS ⇒ mb_mem_update
 155   ].
 156
 157 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
 158 ndefinition mem_update_bit ≝
 159 λt:memory_impl.
 160  match t
 161   return λt.aux_mem_type t → aux_chk_type t → oct → word16 → oct → bool → option (aux_mem_type t)
 162  with
 163   [ (*MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 164                λc:aux_chk_type MEM_FUNC.
 165                λsel:oct.λaddr:word16.
 166                λo:oct.
 167                λv:bool.
 168                mf_mem_update m c sel addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 (m addr)) v))
 169   |*) MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 170                λc:aux_chk_type MEM_TREE.
 171                λsel:oct.λaddr:word16.
 172                λo:oct.
 173                λv:bool.
 174                mt_mem_update m c sel addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 (mt_visit ? m sel addr)) v))
 175   | MEM_BITS ⇒ mb_mem_update_bit
 176   ].
 177
 178 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
 179 ndefinition load_from_source_at ≝
 180 λt:memory_impl.
 181  match t
 182   return λt.aux_mem_type t → list byte8 → oct → word16 → aux_mem_type t
 183  with
 184   [ (*MEM_FUNC ⇒ mf_load_from_source_at
 185   |*) MEM_TREE ⇒ mt_load_from_source_at
 186   | MEM_BITS ⇒ mb_load_from_source_at
 187   ].
 188
 189 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
 190 ndefinition check_update_ranged ≝
 191 λt:memory_impl.
 192  match t
 193   return λt.aux_chk_type t → oct → word16 → word16 → memory_type → aux_chk_type t
 194  with
 195   [ (*MEM_FUNC ⇒ mf_check_update_ranged
 196   |*) MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 197                λsel:oct.λaddr:word16.
 198                λrange:word16.
 199                mt_update_ranged ? c sel addr ? (w16_to_recw16 range)
 200   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 201                λsel:oct.λaddr:word16.
 202                λrange:word16.
 203                λv:memory_type.
 204                mt_update_ranged ? c sel addr ? (w16_to_recw16 range) (mk_Array8T ? v v v v v v v v)
 205   ].
 206
 207 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
 208 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
 209 ndefinition check_update_bit ≝
 210 λt:memory_impl.
 211  match t
 212   return λt.aux_chk_type t → oct → word16 → oct → memory_type → aux_chk_type t
 213  with
 214   [ (*MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 215                λsel:oct.λaddr:word16.
 216                λo:oct.
 217                λv:memory_type.
 218                c
 219   |*) MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 220                λsel:oct.λaddr:word16.
 221                λo:oct.
 222                λv:memory_type.
 223                c
 224   | MEM_BITS ⇒ mb_chk_update_bit
 225   ].
 226
 227 ndefinition mem_is_comparable: memory_impl → comparable.
 228  #m; @ (aux_mem_type m)
 229   ##[ nelim m;
 230       ##[ napply mt_zero_memory
 231       ##| napply mb_zero_memory ##]
 232   ##| nelim m;
 233       ##[ napply (forallc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
 234       ##| napply (forallc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
 235   ##| nelim m;
 236       ##[ napply (eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
 237       ##| napply (eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
 238   ##| nelim m;
 239       ##[ napply (eqc_to_eq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
 240       ##| napply (eqc_to_eq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
 241   ##| nelim m;
 242       ##[ napply (eq_to_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
 243       ##| napply (eq_to_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
 244   ##| nelim m;
 245       ##[ napply (neqc_to_neq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
 246       ##| napply (neqc_to_neq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
 247   ##| nelim m;
 248       ##[ napply (neq_to_neqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
 249       ##| napply (neq_to_neqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
 250   ##| nelim m;
 251       ##[ napply (decidable_c (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
 252       ##| napply (decidable_c (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
 253   ##| nelim m;
 254       ##[ napply (symmetric_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
 255       ##| napply (symmetric_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
 256   ##]
 257 nqed.
 258
 259 unification hint 0 ≔ M:memory_impl ⊢ carr (mem_is_comparable M) ≡ aux_mem_type M.
 260
 261 ndefinition chk_is_comparable: memory_impl → comparable.
 262  #m; @ (aux_chk_type m)
 263   ##[ nelim m;
 264       ##[ napply mt_out_of_bound_memory
 265       ##| napply mb_out_of_bound_memory ##]
 266   ##| nelim m;
 267       ##[ napply (forallc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
 268       ##| napply (forallc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
 269   ##| nelim m;
 270       ##[ napply (eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
 271       ##| napply (eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
 272   ##| nelim m;
 273       ##[ napply (eqc_to_eq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
 274       ##| napply (eqc_to_eq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
 275   ##| nelim m;
 276       ##[ napply (eq_to_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
 277       ##| napply (eq_to_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
 278   ##| nelim m;
 279       ##[ napply (neqc_to_neq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
 280       ##| napply (neqc_to_neq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
 281   ##| nelim m;
 282       ##[ napply (neq_to_neqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
 283       ##| napply (neq_to_neqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
 284   ##| nelim m;
 285       ##[ napply (decidable_c (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
 286       ##| napply (decidable_c (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
 287   ##| nelim m;
 288       ##[ napply (symmetric_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
 289       ##| napply (symmetric_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
 290   ##]
 291 nqed.
 292
 293 unification hint 0 ≔ M:memory_impl ⊢ carr (chk_is_comparable M) ≡ aux_chk_type M.