]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 25be562)
New version of freescale:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Mar 2008 14:01:52 +0000 (14:01 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Mar 2008 14:01:52 +0000 (14:01 +0000)
 a) bug fixed for SBC, JUMP e JSR
 b) medium_tests theorems ported to new pattern syntax
 c) new test for a perfect number generator
 d) "lambda-delifting" of let rec reverted (waiting for a better
    implementation of simplify or for the new generation kernel)

16 files changed:
helm/software/matita/library/depends patch | blob | history
helm/software/matita/library/freescale/load_write.ma patch | blob | history
helm/software/matita/library/freescale/medium_tests.ma patch | blob | history
helm/software/matita/library/freescale/medium_tests_lemmas.ma patch | blob | history
helm/software/matita/library/freescale/medium_tests_tools.ma patch | blob | history
helm/software/matita/library/freescale/multivm.ma patch | blob | history
helm/software/matita/library/freescale/opcode.ma patch | blob | history
helm/software/matita/library/freescale/table_HC05.ma patch | blob | history
helm/software/matita/library/freescale/table_HC05_tests.ma patch | blob | history
helm/software/matita/library/freescale/table_HC08.ma patch | blob | history
helm/software/matita/library/freescale/table_HC08_tests.ma patch | blob | history
helm/software/matita/library/freescale/table_HCS08.ma patch | blob | history
helm/software/matita/library/freescale/table_HCS08_tests.ma patch | blob | history
helm/software/matita/library/freescale/table_RS08.ma patch | blob | history
helm/software/matita/library/freescale/table_RS08_tests.ma patch | blob | history
helm/software/matita/library/freescale/translation.ma patch | blob | history

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index 59977807b0191335cbb8625349eba8192389ed57..e02dc916f1c571a55f5c5364be8abfc9d9cd78e4 100644 (file)
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -1,116 +1,116 @@
-Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma
+list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
+list/list.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma
 Z/moebius.ma Z/sigma_p.ma nat/factorization.ma
-Z/times.ma Z/plus.ma nat/lt_arith.ma
-Z/orders.ma Z/z.ma logic/connectives.ma nat/orders.ma
-Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma
 Z/plus.ma Z/z.ma nat/minus.ma
 Z/compare.ma Z/orders.ma nat/compare.ma
-Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
+Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma
 Z/z.ma datatypes/bool.ma nat/nat.ma
-datatypes/constructors.ma logic/equality.ma
+Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma
+Z/orders.ma Z/z.ma logic/connectives.ma nat/orders.ma
+Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
+Z/times.ma Z/plus.ma nat/lt_arith.ma
+decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma
+decidable_kit/fgraph.ma decidable_kit/fintype.ma
+decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma
+decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma
+decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
+decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
+higher_order_defs/functions.ma logic/equality.ma
+higher_order_defs/ordering.ma logic/equality.ma
+higher_order_defs/relations.ma logic/connectives.ma
+Q/q.ma Z/compare.ma Z/plus.ma
+Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
+Fsub/part1a_inversion.ma Fsub/defn.ma
+Fsub/part1a.ma Fsub/defn.ma
+Fsub/defn.ma Fsub/util.ma
+Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma
 datatypes/compare.ma 
+datatypes/constructors.ma logic/equality.ma
 datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
-algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
+algebra/monoids.ma algebra/semigroups.ma
 algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma
 algebra/semigroups.ma higher_order_defs/functions.ma
-algebra/monoids.ma algebra/semigroups.ma
-algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma
-algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma
+algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
 algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma
+algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma
 algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma
-demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
-demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
-demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
-list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
-list/list.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma
+algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma
+logic/coimplication.ma logic/connectives.ma
 logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma
 logic/connectives.ma 
-logic/coimplication.ma logic/connectives.ma
 logic/connectives2.ma higher_order_defs/relations.ma
-nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
-nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
+freescale/memory_func.ma freescale/memory_struct.ma
+freescale/extra.ma datatypes/constructors.ma list/list.ma logic/connectives.ma nat/div_and_mod.ma nat/primes.ma
+freescale/status.ma freescale/memory_abs.ma
+freescale/memory_bits.ma freescale/memory_trees.ma
+freescale/load_write.ma freescale/model.ma
+freescale/micro_tests.ma freescale/multivm.ma
+freescale/byte8.ma freescale/exadecim.ma
+freescale/table_HCS08.ma freescale/opcode.ma
+freescale/multivm.ma freescale/load_write.ma
+freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma
+freescale/translation.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
+freescale/model.ma freescale/status.ma
+freescale/medium_tests.ma freescale/medium_tests_lemmas.ma
+freescale/table_RS08.ma freescale/opcode.ma
+freescale/table_HC05.ma freescale/opcode.ma
+freescale/opcode.ma freescale/aux_bases.ma
+freescale/table_HC08.ma freescale/opcode.ma
+freescale/memory_trees.ma freescale/memory_struct.ma
+freescale/aux_bases.ma freescale/word16.ma
+freescale/memory_struct.ma freescale/translation.ma
+freescale/exadecim.ma freescale/extra.ma
+freescale/medium_tests_tools.ma freescale/multivm.ma
+freescale/word16.ma freescale/byte8.ma
+freescale/medium_tests_lemmas.ma freescale/medium_tests_tools.ma
+freescale/table_HC05_tests.ma freescale/table_HC05.ma
+freescale/table_RS08_tests.ma freescale/table_RS08.ma
+freescale/table_HC08_tests.ma freescale/table_HC08.ma
+freescale/table_HCS08_tests.ma freescale/table_HCS08.ma
+technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma
+demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
+demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
+demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
+nat/plus.ma nat/nat.ma
+nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
+nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma
 nat/factorial2.ma nat/exp.ma nat/factorial.ma
-nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
+nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma
+nat/le_arith.ma nat/orders.ma nat/times.ma
+nat/chebyshev_thm.ma nat/neper.ma
 nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
-nat/minus.ma nat/compare.ma nat/le_arith.ma
-nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma
-nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
-nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
-nat/factorial.ma nat/le_arith.ma
-nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma
+nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
+nat/div_and_mod_diseq.ma nat/lt_arith.ma
+nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
+nat/gcd_properties1.ma nat/gcd.ma
 nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
-nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma
-nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
+nat/minus.ma nat/compare.ma nat/le_arith.ma
 nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
+nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma
+nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
 nat/minimization.ma nat/minus.ma
-nat/gcd.ma nat/lt_arith.ma nat/primes.ma
-nat/chebyshev_thm.ma nat/neper.ma
-nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
+nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma
 nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma
-nat/le_arith.ma nat/orders.ma nat/times.ma
-nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
-nat/times.ma nat/plus.ma
-nat/div_and_mod_diseq.ma nat/lt_arith.ma
 nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
-nat/gcd_properties1.ma nat/gcd.ma
-nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma
-nat/lt_arith.ma nat/div_and_mod.ma
-nat/bertrand.ma list/list.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma
-nat/factorization.ma nat/ord.ma
-nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma
-nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
+nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
 nat/nat.ma higher_order_defs/functions.ma
-nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma
-nat/map_iter_p.ma nat/count.ma nat/permutation.ma
-nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma
+nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma
 nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
-nat/plus.ma nat/nat.ma
+nat/gcd.ma nat/lt_arith.ma nat/primes.ma
+nat/o.ma nat/binomial.ma nat/sqrt.ma
+nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma
 nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma
-nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma
 nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
-nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
-nat/o.ma nat/binomial.ma nat/sqrt.ma
-Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
-Q/q.ma Z/compare.ma Z/plus.ma
-freescale/translation.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
-freescale/table_RS08_tests.ma freescale/table_RS08.ma
-freescale/table_HCS08.ma freescale/opcode.ma
-freescale/table_RS08.ma freescale/opcode.ma
-freescale/memory_trees.ma freescale/memory_struct.ma
-freescale/multivm.ma freescale/load_write.ma
-freescale/opcode.ma freescale/aux_bases.ma
-freescale/memory_func.ma freescale/memory_struct.ma
-freescale/micro_tests.ma freescale/multivm.ma
-freescale/exadecim.ma freescale/extra.ma
-freescale/table_HC08.ma freescale/opcode.ma
-freescale/table_HC05.ma freescale/opcode.ma
-freescale/memory_bits.ma freescale/memory_trees.ma
-freescale/word16.ma freescale/byte8.ma
-freescale/table_HC08_tests.ma freescale/table_HC08.ma
-freescale/table_HC05_tests.ma freescale/table_HC05.ma
-freescale/model.ma freescale/status.ma
-freescale/medium_tests.ma freescale/medium_tests_lemmas.ma
-freescale/medium_tests_tools.ma freescale/multivm.ma
-freescale/load_write.ma freescale/model.ma
-freescale/memory_struct.ma freescale/translation.ma
-freescale/table_HCS08_tests.ma freescale/table_HCS08.ma
-freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma
-freescale/extra.ma datatypes/constructors.ma list/list.ma logic/connectives.ma nat/div_and_mod.ma nat/primes.ma
-freescale/aux_bases.ma freescale/word16.ma
-freescale/medium_tests_lemmas.ma freescale/medium_tests_tools.ma
-freescale/status.ma freescale/memory_abs.ma
-freescale/byte8.ma freescale/exadecim.ma
-technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma
-Fsub/part1a.ma Fsub/defn.ma
-Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma
-Fsub/defn.ma Fsub/util.ma
-Fsub/part1a_inversion.ma Fsub/defn.ma
-decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma
-decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
-decidable_kit/fgraph.ma decidable_kit/fintype.ma
-decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma
-decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma
-decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
-higher_order_defs/relations.ma logic/connectives.ma
-higher_order_defs/functions.ma logic/equality.ma
-higher_order_defs/ordering.ma logic/equality.ma
+nat/bertrand.ma list/list.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma
+nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
+nat/factorial.ma nat/le_arith.ma
+nat/lt_arith.ma nat/div_and_mod.ma
+nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
+nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
+nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
+nat/factorization.ma nat/ord.ma
+nat/map_iter_p.ma nat/count.ma nat/permutation.ma
+nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
+nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma
+nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma
+nat/times.ma nat/plus.ma
diff --git a/helm/software/matita/library/freescale/load_write.ma b/helm/software/matita/library/freescale/load_write.ma
index a5fae5375e8f52197421f35ffddded2e7e5e6fdf..28c78b6bb74164d64c5efd582fef2dc09451c5c6 100644 (file)
--- a/helm/software/matita/library/freescale/load_write.ma
+++ b/helm/software/matita/library/freescale/load_write.ma
@@ -260,12 +260,10 @@ definition filtered_inc_w16 ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
  get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
 
