]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/assembly/freescale/load_write.ma
a wrong conjecture bypassed!
[helm.git] / matita / matita / contribs / assembly / freescale / load_write.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/model.ma".
28
29 (* errori possibili nel fetch *)
30 inductive error_type : Type ≝
31   ILL_OP: error_type
32 | ILL_FETCH_AD: error_type
33 | ILL_EX_AD: error_type.
34
35 (* un tipo opzione ad hoc
36    - errore: interessa solo l'errore
37    - ok: interessa info e il nuovo pc
38 *)
39 inductive fetch_result (A:Type) : Type ≝
40   FetchERR : error_type → fetch_result A
41 | FetchOK  : A → word16 → fetch_result A.
42
43 (* **************************** *)
44 (* FETCH E ACCESSO ALLA MEMORIA *)
45 (* **************************** *)
46
47 (* ausialiaria per RS08 read *)
48 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
49    memory mapped, quindi bisona intercettare la lettura.
50    NB: fare molta attenzione alle note sulle combinazioni possibili perche'
51        il comportamento della memoria nell'RS08 e' strano e ci sono
52        precise condizioni che impediscono una semantica circolare dell'accesso
53        (divergenza=assenza di definizione) *)
54 definition RS08_memory_filter_read_aux ≝
55 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
56 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option T.
57 match s with
58  [ mk_any_status alu mem chk _ ⇒ match alu with
59   [ mk_alu_RS08 _ _ _ _ xm psm _ _ ⇒
60 (* 
61    possibili accessi al registro X
62    1) addr=000F: diretto
63    2) addr=000E (X =0F): indiretto
64    3) addr=00CF (PS=00): paging
65   
66    [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
67    non si possono combinare due effetti contemporaneamente!
68    per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni 
69 *) 
70   match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
71         (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
72         (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
73    [ true ⇒ fREG xm
74    | false ⇒
75 (* 
76    possibili accessi al registro PS
77    1) addr=001F: diretto
78    2) addr=000E (X =1F): indiretto
79    3) addr=00DF (PS=00): paging
80 *)
81     match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
82          (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
83          (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
84      [ true ⇒ fREG psm
85      | false ⇒
86 (* 
87    accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging 
88    altrimenti sarebbero 2 indirezioni
89 *)
90       match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
91        [ true ⇒ fMEM mem chk 〈〈x0,x0〉:xm〉
92        | false ⇒ 
93 (* 
94    accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
95 *)
96         match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
97          [ true ⇒ fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
98                                              (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
99 (*
100    accesso normale
101 *)
102          | false ⇒ fMEM mem chk addr ]]]]]].
103
104 (* lettura RS08 di un byte *)
105 definition RS08_memory_filter_read ≝
106 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
107  RS08_memory_filter_read_aux t s addr byte8
108   (λb.Some byte8 b)
109   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read t m c a).
110
111 (* lettura RS08 di un bit *)
112 definition RS08_memory_filter_read_bit ≝
113 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.
114  RS08_memory_filter_read_aux t s addr bool
115   (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
116   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read_bit t m c a sub).
117
118 (* in caso di RS08 si dirotta sul filtro, altrimenti si legge direttamente *)
119 definition memory_filter_read ≝
120 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
121  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
122   mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
123  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.
124   mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
125  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.
126   mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
127  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.
128   RS08_memory_filter_read t s addr
129  ].
130
131 definition memory_filter_read_bit ≝
132 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
133  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
134   mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
135  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.
136   mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
137  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.
138   mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
139  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.
140   RS08_memory_filter_read_bit t s addr sub
141  ].
142
143 (* ausialiaria per RS08 write *)
144 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
145    memory mapped, quindi bisona intercettare la scrittura.
146    NB: fare molta attenzione alle note sulle combinazioni possibili perche'
147        il comportamento della memoria nell'RS08 e' strano e ci sono
148        precise condizioni che impediscono una semantica circolare dell'accesso
149        (divergenza=assenza di definizione) *)
150 definition RS08_memory_filter_write_aux ≝
151 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
152 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option (aux_mem_type t).
153 match s with 
154  [ mk_any_status alu mem chk clk ⇒ match alu with
155   [ mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl ⇒
156 (* 
157    possibili accessi al registro X
158    1) addr=000F: diretto
159    2) addr=000E (X =0F): indiretto
160    3) addr=00CF (PS=00): paging
161   
162    [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
163    non si possono combinare due effetti contemporaneamente!
164    per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni 
165 *) 
166   match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
167         (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
168         (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
169    [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc (fREG xm) psm zfl cfl) mem chk clk)
170    | false ⇒
171 (* 
172    possibili accessi al registro PS
173    1) addr=001F: diretto
174    2) addr=000E (X =1F): indiretto
175    3) addr=00DF (PS=00): paging
176 *)
177     match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
178          (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
179          (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
180      [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm (fREG psm) zfl cfl) mem chk clk)
181      | false ⇒
182 (* 
183    accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging 
184    altrimenti sarebbero 2 indirezioni
185 *)
186       match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
187        [ true ⇒ opt_map ?? (fMEM mem chk 〈〈x0,x0〉:xm〉)
188                  (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
189                                                       
190        | false ⇒
191 (* 
192    accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
193 *)
194         match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
195          [ true ⇒ opt_map ?? (fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
196                                                    (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉)))
197                    (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
198 (*
199    accesso normale
200 *)
201          | false ⇒ opt_map ?? (fMEM mem chk addr)
202                     (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
203
204 (* scrittura RS08 di un byte *)
205 definition RS08_memory_filter_write ≝
206 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λval:byte8.
207  RS08_memory_filter_write_aux t s addr
208   (λb.val)
209   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update t m c a val).
210
211 (* scrittura RS08 di un bit *)
212 definition RS08_memory_filter_write_bit ≝
213 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
214  RS08_memory_filter_write_aux t s addr
215   (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
216   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update_bit t m c a sub val).
217
218 (* in caso di RS08 si dirotta sul filtro, altrimenti si scrive direttamente *)
219 definition memory_filter_write ≝
220 λm:mcu_type.λt:memory_impl.match m
221  return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
222  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
223   opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
224    (λmem.Some ? (set_mem_desc ? t s mem)) 
225  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λval:byte8.
226   opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
227    (λmem.Some ? (set_mem_desc ? t s mem))
228  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8.
229   opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
230    (λmem.Some ? (set_mem_desc ? t s mem)) 
231  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
232   RS08_memory_filter_write t s addr val
233  ].
234
235 definition memory_filter_write_bit ≝
236 λm:mcu_type.λt:memory_impl.match m
237  return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
238  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
239   opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
240    (λmem.Some ? (set_mem_desc ? t s mem)) 
241  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
242   opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
243    (λmem.Some ? (set_mem_desc ? t s mem))
244  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
245   opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
246    (λmem.Some ? (set_mem_desc ? t s mem)) 
247  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
248   RS08_memory_filter_write_bit t s addr sub val
249  ].
250
251 (*
252    Da utilizzarsi solo per gli aggiornamenti di PC (per il fetch),
253    NON per il caricamento degli indiretti.
254    - il caricamento degli immediati spetta al fetcher
255      (incremento progressivo di PC ciclo per ciclo, e riempimento del prefetch
256       che a questo punto DEVE poter indirizzare qualsiasi locazione puntata da PC)
257    - il caricamento degli indiretti non spetta al fetcher
258 *)
259 definition filtered_inc_w16 ≝
260 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
261  get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
262
263 let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
264  match n with
265   [ O ⇒ w
266   | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
267
268 (* 
269    errore1: non esiste traduzione ILL_OP
270    errore2: non e' riuscito a leggere ILL_FETCH_AD
271    altrimenti OK=info+new_pc
272 *)
273 definition fetch ≝
274 λm:mcu_type.λt:memory_impl.λs:any_status m t.
275  let pc ≝ get_pc_reg m t s in
276  let pc_next1 ≝ filtered_inc_w16 m t s pc in
277  let pc_next2 ≝ filtered_inc_w16 m t s pc_next1 in
278  match memory_filter_read m t s pc with
279   [ None ⇒ FetchERR ? ILL_FETCH_AD
280   | Some bh ⇒ match full_info_of_word16 m (Byte bh) with
281    (* non ha trovato una traduzione con 1 byte *)
282    [ None ⇒ match m with
283     (* HC05 non esistono op a 2 byte *)
284     [ HC05 ⇒ FetchERR ? ILL_OP
285     | HC08 ⇒ match eq_b8 bh 〈x9,xE〉 with
286      (* HC08 se il primo byte e' 0x9E il secondo puo' avere senso *)
287      [ true ⇒ match memory_filter_read m t s pc_next1 with
288       [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
289       [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
290      (* HC08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
291      | false ⇒ FetchERR ? ILL_OP
292      ]
293     | HCS08 ⇒ match eq_b8 bh 〈x9,xE〉 with
294      (* HCS08 se il primo byte e' 0x9E il secondo puo' avere senso *)
295      [ true ⇒ match memory_filter_read m t s pc_next1 with
296       [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
297       [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
298      (* HCS08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
299      | false ⇒ FetchERR ? ILL_OP
300      ]
301     (* RS08 non esistono op a 2 byte *)
302     | RS08 ⇒ FetchERR ? ILL_OP
303     ]
304    (* ha trovato una traduzione con 1 byte *)
305    | Some info ⇒ FetchOK ? info pc_next1 ]].
306
307 (* ************************ *)
308 (* MODALITA' INDIRIZZAMENTO *)
309 (* ************************ *)
310
311 (* mattoni base *)
312 (* - incrementano l'indirizzo normalmente *)
313 (* - incrementano PC attraverso il filtro *)
314
315 (* lettura byte da addr *)
316 definition loadb_from ≝
317 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
318  opt_map ?? (memory_filter_read m t s addr)
319   (λb.Some ? (tripleT ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
320
321 (* lettura bit da addr *)
322 definition loadbit_from ≝
323 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
324  opt_map ?? (memory_filter_read_bit m t s addr sub)
325   (λb.Some ? (tripleT ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
326
327 (* lettura word da addr *)
328 definition loadw_from ≝
329 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
330  opt_map ?? (memory_filter_read m t s addr)
331   (λbh.opt_map ?? (memory_filter_read m t s (succ_w16 addr))
332    (λbl.Some ? (tripleT ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
333
334 (* scrittura byte su addr *)
335 definition writeb_to ≝
336 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
337  opt_map ?? (memory_filter_write m t s addr writeb)
338   (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
339
340 (* scrittura bit su addr *)
341 definition writebit_to ≝
342 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
343  opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
344   (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
345
346 (* scrittura word su addr *) 
347 definition writew_to ≝
348 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
349  opt_map ?? (memory_filter_write m t s addr (w16h writew))
350   (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
351     (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
352
353 (* ausiliari per definire i tipi e la lettura/scrittura *)
354
355 (* ausiliaria per definire il tipo di aux_load *)
356 definition aux_load_typing ≝
357 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
358  any_status m t → word16 → word16 → nat →
359  option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
360
361 (* per non dover ramificare i vari load in byte/word *)
362 definition aux_load ≝
363 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
364  [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
365
366 (* ausiliaria per definire il tipo di aux_write *)
367 definition aux_write_typing ≝
368 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
369  any_status m t → word16 → word16 → nat →
370  match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
371  option (Prod (any_status m t) word16).
372
373 (* per non dover ramificare i vari load in byte/word *)
374 definition aux_write ≝
375 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
376  [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
377
378 (* modalita' vere e proprie *)
379
380 (* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
381 definition mode_IMM1_load ≝
382 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
383  opt_map ?? (memory_filter_read m t s cur_pc)
384   (λb.Some ? (tripleT ??? s b (filtered_inc_w16 m t s cur_pc))).
385
386 (* lettura da [curpc]: IMM1 + estensione a word *)
387 definition mode_IMM1EXT_load ≝
388 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
389  opt_map ?? (memory_filter_read m t s cur_pc)
390   (λb.Some ? (tripleT ??? s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
391
392 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
393 definition mode_IMM2_load ≝
394 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
395  opt_map ?? (memory_filter_read m t s cur_pc)
396   (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
397    (λbl.Some ? (tripleT ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
398
399 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
400 definition mode_DIR1_load ≝
401 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
402  opt_map ?? (memory_filter_read m t s cur_pc)
403   (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
404
405 (* lettura da [byte [curpc]]: loadbit *)
406 definition mode_DIR1n_load ≝
407 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
408  opt_map ?? (memory_filter_read m t s cur_pc)
409   (λaddr.loadbit_from m t  s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
410
411 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
412 definition mode_DIR1_write ≝
413 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
414 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
415  opt_map ?? (memory_filter_read m t s cur_pc)
416   (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
417
418 (* scrittura su [byte [curpc]]: writebit *)
419 definition mode_DIR1n_write ≝
420 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
421  opt_map ?? (memory_filter_read m t s cur_pc)
422   (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
423
424 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
425 definition mode_DIR2_load ≝
426 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
427  opt_map ?? (memory_filter_read m t s cur_pc)
428   (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
429    (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
430
431 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
432 definition mode_DIR2_write ≝
433 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
434 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
435  opt_map ?? (memory_filter_read m t s cur_pc)
436   (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
437    (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
438
439 definition get_IX ≝
440 λm:mcu_type.λt:memory_impl.λs:any_status m t.
441  match m with
442   [ HC05 ⇒ opt_map ?? (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉) 
443   | HC08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx) 
444   | HCS08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx) 
445   | RS08 ⇒ None ? ].
446
447 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
448 definition mode_IX0_load ≝
449 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
450  opt_map ?? (get_IX m t s)
451   (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
452
453 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
454 definition mode_IX0_write ≝
455 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
456 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
457  opt_map ?? (get_IX m t s)
458   (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
459
460 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
461 definition mode_IX1_load ≝
462 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
463  opt_map ?? (get_IX m t s)
464   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
465    (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
466
467 (* lettura da X+[byte curpc] *)
468 definition mode_IX1ADD_load ≝
469 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
470  opt_map ?? (memory_filter_read m t s cur_pc)
471   (λb.opt_map ?? (get_IX m t s)
472    (λaddr.Some ? (tripleT ??? s (plus_w16nc addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
473
474 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
475 definition mode_IX1_write ≝
476 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
477 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
478  opt_map ?? (get_IX m t s)
479   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
480    (λoffs.(aux_write m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
481
482 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
483 definition mode_IX2_load ≝
484 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
485  opt_map ?? (get_IX m t s)
486   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
487    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
488     (λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
489
490 (* lettura da X+[word curpc] *)
491 definition mode_IX2ADD_load ≝
492 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
493  opt_map ?? (memory_filter_read m t s cur_pc)
494   (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
495    (λbl.opt_map ?? (get_IX m t s)
496     (λaddr.Some ? (tripleT ??? s (plus_w16nc addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
497
498 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
499 definition mode_IX2_write ≝
500 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
501 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
502  opt_map ?? (get_IX m t s)
503   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
504    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
505     (λoffsl.(aux_write m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2 writebw))).
506
507 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
508 definition mode_SP1_load ≝
509 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
510  opt_map ?? (get_sp_reg m t s)
511   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
512    (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
513
514 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
515 definition mode_SP1_write ≝
516 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
517 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
518  opt_map ?? (get_sp_reg m t s)
519   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
520    (λoffs.(aux_write m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
521
522 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
523 definition mode_SP2_load ≝
524 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
525  opt_map ?? (get_sp_reg m t s)
526   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
527    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
528     (λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
529
530 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
531 definition mode_SP2_write ≝
532 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
533 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
534  opt_map ?? (get_sp_reg m t s)
535   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
536    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
537     (λoffsl.(aux_write m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2 writebw))).
538
539 (* ************************************** *)
540 (* raccordo di tutte le possibili letture *)
541 (* ************************************** *)
542
543 (* H:X++ *)
544 definition aux_inc_indX_16 ≝
545 λm:mcu_type.λt:memory_impl.λs:any_status m t.
546  opt_map ?? (get_indX_16_reg m t s)
547   (λX_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 X_op))
548    (λs_tmp.Some ? s_tmp)).
549
550 (* tutte le modalita' di lettura: false=loadb true=loadw *)
551 definition multi_mode_load ≝
552 λbyteflag:bool.λm:mcu_type.λt:memory_impl.
553  match byteflag
554  return λbyteflag:bool.any_status m t → word16 → instr_mode → 
555   option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
556  with
557   (* lettura di un byte *)
558   [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
559 (* NO: non ci sono indicazioni *)
560    [ MODE_INH  ⇒ None ?
561 (* restituisce A *)
562    | MODE_INHA ⇒ Some ? (tripleT ??? s (get_acc_8_low_reg m t s) cur_pc)
563 (* restituisce X *)
564    | MODE_INHX ⇒ opt_map ?? (get_indX_8_low_reg m t s)
565                   (λindx.Some ? (tripleT ??? s indx cur_pc))
566 (* restituisce H *)
567    | MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
568                   (λindx.Some ? (tripleT ??? s indx cur_pc))
569
570 (* NO: solo lettura word *)
571   | MODE_INHX0ADD ⇒ None ?
572 (* NO: solo lettura word *)
573   | MODE_INHX1ADD ⇒ None ?
574 (* NO: solo lettura word *)
575   | MODE_INHX2ADD ⇒ None ?
576
577 (* preleva 1 byte immediato *) 
578    | MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
579 (* NO: solo lettura word *)
580    | MODE_IMM1EXT ⇒ None ?
581 (* NO: solo lettura word *)
582    | MODE_IMM2 ⇒ None ?
583 (* preleva 1 byte da indirizzo diretto 1 byte *) 
584    | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
585 (* preleva 1 byte da indirizzo diretto 1 word *)
586    | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
587 (* preleva 1 byte da H:X *)
588    | MODE_IX0  ⇒ mode_IX0_load true m t s cur_pc
589 (* preleva 1 byte da H:X+1 byte offset *)
590    | MODE_IX1  ⇒ mode_IX1_load true m t s cur_pc
591 (* preleva 1 byte da H:X+1 word offset *)
592    | MODE_IX2  ⇒ mode_IX2_load true m t s cur_pc
593 (* preleva 1 byte da SP+1 byte offset *)
594    | MODE_SP1  ⇒ mode_SP1_load true m t s cur_pc
595 (* preleva 1 byte da SP+1 word offset *)
596    | MODE_SP2  ⇒ mode_SP2_load true m t s cur_pc
597
598 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
599    | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
600 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
601    | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
602 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
603    | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
604 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
605    | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
606
607 (* NO: solo lettura word/scrittura byte *)
608    | MODE_INHA_and_IMM1 ⇒ None ?
609 (* NO: solo lettura word/scrittura byte *)     
610    | MODE_INHX_and_IMM1 ⇒ None ?
611 (* NO: solo lettura word *) 
612    | MODE_IMM1_and_IMM1 ⇒ None ?
613 (* NO: solo lettura word/scrittura byte *) 
614    | MODE_DIR1_and_IMM1 ⇒ None ?
615 (* NO: solo lettura word/scrittura byte *) 
616    | MODE_IX0_and_IMM1  ⇒ None ?
617 (* NO: solo lettura word *) 
618    | MODE_IX0p_and_IMM1 ⇒ None ?
619 (* NO: solo lettura word/scrittura byte *) 
620    | MODE_IX1_and_IMM1  ⇒ None ?
621 (* NO: solo lettura word *) 
622    | MODE_IX1p_and_IMM1 ⇒ None ?
623 (* NO: solo lettura word/scrittura byte *) 
624    | MODE_SP1_and_IMM1  ⇒ None ?
625
626 (* NO: solo scrittura byte *)
627    | MODE_DIRn _          ⇒ None ?
628 (* NO: solo lettura word *)
629    | MODE_DIRn_and_IMM1 _ ⇒ None ?
630 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
631    | MODE_TNY e           ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
632                              (λb.Some ? (tripleT ??? s b cur_pc))
633 (* preleva 1 byte da 0000 0000 000x xxxxb *)
634    | MODE_SRT e           ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
635                              (λb.Some ? (tripleT ??? s b cur_pc))
636    ]
637 (* lettura di una word *)
638   | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
639 (* NO: non ci sono indicazioni *)
640    [ MODE_INH  ⇒ None ?
641 (* NO: solo lettura/scrittura byte *)
642    | MODE_INHA ⇒ None ?
643 (* NO: solo lettura/scrittura byte *)
644    | MODE_INHX ⇒ None ?
645 (* NO: solo lettura/scrittura byte *)
646    | MODE_INHH ⇒ None ?
647
648 (* preleva 1 word immediato *) 
649   | MODE_INHX0ADD ⇒ opt_map ?? (get_IX m t s)
650                      (λw.Some ? (tripleT ??? s w cur_pc))
651 (* preleva 1 word immediato *) 
652   | MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
653 (* preleva 1 word immediato *) 
654   | MODE_INHX2ADD ⇒ mode_IX2ADD_load m t s cur_pc
655
656 (* NO: solo lettura byte *)
657    | MODE_IMM1 ⇒ None ?
658 (* preleva 1 word immediato *) 
659    | MODE_IMM1EXT ⇒ mode_IMM1EXT_load m t s cur_pc
660 (* preleva 1 word immediato *) 
661    | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
662 (* preleva 1 word da indirizzo diretto 1 byte *) 
663    | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
664 (* preleva 1 word da indirizzo diretto 1 word *) 
665    | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
666 (* preleva 1 word da H:X *)
667    | MODE_IX0  ⇒ mode_IX0_load false m t s cur_pc
668 (* preleva 1 word da H:X+1 byte offset *)
669    | MODE_IX1  ⇒ mode_IX1_load false m t s cur_pc
670 (* preleva 1 word da H:X+1 word offset *)
671    | MODE_IX2  ⇒ mode_IX2_load false m t s cur_pc
672 (* preleva 1 word da SP+1 byte offset *)
673    | MODE_SP1  ⇒ mode_SP1_load false m t s cur_pc
674 (* preleva 1 word da SP+1 word offset *)
675    | MODE_SP2  ⇒ mode_SP2_load false m t s cur_pc
676
677 (* NO: solo lettura/scrittura byte *)
678    | MODE_DIR1_to_DIR1 ⇒ None ?
679 (* NO: solo lettura/scrittura byte *)
680    | MODE_IMM1_to_DIR1 ⇒ None ?
681 (* NO: solo lettura/scrittura byte *)
682    | MODE_IX0p_to_DIR1 ⇒ None ?
683 (* NO: solo lettura/scrittura byte *)
684    | MODE_DIR1_to_IX0p ⇒ None ?
685
686 (* preleva 2 byte, possibilita' modificare Io argomento *)
687    | MODE_INHA_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
688                            (λS_immb_and_PC.match S_immb_and_PC with
689                             [ tripleT _ immb cur_pc' ⇒
690                              Some ? (tripleT ??? s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
691 (* preleva 2 byte, possibilita' modificare Io argomento *)
692    | MODE_INHX_and_IMM1 ⇒ opt_map ?? (get_indX_8_low_reg m t s)
693                            (λX_op.opt_map ?? (mode_IMM1_load m t s cur_pc)
694                             (λS_immb_and_PC.match S_immb_and_PC with
695                              [ tripleT _ immb cur_pc' ⇒
696                               Some ? (tripleT ??? s 〈X_op:immb〉 cur_pc')]))
697 (* preleva 2 byte, NO possibilita' modificare Io argomento *)               
698    | MODE_IMM1_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
699                            (λS_immb1_and_PC.match S_immb1_and_PC with
700                             [ tripleT _ immb1 cur_pc' ⇒
701                              opt_map ?? (mode_IMM1_load m t s cur_pc')
702                               (λS_immb2_and_PC.match S_immb2_and_PC with
703                                [ tripleT _ immb2 cur_pc'' ⇒
704                                 Some ? (tripleT ??? s 〈immb1:immb2〉 cur_pc'')])])
705 (* preleva 2 byte, possibilita' modificare Io argomento *)
706    | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load true m t s cur_pc)
707                            (λS_dirb_and_PC.match S_dirb_and_PC with
708                             [ tripleT _ dirb cur_pc' ⇒
709                              opt_map ?? (mode_IMM1_load m t s cur_pc')
710                               (λS_immb_and_PC.match S_immb_and_PC with
711                                [ tripleT _ immb cur_pc'' ⇒
712                                 Some ? (tripleT ??? s 〈dirb:immb〉 cur_pc'')])])
713 (* preleva 2 byte, possibilita' modificare Io argomento *)
714    | MODE_IX0_and_IMM1  ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
715                            (λS_ixb_and_PC.match S_ixb_and_PC with
716                             [ tripleT _ ixb cur_pc' ⇒
717                              opt_map ?? (mode_IMM1_load m t s cur_pc')
718                               (λS_immb_and_PC.match S_immb_and_PC with
719                                [ tripleT _ immb cur_pc'' ⇒
720                                 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
721 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
722    | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
723                            (λS_ixb_and_PC.match S_ixb_and_PC with
724                             [ tripleT _ ixb cur_pc' ⇒
725                              opt_map ?? (mode_IMM1_load m t s cur_pc')
726                               (λS_immb_and_PC.match S_immb_and_PC with
727                                [ tripleT _ immb cur_pc'' ⇒
728                                 (* H:X++ *)
729                                 opt_map ?? (aux_inc_indX_16 m t s)
730                                  (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
731 (* preleva 2 byte, possibilita' modificare Io argomento *)
732    | MODE_IX1_and_IMM1  ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
733                            (λS_ixb_and_PC.match S_ixb_and_PC with
734                             [ tripleT _ ixb cur_pc' ⇒
735                              opt_map ?? (mode_IMM1_load m t s cur_pc')
736                               (λS_immb_and_PC.match S_immb_and_PC with
737                                [ tripleT _ immb cur_pc'' ⇒
738                                 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
739 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
740    | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
741                            (λS_ixb_and_PC.match S_ixb_and_PC with
742                             [ tripleT _ ixb cur_pc' ⇒
743                              opt_map ?? (mode_IMM1_load m t s cur_pc')
744                               (λS_immb_and_PC.match S_immb_and_PC with
745                                [ tripleT _ immb cur_pc'' ⇒
746                                 (* H:X++ *)
747                                 opt_map ?? (aux_inc_indX_16 m t s)
748                                  (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
749 (* preleva 2 byte, possibilita' modificare Io argomento *)
750    | MODE_SP1_and_IMM1  ⇒ opt_map ?? (mode_SP1_load true m t s cur_pc)
751                            (λS_spb_and_PC.match S_spb_and_PC with
752                             [ tripleT _ spb cur_pc' ⇒
753                              opt_map ?? (mode_IMM1_load m t s cur_pc')
754                               (λS_immb_and_PC.match S_immb_and_PC with
755                                [ tripleT _ immb cur_pc'' ⇒
756                                 Some ? (tripleT ??? s 〈spb:immb〉 cur_pc'')])])
757
758 (* NO: solo scrittura byte *)
759    | MODE_DIRn _            ⇒ None ?
760 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
761    | MODE_DIRn_and_IMM1 msk ⇒ opt_map ?? (mode_DIR1n_load m t s cur_pc msk)
762                                (λS_dirbn_and_PC.match S_dirbn_and_PC with
763                                 [ tripleT _ dirbn cur_pc'   ⇒
764                                  opt_map ?? (mode_IMM1_load m t s cur_pc')
765                                   (λS_immb_and_PC.match S_immb_and_PC with
766                                    [ tripleT _ immb cur_pc'' ⇒
767                                      Some ? (tripleT ??? s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
768 (* NO: solo lettura/scrittura byte *)
769    | MODE_TNY _             ⇒ None ?
770 (* NO: solo lettura/scrittura byte *)
771    | MODE_SRT _             ⇒ None ?
772    ]
773   ].
774
775 (* **************************************** *)
776 (* raccordo di tutte le possibili scritture *)
777 (* **************************************** *)
778
779 (* tutte le modalita' di scrittura: true=writeb, false=writew *)
780 definition multi_mode_write ≝
781 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
782  return λbyteflag:bool.any_status m t → word16 → instr_mode →
783   match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
784   option (Prod (any_status m t) word16) with
785  (* scrittura di un byte *)
786  [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
787 (* NO: non ci sono indicazioni *)
788   [ MODE_INH        ⇒ None ?
789 (* scrive A *)
790   | MODE_INHA       ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
791 (* scrive X *)
792   | MODE_INHX       ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
793                       (λtmps.Some ? (pair ?? tmps cur_pc)) 
794 (* scrive H *)
795   | MODE_INHH       ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
796                        (λtmps.Some ? (pair ?? tmps cur_pc)) 
797
798 (* NO: solo lettura word *)
799   | MODE_INHX0ADD ⇒ None ?
800 (* NO: solo lettura word *)
801   | MODE_INHX1ADD ⇒ None ?
802 (* NO: solo lettura word *)
803   | MODE_INHX2ADD ⇒ None ?
804
805 (* NO: solo lettura byte *)
806   | MODE_IMM1       ⇒ None ?
807 (* NO: solo lettura word *)
808   | MODE_IMM1EXT    ⇒ None ?
809 (* NO: solo lettura word *)
810   | MODE_IMM2       ⇒ None ?
811 (* scrive 1 byte su indirizzo diretto 1 byte *)
812   | MODE_DIR1       ⇒ mode_DIR1_write true m t s cur_pc writeb
813 (* scrive 1 byte su indirizzo diretto 1 word *)
814   | MODE_DIR2       ⇒ mode_DIR2_write true m t s cur_pc writeb
815 (* scrive 1 byte su H:X *)
816   | MODE_IX0        ⇒ mode_IX0_write true m t s cur_pc writeb
817 (* scrive 1 byte su H:X+1 byte offset *)
818   | MODE_IX1        ⇒ mode_IX1_write true m t s cur_pc writeb
819 (* scrive 1 byte su H:X+1 word offset *)
820   | MODE_IX2        ⇒ mode_IX2_write true m t s cur_pc writeb
821 (* scrive 1 byte su SP+1 byte offset *)
822   | MODE_SP1        ⇒ mode_SP1_write true m t s cur_pc writeb
823 (* scrive 1 byte su SP+1 word offset *)
824   | MODE_SP2        ⇒ mode_SP2_write true m t s cur_pc writeb
825
826 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
827   | MODE_DIR1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
828 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
829   | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
830 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
831   | MODE_IX0p_to_DIR1   ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
832                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
833                             (* H:X++ *)
834                             opt_map ?? (aux_inc_indX_16 m t S_op)
835                              (λS_op'.Some ? (pair ?? S_op' PC_op))])
836 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
837   | MODE_DIR1_to_IX0p   ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
838                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
839                             (* H:X++ *)
840                             opt_map ?? (aux_inc_indX_16 m t S_op)
841                              (λS_op'.Some ? (pair ?? S_op' PC_op))])
842
843 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
844   | MODE_INHA_and_IMM1 ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
845 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)  
846   | MODE_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
847                            (λtmps.Some ? (pair ?? tmps cur_pc)) 
848 (* NO: solo lettura word *) 
849   | MODE_IMM1_and_IMM1 ⇒ None ?
850 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *) 
851   | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
852 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
853   | MODE_IX0_and_IMM1  ⇒ mode_IX0_write true m t s cur_pc writeb
854 (* NO: solo lettura word *) 
855   | MODE_IX0p_and_IMM1 ⇒ None ?
856 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
857   | MODE_IX1_and_IMM1  ⇒ mode_IX1_write true m t s cur_pc writeb
858 (* NO: solo lettura word *) 
859   | MODE_IX1p_and_IMM1 ⇒ None ?
860 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
861   | MODE_SP1_and_IMM1  ⇒ mode_SP1_write true m t s cur_pc writeb
862
863 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
864   | MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))   
865 (* NO: solo lettura word *)
866   | MODE_DIRn_and_IMM1 _ ⇒ None ?
867 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
868   | MODE_TNY e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
869                    (λtmps.Some ? (pair ?? tmps cur_pc))
870 (* scrive 1 byte su 0000 0000 000x xxxxb *)
871   | MODE_SRT e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
872                       (λtmps.Some ? (pair ?? tmps cur_pc)) ]
873  (* scrittura di una word *)
874  | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
875 (* NO: non ci sono indicazioni *)
876   [ MODE_INH        ⇒ None ?
877 (* NO: solo lettura/scrittura byte *)
878   | MODE_INHA       ⇒ None ?
879 (* NO: solo lettura/scrittura byte *)
880   | MODE_INHX       ⇒ None ?
881 (* NO: solo lettura/scrittura byte *)
882   | MODE_INHH       ⇒ None ?
883
884 (* NO: solo lettura word *)
885   | MODE_INHX0ADD ⇒ None ?
886 (* NO: solo lettura word *)
887   | MODE_INHX1ADD ⇒ None ?
888 (* NO: solo lettura word *)
889   | MODE_INHX2ADD ⇒ None ?
890
891 (* NO: solo lettura byte *)
892   | MODE_IMM1       ⇒ None ?
893 (* NO: solo lettura word *)
894   | MODE_IMM1EXT    ⇒ None ?
895 (* NO: solo lettura word *)
896   | MODE_IMM2       ⇒ None ?
897 (* scrive 1 word su indirizzo diretto 1 byte *) 
898   | MODE_DIR1       ⇒ mode_DIR1_write false m t s cur_pc writew
899 (* scrive 1 word su indirizzo diretto 1 word *)
900   | MODE_DIR2       ⇒ mode_DIR2_write false m t s cur_pc writew
901 (* scrive 1 word su H:X *)
902   | MODE_IX0        ⇒ mode_IX0_write false m t s cur_pc writew
903 (* scrive 1 word su H:X+1 byte offset *)
904   | MODE_IX1        ⇒ mode_IX1_write false m t s cur_pc writew
905 (* scrive 1 word su H:X+1 word offset *)
906   | MODE_IX2        ⇒ mode_IX2_write false m t s cur_pc writew
907 (* scrive 1 word su SP+1 byte offset *)
908   | MODE_SP1        ⇒ mode_SP1_write false m t s cur_pc writew
909 (* scrive 1 word su SP+1 word offset *)
910   | MODE_SP2        ⇒ mode_SP2_write false m t s cur_pc writew
911
912 (* NO: solo lettura/scrittura byte *)
913   | MODE_DIR1_to_DIR1 ⇒ None ?
914 (* NO: solo lettura/scrittura byte *)
915   | MODE_IMM1_to_DIR1 ⇒ None ?
916 (* NO: solo lettura/scrittura byte *)
917   | MODE_IX0p_to_DIR1 ⇒ None ?
918 (* NO: solo lettura/scrittura byte *)
919   | MODE_DIR1_to_IX0p ⇒ None ?
920
921 (* NO: solo lettura word/scrittura byte *)
922   | MODE_INHA_and_IMM1 ⇒ None ?
923 (* NO: solo lettura word/scrittura byte *)     
924   | MODE_INHX_and_IMM1 ⇒ None ?
925 (* NO: solo lettura word *) 
926   | MODE_IMM1_and_IMM1 ⇒ None ?
927 (* NO: solo lettura word/scrittura byte *) 
928   | MODE_DIR1_and_IMM1 ⇒ None ?
929 (* NO: solo lettura word/scrittura byte *) 
930   | MODE_IX0_and_IMM1  ⇒ None ?
931 (* NO: solo lettura word *) 
932   | MODE_IX0p_and_IMM1 ⇒ None ?
933 (* NO: solo lettura word/scrittura byte *)
934   | MODE_IX1_and_IMM1  ⇒ None ?
935 (* NO: solo lettura word *) 
936   | MODE_IX1p_and_IMM1 ⇒ None ?
937 (* NO: solo lettura word/scrittura byte *) 
938   | MODE_SP1_and_IMM1  ⇒ None ?
939
940 (* NO: solo scrittura byte *)
941   | MODE_DIRn _          ⇒ None ?
942 (* NO: solo lettura word *)
943   | MODE_DIRn_and_IMM1 _ ⇒ None ?
944 (* NO: solo lettura/scrittura byte *)
945   | MODE_TNY _           ⇒ None ?
946 (* NO: solo lettura/scrittura byte *)
947   | MODE_SRT _           ⇒ None ?
948   ]
949  ].