1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 set "baseuri" "cic:/matita/freescale/memory_func/".
29 (*include "/media/VIRTUOSO/freescale/memory_struct.ma".*)
30 include "freescale/memory_struct.ma".
32 (* ********************* *)
33 (* MEMORIA E DESCRITTORE *)
34 (* ********************* *)
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
43 (* tutta la memoria non installata *)
44 definition mf_out_of_bound_memory ≝ λ_:word16.MEM_OUT_OF_BOUND.
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.
50 (* ROM? ok, ma il valore viene perso *)
51 [ MEM_READ_ONLY ⇒ Some ? f
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 ? ].
57 (* tutta la memoria a 0 *)
58 definition mf_zero_memory ≝ λ_:word16.〈x0,x0〉.
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.
64 [ MEM_READ_ONLY ⇒ Some ? (f a)
65 | MEM_READ_WRITE ⇒ Some ? (f a)
66 | MEM_OUT_OF_BOUND ⇒ None ? ].
68 (* ************************** *)
69 (* CARICAMENTO PROGRAMMA/DATI *)
70 (* ************************** *)
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 ≝
75 (* fine di source: carica da old_mem *)
77 | cons hd tl ⇒ λx:word16.match lt_w16 x addr with
78 (* e' prima di source: carica da old_mem *)
80 | false ⇒ match eq_w16 x addr with
81 (* la locazione corrisponde al punto corrente di source *)
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
89 (* ********************** *)
90 (* TEOREMI/LEMMMI/ASSIOMI *)
91 (* ********************** *)
94 lemma mem_update_mem_update_a_a:
96 mem_update (mem_update s a v1) a v2 b = mem_update s a v2 b.
104 lemma mem_update_mem_update_a_b:
107 mem_update (mem_update s a1 v1) a2 v2 b = mem_update (mem_update s a2 v2) a1 v1 b.
111 apply (bool_elim ? (eqb b a1)); intros;
112 apply (bool_elim ? (eqb b a2)); intros;
115 rewrite < (eqb_true_to_eq ? ? H1);
116 apply eqb_true_to_eq;
122 lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
125 apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
126 [ rewrite > (eqb_true_to_eq ? ? H);
133 ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
136 apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
144 lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
147 rewrite > not_eq_to_eqb_false; simplify;