-definition filtered_plus_w16 := \lambda m:mcu_type.
-let rec filtered_plus_w16  (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
+let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
  match n with
   [ O ⇒ w
-  | S n' ⇒ filtered_plus_w16 t s (filtered_inc_w16 m t s w) n' ]
-in filtered_plus_w16.
+  | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
 
 (* 
    errore1: non esiste traduzione ILL_OP
@@ -385,6 +383,12 @@ definition mode_IMM1_load ≝
  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.
@@ -460,6 +464,13 @@ definition mode_IX1_load ≝
   (λ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.
@@ -476,6 +487,14 @@ definition mode_IX2_load ≝
    (λ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.
@@ -548,8 +567,17 @@ definition multi_mode_load ≝
    | 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 *) 
@@ -617,8 +645,18 @@ definition multi_mode_load ≝
 (* 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 *) 
@@ -757,8 +795,17 @@ definition multi_mode_write ≝
   | 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 *)
@@ -834,8 +881,17 @@ definition multi_mode_write ≝
 (* 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 *) 
diff --git a/helm/software/matita/library/freescale/medium_tests.ma b/helm/software/matita/library/freescale/medium_tests.ma
index 20a0da441095905c70ae6a5942766170fc130a7f..90762c5fb3e45634921cd99ab44fed8814279523 100644 (file)
--- a/helm/software/matita/library/freescale/medium_tests.ma
+++ b/helm/software/matita/library/freescale/medium_tests.ma
@@ -43,20 +43,21 @@ let m ≝ HCS08 in source_to_byte8 m (
 
 (* [0x18C8]    allineamento *) (compile m ? NOP maINH I) @
 
-(* [0x18C9]       PSHX      *) (compile m ? PSHX maINH I) @
-(* [0x18CA]       PSHH      *) (compile m ? PSHH maINH I) @
-(* [0x18CB]       LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
-(* [0x18CE]       LDA ,X    *) (compile m ? LDA maIX0 I) @
-(* [0x18CF]       LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
-(* [0x18D2]       PSHA      *) (compile m ? PSHA maINH I) @
-(* [0x18D3]       LDA ,X    *) (compile m ? LDA maIX0 I) @
-(* [0x18D4]       LDHX 6,SP *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
-(* [0x18D7]       STA ,X    *) (compile m ? STA maIX0 I) @
-(* [0x18D8]       LDHX 2,SP *) (compile m ? LDHX (maSP1 〈x0,x2〉) I) @
-(* [0x18DB]       PULA      *) (compile m ? PULA maINH I) @
-(* [0x18DC]       STA ,X    *) (compile m ? STA maIX0 I) @
-(* [0x18DD]       AIS #2    *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
-(* [0x18DF]       RTS       *) (compile m ? RTS maINH I) @
+(* argomenti: HX e [0x0D49-A], passaggio ibrido reg, stack *)
+(* [0x18C9] PSHX      *) (compile m ? PSHX maINH I) @
+(* [0x18CA] PSHH      *) (compile m ? PSHH maINH I) @
+(* [0x18CB] LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
+(* [0x18CE] LDA ,X    *) (compile m ? LDA maIX0 I) @
+(* [0x18CF] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
+(* [0x18D2] PSHA      *) (compile m ? PSHA maINH I) @
+(* [0x18D3] LDA ,X    *) (compile m ? LDA maIX0 I) @
+(* [0x18D4] LDHX 6,SP *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
+(* [0x18D7] STA ,X    *) (compile m ? STA maIX0 I) @
+(* [0x18D8] LDHX 2,SP *) (compile m ? LDHX (maSP1 〈x0,x2〉) I) @
+(* [0x18DB] PULA      *) (compile m ? PULA maINH I) @
+(* [0x18DC] STA ,X    *) (compile m ? STA maIX0 I) @
+(* [0x18DD] AIS #2    *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
+(* [0x18DF] RTS       *) (compile m ? RTS maINH I) @
 
 (* void main(void)
    {
@@ -65,55 +66,56 @@ let m ≝ HCS08 in source_to_byte8 m (
    for(limit=3072;pos<(limit/2);pos++)
     { swap(&dati[pos],&dati[limit-pos-1]); } *)
 
-(* [0x18E0]       LDHX #LUNG      *) (compile m ? LDHX (maIMM2 elems) I) @
-(* [0x18E3]       STHX 4,SP       *) (compile m ? STHX (maSP1 〈x0,x4〉) I) @
-(* [0x18E6] 20 32 BRA *+52 ; 191A *) (compile m ? BRA (maIMM1 〈x3,x2〉) I) @
-(* [0x18E8]       TSX             *) (compile m ? TSX maINH I) @
-(* [0x18E9]       LDA 2,X         *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
-(* [0x18EB]       ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
-(* [0x18ED]       PSHA            *) (compile m ? PSHA maINH I) @
-(* [0x18EE]       LDA 1,X         *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
-(* [0x18F0]       ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
-(* [0x18F2]       PSHA            *) (compile m ? PSHA maINH I) @
-(* [0x18F3]       LDA 4,X         *) (compile m ? LDA (maIX1 〈x0,x4〉) I) @
-(* [0x18F5]       SUB 2,X         *) (compile m ? SUB (maIX1 〈x0,x2〉) I) @
-(* [0x18F7]       STA ,X          *) (compile m ? STA maIX0 I) @
-(* [0x18F8]       LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
-(* [0x18FA]       SBC 1,X         *) (compile m ? SBC (maIX1 〈x0,x1〉) I) @
-(* [0x18FC]       PSHA            *) (compile m ? PSHA maINH I) @
-(* [0x18FD]       LDX ,X          *) (compile m ? LDX maIX0 I) @
-(* [0x18FE]       PULH            *) (compile m ? PULH maINH I) @
-(* [0x18FF]       AIX #-1         *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
-(* [0x1901]       TXA             *) (compile m ? TXA maINH I) @
-(* [0x1902]       ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
-(* [0x1904]       PSHH            *) (compile m ? PSHH maINH I) @
-(* [0x1905]       TSX             *) (compile m ? TSX maINH I) @
-(* [0x1906]       STA 3,X         *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
-(* [0x1908]       PULA            *) (compile m ? PULA maINH I) @
-(* [0x1909]       ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
-(* [0x190B]       LDX 3,X         *) (compile m ? LDX (maIX1 〈x0,x3〉) I) @
-(* [0x190D]       PSHA            *) (compile m ? PSHA maINH I) @
-(* [0x190E]       PULH            *) (compile m ? PULH maINH I) @
-(* [0x190F] AD B8 BSR *-70 ; 18C9 *) (compile m ? BSR (maIMM1 〈xB,x8〉) I) @
-(* [0x1911]       AIS #2          *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
-(* [0x1913]       TSX             *) (compile m ? TSX maINH I) @
-(* [0x1914]       INC 2,X         *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
-(* [0x1916] 26 02 BNE *+4 ; 191A  *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
-(* [0x1918]       INC 1,X         *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
-(* [0x191A]       TSX             *) (compile m ? TSX maINH I) @
-(* [0x191B]       LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
-(* [0x191D]       PSHA            *) (compile m ? PSHA maINH I) @
-(* [0x191E]       PULH            *) (compile m ? PULH maINH I) @
-(* [0x191F]       LSRA            *) (compile m ? LSR maINHA I) @
-(* [0x1920]       TSX             *) (compile m ? TSX maINH I) @
-(* [0x1921]       LDX 4,X         *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
-(* [0x1923]       RORX            *) (compile m ? ROR maINHX I) @
-(* [0x1924]       PSHA            *) (compile m ? PSHA maINH I) @
-(* [0x1925]       PULH            *) (compile m ? PULH maINH I) @
-(* [0x1926]       CPHX 2,SP       *) (compile m ? CPHX (maSP1 〈x0,x2〉) I) @
-(* [0x1929] 22 BD BHI *-65 ; 18E8 *) (compile m ? BHI (maIMM1 〈xB,xD〉) I)
-
-(* [0x192B] attraverso simulazione in CodeWarrior si puo' enunciare che dopo
+(* [0x18E0] LDHX #elems     *) (compile m ? LDHX (maIMM2 elems) I) @
+(* [0x18E3] STHX 4,SP       *) (compile m ? STHX (maSP1 〈x0,x4〉) I) @
+(* [0x18E6] BRA *+52 ; 191A *) (compile m ? BRA (maIMM1 〈x3,x2〉) I) @
+(* [0x18E8] TSX             *) (compile m ? TSX maINH I) @
+(* [0x18E9] LDA 2,X         *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
+(* [0x18EB] ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
+(* [0x18ED] PSHA            *) (compile m ? PSHA maINH I) @
+(* [0x18EE] LDA 1,X         *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
+(* [0x18F0] ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
+(* [0x18F2] PSHA            *) (compile m ? PSHA maINH I) @
+(* [0x18F3] LDA 4,X         *) (compile m ? LDA (maIX1 〈x0,x4〉) I) @
+(* [0x18F5] SUB 2,X         *) (compile m ? SUB (maIX1 〈x0,x2〉) I) @
+(* [0x18F7] STA ,X          *) (compile m ? STA maIX0 I) @
+(* [0x18F8] LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
+(* [0x18FA] SBC 1,X         *) (compile m ? SBC (maIX1 〈x0,x1〉) I) @
+(* [0x18FC] PSHA            *) (compile m ? PSHA maINH I) @
+(* [0x18FD] LDX ,X          *) (compile m ? LDX maIX0 I) @
+(* [0x18FE] PULH            *) (compile m ? PULH maINH I) @
+(* [0x18FF] AIX #-1         *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
+(* [0x1901] TXA             *) (compile m ? TXA maINH I) @
+(* [0x1902] ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
+(* [0x1904] PSHH            *) (compile m ? PSHH maINH I) @
+(* [0x1905] TSX             *) (compile m ? TSX maINH I) @
+(* [0x1906] STA 3,X         *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
+(* [0x1908] PULA            *) (compile m ? PULA maINH I) @
+(* [0x1909] ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
+(* [0x190B] LDX 3,X         *) (compile m ? LDX (maIX1 〈x0,x3〉) I) @
+(* [0x190D] PSHA            *) (compile m ? PSHA maINH I) @
+(* [0x190E] PULH            *) (compile m ? PULH maINH I) @
+(* [0x190F] BSR *-70 ; 18C9 *) (compile m ? BSR (maIMM1 〈xB,x8〉) I) @
+(* [0x1911] AIS #2          *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
+(* [0x1913] TSX             *) (compile m ? TSX maINH I) @
+(* [0x1914] INC 2,X         *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
+(* [0x1916] BNE *+4 ; 191A  *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
+(* [0x1918] INC 1,X         *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
+(* [0x191A] TSX             *) (compile m ? TSX maINH I) @
+(* [0x191B] LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
+(* [0x191D] PSHA            *) (compile m ? PSHA maINH I) @
+(* [0x191E] PULH            *) (compile m ? PULH maINH I) @
+(* [0x191F] LSRA            *) (compile m ? LSR maINHA I) @
+(* [0x1920] TSX             *) (compile m ? TSX maINH I) @
+(* [0x1921] LDX 4,X         *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
+(* [0x1923] RORX            *) (compile m ? ROR maINHX I) @
+(* [0x1924] PSHA            *) (compile m ? PSHA maINH I) @
+(* [0x1925] PULH            *) (compile m ? PULH maINH I) @
+(* [0x1926] CPHX 2,SP       *) (compile m ? CPHX (maSP1 〈x0,x2〉) I) @
+(* [0x1929] BHI *-65 ; 18E8 *) (compile m ? BHI (maIMM1 〈xB,xD〉) I)
+
+(* [0x192B] !FINE!
+            attraverso simulazione in CodeWarrior si puo' enunciare che dopo
             42+79*n+5*(n>>9) ci sara' il reverse di n byte (PARI) e
             H:X=n/2 *)
  ).
@@ -121,10 +123,12 @@ let m ≝ HCS08 in source_to_byte8 m (
 (* creazione del processore+caricamento+impostazione registri *)
 definition dTest_HCS08_sReverse_status ≝
 λt:memory_impl.
+λA_op:byte8.
 λHX_op:word16.
 λelems:word16.
 λdata:list byte8.
- set_z_flag HCS08 t (* Z<-true *)
+ set_acc_8_low_reg HCS08 t (* A<-A_op *)
+ (set_z_flag HCS08 t (* Z<-true *)
   (setweak_sp_reg HCS08 t (* SP<-0x0D4A *)
    (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
     (set_pc_reg HCS08 t (* PC<-0x18E0 *)
@@ -140,7 +144,8 @@ definition dTest_HCS08_sReverse_status ≝
      (mk_word16 (mk_byte8 x1 x8) (mk_byte8 xE x0)))
     HX_op)
    (mk_word16 (mk_byte8 x0 xD) (mk_byte8 x4 xA)))
-  true.
+  true)
+ A_op.
 
 (* parametrizzazione dell'enunciato del teorema *)
 (* primo sbozzo: confronto esecuzione con hexdump... *)
@@ -153,7 +158,7 @@ lemma dTest_HCS08_sReverse_dump_aux ≝
  (* 3) match di esecuzione su tempo in forma di tempo esatto *)
  (match execute HCS08 t
   (* parametri IN: t,H:X,strlen(string),string *)
-  (TickOK ? (dTest_HCS08_sReverse_status t 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
+  (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
   (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) with
    [ TickERR s _ ⇒ None ?
@@ -185,7 +190,7 @@ lemma dTest_HCS08_sReverse_aux ≝
  (* 3) match di esecuzione su tempo in forma di tempo esatto *)
  (match execute HCS08 t
   (* parametri IN: t,H:X,strlen(string),string *)
-  (TickOK ? (dTest_HCS08_sReverse_status t 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
+  (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
   (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) with
    [ TickERR s _ ⇒ None ?
@@ -194,7 +199,7 @@ lemma dTest_HCS08_sReverse_aux ≝
    | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
    ] =
   Some ? (set_pc_reg HCS08 t
-   (dTest_HCS08_sReverse_status t (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string)) 
+   (dTest_HCS08_sReverse_status t (fst ?? (shr_b8 (w16h (byte8_strlen string)))) (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string)) 
    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
 
 (*
@@ -228,7 +233,7 @@ qed.
 definition sReverseCalc ≝
 λstring:list byte8.
  match execute HCS08 MEM_TREE
-  (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
+  (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
   (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) with
    [ TickERR s _ ⇒ None ?
    | TickSUSP s _ ⇒ None ? 
@@ -238,7 +243,9 @@ definition sReverseCalc ≝
 definition sReverseNoCalc ≝
 λstring:list byte8.
  Some ? (set_pc_reg HCS08 MEM_TREE
-   (dTest_HCS08_sReverse_status MEM_TREE (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string)) 
+   (dTest_HCS08_sReverse_status MEM_TREE (fst ?? (shr_b8 (w16h (byte8_strlen string))))
+                                         (fst ?? (shr_w16 (byte8_strlen string)))
+                                         (byte8_strlen string) (byte8_reverse string)) 
    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))).
 
 definition sReverseCalc32   ≝ sReverseCalc dTest_random_32.
@@ -259,12 +266,6 @@ definition sReverseNoCalc1024 ≝ sReverseNoCalc dTest_random_1024.
 definition sReverseNoCalc2048 ≝ sReverseNoCalc dTest_random_2048.
 definition sReverseNoCalc3072 ≝ sReverseNoCalc dTest_random_3072.
 
-(*
-lemma ver : sReverseCalc128 = sReverseNoCalc128.
- reflexivity.
-qed.
-*)
-
 (* *********************** *)
 (* HCS08GB60 Counting Sort *)
 (* *********************** *)
@@ -289,29 +290,29 @@ let m ≝ HCS08 in source_to_byte8 m (
     for(;index<3072;index++)
      { counters[dati[index]]++; } *)
 
-(* [0x18C8] 20 1D       BRA *+31;18E7 [3] *) (compile m ? BRA (maIMM1 〈x1,xD〉) I) @
-(* [0x18CA] 9E FE 01    LDHX 1,SP     [5] *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
-(* [0x18CD] D6 01 00    LDA 256,X     [4] *) (compile m ? LDA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
-(* [0x18D0] 48          LSLA          [1] *) (compile m ? ASL maINHA I) @
-(* [0x18D1] 5F          CLRX          [1] *) (compile m ? CLR maINHX I) @
-(* [0x18D2] 59          ROLX          [1] *) (compile m ? ROL maINHX I) @
-(* [0x18D3] AB 00       ADD #0x00     [2] *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
-(* [0x18D5] 87          PSHA          [2] *) (compile m ? PSHA maINH I) @
-(* [0x18D6] 9F          TXA           [1] *) (compile m ? TXA maINH I) @
-(* [0x18D7] A9 0D       ADC #0x0D     [2] *) (compile m ? ADC (maIMM1 〈x0,xD〉) I) @
-(* [0x18D9] 87          PSHA          [2] *) (compile m ? PSHA maINH I) @
-(* [0x18DA] 8A          PULH          [3] *) (compile m ? PULH maINH I) @
-(* [0x18DB] 88          PULX          [3] *) (compile m ? PULX maINH I) @
-(* [0x18DC] 6C 01       INC 1,X       [5] *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
-(* [0x18DE] 26 01       BNE *+3       [3] *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
-(* [0x18E0] 7C          INC ,X        [4] *) (compile m ? INC maIX0 I) @
-(* [0x18E1] 95          TSX           [2] *) (compile m ? TSX maINH I) @
-(* [0x18E2] 6C 01       INC 1,X       [5] *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
-(* [0x18E4] 26 01       BNE *+3       [3] *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
-(* [0x18E6] 7C          INC ,X        [4] *) (compile m ? INC maIX0 I) @
-(* [0x18E7] 9E FE 01    LDHX 1,SP     [5] *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
-(* [0x18EA] 65 0C 00    CPHX #0x0C00  [3] *) (compile m ? CPHX (maIMM2 elems) I) @ (* dimensione dei dati al massimo 0x0C00 *)
-(* [0x18ED] 25 DB       BCS *-35;18CA [3] *) (compile m ? BCS (maIMM1 〈xD,xB〉) I) @
+(* [0x18C8] BRA *+31;18E7 *) (compile m ? BRA (maIMM1 〈x1,xD〉) I) @
+(* [0x18CA] LDHX 1,SP     *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
+(* [0x18CD] LDA 256,X     *) (compile m ? LDA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
+(* [0x18D0] LSLA          *) (compile m ? ASL maINHA I) @
+(* [0x18D1] CLRX          *) (compile m ? CLR maINHX I) @
+(* [0x18D2] ROLX          *) (compile m ? ROL maINHX I) @
+(* [0x18D3] ADD #0x00     *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
+(* [0x18D5] PSHA          *) (compile m ? PSHA maINH I) @
+(* [0x18D6] TXA           *) (compile m ? TXA maINH I) @
+(* [0x18D7] ADC #0x0D     *) (compile m ? ADC (maIMM1 〈x0,xD〉) I) @
+(* [0x18D9] PSHA          *) (compile m ? PSHA maINH I) @
+(* [0x18DA] PULH          *) (compile m ? PULH maINH I) @
+(* [0x18DB] PULX          *) (compile m ? PULX maINH I) @
+(* [0x18DC] INC 1,X       *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
+(* [0x18DE] BNE *+3       *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
+(* [0x18E0] INC ,X        *) (compile m ? INC maIX0 I) @
+(* [0x18E1] TSX           *) (compile m ? TSX maINH I) @
+(* [0x18E2] INC 1,X       *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
+(* [0x18E4] BNE *+3       *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
+(* [0x18E6] INC ,X        *) (compile m ? INC maIX0 I) @
+(* [0x18E7] LDHX 1,SP     *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
+(* [0x18EA] CPHX #elems   *) (compile m ? CPHX (maIMM2 elems) I) @ (* dimensione dei dati al massimo 0x0C00 *)
+(* [0x18ED] BCS *-35;18CA *) (compile m ? BCS (maIMM1 〈xD,xB〉) I) @
 
 (* /* sovrascrittura di dati per produrre la versione ordinata */
    for(index=0;index<256;index++)
@@ -320,52 +321,53 @@ let m ≝ HCS08 in source_to_byte8 m (
      { dati[position++]=index; }
     } *)
 
-(* [0x18EF] 95          TSX          *) (compile m ? TSX maINH I) @
-(* [0x18F0] 6F 01       CLR 1,X      *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
-(* [0x18F2] 7F          CLR ,X       *) (compile m ? CLR maIX0 I) @
-(* [0x18F3] 20 0E       BRA *+16     *) (compile m ? BRA (maIMM1 〈x0,xE〉) I) @
-(* [0x18F5] 95          TSX          *) (compile m ? TSX maINH I) @
-(* [0x18F6] E6 01       LDA 1,X      *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
-(* [0x18F8] 9E FE 03    LDHX 3,SP    *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
-(* [0x18FB] D7 01 00    STA 256,X    *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
-(* [0x18FE] AF 01       AIX #1       *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
-(* [0x1900] 9E FF 03    STHX 3,SP    *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
-(* [0x1903] 95          TSX          *) (compile m ? TSX maINH I) @
-(* [0x1904] EE 01       LDX 1,X      *) (compile m ? LDX (maIX1 〈x0,x1〉) I) @
-(* [0x1906] 58          LSLX         *) (compile m ? ASL maINHX I) @
-(* [0x1907] 9E E6 01    LDA 1,SP     *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
-(* [0x190A] 49          ROLA         *) (compile m ? ROL maINHA I) @
-(* [0x190B] 87          PSHA         *) (compile m ? PSHA maINH I) @
-(* [0x190C] 8A          PULH         *) (compile m ? PULH maINH I) @
-(* [0x190D] 89          PSHX         *) (compile m ? PSHX maINH I) @
-(* [0x190E] 9E BE 0D 00 LDHX 3328,X  *) (compile m ? LDHX (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
-(* [0x1912] 89          PSHX         *) (compile m ? PSHX maINH I) @
-(* [0x1913] 8B          PSHH         *) (compile m ? PSHH maINH I) @
-(* [0x1914] AF FF       AIX #-1      *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
-(* [0x1916] 8B          PSHH         *) (compile m ? PSHH maINH I) @
-(* [0x1917] 87          PSHA         *) (compile m ? PSHA maINH I) @
-(* [0x1918] 8A          PULH         *) (compile m ? PULH maINH I) @
-(* [0x1919] 89          PSHX         *) (compile m ? PSHX maINH I) @
-(* [0x191A] 9E EE 05    LDX 5,SP     *) (compile m ? LDX (maSP1 〈x0,x5〉) I) @
-(* [0x191D] 86          PULA         *) (compile m ? PULA maINH I) @
-(* [0x191E] D7 0D 01    STA 3329,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x1〉〉) I) @
-(* [0x1921] 86          PULA         *) (compile m ? PULA maINH I) @
-(* [0x1922] D7 0D 00    STA 3328,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
-(* [0x1925] 8A          PULH         *) (compile m ? PULH maINH I) @
-(* [0x1926] 88          PULX         *) (compile m ? PULX maINH I) @
-(* [0x1927] 65 00 00    CPHX #0x0000 *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
-(* [0x192A] 8A          PULH         *) (compile m ? PULH maINH I) @
-(* [0x192B] 26 C8       BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
-(* [0x192D] 95          TSX          *) (compile m ? TSX maINH I) @
-(* [0x192E] 6C 01       INC 1,X      *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
-(* [0x1930] 26 01       BNE *+3      *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
-(* [0x1932] 7C          INC ,X       *) (compile m ? INC maIX0 I) @
-(* [0x1933] 9E FE 01    LDHX 1,SP    *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
-(* [0x1936] 65 01 00    CPHX #0x0100 *) (compile m ? CPHX (maIMM2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
-(* [0x1939] 25 C8       BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
-(* [0x193B] 8E                       *) (compile m ? STOP maINH I)
-
-(* [0x193C] attraverso simulazione in CodeWarrior si puo' enunciare che dopo
+(* [0x18EF] TSX          *) (compile m ? TSX maINH I) @
+(* [0x18F0] CLR 1,X      *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
+(* [0x18F2] CLR ,X       *) (compile m ? CLR maIX0 I) @
+(* [0x18F3] BRA *+16     *) (compile m ? BRA (maIMM1 〈x0,xE〉) I) @
+(* [0x18F5] TSX          *) (compile m ? TSX maINH I) @
+(* [0x18F6] LDA 1,X      *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
+(* [0x18F8] LDHX 3,SP    *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
+(* [0x18FB] STA 256,X    *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
+(* [0x18FE] AIX #1       *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
+(* [0x1900] STHX 3,SP    *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
+(* [0x1903] TSX          *) (compile m ? TSX maINH I) @
+(* [0x1904] LDX 1,X      *) (compile m ? LDX (maIX1 〈x0,x1〉) I) @
+(* [0x1906] LSLX         *) (compile m ? ASL maINHX I) @
+(* [0x1907] LDA 1,SP     *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
+(* [0x190A] ROLA         *) (compile m ? ROL maINHA I) @
+(* [0x190B] PSHA         *) (compile m ? PSHA maINH I) @
+(* [0x190C] PULH         *) (compile m ? PULH maINH I) @
+(* [0x190D] PSHX         *) (compile m ? PSHX maINH I) @
+(* [0x190E] LDHX 3328,X  *) (compile m ? LDHX (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
+(* [0x1912] PSHX         *) (compile m ? PSHX maINH I) @
+(* [0x1913] PSHH         *) (compile m ? PSHH maINH I) @
+(* [0x1914] AIX #-1      *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
+(* [0x1916] PSHH         *) (compile m ? PSHH maINH I) @
+(* [0x1917] PSHA         *) (compile m ? PSHA maINH I) @
+(* [0x1918] PULH         *) (compile m ? PULH maINH I) @
+(* [0x1919] PSHX         *) (compile m ? PSHX maINH I) @
+(* [0x191A] LDX 5,SP     *) (compile m ? LDX (maSP1 〈x0,x5〉) I) @
+(* [0x191D] PULA         *) (compile m ? PULA maINH I) @
+(* [0x191E] STA 3329,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x1〉〉) I) @
+(* [0x1921] PULA         *) (compile m ? PULA maINH I) @
+(* [0x1922] STA 3328,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
+(* [0x1925] PULH         *) (compile m ? PULH maINH I) @
+(* [0x1926] PULX         *) (compile m ? PULX maINH I) @
+(* [0x1927] CPHX #0x0000 *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
+(* [0x192A] PULH         *) (compile m ? PULH maINH I) @
+(* [0x192B] BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
+(* [0x192D] TSX          *) (compile m ? TSX maINH I) @
+(* [0x192E] INC 1,X      *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
+(* [0x1930] BNE *+3      *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
+(* [0x1932] INC ,X       *) (compile m ? INC maIX0 I) @
+(* [0x1933] LDHX 1,SP    *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
+(* [0x1936] CPHX #0x0100 *) (compile m ? CPHX (maIMM2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
+(* [0x1939] BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
+(* [0x193B] STOP         *) (compile m ? STOP maINH I)
+
+(* [0x193C] !FINE!
+            attraverso simulazione in CodeWarrior si puo' enunciare che dopo
             25700+150n si sara' entrati in stato STOP corrispondente con ordinamento
             di n byte, A=0xFF H:X=0x0100 *)
  ).
@@ -373,29 +375,32 @@ let m ≝ HCS08 in source_to_byte8 m (
 (* creazione del processore+caricamento+impostazione registri *)
 definition dTest_HCS08_cSort_status ≝
 λt:memory_impl.
+λI_op:bool.
 λA_op:byte8.
 λHX_op:word16.
 λelems:word16.
 λdata:list byte8.
- set_acc_8_low_reg HCS08 t (* A<-A_op *)
-  (set_z_flag HCS08 t (* Z<-true *)
-   (setweak_sp_reg HCS08 t (* SP<-0x0F4B *)
-    (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
-     (set_pc_reg HCS08 t (* PC<-dTest_HCS08_prog *)
-      (start_of_mcu_version
-       MC9S08GB60 t
-       (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
-        (load_from_source_at t (zero_memory t) (* carica source in ROM:dTest_HCS08_prog *)
-          (dTest_HCS08_cSort_source elems) dTest_HCS08_prog)
-         data dTest_HCS08_RAM)
-       (build_memory_type_of_mcu_version MC9S08GB60 t)
-       (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
-       false false false false false false) (* non deterministici tutti a 0 *)
-      dTest_HCS08_prog)
-     HX_op)
-    (mk_word16 (mk_byte8 x0 xF) (mk_byte8 x4 xB)))
-   true)
-  A_op.
+ setweak_i_flag HCS08 t (* I<-I_op *)
+  (set_acc_8_low_reg HCS08 t (* A<-A_op *)
+   (set_z_flag HCS08 t (* Z<-true *)
+    (setweak_sp_reg HCS08 t (* SP<-0x0F4B *)
+     (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
+      (set_pc_reg HCS08 t (* PC<-dTest_HCS08_prog *)
+       (start_of_mcu_version
+        MC9S08GB60 t
+        (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
+         (load_from_source_at t (zero_memory t) (* carica source in ROM:dTest_HCS08_prog *)
+           (dTest_HCS08_cSort_source elems) dTest_HCS08_prog)
+          data dTest_HCS08_RAM)
+        (build_memory_type_of_mcu_version MC9S08GB60 t)
+        (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
+        false false false false false false) (* non deterministici tutti a 0 *)
+       dTest_HCS08_prog)
+      HX_op)
+     (mk_word16 (mk_byte8 x0 xF) (mk_byte8 x4 xB)))
+    true)
+   A_op)
+  I_op.
 
 (* parametrizzazione dell'enunciato del teorema parziale *)
 lemma dTest_HCS08_cSort_aux ≝
@@ -405,7 +410,7 @@ lemma dTest_HCS08_cSort_aux ≝
  (* 2) match di esecuzione su tempo in forma di upperbound *)
  (match execute HCS08 t
   (* parametri IN: t,A,H:X,strlen(string),string *)
-  (TickOK ? (dTest_HCS08_cSort_status t 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
+  (TickOK ? (dTest_HCS08_cSort_status t true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 25700+150*n *)
   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
    [ TickERR s _ ⇒ None ?
@@ -414,7 +419,7 @@ lemma dTest_HCS08_cSort_aux ≝
    | TickOK s ⇒ None ?
    ] =
   Some ? (set_pc_reg HCS08 t
-   (dTest_HCS08_cSort_status t 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string)) 
+   (dTest_HCS08_cSort_status t false 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string)) 
    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC)))).
 
 (* dimostrazione senza svolgimento degli stati *)
@@ -431,7 +436,7 @@ qed.
 definition cSortCalc ≝
 λstring:list byte8.
  match execute HCS08 MEM_TREE
-  (TickOK ? (dTest_HCS08_cSort_status MEM_TREE 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
+  (TickOK ? (dTest_HCS08_cSort_status MEM_TREE true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
    [ TickERR s _ ⇒ None ?
    | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
@@ -441,7 +446,7 @@ definition cSortCalc ≝
 definition cSortNoCalc ≝
 λstring:list byte8.
  Some ? (set_pc_reg HCS08 MEM_TREE
-   (dTest_HCS08_cSort_status MEM_TREE 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string)) 
+   (dTest_HCS08_cSort_status MEM_TREE false 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string)) 
    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC))).
 
 definition cSortCalc32   ≝ cSortCalc dTest_random_32.
@@ -462,8 +467,424 @@ definition cSortNoCalc1024 ≝ cSortNoCalc dTest_random_1024.
 definition cSortNoCalc2048 ≝ cSortNoCalc dTest_random_2048.
 definition cSortNoCalc3072 ≝ cSortNoCalc dTest_random_3072.
 
+(* ********************** *)
+(* HCS08GB60 numeri aurei *)
+(* ********************** *)
+
+(* versione ridotta, in cui non si riazzerano gli elementi di counters *)
+definition dTest_HCS08_gNum_source : word16 → (list byte8) ≝
+λelems:word16.
+let m ≝ HCS08 in source_to_byte8 m (
+(* BEFORE: A=0x00 HX=0x1A00 PC=0x18BE SP=0x016F Z=1 (I=1) *)
+
 (*
-lemma ver : cSortCalc32 = cSortNoCalc32.
- reflexivity.
-qed.
+static unsigned int result[16]={ 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0 };
+word result[16] = 0x0100
+
+void goldenNumbers(void)
+{
+unsigned int res_pos=0,tested_num=0,divisor=0;
+unsigned long int acc=0;
+*)
+
+(* [0x18BE] AIS #-10   *) (compile m ? AIS (maIMM1 〈xF,x6〉) I) @
+(* [0x18C0] TSX        *) (compile m ? TSX maINH I) @
+(* [0x18C1] CLR 9,x    *) (compile m ? CLR (maIX1 〈x0,x9〉) I) @
+(* [0x18C3] CLR 8,X    *) (compile m ? CLR (maIX1 〈x0,x8〉) I) @
+(* [0x18C5] CLR 1,X    *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
+(* [0x18C7] CLR ,X     *) (compile m ? CLR maIX0 I) @
+(* [0x18C8] CLR 3,X    *) (compile m ? CLR (maIX1 〈x0,x3〉) I) @
+(* [0x18CA] CLR 2,X    *) (compile m ? CLR (maIX1 〈x0,x2〉) I) @
+(* [0x18CC] JSR 0x1951 *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x5,x1〉〉) I) @
+
+(*
+for(tested_num=1;tested_num<2;tested_num++)
+ {
 *)
+
+(* [0x18CF] STHX 1,SP          *) (compile m ? STHX (maSP1 〈x0,x1〉) I) @
+(* [0x18D2] BRA *+116 ; 0x1946 *) (compile m ? BRA (maIMM1 〈x7,x2〉) I) @
+(* [0x18D4] BSR *+125 ; 0x1951 *) (compile m ? BSR (maIMM1 〈x7,xB〉) I) @
+(* [0x18D6] STHX 3,SP          *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
+
+(*
+ for(acc=0,divisor=1;divisor<tested_num;divisor++)
+  {
+  if(!(tested_num%divisor))
+   { acc+=divisor; }
+  }
+*)
+
+(* [0x18D9] BRA *+61 ; 0x1916 *) (compile m ? BRA (maIMM1 〈x3,xB〉) I) @
+(* [0x18DB] LDHX 1,SP         *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
+(* [0x18DE] PSHX              *) (compile m ? PSHX maINH I) @
+(* [0x18DF] PSHH              *) (compile m ? PSHH maINH I) @
+(* [0x18E0] LDHX 5,SP         *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
+(* [0x18E3] JSR 0x1A1A        *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x1,xA〉〉) I) @
+(* [0x18E6] AIS #2            *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
+(* [0x18E8] CPHX #0x0000      *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
+(* [0x18EB] BNE *+33 ; 0x190C *) (compile m ? BNE (maIMM1 〈x1,xF〉) I) @
+(* [0x18ED] TSX               *) (compile m ? TSX maINH I) @
+(* [0x18EE] LDA 3,X           *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
+(* [0x18F0] LDX 2,X           *) (compile m ? LDX (maIX1 〈x0,x2〉) I) @
+(* [0x18F2] PSHA              *) (compile m ? PSHA maINH I) @
+(* [0x18F3] PSHX              *) (compile m ? PSHX maINH I) @
+(* [0x18F4] CLRA              *) (compile m ? CLR maINHA I) @
+(* [0x18F5] PSHA              *) (compile m ? PSHA maINH I) @
+(* [0x18F6] PSHA              *) (compile m ? PSHA maINH I) @
+(* [0x18F7] TSX               *) (compile m ? TSX maINH I) @
+(* [0x18F8] PSHX              *) (compile m ? PSHX maINH I) @
+(* [0x19F9] PSHH              *) (compile m ? PSHH maINH I) @
+(* [0x18FA] AIX #8            *) (compile m ? AIX (maIMM1 〈x0,x8〉) I) @
+(* [0x18FC] PSHX              *) (compile m ? PSHX maINH I) @
+(* [0x18FD] PSHH              *) (compile m ? PSHH maINH I) @
+(* [0x18FE] LDHX 3,SP         *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
+(* [0x1901] JSR 0x1A2A        *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x2,xA〉〉) I) @
+(* [0x1904] TSX               *) (compile m ? TSX maINH I) @
+(* [0x1905] AIX #14           *) (compile m ? AIX (maIMM1 〈x0,xE〉) I) @
+(* [0x1907] JSR 0x1A30        *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x3,x0〉〉) I) @
+(* [0x190A] AIS #6            *) (compile m ? AIS (maIMM1 〈x0,x6〉) I) @
+(* [0x190C] STA 0x1800  !COP! *) (compile m ? STA (maDIR2 〈〈x0,xC〉:〈x0,x0〉〉) I) @
+(* [0x190F] TSX               *) (compile m ? TSX maINH I) @
+(* [0x1910] INC 3,X           *) (compile m ? INC (maIX1 〈x0,x3〉) I) @
+(* [0x1912] BNE *+4 ; 0x1916  *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
+(* [0x1914] INC 2,X           *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
+(* [0x1916] LDHX 1,SP         *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
+(* [0x1919] CPHX 3,SP         *) (compile m ? CPHX (maSP1 〈x0,x3〉) I) @
+(* [0x191C] BHI *-65 ; 0x18DB *) (compile m ? BHI (maIMM1 〈xB,xD〉) I) @
+
+(*
+ if(acc==tested_num)
+  { result[res_pos++]=tested_num; }
+ }
+}
+*)
+
+(* [0x191E] CPHX 7,SP          *) (compile m ? CPHX (maSP1 〈x0,x7〉) I) @
+(* [0x1921] BNE *+31 ; 0x1940  *) (compile m ? BNE (maIMM1 〈x1,xD〉) I) @
+(* [0x1923] LDHX 5,SP          *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
+(* [0x1926] BNE *+26 ; 0x1940  *) (compile m ? BNE (maIMM1 〈x1,x8〉) I) @
+(* [0x1928] LDHX 9,SP          *) (compile m ? LDHX (maSP1 〈x0,x9〉) I) @
+(* [0x192B] PSHX               *) (compile m ? PSHX maINH I) @
+(* [0x192C] AIX #1             *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
+(* [0x192E] STHX 10,SP         *) (compile m ? STHX (maSP1 〈x0,xA〉) I) @
+(* [0x1931] PULX               *) (compile m ? PULX maINH I) @
+(* [0x1932] LSLX               *) (compile m ? ASL maINHX I) @
+(* [0x1933] LDA 2,SP           *) (compile m ? LDA (maSP1 〈x0,x2〉) I) @
+(* [0x1936] CLRH               *) (compile m ? CLR maINHH I) @
+(* [0x1937] STA 257,X          *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x1〉〉) I) @
+(* [0x193A] LDA 1,SP           *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
+(* [0x193D] STA 256,X          *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
+(* [0x1940] TSX                *) (compile m ? TSX maINH I) @
+(* [0x1941] INC 1,X            *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
+(* [0x1943] BNE *+3 ; 0x1946   *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
+(* [0x1945] INC ,X             *) (compile m ? INC maIX0 I) @
+(* [0x1946] LDHX 1,SP          *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
+(* [0x1949] CPHX #elems        *) (compile m ? CPHX (maIMM2 elems) I) @
+(* [0x194C] BCS *-120 ; 0x18D4 *) (compile m ? BCS (maIMM1 〈x8,x6〉) I) @
+(* [0x194E] AIS #10            *) (compile m ? AIS (maIMM1 〈x0,xA〉) I) @
+(* [0x1950] STOP ->1951 !FINE! *) (compile m ? STOP maINH I) @
+(* [0x1951] CLRX               *) (compile m ? CLR maINHX I) @
+(* [0x1952] CLRH               *) (compile m ? CLR maINHH I) @
+(* [0x1953] STHX 9,SP          *) (compile m ? STHX (maSP1 〈x0,x9〉) I) @
+(* [0x1956] CLRH               *) (compile m ? CLR maINHH I) @
+(* [0x1957] STHX 7,SP          *) (compile m ? STHX (maSP1 〈x0,x7〉) I) @
+(* [0x195A] INCX               *) (compile m ? INC maINHX I) @
+(* [0x195B] RTS                *) (compile m ? RTS maINH I) @
+
+(*
+static void _PUSH_ARGS_L(void) { ... }
+*)
+
+(* [0x195C] LDA 3,X    *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
+(* [0x195E] PSHA       *) (compile m ? PSHA maINH I) @
+(* [0x195F] LDA 2,X    *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
+(* [0x1961] PSHA       *) (compile m ? PSHA maINH I) @
+(* [0x1962] LDHX ,X    *) (compile m ? LDHX maIX0 I) @
+(* [0x1964] PSHX       *) (compile m ? PSHX maINH I) @
+(* [0x1965] PSHH       *) (compile m ? PSHH maINH I) @
+(* [0x1966] LDHX 7,SP  *) (compile m ? LDHX (maSP1 〈x0,x7〉) I) @
+(* [0x1969] LDA 3,X    *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
+(* [0x196B] STA 17,SP  *) (compile m ? STA (maSP1 〈x1,x1〉) I) @
+(* [0x196E] LDA 2,X    *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
+(* [0x1970] STA 16,SP  *) (compile m ? STA (maSP1 〈x1,x0〉) I) @
+(* [0x1973] LDHX ,X    *) (compile m ? LDHX maIX0 I) @
+(* [0x1975] STHX 14,SP *) (compile m ? STHX (maSP1 〈x0,xE〉) I) @
+(* [0x1978] LDHX 5,SP  *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
+(* [0x197B] JMP ,X     *) (compile m ? JMP maINHX0ADD I) @
+
+(*
+static void _ENTER_BINARY_L(void) { ... }
+*)
+
+(* [0x197C] PSHA       *) (compile m ? PSHA maINH I) @
+(* [0x197D] PSHX       *) (compile m ? PSHX maINH I) @
+(* [0x197E] PSHH       *) (compile m ? PSHH maINH I) @
+(* [0x197F] PSHX       *) (compile m ? PSHX maINH I) @
+(* [0x1980] PSHH       *) (compile m ? PSHH maINH I) @
+(* [0x1981] LDHX 6,SP  *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
+(* [0x1984] PSHX       *) (compile m ? PSHX maINH I) @
+(* [0x1985] PSHH       *) (compile m ? PSHH maINH I) @
+(* [0x1986] LDHX 10,SP *) (compile m ? LDHX (maSP1 〈x0,xA〉) I) @
+(* [0x1989] STHX 8,SP  *) (compile m ? STHX (maSP1 〈x0,x8〉) I) @
+(* [0x198C] LDHX 12,SP *) (compile m ? LDHX (maSP1 〈x0,xC〉) I) @
+(* [0x198F] JMP 0x195C *) (compile m ? JMP (maIMM2 〈〈x1,x9〉:〈x5,xC〉〉) I) @
+
+(*
+static void _IDIVMOD (char dummy_sgn, int j, int dummy, int i, ...) { ... }
+*)
+
+(* [0x1992] TST 4,SP            *) (compile m ? TST (maSP1 〈x0,x4〉) I) @
+(* [0x1995] BNE *+28 ; 0x19B1   *) (compile m ? BNE (maIMM1 〈x1,xA〉) I) @
+(* [0x1997] TSX                 *) (compile m ? TSX maINH I) @
+(* [0x1998] LDA 7,X             *) (compile m ? LDA (maIX1 〈x0,x7〉) I) @
+(* [0x199A] LDX 4,X             *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
+(* [0x199C] CLRH                *) (compile m ? CLR maINHH I) @
+(* [0x199D] DIV                 *) (compile m ? DIV maINH I) @
+(* [0x199E] STA 4,SP            *) (compile m ? STA (maSP1 〈x0,x4〉) I) @
+(* [0x19A1] LDA 9,SP            *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
+(* [0x19A4] DIV                 *) (compile m ? DIV maINH I) @
+(* [0x19A5] STA 5,SP            *) (compile m ? STA (maSP1 〈x0,x5〉) I) @
+(* [0x19A8] CLR 8,SP            *) (compile m ? CLR (maSP1 〈x0,x8〉) I) @
+(* [0x19AB] PSHH                *) (compile m ? PSHH maINH I) @
+(* [0x19AC] PULA                *) (compile m ? PULA maINH I) @
+(* [0x19AD] STA 9,SP            *) (compile m ? STA (maSP1 〈x0,x9〉) I) @
+(* [0x19B0] RTS                 *) (compile m ? RTS maINH I) @
+(* [0x19B1] CLRA                *) (compile m ? CLR maINHA I) @
+(* [0x19B2] PSHA                *) (compile m ? PSHA maINH I) @
+(* [0x19B3] LDX #0x08           *) (compile m ? LDX (maIMM1 〈x0,x8〉) I) @
+(* [0x19B5] CLC                 *) (compile m ? CLC maINH I) @
+(* [0x19B6] ROL 10,SP           *) (compile m ? ROL (maSP1 〈x0,xA〉) I) @
+(* [0x19B9] ROL 9,SP            *) (compile m ? ROL (maSP1 〈x0,x9〉) I) @
+(* [0x19BC] ROL 1,SP            *) (compile m ? ROL (maSP1 〈x0,x1〉) I) @
+(* [0x19BF] LDA 5,SP            *) (compile m ? LDA (maSP1 〈x0,x5〉) I) @
+(* [0x19C2] CMP 1,SP            *) (compile m ? CMP (maSP1 〈x0,x1〉) I) @
+(* [0x19C5] BHI *+31 ; 0x19E4   *) (compile m ? BHI (maIMM1 〈x1,xD〉) I) @
+(* [0x19C7] BNE *+10 ; 0x19D1   *) (compile m ? BNE (maIMM1 〈x0,x8〉) I) @
+(* [0x19C9] LDA 6,SP            *) (compile m ? LDA (maSP1 〈x0,x6〉) I) @
+(* [0x19CC] CMP 9,SP            *) (compile m ? CMP (maSP1 〈x0,x9〉) I) @
+(* [0x19CF] BHI *+21 ; 0x19E4   *) (compile m ? BHI (maIMM1 〈x1,x3〉) I) @
+(* [0x19D1] LDA 9,SP            *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
+(* [0x19D4] SUB 6,SP            *) (compile m ? SUB (maSP1 〈x0,x6〉) I) @
+(* [0x19D7] STA 9,SP            *) (compile m ? STA (maSP1 〈x0,x9〉) I) @
+(* [0x19DA] LDA 1,SP            *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
+(* [0x19DD] SBC 5,SP            *) (compile m ? SBC (maSP1 〈x0,x5〉) I) @
+(* [0x19E0] STA 1,SP            *) (compile m ? STA (maSP1 〈x0,x1〉) I) @
+(* [0x19E3] SEC                 *) (compile m ? SEC maINH I) @
+(* [0x19E4] DBNZX *-46 ; 0x19B6 *) (compile m ? DBNZ (maINHX_and_IMM1 〈xD,x0〉) I) @
+(* [0x19E6] LDA 10,SP           *) (compile m ? LDA (maSP1 〈x0,xA〉) I) @
+(* [0x19E9] ROLA                *) (compile m ? ROL maINHA I) @
+(* [0x19EA] STA 6,SP            *) (compile m ? STA (maSP1 〈x0,x6〉) I) @
+(* [0x19ED] LDA 9,SP            *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
+(* [0x19F0] STA 10,SP           *) (compile m ? STA (maSP1 〈x0,xA〉) I) @
+(* [0x19F3] PULA                *) (compile m ? PULA maINH I) @
+(* [0x19F4] STA 8,SP            *) (compile m ? STA (maSP1 〈x0,x8〉) I) @
+(* [0x19F7] CLR 4,SP            *) (compile m ? CLR (maSP1 〈x0,x4〉) I) @
+(* [0x19FA] RTS                 *) (compile m ? RTS maINH I) @
+
+(*
+static void _LADD_k_is_k_plus_j(_PARAM_BINARY_L) { ... }
+*)
+
+(* [0x19FB] TSX      *) (compile m ? TSX maINH I) @
+(* [0x19FC] LDA 18,X *) (compile m ? LDA (maIX1 〈x1,x2〉) I) @
+(* [0x19FE] ADD 5,X  *) (compile m ? ADD (maIX1 〈x0,x5〉) I) @
+(* [0x1A00] STA 18,X *) (compile m ? STA (maIX1 〈x1,x2〉) I) @
+(* [0x1A02] LDA 17,X *) (compile m ? LDA (maIX1 〈x1,x1〉) I) @
+(* [0x1A04] ADC 4,X  *) (compile m ? ADC (maIX1 〈x0,x4〉) I) @
+(* [0x1A06] STA 17,X *) (compile m ? STA (maIX1 〈x1,x1〉) I) @
+(* [0x1A08] LDA 16,X *) (compile m ? LDA (maIX1 〈x1,x0〉) I) @
+(* [0x1A0A] ADC 3,X  *) (compile m ? ADC (maIX1 〈x0,x3〉) I) @
+(* [0x1A0C] STA 16,X *) (compile m ? STA (maIX1 〈x1,x0〉) I) @
+(* [0x1A0E] LDA 15,X *) (compile m ? LDA (maIX1 〈x0,xF〉) I) @
+(* [0x1A10] ADC 2,X  *) (compile m ? ADC (maIX1 〈x0,x2〉) I) @
+(* [0x1A12] STA 15,X *) (compile m ? STA (maIX1 〈x0,xF〉) I) @
+(* [0x1A14] AIS #10  *) (compile m ? AIS (maIMM1 〈x0,xA〉) I) @
+(* [0x1A16] PULH     *) (compile m ? PULH maINH I) @
+(* [0x1A17] PULX     *) (compile m ? PULX maINH I) @
+(* [0x1A18] PULA     *) (compile m ? PULA maINH I) @
+(* [0x1A19] RTS      *) (compile m ? RTS maINH I) @
+
+(*
+void _IMODU_STAR08(int i, ...) { ... }
+*)
+
+(* [0x1A1A] AIS #-2    *) (compile m ? AIS (maIMM1 〈xF,xE〉) I) @
+(* [0x1A1C] STHX 1,SP  *) (compile m ? STHX (maSP1 〈x0,x1〉) I) @
+(* [0x1A1F] PSHA       *) (compile m ? PSHA maINH I) @
+(* [0x1A20] JSR 0x1992 *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x9,x2〉〉) I) @
+(* [0x1A23] PULA       *) (compile m ? PULA maINH I) @
+(* [0x1A24] AIS #2     *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
+(* [0x1A26] LDHX 3,SP  *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
+(* [0x1A29] RTS        *) (compile m ? RTS maINH I) @
+
+(*
+void _LADD(void) { ... }
+*)
+
+(* [0x1A2A] JSR 0x197C *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x7,xC〉〉) I) @
+(* [0x1A2D] JSR 0x19FB *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈xF,xB〉〉) I) @
+
+(*
+void _POP32(void) { ... }
+*)
+
+(* [0x1A30] PSHA     *) (compile m ? PSHA maINH I) @
+(* [0x1A31] LDA 4,SP *) (compile m ? LDA (maSP1 〈x0,x4〉) I) @
+(* [0x1A34] STA ,X   *) (compile m ? STA maIX0 I) @
+(* [0x1A35] LDA 5,SP *) (compile m ? LDA (maSP1 〈x0,x5〉) I) @
+(* [0x1A38] STA 1,X  *) (compile m ? STA (maIX1 〈x0,x1〉) I) @
+(* [0x1A3A] LDA 6,SP *) (compile m ? LDA (maSP1 〈x0,x6〉) I) @
+(* [0x1A3D] STA 2,X  *) (compile m ? STA (maIX1 〈x0,x2〉) I) @
+(* [0x1A3F] LDA 7,SP *) (compile m ? LDA (maSP1 〈x0,x7〉) I) @
+(* [0x1A42] STA 3,X  *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
+(* [0x1A44] PULA     *) (compile m ? PULA maINH I) @
+(* [0x1A45] PULH     *) (compile m ? PULH maINH I) @
+(* [0x1A46] PULX     *) (compile m ? PULX maINH I) @
+(* [0x1A47] AIS #4   *) (compile m ? AIS (maIMM1 〈x0,x4〉) I) @
+(* [0x1A49] JMP ,X   *) (compile m ? JMP maINHX0ADD I)
+
+(* attraverso simulazione in CodeWarrior si puo' enunciare che dopo
+   80+(65*n*(n+1)*(n+2))/6 si sara' entrati in stato STOP corrispondente
+   AFTER: HX=num PC=0x1951 I=0 *)
+ ).
+
+(* creazione del processore+caricamento+impostazione registri *)
+definition dTest_HCS08_gNum_status ≝
+λt:memory_impl.
+λI_op:bool.
+λA_op:byte8.
+λHX_op:word16.
+λPC_op:word16.
+λaddr:word16.
+λelems:word16.
+λdata:list byte8.
+ setweak_i_flag HCS08 t (* I<-I_op *)
+  (set_acc_8_low_reg HCS08 t (* A<-A_op *)
+   (set_z_flag HCS08 t (* Z<-true *)
+    (setweak_sp_reg HCS08 t (* SP<-0x016F *)
+     (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
+      (set_pc_reg HCS08 t (* PC<-PC_op *)
+       (start_of_mcu_version
+        MC9S08GB60 t
+        (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
+         (load_from_source_at t (zero_memory t) (* carica source in ROM:addr *)
+           (dTest_HCS08_cSort_source elems) addr)
+          data dTest_HCS08_RAM)
+        (build_memory_type_of_mcu_version MC9S08GB60 t)
+        (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
+        false false false false false false) (* non deterministici tutti a 0 *)
+       PC_op)
+      HX_op)
+     (mk_word16 (mk_byte8 x0 x1) (mk_byte8 x6 xF)))
+    true)
+   A_op)
+  I_op.
+
+(* NUMERI AUREI: Somma divisori(x)=x, fino a 0xFFFF sono 6/28/496/8128 *)
+definition dTest_HCS08_gNum_aurei ≝
+λnum:word16.match gt_w16 num 〈〈x1,xF〉:〈xC,x0〉〉 with
+ [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x1〉 ; 〈xF,x0〉 ; 〈x1,xF〉 ; 〈xC,x0〉 ]
+ | false ⇒ match gt_w16 num 〈〈x0,x1〉:〈xF,x0〉〉 with
+  [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x1〉 ; 〈xF,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
+  | false ⇒ match gt_w16 num 〈〈x0,x0〉:〈x1,xC〉〉 with
+   [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
+   | false ⇒ match gt_w16 num 〈〈x0,x0〉:〈x0,x6〉〉 with
+    [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
+    | false ⇒ [ 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
+    ]
+   ]
+  ]
+ ] @ [ 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉
+     ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉
+     ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ].
+
+(* esecuzione execute k*(n+2) *)
+let rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
+ match s with
+  [ TickERR s' error ⇒ TickERR ? s' error
+  | TickSUSP s' susp ⇒ TickSUSP ? s' susp
+  | TickOK s' ⇒ match n with
+   [ O ⇒ TickOK ? s'
+   | S n' ⇒ dTest_HCS08_gNum_execute1 m t (execute m t (TickOK ? s') (ntot+2)) n' ntot ]
+  ].
+
+(* esecuzione execute k*(n+1)*(n+2) *)
+let rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
+ match s with
+  [ TickERR s' error ⇒ TickERR ? s' error
+  | TickSUSP s' susp ⇒ TickSUSP ? s' susp
+  | TickOK s' ⇒ match n with
+   [ O ⇒ TickOK ? s'
+   | S n' ⇒ dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot+1) ntot) n' ntot ]
+  ].
+
+(* esecuzione execute k*n*(n+1)*(n+2) *)
+let rec dTest_HCS08_gNum_execute3 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
+ match s with
+  [ TickERR s' error ⇒ TickERR ? s' error
+  | TickSUSP s' susp ⇒ TickSUSP ? s' susp
+  | TickOK s' ⇒ match n with
+   [ O ⇒ TickOK ? s'
+   | S n' ⇒ dTest_HCS08_gNum_execute3 m t (dTest_HCS08_gNum_execute2 m t (TickOK ? s') ntot ntot) n' ntot ]
+  ].
+
+(* esecuzione execute 80+11*n*(n+1)*(n+2) *)
+definition dTest_HCS08_gNum_execute4 ≝
+λm:mcu_type.λt:memory_impl.λs:tick_result (any_status m t).λntot:nat.
+ match s with
+  [ TickERR s' error ⇒ TickERR ? s' error
+  | TickSUSP s' susp ⇒ TickSUSP ? s' susp
+  | TickOK s' ⇒ execute m t (dTest_HCS08_gNum_execute3 m t (TickOK ? s') 11 ntot) 80
+  ].
+
+(* parametrizzazione dell'enunciato del teorema parziale *)
+lemma dTest_HCS08_gNum_aux ≝
+λt:memory_impl.λnum:word16.
+ (* 2) match di esecuzione su tempo in forma di upperbound *)
+ match dTest_HCS08_gNum_execute4 HCS08 t
+  (TickOK ? (dTest_HCS08_gNum_status t true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
+  (* tempo di esecuzione 80+11*n*(n+1)*(n+2) *)
+  num with
+   [ TickERR s _ ⇒ None ?
+   (* azzeramento tutta RAM tranne dati *)
+   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
+   | TickOK s ⇒ None ?
+   ] =
+  Some ? (dTest_HCS08_gNum_status t false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
+
+definition gNumCalc ≝
+λnum:word16.
+ match dTest_HCS08_gNum_execute4 HCS08 MEM_TREE
+  (TickOK ? (dTest_HCS08_gNum_status MEM_TREE true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
+  num with
+   [ TickERR s _ ⇒ None ?
+   | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
+   | TickOK s ⇒ None ?
+   ].
+
+definition gNumNoCalc ≝
+λnum:word16.
+ Some ? (dTest_HCS08_gNum_status MEM_TREE false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
+
+definition gNumCalc1    ≝ gNumCalc 〈〈x0,x0〉:〈x0,x1〉〉.
+definition gNumCalc2    ≝ gNumCalc 〈〈x0,x0〉:〈x0,x2〉〉.
+definition gNumCalc5    ≝ gNumCalc 〈〈x0,x0〉:〈x0,x5〉〉.
+definition gNumCalc10   ≝ gNumCalc 〈〈x0,x0〉:〈x0,xA〉〉.
+definition gNumCalc20   ≝ gNumCalc 〈〈x0,x0〉:〈x1,x4〉〉.
+definition gNumCalc50   ≝ gNumCalc 〈〈x0,x0〉:〈x3,x2〉〉.
+definition gNumCalc100  ≝ gNumCalc 〈〈x0,x0〉:〈x6,x4〉〉.
+definition gNumCalc250  ≝ gNumCalc 〈〈x0,x0〉:〈xF,xA〉〉.
+definition gNumCalc500  ≝ gNumCalc 〈〈x0,x1〉:〈xF,x4〉〉.
+definition gNumCalc1000 ≝ gNumCalc 〈〈x0,x3〉:〈xE,x8〉〉.
+
+definition gNumNoCalc1    ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x1〉〉.
+definition gNumNoCalc2    ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x2〉〉.
+definition gNumNoCalc5    ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x5〉〉.
+definition gNumNoCalc10   ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,xA〉〉.
+definition gNumNoCalc20   ≝ gNumNoCalc 〈〈x0,x0〉:〈x1,x4〉〉.
+definition gNumNoCalc50   ≝ gNumNoCalc 〈〈x0,x0〉:〈x3,x2〉〉.
+definition gNumNoCalc100  ≝ gNumNoCalc 〈〈x0,x0〉:〈x6,x4〉〉.
+definition gNumNoCalc250  ≝ gNumNoCalc 〈〈x0,x0〉:〈xF,xA〉〉.
+definition gNumNoCalc500  ≝ gNumNoCalc 〈〈x0,x1〉:〈xF,x4〉〉.
+definition gNumNoCalc1000 ≝ gNumNoCalc 〈〈x0,x3〉:〈xE,x8〉〉.
diff --git a/helm/software/matita/library/freescale/medium_tests_lemmas.ma b/helm/software/matita/library/freescale/medium_tests_lemmas.ma
index 44f770ae34e67d41f50e9e7ca41ba948ee4a7f43..81505ac2615211999ab80f6060214f420baf4db1 100644 (file)
--- a/helm/software/matita/library/freescale/medium_tests_lemmas.ma
+++ b/helm/software/matita/library/freescale/medium_tests_lemmas.ma
@@ -127,7 +127,6 @@ axiom MSB16_of_make_word16 :
  ∀bh,bl:byte8.
   MSB_w16 (mk_word16 bh bl) = MSB_b8 bh.
 
-(*
 lemma execute_HCS08_LDHX_maIMM2 :
  ∀t:memory_impl.∀s:any_status HCS08 t.∀bhigh,blow:byte8.
   (get_clk_desc HCS08 t s = None ?) →
@@ -137,7 +136,7 @@ lemma execute_HCS08_LDHX_maIMM2 :
   (memory_filter_read HCS08 t s (filtered_inc_w16 HCS08 t s
                                  (filtered_inc_w16 HCS08 t s
                                   (get_pc_reg HCS08 t s))) = Some ? blow)
-  → execute HCS08 t (TickOK ? s) 3 =
+  → (execute HCS08 t (TickOK ? s) 3 =
     TickOK ? (set_pc_reg HCS08 t
               (setweak_v_flag HCS08 t
                (setweak_n_flag HCS08 t 
@@ -147,11 +146,11 @@ lemma execute_HCS08_LDHX_maIMM2 :
                 (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉))
                (MSB_w16 〈bhigh:blow〉))
               false)
-             (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3)).
+             (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3))).
 
  intros;
  whd in ⊢ (? ? % ?);
- whd in ⊢ (? ? match % return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > H;
 
  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
@@ -169,13 +168,14 @@ lemma execute_HCS08_LDHX_maIMM2 :
    [ true ⇒ tick_execute HCS08 t s (anyOP HCS08 LDHX) MODE_IMM2 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))
    | false ⇒ TickOK (any_status HCS08 t) (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉     (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))]);
  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+
  letin status1 ≝ (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))));
  change in ⊢ (? ? % ?) with
   (match 2 with 
    [ O ⇒ TickOK ? status1
    | S (n':nat) ⇒ execute HCS08 t (tick HCS08 t status1) n']);
- whd in ⊢ (? ? match ? return ? with [_⇒?|_⇒λ_:?.? ? ? % ?] ?);
- unfold status1 in ⊢ (? ? match ? in nat return ? with [_⇒? |_ ⇒ λ_.? ? ? match ? ? ? % in option return ? with [_⇒?|_⇒?] ?] ?);
+ whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
+ unfold status1 in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_. ? ? ? match ? ? ? % in option return ? with [_⇒?|_⇒?] ?] ?);
  rewrite > (get_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))));
  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
  normalize in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? (? ? (? ? ? ? (? ? (? ? ? ? ? ? % ? ? ? ?)))) ?] ?);
@@ -191,14 +191,14 @@ lemma execute_HCS08_LDHX_maIMM2 :
    [ O ⇒ TickOK ? status2
    | S (n':nat) ⇒ execute HCS08 t (tick HCS08 t status2) n']);
  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
- unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒ λ_. ? ? ? match ? ? ? % in option return ? with [_⇒?|_⇒?] ?] ?);
+ unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.  ? ? ? match ? ? ? % in option return ? with [_⇒?|_⇒?] ?] ?);
  rewrite > (get_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))));
  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
  change in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.? ? ? match % in option return ? with [_⇒?|_⇒?] ?] ?) with
   (execute_LDHX HCS08 t status2 MODE_IMM2
  (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)));
  whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.? ? ? match % in option return ? with [_⇒?|_⇒?] ?] ?);
- whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒ λ_.? ? ? match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
+ whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.? ? ? match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 
  unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match ? ? ? % ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
  rewrite > (memory_filter_read_set_clk_desc HCS08 t s (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))
@@ -244,7 +244,7 @@ lemma execute_HCS08_LDHX_maIMM2 :
  rewrite > (set_clk_desc_set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t s (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3));
  rewrite > (set_set_clk_desc HCS08 t (set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t s (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (None ?));
  rewrite > (set_clk_f_set_clk_desc HCS08 t s (λtmps.set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t tmps (set_indX_16_reg_HC08 (alu HCS08 t tmps) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t tmps (get_pc_reg HCS08 t tmps) 3))) in ⊢ (? ? (? ? %) ?);
- [2: assumption ]
+ [2: elim H; reflexivity ]
  reflexivity.
 qed.
 
@@ -286,114 +286,114 @@ lemma execute_HCS08_STHX_maSP1 :
 
  intros;
  whd in ⊢ (? ? % ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > H;
 
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match match % in fetch_result return ? with [FetchERR⇒?|FetchOK⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > H1;
 
- whd in ⊢ (? ? match match % in fetch_result return ? with [FetchERR⇒?|FetchOK⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > H2 in ⊢ (? ? match match match % in option return ? with [None⇒?|Some⇒?] in fetch_result return ? with [FetchERR⇒?|FetchOK⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match match % in fetch_result return ? with [FetchERR⇒?|FetchOK⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- change in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with
+ whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > H2 in ⊢ (? ? match match match % in option return ? with [_⇒?|_⇒?] in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ change in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
   (match quadrupleT ???? (anyOP HCS08 STHX) MODE_SP1 〈〈x9,xE〉:〈xF,xF〉〉 〈x0,x5〉 with [ quadrupleT pseudo mode _ tot_clk ⇒ match eq_b8 〈x0,x1〉 tot_clk with [true⇒tick_execute HCS08 MEM_TREE s pseudo mode (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) |false⇒ TickOK (any_status HCS08 MEM_TREE) (set_clk_desc HCS08 MEM_TREE s (Some (Prod5T byte8 (any_opcode HCS08) instr_mode byte8 word16) (quintupleT byte8 (any_opcode HCS08) instr_mode byte8 word16 〈x0,x1〉 pseudo mode tot_clk (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))]]);
- change in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with
+ change in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
   (match eq_b8 〈x0,x1〉 〈x0,x5〉 with [true⇒ tick_execute HCS08 MEM_TREE s (anyOP HCS08 STHX) MODE_SP1 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) |false⇒ TickOK (any_status HCS08 MEM_TREE) (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))]);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 
  letin status1 ≝ (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE  s (get_pc_reg HCS08 MEM_TREE s))))));
- change in ⊢ (? ? match ? ? % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (status1);
+ change in ⊢ (? ? match ? ? % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with (status1);
  change in ⊢ (? ? % ?) with (execute HCS08 MEM_TREE (TickOK ? status1) 4);
 
  whd in ⊢ (? ? % ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- unfold status1 in ⊢ (? ? match match ? ? ? % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) ) in ⊢ (? ? match match % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- unfold status1 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ unfold status1 in ⊢ (? ? match match ? ? ? % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) ) in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ unfold status1 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  letin status2 ≝ (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))));
  change in ⊢ (? ? % ?) with (execute HCS08 MEM_TREE (TickOK ? status2) 3);
 
  whd in ⊢ (? ? % ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- unfold status2 in ⊢ (? ? match match ? ? ? % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- unfold status2 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ unfold status2 in ⊢ (? ? match match ? ? ? % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ unfold status2 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 
  letin status3 ≝ (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))));
  change in ⊢ (? ? % ?) with (execute HCS08 MEM_TREE (TickOK ? status3) 2);
 
  whd in ⊢ (? ? % ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- unfold status3 in ⊢ (? ? match match ? ? ? % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- unfold status3 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ unfold status3 in ⊢ (? ? match match ? ? ? % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ unfold status3 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 
  letin status4 ≝ (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))));
  change in ⊢ (? ? % ?) with (execute HCS08 MEM_TREE (TickOK ? status4) 1);
 
  whd in ⊢ (? ? % ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- unfold status4 in ⊢ (? ? match match ? ? ? % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- change in ⊢ (? ? match match % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (execute_STHX HCS08 MEM_TREE status4 MODE_SP1 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))));
- whd in ⊢ (? ? match match % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- unfold status4 in ⊢ (? ? match match match match ? ? ? % ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ unfold status4 in ⊢ (? ? match match ? ? ? % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ change in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with (execute_STHX HCS08 MEM_TREE status4 MODE_SP1 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))));
+ whd in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ unfold status4 in ⊢ (? ? match match match match ? ? ? % ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (memory_filter_read_set_clk_desc HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > H3 in ⊢ (? ? match match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > H3 in ⊢ (? ? match match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 
- whd in ⊢ (? ? match match match match ? in option return ? with [None⇒?|Some (x:?)⇒(λoffs:?.%) ?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match match match match ? in option return ? with [None⇒?|Some (x:?)⇒ (λoffs:?.match % in option return ? with [None⇒?|Some⇒?]) ?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match match match match ? in option return ? with [None⇒?|Some (x:?)⇒(λoffs:?.match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?]) ?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match match match match ? in option return ? with [_⇒?|_⇒λ_.(λoffs:?.%) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match match match match ? in option return ? with [_⇒?|_⇒λ_.(λoffs:?.match % in option return ? with [_⇒?|_⇒?]) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match match match match ? in option return ? with [_⇒?|_⇒λ_.(λoffs:?.match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?]) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match match ? in option return ? with [None⇒? |Some (x:?)⇒ (λoffs:?.match match match ? ? ? (? ? ? (? (? %) ?)) in memory_type return ? with [MEM_READ_ONLY⇒?|MEM_READ_WRITE⇒?|MEM_OUT_OF_BOUND⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?]) ?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match match ? in option return ? with [_⇒? |_⇒λ_. (λoffs:?.match match match ? ? ? (? ? ? (? (? %) ?)) in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?]) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_chk_desc_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match match ? in option return ? with [None⇒?|Some (x:?)⇒(λoffs:? .match match match ? ? ? (? ? % ?) in memory_type return ? with [MEM_READ_ONLY⇒?|MEM_READ_WRITE⇒?|MEM_OUT_OF_BOUND⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?]) ?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- change in ⊢ (? ? match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with
-  (match match match getn_array8T o0 memory_type (chk_get MEM_TREE (get_chk_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) in memory_type return λm.(option (Prod16T (Prod16T (Prod16T (Prod16T byte8))))) with [MEM_READ_ONLY⇒ Some (Prod16T (Prod16T (Prod16T (Prod16T byte8)))) (get_mem_desc HCS08 MEM_TREE status4) |MEM_READ_WRITE⇒ Some (Prod16T (Prod16T (Prod16T (Prod16T byte8)))) (mt_update byte8 (get_mem_desc HCS08 MEM_TREE status4) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE status4)) 〈〈x0,x0〉:blow〉) (w16h 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE status4)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE status4))〉)) |MEM_OUT_OF_BOUND⇒None (Prod16T (Prod16T (Prod16T (Prod16T byte8))))] in option return λo.(option (any_status HCS08 MEM_TREE)) with [None⇒None (any_status HCS08 MEM_TREE) |Some x⇒ (λmem.Some (any_status HCS08 MEM_TREE) (set_mem_desc HCS08 MEM_TREE status4 mem)) x] in option return λo.(option (ProdT (any_status HCS08 MEM_TREE) word16)) with [None⇒None (ProdT (any_status HCS08 MEM_TREE) word16) |Some x⇒ (λtmps1.opt_map (any_status HCS08 MEM_TREE) (ProdT (any_status HCS08 MEM_TREE) word16) (memory_filter_write HCS08 MEM_TREE tmps1 (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE status4)) 〈〈x0,x0〉:blow〉)) (w16l 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE status4)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE status4))〉)) (λtmps2.Some (ProdT (any_status HCS08 MEM_TREE) word16) (pair (any_status HCS08 MEM_TREE) word16 tmps2 (filtered_plus_w16 HCS08 MEM_TREE tmps2 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1)))) x]);
- rewrite > H4 in ⊢ (? ? match match match match match match ? ? ? % in memory_type return ? with [MEM_READ_ONLY⇒?|MEM_READ_WRITE⇒?|MEM_OUT_OF_BOUND⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); 
+  in ⊢ (? ? match match match match ? in option return ? with [_⇒?|_⇒λ_.(λoffs:? .match match match ? ? ? (? ? % ?) in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?]) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ change in ⊢ (? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
+  (match match match getn_array8T o0 memory_type (chk_get MEM_TREE (get_chk_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) in memory_type return λm.(option (Prod16T (Prod16T (Prod16T (Prod16T byte8))))) with [MEM_READ_ONLY⇒ Some (Prod16T (Prod16T (Prod16T (Prod16T byte8)))) (get_mem_desc HCS08 MEM_TREE status4) |MEM_READ_WRITE⇒ Some (Prod16T (Prod16T (Prod16T (Prod16T byte8)))) (mt_update byte8 (get_mem_desc HCS08 MEM_TREE status4) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE status4)) 〈〈x0,x0〉:blow〉) (w16h 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE status4)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE status4))〉)) |MEM_OUT_OF_BOUND⇒None (Prod16T (Prod16T (Prod16T (Prod16T byte8))))] in option return λo.(option (any_status HCS08 MEM_TREE)) with [None⇒None (any_status HCS08 MEM_TREE) |Some x⇒ (λmem.Some (any_status HCS08 MEM_TREE) (set_mem_desc HCS08 MEM_TREE status4 mem)) x] in option return λo.(option (Prod (any_status HCS08 MEM_TREE) word16)) with [None⇒None (Prod (any_status HCS08 MEM_TREE) word16) |Some x⇒ (λtmps1.opt_map (any_status HCS08 MEM_TREE) (Prod (any_status HCS08 MEM_TREE) word16) (memory_filter_write HCS08 MEM_TREE tmps1 (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE status4)) 〈〈x0,x0〉:blow〉)) (w16l 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE status4)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE status4))〉)) (λtmps2.Some (Prod (any_status HCS08 MEM_TREE) word16) (pair (any_status HCS08 MEM_TREE) word16 tmps2 (filtered_plus_w16 HCS08 MEM_TREE tmps2 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1)))) x]);
+ rewrite > H4 in ⊢ (? ? match match match match match match ? ? ? % in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?); 
 
- whd in ⊢ (? ? match match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_mem_desc_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? % ? ?)) in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? % ? ?)) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? ? (? (? (? %) ?)))) in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? ? (? (? (? %) ?)))) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? (? (? %) ?) ?)) in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? (? (? %) ?) ?)) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? ? (? (? ? (? %))))) in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? ? (? (? ? (? %))))) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 
  rewrite > (set_clk_desc_set_mem_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) (w16h 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE s)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE s))〉)) )
-  in ⊢ (? ? match match match match ? ? % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match match ? ? % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (w16h_of_make_word16 (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE s)))
-  in ⊢ (? ? match match match match ? ? (? ? ? (? ? ? ? (? ? ? ? %)) ?) in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); 
+  in ⊢ (? ? match match match match ? ? (? ? ? (? ? ? ? (? ? ? ? %)) ?) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?); 
  letin status5 ≝ (set_clk_desc HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)))) (Some (Prod5T byte8 (any_opcode HCS08) instr_mode byte8 word16) (quintupleT byte8 (any_opcode HCS08) instr_mode byte8 word16 〈x0,x4〉 STHX MODE_SP1 〈x0,x5〉  (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))));
- change in ⊢ (? ? match match match match ? ? % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (status5);
- change in ⊢ (? ? match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with
+ change in ⊢ (? ? match match match match ? ? % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with (status5);
+ change in ⊢ (? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
   (opt_map ?? (memory_filter_write HCS08 MEM_TREE status5 (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE status4)) 〈〈x0,x0〉:blow〉)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE status4))) (λtmps2:any_status HCS08 MEM_TREE .Some ? (pair ?? tmps2 (filtered_plus_w16 HCS08 MEM_TREE tmps2 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1))));
  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match ? ? ? (? ? ? ? ? (? %)) ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match ? ? ? (? ? ? ? ? (? %)) ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match ? ? ? (? ? ? ? (? (? (? %) ?)) ?) ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match ? ? ? (? ? ? ? (? (? (? %) ?)) ?) ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 
- whd in ⊢ (? ? match match match ? ? ? % ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- whd in ⊢ (? ? match match match ? ? ? match % in option return ? with [None⇒?|Some⇒?] ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match match match ? ? ? % ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ whd in ⊢ (? ? match match match ? ? ? match % in option return ? with [_⇒?|_⇒?] ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_chk_desc_set_clk_desc HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)))) (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
-  in ⊢ (? ? match match match ? ? ? match match ? ? ? (? ? % ?) in memory_type return ? with [MEM_READ_ONLY⇒?|MEM_READ_WRITE⇒?|MEM_OUT_OF_BOUND⇒?] in option return ? with [None⇒?|Some⇒?] ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match ? ? ? match match ? ? ? (? ? % ?) in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > (get_chk_desc_set_mem_desc HCS08 MEM_TREE s (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) (indX_high_reg_HC08 (alu HCS08 MEM_TREE s))))
-  in ⊢ (? ? match match match ? ? ? match match ? ? ? (? ? % ?) in memory_type return ? with [MEM_READ_ONLY⇒?|MEM_READ_WRITE⇒?|MEM_OUT_OF_BOUND⇒?] in option return ? with [None⇒?|Some⇒?] ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
- rewrite > H5 in ⊢ (? ? match match match ? ? ? match match ? ? ? % in memory_type return ? with [MEM_READ_ONLY⇒?|MEM_READ_WRITE⇒?|MEM_OUT_OF_BOUND⇒?] in option return ? with [None⇒?|Some⇒?] ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+  in ⊢ (? ? match match match ? ? ? match match ? ? ? (? ? % ?) in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
+ rewrite > H5 in ⊢ (? ? match match match ? ? ? match match ? ? ? % in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 
- whd in ⊢ (? ? match match % in option return ? with [None⇒?|Some⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
+ whd in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  whd in ⊢ (? ? % ?);
  rewrite > (filtered_plus_set_mem_desc HCS08 MEM_TREE status5 (mt_update byte8 (get_mem_desc HCS08 MEM_TREE status5) (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE s))) (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1)
   in ⊢ (? ? (? ? (? ? ? (? ? ? ? %) ?)) ?);
@@ -436,4 +436,3 @@ lemma execute_HCS08_STHX_maSP1 :
  [2: elim H; reflexivity ]
  reflexivity.
 qed.
-*)
diff --git a/helm/software/matita/library/freescale/medium_tests_tools.ma b/helm/software/matita/library/freescale/medium_tests_tools.ma
index fcdda667af0140300eb4fcd47c77c3c7c5f5f489..f1e394d2232c8b624d128e895aeb2a9853e8ed72 100644 (file)
--- a/helm/software/matita/library/freescale/medium_tests_tools.ma
+++ b/helm/software/matita/library/freescale/medium_tests_tools.ma
@@ -596,3 +596,9 @@ definition dTest_bytes_aux : list byte8 ≝
    counters, index, position, e stack di esecuzione *)
 definition dTest_zeros : list byte8 ≝
  dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux.
+
+definition dTest_zeros3K : list byte8 ≝
+  dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@
+  dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@
+  dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@
+  dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux@dTest_bytes_aux.
diff --git a/helm/software/matita/library/freescale/multivm.ma b/helm/software/matita/library/freescale/multivm.ma
index 2e63c2054a26a598983e7131da91c76ea6733a47..b78efba70dad77b5371bac1bf15e873ccffefe5b 100644 (file)
--- a/helm/software/matita/library/freescale/multivm.ma
+++ b/helm/software/matita/library/freescale/multivm.ma
@@ -944,7 +944,7 @@ definition execute_SBC ≝
  execute_SBC_SUB_aux m t s i cur_pc true
  (λA_op.λM_op.λC_op.match plus_b8 A_op (compl_b8 M_op) false with
   [ pair resb resc ⇒ match C_op with
-   [ true ⇒ plus_b8 resb 〈xF,xF〉 resc
+   [ true ⇒ plus_b8 resb 〈xF,xF〉 false
    | false ⇒ pair ?? resb resc ]]).
 
 (* C = 1 *)
@@ -1304,14 +1304,12 @@ definition tick ≝
 (* ESECUZIONE *)
 (* ********** *)
 
-definition execute := \lambda m:mcu_type.
-let rec execute  (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
+let rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
  match s with
   [ TickERR s' error ⇒ TickERR ? s' error
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
-  | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute t (tick m t s') n' ]
-  ]
-in execute.
+  | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
+  ].
 
 lemma breakpoint:
  ∀m,u,s,n1,n2. execute m u s (n1 + n2) = execute m u (execute m u s n1) n2.
diff --git a/helm/software/matita/library/freescale/opcode.ma b/helm/software/matita/library/freescale/opcode.ma
index 62199d7d354142d8d35fcb3d816351e423a2ec2c..47312085f146a5c58f104da6e63ddc4a27b17897 100644 (file)
--- a/helm/software/matita/library/freescale/opcode.ma
+++ b/helm/software/matita/library/freescale/opcode.ma
@@ -48,8 +48,17 @@ inductive instr_mode: Type ≝
   (* INHERENT = nessun operando (H implicito) *)
 | MODE_INHH : instr_mode
 
+  (* INHERENT_ADDRESS = nessun operando (HX implicito) *)
+| MODE_INHX0ADD : instr_mode
+  (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *)
+| MODE_INHX1ADD : instr_mode
+  (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *)
+| MODE_INHX2ADD : instr_mode
+
   (* IMMEDIATE = operando valore immediato byte = 0xbb *)
 | MODE_IMM1 : instr_mode
+  (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *)
+| MODE_IMM1EXT : instr_mode
   (* IMMEDIATE = operando valore immediato word = 0xwwww *)
 | MODE_IMM2 : instr_mode
   (* DIRECT = operando offset byte = [0x00bb] *)
@@ -326,40 +335,45 @@ definition magic_of_instr_mode ≝
 | MODE_INHA ⇒ 〈x0,x1〉
 | MODE_INHX ⇒ 〈x0,x2〉
 | MODE_INHH ⇒ 〈x0,x3〉
- 
-| MODE_IMM1 ⇒ 〈x0,x4〉
-| MODE_IMM2 ⇒ 〈x0,x5〉
-| MODE_DIR1 ⇒ 〈x0,x6〉
-| MODE_DIR2 ⇒ 〈x0,x7〉
-| MODE_IX0  ⇒ 〈x0,x8〉
-| MODE_IX1  ⇒ 〈x0,x9〉
-| MODE_IX2  ⇒ 〈x0,xA〉
-| MODE_SP1  ⇒ 〈x0,xB〉
-| MODE_SP2  ⇒ 〈x0,xC〉
-
-| MODE_DIR1_to_DIR1 ⇒ 〈x0,xD〉
-| MODE_IMM1_to_DIR1 ⇒ 〈x0,xE〉
-| MODE_IX0p_to_DIR1 ⇒ 〈x0,xF〉
-| MODE_DIR1_to_IX0p ⇒ 〈x1,x0〉
-
-| MODE_INHA_and_IMM1 ⇒ 〈x1,x1〉
-| MODE_INHX_and_IMM1 ⇒ 〈x1,x2〉
-| MODE_IMM1_and_IMM1 ⇒ 〈x1,x3〉
-| MODE_DIR1_and_IMM1 ⇒ 〈x1,x4〉
-| MODE_IX0_and_IMM1  ⇒ 〈x1,x5〉
-| MODE_IX0p_and_IMM1 ⇒ 〈x1,x6〉
-| MODE_IX1_and_IMM1  ⇒ 〈x1,x7〉
-| MODE_IX1p_and_IMM1 ⇒ 〈x1,x8〉
-| MODE_SP1_and_IMM1  ⇒ 〈x1,x9〉
-
-  (* 26-33: bisogna considerare l'operando implicito *)
-| MODE_DIRn o          ⇒ plus_b8nc 〈x1,xA〉 〈x0,(exadecim_of_oct o)〉
-  (* 34-41: bisogna considerare l'operando implicito *)
-| MODE_DIRn_and_IMM1 o ⇒ plus_b8nc 〈x2,x2〉 〈x0,(exadecim_of_oct o)〉
-  (* 42-57: bisogna considerare l'operando implicito *)
-| MODE_TNY e           ⇒ plus_b8nc 〈x2,xA〉 〈x0,e〉
-  (* 58-99: bisogna considerare gli operandi impliciti *)
-| MODE_SRT t           ⇒ plus_b8nc 〈x3,xA〉 (byte8_of_bitrigesim t)
+
+| MODE_INHX0ADD ⇒ 〈x0,x4〉
+| MODE_INHX1ADD ⇒ 〈x0,x5〉
+| MODE_INHX2ADD ⇒ 〈x0,x6〉
+
+| MODE_IMM1 ⇒ 〈x0,x7〉
+| MODE_IMM1EXT ⇒ 〈x0,x8〉
+| MODE_IMM2 ⇒ 〈x0,x9〉
+| MODE_DIR1 ⇒ 〈x0,xA〉
+| MODE_DIR2 ⇒ 〈x0,xB〉
+| MODE_IX0  ⇒ 〈x0,xC〉
+| MODE_IX1  ⇒ 〈x0,xD〉
+| MODE_IX2  ⇒ 〈x0,xE〉
+| MODE_SP1  ⇒ 〈x0,xF〉
+| MODE_SP2  ⇒ 〈x1,x0〉
+
+| MODE_DIR1_to_DIR1 ⇒ 〈x1,x1〉
+| MODE_IMM1_to_DIR1 ⇒ 〈x1,x2〉
+| MODE_IX0p_to_DIR1 ⇒ 〈x1,x3〉
+| MODE_DIR1_to_IX0p ⇒ 〈x1,x4〉
+
+| MODE_INHA_and_IMM1 ⇒ 〈x1,x5〉
+| MODE_INHX_and_IMM1 ⇒ 〈x1,x6〉
+| MODE_IMM1_and_IMM1 ⇒ 〈x1,x7〉
+| MODE_DIR1_and_IMM1 ⇒ 〈x1,x8〉
+| MODE_IX0_and_IMM1  ⇒ 〈x1,x9〉
+| MODE_IX0p_and_IMM1 ⇒ 〈x1,xA〉
+| MODE_IX1_and_IMM1  ⇒ 〈x1,xB〉
+| MODE_IX1p_and_IMM1 ⇒ 〈x1,xC〉
+| MODE_SP1_and_IMM1  ⇒ 〈x1,xD〉
+
+  (* 27-34: bisogna considerare l'operando implicito *)
+| MODE_DIRn o          ⇒ plus_b8nc 〈x1,xE〉 〈x0,(exadecim_of_oct o)〉
+  (* 35-42: bisogna considerare l'operando implicito *)
+| MODE_DIRn_and_IMM1 o ⇒ plus_b8nc 〈x2,x6〉 〈x0,(exadecim_of_oct o)〉
+  (* 43-58: bisogna considerare l'operando implicito *)
+| MODE_TNY e           ⇒ plus_b8nc 〈x2,xE〉 〈x0,e〉
+  (* 59-100: bisogna considerare gli operandi impliciti *)
+| MODE_SRT t           ⇒ plus_b8nc 〈x3,xE〉 (byte8_of_bitrigesim t)
 ].
 
 (* confronto fra instr_mode *)
@@ -371,64 +385,56 @@ definition eqim ≝
 (* ********************************************* *)
 
 (* su tutta la lista quante volte compare il byte *)
-definition get_byte_count := \lambda m:mcu_type.
-let rec get_byte_count  (b:byte8) (c:nat)
+let rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match thd4T ???? hd with
    [ Byte b' ⇒ match eq_b8 b b' with
-    [ true ⇒ get_byte_count b (S c) tl
-    | false ⇒ get_byte_count b c tl
+    [ true ⇒ get_byte_count m b (S c) tl
+    | false ⇒ get_byte_count m b c tl
     ]
-   | Word _ ⇒ get_byte_count b c tl
+   | Word _ ⇒ get_byte_count m b c tl
    ]
-  ]
-in get_byte_count.
+  ].
 
 (* su tutta la lista quante volte compare la word (0x9E+byte) *)
-definition get_word_count := \lambda m:mcu_type.
-let rec get_word_count (b:byte8) (c:nat)
+let rec get_word_count (m:mcu_type) (b:byte8) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match thd4T ???? hd with
-   [ Byte _ ⇒ get_word_count b c tl
+   [ Byte _ ⇒ get_word_count m b c tl
    | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
-    [ true ⇒ get_word_count b (S c) tl
-    | false ⇒ get_word_count b c tl
+    [ true ⇒ get_word_count m b (S c) tl
+    | false ⇒ get_word_count m b c tl
     ]
    ]
-  ]
-in get_word_count.
+  ].
 
 (* su tutta la lista quante volte compare lo pseudocodice *)
-definition get_pseudo_count := \lambda m:mcu_type.
-let rec get_pseudo_count  (o:opcode) (c:nat)
+let rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match fst4T ???? hd with
    [ anyOP o' ⇒ match eqop m (anyOP m o) (anyOP m o') with
-    [ true ⇒ get_pseudo_count o (S c) tl
-    | false ⇒ get_pseudo_count o c tl
+    [ true ⇒ get_pseudo_count m o (S c) tl
+    | false ⇒ get_pseudo_count m o c tl
     ]
    ]
-  ]
-in get_pseudo_count.
+  ].
 
 (* su tutta la lista quante volte compare la modalita' *)
-definition get_mode_count := \lambda m:mcu_type.
-let rec get_mode_count  (i:instr_mode) (c:nat)
+let rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match eqim (snd4T ???? hd) i with
-   [ true ⇒ get_mode_count i (S c) tl
-   | false ⇒ get_mode_count i c tl
+   [ true ⇒ get_mode_count m i (S c) tl
+   | false ⇒ get_mode_count m i c tl
    ]
-  ]
-  in get_mode_count.
+  ].
 
 (* b e' non implementato? *)
 let rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
@@ -461,19 +467,17 @@ let rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
   ].
 
 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
-definition get_OpIm_count := \lambda  m:mcu_type.
-let rec get_OpIm_count  (o:any_opcode m) (i:instr_mode) (c:nat)
+let rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒
    match (eqop m o (fst4T ???? hd)) ⊗
          (eqim i (snd4T ???? hd)) with
-    [ true ⇒ get_OpIm_count o i (S c) tl
-    | false ⇒ get_OpIm_count o i c tl
+    [ true ⇒ get_OpIm_count m o i (S c) tl
+    | false ⇒ get_OpIm_count m o i c tl
     ] 
-  ]
-  in get_OpIm_count.
+  ].
 
 (* iteratore sugli opcode *)
 definition forall_opcode ≝ λP.
@@ -493,33 +497,38 @@ definition forall_opcode ≝ λP.
 (* iteratore sulle modalita' *)
 definition forall_instr_mode ≝ λP.
   P MODE_INH
-⊗ P MODE_INHA 
-⊗ P MODE_INHX 
+⊗ P MODE_INHA
+⊗ P MODE_INHX
 ⊗ P MODE_INHH
 
-⊗ P MODE_IMM1 
-⊗ P MODE_IMM2 
-⊗ P MODE_DIR1 
+⊗ P MODE_INHX0ADD
+⊗ P MODE_INHX1ADD
+⊗ P MODE_INHX2ADD
+
+⊗ P MODE_IMM1
+⊗ P MODE_IMM1EXT
+⊗ P MODE_IMM2
+⊗ P MODE_DIR1
 ⊗ P MODE_DIR2
-⊗ P MODE_IX0  
-⊗ P MODE_IX1  
-⊗ P MODE_IX2  
-⊗ P MODE_SP1  
+⊗ P MODE_IX0
+⊗ P MODE_IX1
+⊗ P MODE_IX2
+⊗ P MODE_SP1
 ⊗ P MODE_SP2
 
-⊗ P MODE_DIR1_to_DIR1 
+⊗ P MODE_DIR1_to_DIR1
 ⊗ P MODE_IMM1_to_DIR1
-⊗ P MODE_IX0p_to_DIR1 
+⊗ P MODE_IX0p_to_DIR1
 ⊗ P MODE_DIR1_to_IX0p
 
-⊗ P MODE_INHA_and_IMM1 
-⊗ P MODE_INHX_and_IMM1 
+⊗ P MODE_INHA_and_IMM1
+⊗ P MODE_INHX_and_IMM1
 ⊗ P MODE_IMM1_and_IMM1
-⊗ P MODE_DIR1_and_IMM1 
-⊗ P MODE_IX0_and_IMM1  
+⊗ P MODE_DIR1_and_IMM1
+⊗ P MODE_IX0_and_IMM1
 ⊗ P MODE_IX0p_and_IMM1
-⊗ P MODE_IX1_and_IMM1  
-⊗ P MODE_IX1p_and_IMM1 
+⊗ P MODE_IX1_and_IMM1
+⊗ P MODE_IX1p_and_IMM1
 ⊗ P MODE_SP1_and_IMM1
 
 ⊗ forall_oct (λo. P (MODE_DIRn o))
diff --git a/helm/software/matita/library/freescale/table_HC05.ma b/helm/software/matita/library/freescale/table_HC05.ma
index e0c9b33e750f87123c006b01dc57fbd3afad4648..6938cd3e67da4da6fb181a09de9fac379801195b 100644 (file)
--- a/helm/software/matita/library/freescale/table_HC05.ma
+++ b/helm/software/matita/library/freescale/table_HC05.ma
@@ -239,21 +239,21 @@ definition opcode_table_HC05_17 ≝
 
 definition opcode_table_HC05_18 ≝
 [
-  quadrupleT ???? (anyOP HC05 JMP) MODE_DIR1 (Byte 〈xB,xC〉) 〈x0,x2〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_DIR2 (Byte 〈xC,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX2  (Byte 〈xD,xC〉) 〈x0,x4〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX1  (Byte 〈xE,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX0  (Byte 〈xF,xC〉) 〈x0,x2〉
+  quadrupleT ???? (anyOP HC05 JMP) MODE_IMM1EXT  (Byte 〈xB,xC〉) 〈x0,x2〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_IMM2     (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX2ADD (Byte 〈xD,xC〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX1ADD (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX0ADD (Byte 〈xF,xC〉) 〈x0,x2〉
 ].
 
 definition opcode_table_HC05_19 ≝
 [
-  quadrupleT ???? (anyOP HC05 BSR) MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_DIR1 (Byte 〈xB,xD〉) 〈x0,x5〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_DIR2 (Byte 〈xC,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX2  (Byte 〈xD,xD〉) 〈x0,x7〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX1  (Byte 〈xE,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX0  (Byte 〈xF,xD〉) 〈x0,x5〉
+  quadrupleT ???? (anyOP HC05 BSR) MODE_IMM1     (Byte 〈xA,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_IMM1EXT  (Byte 〈xB,xD〉) 〈x0,x5〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_IMM2     (Byte 〈xC,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX2ADD (Byte 〈xD,xD〉) 〈x0,x7〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX1ADD (Byte 〈xE,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX0ADD (Byte 〈xF,xD〉) 〈x0,x5〉
 ].
 
 definition opcode_table_HC05_20 ≝
@@ -378,4 +378,3 @@ definition opcode_table_HC05 ≝
  opcode_table_HC05_21 @ opcode_table_HC05_22 @ opcode_table_HC05_23 @ opcode_table_HC05_24 @
  opcode_table_HC05_25 @ opcode_table_HC05_26 @ opcode_table_HC05_27 @ opcode_table_HC05_28 @
  opcode_table_HC05_29 @ opcode_table_HC05_30 @ opcode_table_HC05_31.
-
diff --git a/helm/software/matita/library/freescale/table_HC05_tests.ma b/helm/software/matita/library/freescale/table_HC05_tests.ma
index 5f92c132ec5249eb281eb99ecdf8891aaf35c817..50f8057039ce3de5f2b2d421f4fef6fc301ed632 100644 (file)
--- a/helm/software/matita/library/freescale/table_HC05_tests.ma
+++ b/helm/software/matita/library/freescale/table_HC05_tests.ma
@@ -26,8 +26,6 @@
 
 include "freescale/table_HC05.ma".
 
-(* CORRETTEZZA *)
-
 (* HC05: opcode non implementati come da manuale *)
 definition HC05_not_impl_byte ≝
  [〈x3,x1〉;〈x3,x2〉;〈x3,x5〉;〈x3,xB〉;〈x3,xE〉
@@ -62,7 +60,7 @@ qed.
 
 (* HC05: modalita' non implementate come da manuale *)
 definition HC05_not_impl_mode ≝
- [ MODE_INHH ; MODE_IMM2 ; MODE_SP1 ; MODE_SP2 ; MODE_DIR1_to_DIR1
+ [ MODE_INHH ; MODE_SP1 ; MODE_SP2 ; MODE_DIR1_to_DIR1
  ; MODE_IMM1_to_DIR1 ; MODE_IX0p_to_DIR1 ; MODE_DIR1_to_IX0p
  ; MODE_INHA_and_IMM1 ; MODE_INHX_and_IMM1 ; MODE_IMM1_and_IMM1
  ; MODE_DIR1_and_IMM1 ; MODE_IX0_and_IMM1 ; MODE_IX0p_and_IMM1
@@ -87,9 +85,11 @@ lemma ok_mode_table_HC05 : forall_instr_mode (λi.
  reflexivity.
 qed.
 
+(*
 lemma ok_OpIm_table_HC05 :
  forall_instr_mode (λi:instr_mode.
  forall_opcode     (λop:opcode.
   leb (get_OpIm_count HC05 (anyOP HC05 op) i 0 opcode_table_HC05) 1)) = true.
  reflexivity.
 qed.
+*)
diff --git a/helm/software/matita/library/freescale/table_HC08.ma b/helm/software/matita/library/freescale/table_HC08.ma
index 7448901115c1671de86af205a07ac86c435668fb..1975fd8b1db3f78ee1d1af7749b46ec194eeae4e 100644 (file)
--- a/helm/software/matita/library/freescale/table_HC08.ma
+++ b/helm/software/matita/library/freescale/table_HC08.ma
@@ -308,21 +308,21 @@ definition opcode_table_HC08_20 ≝
 
 definition opcode_table_HC08_21 ≝
 [
-  quadrupleT ???? (anyOP HC08 JMP) MODE_DIR1 (Byte 〈xB,xC〉) 〈x0,x2〉
-; quadrupleT ???? (anyOP HC08 JMP) MODE_DIR2 (Byte 〈xC,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HC08 JMP) MODE_IX2  (Byte 〈xD,xC〉) 〈x0,x4〉
-; quadrupleT ???? (anyOP HC08 JMP) MODE_IX1  (Byte 〈xE,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HC08 JMP) MODE_IX0  (Byte 〈xF,xC〉) 〈x0,x3〉
+  quadrupleT ???? (anyOP HC08 JMP) MODE_IMM1EXT  (Byte 〈xB,xC〉) 〈x0,x2〉
+; quadrupleT ???? (anyOP HC08 JMP) MODE_IMM2     (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HC08 JMP) MODE_INHX2ADD (Byte 〈xD,xC〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP HC08 JMP) MODE_INHX1ADD (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HC08 JMP) MODE_INHX0ADD (Byte 〈xF,xC〉) 〈x0,x3〉
 ].
 
 definition opcode_table_HC08_22 ≝
 [
-  quadrupleT ???? (anyOP HC08 BSR) MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x4〉
-; quadrupleT ???? (anyOP HC08 JSR) MODE_DIR1 (Byte 〈xB,xD〉) 〈x0,x4〉
-; quadrupleT ???? (anyOP HC08 JSR) MODE_DIR2 (Byte 〈xC,xD〉) 〈x0,x5〉
-; quadrupleT ???? (anyOP HC08 JSR) MODE_IX2  (Byte 〈xD,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC08 JSR) MODE_IX1  (Byte 〈xE,xD〉) 〈x0,x5〉
-; quadrupleT ???? (anyOP HC08 JSR) MODE_IX0  (Byte 〈xF,xD〉) 〈x0,x4〉
+  quadrupleT ???? (anyOP HC08 BSR) MODE_IMM1     (Byte 〈xA,xD〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP HC08 JSR) MODE_IMM1EXT  (Byte 〈xB,xD〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP HC08 JSR) MODE_IMM2     (Byte 〈xC,xD〉) 〈x0,x5〉
+; quadrupleT ???? (anyOP HC08 JSR) MODE_INHX2ADD (Byte 〈xD,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC08 JSR) MODE_INHX1ADD (Byte 〈xE,xD〉) 〈x0,x5〉
+; quadrupleT ???? (anyOP HC08 JSR) MODE_INHX0ADD (Byte 〈xF,xD〉) 〈x0,x4〉
 ].
 
 definition opcode_table_HC08_23 ≝
@@ -475,4 +475,3 @@ opcode_table_HC08_21 @ opcode_table_HC08_22 @ opcode_table_HC08_23 @ opcode_tabl
 opcode_table_HC08_25 @ opcode_table_HC08_26 @ opcode_table_HC08_27 @ opcode_table_HC08_28 @
 opcode_table_HC08_29 @ opcode_table_HC08_30 @ opcode_table_HC08_31 @ opcode_table_HC08_32 @
 opcode_table_HC08_33 @ opcode_table_HC08_34 @ opcode_table_HC08_35.
-
diff --git a/helm/software/matita/library/freescale/table_HC08_tests.ma b/helm/software/matita/library/freescale/table_HC08_tests.ma
index be7b06b396200878391c9b58e50deedc0a635696..d8981d61af1a6676aa346b7888cb59ee7f0c0332 100644 (file)
--- a/helm/software/matita/library/freescale/table_HC08_tests.ma
+++ b/helm/software/matita/library/freescale/table_HC08_tests.ma
@@ -26,8 +26,6 @@
 
 include "freescale/table_HC08.ma".
 
-(* CORRETTEZZA *)
-
 (* HC08: opcode non implementati come da manuale (byte) *)
 definition HC08_not_impl_byte ≝
  [〈x3,x2〉;〈x3,xE〉
@@ -116,10 +114,11 @@ lemma ok_mode_table_HC08 : forall_instr_mode (λi.
  reflexivity.
 qed.
 
+(*
 lemma ok_OpIm_table_HC08 :
  forall_instr_mode (λi:instr_mode.
  forall_opcode     (λop:opcode.
   leb (get_OpIm_count HC08 (anyOP HC08 op) i 0 opcode_table_HC08) 1)) = true.
  reflexivity.
 qed.
-
+*)
diff --git a/helm/software/matita/library/freescale/table_HCS08.ma b/helm/software/matita/library/freescale/table_HCS08.ma
index 522c98d48efcd2a9cfb70b1818c8d5ef57142920..bb5b71f3195f2061fe6e39d6805f3c991e3d50b8 100644 (file)
--- a/helm/software/matita/library/freescale/table_HCS08.ma
+++ b/helm/software/matita/library/freescale/table_HCS08.ma
@@ -320,21 +320,21 @@ definition opcode_table_HCS08_20 ≝
 
 definition opcode_table_HCS08_21 ≝
 [
-  quadrupleT ???? (anyOP HCS08 JMP) MODE_DIR1 (Byte 〈xB,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HCS08 JMP) MODE_DIR2 (Byte 〈xC,xC〉) 〈x0,x4〉
-; quadrupleT ???? (anyOP HCS08 JMP) MODE_IX2  (Byte 〈xD,xC〉) 〈x0,x4〉
-; quadrupleT ???? (anyOP HCS08 JMP) MODE_IX1  (Byte 〈xE,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HCS08 JMP) MODE_IX0  (Byte 〈xF,xC〉) 〈x0,x3〉
+  quadrupleT ???? (anyOP HCS08 JMP) MODE_IMM1EXT  (Byte 〈xB,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HCS08 JMP) MODE_IMM2     (Byte 〈xC,xC〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP HCS08 JMP) MODE_INHX2ADD (Byte 〈xD,xC〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP HCS08 JMP) MODE_INHX1ADD (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HCS08 JMP) MODE_INHX0ADD (Byte 〈xF,xC〉) 〈x0,x3〉
 ].
 
 definition opcode_table_HCS08_22 ≝
 [
-  quadrupleT ???? (anyOP HCS08 BSR) MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x5〉
-; quadrupleT ???? (anyOP HCS08 JSR) MODE_DIR1 (Byte 〈xB,xD〉) 〈x0,x5〉
-; quadrupleT ???? (anyOP HCS08 JSR) MODE_DIR2 (Byte 〈xC,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HCS08 JSR) MODE_IX2  (Byte 〈xD,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HCS08 JSR) MODE_IX1  (Byte 〈xE,xD〉) 〈x0,x5〉
-; quadrupleT ???? (anyOP HCS08 JSR) MODE_IX0  (Byte 〈xF,xD〉) 〈x0,x5〉
+  quadrupleT ???? (anyOP HCS08 BSR) MODE_IMM1     (Byte 〈xA,xD〉) 〈x0,x5〉
+; quadrupleT ???? (anyOP HCS08 JSR) MODE_IMM1EXT  (Byte 〈xB,xD〉) 〈x0,x5〉
+; quadrupleT ???? (anyOP HCS08 JSR) MODE_IMM2     (Byte 〈xC,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HCS08 JSR) MODE_INHX2ADD (Byte 〈xD,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HCS08 JSR) MODE_INHX1ADD (Byte 〈xE,xD〉) 〈x0,x5〉
+; quadrupleT ???? (anyOP HCS08 JSR) MODE_INHX0ADD (Byte 〈xF,xD〉) 〈x0,x5〉
 ].
 
 definition opcode_table_HCS08_23 ≝
@@ -487,4 +487,3 @@ opcode_table_HCS08_21 @ opcode_table_HCS08_22 @ opcode_table_HCS08_23 @ opcode_t
 opcode_table_HCS08_25 @ opcode_table_HCS08_26 @ opcode_table_HCS08_27 @ opcode_table_HCS08_28 @
 opcode_table_HCS08_29 @ opcode_table_HCS08_30 @ opcode_table_HCS08_31 @ opcode_table_HCS08_32 @
 opcode_table_HCS08_33 @ opcode_table_HCS08_34 @ opcode_table_HCS08_35.
-
diff --git a/helm/software/matita/library/freescale/table_HCS08_tests.ma b/helm/software/matita/library/freescale/table_HCS08_tests.ma
index 011d19313f089a6e576527383222867708770ca5..277b8197bf9adaa27c434d13fe6eee8303590c2e 100644 (file)
--- a/helm/software/matita/library/freescale/table_HCS08_tests.ma
+++ b/helm/software/matita/library/freescale/table_HCS08_tests.ma
@@ -26,8 +26,6 @@
 
 include "freescale/table_HCS08.ma".
 
-(* CORRETTEZZA *)
-
 (* HCS08: opcode non implementati come da manuale (byte) *)
 definition HCS08_not_impl_byte ≝
  [〈x8,xD〉
@@ -111,10 +109,11 @@ lemma ok_mode_table_HCS08 : forall_instr_mode (λi.
  reflexivity.
 qed.
 
+(*
 lemma ok_OpIm_table_HCS08 :
  forall_instr_mode (λi:instr_mode.
  forall_opcode     (λop:opcode.
   leb (get_OpIm_count HCS08 (anyOP HCS08 op) i 0 opcode_table_HCS08) 1)) = true.
  reflexivity.
 qed.
-
+*)
diff --git a/helm/software/matita/library/freescale/table_RS08.ma b/helm/software/matita/library/freescale/table_RS08.ma
index 522d87efeefa1279d95fde0e95e094a1b0e04776..6e16f55a625899e3afaf23d0eb9e4e079bac92d2 100644 (file)
--- a/helm/software/matita/library/freescale/table_RS08.ma
+++ b/helm/software/matita/library/freescale/table_RS08.ma
@@ -249,13 +249,13 @@ definition opcode_table_RS08_16 ≝
 
 definition opcode_table_RS08_17 ≝
 [
-  quadrupleT ???? (anyOP RS08 JMP) MODE_DIR2 (Byte 〈xB,xC〉) 〈x0,x4〉
+  quadrupleT ???? (anyOP RS08 JMP) MODE_IMM2 (Byte 〈xB,xC〉) 〈x0,x4〉
 ].
 
 definition opcode_table_RS08_18 ≝
 [
   quadrupleT ???? (anyOP RS08 BSR) MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP RS08 JSR) MODE_DIR2 (Byte 〈xB,xD〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP RS08 JSR) MODE_IMM2 (Byte 〈xB,xD〉) 〈x0,x4〉
 ].
 
 definition opcode_table_RS08_19 ≝
@@ -396,4 +396,3 @@ opcode_table_RS08_13 @ opcode_table_RS08_14 @ opcode_table_RS08_15 @ opcode_tabl
 opcode_table_RS08_17 @ opcode_table_RS08_18 @ opcode_table_RS08_19 @ opcode_table_RS08_20 @
 opcode_table_RS08_21 @ opcode_table_RS08_22 @ opcode_table_RS08_23 @ opcode_table_RS08_24 @
 opcode_table_RS08_25 @ opcode_table_RS08_26 @ opcode_table_RS08_27.
-
diff --git a/helm/software/matita/library/freescale/table_RS08_tests.ma b/helm/software/matita/library/freescale/table_RS08_tests.ma
index 8c1b3cd87ea526ce6b5c5a2539fb475338f521ea..0ad95525eb02a07dd8cc09fde983079dd5581215 100644 (file)
--- a/helm/software/matita/library/freescale/table_RS08_tests.ma
+++ b/helm/software/matita/library/freescale/table_RS08_tests.ma
@@ -26,8 +26,6 @@
 
 include "freescale/table_RS08.ma".
 
-(* CORRETTEZZA *)
-
 (* RS08: opcode non implementati come da manuale *)
 definition RS08_not_impl_byte ≝
  [〈x3,x2〉;〈x3,x3〉;〈x3,xD〉
@@ -59,7 +57,8 @@ qed.
 
 (* RS08: modalita' non implementate come da manuale *)
 definition RS08_not_impl_mode ≝
- [ MODE_INHX ; MODE_INHH ; MODE_IMM2 ; MODE_IX0 ; MODE_IX1 ; MODE_IX2 ; MODE_SP1 ; MODE_SP2
+ [ MODE_INHX ; MODE_INHH ; MODE_INHX0ADD ; MODE_INHX1ADD ; MODE_INHX2ADD ; MODE_IMM1EXT
+ ; MODE_DIR2 ; MODE_IX0 ; MODE_IX1 ; MODE_IX2 ; MODE_SP1 ; MODE_SP2
  ; MODE_IX0p_to_DIR1 ; MODE_DIR1_to_IX0p ; MODE_INHX_and_IMM1 ; MODE_IX0_and_IMM1
  ; MODE_IX0p_and_IMM1 ; MODE_IX1_and_IMM1 ; MODE_IX1p_and_IMM1 ; MODE_SP1_and_IMM1 ].
 
@@ -70,10 +69,11 @@ lemma ok_mode_table_RS08 : forall_instr_mode (λi.
  reflexivity.
 qed.
 
+(*
 lemma ok_OpIm_table_RS08 :
  forall_instr_mode (λi:instr_mode.
  forall_opcode     (λop:opcode.
   leb (get_OpIm_count RS08 (anyOP RS08 op) i 0 opcode_table_RS08) 1)) = true.
  reflexivity.
 qed.
-
+*)
diff --git a/helm/software/matita/library/freescale/translation.ma b/helm/software/matita/library/freescale/translation.ma
index af54b87dd9f3fc881840c26bc900d917cfafa5ab..0463cff55a25cf15797f17560fa496b5d7183495 100644 (file)
--- a/helm/software/matita/library/freescale/translation.ma
+++ b/helm/software/matita/library/freescale/translation.ma
@@ -81,7 +81,11 @@ inductive MA_check : instr_mode → Type ≝
 | maINHA             : MA_check MODE_INHA
 | maINHX             : MA_check MODE_INHX
 | maINHH             : MA_check MODE_INHH
+| maINHX0ADD         : MA_check MODE_INHX0ADD
+| maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
+| maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
 | maIMM1             : byte8  → MA_check MODE_IMM1
+| maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
 | maIMM2             : word16 → MA_check MODE_IMM2
 | maDIR1             : byte8  → MA_check MODE_DIR1
 | maDIR2             : word16 → MA_check MODE_DIR2
@@ -125,8 +129,13 @@ definition args_picker ≝
   | maINHA   ⇒ nil ? 
   | maINHX   ⇒ nil ? 
   | maINHH   ⇒ nil ?
+  (* inherent address: legale se nessun operando/1 byte/1 word *)
+  | maINHX0ADD ⇒ nil ?
+  | maINHX1ADD b ⇒ [ TByte m b ]
+  | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]    
   (* _0/1/2: legale se nessun operando/1 byte/1 word *)
   | maIMM1 b ⇒ [ TByte m b ]
+  | maIMM1EXT b ⇒ [ TByte m b ]
   | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
   | maDIR1 b ⇒ [ TByte m b ]
   | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
Unnamed repository; edit this file 'description' to name the repository.