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