From 7845d9d0221d94418beecf3d7c3aed3efb2af7fc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 13 Mar 2008 14:01:52 +0000 Subject: [PATCH] New version of freescale: 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) --- helm/software/matita/library/depends | 184 ++--- .../matita/library/freescale/load_write.ma | 64 +- .../matita/library/freescale/medium_tests.ma | 763 ++++++++++++++---- .../library/freescale/medium_tests_lemmas.ma | 145 ++-- .../library/freescale/medium_tests_tools.ma | 6 + .../matita/library/freescale/multivm.ma | 10 +- .../matita/library/freescale/opcode.ma | 175 ++-- .../matita/library/freescale/table_HC05.ma | 23 +- .../library/freescale/table_HC05_tests.ma | 6 +- .../matita/library/freescale/table_HC08.ma | 23 +- .../library/freescale/table_HC08_tests.ma | 5 +- .../matita/library/freescale/table_HCS08.ma | 23 +- .../library/freescale/table_HCS08_tests.ma | 5 +- .../matita/library/freescale/table_RS08.ma | 5 +- .../library/freescale/table_RS08_tests.ma | 8 +- .../matita/library/freescale/translation.ma | 9 + 16 files changed, 973 insertions(+), 481 deletions(-) diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 59977807b..e02dc916f 100644 --- 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 a5fae5375..28c78b6bb 100644 --- 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 20a0da441..90762c5fb 100644 --- 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;divisor1951 !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 44f770ae3..81505ac26 100644 --- 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 fcdda667a..f1e394d22 100644 --- 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 2e63c2054..b78efba70 100644 --- 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 62199d7d3..47312085f 100644 --- 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 e0c9b33e7..6938cd3e6 100644 --- 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 5f92c132e..50f805703 100644 --- 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 744890111..1975fd8b1 100644 --- 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 be7b06b39..d8981d61a 100644 --- 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 522c98d48..bb5b71f31 100644 --- 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 011d19313..277b8197b 100644 --- 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 522d87efe..6e16f55a6 100644 --- 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 8c1b3cd87..0ad95525e 100644 --- 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 af54b87dd..0463cff55 100644 --- 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) ] -- 2.39.2