helm/software/matita/library/freescale/memory_func.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_func/".
  28
  29 (*include "/media/VIRTUOSO/freescale/memory_struct.ma".*)
  30 include "freescale/memory_struct.ma".
  31
  32 (* ********************* *)
  33 (* MEMORIA E DESCRITTORE *)
  34 (* ********************* *)
  35
  36 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
  37 definition mf_check_update_ranged ≝
  38 λf:word16 → memory_type.λi.λs.λv.
  39  λx.match in_range x i s with
  40   [ true ⇒ v
  41   | false ⇒ f x ].
  42
  43 (* tutta la memoria non installata *)
  44 definition mf_out_of_bound_memory ≝ λ_:word16.MEM_OUT_OF_BOUND.
  45
  46 (* (mf_mem_update mem check addr val) = scrivi controllando il tipo di memoria *)
  47 definition mf_mem_update ≝
  48 λf:word16 → byte8.λc:word16 → memory_type.λa.λv.
  49  match c a with
  50   (* ROM? ok, ma il valore viene perso *)
  51   [ MEM_READ_ONLY ⇒ Some ? f
  52   (* RAM? ok *)
  53   | MEM_READ_WRITE ⇒ Some ? (λx.match eq_w16 x a with [ true ⇒ v | false ⇒ f x ])
  54   (* NON INSTALLATA? no *)
  55   | MEM_OUT_OF_BOUND ⇒ None ? ].
  56
  57 (* tutta la memoria a 0 *)
  58 definition mf_zero_memory ≝ λ_:word16.〈x0,x0〉.
  59
  60 (* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *)
  61 definition mf_mem_read ≝
  62 λf:word16 → byte8.λc:word16 → memory_type.λa.
  63  match c a with
  64   [ MEM_READ_ONLY ⇒ Some ? (f a)
  65   | MEM_READ_WRITE ⇒ Some ? (f a)
  66   | MEM_OUT_OF_BOUND ⇒ None ? ].
  67
  68 (* ************************** *)
  69 (* CARICAMENTO PROGRAMMA/DATI *)
  70 (* ************************** *)
  71
  72 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
  73 let rec mf_load_from_source_at (old_mem:word16 → byte8) (source:list byte8) (addr:word16) on source ≝
  74 match source with
  75  (* fine di source: carica da old_mem *)
  76  [ nil ⇒ old_mem
  77  | cons hd tl ⇒ λx:word16.match lt_w16 x addr with
  78   (* e' prima di source: carica da old_mem *)
  79   [ true ⇒ old_mem x
  80   | false ⇒ match eq_w16 x addr with
  81    (* la locazione corrisponde al punto corrente di source *)
  82    [ true ⇒ hd
  83    (* la locazione e' piu' avanti: ricorsione *)
  84    | false ⇒ (mf_load_from_source_at old_mem tl (plus_w16nc addr 〈〈x0,x0〉:〈x0,x1〉〉)) x
  85    ]
  86   ]
  87  ].
  88
  89 (* ********************** *)
  90 (* TEOREMI/LEMMMI/ASSIOMI *)
  91 (* ********************** *)
  92
  93 (*
  94 lemma mem_update_mem_update_a_a:
  95  ∀s,a,v1,v2,b.
  96   mem_update (mem_update s a v1) a v2 b = mem_update s a v2 b.
  97  intros;
  98  unfold mem_update;
  99  unfold mem_update;
 100  elim (eqb b a);
 101  reflexivity.
 102 qed.
 103
 104 lemma mem_update_mem_update_a_b:
 105  ∀s,a1,v1,a2,v2,b.
 106   a1 ≠ a2 →
 107    mem_update (mem_update s a1 v1) a2 v2 b = mem_update (mem_update s a2 v2) a1 v1 b.
 108  intros;
 109  unfold mem_update;
 110  unfold mem_update;
 111  apply (bool_elim ? (eqb b a1)); intros;
 112  apply (bool_elim ? (eqb b a2)); intros;
 113  simplify;
 114  [ elim H;
 115    rewrite < (eqb_true_to_eq ? ? H1);
 116    apply eqb_true_to_eq;
 117    assumption
 118  |*: reflexivity
 119  ].
 120 qed.
 121
 122 lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
 123  intros;
 124  unfold update;
 125  apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
 126   [ rewrite > (eqb_true_to_eq ? ? H);
 127     reflexivity
 128   | reflexivity
 129   ]
 130 qed.
 131
 132 lemma inj_update:
 133  ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
 134  intros;
 135  unfold update;
 136  apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
 137   [ reflexivity
 138   | apply H;
 139     intro;
 140     autobatch
 141   ]
 142 qed.
 143
 144 lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
 145  intros;
 146  unfold update;
 147  rewrite > not_eq_to_eqb_false; simplify;
 148   [ reflexivity
 149   | intro;
 150     autobatch
 151   ]
 152 qed.
 153 *)