opt_map ?? (memory_filter_read m t s cur_pc)
(λb.Some ? (tripleT ??? s b (filtered_inc_w16 m t s cur_pc))).
+(* lettura da [curpc]: IMM1 + estensione a word *)
+definition mode_IMM1EXT_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map ?? (memory_filter_read m t s cur_pc)
+ (λb.Some ? (tripleT ??? s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
+
(* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
definition mode_IMM2_load ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
(λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
+(* lettura da X+[byte curpc] *)
+definition mode_IX1ADD_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map ?? (memory_filter_read m t s cur_pc)
+ (λb.opt_map ?? (get_IX m t s)
+ (λaddr.Some ? (tripleT ??? s (plus_w16nc addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
+
(* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
definition mode_IX1_write ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
(λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
+(* lettura da X+[word curpc] *)
+definition mode_IX2ADD_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map ?? (memory_filter_read m t s cur_pc)
+ (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
+ (λbl.opt_map ?? (get_IX m t s)
+ (λaddr.Some ? (tripleT ??? s (plus_w16nc addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
+
(* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
definition mode_IX2_write ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
| MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
(λindx.Some ? (tripleT ??? s indx cur_pc))
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
+
(* preleva 1 byte immediato *)
| MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
(* NO: solo lettura word *)
| MODE_IMM2 ⇒ None ?
(* preleva 1 byte da indirizzo diretto 1 byte *)
(* NO: solo lettura/scrittura byte *)
| MODE_INHH ⇒ None ?
+(* preleva 1 word immediato *)
+ | MODE_INHX0ADD ⇒ opt_map ?? (get_IX m t s)
+ (λw.Some ? (tripleT ??? s w cur_pc))
+(* preleva 1 word immediato *)
+ | MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
+(* preleva 1 word immediato *)
+ | MODE_INHX2ADD ⇒ mode_IX2ADD_load m t s cur_pc
+
(* NO: solo lettura byte *)
| MODE_IMM1 ⇒ None ?
+(* preleva 1 word immediato *)
+ | MODE_IMM1EXT ⇒ mode_IMM1EXT_load m t s cur_pc
(* preleva 1 word immediato *)
| MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
(* preleva 1 word da indirizzo diretto 1 byte *)
| MODE_INHH ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
(λtmps.Some ? (pair ?? tmps cur_pc))
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
+
(* NO: solo lettura byte *)
| MODE_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
(* NO: solo lettura word *)
| MODE_IMM2 ⇒ None ?
(* scrive 1 byte su indirizzo diretto 1 byte *)
(* NO: solo lettura/scrittura byte *)
| MODE_INHH ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
+
(* NO: solo lettura byte *)
| MODE_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
(* NO: solo lettura word *)
| MODE_IMM2 ⇒ None ?
(* scrive 1 word su indirizzo diretto 1 byte *)